Encyclopedia Masses Masses Mass Genesis T10 Boolean Anchor Ratio Wall Boolean Anchored Mass Ratio Le

ARTICLE 3 claims 3 theorems

Masses Mass Genesis T10 Boolean Anchor Ratio Wall Boolean Anchored Mass Ratio Le

A machine-checked proof shows that any two particle masses anchored by a simple Boolean rule must lie within a factor of 64 of each other, and the electron and muon violate that bound.

Verify this page

The ratio wall

In the Recognition Science account, the predicted mass of a particle is not a free parameter. It is computed from a recognition pattern, a discrete record of events over eight ticks, through a mass law that the framework derives. One candidate way to anchor that pattern to a physical species is the Boolean posting alphabet, in which each tick is assigned one of only three amplitudes: 1, 0, or -1. The declaration boolean_anchored_mass_ratio_le_sixtyfour is a proved theorem about that alphabet.

The theorem says: if two particle species both have Boolean-anchored patterns that satisfy the framework's normalization condition, then their predicted masses, measured in any unit, must be within a factor of 64 of each other. The number 64 is not arbitrary. A Boolean window's load, its neutralized energy, is always a multiple of an eighth. So a nonzero load is at least 1/8 and at most 8, and that bounded range, after normalization, pins the mass into the interval [1, 64]. Because the bound is a ratio, rescaling the mass unit by any positive constant cancels out: the factor of 64 holds in every unit system.

The proof is not vacuous. The framework's species table places the electron and the muon in the same lepton sector at the same charge index, eleven rungs apart on a phi-power ladder. Their predicted-mass ratio is exactly phi^11, which is 89*phi + 55, greater than 144. That required ratio exceeds the Boolean ceiling of 64 by a factor better than two. The theorem therefore excludes the Boolean alphabet as the carrier of the anchor load for the species table: the electron and the muon cannot both be Boolean-anchored under the normalization condition.

What the theorem does not claim is as important as what it proves. It does not show what the true anchor is; it only rules out one candidate. It does not exclude composite postings at rational multiplicity, which are unbounded and dense and were measured in a sibling module. It does not compare a number against a threshold in an imported unit. It converts a threshold statement that had no strength into a ratio statement that has some, and the margin is computable: 144/64, better than 2, against a comparison that tests ratios and not exact equality.

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

What this page does not claim

The theorem does not identify the true anchor for any particle species. The theorem does not exclude composite postings at rational multiplicity, which are dense and unbounded. The theorem does not compare a predicted mass against a measured value in any imported unit.

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