Encyclopedia Masses Masses Mass Genesis T10 Galois Conjugate Selector Scratch Conj Window Not Electr

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Galois Conjugate Selector Scratch Conj Window Not Electr

A machine-checked proof shows why one promising selector for particle masses fails on the electron and muon, and what that failure rules out.

Verify this page

A window that cannot hold two leptons

The golden ratio φ, about 1.618, has a mathematical sibling: its Galois conjugate, 1 − φ, which equals about −0.618. In the Recognition Science framework, particle masses are built from powers of φ, and the conjugate is a natural tool because it shrinks as the power grows, while φ itself grows. A selector based on the conjugate's size, the half-open window where the absolute value lies between φ⁻¹ and 1, can uniquely identify a single power of φ. This is the recognition ledger's way of asking which mass a given pattern corresponds to.

The declaration conjWindow_not_electron_and_muon proves that this window cannot simultaneously hold the electron and the muon. In the framework's table, the electron, muon, and tau all sit on one orbit, the same sector power and charge index, at three different transport counts: 50, 61, and 67. The window pins the transport count uniquely, so it can accept at most one of these three. The theorem states, in the framework's own terms, that the electron at count 50 and the muon at count 61 cannot both fall inside the window. It is a negative result, a wall that classifies what no such selector can do.

What the declaration does not claim is broader than what it does. It does not say the window is useless; the window rejects a doubled scale and pins the exponent on an orbit, so it works for a single particle. It does not say the framework's mass predictions fail. The framework's own table places all three leptons on one orbit, and the window's failure to separate two of them is a property of that table, not a refutation of the mass law. The theorem also does not claim that no selector can separate the electron and muon; it only rules out the class of selectors that pin the exponent on an orbit.

The wider class wall, pinning_load_selector_not_electron_and_muon, states the general principle: no condition on the realized load that pins the exponent can accept two same-sector same-charge rows at different rungs. Since every Galois condition on a load in the golden field factors through the load's value, any such condition falls into this class. The window is one member of that class, and the theorem shows it fails on the electron and muon. The framework's library records this as a scratch module, with no target and no new axioms, a formal note on what a promising construction cannot do.

THEOREM conjWindow_not_electron_and_muon · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean
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
THEOREM conjWindow_pins_exponent · 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
THEOREM conjWindow_not_electron_and_muon · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean
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
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

What this page does not claim

The window is useless for selecting a single particle mass. The framework's mass predictions for the electron or muon are incorrect. No selector of any kind can separate the electron and muon.

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