Solver-backed proof campaign — current evidence

Irrationality remains open

The endpoint IR072 is not proved. These are exact local subproofs, with solver hints, native HA checking and independent Lean checking kept separate. No campaign parent admission, Alpha promotion or deployment is claimed.

33 distinct checked statements in this wave; duplicate E/V demonstrations are counted once. Six are named rational foundations. Trace pieces are finite instances, not variable-degree theorems.

Explore the local definition DAG · Original pilot baseline and its historical failures.

What changed

P10 now has a shared, 1,486-node HA proof DAG and an independent Lean check. E and Vampire each selected two original premises for the narrow P08 native reconstruction; this is premise-guided reconstruction, not a TSTP proof translator. Z3 separately checked the six rational conjectures, without supplying trusted axioms.

The composition trace has 13/16 exact pieces HA-checked. Its complete assembly remains open; the separate universal constant-coefficient soundness lemma does not replace the missing execution pieces. Size-limited attempts remain visible below.

A critical reuse: the twice-square lemma

For natural A,B, A²=2B² implies A=B=0. The proof reduces to the existing Fermat fourth-power theorem and rechecks its complete dependency cone. This is a prerequisite for quadratic norm separation, not irrationality of (√2)^(√2).

From natural squares to signed coefficients

SN001 proves that (ap−an)²=2(bp−bn)² forces ap=an and bp=bn, with explicit natural square witnesses and no normalization assumption on the signed pairs. It reuses the exact existing SignedDifferenceSquare definition and the checked IR016 dependency cone.

Named theorem, original formula and exact proof · Reused definition ND0157. The rational/real quantitative lower bound and quadratic interpretation in IR032 remain open.

New universal arithmetic lemmas

• NG001 — Constructive natural strict gap
• SN002 — Witnessed integer norm separation
• SN003 — Signed quadratic norm multiplicativity
• CV001 — Universal natural convolution vanishing

The integer separation witness is distinct from the still-open rational/real lower bound. The convolution result concerns actual natural coefficient tables, not completed rational exp composition. Z3 separately checked the natural-gap conjecture; deterministic HA generation and fresh Lean checks provide the proof evidence.

Actual proof DAG and open planning parents · Exact definitions and theorem uses.

Exact execution evidence

Next mathematical bottlenecks

Variable-degree formal composition and its recurrence; quantitative log–exp composition tails; confluent interpolation; and the positive precision-to-certificate bridge. A finite trace or a solver hit cannot close these.

Workers use one process at a time and fixed resource caps. They make no model calls; agents wrote/reviewed the specifications and generators, and that engineering cost is not measured as zero.

Machine-readable observations · Full planned dependency cone.