Finite positive rational expression bounding the difference between AuxJet at a/b and the fixed-exponential jet, under |c-a/b|<=eps. This definition records the expression, not its validity.
Proposed arity: 9. Parameters: a b q coeff ell k eps bound trace. No reviewed kernel definition exists yet.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.