AP073 — exp bounded majorant — irrationality research

Exact named statement

forall L d x N ab ac h s C. ~d=0 ->
  Le(x,L*d) ->
  NatScaledExpRecurrence(d,x,ab,ac,N) ->
  BetaAt(ab,ac,0,h) ->
  Sum(ab,ac,S N,s) ->
  Pow(9,S L,C) ->
  Le(s,C*h)

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

Fully expanded target AST

Complete certificate and independent checks

281 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: b50deb3120bcff57e9f7bb87d27d0227041c2cae062f4de207339d31f41a23ff
Bundle SHA-256: 9b94bb19dbf67b5b77d0f8e7315675f73673189d0c87d1989f2e93ee18c07d2f

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.

AP037 · AP038 · AP040 · AP041 · AP060 · AP068 · AP069 · AP071 · AP072 · CV008 · CV009 · CV011 · CV022 · CV030 · CV043 · CV044 · CV046 · CV047 · CV048 · CV069 · CV070 · CV094 · CV095 · CV097

Scope

prove a horizon independent power majorant for every actual bounded rational argument by constructing a positive integer argument reference and cancelling only its head without an analytic axiom

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