Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Nonvacuity from the original vacuum coefficient

Abstract

Nonvacuity from the original vacuum coefficient

The separating functional is the zero lattice charge, constant matter polynomial, empty ghost occupation coefficient on all original states. A negative matter current has zero constant row; this proves the same row vanishes for each negative normally ordered Sugawara mode. Every cubic ghost normal-order branch begins with a creator. In the coupling sum the creator ghost row kills m >= -1 and the negative matter row kills m <= -2. Genuine finite action support justifies each finsum map. The functional kills totalCharge on all states and evaluates the actual vacuum to one, then descends to the actual quotient.

Source provenance: the completed original cohomology source supplier, flight 6ae9ead6048411c28e0cbc27 attempt 1, repaired by Codex CLI in the assigned linked native worktree. Original Bakalov–Kac lattice, Scott Carnahan vertexAlg residue/field, Kalle Kytola Sugawara and Mathlib attribution remains in the supplier chain. No literature novelty, independent review, official acceptance, full string theory, or AdS/CFT completion is claimed.

Theorem 1.1 (The coefficient annihilates the charge on every original state).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyNonvacuity.vacuumCoeff_charge

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyNonvacuity.vacuumCoeff_charge (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact compiled statement and source dependencies determine the scope. Critical quotient results use rank 26 and both inverse Gram laws; the coefficient annihilation and original Leibniz results retain their unrestricted D and H telescope. Semantic registration remains subject to its native audit result; no validated certificate is inferred from compilation.

Theorem 1.2 (The actual vacuum coefficient is one).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyNonvacuity.vacuumCoeff_vacuum

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyNonvacuity.vacuumCoeff_vacuum (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact compiled statement and source dependencies determine the scope. Critical quotient results use rank 26 and both inverse Gram laws; the coefficient annihilation and original Leibniz results retain their unrestricted D and H telescope. Semantic registration remains subject to its native audit result; no validated certificate is inferred from compilation.

Theorem 1.3 (The original vacuum is not exact).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyNonvacuity.vacuum_not_boundary

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyNonvacuity.vacuum_not_boundary (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact compiled statement and source dependencies determine the scope. Critical quotient results use rank 26 and both inverse Gram laws; the coefficient annihilation and original Leibniz results retain their unrestricted D and H telescope. Semantic registration remains subject to its native audit result; no validated certificate is inferred from compilation.

Theorem 1.4 (The descended evaluation separates the vacuum).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyNonvacuity.vacuumEvaluation_vacuum

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyNonvacuity.vacuumEvaluation_vacuum (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact compiled statement and source dependencies determine the scope. Critical quotient results use rank 26 and both inverse Gram laws; the coefficient annihilation and original Leibniz results retain their unrestricted D and H telescope. Semantic registration remains subject to its native audit result; no validated certificate is inferred from compilation.

Theorem 1.5 (Nontriviality of the actual critical cohomology).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyNonvacuity.cohomology_nontrivial

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyNonvacuity.cohomology_nontrivial (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact compiled statement and source dependencies determine the scope. Critical quotient results use rank 26 and both inverse Gram laws; the coefficient annihilation and original Leibniz results retain their unrestricted D and H telescope. Semantic registration remains subject to its native audit result; no validated certificate is inferred from compilation.

References