Without assuming c=a/b: bound the selected actual jet by the IR059 analytic term plus W times the maximum of the true lower-jet residuals. Include normalization at the selected node and all 7r lower jets.
Method: native-order. Induction: none. Risk: critical.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.