Alphabeta Math
CounterexampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The whole partition Fock space is not the basic representation

Statement refuted

The assertion that the entire partition Fock module F is the basic representation, i.e. that F=M=Uq(g)∣∅⟩≅V(Λ0) for every finite e≥2, is false. For every finite e≥2 the Fock module is strictly larger than M: the raw basis vector ∣1e⟩ is not in M, and its ambient lower lift G(1e) is also not in M. The full field decomposition is F=⨁k≥0V(Λ0−kδ)⊕p(k), the Λ0 multiplicity is 1, and the higher constituents are nonzero; consequently the full crystal has all partitions as vertices while its empty component is exactly the e-regular partitions.

Facts & Assumptions

Given: The partition Fock space with its crystal and global basis, the module M=V(Λ0), and the decomposition theorem.

[F1]

The empty component of the full crystal is exactly the e-regular partitions and equals the crystal of M; the full crystal is a graph on all partitions; the decomposition is F=⨁kV(Λ0−kδ)⊕p(k) with choice used only there (The empty component is the highest weight crystal B(Λ0), The Axiom of Choice).

[F2]

M is the simple integrable module generated by the vacuum and receives the lower global basis of the empty component (The empty partition generates an integrable highest weight submodule of highest weight Λ0, The basic representation global basis is unitriangular in the partition basis).

[F3]

The top weight Λ0 is maximal, so the top isotypic splitting of the crystal lattice gives F0∩M with residue basis exactly the empty component; the shape 1e has all parts equal and multiplicity e, so it is not e-regular (Uniqueness: crystal bases of integrable modules decompose into highest weight crystals, The level-one partition Fock space and node residues).

Verification

1.1F1givenalgebra

Strictness. By [F1] the full field decomposition contains the summands V(Λ0−kδ) for every k≥0 with multiplicity p(k)≥1, and the Λ0 summand occurs with multiplicity p(0)=1; since p(k)≥1 for k≥1 and those constituents are nonzero, F is strictly larger than its Λ0 constituent M.

1.2F1F2F3algebra

Raw-vector exclusion. The shape 1e is not e-regular: all its parts equal 1 and occur e times, so it lies outside the empty component by [F1]; since the residue basis of F0∩M is exactly the empty component by [F3], every vector in F0∩M has residue a combination of regular labels. The raw vector ∣1e⟩ has nonzero residue in F0/qF0 equal to the nonregular shape 1e, so ∣1e⟩∉M; the same argument applies to G(1e), which is congruent to the same shape modulo qF0.

2.1step 1.1step 1.2∎

Conclusion. The whole partition Fock space is not the basic representation: it has strictly more constituents than the single V(Λ0), and even the explicit raw and lower-lift vectors ∣1e⟩ and G(1e) lie outside M; the nonregular ambient lower vectors are not a basis of a single highest module.

Remarks

  • The decomposition theorem used in step 1.1 is a batch-7 supplier still under construction at authoring time, and the Axiom of Choice is inherited through it; the exclusion of step 2.1 is a finite residue computation and does not itself use choice.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

33 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources