PrimeDistributionRegime
plain-language theorem explainer
The inductive type enumerates the five canonical regimes of prime clustering that Recognition Science associates with J-cost minima on the recognition lattice. A mathematician modeling prime distributions under the RS framework would cite this enumeration when establishing that exactly five regimes exist at configDim D=5. It is introduced as a plain inductive definition deriving Fintype to enable direct cardinality computations.
Claim. Let $R$ be the set of prime distribution regimes defined inductively by the five constructors corresponding to twin primes, cousin primes, sexy primes, prime gaps, and prime clusters, equipped with decidable equality and finite type structure.
background
Recognition Science predicts that prime numbers cluster near J-cost minima on the recognition lattice, where the J-cost function (imported from the Cost module) measures recognition cost with zeros corresponding to Riemann zeta function zeros. The prime counting function receives an RS interpretation in which each prime contributes J-cost of order J(1 + log(n)/n). This module operates at the model level as a hypothesis, positing that five canonical regimes realize configDim D=5.
proof idea
Inductive definition with five explicit constructors, deriving DecidableEq, Repr, BEq, and Fintype to support finite cardinality calculations.
why it matters
This definition supplies the five regimes whose cardinality is asserted to be 5 in the downstream structure PrimeCostCert (which also requires Jcost 1 = 0) and is used by the theorem primeDistributionCount that proves the cardinality equals 5 by decision. It realizes the configDim D=5 prediction for prime distributions in the RS framework, linking primes to J-cost minima; the actual verification remains a hypothesis pending Zhang-Maynard or deeper RS-prime-cost theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.