IR026 — Canonical approximation accuracy

For k=n+8, the sqrt/log quotient error is <=2*2^-k and exponential truncation error <=2^-k; hence |u_n-exp(L/sqrt2)|<=7*2^-k<2^-n and 1<=u_n<=2.

Method: native-order. Induction: none. Risk: critical.

This is a human-readable planning contract, not a parsed kernel formula or accepted proof.

Planned prerequisites and notation

• IR015 — Sqrt2 algebra and strict bounds
• IR020 — Exponential explicit tail
• IR023 — Exponential order and Lipschitz
• IR024 — Log-exp inverse at two
• IR025 — Canonical approximation totality
• IRD09 — CApprox