Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Original critical BRST cohomology fields

Abstract

Original critical BRST cohomology fields

The differential is the literal totalCharge D H on the original tensor State D. Rank 26 and both inverse Gram identities discharge its square anomaly. The quotient is the actual kernel modulo the actual image, embedded by that proved square-zero law. The mixed-parity Leibniz law proves closure of cycles and image stability in both field arguments at every integer mode. Spectral projections of the original parity give homogeneous cycle lifts of homogeneous classes without requiring an arbitrary lift to be homogeneous. All lower truncation is inherited from the actual field action.

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 (Leibniz law for arbitrary mixed states).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyField.charge_mode

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyField.charge_mode (✓ 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 image inside the actual kernel).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyField.boundaries_subtype_range

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyField.boundaries_subtype_range (✓ 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 (Descent in both cycle representatives for every integer mode).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyField.mode_representatives

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyField.mode_representatives (✓ 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 (Homogeneous class lifts through actual parity projections).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyField.homogeneous_cycle_lift

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyField.homogeneous_cycle_lift (✓ 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 (Lower truncation of descended field action).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyField.mode_truncation

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Lattice/LatticeBRSTCohomologyField.mode_truncation (✓ 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