Validate proven unsigned subtraction independently at the Target IR boundary #212

Observable outcome

The public application build accepts the source-to-Core core.integer.subtract<U32/U64> form at the generic Target IR boundary only when independent validation establishes its type and totality. This advances jedit #302 past its newly observed TargetLoweringFailed / InvalidCoreIdentity failure without trusting compiler success as proof.

Evidence

With jedit 83ab52a3744babb63c8ce15cd94d917012e364a2, its pinned Echo provider 49e9efb68001dfd78563d18bac9359a87671e431, and the compiler change in #211, an isolated source copy that returns input.endByte - input.startByte under the existing ordered-range constraint compiles to Core but fails target expression authorization. The current target validator recognizes string concatenation and authenticated lawpack helpers, not this new integer primitive.

Scope

• Preserve unsigned width, argument order, constraints, identity, and semantic closure in generic Target IR.
• Independently validate raw Core: same-width unsigned operands, correct arity/type arguments, domination of exact operand order or unconditional totality.
• Refuse mutated/missing/reversed/disjunctive guards, signed/mixed-width operands, invalid constants, scope leakage, and arithmetic in metadata that relies on not-yet-established predicates.
• Preserve structured failure behavior and existing target artifact compatibility.
• Exercise public source-to-Core-to-target lowering and adversarial Core mutations; advance the real Jim application witness to the next explicit provider boundary.

Exclusions

No Echo application-specific operation, native rope callback, unchecked arithmetic, completed rope algorithm, or production editor cutover. Echo provider verification and interpretation remain separately owned under flyingrobots/echo#684.

Prerequisite and safe merge state

Depends on #210 / #211 for the public source-to-Core operation contract. After this slice, Edict's target boundary is independently safe while unsupported providers can still reject the operation explicitly. Existing producer pins in jedit remain unchanged until an independently verified integration update.

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