Exact named statement
forall ab ac a b N r. Le(a,b) ->
exists tb tc u v p q. NatAffineSlice(ab,ac,N,1,tb,tc,S r) /\ (NatHornerValue(tb,tc,b,S r,u) /\ (NatHornerValue(ab,ac,a,N+S r,v) /\ (Pow(a,r,p) /\ (Pow(b,r,q) /\ Le(p*u,q*v)))))PD0001 — Le · ND0411 — NatAffineSlice · PD0020 — Pow · ND0437 — NatHornerValue
Complete certificate and independent checks
132 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: adec9c34b4e9fd8be3a611ebe168b24c3cfbd3ca6d6b96568180e2849705609f
Bundle SHA-256: 19b994fd3a6014407807961c23e963367e51814be7a6231a0e0fd337f8eb7d0f
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 genuine tail and whole comparison values with exact integer scaled tail majorant for ordered bases not rational division transport or analytic limit
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.