Encyclopedia Masses Masses Mass Genesis T10 Q3 Uniform Site Mass Wall Electron Muon Not Both Q3 Bool

ARTICLE 5 claims 4 theorems 1 measured

Masses Mass Genesis T10 Q3 Uniform Site Mass Wall Electron Muon Not Both Q3 Bool

A machine-checked proof shows that within one proposed framework, the electron and muon cannot both be simple Boolean patterns; the measured mass ratio forbids it.

Verify this page

The Boolean mass wall

The electron and the muon are two of the lightest known particles, and the muon is about 206.7682830 times heavier than the electron. Any theory that tries to build both from the same kind of basic object must explain that large ratio. The Recognition Science framework, which models reality as a discrete record of recognition events, proposes that stable particles are closed patterns on an eight-site cube. The declaration electron_muon_not_both_q3_boolean_carriers is a machine-checked theorem that rules out one simple version of that idea.

In the framework, a recognition event is a unit of record, and a particle's mass is modeled as the total load of meaning carried by its pattern. The theorem starts with a hypothesis: each of the eight sites on the cube carries a load that is either 0, 1, or -1, a Boolean alphabet. Under that hypothesis, the framework proves that any such particle's total load must lie between 7 and 64. Therefore the ratio of the total loads of any two such particles can be at most 64/7, which is about 9.14.

The measured muon-to-electron mass ratio is 206.7682830, far larger than 9.14. The theorem states that if two particles both satisfy the Boolean-site condition and their load ratio equals the measured mass ratio, a contradiction follows. In plain language: within this framework, the electron and muon cannot both be simple Boolean patterns on the eight-site cube. The proof is formal and machine-checked, with no gaps and no special axioms added for this result.

The theorem does not say that the framework's mass model is wrong. It leaves untouched the identity that links rest mass to integrated load for stable closed patterns. It also does not provide a mass formula, a table of particle rungs, or a yardstick for absolute masses. What it does is narrow the search: if the electron and muon are both to be explained by this framework, they cannot both be Boolean-site patterns. The class of such patterns is not empty, since the framework exhibits a concrete example with total load 16, so the refutation applies to a real possibility, not to a phantom.

MEASURED muonElectronMassRatio · IndisputableMonolith/Masses/MassGenesis/T10Q3UniformSiteMassWall.lean
muonElectronMassRatio · IndisputableMonolith/Masses/MassGenesis/T10Q3UniformSiteMassWall.lean:255 
/-- PDG 2024: `m_μ / m_e = 206.7682830(46)`. -/
def muonElectronMassRatio : ℝ := 206.7682830
THEOREM q3_boolean_integratedLoad_mem_Icc · IndisputableMonolith/Masses/MassGenesis/T10Q3UniformSiteMassWall.lean
q3_boolean_integratedLoad_mem_Icc · IndisputableMonolith/Masses/MassGenesis/T10Q3UniformSiteMassWall.lean:213 
/-- 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
THEOREM q3_boolean_mass_ratio_le_sixtyFourSevenths · IndisputableMonolith/Masses/MassGenesis/T10Q3UniformSiteMassWall.lean
q3_boolean_mass_ratio_le_sixtyFourSevenths · IndisputableMonolith/Masses/MassGenesis/T10Q3UniformSiteMassWall.lean:235 
/-- 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 electron_muon_not_both_q3_boolean_carriers · IndisputableMonolith/Masses/MassGenesis/T10Q3UniformSiteMassWall.lean
electron_muon_not_both_q3_boolean_carriers · IndisputableMonolith/Masses/MassGenesis/T10Q3UniformSiteMassWall.lean:262 
/-- No two Q3 Boolean carriers can stand in the measured muon-to-electron load
ratio. -/
theorem electron_muon_not_both_q3_boolean_carriers
    {ψ χ : LightPattern (Fin 8)}
    (Eψ : Q3ClosedPatternEvidence ψ) (Eχ : Q3ClosedPatternEvidence χ)
    (hbψ : BooleanDifferenceSettlementWindow (ψ.window 0))
    (hbχ : BooleanDifferenceSettlementWindow (χ.window 0))
    (hposψ : 0 < siteMeaningLoad ψ 0) (hposχ : 0 < siteMeaningLoad χ 0)
    (hratio :
      integratedMeaningLoad ψ =
        muonElectronMassRatio * integratedMeaningLoad χ) :
    False := by
  have hbound :=
    q3_boolean_mass_ratio_le_sixtyFourSevenths Eψ Eχ hbψ hbχ hposψ hposχ
  have hχ7 : 7 ≤ integratedMeaningLoad χ :=
    (q3_boolean_integratedLoad_mem_Icc Eχ hbχ hposχ).1
  have hχpos : 0 < integratedMeaningLoad χ :=
    lt_of_lt_of_le (by norm_num : (0 : ℝ) < 7) hχ7
  have hle : muonElectronMassRatio * integratedMeaningLoad χ ≤
      (64 / 7) * integratedMeaningLoad χ := by
    rwa [hratio] at hbound
  have hle' : muonElectronMassRatio ≤ 64 / 7 :=
    le_of_mul_le_mul_right hle hχpos
  exact (not_le_of_gt muonElectronMassRatio_gt_bound) hle'
THEOREM gapOneWorldline_integratedLoad_eq_sixteen · IndisputableMonolith/Masses/MassGenesis/T10Q3UniformSiteMassWall.lean
gapOneWorldline_integratedLoad_eq_sixteen · IndisputableMonolith/Masses/MassGenesis/T10Q3UniformSiteMassWall.lean:359 
/-- 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 theorem does not claim that the electron and muon are not both particles in the framework. This theorem does not claim that the framework's mass model is wrong or incomplete. This theorem does not claim that the measured mass ratio is exactly 64/7 or any other simple fraction.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND