RSSummary3Cert
plain-language theorem explainer
A certificate structure that packages three summary claims for Recognition Science: the domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is strictly positive. Downstream code cites it to exhibit a concrete inhabited summary witness. There is no proof body; the structure is a pure Prop bundle filled by sibling lemmas.
Claim. A certificate is a triple of assertions: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
This module is the Plan v7 structural summary of Recognition Science: one functional equation forces $J(x)=(x+x^{-1})/2-1$, hence $\phi$, the gap-45 ladder, $D=3$, and the derived constants, with zero sorry and zero axioms in the certificate layer.
The domain cost is the real-valued cost assigned to a matched pair of positive scales (measure and event). It is the local avatar of the global $J$-cost used throughout the foundation: $J$ is uniquely fixed by the Recognition Composition Law and is nonnegative with a unique minimum at the identity $x=1$. The canonical threshold is the positive cutoff used to separate trivial from nontrivial recognition events in the summary.
Upstream, ObserverForcing already records that every recognition event has nonnegative cost via $J$-cost nonnegativity. The three fields here restate the corresponding domain-level facts needed for a single inhabited summary object.
proof idea
No proof: the declaration is a structure whose fields are propositions. Inhabitation is deferred to the sibling definition cert, which fills the three fields by the already-proved lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The nonempty witness is then cert_inhabited : Nonempty RSSummary3Cert.
why it matters
The structure is the typed interface for the Recognition Science Complete Summary Certificate. Downstream, cert builds a concrete inhabitant and cert_inhabited records that the type is nonempty, closing the structural theorem advertised in the module header (0 sorry, 0 axiom).
In the forcing chain this sits after T5 ($J$-uniqueness) and the nonnegativity of recognition cost: the diagonal vanishing and positivity of the threshold are the minimal numeric hygiene needed before quoting derived constants, the $\phi$-ladder mass formula, or the empirical RS_PASS list. It does not itself force $\phi$, $D=3$, or the eight-tick octave; it only certifies the cost/threshold fragment of the summary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.