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)
57theorem phi_ladder_ne_one {n : ℤ} (hn : n ≠ 0) : phi_ladder n ≠ 1 :=
proof body
Term-mode proof.
58 phi_zpow_ne_one hn
59
60/-! ## Part II: Positive Cost on the φ-Ladder -/
61
used by (1)
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.
-
phi_ladder
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
phi_ladder
in IndisputableMonolith.Foundation.OntologyPredicates
decl_use
-
phi_ladder
in IndisputableMonolith.Foundation.StillnessGenerative
decl_use
-
phi_zpow_ne_one
in IndisputableMonolith.Foundation.StillnessGenerative
decl_use
-
Cost
in IndisputableMonolith.Measurement.RSNative.Core
decl_use