CV073 — weighted monomial recurrence

Exact named statement

forall d p t x v N wb wc vb vc zb zc w0. ~p=0 ->
  (forall k y a b c. Lt(k,S N) ->
  BetaAt(vb,vc,k,y) ->
  Pow(p,k,a) ->
  Pow(t,k,b) ->
  Pow(x,k,c) ->
  a*y=(v*b)*c) ->
  NatExpWeightTable(d,N,wb,wc) ->
  NatPointwiseProductPrefix(wb,wc,vb,vc,zb,zc,S N) ->
  BetaAt(wb,wc,0,w0) ->
  BetaAt(zb,zc,0,w0*v) /\ NatScaledExpRecurrence(d*p,t*x,zb,zc,N)

PD0002 — Lt · PD0013 — BetaAt · ND0423 — NatExpWeightTable · PD0020 — Pow · ND0439 — NatPointwiseProductPrefix · ND0443 — NatScaledExpRecurrence

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: e23d9c7bce72b64cec08978482e066d449fff7b4e18c3a1cfc5bc8dc55f9d6e5
Bundle SHA-256: 3365ad973b40bee6ffab11db7b582e17939db61a4768fd46c46adb6836b31d10

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.

CV072

Scope

same supplied factorial weights monomial values and pointwise products obey scaled exponential recurrence at denominator d times p and numerator t times x with head w0 times v not yet constructed composition bound

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