Exact named statement
forall alpha beta gamma ab ac bb bc cb cc t N. NatLinearTriple(alpha,beta,gamma,ab,ac,bb,bc,cb,cc,N) ->
exists ub uc vb vc wb wc u v w. NatScaledHornerTrace(ab,ac,t,N,ub,uc) /\ (NatScaledHornerTrace(bb,bc,t,N,vb,vc) /\ (NatScaledHornerTrace(cb,cc,t,N,wb,wc) /\ (BetaAt(ub,uc,N,u) /\ (BetaAt(vb,vc,N,v) /\ (BetaAt(wb,wc,N,w) /\ gamma*w=alpha*u+beta*v)))))PD0013 — BetaAt · ND0409 — NatLinearTriple · ND0427 — NatScaledHornerTrace
Complete certificate and independent checks
111 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: ad3d9e7f204d9e713be5a888404827c60c7a6e4a2ceca04adb2deb516e9682df
Bundle SHA-256: 77477ae2e7d646455c9401f03bef0c0e798ef50fd7286954b938c74074793b65
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 three horner evaluations with weighted linearity from pointwise relation not multiplication 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.