Masses Channel Distinction Base Rule Of Channel Distinction Model

The base rule

The declaration base_rule_of_channelDistinctionModel is a theorem in the framework's machine-checked library of formal theorems. It states that under two specific conditions, the base coefficient in a particle's mass formula is exactly 2. The first condition is that the pricing rule is minimal: among all possible pricing rules, it assigns the fewest rungs per degree of freedom. The second condition is the channel distinction model: each gauge channel a particle couples to carries exactly two distinction axes, one for presence and one for orientation.

To see what this means, consider a fermion that couples to the charge channel and the color channel. The theorem says its base coefficient is 2 times the number of active channels. The proof combines two earlier results. One result shows that the number of active channels equals the number of two-sided distinctions standing on the affirm side. The other shows that a nonzero charge is exactly a charge with a sign, so presence and orientation are the two axes of the charge channel. The color channel's orientation axis is provably distinct from its presence axis, so it too carries two axes.

The theorem does not derive the number 2 from nothing. It takes the channel distinction model as a premise, and that model is a definitional choice, not a proved fact. The framework's own documentation marks this clearly: the axes and the counting precedent are kernel-checked, but the identification of a configuration degree of freedom with a distinction axis is the model. The theorem also does not claim that alternative axis counts are impossible. A separate theorem shows that one axis per channel or three axes per channel both satisfy the banked clauses of the table, and both change observable predictions.

In Recognition Science, this result closes a specific gap. It shows that the minimal pricing rule, combined with the two-axis model, yields a base coefficient of 2 for every fermion. The number 2 is not an input; it is the output of the minimality condition and the model. What remains open is whether the physical identification, that a configuration degree of freedom is a distinction axis, is correct. The theorem is conditional on that identification.

/-- **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 (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 (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 theorem does not prove that the channel distinction model is physically true. The theorem does not derive the number 2 from the forcing chain alone. The theorem does not rule out alternative axis counts.

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: