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

ARTICLE 4 claims 4 theorems

Masses Mass Genesis Coupling Dimension From Sector Orientation Freedom Cert

A machine-checked proof that particle mass generation leaves exactly one free choice, the labeling of up versus down, and that no internal structure can decide it.

Verify this page

The orientation certificate

In the Recognition Science account, the generation of particle masses begins with a discrete record of recognition events, a ledger. The framework assigns each particle sector a coupling dimension, a small whole number that indexes how that sector participates in the mass-generating interaction. The declaration OrientationFreedomCert is a machine-checked certificate, a bundled collection of formal theorems, that pins down exactly how much freedom remains in that assignment.

The certificate proves, in the framework's machine-checked library, that the coupling dimension is fully determined by the particle's sector, except for a single conventional choice. The colorless Lepton and Electroweak sectors sit at the self-dual middle dimension 1. The colored Up and Down quark sectors sit at the dual extremes, 0 and 2. Charge conjugation, the operation that swaps a particle with its antiparticle, must map the coupling dimension of one to the dual of the other. The certificate shows this equivariance holds as a theorem, not an assumption, for both possible assignments of which colored sector gets 0 and which gets 2.

The two assignments are genuinely distinct, related by the duality involution, and the certificate proves they are the only two possible equivariant coupling tables. This is the sharpened obstruction: the framework's internal structure, including the gauge structure that realizes weak hypercharge, provably cannot select between them. The choice of which colored charge sign is labeled up is therefore a free Z/2, a sign convention, not a combinatorial consequence.

What the certificate does not claim is equally important. It does not claim to derive the up/down orientation from deeper principles; it proves that no such derivation exists within the framework. It does not claim to predict the numerical values of particle masses. It establishes the structure of the coupling dimension table and the exact nature of its one residual freedom, leaving the orientation as an external datum.

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 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 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 derive the up/down orientation from deeper principles. The certificate does not predict the numerical values of particle masses. The certificate does not claim the coupling dimension table is unique without the orientation choice.

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