evidence_pos
The theorem shows that the marginal likelihood (evidence) of any observation is strictly positive whenever the prior is a discrete probability distribution and the likelihood function takes strictly positive values. Researchers deriving Bayesian updates from variational free energy minimization would cite it to guarantee that normalized posteriors remain well-defined. The proof is a one-line wrapper that unfolds the sum definition of evidence and applies the finite-sum positivity lemma to a nonempty index set.
claimLet $p$ be a probability distribution over a finite index set $ι$, let $L$ be a likelihood function such that $L(o,i)>0$ for every observation $o$ and every $i∈ι$, and let $o$ be given. Then the marginal likelihood satisfies $∑_i p(i)·L(o,i)>0$.
background
The module treats discrete Bayesian filtering as the one-step minimizer of variational free energy on a finite surface. A ProbDist ι consists of a map probs: Fin ι → ℝ that is nonnegative and sums to one; upstream results supply the auxiliary fact that each prob i is strictly positive. The Likelihood ι Obs structure packages a map like: Obs → ι → ℝ together with the axiom like_pos asserting strict positivity of every value. The evidence function is defined exactly as the finite sum ∑_i prior.prob i · L.like o i. The module imports VariationalFreeEnergyFromRCL, placing the construction inside the Recognition Composition Law framework.
proof idea
The term proof first unfolds the definition of evidence, exposing a Finset.sum. It then applies Finset.sum_pos, which reduces the goal to two subgoals: every summand is positive and the index set is nonempty. The first subgoal is discharged by mul_pos applied to prior.prob_pos i and L.like_pos o i; the second is discharged by Finset.univ_nonempty.
why it matters in Recognition Science
evidence_pos supplies the evidence_positive field inside bayesianFilteringCert_holds and is invoked inside the prob_pos field of bayesStep to ensure the normalized distribution is positive. It therefore closes the positivity requirement for the statistical layer that realizes Bayesian filtering as the VFE minimizer. In the Recognition Science chain this step sits between the RCL-derived variational free energy and the concrete filtering theorems; it touches the open question of lifting the construction from finite to continuous observation spaces.
scope and limits
- Does not treat continuous or countably infinite index sets.
- Does not compute a closed-form expression for the evidence value.
- Does not derive the variational free energy functional itself.
- Does not establish uniqueness of the resulting Bayesian update.
Lean usage
exact evidence_pos prior L oformal statement (Lean)
25theorem evidence_pos (prior : ProbDist ι) (L : Likelihood ι Obs) (o : Obs) :
26 0 < evidence prior L o := by
proof body
Term-mode proof.
27 unfold evidence
28 apply Finset.sum_pos
29 · intro i _
30 exact mul_pos (prior.prob_pos i) (L.like_pos o i)
31 · exact Finset.univ_nonempty
32