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

planck_gate_identity

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)

 251theorem planck_gate_identity :
 252    Real.pi * hbar * G = c^3 * lambda_rec^2 := by

proof body

Term-mode proof.

 253  unfold G lambda_rec hbar c ell0 cLagLock tau0 tick
 254  simp only [one_pow, mul_one]
 255  have hpi : Real.pi ≠ 0 := Real.pi_pos.ne'
 256  have hphi5 : phi ^ (-(5 : ℝ)) ≠ 0 := (Real.rpow_pos_of_pos phi_pos _).ne'
 257  field_simp [hpi, hphi5]
 258
 259/-- Equivalent form: c³λ²/(πℏG) = 1. -/

used by (1)

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.