theorem proved term proof

`phi_eq_goldenRatio`

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

formal statement (Lean)

  55theorem phi_eq_goldenRatio : Constants.phi = goldenRatio := by

Term-mode proof.

  56  simp only [Constants.phi, goldenRatio]
  57
  58/-- Coherence energy E_coh = φ^(-5) in eV -/

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

imf_from_j_minimization in IndisputableMonolith.Astrophysics.ObservabilityLimits decl_use
phi51_gt in IndisputableMonolith.Masses.ElectroweakMasses decl_use
phi51_lt in IndisputableMonolith.Masses.ElectroweakMasses decl_use
phi_eq_goldenRatio in IndisputableMonolith.Masses.ElectroweakMasses decl_use
sin2_theta_positive in IndisputableMonolith.Masses.ElectroweakMasses decl_use
phi11_gt in IndisputableMonolith.Masses.Verification decl_use
phi11_lt in IndisputableMonolith.Masses.Verification decl_use
phi17_gt in IndisputableMonolith.Masses.Verification decl_use
phi17_lt in IndisputableMonolith.Masses.Verification decl_use
phi43_gt in IndisputableMonolith.Masses.Verification decl_use
phi43_lt in IndisputableMonolith.Masses.Verification decl_use
phi59_gt in IndisputableMonolith.Masses.Verification decl_use
phi59_lt in IndisputableMonolith.Masses.Verification decl_use
phi70_gt in IndisputableMonolith.Masses.Verification decl_use
phi70_lt in IndisputableMonolith.Masses.Verification decl_use
phi76_gt in IndisputableMonolith.Masses.Verification decl_use
phi76_lt in IndisputableMonolith.Masses.Verification decl_use
phi_eq_goldenRatio in IndisputableMonolith.Masses.Verification decl_use
top_quark_pred_order in IndisputableMonolith.Masses.Verification decl_use

Lean names referenced from this declaration's body.

Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
phi_eq_goldenRatio in IndisputableMonolith.Masses.ElectroweakMasses decl_use
phi_eq_goldenRatio in IndisputableMonolith.Masses.Verification decl_use