AP094 — exp log root half transport — irrationality research

Exact named statement

forall k d s D ab ac x p wb wc tb tc w0 f h y jb jc v z. ~D=0 ->
  NatSqrt2ExpSample(k,d,s,D,ab,ac,x,p,wb,wc,tb,tc,w0,f,h,y) ->
  ~v=0 ->
  NatScaledExpRecurrence((2*((D*p)*d)),((3*x)*s),jb,jc,k+2) ->
  BetaAt(jb,jc,0,v) ->
  Sum(jb,jc,S(k+2),z) ->
  (~d=0) /\ ((~((D*p)*s)=0) /\ ((~(2*((D*p)*d))=0) /\ ((~w0=0) /\ ((~v=0) /\ ((Le(w0*z,v*y)) /\ (Le(d*(v*y),d*(w0*z)+18*(w0*v))))))))

PD0013 — BetaAt · PD0001 — Le · PD0015 — Sum · ND0443 — NatScaledExpRecurrence · ND0448 — NatSqrt2ExpSample

Fully expanded target AST

Complete certificate and independent checks

214 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: d987799164353f66ab8981951790a46ec16203c12f377c44a23181eb042ebe7a
Bundle SHA-256: b234e8883d2975dd2cb5ab32133703fb623196946051fffc74181f9e8a7d3f6c

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.

AP004 · AP007 · AP093 · CV009 · CV086 · CV094 · CV095 · CV096 · CV097 · CV098 · SQ002 · SQ009

Scope

transport the actual original finite exponential sample to an independent positive half root recurrence at the same k plus two degree with order and eighteen over d error cancelling only proved nonzero factors

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