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

planck_mass_eq

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)

 233theorem planck_mass_eq : planck_mass_rs = φ_val^(-5 : ℤ) := by

proof body

Tactic-mode proof.

 234  -- planck_mass_rs = √(ℏ_rs * c_rs / G_rs)
 235  -- = √(φ^(-5) * 1 / φ^5) = √(φ^(-10)) = φ^(-5)
 236  have h_ℏ : ℏ_rs = φ_val^(-5 : ℤ) := ℏ_rs_eq
 237  have h_c : c_rs = 1 := c_rs_eq_one
 238  have h_G : G_rs = φ_val^(5 : ℕ) := rfl
 239  simp only [planck_mass_rs, h_ℏ, h_c, h_G, mul_one]
 240  -- Now: √(φ^(-5) / φ^5) = √(φ^(-10)) = φ^(-5)
 241  -- φ^(-5) / φ^5 = φ^(-5) * φ^(-5) = φ^(-10)
 242  have h1 : φ_val ^ (-5 : ℤ) / φ_val ^ (5 : ℕ) = φ_val ^ (-10 : ℤ) := by
 243    have hphi5_pos : 0 < φ_val ^ (5 : ℕ) := pow_pos phi_pos 5
 244    have hphi5_ne : φ_val ^ (5 : ℕ) ≠ 0 := hphi5_pos.ne'
 245    have hphi10_pos : 0 < φ_val ^ (10 : ℕ) := pow_pos phi_pos 10
 246    have hphi10_ne : φ_val ^ (10 : ℕ) ≠ 0 := hphi10_pos.ne'
 247    field_simp [hphi5_ne, hphi10_ne]
 248  rw [h1]
 249  -- √(φ^(-10)) = φ^(-5) because φ^(-10) = (φ^(-5))^2
 250  have h2 : φ_val ^ (-10 : ℤ) = (φ_val ^ (-5 : ℤ))^2 := by
 251    rw [← zpow_ofNat, ← zpow_mul]
 252    norm_num
 253  rw [h2]
 254  -- √(x²) = x for x ≥ 0
 255  exact sqrt_sq (le_of_lt (zpow_pos phi_pos (-5)))
 256
 257/-! ## Summary: All Constants from φ -/
 258
 259/-- **ALL CONSTANTS FROM φ**
 260
 261    In RS-native units:
 262    - c = 1 (definition of causal coherence)
 263    - ℏ = φ^(-5) (IR gate scale)
 264    - G = φ^5 (curvature extremum)
 265    - α ≈ 1/137 × correction (geometric seed)
 266
 267    These are not free parameters. They are algebraic in φ,
 268    and φ is forced by the self-similarity equation from the
 269    unique cost J. -/

depends on (29)

Lean names referenced from this declaration's body.