Exact named statement
forall H wb wc pb pc qb qc K. exists tb tc vb vc. NatWeightedSeriesTrace(H,wb,wc,pb,pc,qb,qc,tb,tc,vb,vc,K)Complete certificate and independent checks
110 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: 911c376cb25c2cb18aefd0e0b77325ea871669c2faefda9024ec48e53e0a0bbf
Bundle SHA-256: b0631c667d51a9b670287b6589503801ca8d8c2fb482b4473a3ba866ca0cd9d8
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 all lengths weighted series accumulation trace not chain rule
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.