GoldbachRSCert
plain-language theorem explainer
GoldbachRSCert packages three Recognition Science properties into a certificate for Goldbach-type prime sums: exactly five enumerated prime gap categories, vanishing J-cost at unit scale, and inversion symmetry of the J-cost function. Number theorists examining conjectures through lattice cost minimization would cite the certificate as the formal RS interface layer. The declaration is a bare structure definition with no lemmas or computational steps.
Claim. A structure asserting that the cardinality of the set of prime gap categories equals five, that the J-cost of unity is zero, and that the J-cost function satisfies $J(r)=J(r^{-1})$ for every positive real $r$.
background
PrimeGapCategory is the inductive enumeration of five gap classes (twin, cousin, sexy, quad, quintet) whose cardinality is fixed at five. Jcost is the recognition-cost function imported from the Cost module; it assigns a non-negative real to each positive real scale and satisfies the Recognition Composition Law. The module treats primes as J-cost minima on the integer lattice and frames Goldbach as the existence of pairs whose J-costs are equal or opposite.
proof idea
The declaration is a bare structure definition that directly records the three fields with no lemmas applied and no tactics invoked.
why it matters
The structure supplies the type for the downstream goldbachRSCert definition, which instantiates the certificate via primeGapCategoryCount, prime_unit_cost and prime_pair_symmetric. It supplies the RS structural opening for Goldbach, recording the five gap categories as configDim D=5, while the module explicitly states that a full proof still requires Zhang-Maynard plus Chen axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.