HA + independent Lean evidence · Research, not Alpha admission

CV074 — composition majorant

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

Exact named statement

forall k N. exists d ab ac q wb wc w0 f dn pb pc qb qc ahb ahc x p v rb rc sb sc vb vc zb zc s. (~d=0) /\ ((NatAtanhPrefix(d,ab,ac,S k)) /\ ((NatZeroBefore(ab,ac,S k,1)) /\ ((BetaAt(ab,ac,0,0)) /\ ((NatBoundedPrefix(ab,ac,2*d,S k)) /\ ((NatHornerValue(ab,ac,2,S k,x)) /\ ((Pow(2,k,q)) /\ ((Le(x+2*d,(2*d)*q)) /\ ((NatExpWeightTable(d,N,wb,wc)) /\ ((forall j a. Le(j,N) ->
  BetaAt(wb,wc,j,a) ->
  ~d=0 ->
  ~a=0) /\ ((BetaAt(wb,wc,0,w0)) /\ ((Factorial(N,f)) /\ ((Pow(d,N,dn)) /\ ((w0=f*dn) /\ ((forall j w f p. Le(j,N) ->
  BetaAt(wb,wc,j,w) ->
  Factorial(j,f) ->
  Pow(d,j,p) ->
  (w*f)*p=w0) /\ ((~w0=0) /\ ((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) /\ ((~p=0) /\ ((~v=0) /\ ((~(d*p)=0) /\ ((~(w0*v)=0) /\ ((p=q*2) /\ ((Le(x,d*p)) /\ ((Le(2*x,2*(d*p))) /\ ((BetaAt(zb,zc,0,w0*v)) /\ ((NatScaledExpRecurrence(d*p,2*x,zb,zc,N)) /\ (Le(s,9*(w0*v))))))))))))))))))))))))))))))))))))))

PD0001 — Le · PD0002 — Lt · PD0013 — BetaAt · PD0015 — Sum · ND0423 — NatExpWeightTable · ND0427 — NatScaledHornerTrace · PD0020 — Pow · PD0023 — Factorial · ND0405 — NatPowerRow · ND0407 — NatPowerTrace · ND0437 — NatHornerValue · ND0438 — NatRowHornerPrefix · ND0421 — NatWeightedSeriesTrace · ND0439 — NatPointwiseProductPrefix · ND0440 — NatBoundedPrefix · ND0408 — NatZeroBefore · ND0425 — NatAtanhPrefix · ND0443 — NatScaledExpRecurrence

Fully expanded target AST

Complete certificate and independent checks

325 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: 0a0ef5814cf4d9655010b47abf33ab8cbcb9f86f7d6f336cafcc1a6d7556273b
Bundle SHA-256: 1ec6611c5e094c392f09d2203b46e4ce9380c95ad0ab421a8c9f3d7c600aa221

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 · CV022 · CV025 · CV030 · CV032 · CV037 · CV038 · CV039 · CV043 · CV044 · CV046 · CV047 · CV048 · CV049 · CV056 · CV057 · CV058 · CV059 · CV060 · CV061 · CV065 · CV066 · CV072 · CV073

Scope

constructed same atanh table factorial weights whole support composition rows products and sum at base two with nonzero normalization and sum at most nine times w0 times two to J not rational division 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.