cert
The definition assembles a structure certifying that the J-cost Bayes factor satisfies zero cost at the null, non-negativity for positive arguments, threshold exceeding one, and moderate evidence exceeding two. Statisticians modeling information gain in belief revision would cite it to confirm alignment with phi-based thresholds. It is assembled by direct assignment of four pre-proven lemmas on the cost function properties.
claimLet $B(l,p)$ be the Bayes factor cost derived from the J-function on the likelihood ratio $l/p$. The certificate asserts $B(p,p)=0$ for all $p≠0$, $B(l,p)≥0$ whenever $l>0$ and $p>0$, the threshold $t>1$, and the moderate threshold $m>2$.
background
The module treats Bayesian updating as posterior proportional to likelihood times prior, with KL-divergence measuring information gain. Recognition Science predicts the minimum detectable update occurs at J-cost J(φ)≈0.118, yielding Bayes factor B=φ≈1.618 as the barely-convincing threshold and B=φ²≈2.618 as moderate evidence, consistent with Kass-Raftery standards for positive evidence. The J-cost itself is the recognition function J(x)=(x+x^{-1})/2-1, and upstream results establish that all recognition-event costs are non-negative.
proof idea
The definition constructs the structure by direct field assignment: cost-at-null to the theorem proving B(p,p)=0, non-negativity to the theorem proving B(l,p)≥0 via J-cost non-negativity on the ratio, threshold-greater-than-one to the one-less-than-phi lemma, and moderate-greater-than-two to the phi-squared-bounds lemma. No further tactics or reductions occur.
why it matters in Recognition Science
This supplies the central certificate completing the structural theorem for Bayesian updates from J-cost, confirming the phi thresholds match required detectability conditions. It links the non-negativity of recognition costs to empirical Bayes-factor conventions and closes the module's zero-sorry claim. The module falsifier states that any study finding convincing-evidence thresholds consistently outside (1.5,4.0) would challenge the prediction.
scope and limits
- Does not derive the explicit form of the Bayes factor cost function.
- Does not compute numerical costs for concrete likelihood ratios.
- Does not address sequential or multi-observation updates.
- Does not prove convergence of the posterior under repeated updates.
formal statement (Lean)
76noncomputable def cert : BayesianUpdateCert where
77 cost_at_null := bayesFactorCost_at_null
proof body
Definition body.
78 cost_nonneg := bayesFactorCost_nonneg
79 threshold_gt_one := bayesFactorThreshold_gt_one
80 moderate_gt_two := bayesFactorModerate_gt_two
81