AP060 — exp recurrence independence — irrationality research

Exact named statement

forall d e x y N ab ac bb bc h g s t. ~d=0 ->
  ~e=0 ->
  x*e=y*d ->
  NatScaledExpRecurrence(d,x,ab,ac,N) ->
  NatScaledExpRecurrence(e,y,bb,bc,N) ->
  BetaAt(ab,ac,0,h) ->
  BetaAt(bb,bc,0,g) ->
  Sum(ab,ac,S N,s) ->
  Sum(bb,bc,S N,t) ->
  g*s=h*t

PD0013 — BetaAt · PD0015 — Sum · ND0443 — NatScaledExpRecurrence

Fully expanded target AST

Complete certificate and independent checks

37 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: 7beddbf0b9c56535b34cc9097c02c1dd441a5ba9cb163ee87131584651dfc897
Bundle SHA-256: 87bd710ef99048e7cafb38dc72a681d8ea931d8054616880a6d04f87f4ecc748

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

prove cross value equality of two actual supplied exponential recurrences and sums at equal rational arguments without any argument bound or positive head assumption by one ordinary induction and existing sum linearity

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