Exact named statement
∀ x. ∀ y. ∀ z. ∀ n. ∀ m. ∀ k. m + (x · n + y · z) = x · z + y · n + k → ¬x = y → ¬z = n → ¬m = kNo displayed named abbreviation.
Complete certificate and independent checks
34 actual local proof nodes. Each node carries its complete ordinary HA proof body.
Full canonical proof bundle · Original HA receipt · Independent Lean receipt
Target SHA-256: ee1a6a3a9dfc5f7d45c67d4a040a8ff0ccf2d4422f2ddc42e1fad69334c2d581
Bundle SHA-256: e0fd91506b33ed8a390173ed0599e8980e2c99ade59b24c37be92cf05bcfbc38
Checked statement containment
These exact targets occur inside this certificate. These links summarize containment, not direct dependency arrows; the downloadable bundle records every private lemma and ordered edge.
Scope
signed integer binary nonzero not quadratic finite IR046
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.