cross_sector_shift_eq
plain-language theorem explainer
The equality fixes the down-quark cross-sector shift at twelve in the Recognition Science mass ladder. Modelers of sector-dependent fermion masses cite it to anchor the rung correction that appears in the phi-ladder formula for down-type quarks. The proof is a direct computational check that evaluates the shift definition, which reduces to the three-dimensional cube edge count, and obtains twelve.
Claim. Let $s$ denote the down-quark cross-sector shift, defined as the cube edge count evaluated at spatial dimension three. Then $s=12$.
background
The Sector-Dependent Generation Torsion module establishes algebraic properties of the cell counts {13,11,6,8} that partition the cube structure at D=3. The cross-sector shift for down quarks is introduced as an additional +E rung correction in the mass exponent; its definition is the cube edge count at dimension three. Upstream, W is the total cube edge count (equal to 12) and the Lepton inductive type enumerates the six lepton species whose generation structure supplies the reference ladder. The module document states that the +12 shift itself remains a data-motivated hypothesis rather than a first-principles derivation.
proof idea
The proof is a one-line wrapper that applies native_decide to the definition of the shift. Native_decide reduces the expression cube_edges' 3 by direct evaluation and confirms the integer value twelve.
why it matters
The result supplies the concrete numerical anchor for the hypothesized down-quark rung correction inside the mass topology. It closes the algebraic constraint that links the cross-sector shift to the D=3 coincidence W=12, thereby supporting the phi-ladder mass formula and the eight-tick octave structure. No downstream theorems yet invoke the equality, leaving its use in explicit mass calculations as an open integration point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.