AP037 — convolution shift — irrationality research

Exact named statement

forall alpha gamma ab ac L bb bc M cb cc K i u v. BetaZeroExtend(cb,cc,K,0,0) ->
  (forall j a c. Le(j,i) ->
  BetaZeroExtend(ab,ac,L,j,a) ->
  BetaZeroExtend(cb,cc,K,S j,c) ->
  gamma*c=alpha*a) ->
  NatConvolutionCoefficient(ab,ac,L,bb,bc,M,i,u) ->
  NatConvolutionCoefficient(cb,cc,K,bb,bc,M,S i,v) ->
  gamma*v=alpha*u

PD0001 — Le · ND0291 — BetaZeroExtend · ND0401 — NatConvolutionCoefficient

Fully expanded target AST

Complete certificate and independent checks

131 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: d3eb18cd8e8c76b563ea0fbc13a70b6de3140d1c177e036fa23a2411b01980b2
Bundle SHA-256: 66e3363a9ed58930f10db6803f0c605ec5bae24396b0b633a582fd2e26f462b3

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

transport a denominator cleared one place shift through actual finite convolution coefficients using the zero head and only required local indices with all input lengths and zero scalars allowed

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