Exact named statement
forall ab ac bb bc cb cc db dc L. IQuadNonzeroFactors(ab,ac,bb,bc,cb,cc,db,dc,L) ->
exists ub uc vb vc wb wc xb xc rp rn sp sn. IQuadProductTrace(ab,ac,bb,bc,cb,cc,db,dc,ub,uc,vb,vc,wb,wc,xb,xc,L) /\ (IQuadAt(ub,uc,vb,vc,wb,wc,xb,xc,L,rp,rn,sp,sn) /\ ~(rp=rn /\ sp=sn))ND0390 — IQuadAt · ND0392 — IQuadProductTrace · ND0393 — IQuadNonzeroFactors
Complete certificate and independent checks
272 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: d8aa407a2364ad85cd2dec414b57462a4c78a2efe4b79b49e06a0b0bd78acb2d
Bundle SHA-256: ed9f56f1fe3ea3f2e7df33ca725a9163b82883b9364433190cf3001be0abe1e4
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.
IR016 · QF001 · QF002 · QN001 · SI001 · SN001 · SN003
Scope
witnessed nonzero integer quadratic finite product not real IR046
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.