Encyclopedia Masses Masses Mass Genesis Coupling Dimension From Sector Coupling Dimension Cert

ARTICLE 4 claims 4 theorems

Masses Mass Genesis Coupling Dimension From Sector Coupling Dimension Cert

A machine-checked certificate turns a previously assumed symmetry of particle couplings into a proved theorem, while honestly exposing one remaining conventional choice.

Verify this page

The coupling dimension certificate

In the Recognition Science framework, a ledger is a discrete record of events, and each particle sector is assigned a coupling dimension, a number that describes how it interacts. The declaration CouplingDimensionCert is a machine-checked certificate, a formal object that verifies a set of claims about this assignment. Its central result is that a symmetry property, previously taken as an input assumption, is now proved as a theorem from the sector structure.

The property in question is charge-conjugation equivariance. Charge conjugation is a symmetry that swaps a particle with its antiparticle. The certificate proves that when you apply charge conjugation to a pattern, its coupling dimension transforms in a specific dual way: the dimension of the conjugate is the dual dimension of the original. For the colorless lepton sector, this means it sits at the self-dual middle dimension 1. For the colored up and down quark sectors, they occupy the dual extremes 0 and 2, and charge conjugation swaps them. This is all derived from the topology of the pattern, not assumed.

The certificate also proves a sharp limit on what can be derived. There are exactly two possible coupling tables that satisfy the equivariance condition, related by a duality involution. They differ only in which colored charge sign is labeled up versus down. The certificate proves these two are genuinely distinct and that no internal structure can select between them. This remaining freedom is a sign convention, a free choice, not a consequence of the framework's combinatorics.

This matters because it converts a hypothesis into a theorem, and it precisely locates the boundary of what the framework can determine. The coupling dimension is no longer a free parameter; it is fixed by the sector structure up to a single conventional choice. The certificate does not claim to derive the up/down orientation itself, and it does not claim to predict particle masses. It establishes the consistency of the coupling dimension assignment and the exact nature of its remaining freedom.

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 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 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 certificate does not claim to derive the up/down orientation itself; it proves that choice is free. The certificate does not claim to predict particle masses, only to fix the coupling dimension assignment. The certificate does not claim the coupling dimension is unique without qualification; it proves exactly two equivariant tables exist.

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