Item 66: Grounded Replay in Lean

Two types, one fold, two premises, one induction and three corollaries. No dependency on either reference model or on Reflective Integrity, and the whole statement fits on a page.

Four passes were needed before this was worth doing, and each found a false or missing statement in the one before: a rule whose licences need not be grounded, a frontier an unauthorized revocation can empty, a grounding theorem an ungrounded creation refutes, and a certificate that answered a currentness question with a lineage. Porting any of them would have frozen a false statement.

Deliverable shape: Occ, Edit, replay, S1 and S2 as explicit hypotheses; the grounding theorem and its three corollaries proved; an inhabitation witness for the full hypothesis package, per AGENTS.md standard 3. Acceptance check: sorry-free, #print axioms clean, and the witness is the constitution model rather than a record — the point is that the theorem does not mention one. Context: projects/normativity/legitimacy/rounds/2026-08-25-legitimate-evolution/LEGITIMATE_EVOLUTION.md, the MINIMAL MATHEMATICAL STATEMENT section; src/replay.py. Consumed by: any round wanting to cite grounded legitimacy as established rather than as test-supported.