cert_inhabited
plain-language theorem explainer
Researchers modeling information gain via J-cost in Bayesian updates would cite this result to confirm a certificate exists meeting the zero-at-null, nonnegativity, and threshold conditions. It establishes that the BayesianUpdateCert structure is inhabited. The proof is a direct term construction supplying the cert witness.
Claim. There exists a structure $C$ such that the Bayes factor cost vanishes whenever likelihood equals prior, the cost is nonnegative for positive likelihoods and priors, the Bayes factor threshold exceeds one, and the moderate evidence threshold exceeds two.
background
The module formalizes Bayesian updating with posterior proportional to likelihood times prior and information gain via KL-divergence. J-cost is the recognition cost function imported from the Cost module. BayesianUpdateCert is the structure bundling four properties: cost_at_null (vanishes at null), cost_nonneg, threshold_gt_one, and moderate_gt_two. The local setting predicts that the minimum detectable update corresponds to J(φ) ≈ 0.118, with Bayes factors φ and φ² as thresholds matching Kass-Raftery scales. Upstream, the Statistics inductive type from SpinStatistics distinguishes fermiDirac and boseEinstein cases.
proof idea
The proof is a term-mode construction that directly applies the cert constructor to witness Nonempty BayesianUpdateCert.
why it matters
This declaration completes the structural theorem for Bayesian updates from J-cost, as declared in the module documentation with zero sorrys. It grounds the RS prediction linking J(φ) to Bayes factor thresholds φ and φ², connecting to J-uniqueness and the phi fixed point in the forcing chain. The module falsifier remains open: any study showing convincing evidence thresholds consistently outside (1.5, 4.0).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.