topological_conservation_certificate
plain-language theorem explainer
Recognition Science derives conservation laws from topological linking in three dimensions rather than from continuous symmetries. A foundational physicist would cite the certificate to establish that electric charge, baryon number and lepton number are exactly conserved integers only when the spatial dimension is three, with a bijective correspondence to the cube axes. The proof is a term-mode conjunction that packages seven prior results on charge counts, bijections, trajectory invariance and the non-integrality of generic Noether charges.
Claim. When the dimension is three the number of independent topological charges is three and zero in every other dimension; this number equals the count of opposite face pairs; the set of Standard Model charges has three elements consisting of electric charge, baryon number and lepton number; the map sending each such charge to a coordinate axis is bijective; every topological charge is invariant along variational trajectories; and there exist Noether charges whose values are not integers.
background
TopologicalCharge is a structure assigning to each configuration an integer value that is preserved under variational successors, so quantization follows from the codomain being the integers. NoetherCharge assigns a real value preserved under the same successors. The module sets conservation laws as arising from linking numbers in D equals three, which cannot change under continuous deformation of the ledger.
proof idea
This is a one-line term-mode wrapper that applies the conjunction of three_charges_at_D3, no_charges_at_other_D, reflexivity on the face-pairs equality, sm_charge_count, charge_to_axis_bijective, the function invoking topological_charge_trajectory_conserved for each trajectory, and noether_not_necessarily_quantized.
why it matters
The declaration provides the F-012 certificate for topological conservation, collecting the main results of the module into a single statement. It supports the framework claim that conservation is topological and thus stronger than Noetherian, requiring only D equals three rather than a symmetry group. It builds on the dimension forcing chain by showing how D equals three yields exactly three charges corresponding to the Standard Model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.