CV023 — weighted series scaling — irrationality research

Exact named statement

forall H pb pc qb qc wb wc yb yc d K. NatLinearTriple(d,0,1,yb,yc,yb,yc,wb,wc,K) ->
  exists tb tc vb vc rb rc sb sc. NatWeightedSeriesTrace(H,wb,wc,pb,pc,qb,qc,tb,tc,vb,vc,K) /\ (NatWeightedSeriesTrace(H,yb,yc,pb,pc,qb,qc,rb,rc,sb,sc,K) /\ (forall k ub uc eb ec. Le(k,K) ->
  NatPowerRow(tb,tc,vb,vc,k,ub,uc) ->
  NatPowerRow(rb,rc,sb,sc,k,eb,ec) ->
  NatLinearTriple(d,0,1,eb,ec,eb,ec,ub,uc,H)))

PD0001 — Le · ND0405 — NatPowerRow · ND0409 — NatLinearTriple · ND0421 — NatWeightedSeriesTrace

Fully expanded target AST

Complete certificate and independent checks

116 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: 942e7e78560841ddb311dc397deeb9086050bd51b7d759f6926caddefd3d230d
Bundle SHA-256: 3bebdb7ac4f793a5bf43e6e100c0a1286483ea73b7fb8a87d482df3f8422e108

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.

CV019

Scope

constructed weighted traces with all rows scalar transport not exp 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.