CV037 — horner weighted sum — irrationality research

Exact named statement

forall ab ac t N wb wc qb qc. NatGeometricWeightTable(t,N,wb,wc) ->
  NatHornerWeightedPrefix(ab,ac,wb,wc,qb,qc,N) ->
  exists hb hc r. NatScaledHornerTrace(ab,ac,t,N,hb,hc) /\ (BetaAt(hb,hc,N,r) /\ Sum(qb,qc,N,r))

PD0013 — BetaAt · PD0015 — Sum · ND0427 — NatScaledHornerTrace · ND0428 — NatGeometricWeightTable · ND0429 — NatHornerWeightedPrefix

Fully expanded target AST

Complete certificate and independent checks

115 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: 6f5222fbdb659a953b151731a5f8b309685813f395efda3e55af160b5757bfd8
Bundle SHA-256: 1f1e394ceee77030f4f8b71ae091f587e9815c47546e2ee674f699de2c8189c6

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.

CV032

Scope

constructed horner endpoint equals actual sum given geometric weights and pointwise products not their existence 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.