AP095 — requested half transport — irrationality research

Exact named statement

forall n d s D ab ac x p wb wc tb tc w0 f h y jb jc v z. ~D=0 ->
  NatSqrt2ExpSample(n+8,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,(n+8)+2) ->
  BetaAt(jb,jc,0,v) ->
  Sum(jb,jc,S((n+8)+2),z) ->
  exists r. (Pow(2,n,r)) /\ ((~r=0) /\ ((~d=0) /\ ((~w0=0) /\ ((~v=0) /\ ((Le(w0*z,v*y)) /\ (Le(r*(v*y),r*(w0*z)+(w0*v))))))))

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

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: 0b7a36d2e72c832a07f9a5512667ba40107b5b367d5a8715c776889e56a485e5
Bundle SHA-256: 07d48fca1276244b05d415dc9c46a505b1fd357dc8178abea55a624e7347ff7e

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 · AP010 · AP014 · AP093 · AP094 · CV009 · CV086 · CV094 · CV095 · CV096 · CV097 · CV098 · SQ002 · SQ009

Scope

derive requested dyadic half root comparison error for the unchanged n plus eight sample by constructing actual powers and replaying AP015 scale cancellation preserving independent positive heads and original degree

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