Encyclopedia Masses Masses Mass Genesis T10 Boolean Anchor Ratio Wall

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Boolean Anchor Ratio Wall

A machine-checked proof shows why the electron and muon cannot both be anchored by the simplest posting alphabet, no matter what mass unit you choose.

Verify this page

The Boolean anchor ratio wall

In the Recognition Science framework, particle masses are not free parameters. They are predicted by a ledger, a discrete record of recognition events, through a mass law that assigns each species a predicted mass. The framework's library, a machine-checked collection of formal theorems, tests which posting alphabets, the sets of allowed ledger entries, can actually carry these predicted masses. The module T10BooleanAnchorRatioWall examines the simplest alphabet of all: one where each tick posts either +1, -1, or nothing.

This Boolean alphabet has a striking structural property. Because every posting is an integer, the neutralized load of a settlement window, a quantity derived from the raw energy and tick sum, is always a multiple of one eighth. The load is therefore either exactly zero or at least 1/8. A load that is positive cannot be arbitrarily small. This positive floor, combined with a known ceiling of 8, means the load has a bounded ratio. Unlike a dense set, which misses nothing because it fills the number line, a bounded set has real exclusion power. This boundedness survives any rescaling of the mass unit, because a unit cancels in a ratio.

The consequence is a theorem: under the framework's normalization condition, a Boolean anchor pins a predicted mass into the interval [1, 64] in any unit. Two species that are both Boolean-anchored must have predicted masses within a factor of 64 of each other, for every choice of unit. This is the ratio bound, and it is the unit-free statement that gives the wall its strength.

The wall is then instantiated on the species table. The electron and the muon sit in the same lepton sector at the same charge index, eleven rungs apart on the framework's phi-power ladder. Their predicted-mass ratio is therefore exactly phi^11, which is 89*phi + 55, a number greater than 144. The required ratio of more than 144 exceeds the achievable ceiling of 64 by a factor better than two. No choice of mass unit can close this gap. The framework's library proves that the electron and the muon cannot both be Boolean-anchored under the normalization condition.

This is the difference between this wall and earlier exclusion results. It does not say a dense set misses a point. It does not compare a number against a threshold in an imported unit. It says a required ratio exceeds an achievable ratio by a computable factor, and that factor is unit-independent. The module converts a threshold with no strength into a ratio statement with some. It excludes the Boolean alphabet as the carrier of the anchor load for the species table. It does not show what the anchor is, and it does not touch the dense composite-posting family, which remains a separate question.

THEOREM booleanWindow_load_pos_ge_eighth · IndisputableMonolith/Masses/MassGenesis/T10BooleanAnchorRatioWall.lean
booleanWindow_load_pos_ge_eighth · IndisputableMonolith/Masses/MassGenesis/T10BooleanAnchorRatioWall.lean:103 
/-- **A Boolean load is zero or at least an eighth.** The floor is what
distinguishes this alphabet from the dense composite-posting family: an integer
numerator over eight cannot be positive and arbitrarily small. -/
theorem booleanWindow_load_pos_ge_eighth {w : PhotonWindow}
    (hw : BooleanDifferenceSettlementWindow w)
    (hpos : 0 < normSq8 (neutralize w)) :
    1 / 8 ≤ normSq8 (neutralize w) := by
  obtain ⟨N, S, hform⟩ := booleanWindow_load_int_form hw
  rw [hform] at hpos ⊢
  -- `8 N - S ^ 2` is a positive integer, hence at least one.
  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 hone : (1 : ℤ) ≤ 8 * N - S ^ 2 := hint
  have : (1 : ℝ) ≤ ((8 * N - S ^ 2 : ℤ) : ℝ) := by exact_mod_cast hone
  push_cast at this
  linarith
THEOREM booleanAnchor_predictedMass_mem_Icc · IndisputableMonolith/Masses/MassGenesis/T10BooleanAnchorRatioWall.lean
booleanAnchor_predictedMass_mem_Icc · IndisputableMonolith/Masses/MassGenesis/T10BooleanAnchorRatioWall.lean:126 
/-- **Both ends at once.** Under the normalization condition a Boolean anchor
with nonzero load carries a predicted mass between `1` and `64`. -/
theorem booleanAnchor_predictedMass_mem_Icc
    {ψ : LightPattern (Fin 8)}
    (hbool : BooleanDifferenceSettlementWindow (ψ.window 0))
    (hload : LoadNormalizedToTopology ψ)
    (hpos : 0 < predictedMass ψ) :
    1 ≤ predictedMass ψ ∧ predictedMass ψ ≤ 64 := by
  have hsite : normSq8 (neutralize (ψ.window 0)) = predictedMass ψ / 8 :=
    loadNormalizedToTopology_site0_load_eq_predictedMass_div_eight hload
  have hsitepos : 0 < normSq8 (neutralize (ψ.window 0)) := by
    rw [hsite]; linarith
  have hlow := booleanWindow_load_pos_ge_eighth hbool hsitepos
  have hhigh := booleanWindow_neutralizedNormSq_le hbool
  rw [hsite] at hlow hhigh
  constructor <;> linarith
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 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

This module does not identify what the correct anchor is, only that it is not Boolean. This module does not exclude composite postings at rational multiplicity, which are unbounded and dense. This module does not derive the fine-structure constant or any other coupling constant.

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