For the finitely many derivatives and functional coefficients in IR056, construct J(t,N,lambda,W) making every omitted Taylor contribution <2^-t, including the multiplied functional error. Explicitly bound all nodes and frequencies.
Method: native-induction. Induction: tail precision schedule. Risk: critical.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.
Planned prerequisites and notation
- IR020 — Exponential explicit tail
- IR054 — Finite exponential divided-difference estimate
- IR057 — Explicit interpolation coefficient bound
- IR012 — Approximation operations without real sorts
- IR077 — Finite Taylor derivative identity
- IR078 — Denominator-cleared confluent identity
- IRD08 — ExpPartial
- IRD21 — ConfluentFunctional