bayesFactorCost_nonneg
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not apply when likelihood or prior is non-positive.
- Does not establish strict positivity or a positive lower bound.
- Does not compute or bound the numerical value of the cost.
- Does not address iterated or multi-step updates.
formal statement (Lean)
47theorem bayesFactorCost_nonneg (l p : ℝ) (hl : 0 < l) (hp : 0 < p) :
48 0 ≤ bayesFactorCost l p := by
proof body
Term-mode proof.
49 unfold bayesFactorCost; exact Jcost_nonneg (div_pos hl hp)
50
51/-- Barely-convincing Bayes factor: B = φ. -/