Bayes' rule updates posterior odds by the likelihood ratio
ProvedFreeEnergyPrinciple.posteriorOdds_recursionBayes' rule in odds form — the update step of Bayesian model reduction.
Fix a finite hypothesis space and finite evidence space, a prior law over hypotheses, and a finite likelihood kernel from hypotheses to evidence. At evidence whose predictive mass under the model is positive, the posterior odds between a favored hypothesis and a reference hypothesis is the ratio of their exact finite Bayes posteriors.
Then the odds update multiplicatively:
provided the reference prior mass and the reference likelihood are strictly positive — these are not decoration but the exact division premises; a zero-prior hypothesis retains zero posterior mass rather than being recoverable by conditioning, and the substrate's totalized real division returns (not ) at a zero evidence denominator.
This is precisely the comparison step of Bayesian model reduction: when a model is a reduction of , the posterior model odds equal the prior model odds times the Bayes factor [Friston & Penny 2011]. The related multiplicative structure — factorized evidence ratios multiply and sequential model-odds updates agree with one update by the product evidence (catalogue topic fep-120, theorem bayesFactor_multiplicative) — is available from the same definition layer as a further target.
import Definitions.Def_fep_finite_laws import Definitions.Def_fep2_bayesian_model_reduction
namespace FreeEnergyPrinciple
theorem posteriorOdds_recursion
{Hypothesis Evidence : Type*} [Fintype Hypothesis] [Fintype Evidence]
(prior : FiniteLaw Hypothesis)
(likelihood : FiniteKernel Hypothesis Evidence)
(evidence : Evidence)
(evidencePositive : 0 < likelihood.predictive prior evidence)
(favored reference : Hypothesis)
(referencePriorPositive : 0 < prior reference)
(referenceLikelihoodPositive : 0 < likelihood reference evidence) :
posteriorOdds prior likelihood evidence evidencePositive favored reference =
(prior favored / prior reference) *
(likelihood favored evidence / likelihood reference evidence) := by sorry
end FreeEnergyPrincipleRead-back
What the Lean code literally says, in plain math · glm-flash-latest
Theorem posteriorOdds_recursion (namespace FreeEnergyPrinciple). Let (hypotheses) and (evidence) be arbitrary types, both finite. Given a prior on and a likelihood kernel from to distributions over , a point , two hypotheses (favored) and (reference), and the three positivity assumptions
the claim is
That is: the bundle's posterior-odds operation, applied to the prior, kernel, evidence, and the proof that the predictive (marginal) mass of is positive, equals the prior ratio times the likelihood ratio. Only the reference row and the predictive need be positive; may have zero prior or zero likelihood, in which case the right side is . Both denominators are positive by hypothesis, so the divisions are ordinary nondegenerate real division. If were empty the predictive would be , contradicting the first assumption, so that degenerate case is excluded implicitly.
AUDITOR-FLAG: the proof is closed with sorry — unproved. AUDITOR-FLAG: FiniteLaw, FiniteKernel, predictive, and posteriorOdds are defined in imported modules not provided for this audit, so the exact form of posteriorOdds (e.g. whether it is a normalized posterior-probability ratio) is not verifiable from this file alone. AUDITOR-FLAG: the name says "recursion", but the statement is a closed-form product identity, not a recursion.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.