theorem proved term proof

`cert_inhabited`

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

formal statement (Lean)

  82theorem cert_inhabited : Nonempty BayesianUpdateCert := ⟨cert⟩

Term-mode proof.

  83
  84end
  85end BayesianUpdateFromJCost
  86end Statistics
  87end IndisputableMonolith

Lean names referenced from this declaration's body.

Statistics in IndisputableMonolith.QFT.SpinStatistics decl_use
BayesianUpdateCert in IndisputableMonolith.Statistics.BayesianUpdateFromJCost decl_use