Encyclopedia Masses Masses Mass Genesis Coupling Dimension From Sector

ARTICLE 4 claims 3 theorems 1 model

Masses Mass Genesis Coupling Dimension From Sector

A table that assigns each particle sector a small number now follows from the sector structure itself, with one conventional choice left over.

Verify this page

The coupling dimension

In particle physics, a coupling constant measures how strongly a particle interacts; here the framework assigns each sector a coupling dimension, a number that indexes where the sector sits in a boundary structure. The module MassGenesis (the framework's account of how particle masses arise) makes this dimension concrete: it is a function of the sector alone, not a free parameter. The colorless Lepton and Electroweak sectors sit at dimension 1; the colored Up quark sits at dimension 0 and the Down quark at dimension 2.

The central result is a theorem about charge conjugation, the symmetry that maps a particle to its antiparticle. The framework proves that when a charged pattern is charge-conjugated, its coupling dimension transforms by the boundary duality: the conjugate's dimension is the dual of the original's. For the colorless sectors, which charge conjugation fixes, the self-dual middle dimension 1 is unmoved. For the colored pair, which charge conjugation swaps, the dimensions 0 and 2 exchange places. This equivariance was previously an assumption; the module derives it from the sector charge-conjugation orbit structure, making it a proved theorem (couplingDim_equivariant).

The module also proves that only one conventional choice remains. Which colored charge sign sits at dimension 0 versus dimension 2 is not fixed by the structure: both orientations are equivariant, they are related by the duality involution, and they are the only two equivariant solutions. The theorem orientation_is_free_Z2 shows that any coupling table satisfying the structural conditions is exactly one of the two orientations. This freedom is a genuine sign convention, not a derivable consequence, because the gauge structure carries no canonical positive element.

In plain language: the framework's mass-genesis account now has a concrete, sector-indexed coupling dimension, and it proves that the dimension respects charge conjugation in exactly the way the boundary duality requires. The only leftover freedom is which colored sign is called up, a conventional labeling that no internal structure can resolve. This sharpens the earlier result: the positive coupling-dimension theory's central hypotheses now hold as theorems about a concrete function, not as posited inputs.

MODEL couplingDimOfSector · IndisputableMonolith/Masses/MassGenesis/CouplingDimensionFromSector.lean
couplingDimOfSector · IndisputableMonolith/Masses/MassGenesis/CouplingDimensionFromSector.lean:36 
/-- The sector-indexed coupling dimension on the boundary cell dimensions `{0,1,2}`:
    the colorless Lepton (and the neutral Electroweak) sit at the self-dual middle dimension `1`;
    the colored Up sits at the vertex dimension `0` and Down at the face dimension `2`. The
    `Up ↦ 0 / Down ↦ 2` assignment is the up/down orientation (the one external datum); the OTHER
    choice (`Up ↦ 2 / Down ↦ 0`) is equally equivariant (`couplingDimOfSector'`). -/
def couplingDimOfSector : Anchor.Sector → ℕ
  | Anchor.Sector.Electroweak => 1
  | Anchor.Sector.Lepton => 1
  | Anchor.Sector.UpQuark => 0
  | Anchor.Sector.DownQuark => 2
THEOREM couplingDim_equivariant · IndisputableMonolith/Masses/MassGenesis/CouplingDimensionFromSector.lean
couplingDim_equivariant · IndisputableMonolith/Masses/MassGenesis/CouplingDimensionFromSector.lean:59 
/-- **THEOREM (the concrete coupling dimension is charge-conjugation-equivariant).** For a charged
    pattern `T` (`chargeSkew ≠ 0`) and its charge conjugate `Tc` (same color `q3LoopRank`, negated
    `chargeSkew`), the coupling dimension transforms by the boundary duality:
    `couplingDimOfTopology Tc = dualDim (couplingDimOfTopology T)`. This DERIVES the equivariance
    hypothesis `hequiv` of the positive theory from the sector C-orbit structure — it is no longer
    assumed. The proof cases on color (`q3LoopRank = 0`?) and charge sign, applying
    `sectorFromTopology_lepton/up/down` to pin both sectors. -/
theorem couplingDim_equivariant (T Tc : PatternTopology)
    (hloopEq : Tc.q3LoopRank = T.q3LoopRank)
    (hQc : Tc.chargeSkew = - T.chargeSkew)
    (hQ : T.chargeSkew ≠ 0) :
    couplingDimOfTopology Tc = dualDim (couplingDimOfTopology T) := by
  have hTcQ : Tc.chargeSkew ≠ 0 := by rw [hQc]; exact neg_ne_zero.mpr hQ
  unfold couplingDimOfTopology
  by_cases hloop : T.q3LoopRank = 0
  · have hTcLoop : Tc.q3LoopRank = 0 := by rw [hloopEq]; exact hloop
    rw [sectorFromTopology_lepton T hQ hloop, sectorFromTopology_lepton Tc hTcQ hTcLoop]
    decide
  · have hTcLoop : Tc.q3LoopRank ≠ 0 := by rw [hloopEq]; exact hloop
    by_cases hpos : 0 < T.chargeSkew
    · have hcnpos : ¬ 0 < Tc.chargeSkew := by rw [hQc]; omega
      rw [sectorFromTopology_up T hQ hloop hpos,
          sectorFromTopology_down Tc hTcQ hTcLoop hcnpos]
      decide
    · have hcpos : 0 < Tc.chargeSkew := by rw [hQc]; omega
      rw [sectorFromTopology_down T hQ hloop hpos,
          sectorFromTopology_up Tc hTcQ hTcLoop hcpos]
      decide
THEOREM orientation_is_free_Z2 · IndisputableMonolith/Masses/MassGenesis/CouplingDimensionFromSector.lean
orientation_is_free_Z2 · IndisputableMonolith/Masses/MassGenesis/CouplingDimensionFromSector.lean:192 
/-- **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]
THEOREM OrientationFreedomCert · IndisputableMonolith/Masses/MassGenesis/CouplingDimensionFromSector.lean
OrientationFreedomCert · IndisputableMonolith/Masses/MassGenesis/CouplingDimensionFromSector.lean:219 
/-- Master obstruction certificate: the up/down orientation is a genuine `ℤ/2` freedom the duality +
    sector structure provably cannot resolve. Both orientations are charge-conjugation-equivariant
    (each is an admissible coupling table), they are related by the duality involution, they are
    DISTINCT, and they are the ONLY two equivariant solutions. Hence which colored charge sign sits at
    the vertex dimension `0` versus the face dimension `2` is a sign convention, not an RS-combinatorial
    consequence. -/
structure OrientationFreedomCert where
  left_equivariant :
    ∀ (T Tc : PatternTopology), Tc.q3LoopRank = T.q3LoopRank → Tc.chargeSkew = - T.chargeSkew →
      T.chargeSkew ≠ 0 → couplingDimOfTopology Tc = dualDim (couplingDimOfTopology T)
  right_equivariant :
    ∀ (T Tc : PatternTopology), Tc.q3LoopRank = T.q3LoopRank → Tc.chargeSkew = - T.chargeSkew →
      T.chargeSkew ≠ 0 →
      couplingDimOfSector' (sectorFromTopology Tc)
        = dualDim (couplingDimOfSector' (sectorFromTopology T))
  related_by_duality : ∀ s, couplingDimOfSector' s = dualDim (couplingDimOfSector s)
  distinct : couplingDimOfSector ≠ couplingDimOfSector'
  exactly_two :
    ∀ (g : Anchor.Sector → ℕ),
      g Anchor.Sector.Lepton = 1 → g Anchor.Sector.Electroweak = 1 →
      ({g Anchor.Sector.UpQuark, g Anchor.Sector.DownQuark} : Finset ℕ) = {0, 2} →
      g Anchor.Sector.DownQuark = dualDim (g Anchor.Sector.UpQuark) →
      g = couplingDimOfSector ∨ g = couplingDimOfSector'

What this page does not claim

This module does not derive the up/down orientation from any internal structure; it proves that no such derivation exists. The coupling dimension is not a measured physical quantity; it is a framework-internal indexing of sectors. No claim is made that the coupling dimension equals any standard model coupling constant value.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND