Masses Mass Genesis T10 Q3 Uniform Site Mass Wall

The uniform-site mass wall

The muon is about 206.7682830 times heavier than the electron. That ratio is one of the most precisely measured numbers in physics, with an uncertainty of a few parts per million. The module called the uniform-site mass wall asks whether the framework's own picture of matter could ever produce such a spread. The answer it proves is no, under one specific hypothesis.

The framework models a particle as a pattern on eight sites, the vertices of a three-dimensional cube. The number eight is not chosen: the framework derives three spatial dimensions and the eight positions from its core cost function. A ledger, a discrete record of events, assigns a load to each site. The wall assumes two things. First, the particle is a closed pattern on all eight sites. Second, each site's load is Boolean, meaning it can only be 0, 1, or -1. Under those two assumptions, the total load of any such particle must lie between 7 and 64.

That bound is the whole point. If every particle's total load sits in the range 7 to 64, then the ratio of any two such loads cannot exceed 64 divided by 7, roughly 9.14. But the measured muon-to-electron mass ratio is 206.7682830, far beyond that ceiling. The framework's library of machine-checked theorems proves this contradiction directly: no two particles satisfying both assumptions can have loads in the measured ratio. The wall fires.

The proof is not vacuous. The library exhibits a concrete example, a gap-one worldline pattern, that satisfies both assumptions and has total load 16. So the wall rules out a real class of objects, not an empty one. The comparison is ratio against ratio, so no units enter and no mass formula sits on either side. The identity that rest mass equals integrated load for stable closed patterns is untouched by this result.

What the wall establishes is a boundary. It does not say the framework cannot produce the muon and electron. It says the framework cannot produce them if both are closed Boolean patterns on eight equal sites. The hypothesis fails against measurement, so the framework must look elsewhere: non-Boolean windows, unequal site loads, or carriers that are not closed patterns. The wall is a refutation of a specific conjunction, and it is a proved one.

/-- Lower and upper bounds on the integrated load of a Q3 closed pattern whose
anchor window is Boolean and whose site-0 load is positive. -/
theorem q3_boolean_integratedLoad_mem_Icc
    {ψ : LightPattern (Fin 8)}
    (E : Q3ClosedPatternEvidence ψ)
    (hb : BooleanDifferenceSettlementWindow (ψ.window 0))
    (hpos : 0 < siteMeaningLoad ψ 0) :
    7 ≤ integratedMeaningLoad ψ ∧ integratedMeaningLoad ψ ≤ 64 := by
  have htot := q3_integratedLoad_eq_eight_mul_anchor E
  have hsite : siteMeaningLoad ψ 0 = normSq8 (neutralize (ψ.window 0)) := rfl
  rw [hsite] at hpos
  have hlow := booleanWindow_load_pos_ge_sevenEighths hb hpos
  have hhigh := booleanWindow_neutralizedNormSq_le hb
  rw [← hsite] at hlow hhigh
  constructor
  · have : (7 : ℝ) ≤ 8 * siteMeaningLoad ψ 0 := by nlinarith
    rwa [← htot] at this
  · have : 8 * siteMeaningLoad ψ 0 ≤ (64 : ℝ) := by nlinarith
    rwa [← htot] at this

/-- Any two positive-load Q3 Boolean carriers have integrated-load ratio at most
`64/7`. -/
theorem q3_boolean_mass_ratio_le_sixtyFourSevenths
    {ψ χ : LightPattern (Fin 8)}
    (Eψ : Q3ClosedPatternEvidence ψ) (Eχ : Q3ClosedPatternEvidence χ)
    (hbψ : BooleanDifferenceSettlementWindow (ψ.window 0))
    (hbχ : BooleanDifferenceSettlementWindow (χ.window 0))
    (hposψ : 0 < siteMeaningLoad ψ 0) (hposχ : 0 < siteMeaningLoad χ 0) :
    integratedMeaningLoad ψ ≤ (64 / 7) * integratedMeaningLoad χ := by
  obtain ⟨_, hψ64⟩ := q3_boolean_integratedLoad_mem_Icc Eψ hbψ hposψ
  obtain ⟨hχ7, _⟩ := q3_boolean_integratedLoad_mem_Icc Eχ hbχ hposχ
  have h64 : (64 : ℝ) = (64 / 7) * 7 := by norm_num
  calc
    integratedMeaningLoad ψ ≤ 64 := hψ64
    _ = (64 / 7) * 7 := h64
    _ ≤ (64 / 7) * integratedMeaningLoad χ :=
      mul_le_mul_of_nonneg_left hχ7 (by norm_num : (0 : ℝ) ≤ 64 / 7)

theorem muonElectronMassRatio_gt_bound :
    (64 / 7 : ℝ) < muonElectronMassRatio := by
  norm_num [muonElectronMassRatio]

/-- The wall fires on a real object: nothing admissible sits at the measured
muon-to-electron multiple of the gap-one worldline's load `16`
(that target would be about `3308.29`, above the ceiling `64`). -/
theorem no_q3_boolean_partner_at_muon_ratio
    {χ : LightPattern (Fin 8)}
    (Eχ : Q3ClosedPatternEvidence χ)
    (hbχ : BooleanDifferenceSettlementWindow (χ.window 0))
    (hposχ : 0 < siteMeaningLoad χ 0) :
    integratedMeaningLoad χ ≠
      muonElectronMassRatio *
        integratedMeaningLoad (worldlinePattern gapOneTwoPhaseMode) := by
  intro heq
  rw [gapOneWorldline_integratedLoad_eq_sixteen] at heq
  have hle : integratedMeaningLoad χ ≤ 64 :=
    (q3_boolean_integratedLoad_mem_Icc Eχ hbχ hposχ).2
  have hmul : muonElectronMassRatio * 16 ≤ 64 := by
    rwa [heq] at hle
  have hbound := muonElectronMassRatio_gt_bound
  -- `64/7 < r` and `r * 16 ≤ 64` are incompatible
  nlinarith

/-- Total load is eight times the anchor: `8 * 2 = 16`. -/
theorem gapOneWorldline_integratedLoad_eq_sixteen :
    integratedMeaningLoad (worldlinePattern gapOneTwoPhaseMode) = 16 := by
  rw [q3_integratedLoad_eq_eight_mul_anchor gapOneWorldline_q3Evidence,
    gapOneWorldline_anchor_load_eq_two]
  norm_num

What this page does not claim

This wall does not derive any particle mass or mass ratio. This wall does not refute the identity that rest mass equals integrated load for stable closed patterns. This wall does not apply to particles that are not closed patterns on eight sites with Boolean site loads.

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