AP059 — exp large argument product — irrationality research

Exact named statement

forall d x y L ab ac bb bc K m a0 b0 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)) ->
  BetaAt(ab,ac,0,a0) ->
  BetaAt(bb,bc,0,b0) ->
  Pow(2,S m,p) ->
  Pow(L,K,B) ->
  exists cb cc u v s t. (NatConvolutionPrefix(ab,ac,S(S(K+m)+(K+m)),bb,bc,S(S(K+m)+(K+m)),cb,cc,S(S(K+m)+(K+m)))) /\ ((NatScaledExpRecurrence(d,x+y,cb,cc,S(K+m)+(K+m))) /\ ((BetaAt(cb,cc,0,a0*b0)) /\ ((Sum(ab,ac,S(K+m),u)) /\ ((Sum(bb,bc,S(K+m),v)) /\ ((Sum(cb,cc,S(K+m),s)) /\ ((Sum(cb,cc,S(S(K+m)+(K+m)),t)) /\ ((Le(s,u*v)) /\ (Le(p*(u*v),p*s+2*(B*(a0*b0)))))))))))

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

Fully expanded target AST

Complete certificate and independent checks

248 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: 7b046134336250ad84a04def0d99f230641a6586ae277d5538980db4b66aa271
Bundle SHA-256: 67a11f71c4bf3e2627a1a9312bcd6c03448719f660047da1f33d10d257b59445

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 · CV008 · CV009 · CV011 · CV043 · CV044 · CV046 · CV047 · CV048 · CV068 · CV095

Scope

construct the actual finite exponential Cauchy product recurrence head and four sums with an original head normalized quantitative product error for arbitrarily bounded arguments without an exponential addition axiom

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