[chris-dare-dev]

Closes chris-dare-dev/derived-alg-geo-lean#654.

reviewed_statement_pp is the string a review's survival depends on. Every way of getting it wrong is silent: the field looks captured, mfc validate passes, and the failure appears at the next dependency bump as not_checkable — which reads like a broken tool rather than a bad capture.

Capturing the first real one by hand took three attempts, with the schema, the checker and the emitter all open:

#	failure	why it was invisible
1	pp.explicit alone left a ⋯ elision in the K₀ quotient's proof argument	unparseable, but the field looked filled
2	#check @Decl instantiates with fresh universe metavariables printed u_1, u_2, u_3; real levelParams are [w, u, u']	unknown universe level u_2 — reads as tooling failure
3	both were "verified" with universe u_1 u_2 u_3 above an example	supplies by hand the level context restateOne does not have

The fix

--capture <decl> renders ci.type under Emit.ppOpts with pp.explicit := true, then puts the result through restateOne itself — the same parse, the same elabTerm under withoutErrToSorry, the same isDefEq, the same withLevelNames. It returns the string only on restated.

All three failures above produce a rendering that fails that check, so none can reach review.yaml through this path.

Two details that are the whole point:

• ci.type, never #check @Decl. The type carries the declaration's own level parameters; the term carries metavariables under invented names no level context can bind.
• Emit.ppOpts stops being private rather than being copied. A capture rendered under different options than the emitter uses is a different string about the same declaration, and two lists drift.

Verified

capture MathFormalContractTest.restateSubjectPoly
  → ∀ {α : Type u} (a : α), @Eq.{u + 1} α a a       (declaration's own level name)
  → "41 chars, verified restated", exit 0

that string fed back through the producer
  → 1 restated, 0 changed, 0 not_checkable

capture MathFormalContractTest.noSuchThing
  → "declaration ... is not in this environment", exit 1, nothing emitted

The test library asserts all three: the rendering uses the declaration's level name, it round-trips as restated through restateOne, and an absent declaration errors rather than yielding an empty capture.

613 passed, 1 skipped; lake build clean at 26 jobs.