bayesFactorModerate
plain-language theorem explainer
The moderate evidence Bayes factor threshold is set to the square of the golden ratio. Bayesian statisticians applying Recognition Science models cite this constant when calibrating the transition from weak to positive evidence in belief updates. The definition is a direct assignment of phi to the second power.
Claim. The moderate evidence threshold for the Bayes factor is defined as $B = phi^2$, where $phi$ is the golden ratio self-similar fixed point.
background
The module treats Bayesian updating with posterior proportional to likelihood times prior, measuring information gain by KL-divergence from prior to posterior. J-cost is the Recognition Science cost function tied to the J-uniqueness relation J(x) = (x + x^{-1})/2 - 1. The phi constant enters as the self-similar fixed point forced in the unified chain. The module doc states that B = phi^2 approximates 2.618 and matches the Kass-Raftery scale for moderate evidence.
proof idea
One-line definition that directly assigns phi raised to the power 2.
why it matters
This supplies the moderate_gt_two property required by the BayesianUpdateCert structure. It completes the moderate evidence step in the Bayesian update model, aligning the phi-ladder threshold with empirical scales from Kass-Raftery (1995). The placement links to the T6 fixed-point forcing and the overall structural theorem for RS-native statistics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.