rung_separation
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not fix the absolute yardstick ys or its physical units.
- Does not include the gap(Z) correction for specific particle species.
- Does not extend to non-integer rung separations.
- Does not derive the numerical value of phi or its forcing from T6.
formal statement (Lean)
309theorem rung_separation (ys : ℝ) (hys : 0 < ys) (n k : ℤ) :
310 mass_rung ys (n + k) / mass_rung ys n = phi ^ (k : ℝ) := by
proof body
Term-mode proof.
311 have hmr : mass_rung ys n ≠ 0 := ne_of_gt (mass_rung_pos ys hys n)
312 rw [div_eq_iff hmr]
313 unfold mass_rung
314 rw [show ((n + k : ℤ) : ℝ) = (n : ℝ) + (k : ℝ) from by push_cast; ring]
315 rw [Real.rpow_add phi_pos]
316 ring
317
318/-! ## Part 6: The Consciousness Ground State — Zero Defect
319
320The unique zero-cost state (x = 1, J(1) = 0) is the **consciousness
321ground state**: the recognition configuration with zero defect.
322
323All particles live ABOVE this ground state (J > 0). Consciousness IS
324the ground state — the unique zero-defect configuration on the Q₃ lattice.
325
326The "hard problem" dissolves: consciousness is not an emergent property
327but the GROUND STATE of the spectral decomposition. -/
328
329/-- A recognition state on the Q₃ lattice: an assignment of ratios
330 to the 8 vertices, each positive. -/