entails — B follows from A (implication, or the construction A feeds)
discharges — A proves away assumption B
rests on — B is an assumption needed by A (an in-Lean hypothesis, or an out-of-Lean floor)
gap — A has a gap that would be fixed by B (an uncomposed modeling identification, not a stated assumption)
Proven theorem
Hypothesis in statement
Out-of-Lean assumption
Definition — a claim (Prop) or construction (data)
Top-level result (verifier soundness)
Hover or click a node to see what it is, its Lean anchor, and every theorem it connects to — with the lemma that justifies each link.
The spine runs down the left: accepting proof → verifier equation → deployed tree → peel → IPA opening → SnarkRelation. The tinted territories are the machinery that discharges its assumptions.