CV101 — exp two error bound — irrationality research

Exact named statement

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

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

Fully expanded target AST

Complete certificate and independent checks

189 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: 99e2c67d567497309e07b57a9c96266fe4299a7a38f24bf605373710dc0b6857
Bundle SHA-256: ac305ff130d7a1936202c1022e0aa06acc322a556ae0d6684918bc30cb5533bd

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 · CV068 · CV087 · CV088 · CV094 · CV095 · CV096 · CV097 · CV098 · CV100

Scope

supplied finite exponential sums with independent arguments denominators heads and ordered horizons have combined argument and cutoff error via constructed middle prefix and checked polynomial order no analytic limit

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