x > 0 ∧ y > 0 ∧ Δx > 0 ∧ Δy > 0
x' = x + Δx ∧ y' = y − Δy
(1000·x + 997·Δx) · (y − Δy) ≥ 1000·x·y
Read the last line aloud and it is the rule as traders already state it: after charging three parts per thousand on the input, the product of the reserves may only grow. The constants are the familiar fee. The inequality rather than an equation is deliberate and faithful: a trade taking less than the maximum output still satisfies the sentence, so the predicate admits exactly the trades the rule admits. And Δy < y follows from the last line, so it needs no clause of its own. The first line earns its place. Without the funded-pool guard, a pool holding nothing of the input asset satisfies the inequality trivially, its right-hand side collapsing to zero, and could be drained of the output asset; with the guard, that transition is unprovable. On an execution platform this guard hides in initialisation code. Here it is one visible conjunct, and leaving it out is precisely the under-constrained failure the comparison page charges hand-built circuits with, except that here the omission sits in plain first-order text where reading finds it. Notice what else is absent. There is no swap function, no router, no ordering of internal operations, no reentrancy surface, because nothing executes. Any transition satisfying these three lines is a valid trade however it was assembled, and no transition violating them exists on the chain at all. The trader's own inputs answer to their own records' predicates, outside this contract. The mirror trade, paying the second asset and taking the first, is the same three lines with the roles of the two assets, and of their deltas, exchanged, and the pool's full contract is the disjunction of the two directions together with the deposit and withdrawal rules, proportionality equations of the same kind, two lines each. One more property falls out of the model. Relations run in both directions, so the sentence that checks a trade can answer one. An admissible output for a given Δx is the answer to an existential question, and the exact quote adds one further inequality, that one unit more of output would break the bound:(1000·x + 997·Δx) · (y − Δy − 1) < 1000·x·y
No quantifier is needed. The product is monotone in Δy, so being maximal and having the next unit up fail are the same condition. Asked with the output left open, the pair of inequalities returns one answer and then reports the search exhausted: for a pool holding 5000 and 3000, a trader paying 700 is quoted 367, and there is no second answer. Checking and quoting are one artifact, and the quote is derived by the sentence rather than supplied to it. Two trades against the same pool in one block contend for the same record. How Modulus clears contention for pooled state is part of the concurrency design, an open decision, and is documented when it is settled; the predicate above is independent of that answer.