cert
plain-language theorem explainer
This definition assembles a certificate confirming that the J-cost applied to Bayes factors yields zero cost under the null, non-negative costs otherwise, a threshold exceeding one, and a moderate threshold exceeding two. Researchers in information theory and Bayesian epistemology would reference it to ground evidence thresholds in the Recognition Science J-function. The construction is a direct structural definition that references four pre-established component results.
Claim. Let $c(l,p)$ be the cost of the Bayes factor $l/p$ under the J-function. The certificate asserts $c(p,p)=0$ for all $p≠0$, $c(l,p)≥0$ whenever $l>0$ and $p>0$, the detection threshold satisfies $θ>1$, and the moderate evidence threshold satisfies $m>2$.
background
In the Bayesian update module the J-cost measures information gain when moving from prior to posterior via the Bayes factor. The cost derives from the Recognition Science J-function $J(x)=(x+x^{-1})/2-1$, known to be non-negative from the upstream theorem on recognition events. The certificate structure collects four properties: null cost zero, non-negativity, threshold greater than one (via $φ>1$), and moderate greater than two (via $φ^2>2$). The module predicts that the minimum detectable update corresponds to a J-cost of approximately 0.118, with Bayes factors at $φ$ and $φ^2$.
proof idea
The definition constructs the certificate by directly assigning its four fields from sibling results: the null-cost property from the theorem establishing zero at equal arguments, non-negativity from the J-cost non-negativity applied to the ratio, the threshold inequality from the phi lower bound, and the moderate inequality from the phi-squared bounds.
why it matters
This certificate completes the structural verification for the Bayesian update from J-cost, enabling the module claim that Bayes factors of phi and phi squared supply the canonical thresholds for convincing and moderate evidence. It aligns with the Recognition Science forcing chain at the J-uniqueness step and the self-similar fixed point phi. The module falsifier highlights the need for empirical studies to confirm thresholds remain within 1.5 to 4.0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.