We combine the previous results into four Lean theorems that heuristically compose into the end-to-end conclusion: if the OpenVM verifier accepts a proof, the committed RISC-V program ran and produced the claimed output, up to a quantitative soundness error.
Solid arrows show selected Lean proof dependencies, through helper lemmas; dashed arrows show heuristic composition. The heuristic model assumes the extraction bounds hold in a single experiment with one shared ideal-permutation oracle, transcript, and query budget, and then transfers the bound to Poseidon2.
