three_conservation_laws
plain-language theorem explainer
In three spatial dimensions the cube has exactly three pairs of opposite faces, so there are three independent face-pair conservation channels. Cosmology and baryogenesis arguments that identify Sakharov B/L bookkeeping with cube face structure cite this identity. The proof is pure definitional reduction: face-pair count is the identity map on dimension.
Claim. The number of opposite-face pairs on a $D$-cube equals $D$. Specializing to the forced spatial dimension $D = 3$ yields exactly three independent face-pair channels: $\mathrm{face\_pairs}(3) = 3$.
background
The module derives Sakharov conditions for baryogenesis from the RS ledger. Condition 1 (baryon-number violation) is tied to winding charges and multi-axis 8-tick rotations on the $Z^3$ ledger; condition 2 (CP violation) is imported from the chiral Gray-code Berry phase and Jarlskog invariant; condition 3 (departure from equilibrium) remains an explicit underived hypothesis.
Upstream, spatial dimension is forced to $D = 3$ (T8/T9 landmarks: linking and recognition geometry). On a $D$-cube, opposite faces come in pairs, and the count of those pairs is defined to be exactly $D$. That count is the combinatorial stand-in, in this module, for three independent conservation channels aligned with the three spatial axes.
Particle-generation structure elsewhere in the foundation also uses $D = 3$ to force three generations; the same numerical identity appears here as the face-pair count.
proof idea
One-line term proof by rfl. By definition the opposite-face-pair count on a $D$-cube is the identity function on $D$, so evaluating at $D = 3$ is definitionally equal to $3$. No lemmas are unfolded beyond that definitional equality.
why it matters
Gives the combinatorial backbone for reading three independent conservation laws off the $D = 3$ cube in the Sakharov-from-ledger story. Sibling results (deltaB_per_sphaleron, sphaleron_changes_B_by_3, sphaleron_preserves_b_minus_l, and the packaged SakharovConditions / sakharov_from_RS statements) treat the three-generation / three-channel count as the reason a sphaleron-like multi-axis rotation shifts baryon number by $N_{\mathrm{gen}} = 3$ while preserving $B - L$.
Framework landmarks in play: T8 forcing $D = 3$, the eight-tick octave underlying collective phase rotations, and the three-generation structure from the cube. The module doc is explicit that baryon number as ledger winding is an interpretation (audit FQ4) and that out-of-equilibrium physics is not derived; this lemma only locks the $3 = 3$ face-pair identity those later bookkeeping claims rest on. Currently unused by downstream edges, but it is the named numerical hinge for the conservation-law narrative in the file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.