Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

LatticeBRSTFullOriginalRaising

Abstract

LatticeBRSTFullOriginalRaising

Original full BRST remainder on the original all-charge lattice matter tensor original occupation bc ghost carrier. The construction reuses the accepted inverse-Gram Sugawara cancellation and original asymmetric locally finite mode bounds. It assembles the literal Q=T+id tensor Qg, subtracts original d0 and retains the zero-mode charge-energy contribution. Both that contribution and the endpoint-subtracted finite expression raise signed degree; genuine h composes with the inference. All original integral charges, including zero, are covered.

The formal scope of this supplier is the seven public endpoints below. The upstream source audits at https://github.com/the-omega-institute/trureturing/issues/25604 remain 146 unfinished obligations and are not certificates for this module. The seven current public endpoints in this module have a separate unfinished source audit at https://github.com/the-omega-institute/trureturing/issues/25770; that issue records their exact source telescopes, compiled statement/type IDs, and missing source-selection, reconstruction, realization/readout, law, family-variation, sensitivity/dependence, and registration evidence. Native compilation establishes only the exact Lean statements, not source fidelity, physical realization, shell stability or shell bounds. Physical HPL, cohomology, no-ghost, Monster/moonshine, a realized VOA/CFT and fusion theory, original BRST/string completion and AdS-CFT remain active goals. The live shell59141 and energy-shell72841 outputs are neither imported nor assumed.

Definition 1.1 (commonModes).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTFullOriginalRaising.commonModes

Formalization. D5/S3/VertexAlgebra/Lattice/LatticeBRSTFullOriginalRaising.commonModes (✓ std3).

Source. Repository-derived.

Commentary.

The finite union of actual state-action supports for the original matter coupling and the signed quartet d0 modes, with zero inserted once. The set is reconstructed for each original algebraic tensor input; it is not a uniform cutoff.

Theorem 1.2 (totalCharge_sub_d0_finite_capture).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTFullOriginalRaising.totalCharge_sub_d0_finite_capture

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

Source. Repository-derived.

Commentary.

On every original State D and every integral charge p, literal totalCharge minus d0 equals finiteRemainder evaluated at commonModes of that input plus the exact chargeEnergy(p) times identity tensor c0. This all-state algebraic identity uses no inverse-Gram hypothesis and does not silently cancel the energy endpoint.

Theorem 1.3 (full_remainder_fixed_charge_basis_raises).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTFullOriginalRaising.full_remainder_fixed_charge_basis_raises

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

Source. Repository-derived.

Commentary.

For the original actualBasis, any input basis index of integral charge p and any nonzero output coefficient of the literal full Q-d0 satisfy degree(input)+1 <= degree(output). Both HG=1 and GH=1 are retained; p=0 and every signed mode remain included, with no positivity or pPlus nonzero premise.

Theorem 1.4 (h_full_remainder_fixed_charge_basis_raises).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTFullOriginalRaising.h_full_remainder_fixed_charge_basis_raises

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

Source. Repository-derived.

Commentary.

The actual product of the genuine quartet h with original full Q-d0 satisfies the same fixed-charge basis strict raising. The restored energy*c0 contribution is treated as degree +1 and the genuine h as degree zero.

Definition 1.5 (HasCharge).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTFullOriginalRaising.HasCharge

Formalization. D5/S3/VertexAlgebra/Lattice/LatticeBRSTFullOriginalRaising.HasCharge (✓ std3).

Source. Repository-derived.

Commentary.

A state has original integral charge p precisely when every nonzero coefficient in the actual original tensor basis has charge p. This is a predicate on original states, not an operator replacement or a physical-shell certificate.

Theorem 1.6 (original_operators_preserve_charge).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTFullOriginalRaising.original_operators_preserve_charge

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

Source. Repository-derived.

Commentary.

Literal original totalCharge, original d0 and the genuine h preserve HasCharge on every algebraic tensor state, with no inverse-Gram, target-equation, nilpotence, degree or shell-stability premise.

Theorem 1.7 (full_remainder_fixed_charge_vectors).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeBRSTFullOriginalRaising.full_remainder_fixed_charge_vectors

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

Source. Repository-derived.

Commentary.

For an original state of arbitrary integral charge p whose actual basis support has a supplied signed integer lower degree bound a, both literal (Q-d0)v and actual h(Q-d0)v retain charge p and have lower degree bound a+1. The two inverse-Gram equations remain explicit. The input bound is not a theorem of physical-shell boundedness.

References