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)
106theorem phi_gt_onePointSix : φ > (1.6 : ℝ) :=
proof body
Term-mode proof.
107 lt_trans (by norm_num) phi_gt_onePointSixOneEight
108
109/-- φ⁻¹ = φ - 1 (a key identity). -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
phi_cost_pos
in IndisputableMonolith.Foundation.StillnessGenerative
decl_use
depends on (4)
Lean names referenced from this declaration's body.
-
lt_trans
in IndisputableMonolith.Foundation.ArithmeticFromLogic
decl_use
-
identity
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
phi_gt_onePointSixOneEight
in IndisputableMonolith.Foundation.PhiForcing
decl_use
-
identity
in IndisputableMonolith.RRF.Foundation.VantageCategory
decl_use