phi_ladder_stable
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.