primeGapCategoryCount
plain-language theorem explainer
The theorem asserts that the inductive type of prime gap categories has exactly five elements. Researchers reformulating Goldbach sums via J-cost pairings cite this count when equating admissible gap types to the five-dimensional configuration space. The proof is a one-line decision procedure that succeeds on the derived Fintype instance for the five-constructor inductive.
Claim. The finite cardinality of the set of prime gap categories equals five, where the categories are the twin, cousin, sexy, quadruplet, and quintuplet gap types.
background
PrimeGapCategory is the inductive type whose five constructors are twin, cousin, sexy, quad, and quintet; it derives DecidableEq, Repr, BEq, and Fintype. The module situates this count inside the RS structural opening for Goldbach: primes are recognition-cost minima on the integer lattice, and Goldbach sums correspond to J-cost pairings that minimise over prime pairs. Upstream results supply the cost function as the J-cost of a recognition event and the equilibria of strain functionals, both of which underwrite the claim that primes realise recognition equilibria.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic succeeds because the inductive definition of PrimeGapCategory automatically derives a Fintype instance whose cardinality is the number of constructors.
why it matters
This theorem supplies the five_gap_types field of the GoldbachRSCert structure, which packages the count together with unit cost and pair symmetry. The module doc-comment states that the five gap categories equal configDim D = 5, furnishing the RS-level structural explanation for Goldbach without proving the conjecture itself. It closes the first of the three enumerated steps in the module's formalisation of the RS account.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.