Pith. sign in
module module high

IndisputableMonolith.Foundation.MassWeakBases

show as:
view Lean formalization →

Assigns each fermion generation a mass-basis axis on the 3-cube from CW excitation order and torsion. Gen 1 is the ground state (isotropic), gen 2 (edge-dressed, torsion 11) locks to axis 0 (four flips, minimal J-cost), and gen 3 takes the residual axes {1,2}. Also defines the complementary weak basis and mixing-angle data. Cited by the CKM-from-cube derivation; the argument is structural assignment plus involution lemmas, not a deep calculation.

claimOn $Q_3$, the mass-basis assignment maps generation $1$ to the ground (isotropic) coupling, generation $2$ (edge-dressed, torsion $11$) to axis $0$ (the unique axis with four flips per cycle), and generation $3$ (face+edge) to the residual axes $\{1,2\}$. A complementary weak-basis axis map and mixing-angle data are defined so that mass and weak bases label cube axes consistently.

background

Recognition Science places fermion generations on the 8-tick Gray-code cycle of the 3-cube $Q_3$. Upstream, ParticleGenerations fixes three generations; TorsionForcing uniquely selects the torsion triple ${0,11,17}$ compatible with the cycle, the Recognition Composition Law, and the $\phi$-ladder. CycleOperator supplies the unitary $\hat R$ on $\mathbb{C}^8$ induced by that directed walk; GrayCodeChirality records that the walk is chiral (the geometric seed of CP violation); GaugeFromCube extracts $SU(3)\times SU(2)\times U(1)$ from $\mathrm{Aut}(Q_3)$.

This module sits between those structural facts and CKM phenomenology. It introduces mass-basis and weak-basis axis assignments: which cube axes each generation couples to when masses are diagonal versus when the weak interaction is diagonal. The guiding cost is the $J$-functional $J(x)=(x+x^{-1})/2-1$; edge-dressed states prefer the axis flipped most often because that choice minimizes passive-edge $J$-cost per cycle.

proof idea

Definition-heavy module with short supporting lemmas. Mass and weak basis assignments are recorded as structured data (generation $\mapsto$ axis labels). The key preference fact is that the edge-dressed generation (torsion 11 equals passive field edges) selects axis 0, the unique axis with four flips in the Gray cycle. An even-flip generator on vertices is shown to be an involution, and the weak-complement axis map is shown to act as the identity on the residual labeling. A joint lemma checks that both bases label axes coherently; MixingAngleData packages the geometric input needed downstream for Cabibbo-type angles. No long tactic scripts: assignments plus involution/identity checks.

why it matters in Recognition Science

CKMFromCube imports this module to turn cube geometry, torsion ${0,11,17}$, and Gray chirality $[4,2,2]$ into the quark mixing matrix. Without a fixed mass-versus-weak axis dictionary, generation-dependent mixing angles have no geometric source. The assignment gen1$\leftrightarrow$ground, gen2$\leftrightarrow$axis 0, gen3$\leftrightarrow{1,2}$ is the bridge from P-001 (three generations) and torsion forcing to the CKM derivation. It also aligns with the eight-tick octave (T7) and $D=3$ (T8): axes are the three spatial directions of $Q_3$, and the cycle length fixes which axis is "most flipped." Downstream work can treat mixing angles as derived labels rather than free parameters.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (17)