Encyclopedia Masses Masses Mass Genesis T10 Boolean Anchor Ratio Wall Electron Muon Not Both Boolean

ARTICLE 3 claims 3 theorems

Masses Mass Genesis T10 Boolean Anchor Ratio Wall Electron Muon Not Both Boolean

A machine-checked argument shows the electron and muon cannot both be anchored by the simplest possible posting alphabet, because their mass ratio is too large.

Verify this page

The ratio wall

The electron and the muon are two particles in the same family, with the muon about 206.77 times heavier. In the Recognition Science account of mass, particles are patterns of discrete events, and their predicted masses sit on a ladder where each rung multiplies the previous one by the golden ratio phi. The electron and muon are eleven rungs apart, so the framework's mass law predicts their masses differ by a factor of exactly phi to the eleventh power, which is more than 144.

The question is what kind of posting alphabet, the set of symbols a pattern may use, can carry such a ratio. The simplest alphabet is Boolean: each tick in a settlement window is either occupied, empty, or negatively occupied, so its load is an integer multiple of an eighth. A theorem in the framework's machine-checked library of formal theorems proves that any pattern using this alphabet, once normalized, has a predicted mass between 1 and 64. That bound is unit-free: rescaling the mass unit by any positive factor cancels in the ratio, so no choice of units can stretch the ceiling.

The contradiction is now arithmetic. The electron and muon, if both used the Boolean alphabet, would have predicted masses within a factor of 64 of each other. But the mass law requires their ratio to be phi to the eleventh, which exceeds 144. The requirement outruns the alphabet's capacity by a factor better than two, and no unit rescaling closes the gap. The declaration electron_muon_not_both_boolean_anchored is the formal statement of that impossibility: it proves, with no unproved assumptions, that the electron and muon cannot both be Boolean-anchored under the normalization condition.

The theorem is narrow on purpose. It does not say what the correct anchor is, only that this particular simple alphabet cannot serve both particles. It does not rule out composite postings at rational multiplicity, which form a dense set and were analyzed separately. It converts a threshold statement in an imported unit, which had no strength, into a ratio statement that survives every rescaling. That is the wall's margin, and it is what makes the result a genuine exclusion rather than a numerical coincidence.

THEOREM boolean_anchored_mass_ratio_le_sixtyfour · IndisputableMonolith/Masses/MassGenesis/T10BooleanAnchorRatioWall.lean
boolean_anchored_mass_ratio_le_sixtyfour · IndisputableMonolith/Masses/MassGenesis/T10BooleanAnchorRatioWall.lean:143 
/-- **The ratio bound, which is the unit-free statement.** Two Boolean-anchored
patterns satisfying the normalization condition have predicted masses within a
factor of `64`, and rescaling the mass unit by any positive `k` cannot change
that, because `k` cancels. -/
theorem boolean_anchored_mass_ratio_le_sixtyfour
    {ψ χ : LightPattern (Fin 8)} {k : ℝ} (hk : 0 < k)
    (hbψ : BooleanDifferenceSettlementWindow (ψ.window 0))
    (hbχ : BooleanDifferenceSettlementWindow (χ.window 0))
    (hlψ : LoadNormalizedToTopology ψ) (hlχ : LoadNormalizedToTopology χ)
    (hpψ : 0 < predictedMass ψ) (hpχ : 0 < predictedMass χ) :
    k * predictedMass χ ≤ 64 * (k * predictedMass ψ) := by
  obtain ⟨hψ1, _⟩ := booleanAnchor_predictedMass_mem_Icc hbψ hlψ hpψ
  obtain ⟨_, hχ64⟩ := booleanAnchor_predictedMass_mem_Icc hbχ hlχ hpχ
  nlinarith
THEOREM phi_zpow_eleven_gt_oneFortyFour · IndisputableMonolith/Masses/MassGenesis/T10BooleanAnchorRatioWall.lean
phi_zpow_eleven_gt_oneFortyFour · IndisputableMonolith/Masses/MassGenesis/T10BooleanAnchorRatioWall.lean:160 
/-- `phi ^ 11 = 89 phi + 55`, hence above `144`. Only `1 < phi` is needed. -/
theorem phi_zpow_eleven_gt_oneFortyFour : (144 : ℝ) < Constants.phi ^ (11 : ℤ) := by
  have hfib := Constants.PhiLadder.phi_zpow_eq_fib (11 : ℤ)
  have h11 : Int.fib 11 = 89 := by decide
  have h10 : Int.fib (11 - 1) = 55 := by decide
  rw [h11, h10] at hfib
  have hphi : (1 : ℝ) < Constants.phi := Constants.one_lt_phi
  rw [hfib]
  push_cast
  linarith
THEOREM electron_muon_not_both_boolean_anchored · IndisputableMonolith/Masses/MassGenesis/T10BooleanAnchorRatioWall.lean
electron_muon_not_both_boolean_anchored · IndisputableMonolith/Masses/MassGenesis/T10BooleanAnchorRatioWall.lean:171 
/-- **The instantiated wall, with its margin.** The electron and the muon differ
by eleven rungs in one sector at one charge index, so the muon's predicted mass is
`phi ^ 11` times the electron's, which is more than `144` times. A Boolean anchor
allows at most `64`. The requirement exceeds what the alphabet can carry by a
factor better than two, and no choice of mass unit closes the gap. -/
theorem electron_muon_not_both_boolean_anchored
    {ψ χ : LightPattern (Fin 8)} {k : ℝ} (hk : 0 < k)
    (hlψ : LoadNormalizedToTopology ψ) (hlχ : LoadNormalizedToTopology χ)
    (hmψ : predictedMass ψ = MassLaw.predict_mass Anchor.Sector.Lepton 2 1332)
    (hmχ : predictedMass χ = MassLaw.predict_mass Anchor.Sector.Lepton 13 1332) :
    ¬ (BooleanDifferenceSettlementWindow (ψ.window 0)
        ∧ BooleanDifferenceSettlementWindow (χ.window 0)) := by
  rintro ⟨hbψ, hbχ⟩
  have hpψ : 0 < predictedMass ψ := by
    rw [hmψ]; exact MassLaw.predict_mass_pos _ _ _
  have hpχ : 0 < predictedMass χ := by
    rw [hmχ]; exact MassLaw.predict_mass_pos _ _ _
  have hratio := boolean_anchored_mass_ratio_le_sixtyfour hk hbψ hbχ hlψ hlχ hpψ hpχ
  -- The muon's mass is `phi ^ 11` times the electron's.
  have hrung : MassLaw.predict_mass Anchor.Sector.Lepton 13 1332
      = Constants.phi ^ (13 - 2 : ℤ) * MassLaw.predict_mass Anchor.Sector.Lepton 2 1332 :=
    predict_mass_rung_ratio Anchor.Sector.Lepton 2 13 1332
  have hexp : ((13 : ℤ) - 2) = (11 : ℤ) := by norm_num
  rw [hexp] at hrung
  have hphi := phi_zpow_eleven_gt_oneFortyFour
  rw [hmψ, hmχ, hrung] at hratio
  set m : ℝ := MassLaw.predict_mass Anchor.Sector.Lepton 2 1332 with hm
  have hmpos : 0 < m := MassLaw.predict_mass_pos _ _ _
  have hkm : 0 < k * m := mul_pos hk hmpos
  have hcancel : (k * m) * Constants.phi ^ (11 : ℤ) ≤ (k * m) * 64 :=
    calc (k * m) * Constants.phi ^ (11 : ℤ)
        = k * (Constants.phi ^ (11 : ℤ) * m) := by ring
      _ ≤ 64 * (k * m) := hratio
      _ = (k * m) * 64 := by ring
  have hle : Constants.phi ^ (11 : ℤ) ≤ 64 := le_of_mul_le_mul_left hcancel hkm
  linarith

What this page does not claim

The theorem does not identify the correct posting alphabet for the electron or the muon. The theorem does not rule out composite postings at rational multiplicity, which form a dense set. The theorem does not derive the measured electron-muon mass ratio from first principles; it only excludes one alphabet from carrying it.

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