pith. sign in
module module moderate

IndisputableMonolith.Statistics.BayesianUpdateFromJCost

show as:
view Lean formalization →

This module supplies definitions that apply the J-cost function to likelihood ratios, producing Bayes factors, thresholds, and certificates for model comparison. Researchers using Recognition Science for statistical inference would cite these when replacing standard log-likelihoods with J-cost. The module is a collection of definitions and elementary lemmas with no complex proofs.

claimLet $J$ denote the J-cost. Define the Bayes factor from J-cost by $B(r) := J(r)$ where $r$ is the likelihood ratio; introduce thresholds $B > 1$, $B > 2$ for moderate evidence and the certificate type BayesianUpdateCert together with its inhabitant.

background

The module imports Constants (defining the RS time quantum τ₀ = 1 tick) and Cost (supplying the J-cost and related defect measures). It therefore operates inside the Recognition Science setting where all quantities are expressed via the J functional equation and the phi-ladder. The sibling declarations introduce bayesFactorCost, bayesFactorThreshold, bayesFactorModerate and the inhabited certificate BayesianUpdateCert.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the statistical layer that converts J-cost evaluations into Bayes factors, thereby linking the Cost module to downstream inference. It fills the interface between the core J-cost machinery and any later statistical claims that rely on likelihood ratios.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (12)