Masses Mass Genesis T10 Phased Posting Mass Ratio Wall

The mass ratio wall

In physics, the muon is a heavier cousin of the electron, and the ratio of their masses is a measured number: 206.7682830, with an uncertainty of 0.0000046 in the last digits, from the 2024 Particle Data Group. Any theory of particle masses must explain why that ratio is what it is. Recognition Science approaches the problem by treating matter patterns as discrete records, called ledger postings, where each posting is a window of eight complex amplitudes that carries a load, a measure of its size.

The module in question, T10, proves a hard ceiling on that load. The argument is simple. Each of the eight sites in a window can carry at most 8 units of load, so the total load of any pattern is at most 64. Stability, a condition that the pattern persists, forces at least one site to carry positive load, and the smallest positive load allowed is 7/8. Therefore the ratio of the largest possible load to the smallest possible positive load is 64 divided by 7/8, which equals 512/7, about 73.14. The theorem states this as a bound on rest mass: any two stable patterns have a rest mass ratio at most 512/7.

The wall is stated in a deliberately weak form. Earlier versions assumed a stronger condition, that each posting amplitude is exactly 0, 1, or -1. That assumption is fragile: a global phase rotation, a symmetry of the theory, can turn such a window into one with no Boolean entries at all. The repair is to say a window is a phased posting if some single rotation of it is Boolean. This class is closed under the symmetry, and the load is exactly unchanged by the rotation, so the bound survives. The theorem is checked in a machine-checked library of formal theorems, with no unproved axioms beyond the standard logical ones.

Here is the consequence. The measured muon-to-electron ratio, 206.7682830, is about 2.83 times larger than 73.14, a gap of roughly 29 million standard deviations. The framework's theorem says no two stable patterns with phased-posting windows can stand in that ratio. Since the muon and electron do stand in that ratio, at least one of two conjuncts must be false: either realized matter windows are not postings up to phase, or the site index is not eight. The module does not decide which one fails. It also does not claim the bound transfers to physical mass in any direct way, because rest mass here is defined as the integrated load on stable patterns, a modelling choice.

/-- The measured muon-to-electron mass ratio, PDG 2024: `206.7682830(46)`. An
external measurement, carried as a numeral so the exclusion below is a closed
arithmetic fact rather than a claim about the physical world. -/
def measuredMuonElectronMassRatio : ℝ := 206.7682830

/-- **The phased-posting mass ratio wall.** Any two stable closed patterns whose
occupied windows are ledger postings up to phase have rest mass ratio at most
`512/7 ≈ 73.14`. No Q3 hypothesis, no unit, no mass-law constant. -/
theorem phasedPosting_restMass_ratio_le {ψ χ : LightPattern (Fin 8)}
    (hsψ : StableClosedLightPattern ψ) (hsχ : StableClosedLightPattern χ)
    (hbψ : ∀ x ∈ ψ.support, IsPhasedPosting (ψ.window x))
    (hbχ : ∀ x ∈ χ.support, IsPhasedPosting (χ.window x)) :
    restMass ψ ≤ (512 / 7) * restMass χ := by
  rw [restMass_eq_integratedMeaningLoad_of_stable ψ hsψ,
      restMass_eq_integratedMeaningLoad_of_stable χ hsχ]
  have hup : integratedMeaningLoad ψ ≤ 64 :=
    phasedPosting_integratedLoad_le_sixtyFour hbψ
  have hlo : 7 / 8 ≤ integratedMeaningLoad χ :=
    phasedPosting_integratedLoad_ge_sevenEighths hbχ hsχ.2.1
  nlinarith [hup, hlo]

/-- The accepted window really is below the measured ratio, stated separately so
the strength of the exclusion is a checked fact and not a comment. -/
theorem measured_muonElectron_exceeds_ceiling :
    (512 : ℝ) / 7 < measuredMuonElectronMassRatio := by
  unfold measuredMuonElectronMassRatio; norm_num

/-- **The class is gauge closed**, which raw Boolean-ness is not. -/
theorem isPhasedPosting_gauge_closed {w : PhotonWindow} {c : ℂ}
    (hc : Complex.normSq c = 1) (h : IsPhasedPosting w) :
    IsPhasedPosting (fun t => c * w t) := by
  obtain ⟨u, hu, hbool⟩ := h
  refine ⟨u * (starRingEnd ℂ) c, ?_, ?_⟩
  · rw [Complex.normSq_mul, Complex.normSq_conj, hu, hc, one_mul]
  · intro t
    have hcc : (starRingEnd ℂ) c * c = 1 := by
      have hmc := Complex.mul_conj c
      rw [mul_comm] at hmc
      rw [hmc, hc]
      norm_num
    show IsBooleanPostingAmplitude (u * (starRingEnd ℂ) c * (c * w t))
    have heq : u * (starRingEnd ℂ) c * (c * w t)
        = u * ((starRingEnd ℂ) c * c) * w t := by ring
    rw [heq, hcc, mul_one]
    exact hbool t

/-- At most eight sites, each at most `8`. -/
theorem phasedPosting_integratedLoad_le_sixtyFour {ψ : LightPattern (Fin 8)}
    (hb : ∀ x ∈ ψ.support, IsPhasedPosting (ψ.window x)) :
    integratedMeaningLoad ψ ≤ 64 := by
  rw [integratedMeaningLoad_eq_support_sum]
  have hterm : ∀ x ∈ ψ.support, siteMeaningLoad ψ x ≤ 8 := by
    intro x hx
    exact phasedPosting_load_le_eight (hb x hx)
  have hsum : ∑ x ∈ ψ.support, siteMeaningLoad ψ x ≤ ψ.support.card • (8 : ℝ) :=
    Finset.sum_le_card_nsmul _ _ _ hterm
  have hcard : (ψ.support.card : ℝ) ≤ 8 := by
    have := Finset.card_le_univ ψ.support
    simpa [Fintype.card_fin] using (Nat.cast_le (α := ℝ)).mpr this
  have : ψ.support.card • (8 : ℝ) = (ψ.support.card : ℝ) * 8 := by
    simp [nsmul_eq_mul]
  rw [this] at hsum
  nlinarith [hsum, hcard]

What this page does not claim

The module does not identify which of the two assumptions is false. The bound does not transfer to physical mass without the modelling choice that rest mass equals integrated load. The wall does not derive any mass-law formula or predict any particle mass value.

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