HA + independent Lean evidence · Research, not Alpha admission

CV077 — supplied composition bound

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

Exact named statement

forall d ab ac k N wb wc w0. ~d=0 ->
  NatAtanhPrefix(d,ab,ac,S k) ->
  NatExpWeightTable(d,N,wb,wc) ->
  BetaAt(wb,wc,0,w0) ->
  ~w0=0 ->
  exists q pb pc qb qc ahb ahc x p v rb rc sb sc vb vc zb zc s ub uc. (NatPowerTrace(ab,ac,S k,S ((S N)*(S k)),pb,pc,qb,qc,S N)) /\ ((NatScaledHornerTrace(ab,ac,2,S k,ahb,ahc)) /\ ((BetaAt(ahb,ahc,S k,x)) /\ ((Pow(2,S k,p)) /\ ((Pow(2,((S N)*(S k)),v)) /\ ((NatWeightedSeriesTrace(S ((S N)*(S k)),wb,wc,pb,pc,qb,qc,rb,rc,sb,sc,S N)) /\ ((NatRowHornerPrefix(pb,pc,qb,qc,2,S ((S N)*(S k)),vb,vc,S N)) /\ ((NatPointwiseProductPrefix(wb,wc,vb,vc,zb,zc,S N)) /\ ((Sum(zb,zc,S N,s)) /\ ((forall ub uc. NatPowerRow(rb,rc,sb,sc,S N,ub,uc) ->
  NatHornerValue(ub,uc,2,S ((S N)*(S k)),s)) /\ ((forall k y a b c. Lt(k,S N) ->
  BetaAt(vb,vc,k,y) ->
  Pow(p,k,a) ->
  Pow(2,k,b) ->
  Pow(x,k,c) ->
  a*y=(v*b)*c) /\ ((NatHornerValue(ab,ac,2,S k,x)) /\ ((Pow(2,k,q)) /\ ((Le(x+2*d,(2*d)*q)) /\ ((p=q*2) /\ ((~p=0) /\ ((~v=0) /\ ((~(d*p)=0) /\ ((~(w0*v)=0) /\ ((BetaAt(zb,zc,0,w0*v)) /\ ((NatScaledExpRecurrence(d*p,2*x,zb,zc,N)) /\ ((Le(s,9*(w0*v))) /\ ((NatPowerRow(rb,rc,sb,sc,S N,ub,uc)) /\ ((NatHornerValue(ub,uc,2,S ((S N)*(S k)),s)) /\ (forall M. Le(M,((S N)*(S k))) ->
  exists r tb tc u p0 q0 h. (((S N)*(S k))=M+r) /\ ((NatAffineSlice(ub,uc,M,1,tb,tc,S r)) /\ ((NatHornerValue(tb,tc,3,S r,u)) /\ ((Pow(2,M,p0)) /\ ((Pow(3,M,q0)) /\ ((Pow(3,((S N)*(S k)),h)) /\ ((~p0=0) /\ ((~q0=0) /\ ((~h=0) /\ ((~(w0*h)=0) /\ ((Le(u*q0,(9*p0)*(w0*h))) /\ (IRatLe(u,0,w0*h,9*p0,0,q0))))))))))))))))))))))))))))))))))))

PD0001 — Le · PD0002 — Lt · PD0013 — BetaAt · PD0015 — Sum · ND0411 — NatAffineSlice · ND0423 — NatExpWeightTable · ND0427 — NatScaledHornerTrace · PD0020 — Pow · ND0405 — NatPowerRow · ND0407 — NatPowerTrace · ND0437 — NatHornerValue · ND0438 — NatRowHornerPrefix · ND0421 — NatWeightedSeriesTrace · ND0439 — NatPointwiseProductPrefix · ND0425 — NatAtanhPrefix · ND0443 — NatScaledExpRecurrence · ND0444 — IRatLe

Fully expanded target AST

Complete certificate and independent checks

317 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: e21e4c6b538bc01cb88d592709a53809b0e7e69f1048918f9661e0965cd5e421
Bundle SHA-256: 8b53d2ca3cedcb2b91b3752eb9b01fea4860ef11429582dc25a3b8a9efd78a41

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 · CV019 · CV032 · CV037 · CV038 · CV039 · CV043 · CV044 · CV046 · CV047 · CV048 · CV049 · CV056 · CV057 · CV058 · CV059 · CV060 · CV061 · CV062 · CV063 · CV064 · CV065 · CV072 · CV073 · CV075

Scope

supplied atanh and weight codes preserved in constructed full composition majorant and every in range actual rational tail with supplied nonzero head not table identity assumption or analytic limit

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