goldbachRSCert
plain-language theorem explainer
The goldbachRSCert definition supplies an explicit witness to the GoldbachRSCert structure by packaging the five prime gap categories, the zero unit J-cost, and the inversion symmetry of J-cost. A researcher examining Recognition Science accounts of arithmetic would cite this as the formal carrier for the structural Goldbach observation. The construction is a direct record assignment of three module-local theorems into the structure fields.
Claim. Let GoldbachRSCert be the structure whose fields assert that the set of prime gap categories has cardinality five, that the J-cost of the unit ratio equals zero, and that J-cost is invariant under inversion for every positive real argument. The term goldbachRSCert is the explicit term of this structure obtained by supplying the gap-category count, the unit-cost theorem, and the symmetry theorem.
background
In Recognition Science the J-cost function J(r) quantifies the recognition cost of a positive real ratio r and obeys the symmetry J(r) = J(r^{-1}) together with the normalization J(1) = 0. PrimeGapCategory is the finite type enumerating the five admissible gap configurations between consecutive primes (twin, cousin, sexy, prime quad, prime quintet), which the module identifies with configDim D = 5. The GoldbachFromRS module develops the structural link between Goldbach sums and minimal J-cost pairings on the integer lattice, treating primes as recognition equilibria.
proof idea
The definition constructs the GoldbachRSCert record by direct field assignment: five_gap_types receives the value of primeGapCategoryCount, unit_cost receives the value of prime_unit_cost, and pair_symmetric receives the value of prime_pair_symmetric. No tactics or reductions are applied; the term is simply the structure literal whose three fields are the three sibling theorems.
why it matters
This definition supplies the concrete RS witness for the Goldbach structural opening stated in the module documentation. It encodes the observation that five gap categories arise from the D = 5 configuration dimension and that J-cost symmetry explains prime-pair formation. The declaration closes the basic formalization layer in the GoldbachFromRS module and stands ready for any later derivation that would invoke GoldbachRSCert as a hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.