AP052 — exp large argument tail — irrationality research

Exact named statement

forall d x L tb tc M N. ~d=0 ->
  Le(x,L*d) ->
  Le(2*L,M) ->
  NatScaledExpRecurrence(d,x,tb,tc,M+N) ->
  exists ub uc a s. (NatAffineSlice(tb,tc,M,1,ub,uc,S N)) /\ ((NatRatioBoundPrefix(ub,uc,1,S N)) /\ ((BetaAt(tb,tc,M,a)) /\ ((BetaAt(ub,uc,0,a)) /\ ((Sum(ub,uc,S N,s)) /\ (Le(s,2*a))))))

PD0001 — Le · PD0013 — BetaAt · PD0015 — Sum · ND0411 — NatAffineSlice · ND0441 — NatRatioBoundPrefix · ND0443 — NatScaledExpRecurrence

Fully expanded target AST

Complete certificate and independent checks

123 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: bb49801153c9bc3821d1f494707843d81d2f5e20181f6172563fe79531ae95eb
Bundle SHA-256: 911984292a5e6478f05be815332b1ea99357351be9c5150149a0930b1da3293a

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 · CV068

Scope

construct the actual shifted tail head halving relation and sum of a supplied exponential recurrence at any cutoff at least twice its natural argument bound with finite sum at most twice the head including zero cutoffs without an infinite tail

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