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

Fermion

show as:
view Lean formalization →

The declaration enumerates the twelve Standard Model fermion species as an inductive type in the Recognition Science bridge to masses. Researchers mapping particle masses to the phi-ladder via ZOf and gap functions cite it when fixing the species list for anchor-scale calculations. The definition is a direct inductive enumeration that automatically derives decidable equality, representation, and inhabited structure.

claimLet Fermion be the inductive type whose constructors are the twelve species $d,s,b,u,c,t,e,mu,tau,nu_1,nu_2,nu_3$, equipped with decidable equality, a representation instance, and an inhabited instance.

background

The RSBridge.Anchor module supplies the core bridge between the recognition framework and particle physics. It introduces the type Fermion for the twelve Standard Model species (six quarks, three charged leptons, three neutrinos), the charge-indexed integer map ZOf, the display function gap(F) = ln(1 + Z/phi)/ln(phi), and the anchor-scale massAtAnchor. The module states that gap(ZOf i) is the closed-form value claimed to equal the integrated RG residue at the anchor scale mu-star, with tolerance approximately 1e-6. Upstream, the definition re-uses the mu projector coefficient from Cost.Ndim.Projector and the generation torsion tau from Masses.Anchor, together with the SMVerification.Fermion enumeration.

proof idea

The declaration is an inductive definition that directly lists the twelve constructors and derives DecidableEq, Repr, and Inhabited by the deriving clause. No tactics or lemmas are applied; the structure is generated automatically by Lean.

why it matters in Recognition Science

This enumeration is the species index used by SpectralEmergenceCert to obtain three generations from D = 3 and by FermionKineticCert to certify that fermion masses at successive phi-ladder rungs differ by exact factors of phi. It therefore supplies the concrete list required for the single-anchor phenomenology claim that integrated RG residues equal gap(ZOf i). The definition closes the interface between the Recognition Science forcing chain (T8 fixing D = 3) and the mass formula yardstick * phi^(rung - 8 + gap(Z)).

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.