bayesianFilteringCert_holds
plain-language theorem explainer
The theorem certifies that BayesianFilteringCert holds by verifying strict positivity of the evidence and the exact normalized form of the one-step Bayesian update. Researchers deriving filtering rules from variational free energy or the recognition composition law would cite it to anchor discrete Bayesian steps. The proof is a direct term construction that assembles the two structure fields from the lemmas evidence_pos and bayesStep_is_update.
Claim. For any prior probability distribution $p$, likelihood $L$, and observation $o$, the marginal evidence satisfies $0 < e(p,L,o)$. The updated distribution after the Bayesian step obeys $p'(i) = p(i) L(o,i) / e(p,L,o)$ for each state $i$.
background
The module shows that a Bayesian update is the one-step minimizer of variational free energy on a discrete filtering surface, derived from the recognition composition law. ProbDist ι denotes a probability distribution over states ι; Likelihood ι Obs is a family of positive functions on ι indexed by observations. The evidence function is the marginal likelihood obtained by summing prior times likelihood over states; bayesStep applies the normalized product to produce the posterior.
proof idea
Term-mode proof that constructs the BayesianFilteringCert structure directly. It assigns the evidence_positive field to the theorem evidence_pos and the bayes_step_update field to the lambda expression that invokes bayesStep_is_update on the four arguments.
why it matters
The result certifies the discrete filtering surface claimed in the module header, confirming that the Bayesian step is the exact VFE minimizer. It rests on the recognition composition law imported via VariationalFreeEnergyFromRCL and on the positivity and definitional properties proved locally. No downstream theorems are recorded, so its role in larger inference pipelines or extensions to continuous cases remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.