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)
114theorem J_at_phi : (φ + 1/φ) / 2 - 1 = (Real.sqrt 5 - 2) / 2 :=
proof body
Term-mode proof.
115 Inequalities.J_cost_phi
116
117/-- J-cost at φ^n (for n ≥ 1) -/
used by (4)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (5)
Lean names referenced from this declaration's body.
-
J_at_phi
in IndisputableMonolith.Algebra.PhiRing
decl_use
-
J_cost_phi
in IndisputableMonolith.Foundation.Inequalities
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use