`phi_ladder_stable`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.PhiEmergence
domain: Foundation
line: 202 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.PhiEmergence on GitHub at line 202.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 199  x > 0 ∧ x ∈ PhiLadder
 200
 201/-- All φ-ladder positions are stable -/
 202theorem phi_ladder_stable (n : ℤ) : IsStablePosition (φ^n) := by
 203  constructor
 204  · exact phi_pow_pos n
 205  · exact ⟨n, rfl⟩
 206
 207/-- HYPOTHESIS: Stable positions are exactly the φ-ladder.
 208
 209    This is the core claim that self-similar J-cost minimization
 210    forces discrete quantization at φ^n. -/
 211def H_StableIffPhiLadder : Prop :=
 212  ∀ x : ℝ, x > 0 → (IsStablePosition x ↔ x ∈ PhiLadder)
 213
 214/-! ## Summary -/
 215
 216#check IsSelfSimilar
 217#check phi_is_self_similar
 218#check phi_unique_positive
 219#check PhiLadder
 220#check phi_ladder_ratio
 221#check J_at_phi
 222#check H_ThresholdFromPhi
 223#check H_StableIffPhiLadder
 224
 225end PhiEmergence
 226end Foundation
 227end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.