Masses Mass Genesis Topology To Sector

Reading the pattern's labels

In the Recognition Science framework, a particle's identity is not a name attached to it. It is a structure that can be read off. The module called TopologyToSector closes the surface for this reading: it proves that the three canonical functions sectorOf, rungOf, and ZOf (which give the particle's sector, its mass rung, and a charge-related integer) are all computed from the primitive topology of a light pattern, not from any stored label field. The stored labels remain as audit slots only, a check against older values.

The core theorems are simple equalities: sectorOf ψ = sectorFromTopology ψ.topology, and the same for rung and Z. These are proved by reflexivity, meaning the definitions align exactly. The module then derives the sector's behavior under charge conjugation. A colorless pattern (one with zero loop rank) and its charge conjugate both map to the Lepton sector, so the lepton is C-invariant. A colored pattern with positive charge skew maps to Up, its conjugate with negative skew maps to Down, so charge conjugation swaps the colored sectors. The orbit structure is {Lepton} ⊔ {Up, Down}, one fixed point and one 2-orbit, matching the boundary duality orbits {1} ⊔ {0, 2}.

The module also provides canonical first-generation topologies and proves their sector and Z values: the lepton with charge skew -6, spin 1, torsion 0, active edges 1 gives Z = 1332; the up quark with skew 4, spin 3 gives Z = 276; the down quark with skew -2 gives Z = 24. These are concrete checks that the topology-to-sector map produces the expected Standard Model family labels. The construction is still a compact topology model, not the full load-to-mass law.

What this changes: the framework's particle labels are now derived, not assumed. The lepton's charge-conjugation invariance, which the coupling-dimension theory previously took as a hypothesis, is here a theorem about the routing of sectorFromTopology. The colored pair's swap is also derived. The module bundles these into a certificate, topologyToSectorCert, that downstream proofs can use as a single trusted interface.

theorem sectorOf_eq_sectorFromTopology (ψ : LightPattern Λ) :
    sectorOf ψ = sectorFromTopology ψ.topology := rfl

theorem rungOf_eq_rungFromTopology (ψ : LightPattern Λ) :
    rungOf ψ = rungFromTopology ψ.topology := rfl

theorem ZOf_eq_ZFromTopology (ψ : LightPattern Λ) :
    ZOf ψ = ZFromTopology ψ.topology := rfl

/-- **THEOREM (the colorless sector is charge-conjugation invariant).** A colorless pattern
    (`q3LoopRank = 0`, `chargeSkew ≠ 0`) and its charge conjugate (same `q3LoopRank`, negated
    `chargeSkew`) both map to the Lepton sector. The sector map is therefore C-INVARIANT on the
    colorless locus — DERIVING the lepton's charge-conjugation invariance from the routing of
    `sectorFromTopology` rather than assuming it. -/
theorem colorless_sector_C_invariant
    (T Tc : PatternTopology)
    (hloop : T.q3LoopRank = 0) (hQ : T.chargeSkew ≠ 0)
    (hcLoop : Tc.q3LoopRank = 0) (hcQ : Tc.chargeSkew = - T.chargeSkew) :
    sectorFromTopology T = sectorFromTopology Tc ∧
      sectorFromTopology T = Anchor.Sector.Lepton := by
  have hTcQ : Tc.chargeSkew ≠ 0 := by rw [hcQ]; exact neg_ne_zero.mpr hQ
  rw [sectorFromTopology_lepton T hQ hloop, sectorFromTopology_lepton Tc hTcQ hcLoop]
  exact ⟨rfl, rfl⟩

/-- **THEOREM (charge conjugation swaps the colored sectors).** A colored pattern with positive
    skew (`q3LoopRank ≠ 0`, `chargeSkew > 0` → Up) and its charge conjugate (negated skew `< 0`
    → Down) map to DIFFERENT sectors: Up ↦ Down. So C is a 2-orbit `{Up, Down}` on the colored
    sectors, not a fixed point — matching the 2-orbit `{0,2}` of the boundary duality. -/
theorem colored_sector_C_swaps
    (T Tc : PatternTopology)
    (hloop : T.q3LoopRank ≠ 0) (hpos : 0 < T.chargeSkew)
    (hcLoop : Tc.q3LoopRank ≠ 0) (hcQ : Tc.chargeSkew = - T.chargeSkew) :
    sectorFromTopology T = Anchor.Sector.UpQuark ∧
      sectorFromTopology Tc = Anchor.Sector.DownQuark := by
  have hQ : T.chargeSkew ≠ 0 := hpos.ne'
  have hTcQ : Tc.chargeSkew ≠ 0 := by rw [hcQ]; exact neg_ne_zero.mpr hQ
  have hcnpos : ¬ 0 < Tc.chargeSkew := by rw [hcQ]; omega
  exact ⟨sectorFromTopology_up T hQ hloop hpos,
         sectorFromTopology_down Tc hTcQ hcLoop hcnpos⟩

theorem canonical_first_generation_Z_values :
    ZFromTopology (canonicalLeptonTopology (-6) 1 0 1) = 1332 ∧
    ZFromTopology (canonicalUpTopology 4 3 0 1) = 276 ∧
    ZFromTopology (canonicalDownTopology (-2) 3 0 1) = 24 :=
  ⟨canonical_lepton_Z, canonical_up_Z, canonical_down_Z⟩

What this page does not claim

This module does not prove the final load-to-mass-law identity. The stored label fields in PatternTopology are not the source of truth; they are audit slots only. The construction is a compact topology model, not a complete physical derivation of all particle properties.

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/TopologyToSector.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: