feat(formal): the trade-intent correspondence, and the proof that its forbidden shape is vacuous

[cryptskii]

Amendment 2c-E §8.3.

The obligation was wrong, and it is corrected rather than ticked off

§8.3 said the formal predicate consuming TradeIntent should be updated. There was none. Zero references across lean4/ and tla/, to TradeIntent or to any of the four retired members.

So "remove every formal dependency on the retired members" is discharged vacuously, and the amendment now records it as vacuous rather than as done. The real work was to author the predicate.

The module

lean4/DSMTradeIntentCorrespondence.lean, the fifteenth, machine-checks SAT.1–SAT.6 for the six-field exact-output intent.

The market policy is a parameter, so the model fixes no pricing rule, no rounding and no admissibility condition — it proves the shape of the correspondence for any policy. A sample policy exists only to make the counterexamples closed terms the kernel can decide.

The load-bearing result

the_tautological_form_accepts_the_forgery. The forbidden shape — SAT.5 compared against the route's own claim instead of the authenticated V_n — accepts a trade the real predicate refuses.

The two are therefore provably different predicates. That was the specific risk in the ruling: an intent field defined as a function of the selected route turns the satisfaction check into a self-attestation. It is now refuted rather than warned against.

Teeth, one conjunct at a time

An unsigned route, either token swapped, an unsigned amount, an unsigned nonce, a leg count that is not the signed one, and a fee that is not the vault's are each refused separately. The leg-count check is what replaced schema 1's max_hops, and it reads a signed fact rather than a bound carried in the intent it bounds.

Plus one general theorem rather than only examples: a disagreeing output never satisfies, for any policy.

Mutation controls, executed

Reported from the kernel's actual output, not predicted.

mutation	result
SAT.5's operand ← the route's claim	two named theorems proved FALSE, not merely broken; a third loses its proof
SAT.6 removed	a_fee_that_is_not_the_vaults_is_refused proved FALSE

I predicted the first would merely break the second theorem. The kernel refutes it, which is stronger, and the header says what the kernel printed.

Axioms

Per-theorem report included. Five results depend on no axioms at all; only the general theorem reaches simp and takes propext and Quot.sound. decide throughout rather than native_decide, which would add ofReduceBool and trustCompiler and move the proof out of the kernel.

Housekeeping

CI module pin 14 → 15. Two stale live counts corrected. The 2c-C4 history entry saying it landed the fourteenth is left alone, because it records what was true then.

Verification

All 15 modules kernel-check clean under -DwarningAsError=true, which is what the sorry-free claim actually rests on. make lint green; production safety checks green. The edited workflow YAML was re-parsed.

Note on Formal Validation: if that check fails here, it is not this change. There is a pre-existing intermittent java.lang.ArithmeticException: Division by zero in TLC, which hit DSM_small on an earlier main commit and DSM_system on #830. Details in a separate task rather than folded in here.