AP043 — exp supplied product — irrationality research

Exact named statement

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

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

Fully expanded target AST

Complete certificate and independent checks

278 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: 926558364bf250779cdac1389ddfb0966bc77936da82f1e1a24e511ccefdcc45
Bundle SHA-256: 7528721c11078fdd7e425f270ff142f1629aeb9c0086f3426714067128d33823

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 · AP042 · CV008 · CV009 · CV011 · CV043 · CV044 · CV046 · CV047 · CV048 · CV068 · CV087 · CV088 · CV094 · CV095 · CV096 · CV097 · CV098 · CV100

Scope

transport the finite exponential product error to three actual supplied recurrences heads and short sums with independent output code and normalization using checked cross value identity and no infinite addition

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