Encyclopedia Masses Masses Mass Genesis T10 Channel Cost Irreducibility

ARTICLE 5 claims 4 theorems 1 hypothesis

Masses Mass Genesis T10 Channel Cost Irreducibility

The module proves that the only indivisible cost in the mass-generation ledger is the number 2, and that no fermion can carry three active charge channels.

Verify this page

The irreducible channel cost

In the standard model of particle physics, fermions (quarks and leptons) are grouped by the charges they carry: color charge for quarks, electric charge for charged leptons, and so on. The Recognition Science framework asks what happens when the cost of recognizing a particle's charge channels is forced to be minimal. The module under discussion, T10ChannelCostIrreducibility, proves a sharp structural fact about that cost: the only indivisible cost is 2, and no fermion can have three active channels.

The framework starts with a ledger, a discrete record of recognition events. The cost function J(x) = (x + 1/x)/2 - 1 measures the price of recognizing a scale x. The module defines two notions of irreducibility. In the positive integers, a number k is irreducible if it cannot be written as a sum of two positive integers; the only such number is 1. In the rational-cost monoid, a number n is irreducible if it is even, nonzero, and cannot be written as a sum of two smaller even nonzero numbers; the only such number is 2. Both facts are proved in the machine-checked library of formal theorems.

The key theorem, channel_cost_irreducibility_package, bundles these results with a physical consequence. For any fermion f, the number of active channel classes is at most 2. A fermion in the up or down sector has exactly 2; a lepton has 1; a neutrino has 0. Therefore twice the channel count is never 6. The module also proves that the cost of the golden-ratio scale squared, J(phi^2), is exactly 1/2, a rational number. This is the cost of the irreducible channel count 2.

The package concludes with a prediction: at the lepton sector, the deformed total for channel count 2 differs from the deformed total for channel count 0. This is a falsifiable statement, tagged as a prediction, not a theorem. The module does not derive particle masses; it establishes the structural cost irreducibility that mass generation builds upon.

THEOREM posIrreducible_iff_eq_one · IndisputableMonolith/Masses/MassGenesis/T10ChannelCostIrreducibility.lean
posIrreducible_iff_eq_one · IndisputableMonolith/Masses/MassGenesis/T10ChannelCostIrreducibility.lean:115 
/-- **THEOREM (the cone's unique irreducible is `1`).** Every `k ≥ 2` splits as
`1 + (k − 1)`; `1` splits as nothing. -/
theorem posIrreducible_iff_eq_one (k : ℤ) : PosIrreducible k ↔ k = 1 := by
  constructor
  · rintro ⟨hk1, hnd⟩
    by_contra hne
    have hk2 : 2 ≤ k := by omega
    exact hnd ⟨1, k - 1, le_refl 1, by omega, by omega⟩
  · intro h
    subst h
    refine ⟨le_refl 1, ?_⟩
    rintro ⟨a, b, ha, hb, hab⟩
    omega
THEOREM ratCostIrreducible_iff_eq_two · IndisputableMonolith/Masses/MassGenesis/T10ChannelCostIrreducibility.lean
ratCostIrreducible_iff_eq_two · IndisputableMonolith/Masses/MassGenesis/T10ChannelCostIrreducibility.lean:188 
/-- **THEOREM (the family's unique irreducible is `2`, the `φ²`-step).** Every
even `n ≥ 4` splits as `2 + (n − 2)` with both parts in the family; `2` splits
as nothing, since two nonzero family members sum to at least `4`. -/
theorem ratCostIrreducible_iff_eq_two (n : ℕ) : RatCostIrreducible n ↔ n = 2 := by
  constructor
  · rintro ⟨hexp, h0, hnd⟩
    rcases hexp with rfl | hev
    · exact absurd rfl h0
    · have h2 : 2 ≤ n := two_le_of_even_ne_zero hev h0
      by_contra hne
      have hgt : 2 < n := by omega
      obtain ⟨k, hk⟩ := hev
      apply hnd
      exact ⟨2, n - 2, Or.inr ⟨1, rfl⟩, by norm_num, Or.inr ⟨k - 1, by omega⟩,
        by omega, by omega⟩
  · intro h
    subst h
    refine ⟨Or.inr ⟨1, rfl⟩, by norm_num, ?_⟩
    rintro ⟨a, b, haExp, ha0, hbExp, hb0, hsum⟩
    have ha2 : 2 ≤ a := two_le_of_even_ne_zero (haExp.resolve_left ha0) ha0
    have hb2 : 2 ≤ b := two_le_of_even_ne_zero (hbExp.resolve_left hb0) hb0
    omega
THEOREM activeChannelClasses_le_two · IndisputableMonolith/Masses/MassGenesis/T10ChannelCostIrreducibility.lean
activeChannelClasses_le_two · IndisputableMonolith/Masses/MassGenesis/T10ChannelCostIrreducibility.lean:326 
/-- **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 jcost_phi_sq_mirror · IndisputableMonolith/Masses/MassGenesis/T10ChannelCostIrreducibility.lean
jcost_phi_sq_mirror · IndisputableMonolith/Masses/MassGenesis/T10ChannelCostIrreducibility.lean:293 
/-- **THEOREM (the mirror costs the same).** `J(φ⁻²) = 1/2`: cost alone cannot
separate the upward `φ²`-step from its mirror. -/
theorem jcost_phi_sq_mirror : Cost.Jcost ((phi ^ (2 : ℕ))⁻¹) = 1 / 2 := by
  rw [jcost_inv_self]
  exact jcost_phi_sq
HYPOTHESIS channel_cost_irreducibility_package · IndisputableMonolith/Masses/MassGenesis/T10ChannelCostIrreducibility.lean
channel_cost_irreducibility_package · IndisputableMonolith/Masses/MassGenesis/T10ChannelCostIrreducibility.lean:425 
/-- **THEOREM (the C12 package).** One conjunction:

1. both monoids have their irreducibles (`1` in the pricing cone, `2` in the
   rational-cost family);
2. irreducibility coincides with minimality on the pricing cone;
3. irreducibility coincides with minimality on the rational-cost family;
4. the base rule closes from the irreducible per-axis pricing plus the axis
   model;
5. the channel cost's rationality is a consequence of the axis-level premises;
6. the two-class bound: `+6` is twice no species's channel count;
7. the boundary stands without the premise: the coefficient-`4` deformation
   meets every banked clause and changes observable predictions. -/
theorem channel_cost_irreducibility_package (p : DofPricing)
    (hirr : PosIrreducible p.rungPerDof) (M : ChannelDistinctionModel) (Z : ℤ) :
    (PosIrreducible 1 ∧ RatCostIrreducible 2)
    ∧ (∀ k : ℤ, PosIrreducible k ↔ (1 ≤ k ∧ ∀ m : ℤ, 1 ≤ m → k ≤ m))
    ∧ (∀ n : ℕ, RatCostIrreducible n ↔
        (RatCostExp n ∧ n ≠ 0 ∧ ∀ m : ℕ, RatCostExp m → m ≠ 0 → n ≤ m))
    ∧ (∀ f : Fermion,
        p.exponentOf M.distinctionsPerChannel * activeChannelClasses f
          = 2 * activeChannelClasses f)
    ∧ (∃ q : ℚ, Cost.Jcost (phi ^ (2 : ℕ)) = (q : ℝ))
    ∧ (∀ f : Fermion, 2 * activeChannelClasses f ≠ 6)
    ∧ predictAt .Lepton (deformedTotal 2 Fermion.e) Z
        ≠ predictAt .Lepton (deformedTotal 0 Fermion.e) Z :=
  ⟨⟨posIrreducible_one, (ratCostIrreducible_iff_eq_two 2).2 rfl⟩,
   posIrreducible_iff_minimal,
   ratCostIrreducible_iff_minimal,
   fun f => base_rule_of_irreducible_pricing p hirr M f,
   (channel_cost_rational_of_irreducible_pricing p hirr M).2,
   twice_channel_count_ne_six,
   (dofPricing_boundary_without_minimality Z).2.2.2⟩

What this page does not claim

The module does not derive the numerical values of any particle masses. The module does not prove that the cost function J is the only possible cost function; that is a separate theorem. The module does not claim that the prediction about lepton deformed totals has been experimentally verified.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND