pith. machine review for the scientific record. sign in
inductive definition def or abbrev high

Sector

show as:
view Lean formalization →

The inductive type enumerating the four sectors for mass calculations in Recognition Science: leptons, up quarks, down quarks, and electroweak interactions. Mass formula derivations cite this when assigning sector-specific exponents from cube edge counts. It is introduced as a simple inductive definition with four cases and decidable equality.

claimLet $S$ be the inductive type whose four constructors are the lepton sector, up-quark sector, down-quark sector, and electroweak sector.

background

The Masses.Anchor module centralizes parameter-free constants derived from cube geometry in three dimensions. Total edges equal twelve, passive edges eleven, wallpaper groups seventeen, and active edges per tick one. The sector type labels the four cases for which powers of two and phi-exponent offsets are computed separately, as listed in the module table for B_pow and r0 formulas.

proof idea

Inductive definition with four constructors, deriving DecidableEq and Repr. No lemmas or tactics are applied; the declaration directly enumerates the sectors required by the cube geometry formulas.

why it matters in Recognition Science

This type supplies the domain for B_pow and r0 that enter the yardstick in the mass formula. It feeds the totalCost_nonneg theorem in the QRFT Lagrangian skeleton and the SpectralSector decomposition. It realizes the D equals three spatial dimensions from the forcing chain and the cube geometry step in the derivation chain.

scope and limits

formal statement (Lean)

  67inductive Sector | Lepton | UpQuark | DownQuark | Electroweak
  68  deriving DecidableEq, Repr
  69
  70/-! ## Sector Constants — DERIVED from Cube Geometry -/
  71
  72/-- Derived powers of two for each sector.
  73    These are NOT arbitrary—they come from cube edge counting. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (14)

Lean names referenced from this declaration's body.