AP039 — exp convolution prefix — irrationality research

Exact named statement

forall d x y ab ac bb bc N a0 b0. NatScaledExpRecurrence(d,x,ab,ac,N) ->
  NatScaledExpRecurrence(d,y,bb,bc,N) ->
  BetaAt(ab,ac,0,a0) ->
  BetaAt(bb,bc,0,b0) ->
  exists cb cc s. (NatConvolutionPrefix(ab,ac,S N,bb,bc,S N,cb,cc,S N)) /\ ((NatScaledExpRecurrence(d,x+y,cb,cc,N)) /\ ((BetaAt(cb,cc,0,a0*b0)) /\ ((Sum(cb,cc,S N,s)) /\ ((forall j t f p q. Le(j,N) ->
  BetaAt(cb,cc,j,t) ->
  Factorial(j,f) ->
  Pow(d,j,p) ->
  Pow(x+y,j,q) ->
  (t*f)*p=(a0*b0)*q)))))

PD0001 — Le · PD0013 — BetaAt · PD0015 — Sum · ND0402 — NatConvolutionPrefix · PD0020 — Pow · PD0023 — Factorial · ND0443 — NatScaledExpRecurrence

Fully expanded target AST

Complete certificate and independent checks

163 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: b2b010de8d9310bb2658728077ab0ed46dd768c452df5ea955fad36a1c6b40aa
Bundle SHA-256: eb3be34e7edbee2ca6fb1e7702208c35ab377dde25d37f3e7ea8225883911543

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.

AP035 · AP037 · AP038

Scope

construct the actual finite convolution prefix and sum prove its product head added argument recurrence and all index factorial normalization without equating the truncated sum with the full product of input sums

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