AP007 — exp two sided continuity — irrationality research

Exact named statement

forall d e x y C R H N ab ac bb bc a0 b0 s t. ~d=0 ->
  ~e=0 ->
  Le(x,d) ->
  Le(y,e) ->
  Le(C*(d*y),C*(e*x)+R) ->
  Le(C*(e*x),C*(d*y)+H) ->
  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) ->
  Le(C*((d*e)*(a0*t)),C*((d*e)*(b0*s))+9*(R*(a0*b0))) /\ Le(C*((d*e)*(b0*s)),C*((d*e)*(a0*t))+9*(H*(a0*b0)))

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

Fully expanded target AST

Complete certificate and independent checks

164 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: d6c797957cd58e4b92514bcc10063e71045c1cdbe995aeeef3bff5020d434a11
Bundle SHA-256: 147d7fa32b4cefb244f3a689bf9241c30b0170bc7eb867723c690751b82423bc

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.

CV009 · CV094 · CV095 · CV096 · CV097 · CV098

Scope

supplied same degree finite exponential sums have two sided scaled error bounds without input monotonicity by constructive natural order and actual additive gap with independent denominator and head scales

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