Foundation Maximal Forcing Rsmass Ladder Universe Forced Ladder Ratio

The forced ladder ratio

In the Recognition Science framework, particle masses are modeled as sitting on a ladder: each rung's mass is the previous rung's mass multiplied by a fixed number. The declaration forced_ladderRatio establishes, as a proved theorem in the framework's machine-checked library of formal theorems, that this fixed multiplier is the golden ratio φ. The claim is that for any starting mass (called the yardstick) and for every rung index r, the mass at rung r+1 equals φ times the mass at rung r. The proof is a structural identity: it follows directly from the definition of the ladder, with no additional assumptions about the yardstick.

The theorem's substance is a separation between two kinds of claims. The ratio between adjacent rungs is a dimensionless invariant: it does not depend on what the starting mass is. The framework proves this ratio is forced, meaning it holds for every possible yardstick. In contrast, the absolute value of the yardstick itself is independent: the framework provides an explicit countermodel showing that two different yardsticks, 1 and 2, both satisfy the ladder definition but disagree on whether the yardstick equals 1. This establishes that the absolute mass scale is a free coordinate, not a forced invariant.

This result is the first in the framework's mass-ladder layer whose closure certificate uses both branches of the framework's trichotomy: one claim is classified as forced, the other as independent. The framework's classifier proves that every claim in the mass-ladder universe falls into one of three categories: forced, independent, or selected. Here, the scaling invariant is forced and the yardstick is independent, with the selected category empty. The practical consequence is that dimensionless structure is determined by the framework, while absolute units remain a matter of choice.

The theorem does not claim that the golden ratio is the only possible ratio, nor does it derive the absolute mass scale. It does not assert that any particular particle's mass is predicted. It establishes only the relative scaling between adjacent rungs, given the ladder's definition. The yardstick's independence means the framework cannot, from this theorem alone, say what the mass of the first rung is; that remains an open coordinate.

/-- **The phi-ladder scaling invariant is forced over every yardstick.** No gate
is required: the recurrence is a structural identity of the ladder. -/
theorem forced_ladderRatio : Forced Lmass0.admissible isLadderRatioClaim := by
  intro M0 _ r
  show ladderMass M0 (r + 1) = φ * ladderMass M0 r
  unfold ladderMass
  rw [pow_succ]
  ring

/-- The yardstick claim is independent (Prop-level), via the witness. -/
theorem yardstick_independent : Independent Lmass0.admissible isYardstickClaim :=
  independent_of_witness yardstickIndepWitness

/-- **Crown trichotomy on the mass-ladder universe.** Every closure claim is
`Forced`, `Independent`, or `Selected`. Here the closure splits into one forced
invariant and one independent coordinate, with `Selected` empty. -/
theorem massUniverse_trichotomy
    (C : RealityClaim massUniverse.Realization)
    (hC : InClosure Primitive.lawOfLogic massUniverse C) :
    Forced Lmass0.admissible C ∨ Independent Lmass0.admissible C ∨ Selected Lmass0.admissible C :=
  maximal_forcing_closure_trichotomy massUniverseCert C hC

What this page does not claim

The theorem does not derive the absolute mass scale or predict any specific particle mass. It does not claim the golden ratio is the only possible ratio for a mass ladder outside this framework's definition. It does not assert that the yardstick's independence extends to other frameworks or physical theories.

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/Foundation/MaximalForcing/RSMassLadderUniverse.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: