theorem proved term proof

`bayesFactorThreshold_cost`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  56theorem bayesFactorThreshold_cost : Jcost bayesFactorThreshold = phi - 3 / 2 := by

Term-mode proof.

  57  unfold bayesFactorThreshold; exact Jcost_phi_val
  58
  59/-- Moderate evidence: B = φ². -/

Lean names referenced from this declaration's body.

Jcost_phi_val in IndisputableMonolith.Constants decl_use
evidence in IndisputableMonolith.Statistics.BayesianFilteringFromVFE decl_use
bayesFactorThreshold in IndisputableMonolith.Statistics.BayesianUpdateFromJCost decl_use