phi_ladder_div_closed
plain-language theorem explainer
The theorem shows that the set of all integer powers of the golden ratio is closed under division by φ itself. Researchers constructing discrete spectra from J-cost minimization in Recognition Science would cite this algebraic closure when building the ladder of stable states. The proof is a direct term-mode reduction that extracts the witnessing integer exponent, decrements it by one, and rewrites the quotient via the power-subtraction identity.
Claim. If $x$ belongs to the set of all integer powers of the golden ratio, then $x / φ$ also belongs to that set.
background
The module derives the golden ratio from J-cost minimization. PhiLadder is the set of all φ^n for n ∈ ℤ, representing stable positions under the Recognition Composition Law. Upstream results include the cost function induced by multiplicative recognizers, the J-cost of recognition events, and energy conservation under time-translation symmetry, all of which presuppose the ladder as the discrete spectrum of allowed states.
proof idea
The term proof obtains the integer n such that x = φ^n, then supplies n-1 as the witness for the quotient. It rewrites via zpow_sub_one₀ (using phi_pos) followed by div_eq_mul_inv to obtain φ^{n-1}.
why it matters
This closure property confirms the self-similar structure of the φ-ladder required by T6, where φ is the fixed point of the forcing chain. It supplies the algebraic foundation for mass formulas of the form yardstick · φ^(rung-8+gap(Z)) and supports the eight-tick octave (T7) and D=3 emergence (T8). The result has no recorded downstream uses yet, indicating it functions as an early scaffolding lemma for later unification theorems such as the Yang-Mills mass gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.