RSForcingChain005Cert
plain-language theorem explainer
Certificate structure bundling three structural facts for Foundation module 5 of the RS forcing chain: diagonal vanishing of domain cost, non-negativity of domain cost on positive arguments, and positivity of the canonical threshold. Downstream code cites the inhabited instance rather than the bare structure. Pure definition: field types are propositions, no proof body.
Claim. A forcing-chain certificate for module 5 is a triple of properties: (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
Module 5 sits in the RS forcing chain T0–T8, marked as a structural theorem layer with zero sorry and zero axioms. The local objects are a real-valued domain cost on pairs $(m,e)$ and a canonical threshold scalar used as a positivity gate.
Domain cost is the module-level cost functional whose diagonal vanishes and whose values stay nonnegative on the positive quadrant. That nonnegativity mirrors the upstream recognition-event fact that every event cost is nonnegative, proved there by reducing to nonnegativity of the J-cost on positive states.
The certificate is only a packaging type: it names the three propositions that later definitions must discharge, without computing the cost or the threshold itself.
proof idea
No proof: this is a structure declaration whose three fields are proposition-typed. 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 module 5 a single named certificate type so the forcing-chain layer can expose diagonal vanishing, cost nonnegativity, and threshold positivity as one inhabited bundle. Immediate consumers are the concrete witness cert and the theorem cert_inhabited that records Nonempty of the structure.
In the broader RS picture this is bookkeeping for the structural half of the T0–T8 chain (J-uniqueness, $\varphi$ fixed point, eight-tick octave, $D=3$), not a derivation of those landmarks. It keeps cost and threshold hypotheses explicit and reusable without scattering three separate lemmas at every call site.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.