Encyclopedia Masses Masses Mass Genesis T10 Q3 Uniform Site Mass Wall Gap One Worldline Integrated L

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Q3 Uniform Site Mass Wall Gap One Worldline Integrated L

A single pattern in the framework's library carries a total load of exactly 16, a concrete number that later rules out a whole class of particle models.

Verify this page

A worldline's load

The declaration gapOneWorldline_integratedLoad_eq_sixteen is a theorem in the framework's machine-checked library of formal theorems. It states that a specific pattern, called the gap-one worldline, has a total integrated load of exactly 16. Load here is a discrete count of recognition events, not a physical mass; the theorem is about a combinatorial object, not about any measured particle.

The number 16 arises from two simpler facts. First, the pattern is a Q3 closed pattern, meaning it lives on the eight vertices of a three-dimensional cube and respects the framework's recognition cycle. Second, each of the eight sites carries the same load, and for this particular pattern that common site load is 2. Eight sites times a load of 2 gives 16. The theorem is a direct consequence of these two facts, proved by rewriting one into the other.

This specific value matters because it sits inside a larger argument about particle masses. The framework proves that any Q3 closed pattern with a Boolean anchor window, meaning each tick is one of three values, has a total load between 7 and 64. The gap-one worldline, with its load of 16, is an example showing this range is not empty: the class of such patterns really contains objects.

The same bound leads to a refutation. The measured muon-to-electron mass ratio is about 206.77, but the framework proves that any two Boolean Q3 carriers have load ratios at most 64/7, about 9.14. Since 9.14 cannot reach 206.77, the conjunction of "realized particles are Q3 carriers" and "the anchor window is Boolean" is false. The gap-one worldline's load of 16 is the concrete witness that the bound is real, not vacuous.

What the declaration does not claim is equally precise. It does not say that any physical particle has load 16, nor that the gap-one worldline represents a muon or an electron. It does not introduce a mass formula, a rung table, or a unit system. The identity restMass equals integrated load for stable closed patterns is a separate statement, untouched by this theorem. The declaration is a fact about a combinatorial pattern, and its role is to make the later refutation non-vacuous.

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
THEOREM gapOneWorldline_q3Evidence · gapOneWorldline_anchor_load_eq_two · IndisputableMonolith/Masses/MassGenesis/T10Q3UniformSiteMassWall.lean
gapOneWorldline_q3Evidence · IndisputableMonolith/Masses/MassGenesis/T10Q3UniformSiteMassWall.lean:289 
/-- The library's gap-one Rhat worldline is Q3 closed evidence. Assembled from
`worldlinePattern_windowEquivariant` and the three stability fields, without
importing `MasterCertificate`. -/
theorem gapOneWorldline_q3Evidence :
    Q3ClosedPatternEvidence (worldlinePattern gapOneTwoPhaseMode) where
  stable := by
    refine ⟨?_, ?_, ?_⟩
    · exact Finset.univ_nonempty
    · refine ⟨0, Finset.mem_univ _, ?_⟩
      have hw0 :
          (worldlinePattern gapOneTwoPhaseMode).window 0 =
            gapOneTwoPhaseMode := by
        show (RecognitionDynamics.cyclicShift^[(0 : Fin 8).val])
            gapOneTwoPhaseMode = gapOneTwoPhaseMode
        simp
      rw [hw0]
      have hneut : neutralize gapOneTwoPhaseMode = gapOneTwoPhaseMode := by
        funext j
        show gapOneTwoPhaseMode j - (∑ i, gapOneTwoPhaseMode i) / 8 =
          gapOneTwoPhaseMode j
        rw [gapOneTwoPhaseMode_neutral]
        ring
      rw [hneut]
      have hns : normSq8 gapOneTwoPhaseMode = 2 := by
        simp [normSq8, gapOneTwoPhaseMode, Fin.sum_univ_eight,
          Complex.normSq_apply]
        norm_num
      rw [hns]
      norm_num
    · exact ⟨8, by norm_num, dvd_refl 8,
        fun x _ => RecognitionDynamics.cyclicShift_period_8 _⟩
  full_support := rfl
  window_equivariant := worldlinePattern_windowEquivariant gapOneTwoPhaseMode
gapOneWorldline_anchor_load_eq_two · IndisputableMonolith/Masses/MassGenesis/T10Q3UniformSiteMassWall.lean:337 
/-- Anchor site load of the gap-one worldline is exactly `2`: the seed
`(1, -1, 0, …, 0)` is already neutral, so neutralization is the identity and
the squared norm is `1 + 1`. -/
theorem gapOneWorldline_anchor_load_eq_two :
    siteMeaningLoad (worldlinePattern gapOneTwoPhaseMode) 0 = 2 := by
  have hw0 :
      (worldlinePattern gapOneTwoPhaseMode).window 0 = gapOneTwoPhaseMode := by
    show (RecognitionDynamics.cyclicShift^[(0 : Fin 8).val])
        gapOneTwoPhaseMode = gapOneTwoPhaseMode
    simp
  unfold siteMeaningLoad
  rw [hw0]
  have hneut : neutralize gapOneTwoPhaseMode = gapOneTwoPhaseMode := by
    funext j
    show gapOneTwoPhaseMode j - (∑ i, gapOneTwoPhaseMode i) / 8 =
      gapOneTwoPhaseMode j
    rw [gapOneTwoPhaseMode_neutral]
    ring
  rw [hneut]
  simp [normSq8, gapOneTwoPhaseMode, Fin.sum_univ_eight, Complex.normSq_apply]
  norm_num
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 · muonElectronMassRatio_gt_bound · 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)
muonElectronMassRatio_gt_bound · IndisputableMonolith/Masses/MassGenesis/T10Q3UniformSiteMassWall.lean:258 
theorem muonElectronMassRatio_gt_bound :
    (64 / 7 : ℝ) < muonElectronMassRatio := by
  norm_num [muonElectronMassRatio]

What this page does not claim

The declaration does not assign a physical mass to any particle. The declaration does not introduce a mass-law formula or a unit system. The declaration does not imply that the gap-one worldline represents a muon or an electron.

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