AP042 — exp product error — irrationality research

Exact named statement

forall d x y ab ac bb bc n a0 b0 p. ~d=0 ->
  Le(x+y,d) ->
  NatScaledExpRecurrence(d,x,ab,ac,(S n)+n) ->
  NatScaledExpRecurrence(d,y,bb,bc,(S n)+n) ->
  BetaAt(ab,ac,0,a0) ->
  BetaAt(bb,bc,0,b0) ->
  Pow(2,n,p) ->
  exists cb cc u v s t. (NatConvolutionPrefix(ab,ac,S((S n)+n),bb,bc,S((S n)+n),cb,cc,S((S n)+n))) /\ ((NatScaledExpRecurrence(d,x+y,cb,cc,(S n)+n)) /\ ((BetaAt(cb,cc,0,a0*b0)) /\ ((Sum(ab,ac,S n,u)) /\ ((Sum(bb,bc,S n,v)) /\ ((Sum(cb,cc,S n,s)) /\ ((Sum(cb,cc,S((S n)+n),t)) /\ ((Le(s,u*v)) /\ (Le(p*(u*v),p*s+2*(a0*b0))))))))))

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

Fully expanded target AST

Complete certificate and independent checks

243 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: d0f60d98de139b481df7189728d38390769ed3a1530b9f2346887861df4da53a
Bundle SHA-256: 69283fcae5315a56746e333c6d6b9e3162d423ea3c9dc974a3218d0776975369

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.

AP037 · AP038 · AP040 · AP041 · CV008 · CV009 · CV011 · CV043 · CV044 · CV046 · CV047 · CV048 · CV068 · CV087 · CV088 · CV095 · CV100

Scope

construct actual added argument exponential convolution and bound the rectangular degree n product error by two times the product head over two to n using actual finite tails for x plus y at most d without an infinite identity

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