Authoring a proof, and repairing one Forty-eight seconds on a single item — lem-cauchy-bounded — from a Beta's draft, through the phase stratification precheck enforces, to a judge rejection, an adjudication, a repair that changes the graph, and the targeted rejudge that closes it.

0:00 / 0:48

The item is real and published: its facts, citations, final step labels and bracket tags are what is on disk in items/lem-cauchy-bounded.md, with the step prose condensed to fit a frame. The layering is the algorithm of layerRepair in the normative checker, and the workflow around it is LEVELS.md steps 5 to 8. Companion page: the whole level, at low magnification, in build-workflow.html.