permits
plain-language theorem explainer
Definitional packaging, in the Sakharov-from-ledger cosmology module, of the claim that the Z³ double-entry ledger allows balanced multi-axis rotations. Those collective rotations are the ledger stand-in for sphaleron-like processes that change baryon winding. Cosmology and baryogenesis staging cite it when assembling ΔB bookkeeping. There is no proof body: it is a structure/abbrev with zero tactics.
Claim. On the three-dimensional ledger ($D=3$), the double-entry structure admits balanced simultaneous rotations of all spatial axes. Such multi-axis rotations are the processes under which the baryon winding charge need not stay fixed, while remaining compatible with local conservation under ordinary deformations.
background
The ambient module reconstructs Sakharov's three conditions for baryogenesis from Recognition Science ledger structure, with an explicit honesty correction: only B-violation bookkeeping and CP violation are treated as structural; departure from equilibrium is an underived hypothesis parameter (electroweak first-order vs crossover is open, and is a crossover in the minimal SM at $m_H\approx 125,\mathrm{GeV}$).
Condition 1 is framed topologically. Spatial dimension is the forced $D=3$ from the forcing chain. Baryon number is read as one of three independent winding charges on $\mathbb{Z}^3$: conserved under local deformations, but able to jump under global processes that rotate all three axes at once. The module text identifies those processes with collective eight-tick phase rotations and notes that the double-entry ledger is what makes balanced multi-axis rotations admissible.
Upstream constants and ledger geometry in play include the RS-native charge type, polarized birth interface counts, and recognition-equilibrium packages (sigma conservation and variance descent). CP enters later via the chiral Gray-code Berry phase and $J_{\mathrm{CP}}\neq 0$; it is not part of this definition.
proof idea
No proof. Claim status is definitional (def_or_abbrev): a structure (or structure-level packaging) with an empty proof body. It records the ledger permission for balanced multi-axis rotations as a named interface used by later ΔB identities (deltaB_per_sphaleron, sphaleron_changes_B_by_3, $B-L$ preservation) and by the conditional Sakharov bundle SakharovConditions / sakharov_from_RS. Nothing is discharged by tactics or by appeal to a uniqueness lemma here.
why it matters
This declaration sits at the interpretive front of Condition 1 in the Sakharov chain: without a named license for multi-axis ledger rotations, the sphaleron-like ΔB bookkeeping has no structural hook. Downstream, the module assembles SakharovConditions EWFirstOrder with fields b_violation ($\Delta B$ per sphaleron $=3$), cp_violation (CP asymmetry parameter $\neq 0$), and out_of_eq (the named hypothesis). Related siblings include cp_source_positive, sphaleron_preserves_b_minus_l, and the conditional theorem sakharov_from_RS.
Framework landmarks: $D=3$ (forcing T8/T9), the eight-tick octave as the collective rotation clock, and CP from Gray-code chirality / Jarlskog $J_{\mathrm{CP}}>0$. The module doc is explicit that baryon-as-winding is an interpretation, not a derived anomaly (audit FQ4), and that $\Gamma_{\mathrm{sph}}\propto\alpha_W^5 T^4$ is imported SM scaling with $\alpha_W$ not derived. Open question carried forward: the out-of-equilibrium / first-order electroweak hypothesis on every downstream baryogenesis statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.