Decode three rational triples; RatLt-or-RatEq(lo,q) and RatLt-or-RatEq(q,hi). Decoding witnesses remain explicit.
Proposed arity: 3. Parameters: q lo hi. No reviewed kernel definition exists yet.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.