BayesianFilteringCert
plain-language theorem explainer
BayesianFilteringCert packages the positivity of the marginal evidence and the explicit normalized update formula for one-step Bayesian filtering. Workers in variational inference would cite it to certify that the update derived from the Recognition Composition Law satisfies the standard Bayes rule. The declaration is a plain structure definition with no computational content.
Claim. A structure asserting that for any discrete prior distribution $p$ over index set $ι$, likelihood function $L: Obs → ι → ℝ$ with $L(o|i)>0$, and observation $o$, the evidence $e(p,L,o) := ∑_i p(i) L(o|i)$ satisfies $e(p,L,o)>0$, and the updated distribution satisfies $p'(i) = p(i) L(o|i) / e(p,L,o)$ for each $i$.
background
The module establishes that a Bayesian update is the one-step minimizer of variational free energy on a discrete surface. ProbDist is a structure whose field probs : Fin n → ℝ satisfies nonnegativity and summation to one. Likelihood is the sibling structure whose like field is a strictly positive map Obs → ι → ℝ. Evidence is the un-normalized marginal ∑_i prior.prob i · L.like o i. bayesStep constructs the normalized posterior by dividing the product prior.prob i · L.like o i by that marginal.
proof idea
This is a structure definition that directly records the two required properties. No lemmas are applied inside the declaration itself; the fields are later populated by the separate facts evidence_pos and bayesStep_is_update.
why it matters
bayesianFilteringCert_holds assembles the certificate from those two facts, placing the Bayesian filter inside the Recognition framework as the discrete surface of variational free energy minimization. The construction rests on the Recognition Composition Law through the imported VariationalFreeEnergyFromRCL module and supplies the update rule required by the eight-tick octave and phi-ladder mass formulas downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.