Named statement
forall a b.
~(a=b) ->
exists k. (a+S k=b \/ b+S k=a)Unequal natural numbers have a positive additive gap, witnessed in one of the two directions. The proof uses the actual trichotomy body and checked addition commutativity. Z3 is an independent conjecture check, not the source of HA authority.
Exact original expanded HA target
forall a b. ~(a=b) -> exists k. (a+S k=b \/ b+S k=a)Fresh HA and independently compiled Lean checks
Download the exact canonical proof bundle (gzip) · Original run record.
3 local nodes; 192 ordinary proof-body nodes. No receipt is substituted for a proof body.
Target AST SHA-256: f0598e325456d7992079c20535c5d15740fb9f4a35c1a2619d5983c7ac9ac64b
Certificate SHA-256: e614473e462f9589988e7526d85de6427c03caca9edc9fc8ca5285514d1b1cc5
Checked arithmetic DAG · Definition network · Larger IR003 planning cone · All current evidence.
IR072 remains open. This local exact certificate is not an Alpha/Stable admission or a completed irrationality proof.