P10 — p10

Exact named statement

∃ x. 2 · (2 · 2) · (2 · (2 · 2)) · (2 · (2 · 2) · (2 · 2 · (2 · 2))) · (2 · (2 · 2) · (2 · 2 · (2 · 2)) · (2 · (2 · 2) · (2 · 2 · (2 · 2)))) · (2 · (2 · 2) · (2 · 2 · (2 · 2)) · (2 · (2 · 2) · (2 · 2 · (2 · 2))) · (2 · (2 · 2) · (2 · 2 · (2 · 2)) · (2 · (2 · 2) · (2 · 2 · (2 · 2))))) · (3 · 3 · (3 · (3 · 3)) · (3 · (3 · 3) · (3 · (3 · 3))) · (7 · 7 · (7 · (7 · 7)))) + x = 2 · 2 · (2 · (2 · 2)) · (2 · (2 · 2) · (2 · (2 · 2))) · (2 · 2 · (2 · (2 · 2)) · (2 · (2 · 2) · (2 · (2 · 2)))) · (2 · 2 · (2 · (2 · 2)) · (2 · (2 · 2) · (2 · (2 · 2))) · (2 · 2 · (2 · (2 · 2)) · (2 · (2 · 2) · (2 · (2 · 2))))) · (2 · 2 · (2 · (2 · 2)) · (2 · (2 · 2) · (2 · (2 · 2))) · (2 · 2 · (2 · (2 · 2)) · (2 · (2 · 2) · (2 · (2 · 2)))) · (2 · 2 · (2 · (2 · 2)) · (2 · (2 · 2) · (2 · (2 · 2))) · (2 · 2 · (2 · (2 · 2)) · (2 · (2 · 2) · (2 · (2 · 2))))))

No displayed named abbreviation.

Fully expanded target AST

Complete certificate and independent checks

1486 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: 80dd8b78cf3a77c81e05f935df83684e6c758c2614521a877530097572cb61ee
Bundle SHA-256: 5e54a78d26b2ab9c9ea9159abbe793281c84bf9baab4312bf9bb0cbb59dae9f4

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

full fixed P10 not IR064

None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.