HA + independent Lean evidence · Research, not Alpha admission

CV034 — composition evaluation

Full irrationality (IR072/G121) remains open. Stable: 432. Alpha v35: 4,318. This checkpoint changes neither catalogue.

Exact named statement

forall K. exists N d ab ac wb wc db dc pb pc qb qc tb tc vb vc cb cc z fn pn hb hc r p. N=S(S K) /\ ((((~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))))))))))) /\ (BetaAt(wb,wc,0,z) /\ (~z=0 /\ (NatExpAtanhRecurrence(cb,cc,N,z) /\ (forall i a. Lt(i,N) ->
  BetaAt(cb,cc,i,a) ->
  ((i=0 /\ a=z) \/ (exists k. i=S k /\ a=2*z))))))) /\ (Factorial(N,fn) /\ (Pow(d,N,pn) /\ (z=fn*pn /\ (forall j w f p. Le(j,N) ->
  BetaAt(wb,wc,j,w) ->
  Factorial(j,f) ->
  Pow(d,j,p) ->
  (w*f)*p=z))))) /\ (NatScaledHornerTrace(cb,cc,3,N,hb,hc) /\ (BetaAt(hb,hc,N,r) /\ (Pow(3,S K,p) /\ (~p=0 /\ (r+z=(2*z)*p /\ (~(z*p=0))))))))

PD0001 — Le · PD0002 — Lt · PD0013 — BetaAt · ND0401 — NatConvolutionCoefficient · ND0405 — NatPowerRow · ND0407 — NatPowerTrace · ND0421 — NatWeightedSeriesTrace · ND0410 — NatEulerPrefix · ND0423 — NatExpWeightTable · ND0425 — NatAtanhPrefix · ND0400 — NatExpAtanhRecurrence · PD0020 — Pow · PD0023 — Factorial · ND0427 — NatScaledHornerTrace

Fully expanded target AST

Complete certificate and independent checks

284 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: 11b40acf4f70651db35615b86f321bc4dc95ea05a8e711c8a3f41d9c2fd3ed34
Bundle SHA-256: 258242852ea96fe63fafe958f98ae1478c0c38348948623ad9b83231e0fe1f23

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 · CV002 · CV004 · CV008 · CV009 · CV011 · CV012 · CV019 · CV020 · CV021 · CV022 · CV024 · CV025 · CV027 · CV028 · CV029 · CV031 · CV032 · CV033

Scope

constructed normalized composition and same coefficients horner value with exact geometric remainder not analytic identity

None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.