AP087 — half log exp refinement — irrationality research

Exact named statement

forall d e ab ac bb bc k l x z p q m N cb cc eb ec a0 b0 u v P. ~d=0 ->
  ~e=0 ->
  NatAtanhPrefix(d,ab,ac,S k) ->
  NatAtanhPrefix(e,bb,bc,(S k)+l) ->
  NatHornerValue(ab,ac,3,S k,x) ->
  NatHornerValue(bb,bc,3,(S k)+l,z) ->
  Pow(3,S k,p) ->
  Pow(3,(S k)+l,q) ->
  NatScaledExpRecurrence(2*(d*p),3*x,cb,cc,m) ->
  NatScaledExpRecurrence(2*(e*q),3*z,eb,ec,(S m)+N) ->
  BetaAt(cb,cc,0,a0) ->
  BetaAt(eb,ec,0,b0) ->
  Sum(cb,cc,S m,u) ->
  Sum(eb,ec,S((S m)+N),v) ->
  Pow(2,m,P) ->
  ~p=0 /\ (~q=0 /\ (~P=0 /\ (~(2*(d*p))=0 /\ (~(2*(e*q))=0 /\ (Le(b0*u,a0*v) /\ Le((p*P)*(a0*v),(p*P)*(b0*u)+((9*3)*P+2*p)*(a0*b0)))))))

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

Fully expanded target AST

Complete certificate and independent checks

231 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: 74d9571876bc3c082af4e6ab56b2f18a0e49718f24ef4ea8fe3ddf85f58dcf49
Bundle SHA-256: df2878ab2be432ad492885406eec7d5bdff383560a2e4934e947062bdc7b9160

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.

CV009 · CV032 · CV062 · CV068 · CV086 · CV087 · CV088 · CV089 · CV090 · CV092 · CV093 · CV094 · CV095 · CV096 · CV097 · CV098 · CV100 · CV101

Scope

prove independent half logarithm exponential refinement by explicit doubled argument denominators and scaled gap transport while retaining the unchanged original logarithm prefixes values and powers

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