standardModelConservation
plain-language theorem explainer
This definition enumerates the eight conserved quantities of the Standard Model together with the continuous symmetries that generate them. A physicist deriving Noether charges from Recognition Science cost stationarity would reference the list to match ledger invariance to observed conservation. The body is a direct list literal with no computation or lemma applications.
Claim. The Standard Model conservation laws are the list of pairs (Energy, time translation), (Momentum, space translation), (Angular momentum, rotation), (Electric charge, $U(1)_{em}$), (Color charge, $SU(3)_c$), (Weak isospin, $SU(2)_L$ broken), (Baryon number, approximate $U(1)_B$), (Lepton number, approximate $U(1)_L$).
background
The module derives Noether's theorem from Recognition Science cost stationarity: a symmetry is any transformation that leaves the J-cost unchanged, while conservation means the associated charge remains constant along solutions because of ledger balance. The upstream Physical structure supplies the minimal assumptions of positive c, ħ, and G on bridge anchors. RS-native units fix c = 1 with Energy, Momentum, and Time as real numbers, and the Lepton inductive type classifies the six lepton species.
proof idea
The definition is a direct list literal containing the eight symmetry-conservation pairs. No lemmas or tactics are invoked; the construction simply enumerates the pairs that the module doc presents as key examples.
why it matters
The definition supplies the concrete mapping required by the module's core insight that Noether charges arise from J-cost invariance under continuous symmetries. It populates the key-examples table in the module documentation and thereby supports the paper proposition on ledger-derived conservation. The listed entries instantiate the framework landmarks of time-translation symmetry yielding energy and gauge symmetries yielding charges, while the falsification criteria in the same file record the physical limits of the mapping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.