Masses Channel Distinction Channel Count Is Distinction Count

The channel count as a distinction count

A fundamental particle such as an electron can couple to a force, or not. In the Recognition Science framework, this coupling is not a vague affinity but a discrete record: a ledger, a list of facts the universe keeps about the particle. The declaration channel_count_is_distinction_count states a precise identity: the number of active channels a particle couples to equals the number of its two-sided distinctions that stand on the affirm side. In plainer words, counting the forces a particle feels is the same as counting the yes/no decisions it makes about those forces.

The theorem is proved for the two channels in the framework's model: charge and color. The charge channel's distinction is whether the particle's charge is nonzero, and the theorem couplesToCharge_true_iff establishes that this is exactly the condition for coupling. The color channel's second axis is its orientation, up or down, and the theorem color_orientation_is_second_distinction proves that the two possible orientations are genuinely distinct data. The counting theorem then sums these: one for each channel where the distinction is affirmed, zero where it is not.

The framework's library, a machine-checked collection of formal theorems, also proves a precedent that fixes the unit of counting. The B-22 coherence exponent counts 3 spatial plus 1 temporal plus 1 balance axis to give 5, and the theorem b22_counts_two_sided_axis_as_one shows that a two-sided axis counts as one degree of freedom, not two. The theorem sides_as_dofs_breaks_b22 confirms that counting sides instead would give 6, breaking the established value. This precedent is what lets the framework identify a distinction axis, not a side, as the unit being counted.

In Recognition Science, the model then takes the step beyond the proved theorems: it chooses that each coupled gauge channel carries exactly two banked axes, presence and orientation. This is a definitional choice, not a proved result. Under this model and the minimal per-degree-of-freedom pricing, the base coefficient for a rung becomes 2, as proved in base_rule_of_channelDistinctionModel. The boundary of the model is also marked: the theorem channelDistinction_boundary shows that alternative axis counts, one or three per channel, would change observable predictions, so the choice of two is not vacuous.

What the declaration does not claim is as important as what it proves. It does not claim that the identification of a channel with exactly two distinctions is derived; that is the model. It does not claim that the physical bridge from recognition to actual forces is closed; that remains open. And it does not claim that the counting applies beyond the two channels, charge and color, that the framework currently models. The theorem is a precise, kernel-checked identity within a specific model, and the model's boundaries are part of the statement.

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

/-- The charge predicate decides nonzero charge. -/
theorem couplesToCharge_true_iff (f : Fermion) :
    couplesToCharge f = true ↔ tildeQ f ≠ 0 := by
  unfold couplesToCharge
  by_cases h : tildeQ f = 0 <;> simp [h]

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

What this page does not claim

The identification of a channel with exactly two distinctions is a proved result; it is a model choice. The physical bridge from recognition to actual forces is closed; that remains open. The counting applies to channels beyond charge and color that the framework does not yet model.

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: