Masses Mass Genesis T10 Phased Posting Mass Ratio Wall Phased Posting Integrated

The load floor

The declaration phasedPosting_integratedLoad_ge_sevenEighths is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It concerns a ledger, a discrete record of events, in which each event is a posting, an entry in that record. The theorem states that if a stable, closed pattern of such postings has at least one site with positive load, then the total integrated load across all sites is at least seven eighths. The number seven eighths is not arbitrary: it falls out of the fact that each site carries at most eight units, and stability forces at least one site to carry a positive amount, which itself must be at least seven eighths.

The theorem is a lower bound on a quantity the framework calls rest mass. That quantity is defined as the integrated meaning load on stable closed patterns, a modelling choice that the library does not derive. The bound transfers to physical mass only under that choice. The theorem's real strength appears when it is combined with its upper-bound counterpart to form a ratio. Any two stable closed patterns whose occupied windows are postings up to a global phase have a rest mass ratio at most 512/7, about 73.14. This is a ratio against ratio, so no unit enters and no mass-law formula sits on either side.

The framework then compares that ceiling to a measured value. The measured muon-to-electron mass ratio, from the Particle Data Group 2024, is 206.7682830 with an uncertainty of 0.0000046. The accepted window of 512/7 is below that measured ratio by a factor of 2.83, which is about 2.9 times ten to the seventh standard deviations. The theorem therefore refutes the conjunction that realized matter patterns are postings up to phase and that the site index is Fin 8. Which conjunct fails is not decided. The exclusion is a closed arithmetic fact because the measured value is carried as a numeral in the library, not as a claim about the physical world.

The theorem does not claim that any specific particle has a particular mass, nor does it derive a mass formula, a rung table, a sector power, or a yardstick. It does not say that the muon-to-electron ratio is impossible in general, only that it is impossible under the specific hypothesis that realized matter windows are postings up to phase on eight sites. The load-bearing hypothesis is the posting alphabet at every occupied site, and nothing else: full support, window equivariance, the Q3 support action, uniform site load, and gauge fixing are all unused. The theorem is a leaf in the library, meaning nothing imports it, so the verification receipt is a one-time hand check at a particular commit, not a standing guarantee.

/-- Stability supplies one occupied site of positive load, and the floor lifts to
the total. -/
theorem phasedPosting_integratedLoad_ge_sevenEighths {ψ : LightPattern (Fin 8)}
    (hb : ∀ x ∈ ψ.support, IsPhasedPosting (ψ.window x))
    (hnt : NontrivialNeutralLoad ψ) :
    7 / 8 ≤ integratedMeaningLoad ψ := by
  obtain ⟨x, hx, hpos⟩ := hnt
  have hsite : 7 / 8 ≤ siteMeaningLoad ψ x :=
    phasedPosting_load_pos_ge_sevenEighths (hb x hx) hpos
  have hle : siteMeaningLoad ψ x ≤ integratedMeaningLoad ψ := by
    rw [integratedMeaningLoad_eq_support_sum]
    exact Finset.single_le_sum (fun y _ => siteMeaningLoad_nonneg ψ y) hx
  linarith

/-- **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 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 instantiated refutation.** No two stable closed patterns with
phased-posting windows on `Fin 8` can stand in the measured muon-to-electron mass
ratio. Since the muon and the electron do stand in that ratio, at least one of
"realized matter windows are postings up to phase" and "the site index is `Fin 8`"
is false. -/
theorem phasedPosting_excludes_measured_muonElectron {ψ χ : LightPattern (Fin 8)}
    (hsψ : StableClosedLightPattern ψ) (hsχ : StableClosedLightPattern χ)
    (hbψ : ∀ x ∈ ψ.support, IsPhasedPosting (ψ.window x))
    (hbχ : ∀ x ∈ χ.support, IsPhasedPosting (χ.window x)) :
    restMass ψ ≠ measuredMuonElectronMassRatio * restMass χ :=
  phasedPosting_ratio_excluded hsψ hsχ hbψ hbχ (by
    unfold measuredMuonElectronMassRatio; norm_num)

What this page does not claim

The theorem does not decide which of the two conjuncts in the refuted conjunction is false. The theorem does not derive a mass formula, a rung table, a sector power, or a yardstick for any particle. The theorem does not claim that the muon-to-electron ratio is impossible in general, only under the specific hypothesis of phased postings on eight sites.

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: