QF005 — bounded quadratic product — irrationality research

Exact named statement

forall ab ac bb bc cb cc db dc L H. IQuadFactorHeightBound(ab,ac,bb,bc,cb,cc,db,dc,L,H) ->
  IQuadNonzeroFactors(ab,ac,bb,bc,cb,cc,db,dc,L) ->
  exists N ub uc vb vc wb wc xb xc rp rn sp sn. Pow(H,L,N) /\ (IQuadCanonicalTrace(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) /\ (IQuadHeightBound(rp,rn,sp,sn,N) /\ ~(rp=rn /\ sp=sn))))

ND0390 — IQuadAt · ND0393 — IQuadNonzeroFactors · ND0397 — IQuadCanonicalTrace · PD0020 — Pow · ND0398 — IQuadHeightBound · ND0399 — IQuadFactorHeightBound

Fully expanded target AST

Complete certificate and independent checks

297 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: dcb0b757df5bea77acb675edba870bb7cc99be0a5f700ee1782c1f55f324ec14
Bundle SHA-256: c46933a920ba23989841a3f8e243c32c16a127b9a15cf699cd8d4b4ab448bad0

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 · QF004 · QH001 · QH002 · QN001 · SI001 · SN001 · SN003

Scope

constructed bounded 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.