H_StableIffPhiLadder
plain-language theorem explainer
Stable positions coincide exactly with the φ-ladder points. Researchers deriving quantization from J-cost minimization in Recognition Science cite this as the step that forces discrete spectrum from self-similarity. The declaration introduces the biconditional directly as a bare Prop definition grounded in the predicates IsStablePosition and PhiLadder.
Claim. For every positive real $x$, $x$ is a stable position (J-cost locally minimized) if and only if $x$ belongs to the φ-ladder.
background
The module Φ-Emergence derives the golden ratio from J-cost minimization. J-cost is given by $J(x) = (x + x^{-1})/2 - 1$. IsSelfSimilar(r) holds when $r^2 = r + 1$. PhiLadder collects the discrete positions generated by powers of φ. IsStablePosition(x) is defined to hold precisely when $x > 0$ and $x$ lies on the ladder, with the hypothesis asserting that local J-minimization coincides with this membership. Upstream, J_at_phi establishes the coherence cost at φ equals $(√5 - 2)/2$, while phi_is_self_similar proves φ is the unique positive self-similar ratio satisfying the quadratic.
proof idea
This is a direct definition of the Prop that encodes the universal biconditional. No tactics or reductions are applied; the declaration simply assembles the predicates IsStablePosition and PhiLadder already introduced in the same module and justified by the upstream lemmas J_at_phi and phi_is_self_similar.
why it matters
This supplies the core hypothesis in the φ-Emergence module that self-similar J-cost minimization forces discrete quantization at φ^n. It sits inside the forcing chain after T5 (J-uniqueness) and T6 (φ as fixed point) and before threshold derivations such as H_ThresholdFromPhi. The statement touches the open question of how the eight-tick octave interacts with the ladder to produce the unit threshold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.