ReciprocitySymCert
plain-language theorem explainer
Certificate structure that packages three algebraic conditions witnessing reciprocity symmetry of the recognition domain cost: vanishing self-comparison cost, non-negativity off the diagonal, and a strictly positive canonical threshold. Anyone assembling or discharging the reciprocity-symmetry witness cites this type. Pure structure definition; no proof body.
Claim. A reciprocity-symmetry certificate is a record of three properties: (i) for every nonzero real $r$, the domain cost of comparing $r$ with itself is zero; (ii) for all positive reals $m$ and $e$, the domain cost of comparing $m$ with $e$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module states the reciprocity symmetry of Recognition Science: $J(x)=J(1/x)$ for all $x>0$, equivalently that the cost of comparing $a$ to $b$ equals the cost of comparing $b$ to $a$. That symmetry is the structural constraint that uniquely fixes the J-cost (the T5 uniqueness step of the forcing chain).
Here the comparison cost is packaged as a two-argument domain cost on reals. Self-comparison must sit at the J-minimum (cost zero when the two arguments agree and are nonzero). Off the diagonal the cost stays nonnegative, matching the upstream fact that every recognition-event cost is nonnegative via $J$-cost non-negativity. A separate positive canonical threshold supplies the scale against which reciprocity is certified.
The local status line marks the reciprocity package as a structural theorem layer (zero sorry, zero axiom), of which this certificate type is the interface.
proof idea
No proof: this is a structure declaration whose three fields are propositions. Inhabitation is deferred to the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and to the one-line nonempty theorem that wraps that witness.
why it matters
Gives the typed interface for the reciprocity-symmetry certificate used by the module's concrete witness and by the nonempty theorem that exposes it. Downstream, those two declarations discharge the structure and close the local reciprocity package.
In the broader framework this sits under the reciprocity law that forces $J(x)=J(1/x)$ and thereby pins the unique J-cost of the forcing chain (T5), the same cost that enters the Recognition Composition Law. Without a certificate type of this shape, later foundation lemmas cannot cite a single inhabited object guaranteeing zero self-cost, non-negativity, and a positive threshold together.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.