CV102 — exp rational two error — 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 ->
  ~a0=0 ->
  ~b0=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) ->
  IRatLe(s,0,a0,t,0,b0) /\ IRatLe(t,0,b0,(d*e)*(p*s)+(9*(g*p)+2*(d*e))*a0,0,(d*e)*(p*a0))

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

Fully expanded target AST

Complete certificate and independent checks

193 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: f3522601cd0c5260ecf6f5cde1c301a2d74e3f5b53f165eea0ef9f3bf32c837c
Bundle SHA-256: dc1c490b0ea909db229a2530e7eb7c1ef55ea80df983a1c1351582e8c4802062

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

Scope

independently supplied exponential computations at ordered arguments and distinct horizons have valid rational bounds with separate argument and dyadic tail errors after proving all denominators and cutoff power nonzero 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.