Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Negative right-source compatibility propagation

Abstract

Negative right-source compatibility propagation

OriginalCompatible is the full three-supported coefficient law on the exact original source mu and actual correctedField. Its parameters gamma and delta are arbitrary integers; p,q,r and actual x are universally quantified. The left slice uses gamma+delta without parity reduction. In odd-odd sectors this sum is 2, whose conversion to lift 0 increases the physical mode by one; the carry is retained, not removed by an integer-binomial replacement.

The inverse/full-law bridge uses the Hahn tail of the actual original Y(a)b and independently certified physical locality. OriginalCompatible implies zero defect by finite inversion. Zero defect implies every signed compatibility coefficient by the supported recurrence. These are proof steps, not premises on the target module.

The source zero mode sends projectedGround(alpha,epsilon) to bilinear(unitCharge(i),alpha) times projectedGround(alpha,not epsilon). This formula includes the zero-charge coefficient and never divides by it. Therefore compatibility at both smaller projected signs suffices for the actual h0 correction.

Negative-current propagation consumes the unconditional native defect transport, kills its two smaller defects, and recovers the entire signed coefficient law. The original second source b and actual input x are unrestricted. The word theorem iterates actual source neutral modes with negative indices -(j.2+1).

The word theorem assumes the displayed exact full ground-pair compatibility for every pair of charges, both projected signs and every lift. That ground-pair base remains unproved here. Arbitrary-first transport and the complete Moonshine, VOA, CFT, anomaly, fusion, string and AdS/CFT programme remain open. These are repository-derived consequences of classical twisted-lattice calculus; no literature novelty or physical realization is claimed.

Theorem 1.1 (Full law implies zero defect).

Lean statement: D5/S3/VertexAlgebra/GroundRightCurrentTransport/Propagation.compatible_defect

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/GroundRightCurrentTransport/Propagation.compatible_defect (✓ std3). ∎

Source. Repository-derived.

Commentary.

The original full three-supported coefficient law implies vanishing of each native defect, by the source tail and finite inverse residue transform.

Theorem 1.2 (Zero defects recover the full law).

Lean statement: D5/S3/VertexAlgebra/GroundRightCurrentTransport/Propagation.defect_compatible

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/GroundRightCurrentTransport/Propagation.defect_compatible (✓ std3). ∎

Source. Repository-derived.

Commentary.

Vanishing of all signed native defects recovers every p,q,r coefficient, all three finite-support clauses and both ordered terms of the original law.

Theorem 1.3 (Scalar multiplication of the first source).

Lean statement: D5/S3/VertexAlgebra/GroundRightCurrentTransport/Propagation.compatible_smul_left

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/GroundRightCurrentTransport/Propagation.compatible_smul_left (✓ std3). ∎

Source. Repository-derived.

Commentary.

OriginalCompatible is preserved by every complex scalar in its first source, with its original supports transported by scalar multiplication.

Theorem 1.4 (Exact projected ground zero mode).

Lean statement: D5/S3/VertexAlgebra/GroundRightCurrentTransport/Propagation.ground_zero_mode

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/GroundRightCurrentTransport/Propagation.ground_zero_mode (✓ std3). ∎

Source. Repository-derived.

Commentary.

The original neutral zero mode multiplies by the bilinear charge coefficient and reverses the projected ground sign. Zero charge is included and the coefficient is never divided out.

Theorem 1.5 (Full negative-current compatibility step).

Lean statement: D5/S3/VertexAlgebra/GroundRightCurrentTransport/Propagation.projectedGround_negative_current_step

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/GroundRightCurrentTransport/Propagation.projectedGround_negative_current_step (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every positive natural m and current i, compatibility of the smaller original b at both projected signs and all lifts implies OriginalCompatible(projectedGround(alpha,epsilon),neutralMode(i,-m,b),gamma,delta), for arbitrary epsilon, gamma and delta.

Theorem 1.6 (Conditional full right-word propagation).

Lean statement: D5/S3/VertexAlgebra/GroundRightCurrentTransport/Propagation.projectedGround_right_word

Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/GroundRightCurrentTransport/Propagation.projectedGround_right_word (✓ std3). ∎

Source. Repository-derived.

Commentary.

Assuming only exact all-charge, both-sign ground-pair OriginalCompatible at every lift, the same full signed law holds with the second projected ground source replaced by any finite word of actual negative source currents.

References