Encyclopedia Masses Masses Mass Genesis Coupling Dimension From Sector Coupling Dim Equivariant

ARTICLE 4 claims 4 theorems

Masses Mass Genesis Coupling Dimension From Sector Coupling Dim Equivariant

A machine-checked theorem pins down where each particle family couples in the framework's geometry, and proves that one remaining choice is a genuine convention, not a hidden assumption.

Verify this page

The coupling dimension

In particle physics, a coupling constant measures how strongly a particle interacts with a force. The Recognition Science framework replaces that single number with a coupling dimension: a small whole number, 0, 1, or 2, that records where on a geometric boundary a particle family sits. The declaration couplingDim_equivariant is a machine-checked theorem that fixes this dimension for every known particle family, and proves that the assignment respects charge conjugation, the symmetry that swaps particles with their antiparticles.

The framework's ledger, a discrete record of recognition events, organizes particles into sectors. The theorem assigns the colorless Lepton and Electroweak sectors to dimension 1, the self-dual middle of the boundary. The colored Up quark sits at dimension 0, and its charge conjugate, the Down quark, at dimension 2. The proof derives this from the sector structure, so what was once an assumption is now a proved consequence. The theorem states that applying charge conjugation to any charged pattern sends its coupling dimension to the dual dimension, swapping 0 with 2 and leaving 1 fixed.

The theorem also proves a limit. The assignment of Up to 0 and Down to 2 is one of exactly two possible tables; the opposite choice, Up at 2 and Down at 0, works just as well. The framework's library proves that no internal structure can decide between them. Which colored sign is called "up" is a convention, a free choice, not a consequence of the geometry. This is the sharpest honest result: the framework fixes the coupling dimension up to one binary label, and proves that the label cannot be derived.

THEOREM couplingDim_lepton_eq_one · IndisputableMonolith/Masses/MassGenesis/CouplingDimensionFromSector.lean
couplingDim_lepton_eq_one · IndisputableMonolith/Masses/MassGenesis/CouplingDimensionFromSector.lean:112 
/-- **THEOREM (lepton couples at the self-dual middle dimension `1`, concretely).** A colorless
    charged pattern couples at `1` — the Poincaré-self-dual middle dimension of the boundary
    sphere. No assumption: derived from `sectorFromTopology_lepton`. -/
theorem couplingDim_lepton_eq_one (T : PatternTopology)
    (hloop : T.q3LoopRank = 0) (hQ : T.chargeSkew ≠ 0) :
    couplingDimOfTopology T = 1 := by
  unfold couplingDimOfTopology
  rw [sectorFromTopology_lepton T hQ hloop]
  rfl
THEOREM couplingDim_colored_pair · IndisputableMonolith/Masses/MassGenesis/CouplingDimensionFromSector.lean
couplingDim_colored_pair · IndisputableMonolith/Masses/MassGenesis/CouplingDimensionFromSector.lean:122 
/-- **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 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]

What this page does not claim

The theorem does not derive the numerical value of any coupling constant, only the dimension index. The theorem does not claim that the up/down orientation is fixed by any internal structure; it proves the opposite. The theorem does not cover neutral patterns, which have zero charge skew and are excluded from its hypotheses.

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