Exact named statement
∀ x. ∀ y. ∀ z. ∀ n. ∀ m. ∀ k. ∀ i. ∀ j. ∀ u. ∀ v. ∀ w. ∀ x0. (∀ x1. ∀ x2. S x1 ≤ i → S x1 ≤ z ∧ (S x2 ≤ S (S x1 · y) ∧ (∃ x3. x = x3 · S (S x1 · y) + x2)) ∨ z ≤ x1 ∧ x2 = 0 → x2 = 0) → (∀ x1. ∀ x2. S x1 ≤ j → S x1 ≤ k ∧ (S x2 ≤ S (S x1 · m) ∧ (∃ x3. n = x3 · S (S x1 · m) + x2)) ∨ k ≤ x1 ∧ x2 = 0 → x2 = 0) → S u ≤ i + j → (∀ x1. S x1 ≤ S u → ∃ x2. S x2 ≤ S (S x1 · w) ∧ (∃ x3. v = x3 · S (S x1 · w) + x2) ∧ (∃ x3. ∃ x4. ∃ x5. x1 + x3 = u ∧ ((S x1 ≤ z ∧ (S x4 ≤ S (S x1 · y) ∧ (∃ x6. x = x6 · S (S x1 · y) + x4)) ∨ z ≤ x1 ∧ x4 = 0) ∧ ((S x3 ≤ k ∧ (S x5 ≤ S (S x3 · m) ∧ (∃ x6. n = x6 · S (S x3 · m) + x5)) ∨ k ≤ x3 ∧ x5 = 0) ∧ x2 = x4 · x5)))) → (∃ x1. ∃ x2. 1 ≤ S (1 · x2) ∧ (∃ x3. x1 = x3 · S (1 · x2) + 0) ∧ (S x0 ≤ S (S S u · x2) ∧ (∃ x3. x1 = x3 · S (S S u · x2) + x0) ∧ (∀ x3. S x3 ≤ S u → ∃ x4. ∃ x5. ∃ x6. S x4 ≤ S (S x3 · w) ∧ (∃ x7. v = x7 · S (S x3 · w) + x4) ∧ (S x5 ≤ S (S x3 · x2) ∧ (∃ x7. x1 = x7 · S (S x3 · x2) + x5) ∧ (S x6 ≤ S (S S x3 · x2) ∧ (∃ x7. x1 = x7 · S (S S x3 · x2) + x6) ∧ x6 = x5 + x4))))) → x0 = 0No displayed named abbreviation.
Complete certificate and independent checks
28 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: b5ca16c60cf9aff317a93603448843e717d17228380fb7c1a1287e31f12e5e22
Bundle SHA-256: 93d3871e7c7f06fc5974b61bec48616a7a7f13e6f919bf7dbf34570624e918b6
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
universal natural convolution vanishing not IR079
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.