bayesianFilteringCert_holds
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive the variational free energy functional itself.
- Does not treat continuous state spaces or continuous-time filtering.
- Does not address approximate or variational inference beyond exact Bayes.
- Does not link to spatial dimensions, the phi ladder, or forcing-chain constants.
formal statement (Lean)
66theorem bayesianFilteringCert_holds : BayesianFilteringCert (ι := ι) (Obs := Obs) :=
proof body
Term-mode proof.
67{ evidence_positive := evidence_pos
68 bayes_step_update := fun prior L o i => bayesStep_is_update prior L o i }
69
70end
71
72end IndisputableMonolith.Statistics.BayesianFilteringFromVFE