bayesFactorThreshold_gt_one
plain-language theorem explainer
The theorem establishes that the Bayes factor threshold exceeds one, confirming the golden ratio supplies a strictly positive information gain for the minimum detectable Bayesian update in J-cost models. Statisticians calibrating evidence thresholds against the phi-ladder would cite this when linking odds ratios to Recognition Science predictions. The proof is a one-line wrapper that invokes the established one_lt_phi inequality.
Claim. $1 < B$ where $B = phi$ is the barely-convincing Bayes factor threshold (the odds ratio at which a Bayesian update becomes subjectively detectable).
background
In the BayesianUpdateFromJCost module the threshold is introduced as the canonical point where posterior odds cross from essentially unchanged to meaningfully updated. The module sets this equal to the golden ratio phi and ties it to a J-cost of J(phi) approximately 0.118, consistent with the Recognition Composition Law and the minimum detectable step on the phi-ladder. The upstream one_lt_phi lemma (appearing in Constants, PhiSupport, and PhiSupport.Lemmas) supplies the elementary fact that phi exceeds one, proved via norm_num and square-root comparisons of 1 and 5.
proof idea
The proof is a one-line wrapper that applies the lemma one_lt_phi directly to the definition bayesFactorThreshold := phi.
why it matters
The result supplies the threshold_gt_one field inside the BayesianUpdateCert structure used by cert. It fills the RS prediction that a Bayes factor of phi marks the transition to detectable belief change, aligning with Kass-Raftery scales for positive evidence. The declaration touches T5 J-uniqueness and T6 phi fixed-point steps in the forcing chain; the module falsifier remains any empirical study placing the convincing-evidence threshold consistently outside (1.5, 4.0).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.