CV036 — horner zero tail — irrationality research

Exact named statement

forall ab ac t M N. (forall j a. Lt(j,N) ->
  BetaAt(ab,ac,M+j,a) ->
  a=0) ->
  exists hb hc u v p. NatScaledHornerTrace(ab,ac,t,M+N,hb,hc) /\ (BetaAt(hb,hc,M,u) /\ (BetaAt(hb,hc,M+N,v) /\ (Pow(t,N,p) /\ v=p*u)))

PD0002 — Lt · PD0013 — BetaAt · ND0427 — NatScaledHornerTrace · PD0020 — Pow

Fully expanded target AST

Complete certificate and independent checks

122 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: ba1d797f495177c7c2b6f504d04e3cb81acb6460d86b60a22e46f3369a8a78d9
Bundle SHA-256: 106c098a8896d97701ffa0444b2cadc8aafab9d4bbdab9c5603b903fb8963881

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

Scope

constructed horner endpoints and actual power with exact zero tail scaling not multiplication or analytic identity

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