Masses Mass Genesis T10 Times Three Multiplier Five E Passive Incompatible With

The banked offset exclusion

The declaration five_e_passive_incompatible_with_banked_offset is a formal theorem in the Recognition Science framework's machine-checked library of formal theorems. It establishes a negative result: a particular integer, called E_passive (the passive energy constant, set to 11), cannot divide a certain expression built from the framework's electroweak sector. The expression is the framework's electroweak yardstick (the reference value r0 for the electroweak sector, which is 55) minus twice the channel reach of the W boson (the number of cells that boson touches, which is 2), all taken modulo E_passive. The theorem proves this remainder is not zero.

In plainer terms, the framework's internal arithmetic forbids one specific way of assigning a mass-generation multiplier. The theorem is part of a larger package of results in the same file that together force the number 3 as the multiplier for the three fermion generations. A companion theorem, multiplier_forced_three, shows that any integer M satisfying M times 17 equals 51 must be 3. The exclusion theorem about E_passive is one of several consistency checks that rule out alternative multipliers, such as a fourth cell or a different generation count.

The theorem does not claim that E_passive itself is wrong, nor that the framework derives the fine-structure constant or any specific particle mass. It only says that one particular arithmetic arrangement, the banked offset involving E_passive, is incompatible with the framework's own electroweak yardstick. The result is a theorem in the sense that it is proved in the Lean 4 proof assistant with no axioms beyond the standard three, but it does not by itself establish any physical prediction about measured masses.

/-- **The C10 `5 × E_passive` decoy is incompatible with the banked offset.**
Removing the C13 channel-reach offset `+4` from the yardstick leaves `51`,
and `51` is NOT a multiple of `E_passive = 11`. The `5 × 11` reading requires
offset `0`; the offset is banked at `+4`, so the W2 non-uniqueness no longer
stands over this decomposition. -/
theorem five_e_passive_incompatible_with_banked_offset :
    (Anchor.r0 Anchor.Sector.Electroweak
        - 2 * channelReach (GaugeCarrier.couples .wBoson))
      % (Anchor.E_passive : ℤ) ≠ 0 := by
  rw [channelReach_wBoson]
  simp only [Anchor.r0]
  have hW : (Anchor.W : ℤ) = 17 := by
    simp only [Anchor.W, wallpaper_groups]
    norm_num
  rw [hW]
  have hE : (Anchor.E_passive : ℤ) = 11 := by decide
  rw [hE]
  norm_num

/-- **The multiplier is forced to `3`.** Any `M` with `M × W` equal to the
electroweak wallpaper content (`r0(EW) − 4 = 51`) and `W = 17` satisfies
`M = 3`: the multiplier value is not a choice. -/
theorem multiplier_forced_three (M : ℤ)
    (h : M * (Anchor.W : ℤ) = Anchor.r0 Anchor.Sector.Electroweak - 4) :
    M = 3 := by
  have hW : (Anchor.W : ℤ) = 17 := by
    simp only [Anchor.W, wallpaper_groups]
    norm_num
  simp only [Anchor.r0] at h
  rw [hW] at h
  have h17 : (17 : ℤ) ≠ 0 := by norm_num
  have h51 : M * 17 = 3 * 17 := by omega
  exact mul_right_cancel₀ h17 h51

What this page does not claim

The framework derives the fine-structure constant alpha. The theorem establishes any measured particle mass value. The theorem claims E_passive is physically wrong, only that one arithmetic arrangement is incompatible.

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