Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Original Corrected Source with Two Twisted Inputs

Abstract

Original Corrected Source with Two Twisted Inputs

The original Carrier remains the source. For two actual twisted tensor inputs x,y, define K_L(e)(x,y)(a)=B((correctedField D hu a).coeff e x,y). This is a full algebraic dual coefficient, with the operator acting on the first input; no ground symmetry is used to identify it with a right orientation.

The existing corrected singleton coefficient proof in ChargedResidue.LatticeHalfFockChargedResidue and its addition and scalar laws are reused through their canonical public names in the original owner. Only their visibility changes; their statements and proof bodies are unchanged.

For every charge and each nonzero ground u, the charged adjoint consumer supplies an x with nonzero K_L(-N)(x,1 tensor u) on the original generator single a 1. The charged_ground_leading is an existing theorem, not a premise supplied by this module. This does not prove a full corrected-source adjoint, restricted-dual state, intertwining field, mixed Jacobi, fusion rule, Monster realization or complete string/AdS construction.

Information-escape registration remains unfinished: the faithful compiled Reg mirrors currently report declared_unresolved. The source-reconstruction diagnostics and missing binding certificates are recorded at https://github.com/the-omega-institute/trureturing/issues/21134 under the repository linked-issue exception. Compilation does not assert a validated registration.

Definition 1.1 (correctedDualCoefficient).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/CorrectedDualCoefficient.correctedDualCoefficient

Formalization. D5/S3/VertexAlgebra/TwistedGround/CorrectedDualCoefficient.correctedDualCoefficient (✓ std3).

Source. Repository-derived.

Commentary.

The left-oriented full algebraic dual on the original Carrier, bilinear in two actual twisted inputs.

Theorem 1.2 (correctedDualCoefficient nonzero second ground).

Lean statement: D5/S3/VertexAlgebra/TwistedGround/CorrectedDualCoefficient.correctedDualCoefficient_nonzero_second_ground

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/TwistedGround/CorrectedDualCoefficient.correctedDualCoefficient_nonzero_second_ground (✓ std3). ∎

Source. Repository-derived.

Commentary.

A nonzero original-source generator coordinate exists at exponent -bilinear D a a for every charge and every nonzero actual ground second input. The proof consumes the native tensor adjoint chain and reuses the original singleton identification.

References