BayesianUpdateCert
plain-language theorem explainer
BayesianUpdateCert bundles the non-negativity of J-cost on likelihood ratios with the golden-ratio thresholds for evidence strength. Epistemologists and statisticians modeling information gain would cite the record when certifying that a Bayes factor of phi marks the boundary between null and detectable updates. It is assembled as a structure definition from four sibling lemmas on cost and thresholds.
Claim. A record type whose fields assert that the J-cost of a Bayes factor vanishes when likelihood equals prior (for nonzero prior), remains nonnegative for positive likelihood and prior, that the barely-convincing threshold exceeds 1, and that the moderate-evidence threshold exceeds 2.
background
Recognition Science quantifies Bayesian updates via the J-cost of the likelihood ratio, where J(x) = (x + x^{-1})/2 - 1. The module defines this cost directly on the ratio and imports the upstream result that every recognition event carries nonnegative cost. The local setting predicts that the minimum detectable update occurs at a Bayes factor of phi, with phi squared as the moderate-evidence level, aligning with Kass-Raftery scales.
proof idea
This is a structure definition that packages four properties. The null-cost and nonnegativity fields are supplied by the sibling lemmas bayesFactorCost_at_null and bayesFactorCost_nonneg. The two threshold inequalities are taken from the definitions of bayesFactorThreshold and bayesFactorModerate together with their comparison lemmas.
why it matters
It supplies the certified record instantiated by the downstream cert definition and shown inhabited by cert_inhabited. This closes the structural theorem for Bayesian updates from J-cost, connecting the forcing chain's phi fixed point to empirical evidence thresholds. It touches the open question of whether subjective conviction studies consistently place the convincing threshold inside (1.5, 4.0).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.