Exact named statement
forall ab ac L bb bc M r s N. NatZeroAfter(ab,ac,L,r) ->
NatZeroAfter(bb,bc,M,s) ->
exists cb cc. NatConvolutionPrefix(ab,ac,L,bb,bc,M,cb,cc,N) /\ NatZeroAfter(cb,cc,N,r+s)Complete certificate and independent checks
127 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: 10fb7e6300ce6b56bf6d231d7f357343629838d1ed95469a0309b42e521c276a
Bundle SHA-256: eb53e85a3f7f6adb863962998a2b23b4c0e83382b1cec2a9e0e971829a777a45
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
constructed actual convolution with output zero after sum of explicit input cutoffs not power support or analytic tail estimate
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.