bayesFactorModerate_gt_two
plain-language theorem explainer
The moderate-evidence Bayes factor exceeds 2. RS statisticians cite the result to confirm that the φ² threshold clears the lower bound for moderate evidence in standard scales. The proof unfolds the definition and feeds the lower half of the phi-squared bounds lemma into linear arithmetic.
Claim. The moderate Bayes factor satisfies $2 < phi^2$, where $phi$ is the golden ratio.
background
The module models Bayesian updating via the J-cost on likelihood ratios. Moderate evidence is the threshold B = phi², placed between the minimal detectable update and stronger categories to match Kass-Raftery guidelines for positive evidence. The local setting treats the step from prior to posterior as an information gain measured by this cost functional. Upstream, the phi_squared_bounds lemma from Constants asserts (2.5 : ℝ) < phi^2 ∧ phi^2 < 2.7, derived from 1.5 < phi < 1.62 and the identity phi² = phi + 1. A tighter version in CosmologicalPredictionsProved gives 2.59 < phi² < 2.62.
proof idea
One-line wrapper. Unfolds the definition of the moderate factor to phi^2, obtains the phi_squared_bounds lemma, and applies linarith to its left conjunct.
why it matters
Supplies the moderate_gt_two field inside the BayesianUpdateCert record. This certifies that the J-cost model respects the conventional moderate-evidence floor. It realizes the RS prediction that B = phi² lies above 2, consistent with the self-similar fixed point and the phi-ladder constants. No open scaffolding is closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.