cert
plain-language theorem explainer
Packages three structural properties of the domain cost and the canonical threshold into one inhabited certificate for the RS falsifiability master theorem (v3). Anyone citing the 3-sigma falsifiability claim would point here for the concrete witness. The body is a structure instance that wires three already-proved sibling lemmas; no new mathematics is derived.
Claim. There is a certificate asserting: (i) the domain cost vanishes on the diagonal, $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative for positive model and experimental values; (iii) the canonical threshold is strictly positive.
background
This module states the RS Falsifiability Master Theorem v3 as a structural theorem (zero sorry, zero axiom): any measurement outside the RS prediction band at $3\sigma$ falsifies the framework. Named falsifiers include $\Lambda$ outside $(1.88,2.03)$, $\alpha^{-1}$ outside $(137.030,137.039)$, and BTFR slope outside $(3.8,4.2)$.
The certificate type bundles three Prop fields on a domain-level cost comparison between model value $m$ and experimental value $e$. The first field requires the cost to vanish when model equals experiment (off zero). The second requires nonnegativity for positive arguments. The third requires a strictly positive canonical threshold against which residuals are judged.
Upstream, nonnegativity of recognition cost is already known from ObserverForcing: "The cost of any recognition event is non-negative," via $J$-cost nonnegativity on positive states. The present certificate lifts that style of positivity to the domain-cost comparison used by the falsifiability theorem.
proof idea
One-line structure instance. The three fields of RSFalsifiability3Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No tactics, no rewriting, no new proof obligations: the definition is pure assembly of already-established facts into the certificate record.
why it matters
Gives the master falsifiability theorem a single named witness that the cost comparison is a genuine defect measure (zero on match, nonnegative off match) with a positive decision threshold. Without this package, the $3\sigma$ band claims in the module doc would float free of a Lean-checkable cost interface.
In the broader Recognition Science chain this sits on the foundation side: cost positivity traces to $J$-cost uniqueness (T5) and the Recognition Composition Law, while the numerical bands cited in the module ($\alpha^{-1}$ window, etc.) are the empirical face of the same framework. No downstream consumers are recorded yet; the natural parent is the inhabitedness lemma and any top-level falsifiability theorem that consumes the certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.