CV003 — natural convolution — irrationality research

Exact named statement

forall ab ac L bb bc M N. exists cb cc. NatConvolutionPrefix(ab,ac,L,bb,bc,M,cb,cc,N) /\ (forall eb ec. NatConvolutionPrefix(ab,ac,L,bb,bc,M,eb,ec,N) ->
  (forall j a. Lt(j,N) ->
  BetaAt(cb,cc,j,a) ->
  BetaAt(eb,ec,j,a)))

PD0002 — Lt · PD0013 — BetaAt · ND0402 — NatConvolutionPrefix

Fully expanded target AST

Complete certificate and independent checks

126 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: b5ad2ef80b9ae8fd100f25b2a128eac7af5d8d58a783e89d2aab7f5bf9c4b0d8
Bundle SHA-256: ce973e6781fe1dd61db9e92cb368d4a86875740fa2a5cf0c744884a56486588b

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 unique finite natural convolution not power tables or IR079

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