IndisputableMonolith.Statistics.BayesianUpdateFromJCost

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# Bayesian Update from J-Cost (Plan v7 fifty-fourth pass)
   7
   8## Status: STRUCTURAL THEOREM (0 sorry, 0 axiom).
   9
  10Bayesian updating: posterior ∝ likelihood × prior.
  11The KL-divergence from prior to posterior measures information gain.
  12
  13RS prediction: the minimum detectable Bayesian update (the step
  14that changes beliefs from "essentially unchanged" to "meaningfully
  15updated") corresponds to a J-cost of J(φ) ≈ 0.118 on the
  16likelihood ratio.
  17
  18Specifically: a Bayes factor B = φ (odds ratio φ ≈ 1.618) is the
  19canonical "barely convincing" threshold, and B = φ² ≈ 2.618 is
  20the "moderate evidence" threshold — matching Kass-Raftery (1995)
  21who define Bayes factor 3-10 as "positive" evidence.
  22
  23## Falsifier
  24
  25Any Bayesian epistemology study showing the threshold for
  26"subjectively convincing" evidence at Bayes factors consistently
  27outside (1.5, 4.0).
  28-/
  29
  30namespace IndisputableMonolith
  31namespace Statistics
  32namespace BayesianUpdateFromJCost
  33
  34open Constants
  35open Cost
  36
  37noncomputable section
  38
  39/-- J-cost on the likelihood ratio (Bayes factor). -/
  40def bayesFactorCost (likelihood prior : ℝ) : ℝ :=
  41  Jcost (likelihood / prior)
  42
  43theorem bayesFactorCost_at_null (p : ℝ) (h : p ≠ 0) :
  44    bayesFactorCost p p = 0 := by
  45  unfold bayesFactorCost; rw [div_self h]; exact Jcost_unit0
  46
  47theorem bayesFactorCost_nonneg (l p : ℝ) (hl : 0 < l) (hp : 0 < p) :
  48    0 ≤ bayesFactorCost l p := by
  49  unfold bayesFactorCost; exact Jcost_nonneg (div_pos hl hp)
  50
  51/-- Barely-convincing Bayes factor: B = φ. -/
  52def bayesFactorThreshold : ℝ := phi
  53
  54theorem bayesFactorThreshold_gt_one : 1 < bayesFactorThreshold := one_lt_phi
  55
  56theorem bayesFactorThreshold_cost : Jcost bayesFactorThreshold = phi - 3 / 2 := by
  57  unfold bayesFactorThreshold; exact Jcost_phi_val
  58
  59/-- Moderate evidence: B = φ². -/
  60def bayesFactorModerate : ℝ := phi ^ (2 : ℕ)
  61
  62theorem bayesFactorModerate_pos : 0 < bayesFactorModerate := by
  63  unfold bayesFactorModerate; exact pow_pos phi_pos _
  64
  65theorem bayesFactorModerate_gt_two : (2 : ℝ) < bayesFactorModerate := by
  66  unfold bayesFactorModerate
  67  have h := phi_squared_bounds
  68  linarith [h.1]
  69
  70structure BayesianUpdateCert where
  71  cost_at_null : ∀ p : ℝ, p ≠ 0 → bayesFactorCost p p = 0
  72  cost_nonneg : ∀ l p : ℝ, 0 < l → 0 < p → 0 ≤ bayesFactorCost l p
  73  threshold_gt_one : 1 < bayesFactorThreshold
  74  moderate_gt_two : (2 : ℝ) < bayesFactorModerate
  75
  76noncomputable def cert : BayesianUpdateCert where
  77  cost_at_null := bayesFactorCost_at_null
  78  cost_nonneg := bayesFactorCost_nonneg
  79  threshold_gt_one := bayesFactorThreshold_gt_one
  80  moderate_gt_two := bayesFactorModerate_gt_two
  81
  82theorem cert_inhabited : Nonempty BayesianUpdateCert := ⟨cert⟩
  83
  84end
  85end BayesianUpdateFromJCost
  86end Statistics
  87end IndisputableMonolith
  88