iterFilter_nil
The base case of iterative Bayesian filtering states that applying no observations leaves the prior distribution unchanged. Researchers deriving discrete filters from variational free energy would cite this identity when inducting over observation lists. The proof is immediate by reflexivity matching the recursive definition of iterFilter.
claimLet $L$ be a likelihood function from observations to states with positive real values and let $p$ be a probability distribution over states. Then the iterative filter applied to the empty observation list returns $p$ unchanged.
background
The module treats Bayesian filtering as sequential one-step minimizers of variational free energy. Likelihood is the structure supplying a positive real-valued function from observations to states. ProbDist is the structure of non-negative functions summing to one, drawn from ShannonEntropy. iterFilter is defined recursively by applying bayesStep to each observation in turn, with the empty-list case returning the input distribution directly.
proof idea
The proof is a one-line wrapper that applies reflexivity to the base case of the recursive definition of iterFilter.
why it matters in Recognition Science
This identity supplies the base case needed for inductive arguments about the full filtering process. It supports downstream certification that iterated updates remain consistent with the variational free energy derivation from the Recognition Composition Law. In the Recognition framework it anchors the discrete filtering surface described in the module documentation.
scope and limits
- Does not establish convergence or stability of the iterated filter.
- Does not extend to continuous observation or state spaces.
- Does not address numerical stability or approximation error.
- Does not connect to the full T0-T8 forcing chain or phi-ladder.
formal statement (Lean)
53theorem iterFilter_nil (L : Likelihood ι Obs) (p : ProbDist ι) :
54 iterFilter L [] p = p := rfl
proof body
55