Named statement
forall ab ac bb bc cb cc db dc ub uc vb vc wb wc xb xc L rp rn sp sn.
IQuadProductTrace(ab,ac,bb,bc,cb,cc,db,dc,ub,uc,vb,vc,wb,wc,xb,xc,L) ->
IQuadNonzeroFactors(ab,ac,bb,bc,cb,cc,db,dc,L) ->
IQuadAt(ub,uc,vb,vc,wb,wc,xb,xc,L,rp,rn,sp,sn) ->
~(rp=rn /\ sp=sn)For every finite length, a supplied β-table product trace beginning at one has a nonzero terminal value if every decoded factor is nonzero. Each executed step supplies actual factor, predecessor and successor coordinates and both multiplication equations. Induction, exact β-decoding uniqueness and QN001 prove the claim. The execution definition contains no nonvanishing conclusion. Trace existence, rational denominators and real interpretation remain separate open obligations.
Exact original expanded HA target
∀ x. ∀ y. ∀ z. ∀ n. ∀ m. ∀ k. ∀ i. ∀ j. ∀ u. ∀ v. ∀ w. ∀ x0. ∀ x1. ∀ x2. ∀ x3. ∀ x4. ∀ x5. ∀ x6. ∀ x7. ∀ x8. ∀ x9. 2 ≤ S (1 · v) ∧ (∃ x10. u = x10 · S (1 · v) + 1) ∧ (1 ≤ S (1 · x0) ∧ (∃ x10. w = x10 · S (1 · x0) + 0) ∧ (1 ≤ S (1 · x2) ∧ (∃ x10. x1 = x10 · S (1 · x2) + 0) ∧ (1 ≤ S (1 · x4) ∧ (∃ x10. x3 = x10 · S (1 · x4) + 0)))) ∧ (∀ x10. S x10 ≤ x5 → ∃ x11. ∃ x12. ∃ x13. ∃ x14. ∃ x15. ∃ x16. ∃ x17. ∃ x18. ∃ x19. ∃ x20. ∃ x21. ∃ x22. S x15 ≤ S (S x10 · y) ∧ (∃ x23. x = x23 · S (S x10 · y) + x15) ∧ (S x16 ≤ S (S x10 · n) ∧ (∃ x23. z = x23 · S (S x10 · n) + x16) ∧ (S x17 ≤ S (S x10 · k) ∧ (∃ x23. m = x23 · S (S x10 · k) + x17) ∧ (S x18 ≤ S (S x10 · j) ∧ (∃ x23. i = x23 · S (S x10 · j) + x18)))) ∧ (S x11 ≤ S (S x10 · v) ∧ (∃ x23. u = x23 · S (S x10 · v) + x11) ∧ (S x12 ≤ S (S x10 · x0) ∧ (∃ x23. w = x23 · S (S x10 · x0) + x12) ∧ (S x13 ≤ S (S x10 · x2) ∧ (∃ x23. x1 = x23 · S (S x10 · x2) + x13) ∧ (S x14 ≤ S (S x10 · x4) ∧ (∃ x23. x3 = x23 · S (S x10 · x4) + x14)))) ∧ (S x19 ≤ S (S S x10 · v) ∧ (∃ x23. u = x23 · S (S S x10 · v) + x19) ∧ (S x20 ≤ S (S S x10 · x0) ∧ (∃ x23. w = x23 · S (S S x10 · x0) + x20) ∧ (S x21 ≤ S (S S x10 · x2) ∧ (∃ x23. x1 = x23 · S (S S x10 · x2) + x21) ∧ (S x22 ≤ S (S S x10 · x4) ∧ (∃ x23. x3 = x23 · S (S S x10 · x4) + x22)))) ∧ (x19 + (x11 · x16 + x12 · x15 + 2 · (x13 · x18 + x14 · x17)) = x11 · x15 + x12 · x16 + 2 · (x13 · x17 + x14 · x18) + x20 ∧ x21 + (x11 · x18 + x12 · x17 + (x13 · x16 + x14 · x15)) = x11 · x17 + x12 · x18 + (x13 · x15 + x14 · x16) + x22)))) → (∀ x10. ∀ x11. ∀ x12. ∀ x13. ∀ x14. S x10 ≤ x5 → S x11 ≤ S (S x10 · y) ∧ (∃ x15. x = x15 · S (S x10 · y) + x11) ∧ (S x12 ≤ S (S x10 · n) ∧ (∃ x15. z = x15 · S (S x10 · n) + x12) ∧ (S x13 ≤ S (S x10 · k) ∧ (∃ x15. m = x15 · S (S x10 · k) + x13) ∧ (S x14 ≤ S (S x10 · j) ∧ (∃ x15. i = x15 · S (S x10 · j) + x14)))) → ¬(x11 = x12 ∧ x13 = x14)) → S x6 ≤ S (S x5 · v) ∧ (∃ x10. u = x10 · S (S x5 · v) + x6) ∧ (S x7 ≤ S (S x5 · x0) ∧ (∃ x10. w = x10 · S (S x5 · x0) + x7) ∧ (S x8 ≤ S (S x5 · x2) ∧ (∃ x10. x1 = x10 · S (S x5 · x2) + x8) ∧ (S x9 ≤ S (S x5 · x4) ∧ (∃ x10. x3 = x10 · S (S x5 · x4) + x9)))) → ¬(x6 = x7 ∧ x8 = x9)Fresh HA and independently compiled Lean checks
Download the exact canonical proof bundle (gzip) · Original run record.
224 local nodes; 81,603 ordinary proof-body nodes. No receipt is substituted for a proof body.
Target AST SHA-256: d27f07d45ef919c5b7597e15e774478ab7ae46fc82e18fd16fa82e860df90768
Certificate SHA-256: 4933e2fe5136b4c700fbe804b81d20ba2331ec53c1f0a18501bab03becf2675f
Checked arithmetic DAG · Definition network · Larger IR046 planning cone · All current evidence.
IR072 remains open. This local exact certificate is not an Alpha/Stable admission or a completed irrationality proof.