AP002 — exp sample — irrationality research

Exact named statement

forall k. exists d s D ab ac x p wb wc tb tc w0 f h y. (NatSqrt2ExpSample(k,d,s,D,ab,ac,x,p,wb,wc,tb,tc,w0,f,h,y)) /\ ((~w0=0) /\ ((~((D*p)*s)=0) /\ ((Le(((3*x)*d),((D*p)*s))) /\ ((NatScaledExpRecurrence(((D*p)*s),((3*x)*d),tb,tc,(k+2))) /\ (forall j t f0 p0 q. Le(j,(k+2)) ->
  BetaAt(tb,tc,j,t) ->
  Factorial(j,f0) ->
  Pow(((D*p)*s),j,p0) ->
  Pow(((3*x)*d),j,q) ->
  (t*f0)*p0=w0*q)))))

PD0013 — BetaAt · PD0020 — Pow · PD0001 — Le · PD0023 — Factorial · ND0443 — NatScaledExpRecurrence · ND0448 — NatSqrt2ExpSample

Fully expanded target AST

Complete certificate and independent checks

186 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: 934fbe9c81ad757420933f697a47c0e82aa1b3e12a326f07d6080b94c7c3e24f
Bundle SHA-256: 254ee848b9237c568db4089d6f5460ffcf482cbd5b4d6aa34ec8937eaaa075e9

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.

AP001 · CV022 · CV025 · CV030 · CV032 · CV069 · CV070 · CV086 · SQ001 · SQ002 · SQ003 · SQ004

Scope

construct actual finite exponential sample of log root quotient with nonzero normalization factorial power weight term tables sum recurrence and all index normalization no analytic identity or accuracy claim

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