Exact named statement
0 = 0 · 0 ∧ (0 = 0 · 0 + 2 · S (2 · (2 · (2 · S (2 · (2 · S (2 · 1)))))) · 0 ∧ 0 = 0 · (2 · (2 · S (2 · (2 · (2 · (2 · S (2 · (2 · (2 · (2 · S (2 · S (2 · (2 · S (2 · (2 · 1))))))))))))))) + (2 · S (2 · (2 · (2 · S (2 · (2 · S (2 · 1)))))) · 0 + 0 · 0)) ∧ (2 · (2 · (2 · S (2 · (2 · (2 · S (2 · S (2 · S (2 · S (2 · S (2 · S (2 · (2 · (2 · S (2 · (2 · S (2 · (2 · S (2 · S (2 · (2 · (2 · (2 · 1)))))))))))))))))))))) = 0 · 0 + 2 · S (2 · (2 · (2 · S (2 · (2 · S (2 · 1)))))) · (2 · (2 · S (2 · (2 · (2 · (2 · S (2 · (2 · (2 · (2 · S (2 · S (2 · (2 · S (2 · (2 · 1))))))))))))))) + (0 · 0 + 2 · S (2 · S (2 · (2 · (2 · (2 · 1))))) · 0) ∧ 0 = 0 · (2 · (2 · (2 · S (2 · S (2 · (2 · S (2 · S (2 · (2 · S (2 · (2 · (2 · S (2 · S (2 · 1)))))))))))))) + 2 · S (2 · (2 · (2 · S (2 · (2 · S (2 · 1)))))) · 0 + (0 · (2 · (2 · S (2 · (2 · (2 · (2 · S (2 · (2 · (2 · (2 · S (2 · S (2 · (2 · S (2 · (2 · 1))))))))))))))) + (2 · S (2 · S (2 · (2 · (2 · (2 · 1))))) · 0 + 0 · 0)) ∧ (2 · (2 · (2 · S (2 · (2 · (2 · S (2 · S (2 · S (2 · S (2 · S (2 · S (2 · (2 · (2 · S (2 · (2 · S (2 · (2 · S (2 · S (2 · (2 · (2 · (2 · 1)))))))))))))))))))))) = 0 · 0 + (2 · S (2 · (2 · (2 · S (2 · (2 · S (2 · 1)))))) · (2 · (2 · (2 · S (2 · S (2 · (2 · S (2 · S (2 · (2 · S (2 · (2 · (2 · S (2 · S (2 · 1)))))))))))))) + 0 · 0) + (2 · S (2 · S (2 · (2 · (2 · (2 · 1))))) · (2 · (2 · S (2 · (2 · (2 · (2 · S (2 · (2 · (2 · (2 · S (2 · S (2 · (2 · S (2 · (2 · 1))))))))))))))) + (0 · 0 + 2 · S (2 · (2 · S (2 · (2 · 1)))) · 0)) ∧ 0 = 0 · (2 · (2 · S (2 · S (2 · (2 · (2 · (2 · (2 · (2 · (2 · (2 · S (2 · S (2 · (2 · 1)))))))))))))) + (2 · S (2 · (2 · (2 · S (2 · (2 · S (2 · 1)))))) · 0 + 0 · (2 · (2 · (2 · S (2 · S (2 · (2 · S (2 · S (2 · (2 · S (2 · (2 · (2 · S (2 · S (2 · 1))))))))))))))) + (2 · S (2 · S (2 · (2 · (2 · (2 · 1))))) · 0 + 0 · (2 · (2 · S (2 · (2 · (2 · (2 · S (2 · (2 · (2 · (2 · S (2 · S (2 · (2 · S (2 · (2 · 1))))))))))))))) + (2 · S (2 · (2 · S (2 · (2 · 1)))) · 0 + 0 · 0))))No displayed named abbreviation.
Complete certificate and independent checks
456 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: d726769334d24cee7d918bed620ab71b89fabcd9e0a14bcd18f47d9399d8595e
Bundle SHA-256: 8ba81fc9bda0364c60ee78c7198be6296945bd1a5db20503a3cf6059b725672e
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.
Scope
complete exact subconjunction child
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.