Audited Operational Realisability: Canonical Inference Closure and Evidence-Preserving Composition

Conditional mathematical arguments need careful bookkeeping: which obligations were incurred, which have been addressed, and which were addressed in a way that actually proves the target. Audited Operational Realisability (AOR) is a mathematical theory of this bookkeeping. An audit state consists of demanded records and stored certificates; each certificate carries a status, such as budgeted or blocked, and a payload whose meaning is fixed in advance. We separate three conclusions that are easily conflated. Inference closure registers every dependency of a demanded record, accounting requires a stored certificate for each demanded or dependency-reachable record, and delivery requires a certificate whose status an explicit consumer policy accepts as proving its target. A certificate recording that a budget is exceeded accounts for the obligation but does not deliver feasibility to a consumer who requires it. We prove that inference closure is a reflection that creates no evidence, in a category whose arrows preserve certificates exactly, and that this category has colimits in which every accepted certificate is already stored at some object of the diagram. For operations that add evidence, we prove finite completion when every unaccounted state satisfying an invariant admits a legal step that preserves the invariant and lowers a natural-number rank, and confluence under replayability, and we strictly separate accounting, recoverability, and uniform quantitative control. Retained evidence passes to increasing unions, and witnesses pass to limits under compactness and closed validity, provided an accepted payload is returned at the limit; without compactness they may escape. Two examples mark the boundary of accounting: a query system that pays its declared costs, is accounted, and identifies each hidden world along its exhaustive run, yet admits no finite-stage guarantee uniform over all worlds; and a target on binary streams, Lipschitz for the first-difference metric, whose shrinking finite-prefix certificates, priced within a summable credit, are all accepted, with centers converging to the target. The numbered theorems and the lemma are formalized in Lean 4 with Mathlib; the analytic estimates of applications remain explicit hypotheses.