CV001 — Universal convolution vanishing

Named statement

forall ab ac L bb bc M r s i db dc n.
  (forall j a. Lt(j,r) ->
  BetaZeroExtend(ab,ac,L,j,a) ->
  a=0) ->
  (forall j b. Lt(j,s) ->
  BetaZeroExtend(bb,bc,M,j,b) ->
  b=0) ->
  Lt(i,r+s) ->
  PolynomialDiagonalPrefix(ab,ac,L,bb,bc,M,i,db,dc,S i) ->
  Sum(db,dc,S i,n) ->
  n=0

If two natural coefficient tables vanish below indices r and s, an actually executed antidiagonal convolution below r+s sums to zero. The table, diagonal, and summation witnesses are explicit. This is not yet an ascending rational-series power theorem, formal exp composition, or an analytic tail estimate.

Exact original expanded HA target

∀ 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 = 0

Fresh HA and independently compiled Lean checks

Download the exact canonical proof bundle (gzip) · Original run record.

28 local nodes; 1,400 ordinary proof-body nodes. No receipt is substituted for a proof body.

Target AST SHA-256: b5ca16c60cf9aff317a93603448843e717d17228380fb7c1a1287e31f12e5e22
Certificate SHA-256: 93d3871e7c7f06fc5974b61bec48616a7a7f13e6f919bf7dbf34570624e918b6

Checked arithmetic DAG · Definition network · Larger IR079 planning cone · All current evidence.

IR072 remains open. This local exact certificate is not an Alpha/Stable admission or a completed irrationality proof.