CV051 — power width transport — irrationality research

Exact named statement

forall ab ac L H J K. Le(H,J) ->
  exists pb pc qb qc rb rc sb sc. NatPowerTrace(ab,ac,L,H,pb,pc,qb,qc,K) /\ (NatPowerTrace(ab,ac,L,J,rb,rc,sb,sc,K) /\ (forall k ub uc vb vc i a. Le(k,K) ->
  NatPowerRow(pb,pc,qb,qc,k,ub,uc) ->
  NatPowerRow(rb,rc,sb,sc,k,vb,vc) ->
  Lt(i,H) ->
  BetaAt(ub,uc,i,a) ->
  BetaAt(vb,vc,i,a)))

PD0001 — Le · PD0002 — Lt · PD0013 — BetaAt · ND0405 — NatPowerRow · ND0407 — NatPowerTrace

Fully expanded target AST

Complete certificate and independent checks

141 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: d22452396ee9b966bdb17b27cd501a09a8cda4e1433e5d3885685cd54982e6eb
Bundle SHA-256: 82e79e5d443ffe702660ea79c2d7ee9acfe8005212bd913d69866558ff5954bb

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.

CV004

Scope

constructed two actual power traces and all row low coefficient transport under explicit width order not truncated full evaluation equality

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