AP074 — exp bounded continuity — irrationality research

Exact named statement

forall L d e x y g N ab ac bb bc a0 b0 s t C r. ~d=0 ->
  ~e=0 ->
  Le(x,L*d) ->
  Le(y,L*e) ->
  Le(d*y,e*x+g) ->
  Le(e*x,d*y+g) ->
  NatScaledExpRecurrence(d,x,ab,ac,N) ->
  NatScaledExpRecurrence(e,y,bb,bc,N) ->
  BetaAt(ab,ac,0,a0) ->
  BetaAt(bb,bc,0,b0) ->
  Sum(ab,ac,S N,s) ->
  Sum(bb,bc,S N,t) ->
  Pow(9,S L,C) ->
  Le((r*g)*C,d*e) ->
  Le(r*(b0*s),r*(a0*t)+a0*b0) /\ Le(r*(a0*t),r*(b0*s)+a0*b0)

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

Fully expanded target AST

Complete certificate and independent checks

288 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: 33db4b325e45a75d8927db006e7cc1ae244b680af38c9eda0005ba8149899723
Bundle SHA-256: e8deaebfa9c117104743c0ae0298c1d8cffe8f8ccf5f713f332a46ffeb48873e

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 · AP060 · AP068 · AP069 · AP070 · AP071 · AP072 · AP073 · CV008 · CV009 · CV011 · CV022 · CV030 · CV043 · CV044 · CV046 · CV047 · CV048 · CV069 · CV070 · CV094 · CV095 · CV097

Scope

prove two sided absolute continuity of actual independent bounded finite exponential computations by a checked power majorant decidable order split and explicit precision budget without an analytic limit claim

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