AP058 — exp normalized witness — irrationality research

Exact named statement

forall d x L K m N. ~d=0 ->
  Le(x,L*d) ->
  Le(2*L,K) ->
  exists wb wc tb tc h f q t p B s. (NatExpWeightTable(d,(K+m)+N,wb,wc)) /\ ((NatPowerWeightedPrefix(x,wb,wc,tb,tc,S((K+m)+N))) /\ ((BetaAt(wb,wc,0,h)) /\ ((BetaAt(tb,tc,0,h)) /\ ((~h=0) /\ ((Factorial((K+m)+N,f)) /\ ((Pow(d,(K+m)+N,q)) /\ ((h=f*q) /\ ((Sum(tb,tc,S((K+m)+N),t)) /\ ((NatScaledExpRecurrence(d,x,tb,tc,(K+m)+N)) /\ ((forall j v fj dj xj. Le(j,(K+m)+N) ->
  BetaAt(tb,tc,j,v) ->
  Factorial(j,fj) ->
  Pow(d,j,dj) ->
  Pow(x,j,xj) ->
  (v*fj)*dj=h*xj) /\ ((Pow(2,m,p)) /\ ((~p=0) /\ ((Pow(L,K,B)) /\ ((Sum(tb,tc,K+m,s)) /\ ((Le(s,t)) /\ (Le(p*t,p*s+2*(B*h))))))))))))))))))

PD0001 — Le · PD0013 — BetaAt · PD0015 — Sum · ND0423 — NatExpWeightTable · PD0020 — Pow · PD0023 — Factorial · ND0442 — NatPowerWeightedPrefix · ND0443 — NatScaledExpRecurrence

Fully expanded target AST

Complete certificate and independent checks

184 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: d7fe383cf8b88b0d32538bcdd03ef48992ec2b80666f1188f153a402dde188e5
Bundle SHA-256: df0dfd944205f1586fc319d7674976003be31c2c08bfe39b5a678294a9277e16

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.

AP051 · AP052 · AP053 · AP054 · AP055 · AP056 · AP057 · CV009 · CV022 · CV030 · CV068 · CV069 · CV070

Scope

construct actual factorial weighted exponential tables positive original normalization both powers and sums with original head normalized finite tail error for arbitrary bounded arguments without an analytic exponential

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