Positive-denominator RatEq is reflexive, symmetric and transitive; signed numerator pairs may be noncanonical.
Method: native-ring. Induction: none. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.
Planned prerequisites and notation
Open this dependency coneChecked supporting leaves, not parent closure
- RF001 — Reflexive
- RF002 — Symmetric
- RF003 — Transitive
- RF004 — Scale nonzero
- RF005 — Numerator shift
- RF006 — Negation compatible
The planning contract above remains open. Checked arithmetic DAG · Complete execution evidence.