Exact named statement
forall ab ac L H J wb wc K. Le(H,J) ->
exists pb pc qb qc rb rc sb sc tb tc vb vc db dc eb ec. NatPowerTrace(ab,ac,L,H,pb,pc,qb,qc,K) /\ (NatPowerTrace(ab,ac,L,J,rb,rc,sb,sc,K) /\ (NatWeightedSeriesTrace(H,wb,wc,pb,pc,qb,qc,tb,tc,vb,vc,K) /\ (NatWeightedSeriesTrace(J,wb,wc,rb,rc,sb,sc,db,dc,eb,ec,K) /\ ((forall k ub uc fb fc i a. Le(k,K) ->
NatPowerRow(pb,pc,qb,qc,k,ub,uc) ->
NatPowerRow(rb,rc,sb,sc,k,fb,fc) ->
Lt(i,H) ->
BetaAt(ub,uc,i,a) ->
BetaAt(fb,fc,i,a)) /\ (forall k ub uc fb fc i a. Le(k,K) ->
NatPowerRow(tb,tc,vb,vc,k,ub,uc) ->
NatPowerRow(db,dc,eb,ec,k,fb,fc) ->
Lt(i,H) ->
BetaAt(ub,uc,i,a) ->
BetaAt(fb,fc,i,a))))))PD0001 — Le · PD0002 — Lt · PD0013 — BetaAt · ND0405 — NatPowerRow · ND0407 — NatPowerTrace · ND0421 — NatWeightedSeriesTrace
Complete certificate and independent checks
151 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: 47daedfb22c29d1e812581a080205cad3a0b0a394afbe6937e03886dcfd6c17e
Bundle SHA-256: 6e941807907f0cf199d63cefee4e47b7d1726ad90e6c2dd9f20a55897bdad89f
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 cross width powers and weighted compositions preserving all low coefficients with same input and weights not full evaluation or tail identity
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.