Exact named statement
((forall d ab ac N. (NatAtanhPrefix(d,ab,ac,N)) \/ ~(NatAtanhPrefix(d,ab,ac,N)))) /\ (((forall d N wb wc. (NatExpWeightTable(d,N,wb,wc)) \/ ~(NatExpWeightTable(d,N,wb,wc)))) /\ ((forall x wb wc tb tc N. (NatPowerWeightedPrefix(x,wb,wc,tb,tc,N)) \/ ~(NatPowerWeightedPrefix(x,wb,wc,tb,tc,N)))))ND0425 — NatAtanhPrefix · ND0423 — NatExpWeightTable · ND0442 — NatPowerWeightedPrefix
Complete certificate and independent checks
133 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: 6dbc10516866227c027792d1af728a7e88461da6be67734ad5f93540f85317ce
Bundle SHA-256: 602f3a841c85f0210c2c54d4c23d406e6539f247b720acc6a07b04b76c495bb2
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
compile and replay actual beta power row decisions and bounded induction decisions for supplied coefficient weight and term tables including incorrect tables empty prefixes and zero scales without claiming the complete CApprox record
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.