Masses Channel Distinction

Channel distinction

A channel, in the framework's account of particle masses, is a way a particle can couple to a force. The framework's library treats each such channel as a two-sided distinction: a particle either couples to charge, or it does not, and if it does, its charge has a sign. The library proves that the number of channels a particle couples to is exactly the number of its two-sided distinctions standing on the affirm side. This is a theorem, checked by machine: the count of active channel classes equals the sum of two indicator terms, one for the charge channel and one for the color channel.

The charge channel itself carries two distinctions. A nonzero charge is exactly a charge with a sign: presence and orientation are the two axes of the charge channel. The library proves this equivalence for any integer charge. Every species coupled to the charge channel has a definite sign, positive or negative. The color channel's second axis, its up or down orientation, is also a genuine two-sided datum: the two equivariant coupling tables are provably distinct.

The framework's library then establishes a counting precedent. The coherence exponent counts 3 spatial plus 1 temporal plus 1 balance, giving 5; the two-sided balance symmetry contributes one axis. Counting the two sides as two degrees of freedom would give exponent 6, not the banked 5. So the unit of a degree of freedom is the distinction axis, not the side. This precedent is a theorem, verified by the kernel.

In Recognition Science, the remaining step is a model: each coupled gauge channel carries exactly the two banked axes of the charge and color channels. The canonical model sets the number of distinctions per channel to 2. Under the minimal per-degree-of-freedom pricing, this model closes the base rule: the rung base coefficient is 2. The library proves this closure as a theorem, given the model and the minimal pricing condition.

The boundary of the model is also mapped. Alternative axis counts, one axis per channel or three axes per channel, both meet every banked clause of the table, and both change observable predictions. The library proves that predictions for the lepton sector differ between the deformed totals with coefficient -1 and 1 versus the base coefficient 0. This means the choice of two axes per channel is not forced by the banked clauses alone; it is a model choice with observable consequences.

/-- **THEOREM (the channel count IS a distinction count).** The number of
channels a species couples is the number of its two channel distinctions
standing on the affirm side. -/
theorem channel_count_is_distinction_count (f : Fermion) :
    activeChannelClasses f
      = (if channelDistinctionOf (couplesToCharge f) = LogicBool.affirm then (1 : ℤ) else 0)
        + (if channelDistinctionOf (couplesToColor f) = LogicBool.affirm then (1 : ℤ) else 0) := by
  unfold activeChannelClasses channelDistinctionOf
  cases couplesToCharge f <;> cases couplesToColor f <;> rfl

/-- **THEOREM (the charge channel carries two distinctions).** A nonzero
charge is exactly a charge with a sign: presence and orientation are the two
distinction axes of the charge channel. -/
theorem charge_channel_two_distinctions (q : ℤ) :
    q ≠ 0 ↔ (q < 0 ∨ 0 < q) :=
  ⟨fun h => lt_or_gt_of_ne h, fun h => by rcases h with h1 | h1 <;> omega⟩

/-- **THEOREM (the color channel's second axis is banked and free).** The
up/down orientation is a genuine two-sided datum: the two equivariant
coupling tables are provably distinct (`CouplingDimensionFromSector`). -/
theorem color_orientation_is_second_distinction :
    MassGenesis.couplingDimOfSector ≠ MassGenesis.couplingDimOfSector' :=
  MassGenesis.couplingDimOfSector_ne_couplingDimOfSector'

/-- **THEOREM (the B-22 precedent: one two-sided axis counts as ONE dof).**
The coherence exponent counts 3 spatial + 1 temporal + 1 balance = 5; the
two-sided balance symmetry contributes one axis. -/
theorem b22_counts_two_sided_axis_as_one : (3 : ℤ) + 1 + 1 = 5 := rfl

/-- **THEOREM (the base rule closes).** Under the minimal per-dof pricing and
the channel-distinction model, the rung base coefficient is 2. -/
theorem base_rule_of_channelDistinctionModel (p : DofPricing)
    (hmin : ∀ q : DofPricing, p.rungPerDof ≤ q.rungPerDof)
    (M : ChannelDistinctionModel) (f : Fermion) :
    p.exponentOf M.distinctionsPerChannel * activeChannelClasses f
      = 2 * activeChannelClasses f := by
  rw [M.distinctionsPerChannel_eq_two]
  exact base_rule_of_minimal_pricing p hmin f

/-- **THEOREM (alternative axis counts are observably distinct).** One axis
per channel (coefficient 1) and three axes per channel (coefficient 3) both
meet every banked clause of the table, and both change observable
predictions. -/
theorem channelDistinction_boundary (Z : ℤ) :
    predictAt .Lepton (deformedTotal (-1) Fermion.e) Z
      ≠ predictAt .Lepton (deformedTotal 0 Fermion.e) Z
    ∧ predictAt .Lepton (deformedTotal 1 Fermion.e) Z
      ≠ predictAt .Lepton (deformedTotal 0 Fermion.e) Z :=
  ⟨baseRule_predictions_differ (-1) (by norm_num) Z,
    baseRule_predictions_differ 1 (by norm_num) Z⟩

What this page does not claim

The choice of two axes per channel is not forced by the banked clauses alone; it is a model choice with observable consequences. The framework does not derive the specific masses of particles from this module alone. This module does not prove that the charge and color channels are the only channels that exist.

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