Masses Channel Distinction Channel Distinction Of Eq Affirm Iff

The channel predicate

A channel predicate is a yes-or-no test attached to a physical channel, such as charge or color. The declaration channelDistinctionOf_eq_affirm_iff proves, in the framework's machine-checked library of formal theorems, that the predicate affirms exactly when the underlying Boolean is true. That is, the predicate's two-sided distinction, its affirm side versus its reject side, lines up perfectly with the Boolean's true and false. The proof is a two-line case split: check the Boolean, then decide.

The surrounding lemmas give this simple equivalence its weight. One theorem, channel_count_is_distinction_count, shows that the number of channels a fermion couples to equals the number of its channel distinctions standing on the affirm side. Another, couplesToCharge_true_iff, ties the charge predicate to a nonzero charge value, and charge_channel_two_distinctions splits that nonzero condition into a sign: positive or negative. Together they establish that a nonzero charge carries two distinction axes, presence and orientation, and that a charged species always has a definite sign.

The framework then models each coupled gauge channel as carrying exactly those two banked axes. The ChannelDistinctionModel structure fixes distinctionsPerChannel = 2, and the canonical model instantiates it. A theorem, base_rule_of_channelDistinctionModel, closes the loop: under minimal per-degree-of-freedom pricing, the rung base coefficient becomes 2. A boundary theorem, channelDistinction_boundary, shows that alternative axis counts, one or three per channel, both meet every banked clause yet change observable predictions, so the model is not vacuous.

What the declaration does not claim is equally important. It does not assert that any particular physical channel exists, nor that the two-axes-per-channel model is the only possible one. The identification of a configuration degree of freedom with a distinction axis is a model, explicitly labeled as such in the source. The axes and the counting precedent are kernel-checked; the identification is the model.

/-- The predicate affirms exactly when the Boolean is true. -/
theorem channelDistinctionOf_eq_affirm_iff (b : Bool) :
    channelDistinctionOf b = LogicBool.affirm ↔ b = true := by
  cases b <;> decide

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

/-- 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 prove that any specific physical channel exists or that the two-axes model is the only possible one. The model's identification of a degree of freedom with a distinction axis is a definitional choice, not a theorem. The boundary theorem shows alternatives are observable, but it does not say which alternative nature chooses.

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: