Masses Mass Genesis Coupling Dimension From Sector Coupling Dim Lepton Eq One

The lepton's coupling dimension

In the Recognition Science framework, a ledger (a discrete record of events) assigns to each particle pattern a coupling dimension, a number that indexes how the pattern participates in the framework's interaction structure. The theorem couplingDim_lepton_eq_one states that any charged, colorless pattern, which the framework identifies as a lepton, has coupling dimension exactly 1. The proof is short: it unfolds the definition of coupling dimension, applies a previously established lemma that routes colorless charged patterns to the lepton sector, and concludes by reflexivity.

The number 1 is not arbitrary. In the framework's geometry, the boundary of a pattern is a sphere, and dimensions come in Poincaré-dual pairs: 0 pairs with 2, while 1 is self-dual. The theorem places the lepton at this self-dual middle dimension. A companion theorem, couplingDim_colored_pair, places the colored up and down quark patterns at the dual extremes 0 and 2. Together they form a certificate that the framework's positive coupling-dimension theory, previously conditional on an abstract map, now holds as a concrete theorem.

What the theorem does not claim is equally important. It does not say that the coupling dimension 1 is derived from the gauge structure; the up/down orientation, which colored sign sits at dimension 0 versus 2, remains a free choice. The framework proves there are exactly two equivariant coupling tables, related by the duality involution, and that no internal datum selects between them. The orientation is a sign convention, not a combinatorial consequence.

The theorem also does not claim that the lepton's coupling dimension determines its mass, or that it predicts any measured value. It is a structural statement about the framework's own indexing of particle patterns, not an empirical claim. The framework's particle masses sit on a separate phi-power ladder, and comparisons against measured values are empirical checks, not consequences of this theorem.

/-- **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 (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 derive the lepton's coupling dimension from gauge structure. It does not predict any measured particle mass or coupling constant. It does not claim that the up/down orientation is fixed by the framework's internal structure.

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: