prime_lattice_minimum
plain-language theorem explainer
The J-cost function vanishes at argument one, placing a prime exactly at a recognition lattice minimum. Researchers deriving prime spectra from Recognition Science would cite this as the base lattice point for cost minima. The result is a direct appeal to the unit case of the J-cost definition.
Claim. $J(1) = 0$, where $J(x) = (x-1)^2/(2x)$ is the recognition cost at unit ratio.
background
The module develops the prime cost spectrum by mapping primes to J-cost minima on the recognition lattice. J-cost is defined as $J(x) = (x-1)^2/(2x)$, which is zero precisely at $x=1$ and positive elsewhere. The local setting treats five prime distribution regimes (twin, cousin, sexy primes, gaps, clusters) as a five-dimensional configuration space, with the Riemann zeta zeros interpreted as cost zeros and the prime counting function linked to incremental J-cost additions of the form $J(1 + log(n)/n)$.
proof idea
One-line wrapper that applies the Jcost_unit0 lemma, which itself reduces to simp on the Jcost definition.
why it matters
This supplies the lattice_min field of the PrimeCostCert definition, which packages the five prime regimes together with the zero-cost point. It anchors the hypothesis that primes sit at J-cost minima, consistent with the Recognition Composition Law and the forcing chain from T5 (J-uniqueness) through T8 (D=3). The module notes that full linkage to Zhang-Maynard-type results remains at the MODEL level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.