pith. machine review for the scientific record. sign in
theorem proved tactic proof

electron_structural_mass_forced

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 197theorem electron_structural_mass_forced :
 198    electron_structural_mass = (2 : ℝ) ^ (-22 : ℤ) * phi ^ (51 : ℤ) := by

proof body

Tactic-mode proof.

 199  unfold electron_structural_mass lepton_yardstick
 200  rw [E_coh_eq]
 201  simp only [lepton_B_eq, lepton_R0_eq, electron_rung_eq, octave_period_eq]
 202  have hne : (phi : ℝ) ≠ 0 := phi_ne_zero
 203  -- Simplify 2 - 8 to -6
 204  have hsub : (2 : ℤ) - (8 : ℕ) = (-6 : ℤ) := by norm_num
 205  simp only [hsub]
 206  -- Now combine the phi powers
 207  have h1 : phi ^ (-5 : ℤ) * phi ^ (62 : ℤ) = phi ^ (57 : ℤ) := by
 208    rw [← zpow_add₀ hne]; norm_num
 209  have h2 : phi ^ (57 : ℤ) * phi ^ (-6 : ℤ) = phi ^ (51 : ℤ) := by
 210    rw [← zpow_add₀ hne]; norm_num
 211  simp only [h1, mul_assoc]
 212  rw [h2]
 213
 214/-- Theorem: All lepton sector constants are derived from cube geometry.
 215    This proves the sector is parameter-free.
 216
 217    Note: MassTopology uses literal 3 while AlphaDerivation uses D = 3.
 218    They are definitionally equal. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (19)

Lean names referenced from this declaration's body.