AP017 — paired horner — irrationality research

Exact named statement

forall ab ac bb bc t K x y. NatAffineSlice(ab,ac,1,2,bb,bc,K) ->
  (forall j a. Le(j,K) ->
  BetaAt(ab,ac,2*j,a) ->
  a=0) ->
  NatHornerValue(ab,ac,t,S(2*K),x) ->
  NatHornerValue(bb,bc,t*t,K,y) ->
  x=t*y

PD0001 — Le · PD0013 — BetaAt · ND0411 — NatAffineSlice · ND0437 — NatHornerValue

Fully expanded target AST

Complete certificate and independent checks

40 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: 5235c154de5a45ae307e0f3e33b64ea3ba043dd2efe3fdc302aa824d100fe5d9
Bundle SHA-256: 74390410057e6f52c8976706ee47906b16fb7699670d7602f3ac336bd25b2854

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

compare actual supplied horner histories by explicit pairwise induction to prove long value equals base times odd slice value at squared base with every even coefficient zero including the terminal entry

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