Masses Mass Genesis T10 Channel Cost Irreducibility Decoy Yardstick Ne Channel R

The decoy yardstick

The number 57 is a recurring integer in the Recognition Science framework's mass formulas. The theorem named decoy_yardstick_ne_channel_reading proves a precise negative statement about it: for any fermion, the integer 57 is not equal to 3 times the wallpaper-group constant W (which is 17) plus 2 times the fermion's number of active channel classes. In plainer terms, 57 cannot be produced by that particular combination of a fixed structural constant and a particle's channel count.

The proof is short and computational. The library first establishes that W equals 17, and that every fermion has at most two active channel classes. With those two facts, the arithmetic is forced: 3 times 17 is 51, and adding 2, 4, or 0 (the possible values of twice the channel count) gives 53, 55, or 51, never 57. The theorem is a machine-checked result in the framework's library of formal theorems, meaning the reasoning is verified by a computer and carries no hidden assumptions beyond the framework's own definitions.

The name "decoy yardstick" signals its role. The framework also proves a companion result, ew_yardstick_channel_reading, which shows that the electroweak sector's reference value equals exactly 3W plus twice the channel count of the up quark, which is 51 plus 4, or 55. The decoy theorem shows that 57 is not another such reading; it is a number that looks like it could be a channel-based yardstick but is not. This distinction matters for preserving the framework's internal accounting consistency: if 57 could be read as a channel combination, the mass formulas would have two competing interpretations for the same integer.

What the theorem does not claim is just as important. It does not say what 57 actually is, or why it appears in the mass formulas. It does not assert that any physical measurement equals 57, and it does not identify 57 with any particle property. The theorem is purely a negative structural result about arithmetic consistency within the framework's definitions. The physical meaning of 57, if any, remains an open question that this declaration does not address.

/-- **THEOREM (the discriminator).** The decoy yardstick `57 = 3W + 6` admits
NO channel reading: `57 − 3W = 6` is twice no species's coupled channel count.
Given the channel reading of the offset, the two-class structure selects `+4`
over `+6`. -/
theorem decoy_yardstick_ne_channel_reading (f : Fermion) :
    (57 : ℤ) ≠ 3 * (Anchor.W : ℤ) + 2 * activeChannelClasses f := by
  have hW : (Anchor.W : ℤ) = 17 := by
    simp only [Anchor.W, wallpaper_groups]
    norm_num
  have hb := activeChannelClasses_le_two f
  rw [hW]
  omega

/-- The decoy yardstick's offset over `3W` is `6`. -/
theorem decoy_offset_over_3W : (57 : ℤ) - 3 * (Anchor.W : ℤ) = 6 := by
  have hW : (Anchor.W : ℤ) = 17 := by
    simp only [Anchor.W, wallpaper_groups]
    norm_num
  rw [hW]
  norm_num

/-- **THEOREM (the two-class bound).** No species couples to more than two
channel classes: the banked predicate structure has exactly two. -/
theorem activeChannelClasses_le_two (f : Fermion) : activeChannelClasses f ≤ 2 := by
  rw [activeChannelClasses_eq]
  cases RSBridge.sectorOf f <;> decide

/-- **THEOREM (the banked yardstick admits the channel reading).**
`r0(EW) = 3W + 2 × (quark channel count)`: the `+4` is twice the maximal, and
quark-attained, channel count. Recorded as arithmetic on the stipulated value;
the forcing content is the bound, not this equality. -/
theorem ew_yardstick_channel_reading :
    Anchor.r0 Anchor.Sector.Electroweak
      = 3 * (Anchor.W : ℤ) + 2 * activeChannelClasses Fermion.u := by
  have hu : activeChannelClasses Fermion.u = 2 := by
    simp [activeChannelClasses, couplesToCharge, couplesToColor, tildeQ, RSBridge.sectorOf]
  have hW : (Anchor.W : ℤ) = 17 := by
    simp only [Anchor.W, wallpaper_groups]
    norm_num
  simp only [Anchor.r0]
  rw [hu, hW]
  norm_num

What this page does not claim

The theorem does not identify what the number 57 represents physically. The theorem does not assert that any measured particle property equals 57. The proof does not depend on any empirical measurement, only on the framework's definitions.

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