phi_ladder_stable
Every integer power of the golden ratio qualifies as a stable position under local J-cost minimization. Researchers deriving discrete spectra from self-similar recognition would cite this to confirm the phi-ladder supplies the quantized states. The term-mode proof splits the stability predicate via constructor and discharges the conjuncts with positivity of phi powers plus explicit ladder membership.
claimFor every integer $n$, the number $x = φ^n$ satisfies $x > 0$ and $x$ belongs to the $φ$-ladder, hence $x$ is stable (J-cost is locally minimized).
background
The φ-Emergence module derives the golden ratio from J-cost minimization on self-similar patterns. IsStablePosition(x) is the predicate $x > 0 ∧ x ∈ PhiLadder$, where the ladder is the discrete set of all integer powers of φ (the positive root of $r^2 = r + 1$). This rests on the upstream lemma phi_pow_pos, which states $φ^n > 0$ for any integer $n$ by zpow_pos applied to the positivity of φ.
proof idea
The term proof applies constructor to the conjunction inside IsStablePosition. The positivity conjunct is supplied directly by the lemma phi_pow_pos n. The ladder-membership conjunct is witnessed by the explicit pair ⟨n, rfl⟩ that exhibits the integer exponent.
why it matters in Recognition Science
The result fills the core claim that self-similar J-cost minimization forces discrete quantization at φ^n. It anchors the φ-Emergence section of the forcing chain and prepares composition with the Recognition Composition Law and the eight-tick octave. No downstream uses are recorded, leaving open its integration into mass formulas and the alpha band.
scope and limits
- Does not prove that the phi-ladder contains every stable position.
- Does not treat stability for non-self-similar or non-positive carriers.
- Does not evaluate the numerical J-cost at ladder points.
- Does not address perturbations or continuous deformations of the ladder.
formal statement (Lean)
202theorem phi_ladder_stable (n : ℤ) : IsStablePosition (φ^n) := by
proof body
Term-mode proof.
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. -/