Masses Mass Genesis T10 Q3 Uniform Site Mass Wall Boolean Window Load Pos Ge Sev

The Boolean floor

The declaration booleanWindow_load_pos_ge_sevenEighths is a proved theorem in a machine-checked library of formal theorems. It states a precise inequality about a quantity called the load of a window. In plain terms, it says: if a window's entries are each restricted to one of three values (0, 1, or -1), and if the window's load is positive, then that load is at least 7/8. The theorem is a formal statement about a mathematical object, not a claim about any specific physical particle.

The setting is a discrete model of recognition events. A window is a short sequence of such events, and its load is a number computed from those events. The theorem's content is purely combinatorial: it shows that among all windows with entries in {0, 1, -1} and positive load, the smallest possible load is exactly 7/8. This is a sharp bound, meaning there exists a window achieving it; the theorem does not merely say the load is greater than zero, it pins down the exact floor.

In Recognition Science, this theorem is one step in a larger argument about particle masses. The framework models certain stable patterns as carriers of mass, with the mass proportional to a total load. The theorem helps establish that if a pattern's window is Boolean (entries in {0, 1, -1}) and its site load is positive, then the total load lies between 7 and 64. That range, in turn, implies a maximum ratio between the masses of two such carriers: 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 framework's library proves that no two Boolean-window carriers can have a mass ratio reaching that measured value. This is a refutation of a specific hypothesis: that both the muon and the electron are such carriers. The refutation is precise and quantitative, with the discrepancy being about 197.63 against a measurement uncertainty of 4.6 × 10⁻⁶.

What the theorem does not claim is equally important. It does not prove any mass formula, nor does it assign a specific mass to any particle. It does not say that the muon or electron is not a carrier; it only rules out the conjunction that both are carriers with Boolean windows. The identity that mass equals integrated load for stable patterns is untouched by this result. The theorem is a negative result about a class of models, not a positive statement about which model is correct.

/-- **Sharp Boolean floor.** A positive Boolean load is at least `7/8`, not
merely `1/8`. The numerator `8N - S^2` is a positive integer that cannot be
`1..6` under the Boolean bounds `0 ≤ N ≤ 8` and `|S| ≤ N`. -/
theorem booleanWindow_load_pos_ge_sevenEighths {w : PhotonWindow}
    (hw : BooleanDifferenceSettlementWindow w)
    (hpos : 0 < normSq8 (neutralize w)) :
    7 / 8 ≤ normSq8 (neutralize w) := by
  obtain ⟨N, S, hform, hN0, hN8, hSAbs⟩ := booleanWindow_load_int_form_bounded hw
  rw [hform] at hpos ⊢
  have hAbsS : |S| ≤ N := by
    have : |S| ≤ |N| := by
      have h' : (S.natAbs : ℤ) ≤ (N.natAbs : ℤ) := Nat.cast_le.mpr hSAbs
      rwa [Int.natCast_natAbs, Int.natCast_natAbs] at h'
    rwa [abs_of_nonneg hN0] at this
  have hint : (0 : ℤ) < 8 * N - S ^ 2 := by
    by_contra hle
    push_neg at hle
    have : ((8 * N - S ^ 2 : ℤ) : ℝ) ≤ 0 := by exact_mod_cast hle
    push_cast at this
    linarith
  have hge7 := eightN_sub_Ssq_ge_seven N S hN0 hN8 hAbsS hint
  have heq : (N : ℝ) - (S : ℝ) ^ 2 / 8 = ((8 * N - S ^ 2 : ℤ) : ℝ) / 8 := by
    push_cast
    ring
  rw [heq]
  have hcast : (7 : ℝ) ≤ ((8 * N - S ^ 2 : ℤ) : ℝ) := by exact_mod_cast hge7
  exact div_le_div_of_nonneg_right hcast (by norm_num : (0 : ℝ) ≤ 8)

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

/-- 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'

What this page does not claim

The theorem does not prove any specific mass value for any particle. The theorem does not rule out the muon or electron being a carrier under a different window structure. The theorem does not establish that the identity mass equals integrated load is false.

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: