Encyclopedia Masses Masses Mass Genesis T10 Galois Conjugate Selector Scratch Dressed Load Injective

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Galois Conjugate Selector Scratch Dressed Load Injective

A single theorem about a mathematical formula shows why the electron, muon, and tau cannot be told apart by one simple measure, and what that means for a theory of particle masses.

Verify this page

The injectivity lemma

The declaration dressedLoad_injective_in_exponent is a lemma about a specific formula used in the Recognition Science framework's account of particle masses. The formula, called dressedLoad, takes three whole-number inputs: a sector power B, a transport count n, and a charge index Z. The lemma states that if two choices of the transport count n produce the same numerical value of this formula, while B and Z are held fixed, then the two choices of n must actually be the same. In plain terms, the formula is one-to-one in its exponent: no two different transport counts can collide to give the same dressed load. This is a proved theorem in the framework's machine-checked library of formal theorems, with the proof relying on the fact that the golden ratio phi and its Galois conjugate move in opposite directions as the exponent grows.

The theorem matters because the framework's own mass table places the electron, muon, and tau on a single orbit, meaning they share the same sector power B = -22 and charge index Z = 1332, but sit at three different transport counts: 50, 61, and 67. The injectivity lemma guarantees that any condition on the realized load that pins down the exponent can accept at most one of these three rows. The framework's library proves this as a class wall: no condition on the load that pins the exponent can accept two same-sector, same-charge rows at different rungs. Since the representation of a number as a + b * phi is unique, every Galois condition on a load factors through the load's value and therefore falls into this class. The surviving candidate, a half-open window on the conjugate magnitude, does pin the exponent on an orbit, but it selects one count where the physics needs three, so it cannot separate the three leptons.

The theorem does not claim that the framework has derived the lepton masses, nor that any Galois-based selector succeeds. The module is explicitly a scratch module: it states no target and imports no target, and it proves no new axiom. The injectivity lemma is a structural fact about the formula, not a physical prediction. It establishes a limitation on a class of selectors, not a positive result about which selector works. The framework's account of the lepton masses remains an open target, and this theorem is part of the evidence that the simple Galois-conjugate approach cannot close it.

THEOREM dressedLoad_injective_in_exponent · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean
dressedLoad_injective_in_exponent · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean:142 
/-- **The orbit is faithfully indexed.** On a fixed sector power and charge index the
load determines the transport count, so "pinning the load" and "pinning the count"
are the same problem. This is `ladder_injective` in dressed form. -/
theorem dressedLoad_injective_in_exponent (B Z : ℤ) (hZ : 0 ≤ Z) {n n' : ℤ}
    (h : dressedLoad B n Z = dressedLoad B n' Z) : n = n' := by
  have h2 : (0 : ℝ) < (2 : ℝ) ^ (B - 3) := zpow_pos (by norm_num) _
  have hZR : (0 : ℝ) ≤ (Z : ℝ) := by exact_mod_cast hZ
  have hd : (0 : ℝ) < phi + (Z : ℝ) := by
    have := Constants.PhiLadder.phi_pos
    linarith
  have hstep : phi ^ n = phi ^ n' := by
    have := h
    unfold dressedLoad at this
    have h' : (2 : ℝ) ^ (B - 3) * (phi + (Z : ℝ)) * phi ^ n
        = (2 : ℝ) ^ (B - 3) * (phi + (Z : ℝ)) * phi ^ n' := by
      linear_combination this
    exact mul_left_cancel₀ (by positivity) h'
  exact Constants.PhiLadder.rung_of_value_unique hstep
THEOREM electron_required_load_eq · muon_required_load_eq · tau_required_load_eq · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean
electron_required_load_eq · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean:343 
theorem electron_required_load_eq :
    MassLaw.predict_mass (rowSector ChargedMassRow.electron)
        (rowRung ChargedMassRow.electron) (rowZ ChargedMassRow.electron) / 8
      = dressedLoad (Anchor.B_pow Anchor.Sector.Lepton) 50 1332 := by
  rw [← dressedLoad_eq_required_load (rowSector ChargedMassRow.electron)
      (rowRung ChargedMassRow.electron) (rowZ ChargedMassRow.electron)
      (by norm_num [rowZ])]
  simp only [rowSector, rowRung, rowZ]
  rw [Anchor.r0_Lepton_eq]
  norm_num
muon_required_load_eq · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean:354 
theorem muon_required_load_eq :
    MassLaw.predict_mass (rowSector ChargedMassRow.muon)
        (rowRung ChargedMassRow.muon) (rowZ ChargedMassRow.muon) / 8
      = dressedLoad (Anchor.B_pow Anchor.Sector.Lepton) 61 1332 := by
  rw [← dressedLoad_eq_required_load (rowSector ChargedMassRow.muon)
      (rowRung ChargedMassRow.muon) (rowZ ChargedMassRow.muon)
      (by norm_num [rowZ])]
  simp only [rowSector, rowRung, rowZ]
  rw [Anchor.r0_Lepton_eq]
  norm_num
tau_required_load_eq · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean:365 
theorem tau_required_load_eq :
    MassLaw.predict_mass (rowSector ChargedMassRow.tau)
        (rowRung ChargedMassRow.tau) (rowZ ChargedMassRow.tau) / 8
      = dressedLoad (Anchor.B_pow Anchor.Sector.Lepton) 67 1332 := by
  rw [← dressedLoad_eq_required_load (rowSector ChargedMassRow.tau)
      (rowRung ChargedMassRow.tau) (rowZ ChargedMassRow.tau)
      (by norm_num [rowZ])]
  simp only [rowSector, rowRung, rowZ]
  rw [Anchor.r0_Lepton_eq]
  norm_num
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 conjWindow_pins_exponent · conjWindow_not_muon_and_tau · 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_muon_and_tau · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean:422 
/-- And on the muon/tau pair. -/
theorem conjWindow_not_muon_and_tau :
    ¬ (InConjWindow (dressedLoadConj (Anchor.B_pow Anchor.Sector.Lepton) 61 1332)
      ∧ InConjWindow (dressedLoadConj (Anchor.B_pow Anchor.Sector.Lepton) 67 1332)) := by
  rintro ⟨h61, h67⟩
  have := conjWindow_pins_exponent (Anchor.B_pow Anchor.Sector.Lepton) 1332 61 67 h61 h67
  omega

What this page does not claim

The framework has derived the lepton masses. Any Galois-based selector succeeds in separating the leptons. The injectivity lemma is a physical prediction rather than a structural fact about the formula.

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