AP040 — convolution prefix order — irrationality research

Exact named statement

forall ab ac L bb bc M N O i u v. Le(L,N) ->
  Le(M,O) ->
  NatConvolutionCoefficient(ab,ac,L,bb,bc,M,i,u) ->
  NatConvolutionCoefficient(ab,ac,N,bb,bc,O,i,v) ->
  Le(u,v)

PD0001 — Le · ND0401 — NatConvolutionCoefficient

Fully expanded target AST

Complete certificate and independent checks

46 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: a4ddc6ed1dd2d269caed60e2cc1647676c11767abf060d3c1641e5d50ed1adb0
Bundle SHA-256: aaac37a0c2c53902ca053f77467100e9b542536f01288e2ba1d04e158e54a5d2

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.

CV095

Scope

prove order of actual convolution coefficients under both input prefix length extensions with fixed beta codes by padding product and finite sum order including empty lengths and all indices

None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.