Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Inherited laws on original BRST cohomology

Abstract

Inherited laws on original BRST cohomology

The descended field retains vacuum, creation, translation covariance, parity, and signed locality. Locality uses homogeneous cycle lifts proved by the actual projections and an exponent uniform in the input class. No Jacobi, image closure, energy positivity, no-ghost property, or nonzero-class assumption is added. The nontriviality equivalence identifies vacuum non-exactness; the separate coefficient-functional module proves it.

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 (Descended vacuum field).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyLaws.vacuum_field

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyLaws.vacuum_field (✓ 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 (Creation on the quotient).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyLaws.creation

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyLaws.creation (✓ 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 (Translation covariance).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyLaws.covariance

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyLaws.covariance (✓ 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 (Inherited parity law).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyLaws.field_parity

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyLaws.field_parity (✓ 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 (Uniform signed locality).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyLaws.locality

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyLaws.locality (✓ 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.6 (Exact vacuum non-exactness criterion).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyLaws.nontrivial_iff_vacuum_not_boundary

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyLaws.nontrivial_iff_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.

References