Encyclopedia Masses Masses Mass Genesis T10 Galois Conjugate Selector Scratch

ARTICLE 5 claims 5 theorems

Masses Mass Genesis T10 Galois Conjugate Selector Scratch

A machine-checked library proves that no condition on a certain algebraic conjugate can pick out the electron, muon, and tau all at once.

Verify this page

The Galois selector

In the Recognition Science account of particle masses, each charged lepton sits on a ladder of possible transport counts, whole numbers that index how many recognition steps a mass represents. The electron, muon, and tau occupy the same sector and charge index, but at transport counts 50, 61, and 67. A natural hope is that some algebraic test on the mass formula could select exactly those three counts. This scratch file in the framework's machine-checked library tests that hope with the Galois conjugate of the golden ratio and proves the hope fails.

The golden ratio phi satisfies phi^2 = phi + 1, and its Galois conjugate is 1 - phi, which equals -1/phi. The conjugate is special because it moves in the opposite direction from phi: powers of phi grow without bound, while powers of the conjugate shrink toward zero. That contrast means the conjugate can see the transport count, where ordinary divisibility and valuation tests cannot. The library proves three candidate tests. The symmetric norm product carries only the parity of the count, so the muon and tau, both at odd counts, become indistinguishable. The antisymmetric ratio is unchanged when the whole load is doubled, so it accepts a spurious doubled-scale witness. Only the conjugate magnitude, constrained to a half-open window between phi^-1 and 1, pins the count uniquely on an orbit.

That surviving test still cannot do the job. The window pins one count per orbit, but the theory's own table places all three leptons on one orbit, with sector power B = -22 and charge index Z = 1332. A theorem in the module states the class wall: no condition on the realized load that pins the exponent can accept two same-sector same-charge rows at different rungs. Because the representation of a load as a + b*phi is unique, every Galois condition factors through the load's value and falls inside that wall. The module concludes with the concrete consequence: the conjugate window rejects the doubled scale, but it also rejects the electron together with the muon, and the muon together with the tau.

This scratch file states no target and imports no target, and it contains no unproved assumptions. What it establishes is a negative result, and a sharp one. The Galois conjugate, the one classical construction that seemed able to see the transport count, cannot separate the three leptons because any test that pins one count must reject the other two. The search for a selector that distinguishes the leptons therefore needs a different structural idea, one that does not factor through the load's value alone.

THEOREM phiConj_eq_neg_inv · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean
phiConj_eq_neg_inv · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean:86 
/-- The conjugate is minus the inverse: this is what makes the two embeddings move
in opposite directions. -/
theorem phiConj_eq_neg_inv : phiConj = -phi⁻¹ := by
  have hne : phi ≠ 0 := Constants.PhiLadder.phi_ne_zero
  have h : phiConj * phi = (-phi⁻¹) * phi := by
    rw [phiConj_mul_phi]
    field_simp
  exact mul_right_cancel₀ hne h
THEOREM galoisNorm_dressed · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean
galoisNorm_dressed · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean:163 
/-- **The Galois norm of the dressed target, exactly.** The transport count enters
only through `(-1) ^ n`. -/
theorem galoisNorm_dressed (B n Z : ℤ) :
    dressedLoad B n Z * dressedLoadConj B n Z
      = (2 : ℝ) ^ (2 * (B - 3)) * (-1 : ℝ) ^ n * ((Z : ℝ) ^ 2 + (Z : ℝ) - 1) := by
  have hpow : (2 : ℝ) ^ (2 * (B - 3))
      = (2 : ℝ) ^ (B - 3) * (2 : ℝ) ^ (B - 3) := by
    rw [show 2 * (B - 3) = (B - 3) + (B - 3) by ring,
      zpow_add₀ (by norm_num : (2 : ℝ) ≠ 0)]
  rw [dressedLoad, dressedLoadConj, hpow]
  calc (2 : ℝ) ^ (B - 3) * phi ^ n * (phi + (Z : ℝ))
          * ((2 : ℝ) ^ (B - 3) * phiConj ^ n * (phiConj + (Z : ℝ)))
      = (2 : ℝ) ^ (B - 3) * (2 : ℝ) ^ (B - 3) * (phi ^ n * phiConj ^ n)
          * ((phi + (Z : ℝ)) * (phiConj + (Z : ℝ))) := by ring
    _ = (2 : ℝ) ^ (B - 3) * (2 : ℝ) ^ (B - 3) * (-1 : ℝ) ^ n
          * ((Z : ℝ) ^ 2 + (Z : ℝ) - 1) := by
          rw [phi_mul_phiConj_zpow, dressing_mul_conj]
THEOREM galoisRatio_doubled_eq · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean
galoisRatio_doubled_eq · IndisputableMonolith/Masses/MassGenesis/T10GaloisConjugateSelectorScratch.lean:219 
/-- **The Galois-pair ratio is scale-invariant.** -/
theorem galoisRatio_doubled_eq (B n Z : ℤ) :
    dressedLoad (B + 2) n Z / dressedLoadConj (B + 2) n Z
      = dressedLoad B n Z / dressedLoadConj B n Z := by
  rw [dressedLoad_doubled, dressedLoadConj_doubled,
    mul_div_mul_left _ _ (by norm_num : (4 : ℝ) ≠ 0)]
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 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

This module does not prove that the electron, muon, and tau have the measured masses; it only analyzes a candidate selector for their transport counts. This module does not establish that no selector of any kind can distinguish the leptons; it proves a wall for conditions that pin the exponent on a single orbit. This module does not claim the Galois conjugate is useless for all purposes; it shows the three natural combinations fail to close the T10 residual.

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