CV032 — horner trace — irrationality research

Exact named statement

forall ab ac t N. exists hb hc. NatScaledHornerTrace(ab,ac,t,N,hb,hc) /\ (forall tb tc. NatScaledHornerTrace(ab,ac,t,N,tb,tc) ->
  forall k h u. Le(k,N) ->
  BetaAt(hb,hc,k,h) ->
  BetaAt(tb,tc,k,u) ->
  h=u)

PD0001 — Le · PD0013 — BetaAt · ND0427 — NatScaledHornerTrace

Fully expanded target AST

Complete certificate and independent checks

107 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: ef5c41487529723c8676ac25e7e7972e81abf1f34730285cf1abfaae5b63ce80
Bundle SHA-256: 97f4656c45ac339b593d9cfb83632028e297d6ba9cfc7ef4bd2c7bfe7f066787

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 integer horner trace with all in range value uniqueness not rational or analytic identity

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