Masses Mass Genesis T10 Unit Free Anchor Wall Electron Muon No Unit Rescaling Ma

The unit-free wall

In the Recognition Science framework, particle masses are not free parameters. A mass law assigns each species a predicted mass, a number of eV computed from a ladder of golden-ratio rungs. The declaration electron_muon_no_unit_rescaling_makes_both_rational states a precise obstruction about the electron and the muon, the two lightest charged leptons. It says that no matter what positive rescaling of the mass unit you apply, you cannot make both of their predicted masses equal to rational numbers when expressed as multiples of the framework's unit posting amplitude.

The statement is a theorem in the framework's machine-checked library, proved with no gaps and no special axioms. Its content is a ratio argument. The electron sits on rung 2 of the lepton sector, the muon on rung 13, both at the same charge index. The mass law makes the ratio of their predicted masses equal to phi raised to the power 11, where phi is the golden ratio, about 1.618. That ratio is irrational, since the 11th Fibonacci number is 89, nonzero. Two rational numbers, however, always stand in a rational ratio. A common rescaling by any positive factor k cancels out of the ratio. So no choice of k can make both masses rational at once.

The theorem does not say the electron or muon mass is irrational in any absolute sense. It says only that they cannot both be rational multiples of the same unit posting. The framework's own unit posting is one amplitude; the mass law makes the amplitude scale as the square root of the mass. A single amplitude cannot serve two different masses, and the electron and muon are enough to run that argument. The declaration is the instantiated form of a more general result about any two rungs of one sector.

This unit-free wall survives a change of mass unit, which is exactly what the framework's earlier ceiling argument did not do. That ceiling compared a count against an energy in eV, and rescaling the unit could move any predicted mass below the ceiling. The ratio wall here compares two quantities that are both dimensionless once divided through, so no unit identification repairs it. The electron and muon are the concrete pair that makes the wall non-vacuous on the theory's own species table.

/-- Two rungs of one sector at one charge index stand in ratio `phi ^ (r' - r)`. -/
theorem predict_mass_rung_ratio (s : Anchor.Sector) (r r' Z : ℤ) :
    MassLaw.predict_mass s r' Z
      = phi ^ (r' - r) * MassLaw.predict_mass s r Z := by
  have hcast : (r' : ℝ) - (r : ℝ) = ((r' - r : ℤ) : ℝ) := by push_cast; ring
  rw [predict_mass_rung_shift s r r' Z, hcast, Real.rpow_intCast]

/-- `phi ^ n` is irrational whenever its Fibonacci coefficient is nonzero, which is
every `n` except zero. `phi_zpow_eq_fib` supplies the closed form. -/
theorem phi_zpow_irrational {n : ℤ} (hn : Int.fib n ≠ 0) :
    Irrational (phi ^ n) := by
  rw [Constants.PhiLadder.phi_zpow_eq_fib n]
  exact (Constants.PhiLadder.phi_irrational.intCast_mul hn).add_intCast _

/-- The electron against the muon: rungs `2` and `13`, ratio `phi ^ 11`, and
`Int.fib 11 = 89`. So no mass unit makes both leptons rational compositions of the
ledger's unit posting. -/
theorem electron_muon_no_unit_rescaling_makes_both_rational
    {k : ℝ} (hk : 0 < k) (q q' : ℚ) :
    ¬ (k * (MassLaw.predict_mass Anchor.Sector.Lepton 2 1332 / 8) = (q : ℝ) ∧
        k * (MassLaw.predict_mass Anchor.Sector.Lepton 13 1332 / 8) = (q' : ℝ)) := by
  refine no_unit_rescaling_makes_two_rungs_rational Anchor.Sector.Lepton 1332 ?_ hk q q'
  decide

/-- **The ceiling wall does not survive a change of mass unit.** For every pattern
there is a positive rescaling of the mass unit placing its rescaled predicted mass
below the Boolean ceiling. Nothing about the pattern is used except that its
predicted mass is positive, so this applies to the whole charged spectrum. -/
theorem exists_unit_rescaling_below_ceiling (ψ : LightPattern (Fin 8)) :
    ∃ k : ℝ, 0 < k ∧ k * predictedMass ψ < 64 := by
  have hpos : 0 < predictedMass ψ := predictedMass_pos ψ
  refine ⟨1 / predictedMass ψ, div_pos one_pos hpos, ?_⟩
  have hcancel : 1 / predictedMass ψ * predictedMass ψ = 1 := by
    field_simp
  rw [hcancel]
  norm_num

What this page does not claim

The electron or muon mass is irrational in any absolute sense, only that they cannot both be rational multiples of the same unit posting. The framework derives the numerical values of the electron and muon masses in eV from first principles. The unit-free wall explains why the electron and muon have the masses they do, rather than any other pair of rungs.

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/T10UnitFreeAnchorWall.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: