base_shift_bounds
plain-language theorem explainer
The base shift, defined as twice the wallpaper group count plus the exact ledger fraction, satisfies the numerical bound 34.6590 < base_shift < 34.6592. Researchers deriving forced lepton masses on the phi-ladder cite this to fix the zero rung under T8 ledger quantization. The proof is a direct term reduction that substitutes the rational ledger fraction and evaluates the resulting arithmetic.
Claim. $34.6590 < 2W + f < 34.6592$ where $W = 17$ is the number of wallpaper groups and $f = 29/44$ is the exact ledger fraction from cube-edge counting.
background
In Recognition Science the base shift anchors the electron mass on the phi-ladder via the formula yardstick * phi^(rung - 8 + gap(Z)). It is introduced in MassTopology as the noncomputable definition base_shift := 2 * W + ledger_fraction, with W the constant 17 (Fedorov 1891) and ledger_fraction the rational supplied by the sibling lemma ledger_fraction_exact. The ElectronMass.Necessity module proves the electron mass is forced from T8 ledger quantization together with the geometric constants already derived in AlphaDerivation and MassTopology. Upstream results include the wallpaper_groups definition (17) and the exact equality ledger_fraction = 29/44 obtained by norm_num on the edge counts (12 cube edges, passive and active field edges per tick).
proof idea
Term-mode proof that first simplifies base_shift, W and wallpaper_groups, then rewrites via the ledger_fraction_exact lemma to replace the fraction by 29/44, and finally applies norm_num to discharge the two-sided numerical inequality on the resulting rational.
why it matters
The lemma supplies the tight numerical anchor used by the downstream refined_shift_bounds result, which adds the radiative correction while keeping the interval. It completes one concrete step in the T9 necessity argument that the electron mass formula is forced from T8 and the eight-tick octave (T7) together with D = 3. The bound therefore sits inside the chain that runs from J-uniqueness (T5) through the Recognition Composition Law to the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.