Encyclopedia Masses Masses Mass Genesis T10 Galois Conjugate Selector Scratch Pinning Load Selector

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Galois Conjugate Selector Scratch Pinning Load Selector

A machine-checked theorem in the Recognition Science framework proves that no rule based on a particle's realized mass-like load can pick out both the electron and the muon from the same family.

Verify this page

A wall against mass selectors

The electron and the muon are two of the three charged leptons, the family that also includes the tau. In the Recognition Science framework, particle masses sit on a ladder built from powers of the golden ratio, and each particle occupies a rung on that ladder. The framework's library, a machine-checked collection of formal theorems, models the electron, muon, and tau as sharing one orbit: the same sector power and charge index, but three different rungs, at transport counts 50, 61, and 67.

The declaration pinning_load_selector_not_electron_and_muon proves a class wall. It says that no condition on a particle's realized load, the mass-like quantity that a selector rule would inspect, can both pin down the rung uniquely and accept two different rungs from the same orbit. The theorem is general: it applies to any selector that pins the exponent, not just to a Galois-conjugate window or a norm. The proof works because the representation of a load as a plus b times the golden ratio is unique, so any condition on the load factors through its value and becomes a member of that class.

The wall matters because the three natural Galois-conjugate selectors each fail in a different way. The symmetric norm carries only the parity of the rung, so it cannot separate the muon at 61 from the tau at 67, both odd. The antisymmetric ratio is unchanged when the load is doubled, so it accepts a doubled-scale witness. The conjugate magnitude alone, the half-open Pisot window, does pin the rung on an orbit, but it pins only one rung where the physics needs three. The class wall states that no selector in the whole class can do better.

What the declaration does not claim is just as important. It does not prove that the framework's mass ladder is correct, nor that the electron and muon masses match measurements. It does not rule out a selector that uses information beyond the realized load, such as the sector or the charge index. It does not say that the conjugate window is the right selector; it says the window pins a rung but cannot pin two at once. The theorem is a negative result about a class of selectors, not a positive identification of any particle.

The consequence is a sharper map of the search space. Anyone trying to derive the three lepton masses from a single rule now knows the rule cannot be a function of the realized load alone. The next step is to look for structure that breaks the symmetry between rungs, perhaps in the sector or charge data, or in a condition that is not a function of the load at all.

THEOREM pinning_load_selector_not_electron_and_muon · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean
pinning_load_selector_not_electron_and_muon · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean:376 
/-- **THE CLASS WALL.** No condition on the realized anchor load that pins the
transport count on the lepton orbit can accept both the electron's required load and
the muon's. They share sector and charge index, so they share the orbit, and their
counts differ by eleven.

`LoadNormalizedToTopology` has to hold of every realized pattern, so a selector that
forces it must accept every charged row. Hence no exponent-pinning load condition
forces the residual. Galois or otherwise. -/
theorem pinning_load_selector_not_electron_and_muon
    (C : ℝ → Prop)
    (hpin : PinsExponentOnOrbit C (Anchor.B_pow Anchor.Sector.Lepton) 1332) :
    ¬ (C (MassLaw.predict_mass (rowSector ChargedMassRow.electron)
            (rowRung ChargedMassRow.electron) (rowZ ChargedMassRow.electron) / 8)
      ∧ C (MassLaw.predict_mass (rowSector ChargedMassRow.muon)
            (rowRung ChargedMassRow.muon) (rowZ ChargedMassRow.muon) / 8)) := by
  rintro ⟨he, hmu⟩
  rw [electron_required_load_eq] at he
  rw [muon_required_load_eq] at hmu
  have := hpin 50 61 he hmu
  omega
THEOREM galoisNorm_muon_eq_tau · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean
galoisNorm_muon_eq_tau · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean:190 
/-- **The norm cannot separate the muon from the tau.** Rungs `13` and `19` in the
lepton sector give transport counts `61` and `67`, both odd, so their dressed Galois
norms are equal. Any selector built from the norm alone accepts both or neither. -/
theorem galoisNorm_muon_eq_tau :
    dressedLoad (-22) 67 1332 * dressedLoadConj (-22) 67 1332
      = dressedLoad (-22) 61 1332 * dressedLoadConj (-22) 61 1332 :=
  galoisNorm_eq_of_even_diff (-22) 1332 61 67 3 (by norm_num)
THEOREM ratioSelector_accepts_doubled · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean
ratioSelector_accepts_doubled · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean:226 
/-- **Every condition on the Galois-pair ratio accepts the doubled-scale witness.**
So no ratio condition can be a scale selector, for the same reason `J` of a ratio
cannot: the object is degree zero. -/
theorem ratioSelector_accepts_doubled (P : ℝ → Prop) (B n Z : ℤ)
    (h : P (dressedLoad B n Z / dressedLoadConj B n Z)) :
    P (dressedLoad (B + 2) n Z / dressedLoadConj (B + 2) n Z) := by
  rwa [galoisRatio_doubled_eq]
THEOREM conjWindow_pins_exponent · conjWindow_not_electron_and_muon · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean
conjWindow_pins_exponent · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean:286 
/-- **The conjugate window pins the transport count.** On one orbit at most one count
puts the conjugate load in the half-open window, because the window has width exactly
one ladder step. So the Galois condition really does select, which is what every
previous selector failed to do. -/
theorem conjWindow_pins_exponent (B Z n n' : ℤ)
    (h : InConjWindow (dressedLoadConj B n Z))
    (h' : InConjWindow (dressedLoadConj B n' Z)) :
    n = n' := by
  have key : ∀ m : ℤ, InConjWindow (dressedLoadConj B m Z) →
      phi ^ (m - 1) ≤ conjOrbitConst B Z ∧ conjOrbitConst B Z < phi ^ m := by
    intro m hm
    have hinv := abs_dressedLoadConj_mul_zpow B m Z
    have hpm : (0 : ℝ) < phi ^ m := zpow_pos Constants.PhiLadder.phi_pos m
    have hstep : phi ^ (m - 1) = phi⁻¹ * phi ^ m := by
      rw [show (m - 1 : ℤ) = -1 + m by ring,
        zpow_add₀ Constants.PhiLadder.phi_ne_zero]
      norm_num
    refine ⟨?_, ?_⟩
    · have h1 : phi⁻¹ * phi ^ m ≤ |dressedLoadConj B m Z| * phi ^ m :=
        mul_le_mul_of_nonneg_right hm.1 hpm.le
      rw [hinv] at h1
      rw [hstep]
      exact h1
    · have h2 : |dressedLoadConj B m Z| * phi ^ m < 1 * phi ^ m :=
        mul_lt_mul_of_pos_right hm.2 hpm
      rw [hinv, one_mul] at h2
      exact h2
  obtain ⟨hlo, hhi⟩ := key n h
  obtain ⟨hlo', hhi'⟩ := key n' h'
  by_contra hne
  rcases lt_or_gt_of_ne hne with hlt | hgt
  · have hmono : phi ^ n ≤ phi ^ (n' - 1) :=
      zpow_le_zpow_right₀ (le_of_lt Constants.PhiLadder.one_lt_phi) (by omega)
    linarith
  · have hmono : phi ^ n' ≤ phi ^ (n - 1) :=
      zpow_le_zpow_right₀ (le_of_lt Constants.PhiLadder.one_lt_phi) (by omega)
    linarith
conjWindow_not_electron_and_muon · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean:412 
/-- **The conjugate window, killed by the class wall.** Stated directly on the
conjugate so it does not need `sigma` as a function on the reals: the window cannot
hold at both of the two counts the electron and the muon require. -/
theorem conjWindow_not_electron_and_muon :
    ¬ (InConjWindow (dressedLoadConj (Anchor.B_pow Anchor.Sector.Lepton) 50 1332)
      ∧ InConjWindow (dressedLoadConj (Anchor.B_pow Anchor.Sector.Lepton) 61 1332)) := by
  rintro ⟨h50, h61⟩
  have := conjWindow_pins_exponent (Anchor.B_pow Anchor.Sector.Lepton) 1332 50 61 h50 h61
  omega

What this page does not claim

The theorem does not prove that the framework's mass ladder matches measured particle masses. The theorem does not identify which selector, if any, correctly derives the lepton masses. The theorem does not rule out selectors that use information beyond the realized load, such as sector or charge index.

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