IR003 — Rational order and decision

RatLt and RatEq are decidable; exactly one of x<y,x=y,y<x holds for valid triples; positive-denominator clearing preserves strict inequalities.

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

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

Planned prerequisites and notation

• IR001 — Rational representation equivalence
• IRD03 — RatLt

Checked supporting leaves, not parent closure

• NG001 — Constructive natural strict gap

The planning contract above remains open. Checked arithmetic DAG · Complete execution evidence.