primeDistributionCount
plain-language theorem explainer
The theorem asserts that the inductive type of prime distribution regimes on the J-cost lattice has exactly five elements. A number theorist working inside Recognition Science would cite the count when connecting prime clustering to recognition minima. The proof is a one-line decision procedure that evaluates the Fintype cardinality directly from the five constructors.
Claim. The finite type whose elements are the regimes twin primes, cousin primes, sexy primes, prime gaps and prime clusters has cardinality five: $|P| = 5$ where $P = $ {twin primes, cousin primes, sexy primes, prime gaps, prime clusters}.
background
The module models primes as clustering near J-cost minima on the recognition lattice, with the cost of any recognition event given by its J-cost. The inductive type PrimeDistributionRegime enumerates five regimes: twin primes, cousin primes, sexy primes, prime gaps and prime clusters; these are declared to equal configDim D = 5 at the model level. Upstream, the cost function on a multiplicative recognizer is the derived cost of its comparator on positive ratios, while the cost of a recognition event is the J-cost of its state.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype.card expression. The Fintype instance is derived automatically from the five constructors of PrimeDistributionRegime together with the DecidableEq and BEq instances.
why it matters
The result supplies the five_regimes component of the primeCostCert definition, completing the model-level count inside the Prime Cost Spectrum. It instantiates the module claim that five regimes equal configDim D = 5 and supports the broader link between the prime counting function and incremental J-cost. The module records that the correspondence to zeta zeros remains at hypothesis level pending deeper RS-prime-cost theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.