Actual balanced three-field transport
Abstract
Actual balanced three-field transport
Theorem 1.1 (Balanced transport with the original witnesses).
Lean statement: D5/S3/VertexAlgebra/Sectors/LatticeSectorThreeFieldBalancedTransport.actual_three_field_balanced_transport
Proof. Machine-checked in Lean as D5/S3/VertexAlgebra/Sectors/LatticeSectorThreeFieldBalancedTransport.actual_three_field_balanced_transport (✓ std3). ∎
Source. Repository-derived.
Commentary.
For arbitrary lattice data, charges and oscillator descendants, k is chosen before δ,w. The actual raw-inner supplier is obtained once. The original a,P, canonical truncations, all six signed product laws, and the old cleared, polynomial-action and finite raw-inner reconstruction facts are carried unchanged. The new actual balanced channel under the literal substituted clearing equals signedExtend of the same generally infinite P at the lawful native [s+x,x,z] substitution. The coupled second Jacobi term vanishes using original u/t locality and u-on-w truncation. Original v/t locality and v-on-w truncation give the lower second-coordinate support needed for the signed collision theorem. Independently, canonical truncation of u on v gives a uniform lower s bound and canonical truncation of t on w gives a uniform lower z bound, both uniform in x; no uniform x bound is asserted. All signed targets, zero series, repeated charges, rank zero and indefinite data remain in scope. There is no finite-P, domain, positivity, energy or charge restriction. Only these two charts share witnesses by construction. No raw balanced inverse, unrestricted raw substitution, five-tree common P, pentagon, coherence, analytic convergence or physical realization is claimed. Suppliers retain their original attributions and normalization.