This preprint gives a finite obstruction-calculus response to categorical models of self-revising discovery systems. The central claim is that categorical regime transition can identify residual content, but residual detection is not yet certification. Under declared finite-dimensional rational carriers, exact realization, replay, bounded budget, positive operation cost, and a total terminalizer, transported residuals can be routed to explicit terminal statuses: ExactRepair, StabilizedSurvivor, OpenObstruction, LicensedLift, BudgetUnknown, NoRule, or Refused. The paper positions Wang–Buehler-style categorical transport as a useful grammar for candidate discovery episodes, then supplies the missing finite residual-terminalization boundary. It distinguishes transport residuals from authority-bearing terminal status, separates MDL/AIC or benchmark gates from certificates, and gives a finite realization-compatibility lemma connecting transported cokernel residuals to FOC quotient residuals under exact image-matching hypotheses. The release is supported by a Paper022 Lean4 stack of 37 files covering quotient-bridge kernels, terminalizer routing, gate/certificate separation, numeric-gate provenance, discovery certificate packets, authority firewalls, production-manifest interfaces, audit gates, and negative examples. These mechanizations certify local finite interfaces and examples; they do not claim production-scale scientific discovery, empirical validation, global convergence, or physical/quantum authority.
Jeremy H. Carroll (Fri,) studied this question.