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

Quark

show as:
view Lean formalization →

The six standard model quark flavors are enumerated as an inductive type with decidable equality and finite cardinality six. Recognition Science modelers cite this enumeration to link the particle content to the six faces of a three-dimensional cube. The declaration is a direct inductive definition with six constructors that automatically derives the finite type instance.

claimThe set of quark flavors is the finite set $Q = {u, d, s, c, b, t}$ equipped with decidable equality and cardinality six.

background

The CubeFaceUniversality module establishes that the number 6 equals the face count of the 3-cube via the Euler characteristic $V - E + F = 8 - 12 + 6 = 2$. The HasCubeFaceCount predicate asserts that a type has cardinality exactly 6, and the Quark inductive type supplies one instance of this count. The module collects parallel 6-fold structures across domains, all attributed to spatial dimension $D = 3$.

proof idea

This is an inductive definition with six constructors. The deriving clauses for DecidableEq, Repr, BEq, and Fintype generate the required instances automatically, so that downstream theorems obtain the cardinality by unfolding HasCubeFaceCount and deciding the equality.

why it matters in Recognition Science

This definition supplies the quark enumeration required by CubeFaceUniversalityCert and the theorems quark_has_6 and quark_lepton_sum. It realizes the T8 step of the forcing chain by fixing $D = 3$, which forces the face count to 6. The structure appears in fermion counts and mass ladder derivations downstream in BaselineDerivation and QuarkVerification modules.

scope and limits

formal statement (Lean)

  31inductive Quark where
  32  | up | down | strange | charm | bottom | top
  33  deriving DecidableEq, Repr, BEq, Fintype
  34

used by (33)

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

… and 3 more