bayesFactorModerate_gt_two
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the Bayes factor from the J-cost equation.
- Does not connect the threshold to specific likelihood ratios or priors.
- Does not address empirical calibration against human evidence perception.
- Does not bound other thresholds such as the minimal or strong evidence levels.
Lean usage
have h : (2 : ℝ) < bayesFactorModerate := bayesFactorModerate_gt_twoformal statement (Lean)
65theorem bayesFactorModerate_gt_two : (2 : ℝ) < bayesFactorModerate := by
proof body
Term-mode proof.
66 unfold bayesFactorModerate
67 have h := phi_squared_bounds
68 linarith [h.1]
69