Masses Channel Distinction Charge Channel Two Distinctions

The charge channel's two distinctions

In the Recognition Science account of particle masses, the framework's library of machine-checked theorems proves that a nonzero electric charge is exactly the same datum as a charge with a sign. The theorem charge_channel_two_distinctions states this as a logical equivalence: for any integer charge q, the statement q ≠ 0 holds if and only if q < 0 or 0 < q. This is a formal way of saying that the charge channel carries two distinction axes: presence (is the charge nonzero?) and orientation (is it negative or positive?). The proof is immediate from the ordering of the integers, and the framework's kernel checks it.

The declaration sits inside a larger structure that counts how many channels a fermion couples to. A separate theorem, channel_count_is_distinction_count, proves that the number of active channel classes for a fermion equals the number of its two channel distinctions standing on the affirm side. The charge channel contributes one to this count when the fermion couples to charge, and the color channel contributes one when it couples to color. The charge theorem supplies the precise meaning of "couples to charge": it is true exactly when the charge value is nonzero.

The two-axis reading is not an idle philosophical gloss. The framework's library proves a counting precedent in the B-22 coherence exponent: it counts 3 spatial plus 1 temporal plus 1 balance axis, and the two-sided balance symmetry contributes exactly one degree of freedom, not two. A theorem sides_as_dofs_breaks_b22 shows that counting the two sides as two degrees of freedom would give exponent 6 instead of the banked 5. The unit of a degree of freedom is therefore the distinction axis, not the side. The charge theorem fits this pattern: presence and orientation are two axes on one channel, and the channel counts once.

What the declaration does not claim is just as important. It does not derive the numerical value of any particle's charge, nor does it explain why a particular fermion couples to the charge channel at all. It establishes only the logical structure: nonzero charge and signed charge are the same fact. The framework's model chooses to identify each coupled gauge channel as carrying exactly these two banked axes, presence and orientation. That identification is a definitional choice, not a theorem. The theorem itself is about the integers; the model is about how to read them as physics.

/-- **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 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 sides-as-dofs reading is refuted by the precedent).**
Counting the two-sided balance as two dofs would give exponent 6, not the
banked 5. So the dof unit is the distinction axis, not the side. -/
theorem sides_as_dofs_breaks_b22 : (3 : ℤ) + 1 + 2 ≠ 5 := by decide

/-- The remaining model: a configuration dof is a distinction AXIS (B-22's
own counting), and each coupled gauge channel carries exactly the two banked
axes of Part II. The axes and the precedent are kernel-checked; the
identification is the model. -/
structure ChannelDistinctionModel where
  distinctionsPerChannel : ℕ
  distinctionsPerChannel_eq_two : distinctionsPerChannel = 2

What this page does not claim

The declaration does not derive the numerical value of any particle's charge. The declaration does not explain why a particular fermion couples to the charge channel. The two-axis identification is a model, not a theorem about physics.

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: