electron_structural_mass_forced
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not assign the electron rung; that is supplied by electron_rung.
- Does not convert the dimensionless ratio into MeV; that step occurs in mass_ref_MeV.
- Does not prove that the rung assignment is unique across generations.
- Does not invoke the Recognition Composition Law or the J-cost function.
Lean usage
have hme : electron_structural_mass = (2 : ℝ) ^ (-(22 : ℤ)) * phi ^ (51 : ℤ) := electron_structural_mass_forcedformal statement (Lean)
78theorem electron_structural_mass_forced :
79 electron_structural_mass = (2 : ℝ) ^ (-22 : ℤ) * phi ^ (51 : ℤ) := by
proof body
Tactic-mode proof.
80 unfold electron_structural_mass lepton_yardstick E_coh lepton_B lepton_R0 electron_rung
81 have hne : (phi : ℝ) ≠ 0 := phi_ne_zero
82 have h1 : phi ^ (-5 : ℤ) * phi ^ (62 : ℤ) = phi ^ (57 : ℤ) := by
83 rw [← zpow_add₀ hne]; norm_num
84 have h2 : phi ^ (57 : ℤ) * phi ^ (-6 : ℤ) = phi ^ (51 : ℤ) := by
85 rw [← zpow_add₀ hne]; norm_num
86 have hsub : ((2 : ℤ) - 8 : ℤ) = (-6 : ℤ) := by norm_num
87 simp only [hsub, h1, mul_assoc]
88 rw [h2]
89
90end ElectronMass
91end Physics
92end IndisputableMonolith