electron_structural_mass_forced
plain-language theorem explainer
The theorem forces the electron structural mass to equal 2 to the power -22 times phi to the power 51. Workers deriving lepton masses on the Recognition Science phi-ladder cite this when closing the geometric mass formula for the first-generation lepton. The proof unfolds the structural-mass definition together with the yardstick, B, R0 and rung constants, then reduces the resulting phi exponents via addition and a single norm_num step.
Claim. The electron structural mass satisfies $m_ {struct} = 2^{-22} phi^{51}$.
background
In the T9 Electron Mass Definitions module the structural mass is introduced as the product of the lepton yardstick and phi raised to (rung minus the eight-tick octave period). For the electron the rung is fixed at 2, so the exponent simplifies to -6 once the yardstick is expanded. The yardstick itself is built from the coherence energy E_coh, the lepton B factor and the R0 length scale, each of which carries explicit powers of phi. The only non-trivial lemma required is phi_ne_zero, which guarantees that the base is nonzero so that the exponent-addition rule zpow_add₀ applies without side conditions.
proof idea
The tactic proof first unfolds electron_structural_mass, lepton_yardstick, E_coh, lepton_B, lepton_R0 and electron_rung. It obtains phi_ne_zero, then proves two auxiliary equalities that combine the exponents -5 + 62 and 57 - 6. A norm_num step records that 2 - 8 equals -6. The final simp and rw steps reassociate the product and substitute the combined exponent 51.
why it matters
This closed form is invoked directly by alphaG_pred_closed to obtain the predicted fine-structure constant and by structural_mass_bounds to produce the numerical interval (10856, 10858). It therefore supplies the concrete mass value required by the Recognition Science mass formula (yardstick times phi to the power rung-8) at the electron rung. The result sits inside the T9 block that separates definitions from necessity theorems and thereby prevents import cycles while feeding the downstream alpha-G scorecard.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.