CV038 — geometric weights — irrationality research

Exact named statement

forall t N. exists wb wc p. NatGeometricWeightTable(t,N,wb,wc) /\ (Pow(t,N,p) /\ (BetaAt(wb,wc,0,p) /\ (forall j w q. Le(j,N) ->
  BetaAt(wb,wc,j,w) ->
  Pow(t,j,q) ->
  w*q=p)))

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

Fully expanded target AST

Complete certificate and independent checks

123 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: 917e753656a45bbae99c1856843859780ffcc5d52d3d25e45991093293a278be
Bundle SHA-256: 18b213e913d77b5362b7f2b8bfe27f7969d2379affd7519141080407eb31caa8

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.

Scope

constructed terminal one geometric weights and actual power with all weight power identities not weighted term existence 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.