CV030 — weight factorials — irrationality research

Exact named statement

forall d N. exists wb wc w0 f p. NatExpWeightTable(d,N,wb,wc) /\ ((forall j a. Le(j,N) ->
  BetaAt(wb,wc,j,a) ->
  ~d=0 ->
  ~a=0) /\ (BetaAt(wb,wc,0,w0) /\ (Factorial(N,f) /\ (Pow(d,N,p) /\ (w0=f*p /\ (forall j w f p. Le(j,N) ->
  BetaAt(wb,wc,j,w) ->
  Factorial(j,f) ->
  Pow(d,j,p) ->
  (w*f)*p=w0))))))

PD0001 — Le · PD0013 — BetaAt · ND0423 — NatExpWeightTable · PD0020 — Pow · PD0023 — Factorial

Fully expanded target AST

Complete certificate and independent checks

130 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: 7416c0350bc9ea0e640eccd8e16eeb667dc7c4ae78dfb37bc2abd3442cdaa923
Bundle SHA-256: c7972044ee20c85a4f3cf7cff03b6217745c4a16071999769c4714bf6d940e10

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.

CV022

Scope

constructed actual weight factorial power normalization not rational 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.