A CApprox computation and exact rational evaluation establish |P(u_precision)|>2*M_P*2^(-precision), with M_P=1+sum(j>=1,j*abs(a_j)*2^(j-1)).
Proposed arity: 3. Parameters: poly precision witness. No reviewed kernel definition exists yet.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.