HA + independent Lean evidence · Research, not Alpha admission

AP084 — log exp uniform two

Full irrationality (IR072/G121) remains open. Stable: 432. Alpha v35: 4,318. This checkpoint changes neither catalogue.

Exact named statement

forall n. exists r. Pow(2,n,r) /\ (~r=0 /\ (forall e bb bc l z q N eb ec b v. ~e=0 ->
  NatAtanhPrefix(e,bb,bc,(S(S(18*r)))+l) ->
  NatHornerValue(bb,bc,3,(S(S(18*r)))+l,z) ->
  Pow(3,(S(S(18*r)))+l,q) ->
  NatScaledExpRecurrence(e*q,3*z,eb,ec,(S(S(S(18*r))))+N) ->
  BetaAt(eb,ec,0,b) ->
  Sum(eb,ec,S((S(S(S(18*r))))+N),v) ->
  ~q=0 /\ (~(e*q)=0 /\ (Le(r*v,(r*2)*b+2*b) /\ Le((r*2)*b,r*v+b)))))

PD0001 — Le · PD0013 — BetaAt · ND0425 — NatAtanhPrefix · ND0437 — NatHornerValue · PD0020 — Pow · ND0443 — NatScaledExpRecurrence · PD0015 — Sum

Fully expanded target AST

Complete certificate and independent checks

511 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: 018632b34699a2f0f8feb879b56eb195d89cfb1304ffe2f5da46ef3ed3607898
Bundle SHA-256: 0bf21cd1c9bfc2162b766da7d48f010422e725cddc665f08f8d2b12460ef34ce

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.

AP032 · AP033 · AP034 · AP082 · AP083 · CV001 · CV002 · CV004 · CV008 · CV009 · CV011 · CV012 · CV019 · CV020 · CV021 · CV022 · CV024 · CV025 · CV027 · CV028 · CV029 · CV031 · CV032 · CV033 · CV037 · CV038 · CV039 · CV043 · CV044 · CV046 · CV047 · CV048 · CV049 · CV056 · CV057 · CV058 · CV059 · CV060 · CV061 · CV062 · CV063 · CV064 · CV065 · CV068 · CV072 · CV073 · CV075 · CV077 · CV078 · CV079 · CV081 · CV082 · CV083 · CV084 · CV086 · CV087 · CV088 · CV089 · CV090 · CV092 · CV093 · CV094 · CV095 · CV096 · CV097 · CV098 · CV100 · CV101

Scope

construct one actual dyadic reference before arbitrary independent later logarithm and exponential tables and prove uniform near two bounds by positive reference head cancellation without assuming an analytic limit

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