Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Original relative-shell coefficient degree bound

Abstract

Original relative-shell coefficient degree bound

The original state carrier is Carrier D tensor[Complex] CountableOccupationFock.Fock. The shell is literally (fixedMomentum D p intersect ker(ghostB D 0)) intersect ker(matterMode D H 0 + ghostVirasoro D 0), with the unshifted total zero mode. D is arbitrary LatticeData, F is its original NullFrame, B is any finite basis of F.K, and H obeys exactly the two displayed inverse-Gram equations. All original integral charges p, including zero, remain in scope. There is no rank-26, nonzero-momentum, Gram-positivity or nilpotence assumption.

For an actualBasis index i=((q,m),S), set E(m)=sum over (label,r) of m(label,r)*(r+1). The original filtration degree is exponentDegree(m)+charge(S)-1, with signed matter weights +1,-1,0. Put N=(1-chargeEnergy D p).toNat. The result proves q=p, 3 not in S, E(m)+relativeEnergy(S)=1-chargeEnergy D p, and -N <= degree(i) <= N. The empty state is included; only the selected coefficient is required nonzero.

The ghost estimate is |charge(S)-1| <= count(S) <= relativeEnergy(S). Site 1 is treated as an occupied negative-energy site or as the missing-site-1 hole in count, exactly as in the native occupation carrier. The exclusion of site 3 is deduced from the original b(0) kernel. Positive regular site energies provide the count bound; relativeEnergy nonnegativity does not assert positivity of a Hermitian form.

The tensor/coordinate bridge first extracts the actual original coefficient slice at fixed charge q and occupation S. Applying NullFrame.coordinateEquiv B gives coordinateSlice, whose coefficient at m equals actualBasis.repr x i for every state x, by equality of linear maps on the original tensor basis. A nonzero coordinate coefficient forces the original slice to be nonzero, hence some original coefficient is nonzero. Native mem_relativeMassShell_iff fixes its charge, b(0) exclusion and integer energy. Every original monomial in the same slice then has the same oscillatorEnergy, by subtracting their shell equations. Native NullFrame.frequency_grading transfers this weighted homogeneity through the actual polynomial substitution. Thus the selected coordinate coefficient has exactly that frequency energy. No coefficientwise identification between unrelated monomials is assumed.

The final estimate uses the finite triangle inequality to bound |exponentDegree(m)| by E(m), combines it with the original signed ghost estimate, and substitutes the derived shell equation. Nonnegative E and relativeEnergy imply chargeEnergy D p <= 1 whenever the selected coefficient is nonzero, so massShellCutoff_cast applies. For charge energy greater than one, use native LatticeRelativeMassShell.relativeMassShell_eq_bot_of_one_lt directly; no duplicate wrapper is retained.

This unit supplies the original coefficient degree interval needed before HPL truncation. It does not prove a raising theorem, HPL, nilpotence, cohomology, no-ghost, a physical string realization, Monster moonshine, complete VOA/CFT, anomaly or fusion completion, or AdS/CFT. The proof is repo-derived algebraic content; no literature novelty is claimed.

Registration audit is unfinished. The existing DependentFamily enrollment alone supplies neither a source-family reconstruction for the tensor/coordinate and degree readouts nor the whole-family variation, sensitivity and observational-dependence proofs for these exact telescopes. No declared_validated registration is claimed. See https://github.com/the-omega-institute/trureturing/issues/25849 for all six public theorem targets and their concrete missing evidence.

Theorem 1.1 (ghost_abs_charge_sub_one_le_count).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeRelativeShellDegreeBounds.ghost_abs_charge_sub_one_le_count

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

Source. Repository-derived.

Commentary.

For every finite occupation excluding site 3, the original signed ghost charge minus one has absolute value at most the original quartet count. The proof splits on actual occupation of site 1: its removal cancels the charge shift when present; its absence contributes the extra hole counted by count.

Exact Lean telescope: theorem ghost_abs_charge_sub_one_le_count (S : Finset ℕ) (h3 : 3 ∉ S) : |charge S - 1| ≤ (count S : ℤ)

Theorem 1.2 (ghost_count_le_relativeEnergy).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeRelativeShellDegreeBounds.ghost_count_le_relativeEnergy

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

Source. Repository-derived.

Commentary.

Each regular occupied site has positive integer siteEnergy, hence contributes at least one. The native relativeEnergy_split accounts exactly for the absent-site-1 hole. This proves domination of the original quartet count for every occupation excluding site 3.

Exact Lean telescope: theorem ghost_count_le_relativeEnergy (S : Finset ℕ) (h3 : 3 ∉ S) : (count S : ℤ) ≤ relativeEnergy S

Definition 1.3 (frameEnergy).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeRelativeShellDegreeBounds.frameEnergy

Formalization. D5/S3/VertexAlgebra/Lattice/LatticeRelativeShellDegreeBounds.frameEnergy (✓ std3).

Source. Repository-derived.

Commentary.

The natural weighted exponent sum uses frequencyWeight(label,r)=r+1, the original creation frequency. No sign of the Gram form enters this sum.

Exact Lean telescope: def frameEnergy {t : ℕ} (m : Exponents t) : ℕ

Theorem 1.4 (abs_exponentDegree_le_frameEnergy).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeRelativeShellDegreeBounds.abs_exponentDegree_le_frameEnergy

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

Source. Repository-derived.

Commentary.

The original signed exponentDegree is the sum of exponent multiplicity times variableWeight, with plus weight 1, minus weight -1 and transverse weight 0. The finite triangle inequality and 1 <= r+1 bound it by the actual frequency-weighted sum.

Exact Lean telescope: theorem abs_exponentDegree_le_frameEnergy {t : ℕ} (m : Exponents t) : |exponentDegree m| ≤ (frameEnergy m : ℤ)

Definition 1.5 (originalSlice).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeRelativeShellDegreeBounds.originalSlice

Formalization. D5/S3/VertexAlgebra/Lattice/LatticeRelativeShellDegreeBounds.originalSlice (✓ std3).

Source. Repository-derived.

Commentary.

This linear map extracts the original tensor coefficient at ((p,d),S) for every original oscillator exponent d, using an injective comapDomain and the actual tensorCoeffEquiv. It leaves the original charge and ghost occupation untouched.

Exact Lean telescope: def originalSlice (D : LatticeData) (p : Charge D) (S : Finset ℕ) : State D →ₗ[ℂ] Oscillator D

Theorem 1.6 (originalSlice_coeff).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeRelativeShellDegreeBounds.originalSlice_coeff

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

Source. Repository-derived.

Commentary.

The extracted polynomial coefficient is exactly the original tensor-basis coefficient; it is not a new shell definition or an energy certificate. This identity is consumed in the tensor bridge and the shell support argument.

Exact Lean telescope: @[simp] theorem originalSlice_coeff (D : LatticeData) (x : State D) (p : Charge D) (S : Finset ℕ) (d : Exponent D) : (originalSlice D p S x).coeff d = coeff D x ((p,d),S)

Definition 1.7 (coordinateSlice).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeRelativeShellDegreeBounds.coordinateSlice

Formalization. D5/S3/VertexAlgebra/Lattice/LatticeRelativeShellDegreeBounds.coordinateSlice (✓ std3).

Source. Repository-derived.

Commentary.

Apply the native NullFrame.coordinateEquiv to originalSlice. This is the actual polynomial substitution from the completed null-frame basis and its inverse, rather than a replacement coordinate energy.

Exact Lean telescope: def coordinateSlice {D : LatticeData} (F : NullFrame D) {t : ℕ} (B : Module.Basis (Fin t) ℂ F.K) (p : Charge D) (S : Finset ℕ) : State D →ₗ[ℂ] PolynomialCoordinates (NullFrame.Label t)

Theorem 1.8 (actualBasis_repr_eq_coordinateSlice).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeRelativeShellDegreeBounds.actualBasis_repr_eq_coordinateSlice

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

Source. Repository-derived.

Commentary.

Equality of two complex-linear coefficient maps is proved on the original tensorBasis. There each vector is an actual sector with polynomial coordinateEquiv(monomial d 1); native sector_coefficient computes actualBasis.repr, and originalSlice_tmul computes the extracted slice. Basis extensionality extends this equality to every tensor state.

Exact Lean telescope: theorem actualBasis_repr_eq_coordinateSlice {D : LatticeData} (F : NullFrame D) {t : ℕ} (B : Module.Basis (Fin t) ℂ F.K) (x : State D) (i : StateIndex D t) : (actualBasis F B).repr x i = (coordinateSlice F B i.1.1 i.2 x).coeff i.1.2

Theorem 1.9 (actualBasis_coefficient_shell_degree_bound).

Lean statement: D5/S3/VertexAlgebra/Lattice/LatticeRelativeShellDegreeBounds.actualBasis_coefficient_shell_degree_bound

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

Source. Repository-derived.

Commentary.

For each nonzero coefficient in the actual transported basis of an arbitrary state in the literal original relative shell, the charge is p, ghost site 3 is absent, the exact integer frequency-energy equation holds, and the original signed degree lies in the displayed cutoff interval. Shell membership, not any coordinate-energy or desired-bound premise, supplies the energy equation.

Exact Lean telescope: theorem actualBasis_coefficient_shell_degree_bound (D : LatticeData) (F : NullFrame D) {t : ℕ} (B : Module.Basis (Fin t) ℂ F.K) (H : Matrix (Fin D.rank) (Fin D.rank) ℂ) (hHG : H * LatticeSugawaraCurrents.gramComplex D = 1) (hGH : LatticeSugawaraCurrents.gramComplex D * H = 1) (p : Charge D) (x : State D) (hx : x ∈ relativeMassShell D H p) (i : StateIndex D t) (hi : (actualBasis F B).repr x i ≠ 0) : i.1.1 = p ∧ 3 ∉ i.2 ∧ (frameEnergy i.1.2 : ℤ) + relativeEnergy i.2 = 1 - chargeEnergy D p ∧ -(massShellCutoff D p : ℤ) ≤ degree i ∧ degree i ≤ (massShellCutoff D p : ℤ)

References