CV094 — exp term difference — irrationality research

Exact named statement

forall d x y g N ab ac bb bc a0. ~d=0 ->
  y=x+g ->
  NatScaledExpRecurrence(d,x,ab,ac,N) ->
  NatScaledExpRecurrence(d,y,bb,bc,N) ->
  BetaAt(ab,ac,0,a0) ->
  BetaAt(bb,bc,0,a0) ->
  forall k a b c. Le(S k,N) ->
  BetaAt(ab,ac,S k,a) ->
  BetaAt(bb,bc,S k,b) ->
  BetaAt(bb,bc,k,c) ->
  Le(a,b) /\ Le(d*b,d*a+g*c)

PD0001 — Le · PD0013 — BetaAt · ND0443 — NatScaledExpRecurrence

Fully expanded target AST

Complete certificate and independent checks

40 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: b58a497476351e3cc07a976d42021351568e27076943567eb7a2186d2dbc51d9
Bundle SHA-256: 44a7cc4e855ca9dc684c975187a4d1ab6ca93a7159fb656c8487dcc8daff9ea6

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.

Scope

supplied exponential term recurrences with common nonzero denominator shared actual head and nonnegative argument gap have all index monotonicity and finite difference bound not derivative or infinite sum

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