electron_structural_mass_forced
plain-language theorem explainer
The electron structural mass equals 2 to the power of negative 22 times phi to the 51, forced by the geometry of the 3-cube and the phi-ladder offsets. Researchers closing the lepton sector in Recognition Science cite this result to establish that the electron mass scale carries no free parameters. The proof unfolds the mass definition, substitutes the coherence exponent and rung equations, then reduces the phi powers via exponent addition after invoking phi nonzero.
Claim. The electron structural mass satisfies $m_ {struct} = 2^{-22} phi^{51}$, where the binary exponent -22 is twice the passive edge count of the 3-cube and the total exponent 51 is the sum of the coherence offset -5, the lepton R0 offset 62, and the rung adjustment 2-8.
background
In the T9 module the lepton sector constants are derived from cube geometry with D=3. The 3-cube supplies 12 edges; one active edge per tick leaves 11 passive field edges that fix the lepton binary exponent at -22. The phi-offset r0 equals 62 from four wallpaper tilings of 17 groups minus the octave adjustment from baseline rung r_e=2. The coherence exponent equals phi to the -5 by the upstream theorem E_coh_eq. These factors multiply the lepton yardstick to give the structural mass.
proof idea
The tactic proof unfolds electron_structural_mass and lepton_yardstick, rewrites via E_coh_eq, then applies simp with the sibling equations lepton_B_eq, lepton_R0_eq, electron_rung_eq and octave_period_eq. It obtains phi_ne_zero to license zpow_add, computes the integer difference 2-8=-6, and chains two zpow_add reductions to collapse the product of three phi powers into phi^51.
why it matters
This theorem supplies the closed form required by alphaG_pred_closed for the predicted alpha-G score and by structural_mass_bounds for the numerical interval (10856,10858). It realizes the T9 derivation chain that lepton constants are forced by D=3, passive edge count 11, wallpaper groups 17, and the eight-tick octave, removing free parameters from the electron mass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.