CV040 — horner monomials — irrationality research

Exact named statement

forall ab ac t N. exists wb wc p qb qc hb hc r. ((NatGeometricWeightTable(t,N,wb,wc) /\ (Pow(t,N,p) /\ (BetaAt(wb,wc,0,p) /\ (forall j w q. Le(j,N) ->
  BetaAt(wb,wc,j,w) ->
  Pow(t,j,q) ->
  w*q=p)))) /\ (NatHornerWeightedPrefix(ab,ac,wb,wc,qb,qc,N) /\ (NatScaledHornerTrace(ab,ac,t,N,hb,hc) /\ (BetaAt(hb,hc,N,r) /\ Sum(qb,qc,N,r))))) /\ ((forall e j w q. j+e=N ->
  BetaAt(wb,wc,j,w) ->
  Pow(t,e,q) ->
  w=q) /\ (forall j e a q c. (S j)+e=N ->
  BetaAt(ab,ac,j,a) ->
  Pow(t,e,q) ->
  BetaAt(qb,qc,j,c) ->
  c=a*q))

PD0001 — Le · PD0013 — BetaAt · PD0015 — Sum · ND0427 — NatScaledHornerTrace · ND0428 — NatGeometricWeightTable · ND0429 — NatHornerWeightedPrefix · PD0020 — Pow

Fully expanded target AST

Complete certificate and independent checks

142 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: 76c2e7135bb0294d18ddca7f6750fc378916725dd05a107878f9dc22c55483d1
Bundle SHA-256: c01db734918315570a4e104464a29d4f6932796b37d351bae01926e53c12e496

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 · CV037 · CV038 · CV039

Scope

constructed same horner sum with exact complementary power and monomial terms 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.