The whole verifier collapsed into one multi-scalar multiplication; the proof accepts exactly when that MSM is the group identity. Checked equal to the Rust verifier's captured MSM, for the specific circuit under analysis. The map's pinned to Rust node.

Conditional capstones take an opaque accepts : Prop — a scaffold, not finished soundness; deployed capstones take the concrete accept (assembled MSM = identity).

halo2's explicit IPA verifier equation, recovered from the compact MSM = 0 accept — the readable form the IPA argument consumes.

Rewinding the random oracle to get three accepting continuations per round at distinct, nonzero challenges; assembled into the transcript tree the extractor consumes. Proven (an averaging argument) once the accept probability beats the knowledge error kerr/Nᵏ.

Re-running the schedule with the oracle reprogrammed at a round prefix: redrawing the IPA round vector is exactly reprogramming the deployed oracle (roChallenges_reprogramRounds) — the bridge from the forking measure to the deployed rewound runs, and the load-bearing consumer of transcript ordering. The _rewind capstones state the accept probability over these runs.

halo2's verifier equation recast as the accept predicate of a concrete prover strategy read off the proof — the proven half of the prover-as-oracle bridge; only the random-oracle measure underneath stays a floor.

The transcript-ordering guarantee: each IPA round point sits in the transcript prefix before its challenge is drawn, so later messages cannot bend earlier challenges.

The auxiliary generators the deployed verifier folds into the MSM alongside the main g basis — the fold and blinding terms.

Stripping the U/W terms off the deployed transcript tree to recover a clean, g-only IPA tree — or, failing that, a discrete-log relation.

Extraction of the witness from three accepting transcripts at pairwise-distinct, nonzero challenges per round.

Folding the claimed value and synthetic blinder into the opened commitment: P′ = P − [v]g₀ + [ξ]S. The un-shift/un-blind lemmas move an opening of P′ back to the actual multiopen commitment at its true value — the value-placement step deployed_forking_relation performs on the equation-to-tree edge.

A nontrivial discrete-log relation, carried as data with its coefficients explicit. One always exists at prime order, so an ∃-closed Prop version (or an ∨-branch concluding it) is vacuous as a statement; the reductions compute one from a break, and the force is the computational assumption that no efficient adversary can find one.

The data-carrying relation witness the discrete-log reduction consumes — an explicit function of the prover's representations, no Classical.choice. Reached from the forking side's existential relation only across a gap: an uncomposed modeling identification (issue #15), drawn on the map as its own edge kind. The other gap reads the sampled-basis probability bound at the deployed URS.

The AGM trick: hide a discrete-log challenge in one basis slot fixed before the adversary runs; a found relation hitting that slot yields the discrete log.

The random-slot accounting: the planted slot is hit with probability at least 1/|basis| of the finder's, so relation-finding probability is bounded by a multiple of the discrete-log advantage — where DL-hardness enters as an explicit, priced hypothesis.

The decoded columns satisfy the circuit gates — the constraint half of the SNARK relation, paired with the IPA opening.

The x₄ forking floor: given an accepting honest run, an accept measure beating the pair-count bound extracts an injective family of accepting x₄-rewound runs — one IPA witness per run, the batch the decode inverts.

The x₄-level columns recovered from the batched multiopen witness by Vandermonde inversion of rewound openings — the point-set aggregates (qᵢ, q′), not yet circuit columns; the x₁ unbatch reads the member commitments out of them.

The multiopen batching layers: x₄ folds all opening claims into one by powers of the challenge; x₁ bundles the commitments queried at each point set into an aggregate, which the unbatch opens back to the individual member commitments — pinning the extracted witness as the two-level power combination of their column witnesses.

The challenge values that fool the gate check — the roots of the constraint-difference polynomial; a uniform random-oracle challenge lands in it with probability ≤ d/p (Schwartz–Zippel). A challenge outside it is the map's sound challenge.

The top-level orchard_verifier_vesta_* theorems, forming a ladder of increasingly strong variants (conditional → reductions → forking → deployed / adaptive / rewind), each in an opening and a constraint form. The map's verifier soundness node is the base capstone. Two wrappers sit on top (not a full product across rungs): _agm_dl — the map's AGM soundness — routes the relation branch through the fixed-slot adapter to the trichotomy opening ∨ discrete-log solution ∨ soundness loss, that branch bounded separately in the probability layer; _xgood derives hgood (the sound challenge) instead of assuming it.

The verifier's gate/quotient point-check, plus carrying the gate challenge x over to the multiopen point x₃. Carried as the capstone hypothesis hquot; still open.

The challenge avoids the Schwartz–Zippel bad set, so the point-check at x implies the full gate identity. Carried as the capstone hypothesis hgood; discharged by the SZ territory's _xgood wrapper.

The accepting-proof probability beats the knowledge error kerr/Nᵏ — enough for the forking lemma to extract. Carried as the capstone hypothesis hprob; the measure-side random-oracle floor.

The remaining structural capstone hypotheses: z ≠ 0 (every rung), g₀ ≠ 0 (every forking rung), the S-opening commit s = ipaS (deployed/adaptive/rewind rungs), and value recovery ξ·⟨s,b⟩ = 0 (constraint rungs only). Assumed in-Lean, priced rather than discharged.

The two gaps the composition does not yet cross: on the output side, hencodes — gate satisfaction (SnarkRelation) implies the intended high-level statement; on the input side, VK correctness — the verifying key fed to the verifier faithfully encodes the real deployed circuit. Both outside Lean; not started.

Break events are structures carrying the breaking data (colliding queries, relation coefficients); the reductions producing them are plain computable defs. An ∃-closed break Prop is vacuously true at the instantiations of interest (relations always exist at prime order; compressing hashes always have collisions), so the content lives in the data, protected by compiler-checked computability and pinned axiom sets. See Breaks as computed data.

Build-time pins on what a theorem may rest on: assert_no_sorry over the elaborated dependency graph plus a #guard_msgs-pinned #print axioms, so a stray sorry or a new axiom fails the build instead of silently widening the trusted base. See Trust discipline.