AP023 — factorial 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. (Factorial(S(2*k),D)) /\ ((~D=0) /\ ((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

190 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: a49dec85075c8e059c999c262ce992200a03c7c1611ff0d9003643f5237b1fcf
Bundle SHA-256: c16e77ecbdceec882bf43df4a345bd3a875fc7d0f4225e50983785e982294a61

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.

AP022 · CV022 · CV030 · CV032 · CV069 · CV070 · CV086 · SQ001 · SQ002 · SQ003 · SQ004

Scope

construct the complete finite log root exponential sample with prescribed coefficient scale factorial two k plus one preserving positive scale all actual computations recurrence and normalization without claiming the whole PR trace or analytic identification

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