CV033 — geometric horner — irrationality research

Exact named statement

forall ab ac z k. (forall i a. Lt(i,S k) ->
  BetaAt(ab,ac,i,a) ->
  ((i=0 /\ a=z) \/ (exists j. i=S j /\ a=2*z))) ->
  exists hb hc r p. NatScaledHornerTrace(ab,ac,3,S k,hb,hc) /\ (BetaAt(hb,hc,S k,r) /\ (Pow(3,k,p) /\ (~p=0 /\ r+z=(2*z)*p)))

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

Fully expanded target AST

Complete certificate and independent checks

126 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: fbb3d37960c61bdda6f6242ac8a1ea3bd5ea98c9d28b11ee26556b39dce16fd6
Bundle SHA-256: d21aa29f793a9af547b2a92db2057ac2e272fb688da7b44c6bf1226b24b72ca9

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 value and nonzero power with exact geometric remainder given all coefficients not analytic identity

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