For the finitely many named rational-sequence codes used here, prove addition/product/reciprocal enclosure transport with explicit input-precision moduli; no quantification over arbitrary functions.
Method: native-induction. Induction: precision. Risk: critical.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.