Proof available to an agent must be carried by retained, inspectable physical records. A declared proof interface determines which alternatives those records must separate and thereby induces a lower-bound family R(n). If the agent has work budget B < ∞ and every irreversible retained distinction costs at least ε > 0, then any instance satisfying εR(n) > B lies beyond that interface. The Physical Counting Impossibility Theorem therefore rules out universal exact proof for every fixed-budget substrate whenever R(n) is unbounded. Under Landauer/Bennett accounting, the ideal physical scale is ε ≥ k_BTln 2 per irreversible bit, experimentally verified to ±10%. For separable audit interfaces, exact query complexity gives R(n) = D(fₙ): parity requires n retained local distinctions, while a hidden n-bit truth table requires 2ⁿ. Global observables, compressed audits, interactive protocols, quantum witnesses, and finite survey catalogs define different evidence objects and therefore different families R(n). A reversible device may produce an answer and erase its scratch history; proof additionally requires the records licensed by the declared interface. Finite causal access supplies an independent bound on record acquisition.