AP061 — exp supplied large product — irrationality research

Exact named statement

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

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

Fully expanded target AST

Complete certificate and independent checks

255 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: 5b7c88d4d5aebd8dea844bd2f45f5a1966eacf6503b969bc711e7b8e1bc1163d
Bundle SHA-256: bd5cfc30ebecd494e85593efcf0c03cd77f252288449cc975a0d04d79cc5c861

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 · AP051 · AP052 · AP053 · AP054 · AP055 · AP056 · AP057 · AP059 · AP060 · CV008 · CV009 · CV011 · CV043 · CV044 · CV046 · CV047 · CV048 · CV068 · CV095

Scope

retain three independently supplied exponential tables heads and sums with general argument product error using unrestricted recurrence value independence and no analytic addition axiom

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