CV021 — finite composition euler — irrationality research

Exact named statement

forall ab ac L H wb wc N. exists db dc pb pc qb qc yb yc tb tc vb vc rb rc sb sc. NatEulerPrefix(ab,ac,db,dc,L) /\ (NatPowerTrace(ab,ac,L,H,pb,pc,qb,qc,N) /\ (NatShiftedEulerPrefix(wb,wc,yb,yc,N) /\ (NatWeightedSeriesTrace(H,wb,wc,pb,pc,qb,qc,tb,tc,vb,vc,S N) /\ (NatWeightedSeriesTrace(H,yb,yc,pb,pc,qb,qc,rb,rc,sb,sc,N) /\ (forall fb fc gb gc i p t. NatPowerRow(tb,tc,vb,vc,S N,fb,fc) ->
  NatPowerRow(rb,rc,sb,sc,N,gb,gc) ->
  Lt(i,H) ->
  BetaAt(fb,fc,i,p) ->
  NatConvolutionCoefficient(db,dc,L,gb,gc,H,i,t) ->
  i*p=t)))))

PD0002 — Lt · PD0013 — BetaAt · ND0401 — NatConvolutionCoefficient · ND0405 — NatPowerRow · ND0407 — NatPowerTrace · ND0421 — NatWeightedSeriesTrace · ND0410 — NatEulerPrefix · ND0422 — NatShiftedEulerPrefix

Fully expanded target AST

Complete certificate and independent checks

208 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: b8aae36bc9df2d03bb7bd14cae145075883cbe46a5eb5d5881d71b46927b2a65
Bundle SHA-256: 7e48274c5a65c371d3cc536fd0d8fdb08596ba956b8795ea96c1b30349d08688

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.

CV004 · CV008 · CV009 · CV011 · CV012 · CV019 · CV020

Scope

constructed finite composition euler chain rule not exponential 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.