From enzyme activity to functional recovery: kinetic guarantees, sharp population bounds and measurement requirements

An enzyme assay reports a rate. A recovery claim concerns a trajectory. A population guarantee concerns how many trajectories complete a task. We treat these as three distinct objects and compute what each observation certifies about the next. For a prescribed, G6PD-inspired kinetic family we show that a finite nonnegative dual certificate on observed rate bands implies literal solutions and a uniform arrival deadline for every observation-compatible parameter vector, and we exhibit a parameter sequence along which every member eventually recovers while no common deadline exists. For finite weighted populations that differ only in catalytic capacity, with mean capacity one and support $[5/8,9/14]\cup[1,11/8]$, the set of fractions reaching the target by time $120$ is exactly $[20/41,1]$, although every such population has the same entire pooled clamped initial-rate response surface; a calibrated classification readout narrows the exact set to $[33/49,4/5]$, and one three-capacity construction realizes every value in both sets. These claims, including solution existence, are verified in Lean 4, as are the resulting minimax constants, the decision rule, and the weighting conversion. Ordinary analysis then quantifies what the modelling assumptions contribute: removing the support gap replaces the lower endpoint by an unattained infimum near $.1164$; allowing a fraction $\eta$ of off-band capacity gives a sharp interpolating infimum; equal mean and equal variance still permit recovery fractions $1/4$ and $3/4$; readout error and cell-weight normalization draw on one exactly computable margin; and the deadline-free limit of the guarantee is $197/407<1/2$, approached at the exponential rate $9/8470$ per unit model time with an explicitly identified prefactor. A row-span criterion decides when a further assay can help at all, and a monotone comparison theorem, together with a positive two-state counterexample, delimits transfer of the scalar threshold to multidimensional models. All numerical inputs are designed model values. The results specify measurement requirements; they do not supply a clinically calibrated recovery predictor.