Biochemical readouts that preserve native function Reporter storage, finite-time inference and certified recovery in a shared cofactor pool

A reporter that consumes a regenerated cofactor also stores it: while the cofactor sits in a reporter complex it is available neither to the native reaction it is meant to report on nor to the regenerating reaction that would replenish it. We show that this storage makes a reporter’s effective turnover activity insufficient to determine its effect on native function. For an explicit mass-action source in which the reporter complex is retained, the complete-recovery native-output loss per reporter product equals $k(p+c)/\bigl(c(p+k)\bigr)$, with $p$ the regeneration coefficient, $k$ the native-use coefficient and $c$ the reporter’s catalytic release coefficient. The instantaneous-turnover idealisation predicts $k/(p+k)$; the discrepancy is the factor $1+p/c$, which is a factor of six at $p=1$, $c=0.2$. The identity is an invariant of the source rather than of a schedule: it holds for every nonnegative, time-varying association profile of finite total exposure, so no dosing or gating strategy removes it at fixed final reporter product. We then give general design inequalities that make a finite readout simultaneously preserving and discriminating, and a rational witness: over a declared uncertainty region for nine parameters, an eight-unit acquisition suppresses native flux by less than $4.73\%$ throughout acquisition and recovery, while separating two promised functional classes with a residual detector margin of $1214759671/218587500000>0.0055$. Ideal shut-off is not required: if the post-acquisition association flux decays at rate $\gamma$, an explicit convolution bound converts $\gamma$ into a certified recovery deadline, five time units at $\gamma\ge21$ and $11.2$ at $\gamma=1$, while the additional cumulative loss is bounded by $\mathcal{R}_{\mathrm{extra}}\le (k/a)(1+p/c)uC/\gamma$ and is not zero. Dropping the two-class promise, set inversion of the same envelopes returns an outer interval for the regeneration capacity and hence for the classified native flux, with no distributional assumption added. Replacing the linear rates by increasing differentiable ones yields a divided-slope sandwich for the cost per product that collapses to the linear coefficient in the low-saturation limit. A negative result limits all of this: an unobserved background consumer makes native and total cofactor use observationally indistinguishable, so reporter data alone cannot identify native function without an independent native-specific calibration. Source algebra, the finite integral account, the nonlinear sandwich, the exponential recovery certificates and the exact decision arithmetic are verified in Lean 4; existence, invariance, comparison and convergence are conventional proofs. This is a conditional methods theorem with a prospective biochemical implementation, not an empirically validated assay.