CV028 — composition recurrence — irrationality research

Exact named statement

forall N. exists d ab ac wb wc db dc pb pc qb qc tb tc vb vc cb cc. ~d=0 /\ (NatAtanhPrefix(d,ab,ac,N) /\ (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,N) /\ (NatPowerTrace(ab,ac,N,N,pb,pc,qb,qc,N) /\ (NatWeightedSeriesTrace(N,wb,wc,pb,pc,qb,qc,tb,tc,vb,vc,S N) /\ (NatPowerRow(tb,tc,vb,vc,S N,cb,cc) /\ ((forall j x y. Lt(j,N) ->
  BetaAt(cb,cc,j,x) ->
  NatConvolutionCoefficient(db,dc,N,cb,cc,N,j,y) ->
  d*(j*x)=y) /\ ((forall i a b c. Lt(S(S i),N) ->
  BetaAt(cb,cc,i,a) ->
  BetaAt(cb,cc,S i,b) ->
  BetaAt(cb,cc,S(S i),c) ->
  (S(S i))*c=i*a+2*b))))))))))

PD0001 — Le · PD0002 — Lt · PD0013 — BetaAt · ND0401 — NatConvolutionCoefficient · ND0405 — NatPowerRow · ND0407 — NatPowerTrace · ND0421 — NatWeightedSeriesTrace · ND0410 — NatEulerPrefix · ND0423 — NatExpWeightTable · ND0425 — NatAtanhPrefix

Fully expanded target AST

Complete certificate and independent checks

245 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: 52788665088b222b10bd5663fc56a1708052b6dff8d6bda63f6719cae2553927
Bundle SHA-256: c29b4cd038b31a9cec9ead465584d49e015dc18993c8d71ddb849b591b070a89

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 · CV024 · CV025 · CV027

Scope

constructed actual finite composition three term recurrence not initial values 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.