CV047 — cauchy grid sums — irrationality research

Exact named statement

forall ab ac L bb bc M. exists N gb gc x. N=L+M /\ (NatCauchyGrid(ab,ac,L,bb,bc,M,N,gb,gc) /\ (Sum(bb,bc,M,x) /\ ((forall k. Lt(k,N) ->
  exists u. NatConvolutionCoefficient(ab,ac,L,bb,bc,M,k,u) /\ NatAffineSum(gb,gc,(S N)*k,1,N,u)) /\ (forall j a. Lt(j,N) ->
  BetaZeroExtend(ab,ac,L,j,a) ->
  exists y. NatAffineSum(gb,gc,j,S N,N,y) /\ y=a*x))))

PD0002 — Lt · PD0015 — Sum · ND0291 — BetaZeroExtend · ND0401 — NatConvolutionCoefficient · ND0433 — NatCauchyGrid · ND0412 — NatAffineSum

Fully expanded target AST

Complete certificate and independent checks

149 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: f9641b30ca39287a97a195a21f4f444b93c513dc143c2f42166caff02b8f76a0
Bundle SHA-256: 3f86c41ea1d9b3740f12a7e74c131e5baf272e7b037b4bd54b45967ab9324f95

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.

CV009 · CV011 · CV043 · CV044 · CV046

Scope

constructed single cauchy grid and all full length row column sums with shared right sum and zero columns not yet fubini sum product or evaluation

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