bayesFactorCost_nonneg
plain-language theorem explainer
The non-negativity of the J-cost on a Bayes factor for positive likelihood and prior follows directly from the corresponding property of J. Researchers modeling information gain in Bayesian updates under Recognition Science would cite this to confirm the measure remains non-negative. The term-mode proof is a one-line wrapper that unfolds the definition and invokes the J-cost non-negativity lemma on the positive ratio.
Claim. For positive real numbers $l > 0$ and $p > 0$, the J-cost of the likelihood ratio satisfies $0 ≤ J(l/p)$.
background
The module develops Bayesian updating in Recognition Science, where posterior ∝ likelihood × prior and information gain is the J-cost on the likelihood ratio. J-cost is the function $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$, non-negative by AM-GM as shown in the Cost module. The module doc states that a Bayes factor of φ corresponds to the minimum detectable update with J-cost ≈ 0.118, and φ² to moderate evidence matching Kass-Raftery thresholds.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the Bayes factor cost definition to expose the J-cost of the ratio, then applies the Jcost_nonneg lemma to the positive quantity produced by div_pos on the hypotheses.
why it matters
This supplies the non-negativity field in the BayesianUpdateCert definition that certifies the module's structural theorem on Bayes factor thresholds. It supports the Recognition Science claim that the barely convincing threshold is the Bayes factor φ, consistent with the phi-ladder and T5 J-uniqueness. The parent cert assembles this with sibling results to close the interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.