AP020 — finite odd log series — irrationality research

Exact named statement

forall d ab ac k x p. ~d=0 ->
  NatAtanhPrefix(d,ab,ac,S(2*k)) ->
  NatHornerValue(ab,ac,3,S(2*k),x) ->
  Pow(3,S(2*k),p) ->
  exists bb bc y q tb tc. (NatAffineSlice(ab,ac,1,2,bb,bc,k) /\ ((forall j a. Lt(j,k) ->
  BetaAt(bb,bc,j,a) ->
  (S(2*j))*a=2*d) /\ (NatHornerValue(bb,bc,9,k,y) /\ (Pow(9,k,q) /\ (~q=0 /\ (~p=0 /\ (x=3*y /\ (p=3*q /\ (IRatEq(3*x,0,d*p,3*y,0,d*q) /\ (Sum(tb,tc,k,y) /\ (forall j c. Lt(j,k) ->
  BetaAt(tb,tc,j,c) ->
  exists r. Pow(3,S(2*j),r) /\ IRatEq(3*c,0,d*q,2,0,(S(2*j))*r))))))))))))

PD0002 — Lt · PD0013 — BetaAt · ND0411 — NatAffineSlice · ND0437 — NatHornerValue · ND0425 — NatAtanhPrefix · PD0020 — Pow · ND0383 — IRatEq · PD0015 — Sum

Fully expanded target AST

Complete certificate and independent checks

169 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: 1d918aad2d021a46dc9e5a2a09b838014a15d6b30db745a7c4c5c0f2f8c34c20
Bundle SHA-256: b32cdcbcfc160830a6b0f97c0b6d132c5c05de4c5fef88f07c57ac3d0a7cb520

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.

AP016 · AP017 · AP018 · AP019 · CV032 · CV037 · CV038 · CV039

Scope

preserve the original finite log computations and construct an actual sum table identifying every normalized term with its odd reciprocal using constructed positive denominator powers without assuming an infinite logarithm identity

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