Loading the exact theorem scope…
READING THE PROOF
Drag the background to pan. Scroll, pinch or use + / − to zoom. Fit all shows the whole current view; the small map moves you around it.
Hover or focus a box for metadata. Select it for the complete Lean statement, exact source line, dependencies and audits. The ↗ on each box opens its source directly. Double-click a box, or use Expand dependencies, to reveal earlier steps.
Coloured zones group mathematical families. Select a family chip to reveal its authored theorem steps. Search also finds definitions and generated helpers in the full selected proof.
An arrow means the later declaration references the earlier one. A dashed arrow follows an actual path through collapsed declarations; select it to inspect or expand that path. This is a dependency graph, not a claim that a single theorem implies the next without its other hypotheses.
Authored dependencies are followed to external Lean/mathlib declarations and explicitly marked generated-data proof boundaries. Their complete transitive axioms are audited. The separate optional workflow checks every underlying range, anchor and cover group; ordinary CI checks this frozen snapshot without repeating the exhaustive certificate.
Keyboard: / search, F fit, + / − zoom, arrow keys pan on the canvas, Enter inspect a focused box, Esc close panels.
Metadata and reproduction guide ↗