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

Fermion

show as:
view Lean formalization →

The Fermion inductive type enumerates the twelve Standard Model fermions by species label. Recognition Science researchers cite this enumeration to index the Z-map, gap function, and phi-ladder mass assignments. The declaration is a direct inductive construction that derives decidable equality, representation, and inhabitedness with no further computation.

claimLet $F$ be the inductive type whose constructors are $d,s,b,u,c,t,e,mu,tau,nu_1,nu_2,nu_3$, corresponding to the six quarks, three charged leptons, and three neutrinos.

background

The RSBridge.Anchor module supplies the core bridge from the recognition framework to particle physics. It defines the Fermion species, the charge-indexed integer $Z_i = q̃^2 + q̃^4$ (plus 4 for quarks), the gap function $F(Z) = ln(1 + Z/phi)/ln(phi)$, and the mass-at-anchor scale. The local theoretical setting is Single Anchor Phenomenology, which asserts that the integrated RG residue at the anchor equals the gap function to tolerance ~1e-6. Upstream results include the scalar coefficient mu in the quadratic projector relation $A^2 = mu A$ and the generation torsion tau taking values 0, 11, 17 for generations 0, 1, 2.

proof idea

The declaration is a direct inductive definition that introduces twelve distinct constructors and attaches deriving instances for DecidableEq, Repr, and Inhabited. No lemmas or tactics are invoked; the structure is primitive.

why it matters in Recognition Science

This definition supplies the indexing set for downstream certificates such as FermionKineticCert (which derives fifteen fermions per generation from five EW sectors times three colors) and SpectralEmergenceCert (which obtains three generations from the D=3 cube geometry). It fills the enumeration step that connects the forced eight-tick octave and D=3 spatial dimensions to the observed fermion spectrum. Parent results include generations_eq_dimension and the structural derivation fermionsPerGeneration_val.

scope and limits

formal statement (Lean)

  34inductive Fermion
  35| d | s | b | u | c | t | e | mu | tau | nu1 | nu2 | nu3
  36deriving DecidableEq, Repr, Inhabited
  37

used by (40)

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

… and 10 more

depends on (4)

Lean names referenced from this declaration's body.