Exact named statement
forall N. exists d ab ac. Factorial(N,d) /\ (~d=0 /\ (NatAtanhPrefix(d,ab,ac,N) /\ NatZeroBefore(ab,ac,N,1)))ND0425 — NatAtanhPrefix · ND0408 — NatZeroBefore · PD0023 — Factorial
Complete certificate and independent checks
124 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: 717987b66df365b93849f2f28931c0d8b1ef892d210f4590b9c62997aee7989a
Bundle SHA-256: e60cea590e8fc2dcd2f130c163423b166de275b0d0af5036748f9e0bd034d9f5
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.
Scope
construct the actual positive factorial N as the prescribed logarithm coefficient scale and the actual coefficient prefix using a proved positive divisor induction and existing prefix construction without claiming the whole canonical PR approximation trace
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.