Masses Mass Genesis T10 Boson Channel Reach Only Maximal Reach Lands On Banked Y

The banked yardstick

The standard model of particle physics sorts matter into quarks, charged leptons, and neutrinos, and it sorts the forces that act on them into the electromagnetic, strong, and weak interactions. A gauge carrier is a particle that transmits one of these forces: the photon for electromagnetism, the gluon for the strong force, and the W and Z bosons for the weak force. Each carrier reaches a certain set of fermions, the matter particles it can interact with. The photon, for example, reaches only particles that carry electric charge, while the W boson reaches every fermion.

In Recognition Science, a framework that derives physical structure from a forced cost of recognition, a machine-checked library of formal theorems examines how many distinct channels each carrier can resolve. A channel is a way of telling two species of fermion apart: the charge channel distinguishes charged from uncharged particles, and the colour channel distinguishes quarks from leptons. The library proves that the photon resolves one channel, the gluon resolves none, and the W and Z bosons each resolve two. No carrier can resolve three, because a fermion that carries colour also carries charge, so the two channels never act independently.

The declaration only_maximal_reach_lands_on_banked_yardstick establishes a precise numerical consequence. The framework defines a target number, the banked yardstick, built from a fixed offset and a multiple of the W boson's channel reach. The theorem proves that a carrier lands on this yardstick exactly when its channel reach is maximal, meaning it resolves both the charge and colour channels. The W and Z bosons, with reach two, hit the target. The photon, with reach one, and the gluon, with reach zero, miss it. A separate theorem shows that no carrier with submaximal reach can land on the yardstick, and that a decoy number built from a different counting scheme also misses.

The result is a structural fact about the framework's model of gauge carriers, not a measurement of any physical quantity. It does not claim that the W boson's mass equals the yardstick, nor that the framework predicts the numerical values of particle masses. The theorem concerns a counting relation between channels and a target number; it says nothing about why the W boson weighs about 80 gigaelectronvolts. The framework's broader mass ladder is a separate claim, and this declaration does not establish it.

/-- **THEOREM (the photon reach is `1`).** -/
theorem channelReach_photon : channelReach (GaugeCarrier.couples .photon) = 1 := by
  unfold channelReach
  rw [if_neg photon_not_resolvesCharge, if_pos photon_resolvesColor]
  norm_num

/-- **THEOREM (the gluon reach is `0`).** Its coupled set is a single
channel cell: it resolves no channel distinction. -/
theorem channelReach_gluon : channelReach (GaugeCarrier.couples .gluon) = 0 := by
  unfold channelReach
  rw [if_neg gluon_not_resolvesCharge, if_neg gluon_not_resolvesColor]
  norm_num

/-- **THEOREM (the electroweak reach is `2`).** -/
theorem channelReach_wBoson : channelReach (GaugeCarrier.couples .wBoson) = 2 := by
  unfold channelReach
  rw [if_pos wBoson_resolvesCharge, if_pos wBoson_resolvesColor]
  norm_num

/-- **THEOREM (the Z reach is `2`).** -/
theorem channelReach_zBoson : channelReach (GaugeCarrier.couples .zBoson) = 2 := by
  unfold channelReach
  rw [if_pos zBoson_resolvesCharge, if_pos zBoson_resolvesColor]
  norm_num

/-- **THEOREM (no boson reach has three classes).** -/
theorem channelReach_ne_three (S : Fermion → Bool) : channelReach S ≠ 3 := by
  have h := channelReach_le_two S
  omega

/-- **THEOREM (the electroweak reach equals the quark channel count).**
The maximal boson reach IS the maximal species channel count, which the
C12 module proved is attained exactly at the quark sectors
(`activeChannelClasses_eq_two_iff`). -/
theorem ew_reach_eq_quark_channel_count :
    channelReach (GaugeCarrier.couples .wBoson) = activeChannelClasses Fermion.u := by
  rw [channelReach_wBoson]
  have hu : activeChannelClasses Fermion.u = 2 := by
    simp [activeChannelClasses, couplesToCharge, couplesToColor, tildeQ, RSBridge.sectorOf]
  rw [hu]

/-- **THEOREM (the sub-maximal readings miss the electroweak yardstick).**
Reading the offset at the lepton channel count (`1`, offset `+2`,
yardstick `53`) or the neutrino channel count (`0`, offset `+0`,
yardstick `51`) yields integers that are not `r0(EW) = 55`: the
maximality clause is what lands the offset on `+4`. -/
theorem submaximal_species_readings_miss_ew_yardstick :
    3 * (Anchor.W : ℤ) + 2 * activeChannelClasses Fermion.e
      ≠ Anchor.r0 Anchor.Sector.Electroweak ∧
    3 * (Anchor.W : ℤ) + 2 * activeChannelClasses Fermion.nu1
      ≠ Anchor.r0 Anchor.Sector.Electroweak := by
  have hW : (Anchor.W : ℤ) = 17 := by
    simp only [Anchor.W, wallpaper_groups]
    norm_num
  have he : activeChannelClasses Fermion.e = 1 := by
    simp [activeChannelClasses, couplesToCharge, couplesToColor, tildeQ, RSBridge.sectorOf]
  have hnu : activeChannelClasses Fermion.nu1 = 0 := by
    simp [activeChannelClasses, couplesToCharge, couplesToColor, tildeQ, RSBridge.sectorOf]
  simp only [Anchor.r0]
  rw [hW, he, hnu]
  norm_num

What this page does not claim

The theorem does not claim that the W boson's measured mass equals the yardstick. It does not claim that the framework predicts the numerical values of any particle masses. It does not claim that the yardstick is a physical observable rather than a structural target.

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/T10BosonChannelReach.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: