IsStablePosition
plain-language theorem explainer
A real number is stable when positive and an element of the phi-ladder. Researchers modeling J-cost minimization for self-similar patterns cite this predicate to identify the discrete states that emerge. The declaration is a direct definition that conjoins positivity with ladder membership.
Claim. A real number $x$ is a stable position when $x > 0$ and $x = phi^n$ for some integer $n$.
background
The module develops emergence of the golden ratio from J-cost minimization. The doc-comment states that a position $x > 0$ is stable if J-cost is locally minimized there, and that self-similar patterns require the ratio to satisfy $r^2 = r + 1$ for stability. The phi-ladder is the set of all $phi^n$ for $n$ in integers, per the upstream PhiLadder definition in the same module and the parallel definition in YangMillsMassGap.
proof idea
This is a definition that directly sets the predicate to the conjunction of $x > 0$ and membership in the phi-ladder set. No lemmas or tactics are applied.
why it matters
The predicate supports the hypothesis H_StableIffPhiLadder that stable positions coincide exactly with the phi-ladder, the core claim that self-similar J-cost minimization forces discrete quantization at phi powers. It is also used by the theorem showing all phi-ladder positions are stable. This aligns with the framework step forcing phi as the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.