HA + independent Lean evidence · Research, not Alpha admission

ND0394 — IQuadCanonicalProduct

Full irrationality (IR072/G121) remains open. Stable: 432. Alpha v35: 4,318. This checkpoint changes neither catalogue.

Conservative definition

Parameters: ap, an, bp, bn, cp, cn, dp, dn, rp, rn, sp, sn

rp = ap · cp + an · cn + 2 · (bp · dp + bn · dn) ∧ (rn = ap · cn + an · cp + 2 · (bp · dn + bn · dp) ∧ (sp = ap · dp + an · dn + (bp · cp + bn · cn) ∧ sn = ap · dn + an · dp + (bp · cn + bn · cp)))

Definition prerequisites

Theorem uses (notation, not proof premises)

QH001