Exact named statement
forall ab ac t M N. exists bb bc x y z p. NatAffineSlice(ab,ac,M,1,bb,bc,N) /\ (NatHornerValue(ab,ac,t,M,x) /\ (NatHornerValue(bb,bc,t,N,y) /\ (NatHornerValue(ab,ac,t,M+N,z) /\ (Pow(t,N,p) /\ z=p*x+y))))ND0411 — NatAffineSlice · PD0020 — Pow · ND0437 — NatHornerValue
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: 9cde54938675644bbc152c11b3e0270bf4ac303df68a8275b2e5ab6341e8f467
Bundle SHA-256: bfe45da726ddbbc6db9574b817d48471d27286387f9a56505fde8f0e6598baf9
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
constructed actual shifted tail and prefix tail whole horner values with exact power scaled splitting including zero empty cases not a tail estimate
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.