CV093 — independent atanh truncation

Exact named statement

forall d e ab ac bb bc M N x z p h. ~d=0 ->
  ~e=0 ->
  NatAtanhPrefix(d,ab,ac,M) ->
  NatAtanhPrefix(e,bb,bc,M+N) ->
  NatHornerValue(ab,ac,3,M,x) ->
  NatHornerValue(bb,bc,3,M+N,z) ->
  Pow(3,M,p) ->
  Pow(3,M+N,h) ->
  IRatLe(3*x,0,d*p,3*z,0,e*h) /\ IRatLe(3*z,0,e*h,3*x+3*d,0,d*p)

PD0020 — Pow · ND0437 — NatHornerValue · ND0425 — NatAtanhPrefix · ND0444 — IRatLe

Fully expanded target AST

Complete certificate and independent checks

155 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: c8bd73e82050b43d383204e7e5e1fc00bda755d88df07a5fb9b1c8f5700f3f6b
Bundle SHA-256: d687a27e5e4e4a010c27dcdc93fe18548e682cd1bfa3c03e7d32e04aa65f1acd

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.

CV032 · CV062 · CV089 · CV090 · CV092

Scope

independently supplied atanh prefix and longer table scales values and powers give valid rational monotonicity and uniform error three over three to cutoff without code equality 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.