bayesFactorModerate_pos
plain-language theorem explainer
The theorem establishes that the moderate-evidence Bayes factor equals the square of the golden ratio and is therefore positive. Bayesian statisticians working with Recognition Science thresholds would cite it to anchor the lower bound on evidence strength. The proof is a one-line wrapper that unfolds the definition and invokes the standard positivity of powers with positive base.
Claim. $0 < B$ where the moderate Bayes factor is defined by $B = phi^2$ and $phi$ is the golden-ratio fixed point of the self-similar forcing chain.
background
The module treats Bayesian updating via the J-cost function of Recognition Science. Posterior odds equal prior odds times the likelihood ratio; the information gain is quantified by the J-cost of that ratio. The moderate-evidence threshold is set at $B = phi^2$, matching the Kass-Raftery interval for positive evidence. Upstream result: Moderate evidence: B = φ². The local setting is the structural theorem that the minimum detectable update corresponds to J-cost J(phi) approximately 0.118.
proof idea
One-line wrapper. It unfolds the definition of the moderate Bayes factor as phi raised to the second natural power, then applies the lemma pow_pos to the already-established positivity of phi.
why it matters
The result closes the positivity requirement inside the Bayesian-update structural theorem of the module. It supplies the concrete lower bound needed for the RS prediction that a Bayes factor of phi squared marks the transition from negligible to moderate evidence. The module supplies an explicit falsifier: any empirical study placing the subjective threshold consistently outside the interval (1.5, 4.0).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.