quarkFlavour_count
plain-language theorem explainer
The theorem states that the finite type of quark flavours has cardinality exactly six. Modelers of mass hierarchies on the phi-ladder cite it to fix the discrete count before ratio derivations. The proof is a one-line decision procedure that evaluates the cardinality directly from the inductive enumeration.
Claim. The finite type of quark flavours has cardinality six: $|QuarkFlavour| = 6$, where the type enumerates the six flavours up, down, strange, charm, bottom and top.
background
The module places six quark flavours on a phi-ladder mass scale, with the explicit count expressed as three generations times two charge types. The inductive type QuarkFlavour is defined by six constructors (up, down, strange, charm, bottom, top) and derives Fintype, DecidableEq and related instances so that its cardinality is computable by decision procedures. This supplies the discrete starting point for subsequent mass-ratio and positivity statements in the same module.
proof idea
The proof is a term-mode one-line wrapper that invokes the decide tactic. The tactic succeeds because the inductive definition of QuarkFlavour derives Fintype, allowing the decision procedure to enumerate the six cases and confirm the equality.
why it matters
The result populates the six_flavours field inside the QuarkMassCert definition, which assembles the full certification of the quark mass hierarchy. It supplies the basic counting step required by the phi-ladder construction in the Recognition Science framework before mass formulas and ratios are introduced. No open questions or scaffolding remain at this level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.