QuarkFlavour
plain-language theorem explainer
QuarkFlavour enumerates the six standard quark species as an inductive type. Recognition Science researchers modeling the phi-ladder mass hierarchy cite it to ground the finite set of flavors before proving cardinality and mass ratios. The declaration is a direct inductive definition that derives Fintype, DecidableEq and related instances to support later counting and certification steps.
Claim. Let $Q$ be the finite set of quark flavors consisting of the up, down, strange, charm, bottom and top quarks.
background
The module introduces six quark flavours placed on a phi-ladder mass scale, with adjacent-flavour mass ratios treated as coarse structural data. Six equals three generations times two charge types (up-type versus down-type). The inductive definition supplies the base type whose Fintype instance is used to certify the total count and to attach positive mass values via the phi-ladder.
proof idea
The declaration is the inductive definition of the six flavors together with the derived instances DecidableEq, Repr, BEq and Fintype; no separate proof body is required.
why it matters
It supplies the finite carrier set required by the downstream count theorem (Fintype.card QuarkFlavour = 6) and by the QuarkMassCert structure that records the six-flavour count, the three-times-two decomposition, the uniform phi ratio between adjacent masses, and positivity. The definition therefore realizes the six = 3 generations × 2 charge types step inside the Recognition Science phi-ladder construction for quark masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.