rung_separation
plain-language theorem explainer
rung_separation establishes that the φ-ladder is self-similar: for any positive yardstick ys the mass at rung n+k divided by the mass at rung n equals φ^k. Particle physicists modeling mass hierarchies from Recognition Science would cite this when scaling across generations or tiers on the ladder. The short term-mode proof reduces the ratio directly by unfolding the mass definition, applying real exponent additivity, and simplifying with ring.
Claim. Let $y_s > 0$. For integers $n,k$, the mass function on the φ-ladder satisfies $m(y_s,n+k)/m(y_s,n) = φ^k$, where $m(y_s,r)$ denotes the mass at rung $r$ scaled by yardstick $y_s$.
background
The Spectral Emergence module derives the Standard Model gauge structure and mass hierarchy from the binary cube Q₃ forced by D=3. The φ-ladder arises as the discrete mass spectrum on Q₃ edges, with rung integers labeling levels and J-cost supplying the exponential scaling. mass_rung ys r is the explicit mass function at rung r for yardstick ys, known to be positive by the upstream lemma mass_rung_pos. The module imports Constants.phi and Cost to enforce the self-similar property required by the Recognition Composition Law.
proof idea
The term proof first obtains mass_rung ys n ≠ 0 from mass_rung_pos ys hys n. It rewrites the division claim via div_eq_iff, unfolds mass_rung, casts the integer sum n+k to reals, invokes Real.rpow_add on the positive base phi, and finishes with ring.
why it matters
This algebraic identity closes the self-similarity step of the φ-ladder mass hierarchy inside Spectral Emergence, directly supporting the yardstick * φ^(rung) formula that follows from T6 (phi forced) and T8 (D=3). It supplies the scaling relation used to place particle masses on the ladder without free parameters. No downstream theorems yet reference it, but it is a prerequisite for any quantitative mass prediction in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.