Per-component diagnosis of ungroundedness: PARADOX (no classical models — refusal permanent), UNDERDETERMINED (models exist — liftable by stipulation), INPUT, DOWNSTREAM with culprits; the stipulation theorem measured totally; parity re-derived \(62/62\). The even two-cycle’s two classical models are kernel-checked.

For every finite system: lazy evaluation is monotone over the whole language, the jump is monotone, the iteration from \(\bot \) stabilizes within \(n{+}1\) steps at the least fixed point, and the grounded part is identical in every fixed point — quarantine is well-defined. Zero axioms (information-measure pigeonhole, no WF machinery).