AP036 — exp recurrence series — irrationality research

Exact named statement

forall d x tb tc N h. ~d=0 ->
  ~h=0 ->
  NatScaledExpRecurrence(d,x,tb,tc,N) ->
  BetaAt(tb,tc,0,h) ->
  forall j t. Le(j,N) ->
  BetaAt(tb,tc,j,t) ->
  exists f0 p0 q0. (Factorial(j,f0)) /\ ((Pow(d,j,p0)) /\ ((Pow(x,j,q0)) /\ ((~f0=0) /\ ((~p0=0) /\ (IRatEq(t,0,h,q0,0,f0*p0))))))

PD0013 — BetaAt · PD0020 — Pow · PD0001 — Le · PD0023 — Factorial · ND0443 — NatScaledExpRecurrence · ND0383 — IRatEq

Fully expanded target AST

Complete certificate and independent checks

130 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: 88e50501342eaa8afeb980d49d5c37f6d456c6f32acfa9cabd11f610e93e959c
Bundle SHA-256: c15e4cf76dd83de836f3bbd457e0e5a21ae6779ee70dc926cd75fcecbb7e1aa6

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.

AP035

Scope

identify every actual supplied exponential recurrence term with its valid rational factorial series value constructing the factorial and both powers from retained generic proofs without an infinite series claim

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