IndisputableMonolith.Statistics.BayesianUpdateFromJCost
This module defines the J-cost applied to Bayes factors for use in statistical updates under Recognition Science. Researchers formalizing likelihood-based inference or information measures in the RS setting would reference it when extending cost functions to Bayesian contexts. The module consists of targeted definitions and elementary properties for the cost on likelihood ratios.
claimThe module supplies $C(B) := J(B)$ where $B$ denotes a Bayes factor (likelihood ratio) and $J(x) = (x + x^{-1})/2 - 1$, together with lemmas establishing $C(1) = 0$, $C(B) > 0$ for $B > 1$, and threshold comparisons such as $C(B) > 1$ for moderate evidence.
background
Recognition Science derives its cost measure from the J-functional on positive reals, introduced via the forcing chain and satisfying the Recognition Composition Law. The Cost module supplies the base J-cost definition, while Constants fixes the RS time quantum at one tick. This statistics module applies that cost directly to likelihood ratios, treating them as Bayes factors in an inference setting that remains independent of specific priors.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module bridges the abstract J-functional to statistical applications, supplying the cost interface needed for Bayesian update rules in the Recognition framework. It prepares the ground for downstream results that would incorporate these costs into probability revisions, consistent with the phi-ladder and RCL structures.
scope and limits
- Does not derive explicit posterior update formulas.
- Does not specify priors or data models.
- Does not link to physical constants such as alpha or G.
- Does not address continuous versus discrete likelihoods.
depends on (2)
declarations in this module (12)
-
def
bayesFactorCost -
theorem
bayesFactorCost_at_null -
theorem
bayesFactorCost_nonneg -
def
bayesFactorThreshold -
theorem
bayesFactorThreshold_gt_one -
theorem
bayesFactorThreshold_cost -
def
bayesFactorModerate -
theorem
bayesFactorModerate_pos -
theorem
bayesFactorModerate_gt_two -
structure
BayesianUpdateCert -
def
cert -
theorem
cert_inhabited