Masses Mass Genesis Phi Rung Quantization Closed Pattern Scale Forces Universal

The universal ratio

The golden ratio, usually written φ, is the number that solves r² = r + 1, roughly 1.618. It appears across geometry and nature: in the proportions of a pentagon, in the growth of a sunflower, and in the Fibonacci sequence where each term is the sum of the two before it. The framework's declaration closedPatternScale_forces_universal_phi takes this classical constant and gives it a new job: it becomes the forced spacing between stable patterns in the framework's ledger, a discrete record of recognition events.

In Recognition Science, the framework models a stable pattern as a ledger, a discrete record of events that maintains its identity over time. The declaration proves that any closed, additive geometric scale sequence attached to such a stable pattern must have a ratio equal to φ. The key word is closed: the sequence must be able to return to its starting point after a finite number of steps. The theorem then states that this ratio is universal. For any two stable patterns, their sequence ratios are equal. The proof is direct: each ratio is shown to equal φ, so they must equal each other.

This universality is the core result. It means the ratio is not a free parameter chosen to fit data. It is forced by the structure of closure itself. The theorem is independent of the particle sector and of any empirical mass measurements. It derives the constant from the framework's own logic, not from observation. The framework's machine-checked library of formal theorems contains the proof, and the proof is axiom-clean, resting only on the standard three axioms of the underlying type theory.

The declaration also establishes a rung scale. Each stable pattern has an integer rung, a topology-derived label. The rung scale is the corresponding power of φ, and it is positive. This scale is invariant under the framework's evolution operation, meaning it does not change as the pattern evolves over time. Stepping the rung by one multiplies the scale by φ, creating a ladder of discrete scales. A stable pattern is always quantized, meaning its rung scale is always a power of φ.

What this declaration does not claim is equally important. It does not prove that the rest mass of a particle equals the mass law's prediction. That final equality remains a separate, open target. The declaration establishes the structure of the rung scale, but not the final mass value. It proves the ratio is universal, not what the masses are. The framework derives the spacing, not the content.

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χ]

theorem phiRungScale_pos (ψ : LightPattern Λ) :
    0 < phiRungScale ψ := by
  unfold phiRungScale
  exact zpow_pos Constants.phi_pos (rungOf ψ)

theorem phiRungQuantized_of_stable
    (ψ : LightPattern Λ) (_hψ : StableClosedLightPattern ψ) :
    PhiRungQuantized ψ :=
  ⟨rungOf ψ, rfl, rfl⟩

/-- 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

What this page does not claim

It does not prove that the rest mass of any particle equals the mass law's prediction. It does not claim the ratio is derived from empirical mass data. It does not establish the value of any specific particle mass.

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: