CV041 — convolution weights — irrationality research

Exact named statement

forall t L M. exists lb lc pl mb mc pm nb nc pn. (NatGeometricWeightTable(t,L,lb,lc) /\ (Pow(t,L,pl) /\ (BetaAt(lb,lc,0,pl) /\ (forall j w q. Le(j,L) ->
  BetaAt(lb,lc,j,w) ->
  Pow(t,j,q) ->
  w*q=pl)))) /\ ((NatGeometricWeightTable(t,M,mb,mc) /\ (Pow(t,M,pm) /\ (BetaAt(mb,mc,0,pm) /\ (forall j w q. Le(j,M) ->
  BetaAt(mb,mc,j,w) ->
  Pow(t,j,q) ->
  w*q=pm)))) /\ ((NatGeometricWeightTable(t,L+M,nb,nc) /\ (Pow(t,L+M,pn) /\ (BetaAt(nb,nc,0,pn) /\ (forall j w q. Le(j,L+M) ->
  BetaAt(nb,nc,j,w) ->
  Pow(t,j,q) ->
  w*q=pn)))) /\ (forall i j k a b c. Lt(i,L) ->
  Lt(j,M) ->
  i+j=k ->
  BetaAt(lb,lc,S i,a) ->
  BetaAt(mb,mc,S j,b) ->
  BetaAt(nb,nc,S k,c) ->
  c=t*(a*b))))

PD0001 — Le · PD0002 — Lt · PD0013 — BetaAt · ND0428 — NatGeometricWeightTable · PD0020 — Pow

Fully expanded target AST

Complete certificate and independent checks

135 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: 2673216a113a76804e456d1ac260a39e3d0707fa44828c7d4e784d90e55e6f87
Bundle SHA-256: 9d6be9a12cba3dd86cda9629336da3aa6a5c55902974c818f3fddb9f2a5d4e23

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.

CV038

Scope

constructed three geometric tables with convolution weight product law via actual archived power add not full evaluation 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.