Foundation Winding Charges

Winding charges as conserved quantities

Foundation winding charges are the topological mechanism behind conservation in Recognition Science. A world-line in the ledger is a sequence of positions on the integer lattice ℤ^D, changing by one step along a single axis each tick, or staying put. For each axis, the winding number of a path is the net signed displacement along that axis: the count of steps in the plus direction minus the count of steps in the minus direction. Because the dynamics updates one tick at a time, it acts only by local deformations, and local deformations preserve every winding number. Winding numbers are therefore exactly conserved, not approximately.

The module proves the core facts about these charges. Winding numbers are integers by construction, they add under path concatenation, and they are invariant under inserting or removing a cancelling pair, a plus step followed by a minus step on the same axis. Different axes give independent charges: a path can change its winding number along one axis without affecting any other. Consequently there are exactly D independent winding charges in D dimensions. The theorem D_independent_charges states that for any positive D, there are D winding charges, they are pairwise distinguishable, and each can take any integer value independently of the others.

For D = 3, the three winding numbers correspond to electric charge, baryon number, and lepton number. The identification of which axis maps to which charge is a definitional choice, but the count of three independent charges is forced by the combinatorics. The theorem winding_gives_three_charges proves that the number of axes in three dimensions equals the independent charge count. A separate theorem, all_threes_unified, shows that the number of winding charges, face-pairs, colors, Standard Model charges, and the topological charge count all equal 3. This module fills a gap left by TopologicalConservation.lean, which defined the charge count as a conditional rather than deriving it.

The winding numbers are integer-valued and exactly conserved, which makes them topological charges in the ledger. The module constructs a winding_label_is_topological definition that packages a winding number together with a proof of its conservation as a topological charge. The result is a concrete, combinatorial account of why conservation laws hold: they are not imposed, they are forced by the structure of paths on a lattice.

THEOREM winding_number · winding_additive · insert_cancelling_preserves_winding · IndisputableMonolith/Foundation/WindingCharges.lean

THEOREM winding_numbers_independent · IndisputableMonolith/Foundation/WindingCharges.lean

THEOREM D_independent_charges · IndisputableMonolith/Foundation/WindingCharges.lean

MODEL winding_gives_three_charges · IndisputableMonolith/Foundation/WindingCharges.lean

THEOREM all_threes_unified · IndisputableMonolith/Foundation/WindingCharges.lean

What this page does not claim

This answer does not claim that the mapping of winding numbers to electric charge, baryon number, and lepton number is derived rather than a definitional choice. This answer does not claim that the physical recognition-to-linking bridge connecting these lattice paths to three dimensions is established. This answer does not claim that the winding number construction is the only possible topological mechanism for conservation.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/WindingCharges.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: