RSFalsifiability3Cert
plain-language theorem explainer
Certificate bundling three structural properties for RS falsifiability v3: diagonal domain-cost vanishes off zero, domain-cost is nonnegative on positive arguments, and the canonical threshold is strictly positive. Downstream code builds a concrete inhabitant and proves the type is nonempty. Pure structure definition; no proof obligations live here.
Claim. A certificate is a triple of properties: (i) for every real $r \neq 0$, the domain cost satisfies $\mathrm{domainCost}(r,r)=0$; (ii) for all $m,e>0$, $\mathrm{domainCost}(m,e)\ge 0$; (iii) the canonical threshold $T$ obeys $T>0$.
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 external falsifiers include $\Lambda$ outside $(1.88,2.03)$, $\alpha^{-1}$ outside $(137.030,137.039)$, and BTFR slope outside $(3.8,4.2)$.
Domain cost is the module-local cost functional on pairs of reals (model and evidence scales). The diagonal identity $\mathrm{domainCost}(r,r)=0$ encodes perfect match; nonnegativity for positive arguments is the cost axiom inherited from the recognition $J$-cost. Upstream, ObserverForcing proves that every recognition event has nonnegative cost via $J$-cost nonnegativity on positive states. The canonical threshold is the positive cutoff against which residual cost is compared when declaring a band violation.
proof idea
No proof body: this is a structure declaration. The three fields are pure propositions (diagonal vanishing of domain cost, nonnegativity on the positive quadrant, positivity of the canonical threshold). Inhabitation is deferred to the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives a single named type for the minimal cost-and-threshold package that the falsifiability master theorem needs. Downstream, cert assembles a concrete value of this structure from the three sibling lemmas, and cert_inhabited records Nonempty of the certificate type. That inhabitation is the structural half of the claim that RS is empirically falsifiable: once residual domain cost can be compared to a positive threshold, a $3\sigma$ band miss is a hard refute. Ties to the foundation layer (cost nonnegativity from the $J$-cost / recognition-event calculus) rather than to a specific forcing step T0–T8, but supports the same empirical band claims used for $\alpha^{-1}$ and related constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.