Encyclopedia Masses Masses Mass Genesis T10 Q3 Uniform Site Mass Wall Q3 Boolean Mass Ratio Le Sixty

ARTICLE 5 claims 4 theorems 1 measured

Masses Mass Genesis T10 Q3 Uniform Site Mass Wall Q3 Boolean Mass Ratio Le Sixty

A machine-checked theorem puts a hard ceiling on how different two particle masses can be, if each is built from eight identical sites with a simple on-off anchor.

Verify this page

The Boolean mass ratio bound

The declaration q3_boolean_mass_ratio_le_sixtyFourSevenths is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It concerns matter carriers built from eight sites, the vertices of a recognition 3-cube visited in a Gray cycle. The framework models each such carrier as a ledger, a discrete record of events, whose total load is exactly eight times the load of one site. The theorem adds the hypothesis that each site's anchor window is Boolean, meaning every tick in it takes one of only three values: 0, 1, or -1.

Under that hypothesis, the theorem proves that the common site load lies between 7/8 and 8, so the total load of any such carrier lies between 7 and 64. Consequently, for any two such carriers, the ratio of their total loads is at most 64/7, which is about 9.14. The proof is a direct consequence of the uniformity of site loads and the finite alphabet imposed by the Boolean condition. The theorem is not about any specific particle; it is a structural bound on the entire class of carriers satisfying the hypotheses.

The bound matters because it collides with a measured fact. The muon-to-electron mass ratio is measured to be 206.7682830, with a PDG uncertainty of 4.6 × 10⁻⁶. Since 64/7 is about 9.14, no Boolean eight-site carrier can be a muon if another is an electron: the ratio is nearly twenty-two times too large. A separate theorem in the same module, no_q3_boolean_partner_at_muon_ratio, states this refutation formally. The class of Boolean carriers is not empty: the library's gap-one worldline is a Q3 closed pattern with Boolean anchor and site load exactly 2, hence total load 16, so the bound fires on a real object.

The theorem does not claim any mass-law formula, rung table, or yardstick. It does not say that real particles are Q3 Boolean carriers; it says that if they were, their mass ratio could not reach the measured muon-to-electron value. The identity restMass = integratedMeaningLoad for stable closed patterns is untouched by this result. The comparison is ratio against ratio, so no unit enters and no mass-law formula sits on either side.

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)
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 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

No mass-law formula, rung table, or yardstick appears in the theorem or its proof. The theorem does not assert that real particles are Q3 Boolean carriers; it refutes that conjunction against the measured muon-to-electron ratio. The identity restMass = integratedMeaningLoad for stable closed patterns is not touched by this result.

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