PrimeCostCert
plain-language theorem explainer
PrimeCostCert packages the claim of exactly five prime distribution regimes on the recognition lattice together with the statement that J-cost vanishes at unity. Researchers modeling prime clustering via J-cost minima cite this structure to record the five-regime hypothesis at model level. The declaration is a bare structure definition whose two fields directly assert the cardinality and the lattice minimum.
Claim. A structure whose fields assert that the set of prime distribution regimes has cardinality five and that the J-cost function satisfies J(1) = 0.
background
The module links primes to J-cost minima on the recognition lattice, with the Riemann zeta zeros interpreted as cost zeros and the prime counting function receiving an RS reading in which each prime contributes an incremental J-cost of order J(1 + log n / n). PrimeDistributionRegime is the inductive type whose five constructors are twinPrimes, cousinPrimes, sexyPrimes, primeGaps and primeClusters; the module states that these five regimes equal configDim D = 5. The surrounding note records that the construction remains at MODEL level as a hypothesis whose full justification would require Zhang-Maynard or deeper RS-prime-cost theory.
proof idea
The declaration is a structure definition that introduces a record type with exactly two fields; the first records the Fintype cardinality of the regime inductive and the second records the J-cost evaluation at one. No lemmas or tactics are invoked.
why it matters
The structure supplies the type instantiated by the downstream primeCostCert witness, thereby closing the model-level hypothesis inside the prime cost spectrum module. It encodes the five-regime prediction that arises from configDim D = 5 and sits inside the broader Recognition Science program that derives spatial dimension D = 3 from the eight-tick octave. The module leaves open the derivation from the forcing chain or from Zhang-Maynard-type gap results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.