Exact named statement
forall ab ac L bb bc M. exists rb rc x y z. NatConvolutionPrefix(ab,ac,L,bb,bc,M,rb,rc,L+M) /\ (Sum(ab,ac,L,x) /\ (Sum(bb,bc,M,y) /\ (Sum(rb,rc,L+M,z) /\ z=x*y)))Complete certificate and independent checks
162 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: 074045ab4db4d6936b3447f35096441e7ed3857f9eb93287ea1335d93cbad0dc
Bundle SHA-256: e36b7cbb77811b8fac027866066f3e9f28703f247168785b2c003b12e2efc7d7
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.
CV008 · CV009 · CV011 · CV043 · CV044 · CV046 · CV047
Scope
constructed full length natural convolution and all three sums with output sum equal to product of input sums via actual fubini not horner or analytic identity
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.