AP075 — exp dyadic continuity — irrationality research

Exact named statement

forall L d e x y g n N ab ac bb bc a0 b0 s t r p. ~d=0 ->
  ~e=0 ->
  Le(x,L*d) ->
  Le(y,L*e) ->
  Le(d*y,e*x+g) ->
  Le(e*x,d*y+g) ->
  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) ->
  Pow(2,n,r) ->
  Pow(2,S(9*(S L)+n),p) ->
  Le(p*g,d*e) ->
  ~r=0 /\ (~p=0 /\ (Le(r*(b0*s),r*(a0*t)+a0*b0) /\ Le(r*(a0*t),r*(b0*s)+a0*b0)))

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

Fully expanded target AST

Complete certificate and independent checks

299 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: 52a66a0660b914cf13ff19d92ee7d59293e729e8ef8813555714e427ec0646c4
Bundle SHA-256: 619b8df88cde20ce381fc9c7a79e48d8c81e09e3824a99bd36b97584bee770af

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 · AP062 · AP068 · AP069 · AP070 · AP071 · AP072 · AP073 · AP074 · CV008 · CV009 · CV011 · CV022 · CV030 · CV043 · CV044 · CV046 · CV047 · CV048 · CV069 · CV070 · CV094 · CV095 · CV097

Scope

prove an explicit linear dyadic input precision modulus for two actual bounded finite exponential computations by constructing the majorant power and reusing the checked symbolic binary budget without changing the original approximation program

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