CV058 — finite power evaluation — irrationality research

Exact named statement

forall ab ac L t J K. Le(S(K*L),S J) ->
  exists pb pc qb qc ahb ahc x p v. NatPowerTrace(ab,ac,L,S J,pb,pc,qb,qc,K) /\ (NatScaledHornerTrace(ab,ac,t,L,ahb,ahc) /\ (BetaAt(ahb,ahc,L,x) /\ (Pow(t,L,p) /\ (Pow(t,J,v) /\ (forall k ub uc uhb uhc y a b c. Le(k,K) ->
  NatPowerRow(pb,pc,qb,qc,k,ub,uc) ->
  NatScaledHornerTrace(ub,uc,t,S J,uhb,uhc) ->
  BetaAt(uhb,uhc,S J,y) ->
  Pow(p,k,a) ->
  Pow(t,k,b) ->
  Pow(x,k,c) ->
  a*y=(v*b)*c)))))

PD0001 — Le · PD0013 — BetaAt · ND0427 — NatScaledHornerTrace · PD0020 — Pow · ND0405 — NatPowerRow · ND0407 — NatPowerTrace

Fully expanded target AST

Complete certificate and independent checks

253 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: 5106a1fb454a028ea96ed82dcd34c652807316d25e5009ec9a5c5f7191df4689
Bundle SHA-256: fd1e3c3606821577e5c30e547c3fd17f3f7408f9fdb3083854024f19f3b756a1

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.

CV004 · CV008 · CV009 · CV011 · CV032 · CV037 · CV038 · CV039 · CV043 · CV044 · CV046 · CV047 · CV048 · CV049 · CV056 · CV057

Scope

constructed finite power trace with all exponent horner evaluation under explicit whole support width bound retaining unit and all scaling factors not analytic composition

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