Masses Mass Genesis Phi Rung Quantization Predicted Mass Unfold Topological Labe

The mass formula on a rung

The declaration predictedMass_unfold_topological_labels is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It establishes a precise rewriting of the framework's predicted mass for a particle. The theorem states that the predicted mass of any stable light pattern equals the product of two factors: a sector-specific yardstick and the golden ratio φ raised to a power. That power is the pattern's integer topology rung minus 8, plus a small gap correction term.

In plainer language, the theorem separates the mass prediction into two parts. One part, the yardstick, sets the overall scale for a class of particles. The other part is a pure power of the golden ratio, and the exponent is built from an integer that comes from the pattern's topology. The theorem shows that this integer, called the rung, is the only part of the exponent that varies between patterns in the same sector. Stepping the rung by one multiplies the predicted mass by φ. The theorem is a definitional unfolding: it takes the existing mass formula and shows it is equivalent to this rung-based expression.

What the theorem does not claim is just as important. It does not establish that the predicted mass equals any measured rest mass. That equality remains a separate, later target in the framework's development. The theorem also does not claim that the rung integer itself is derived from first principles here; it is taken as given by the stable pattern's topology. The theorem is a structural identity, not a numerical prediction.

/-- The existing mass-law prediction expands to the topology labels. This is
only the old formula evaluated on the pattern labels; it is not the M7 theorem
that invariant load equals that prediction. -/
theorem predictedMass_unfold_topological_labels
    (ψ : LightPattern Λ) :
    predictedMass ψ =
      Anchor.yardstick (sectorOf ψ) *
        (Constants.phi ^
          ((rungOf ψ : ℝ) - 8 + MassLaw.gap_correction (ZOf ψ))) := by
  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

The theorem does not establish that predicted mass equals any measured rest mass. The theorem does not derive the rung integer from first principles. The theorem does not assign numerical values to the yardstick or the gap correction.

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: