winding_charges_certificate
plain-language theorem explainer
Winding numbers on lattice paths in dimension D are additive under concatenation and invariant under insertion of cancelling step pairs. For D=3 this produces exactly three independent topological charges that match the count of face pairs and SM charges. Researchers deriving conservation laws from topology rather than Noether symmetry in Recognition Science cite the certificate to ground charge quantization. The proof is a term-mode five-tuple that directly assembles five lemmas on additivity, invariance, and dimension counting.
Claim. Let $w_k$ map a lattice path in dimension $D$ to its net signed displacement along axis $k$. Then $w_k(p_1 ++ p_2) = w_k(p_1) + w_k(p_2)$ for any paths $p_1, p_2$, and if $s_1, s_2$ form a cancelling pair then $w_k(p_1 ++ [s_1, s_2] ++ p_2) = w_k(p_1 ++ p_2)$. When $D=3$ the number of independent charges equals 3, which equals the number of face pairs and the cardinality of SMCharge.
background
A LatticePath in dimension D is a finite list of LatticeSteps; each step is a plus or minus move along one axis or a stay. The winding number along axis k is the net count of +k steps minus -k steps. The module shows that local deformations of paths, realized by inserting cancelling pairs, leave every winding number unchanged, so the numbers are conserved under the variational dynamics that updates one tick at a time.
proof idea
The proof is a term-mode tuple. It applies winding_additive to obtain additivity, insert_cancelling_preserves_winding to obtain invariance under cancelling pairs, Fintype.card_fin 3 for the cardinality identity, loops_eq_face_pairs_D3 to equate the loop count with face pairs at D=3, and sm_charges_match_D3 to match SMCharge cardinality with independent_charge_count 3.
why it matters
The certificate supplies the combinatorial derivation that TopologicalConservation left as a definition, showing that exactly three independent charges arise when D=3. It unifies the count with face pairs, colors, and generations, confirming that conservation follows from lattice topology rather than continuous symmetry. In the Recognition Science chain this step closes the gap between the D=3 forcing and the independent_charge_count used for particle spectra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.