phi_ladder_div_closed
plain-language theorem explainer
The set of all φ-powers is closed under division by φ. Modelers of discrete spectra or mass ladders in Recognition Science cite this when shifting rungs by one step. The proof is a term-mode reduction that extracts the defining integer exponent and rewrites via the zpow subtraction identity.
Claim. If $x = \phi^n$ for some $n \in \mathbb{Z}$, then $x / \phi = \phi^{n-1}$.
background
The module develops φ as the self-similar fixed point that emerges from J-cost minimization. PhiLadder is the set {x | ∃ n : ℤ, x = φ^n}. Upstream results supply the cost definitions from MultiplicativeRecognizerL4 and ObserverForcing, which treat J-cost as the derived cost on positive ratios, together with the energy-conservation statement from EnergyConservationDomainCert.
proof idea
Obtains the integer n such that x = φ^n from the membership hypothesis, replaces it by n-1, then rewrites the division using zpow_sub_one₀ (invoking phi_pos) followed by div_eq_mul_inv.
why it matters
The result supplies the downward closure half of the φ-ladder algebra, complementing the sibling phi_ladder_mul_closed. It supports the T6 self-similar fixed point and the rung structure used in YangMillsMassGap.PhiLadder and mass-gap arguments. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.