Masses Mass Genesis T10 Channel Cost Irreducibility Channel Cost Irreducibility

The irreducible channel

In the Recognition Science framework, a ledger, a discrete record of events, assigns a cost to each act of recognition. The declaration channel_cost_irreducibility_package is a single machine-checked theorem that bundles together several facts about that cost. Its central result is about irreducibility: a cost is irreducible if it cannot be written as the sum of two smaller positive costs. The theorem proves that in the positive integers, the only irreducible cost is 1, and in the rational costs generated by the framework's cost function, the only irreducible cost is 2.

The proof works by defining two different notions of decomposition. A positive integer is decomposable if it is the sum of two positive integers; the theorem proves that every integer greater than 1 is decomposable, leaving 1 as the sole irreducible. For the rational costs, which are values of the framework's cost function at powers of the golden ratio, the theorem proves that 2 is the only irreducible value. This is a purely formal result, checked by the machine, and it does not depend on any physical measurement.

The package then connects this abstract result to the framework's model of particle masses. It proves that for any fermion, the number of active channel classes is at most 2, and that twice this number is never 6. This means that a certain combination of channels, which would correspond to a specific mass value, is forbidden. The package also proves that the cost function at the square of the golden ratio is rational, and that a particular prediction about the electron's mass differs from a prediction with zero channels.

In Recognition Science, this theorem is part of a chain that forces the structure of particle masses. The irreducibility of the cost 2 is what makes the two-channel configuration the minimal nonzero possibility. The package does not claim that this proves the actual mass of any particle, nor does it claim that the framework's model of particle masses is unique. It establishes a structural constraint, not a numerical prediction.

/-- **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 (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 (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 decoy offset is unreachable).** `+6` is twice no species's
channel count: it would require a third channel class, and the banked predicate
structure has exactly two. -/
theorem twice_channel_count_ne_six (f : Fermion) : 2 * activeChannelClasses f ≠ 6 := by
  have h := activeChannelClasses_le_two f
  omega

/-- **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

What this page does not claim

This theorem does not prove the numerical value of any particle mass. This theorem does not claim that the framework's model of particle masses is unique. This theorem does not establish that the cost of recognition is physically observable.

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: