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)
47theorem phi_interval_contains :
48 phiInterval.contains ((1 + Real.sqrt 5) / 2) := phi_in_phiInterval
proof body
Term-mode proof.
49
50/-- Prove that log(φ) is in its interval -/
depends on (10)
Lean names referenced from this declaration's body.
-
contains
in IndisputableMonolith.Ethics.StakeGraph
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
that
in IndisputableMonolith.NumberTheory.PhiLadderLattice
decl_use
-
contains
in IndisputableMonolith.Numerics.Interval.Basic
decl_use
-
phi_in_phiInterval
in IndisputableMonolith.Numerics.Interval.Pow
decl_use
-
phiInterval
in IndisputableMonolith.Numerics.Interval.Pow
decl_use
-
interval
in IndisputableMonolith.Unification.SpacetimeEmergence
decl_use