theorem proved term proof

`phi_squared`

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

formal statement (Lean)

  36@[simp] theorem phi_squared : Constants.phi ^ 2 = Constants.phi + 1 := by

Term-mode proof.

  37  simp [phi_def, Real.goldenRatio_sq]
  38
  39/-- φ = 1 + 1/φ as an algebraic corollary. -/

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

imf_from_j_minimization in IndisputableMonolith.Astrophysics.ObservabilityLimits decl_use
information_balance_gives_phi in IndisputableMonolith.Astrophysics.ObservabilityLimits decl_use
phi_fixed_point' in IndisputableMonolith.PhiSupport decl_use
phi_squared in IndisputableMonolith.PhiSupport decl_use
phi_fixed_point in IndisputableMonolith.PhiSupport.Lemmas decl_use

Lean names referenced from this declaration's body.

Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
phi_squared in IndisputableMonolith.PhiSupport decl_use
phi_def in IndisputableMonolith.PhiSupport.Lemmas decl_use