BayesianFilteringCert
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not establish convergence of iterated filtering.
- Does not treat continuous state or observation spaces.
- Does not derive the update from an explicit free-energy functional.
- Does not address computational complexity of the summation.
Lean usage
theorem example_cert : BayesianFilteringCert (ι := ι) (Obs := Obs) := bayesianFilteringCert_holdsformal statement (Lean)
59structure BayesianFilteringCert where
60 evidence_positive : ∀ (prior : ProbDist ι) (L : Likelihood ι Obs) (o : Obs),
61 0 < evidence prior L o
62 bayes_step_update : ∀ (prior : ProbDist ι) (L : Likelihood ι Obs) (o : Obs) (i : ι),
63 (bayesStep prior L o).prob i =
64 prior.prob i * L.like o i / evidence prior L o
65