def
definition
IsStablePosition
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.PhiEmergence on GitHub at line 198.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
195/-- A position x > 0 is stable if J-cost is locally minimized there.
196
197 For self-similar patterns, stability requires the ratio to satisfy r² = r + 1. -/
198def IsStablePosition (x : ℝ) : Prop :=
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