prime_unit_cost
plain-language theorem explainer
The theorem states that the J-cost of the unit ratio is zero, establishing the base equilibrium for primes as recognition minima on the integer lattice. Researchers deriving Goldbach decompositions from Recognition Science would cite it when populating the unit_cost field of a structural certificate. The proof is a direct one-line application of the Jcost_unit0 lemma.
Claim. The J-cost function satisfies $J(1) = 0$, where $J(x) = (x-1)^2/(2x)$ for positive real $x$.
background
In the GoldbachFromRS module, primes are recognition-cost minima on the integer lattice, and Goldbach corresponds to pairs of primes with equal or opposite J-costs. The J-cost arises from the multiplicative recognizer as the derived cost of its comparator, equivalently the cost of any recognition event; upstream Jcost_unit0 records that this cost vanishes at unity by direct simplification of the squared-ratio definition. The module frames the result as the structural base case for cost pairings, noting that five prime-gap categories correspond to configDim D = 5 but that a full Goldbach proof still requires external number-theoretic axioms.
proof idea
The proof is a one-line wrapper that applies the Jcost_unit0 lemma from the Cost module (itself obtained by simp on the Jcost definition).
why it matters
This supplies the unit_cost component of the goldbachRSCert definition, which assembles the five-gap count, unit cost, and pair symmetry into the RS certificate for even-number prime sums. It anchors the framework's view of primes as J-cost equilibria, consistent with the Recognition Composition Law and the T5 J-uniqueness step. The module treats the result as the opening move toward a structural explanation rather than a complete proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.