CV097 — exp rescaling — irrationality research

Exact named statement

forall d x f c N ab ac a0 s. NatScaledExpRecurrence(d,x,ab,ac,N) ->
  BetaAt(ab,ac,0,a0) ->
  Sum(ab,ac,S N,s) ->
  exists ub uc t. NatLinearTriple(c,0,1,ab,ac,ab,ac,ub,uc,S N) /\ (NatScaledExpRecurrence(d*f,f*x,ub,uc,N) /\ (BetaAt(ub,uc,0,c*a0) /\ (Sum(ub,uc,S N,t) /\ (t=c*s))))

PD0013 — BetaAt · PD0015 — Sum · ND0409 — NatLinearTriple · ND0443 — NatScaledExpRecurrence

Fully expanded target AST

Complete certificate and independent checks

114 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: 1366d756cc52f3aeda1363ed3188f534bc5489ed2977f09a101be2c92e875243
Bundle SHA-256: 571d69eb382e46b1bd32c0d1a0b8ef59d2b3ca43a214e92a0e9ddcacd0191b0a

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

construct actual scaled exponential table recurrence at common multiplied denominator scaled head and exact scaled sum including zero scalars and degree no code equality or rational validity assumption

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