CV098 — exp cross 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 ->
  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) ->
  Le(b0*s,a0*t) /\ Le((d*e)*(a0*t),(d*e)*(b0*s)+9*(g*(a0*b0)))

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

Fully expanded target AST

Complete certificate and independent checks

156 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: cd70bc49ad3f8d993f61ab9ed4f3acc069f1cd0aac88b3f00bfd88e97d93da9c
Bundle SHA-256: e4d094f2bd99f93d7c2951a5a03e735e0d7ba193e0b6c117d1385ed11a50bc8d

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

Scope

supplied finite exponential recurrences with independent nonzero denominators and arbitrary initial scales obey cross multiplied continuity by constructing actual rescaled tables and sums not code equality or analytic limit

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