evidence
plain-language theorem explainer
The evidence definition computes the marginal likelihood of an observation o as the sum over states of prior probability times likelihood value. Researchers deriving one-step Bayesian updates from variational free energy in Recognition Science cite this when connecting discrete filtering to the RCL. The definition is a direct summation that follows from the ProbDist and Likelihood structures without additional lemmas.
Claim. For prior distribution $p$ over states $ι$, likelihood function $ℓ : Obs → ι → ℝ$, and observation $o$, the evidence equals $∑_i p(i) ⋅ ℓ(o,i)$.
background
The module establishes a discrete filtering surface in which a Bayesian update is the one-step VFE minimizer. ProbDist from VariationalFreeEnergyFromRCL supplies a probability distribution on ι with positive components summing to one, while Likelihood is the structure holding the positive real function like : Obs → ι → ℝ. Upstream results include the basic ProbDist from ShannonEntropy and the Ledger L from Recognition, both supplying the discrete probability primitives used here.
proof idea
One-line definition that directly applies the summation operator to the product of the prior probability function and the likelihood value at the given observation.
why it matters
This supplies the evidence term required by BayesianFilteringCert and downstream declarations such as observationalStatus in Cosmology and btfr_mass_velocity_relation in Gravity. It fills the likelihood integration step that follows from the Recognition Composition Law in the VFE derivation and supports the eight-tick filtering constructions referenced in the RRF hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.