CV026 — atanh euler — irrationality research

Exact named statement

forall d ab ac N. NatAtanhPrefix(d,ab,ac,N) ->
  exists db dc. NatEulerPrefix(ab,ac,db,dc,N) /\ ((Lt(0,N) ->
  BetaAt(db,dc,0,0)) /\ ((Lt(1,N) ->
  BetaAt(db,dc,1,2*d)) /\ (forall i a b. Lt(S(S i),N) ->
  BetaAt(db,dc,i,a) ->
  BetaAt(db,dc,S(S i),b) ->
  a=b)))

PD0002 — Lt · PD0013 — BetaAt · ND0425 — NatAtanhPrefix · ND0410 — NatEulerPrefix

Fully expanded target AST

Complete certificate and independent checks

111 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: 5a9b991ec4dccaeb1d26ec04fa722f7dd24100442b583d871f9cb4b5887431b2
Bundle SHA-256: 9395c1f7fc2f6eb5e13d52f715f983964060b080a6743960bf1787349b809ca9

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.

Scope

constructed atanh euler table with initial values and period two not analytic derivative

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