Masses Mass Genesis Phi Rung Quantization Closed Pattern Scale Ratio Eq Phi

The forced ratio

A geometric scale sequence is a list of numbers where each term is a fixed multiple of the one before it, like 1, 2, 4, 8. The fixed multiple is the ratio. The theorem closedPatternScale_ratio_eq_phi states that if such a sequence is closed, meaning it wraps around on itself consistently, and it is attached to a stable pattern in the framework, then that ratio must be the golden ratio, φ. The golden ratio is the number that satisfies r² = r + 1, approximately 1.618. The proof is a direct consequence of a prior result in the framework's library, closed_ratio_is_phi, which shows that closure alone forces the ratio.

The statement is universal across all stable patterns. A second theorem, closedPatternScale_forces_universal_phi, shows that any two such closed sequences, even from different particle sectors, have the same ratio. This is what makes the ratio a universal constant of the framework rather than a property of one particular pattern. The ratio does not depend on any empirical mass data; it is a purely structural consequence of the closure condition.

In Recognition Science, this result sits at the bottom of a ladder. The framework models a particle as a stable closed light pattern, and the pattern carries a topology-derived integer rung. The rung scale, the actual size associated with that rung, is a power of φ. The theorem phiRungScale_step proves that stepping the rung up by one multiplies the scale by φ. So the ratio φ is not an input; it is forced by the geometry of closure, and the rung ladder then quantizes the scales into discrete φ-powered steps.

What the theorem does not claim is the final mass law. The framework's own documentation is explicit: this theorem does not prove that the rest mass of a pattern equals the framework's predicted mass. That equality remains a separate, later result. The ratio is a property of the scale sequence, not a derivation of particle masses. The masses, when they come, will use this ratio, but the ratio itself is established here independently of any mass formula.

The practical consequence is a clean separation of concerns. The framework can prove a universal scaling ratio from pure closure, and then separately attempt to attach that ratio to physical masses. The first part is a theorem; the second part is a further step. A reader can trust the ratio without yet trusting the mass law, because the ratio's proof does not depend on it.

theorem closedPatternScale_ratio_eq_phi
    {ψ : LightPattern Λ} (S : ClosedPatternScale ψ) :
    S.sequence.ratio = Constants.phi :=
  Foundation.PhiForcingDerived.closed_ratio_is_phi S.sequence S.closed

/-- The universal ratio forced by a closed pattern scale is independent of
the particle sector and of empirical mass data. -/
theorem closedPatternScale_forces_universal_phi
    {ψ χ : LightPattern Λ}
    (Sψ : ClosedPatternScale ψ) (Sχ : ClosedPatternScale χ) :
    Sψ.sequence.ratio = Sχ.sequence.ratio := by
  rw [closedPatternScale_ratio_eq_phi Sψ,
      closedPatternScale_ratio_eq_phi Sχ]

/-- A one-rung topology step multiplies the rung scale by `phi`. -/
theorem phiRungScale_step
    (ψ χ : LightPattern Λ)
    (hstep : rungOf χ = rungOf ψ + 1) :
    phiRungScale χ = Constants.phi * phiRungScale ψ := by
  unfold phiRungScale
  rw [hstep]
  calc
    Constants.phi ^ (rungOf ψ + 1)
        = Constants.phi ^ (rungOf ψ) * Constants.phi ^ (1 : ℤ) := by
            rw [zpow_add₀ Constants.phi_ne_zero]
    _ = Constants.phi ^ (rungOf ψ) * Constants.phi := by
            simp
    _ = Constants.phi * Constants.phi ^ (rungOf ψ) := by
            ring

theorem closedPatternScale_ratio_eq_phi
    {ψ : LightPattern Λ} (S : ClosedPatternScale ψ) :
    S.sequence.ratio = Constants.phi :=
  Foundation.PhiForcingDerived.closed_ratio_is_phi S.sequence S.closed

What this page does not claim

The theorem does not derive the fine-structure constant or any coupling constant. It does not prove the Riemann Hypothesis or any equivalent statement. It does not establish that any particular particle's mass equals the predicted value; that remains a separate, later result.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Masses/MassGenesis/PhiRungQuantization.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: