CV024 — denominator euler — irrationality research

Exact named statement

forall ab ac L d N. NatZeroBefore(ab,ac,L,1) ->
  exists wb wc db dc pb pc qb qc yb yc tb tc vb vc rb rc sb sc. NatExpWeightTable(d,N,wb,wc) /\ ((forall j a. Le(j,N) ->
  BetaAt(wb,wc,j,a) ->
  ~d=0 ->
  ~a=0) /\ (NatEulerPrefix(ab,ac,db,dc,L) /\ (NatPowerTrace(ab,ac,L,N,pb,pc,qb,qc,N) /\ (NatShiftedEulerPrefix(wb,wc,yb,yc,N) /\ (NatWeightedSeriesTrace(N,wb,wc,pb,pc,qb,qc,tb,tc,vb,vc,S N) /\ (NatWeightedSeriesTrace(N,yb,yc,pb,pc,qb,qc,rb,rc,sb,sc,N) /\ ((forall fb fc i p v. NatPowerRow(tb,tc,vb,vc,S N,fb,fc) ->
  Lt(i,N) ->
  BetaAt(fb,fc,i,p) ->
  NatConvolutionCoefficient(db,dc,L,fb,fc,N,i,v) ->
  d*(i*p)=v))))))))

PD0001 — Le · PD0002 — Lt · PD0013 — BetaAt · ND0401 — NatConvolutionCoefficient · ND0405 — NatPowerRow · ND0407 — NatPowerTrace · ND0421 — NatWeightedSeriesTrace · ND0410 — NatEulerPrefix · ND0422 — NatShiftedEulerPrefix · ND0423 — NatExpWeightTable · ND0408 — NatZeroBefore

Fully expanded target AST

Complete certificate and independent checks

224 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: b3b638e846a53d3cee1e16e8f927226ab00da021924e9c98b2978fc3a534989f
Bundle SHA-256: e727513a9752a1f0ca45550447de9ad92c582a4d221c1c8380146aa1aae068c4

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.

CV001 · CV004 · CV008 · CV009 · CV011 · CV012 · CV019 · CV020 · CV021 · CV022

Scope

constructed denominator cleared finite euler equation not factorial 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.