bayesFactorCost
plain-language theorem explainer
The definition sets the cost of a Bayesian update to the J-cost of the likelihood ratio. Epistemologists and statisticians working within Recognition Science would cite it to quantify information gain in belief revision. It is implemented as a direct call to the J-cost function on the ratio.
Claim. The Bayes factor cost is defined as $J(L/P)$, where $J$ is the J-cost function, $L$ is the likelihood, and $P$ is the prior.
background
The module models Bayesian updating with posterior proportional to likelihood times prior, replacing KL-divergence information gain by J-cost on the likelihood ratio. J-cost satisfies the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$ and vanishes at unity. The local setting predicts that a Bayes factor of phi marks the minimum detectable update, with $J(phi) approx 0.118$.
proof idea
The definition is a one-line wrapper applying the Jcost function directly to the ratio of likelihood over prior.
why it matters
It supplies the core cost measure used in the BayesianUpdateCert structure, which certifies vanishing cost at the null, nonnegativity, and thresholds exceeding 1 and 2. This realizes the Recognition Science prediction that the barely-convincing Bayes factor equals phi from the forcing chain T6, with moderate evidence at phi squared.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.