IR025 — Canonical approximation totality

For every n, CApprox(n,up,um,ud,trace) has witnesses with ud>0; results are unique up to RatEq. No unbounded numerical search is part of this algorithm.

Method: native-induction. Induction: finite algorithm traces. Risk: routine.

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

Planned prerequisites and notation

• IR014 — Dyadic sqrt2 enclosures
• IR017 — Logarithm series remainder
• IR019 — Exponential partial-sum totality
• IR005 — Finite rational folds
• IRD09 — CApprox