Exact named statement
forall ab ac L t J K wb wc pb pc qb qc rb rc sb sc. Le(S(K*L),S J) ->
NatPowerTrace(ab,ac,L,S J,pb,pc,qb,qc,K) ->
NatWeightedSeriesTrace(S J,wb,wc,pb,pc,qb,qc,rb,rc,sb,sc,K) ->
exists ahb ahc x p v vb vc zb zc s. (NatScaledHornerTrace(ab,ac,t,L,ahb,ahc)) /\ ((BetaAt(ahb,ahc,L,x)) /\ ((Pow(t,L,p)) /\ ((Pow(t,J,v)) /\ ((NatRowHornerPrefix(pb,pc,qb,qc,t,S J,vb,vc,K)) /\ ((NatPointwiseProductPrefix(wb,wc,vb,vc,zb,zc,K)) /\ ((Sum(zb,zc,K,s)) /\ ((forall ub uc. NatPowerRow(rb,rc,sb,sc,K,ub,uc) ->
NatHornerValue(ub,uc,t,S J,s)) /\ (forall k y a b c. Lt(k,K) ->
BetaAt(vb,vc,k,y) ->
Pow(p,k,a) ->
Pow(t,k,b) ->
Pow(x,k,c) ->
a*y=(v*b)*c))))))))PD0001 — Le · PD0002 — Lt · PD0013 — BetaAt · PD0015 — Sum · ND0427 — NatScaledHornerTrace · PD0020 — Pow · ND0405 — NatPowerRow · ND0407 — NatPowerTrace · ND0437 — NatHornerValue · ND0438 — NatRowHornerPrefix · ND0421 — NatWeightedSeriesTrace · ND0439 — NatPointwiseProductPrefix
Complete certificate and independent checks
263 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: afd8a2cb3249c998e8a875e5136ae8ea7ce51566569fff1a737c3bb58e6fb097
Bundle SHA-256: fb723fc358c8247fa1a3bef7a64b5c8c4292429c439b19843823037a8c8e4873
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.
CV008 · CV009 · CV011 · CV032 · CV037 · CV038 · CV039 · CV043 · CV044 · CV046 · CV047 · CV048 · CV049 · CV056 · CV057
Scope
arbitrary base evaluation of supplied whole support power and weighted accumulation traces constructs actual row values products sum and monomial law without replacing any supplied trace not analytic limit
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.