Encyclopedia Masses Masses Mass Genesis T10 Phased Posting Mass Ratio Wall Phased Posting Excludes M

ARTICLE 4 claims 3 theorems 1 model

Masses Mass Genesis T10 Phased Posting Mass Ratio Wall Phased Posting Excludes M

A machine-checked theorem says two hypothetical matter patterns cannot have the muon-to-electron mass ratio, and the proof names exactly which assumption fails.

Verify this page

The ratio wall

The muon is about 206.7682830 times heavier than the electron, a ratio measured to seven decimal places (PDG 2024). The declaration phasedPosting_excludes_measured_muonElectron is a theorem in the framework's machine-checked library of formal theorems. It proves that no two stable, closed patterns of the kind the framework studies can stand in that exact ratio. The proof is a closed arithmetic fact: the largest ratio such patterns can have is 512/7, about 73.14, and the measured ratio is larger by a factor of 2.83, roughly 29 million standard deviations.

The framework models matter as patterns of ledger postings, a discrete record of events on a finite set of sites. A posting is a number attached to a site, and a window is the collection of postings at all sites. The theorem assumes each occupied window is a phased posting: some single global rotation of the window makes every entry a Boolean value, either 0, 1, or -1. This is a gauge-invariant condition, because rotating the whole window by one phase does not change the load, the sum of squared magnitudes after removing the average. The proof shows the load per site is at most 8 and at least 7/8, so the total load of any pattern is between those bounds, and the ratio of two such totals cannot exceed 64 divided by 7/8, which is 512/7.

The theorem does not say which assumption fails. It states a conjunction: that realized matter windows are postings up to phase, and that the site index is eight. The measured ratio refutes that conjunction, but the proof does not decide whether the posting hypothesis is wrong or the number of sites is wrong. The theorem also does not derive the mass ratio, only bounds it. It carries no mass-law formula, no rung table, and no unit, because it compares ratios, not absolute values. The bound on rest mass transfers to physical mass only under a modelling choice that defines rest mass as integrated meaning load, a choice the library does not derive.

The verification receipt is a one-time hand check at a specific commit, not a standing guarantee. The module is a leaf, imported by nothing, so it sits in no build target and CI does not elaborate it. Anyone quoting these theorems should rebuild the module rather than trust the header. The proof audits to the standard three axioms, but that is a statement about postulates, not about the ambient type theory, which still supplies the universe hierarchy, inductive formation, and dependent types.

THEOREM phasedPosting_excludes_measured_muonElectron · IndisputableMonolith/Masses/MassGenesis/T10PhasedPostingMassRatioWall.lean
phasedPosting_excludes_measured_muonElectron · IndisputableMonolith/Masses/MassGenesis/T10PhasedPostingMassRatioWall.lean:256 
/-- **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)
THEOREM phasedPosting_restMass_ratio_le · measured_muonElectron_exceeds_ceiling · IndisputableMonolith/Masses/MassGenesis/T10PhasedPostingMassRatioWall.lean
phasedPosting_restMass_ratio_le · IndisputableMonolith/Masses/MassGenesis/T10PhasedPostingMassRatioWall.lean:219 
/-- **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]
measured_muonElectron_exceeds_ceiling · IndisputableMonolith/Masses/MassGenesis/T10PhasedPostingMassRatioWall.lean:269 
/-- 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
THEOREM phasedPosting_excludes_measured_muonElectron · IndisputableMonolith/Masses/MassGenesis/T10PhasedPostingMassRatioWall.lean
phasedPosting_excludes_measured_muonElectron · IndisputableMonolith/Masses/MassGenesis/T10PhasedPostingMassRatioWall.lean:256 
/-- **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)
MODEL phasedPosting_restMass_ratio_le · IndisputableMonolith/Masses/MassGenesis/T10PhasedPostingMassRatioWall.lean
phasedPosting_restMass_ratio_le · IndisputableMonolith/Masses/MassGenesis/T10PhasedPostingMassRatioWall.lean:219 
/-- **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]

What this page does not claim

The theorem does not derive the muon-to-electron mass ratio, only excludes it. The theorem does not claim the posting hypothesis is false, nor that the eight-site index is false. The verification receipt is a one-time hand check, not a standing guarantee.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND