Lower proven unsigned subtraction into Core without weakening totality #210

Problem

The public application build at Edict main
3f81f759e921a69b04fe8cf8e62e62f8f3dc7b7e rejects an authored unsigned
difference even when the input contract proves that it cannot underflow:

where input.lower <= input.upper
{
  let distance: U64 = input.upper - input.lower;
  return { distance };
}

Reproduced by adding the actual deleted-byte-count expression to Jim's
application from flyingrobots/jedit#302. The public JSONL application build
returns ApplicationCompilationFailed with a TypeCheck
UnsupportedSourceShape at the subtraction. This is an Edict language gap,
not an Echo application operation.

Intended compiler scope

• Lower U32 and U64 subtraction only when a conservative compiler proof
  establishes no underflow from exact operands, literal bounds, or dominating
  conjunctive input constraints.
• Preserve unsigned width and operand order in canonical Core.
• Reject absent/reversed/disjunctive evidence, incompatible widths, and signed
  operands outside this slice. Evidence must not leak between intents or apply
  to basis/constraint evaluation before it has been checked.
• Keep target support explicit. A source-to-Core result does not establish
  Target/package/runtime support; downstream verifiers must independently check
  totality before accepting the operation.
• Update the language specification and compiler-spine requirement/test matrix.

Evidence

Positive witnesses must exercise compile_to_core; negative witnesses must
assert structured errors. Changes to operands, guard, or width must alter Core
meaning or reject. The public Jim build must advance beyond its current source
error before this compiler slice is complete.

Related: #192, flyingrobots/jedit#296, flyingrobots/echo#684.

No application vocabulary, rope helper, native callback, unchecked wrapping or
trapping arithmetic, or claim of end-to-end editing is in scope for this issue.