CV099 — exp rational continuity — irrationality research

Exact named statement

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

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

Fully expanded target AST

Complete certificate and independent checks

159 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: 82b80b04322470f648dfee85b1aab63cea1636dce56258cd64822934f90d7e32
Bundle SHA-256: a8da7ae8b4871484dc4eef2f3e675c1bfae67c2c29c1240fcbf03895414f3c6b

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 finite exponential sums with independent positive denominators and heads have valid rational monotonicity and nine times argument difference bound after explicit nonzero denominator proofs 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.