Masses Mass Genesis Coupling Dimension From Sector Coupling Dim Colored Pair

The colored pair's dimensions

In the Recognition Science framework, a ledger (a discrete record of events) carries a cost, and from that cost the framework derives a chain of physical structure. One branch of that chain concerns coupling dimensions, which are whole numbers attached to particle sectors. The theorem couplingDim_colored_pair states that a colored Up pattern and its charge conjugate Down pattern take the coupling dimensions {0, 2}.

This is a concrete result. The framework's library of formal theorems proves that a colorless Lepton couples at dimension 1, the self-dual middle dimension of the boundary sphere. The colored pair, by contrast, covers the two dual extremes, 0 and 2. The theorem is proved for any pattern with nonzero charge skew and nonzero loop rank, and it relies on the earlier result that charge conjugation swaps the colored Up and Down sectors.

The significance is that the equivariance hypothesis, which the positive coupling-dimension theory previously assumed as an abstract input, is now derived as a theorem. The library shows that the coupling dimension of a charge conjugate equals the dual of the original. This is not a definitional choice; it is a proved consequence of the sector structure.

What the theorem does not claim is also sharp. It does not fix which colored sign sits at dimension 0 versus dimension 2. The opposite orientation, Up at 2 and Down at 0, is equally equivariant. The library proves there are exactly two equivariant coupling tables, related by the duality involution, and that no internal datum selects between them. The up/down orientation remains a free choice, a sign convention, not a combinatorial consequence.

/-- **THEOREM (colored pair covers the dual extremes `{0,2}`, concretely).** A colored Up pattern
    and its charge conjugate Down take coupling dimensions `{0,2}` — the non-self-dual
    Poincaré-dual extremes. Derived from `colored_sector_C_swaps`. -/
theorem couplingDim_colored_pair (T Tc : PatternTopology)
    (hloop : T.q3LoopRank ≠ 0) (hpos : 0 < T.chargeSkew)
    (hcLoop : Tc.q3LoopRank ≠ 0) (hcQ : Tc.chargeSkew = - T.chargeSkew) :
    ({couplingDimOfTopology T, couplingDimOfTopology Tc} : Finset ℕ) = {0, 2} := by
  obtain ⟨hu, hd⟩ := colored_sector_C_swaps T Tc hloop hpos hcLoop hcQ
  unfold couplingDimOfTopology
  rw [hu, hd]
  decide

/-- **THEOREM (the up/down orientation is a free `ℤ/2`: there are EXACTLY two equivariant coupling
    dimensions).** Any `g : Anchor.Sector → ℕ` that sends the charge-conjugation-fixed sectors
    (Lepton, Electroweak) to the self-dual middle `1`, sends the colored C-pair to the dual extremes
    `{0,2}`, and is equivariant on that pair (`g Down = dualDim (g Up)`) is EXACTLY one of the two
    orientations `couplingDimOfSector` / `couplingDimOfSector'`. Combined with `couplingDim_equivariant`
    and `couplingDim_equivariant'` (both ARE equivariant), this proves the orientation is not fixed by
    the duality + sector structure — it is a genuine `ℤ/2` convention, the conventional choice of
    which `chargeSkew` sign is labeled "up." -/
theorem orientation_is_free_Z2
    (g : Anchor.Sector → ℕ)
    (hLep : g Anchor.Sector.Lepton = 1)
    (hEW : g Anchor.Sector.Electroweak = 1)
    (hPair : ({g Anchor.Sector.UpQuark, g Anchor.Sector.DownQuark} : Finset ℕ) = {0, 2})
    (hEquiv : g Anchor.Sector.DownQuark = dualDim (g Anchor.Sector.UpQuark)) :
    g = couplingDimOfSector ∨ g = couplingDimOfSector' := by
  have hUp : g Anchor.Sector.UpQuark = 0 ∨ g Anchor.Sector.UpQuark = 2 := by
    have hmem : g Anchor.Sector.UpQuark ∈ ({0, 2} : Finset ℕ) := by
      rw [← hPair]; exact Finset.mem_insert_self _ _
    simpa using hmem
  rcases hUp with h0 | h2
  · left
    have hDown : g Anchor.Sector.DownQuark = 2 := by rw [hEquiv, h0]; rfl
    funext s; cases s <;> simp [couplingDimOfSector, hLep, hEW, h0, hDown]
  · right
    have hDown : g Anchor.Sector.DownQuark = 0 := by rw [hEquiv, h2]; rfl
    funext s; cases s <;> simp [couplingDimOfSector', hLep, hEW, h2, hDown]

What this page does not claim

The theorem does not specify which colored sign is up. The theorem does not derive the up/down orientation from the gauge structure. The theorem does not assign a numerical mass value to any particle.

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/MassGenesis/CouplingDimensionFromSector.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: