primeCostCert
plain-language theorem explainer
primeCostCert supplies a concrete witness to the PrimeCostCert structure by populating the regime count and the unit J-cost minimum. A researcher modeling prime distributions through recognition cost would reference this instance when building the five-regime spectrum. The construction is a direct record definition that delegates the cardinality to a decision procedure and the cost zero to an upstream unit lemma.
Claim. The prime cost certificate is the structure asserting that the cardinality of the set of prime distribution regimes equals five and that the J-cost function satisfies $J(1)=0$.
background
Recognition Science models prime distributions via the J-cost function on the recognition lattice, where primes are predicted to cluster at cost minima. The module treats five regimes (twin primes, cousin primes, sexy primes, gaps, clusters) as the configuration dimension D=5 and notes that the correspondence with zeta zeros remains at the model level. The J-cost function measures recognition cost at rational ratios, with the value zero at argument one marking exact lattice alignment.
proof idea
The definition is a one-line record construction. It sets the five_regimes field to the result of primeDistributionCount and the lattice_min field to prime_lattice_minimum.
why it matters
This definition completes the model-level prime cost spectrum by supplying the concrete certificate required for the five-regime structure. It fills the hypothesis interface described in the module documentation, linking J-cost minima to prime clustering predictions without deriving the underlying distribution theorems. It stands ready for deeper RS-prime-cost theory once Zhang-Maynard level results are incorporated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.