iterFilter_cons
The cons case of the recursive definition of iterative Bayesian filtering reduces filtering a list of observations to a single Bayesian update step followed by filtering the tail. Researchers deriving discrete filters from variational free energy would cite this identity when unfolding multi-step updates or proving inductive properties. The proof holds by direct unfolding of the recursive clause in the definition of the filter.
claimLet $L$ be a likelihood structure supplying a positive real-valued function on observation-state pairs, let $p$ be a discrete probability distribution over states, let $o$ be an observation, and let $os$ be a list of observations. Then the iterative filter applied to the list $o :: os$ starting from $p$ equals the iterative filter applied to the tail $os$ starting from the Bayesian update of $p$ by observation $o$ under $L$.
background
The module treats discrete Bayesian filtering as successive one-step minimizers of variational free energy, with each update derived from the recognition composition law. A Likelihood is a structure containing a function like: Obs → ι → ℝ that is strictly positive on every observation-state pair. A ProbDist is a finite discrete probability distribution whose components are non-negative and sum to one. The bayesStep operation multiplies the prior probabilities by the likelihood values for the observed datum and normalizes by the marginal evidence. The iterFilter function is defined recursively on the observation list: the empty list returns the input distribution unchanged, while a cons cell applies one bayesStep and recurses on the remaining list.
proof idea
The proof is a direct definitional equality obtained by pattern-matching on the cons constructor in the recursive definition of iterFilter.
why it matters in Recognition Science
This identity justifies inductive arguments over finite sequences of observations inside the Bayesian filtering construction that links each step to variational free energy minimization. It supports downstream certification results such as bayesianFilteringCert_holds by allowing properties to be lifted from single updates to arbitrary lists. In the Recognition Science setting it anchors the discrete filtering surface to the RCL-derived free-energy functional without introducing additional hypotheses.
scope and limits
- Does not prove convergence or stability of the iterated filter for long sequences.
- Does not extend to continuous observation spaces or infinite lists.
- Does not derive the variational free energy expression from first principles.
- Does not establish uniqueness of the Bayesian update among all possible updates.
formal statement (Lean)
56theorem iterFilter_cons (L : Likelihood ι Obs) (o : Obs) (os : List Obs) (p : ProbDist ι) :
57 iterFilter L (o :: os) p = iterFilter L os (bayesStep p L o) := rfl
proof body
58