Verify AlphaProof Nexus port docker builds (6 unverified PRs)

[rjwalters]

Follow-up to epic #20732. Six of the seven AlphaProof Nexus integration PRs merged with no docker-build verification — the syntactic adaptations look clean but no port has been confirmed to elaborate beyond the smallest case.

Goal. Run ./proofs/scripts/docker-build.sh for each newly added file. Each build is independent.

Checklist

• ./proofs/scripts/docker-build.sh Proofs.Erdos12ProblemAPNPartI — PR Integrate AlphaProof Nexus proof for Erdős #12 (parts i, ii) #20835 (closes Integrate AlphaProof Nexus proof for Erdős #12 (parts i, ii) #20733)
• ./proofs/scripts/docker-build.sh Proofs.Erdos12ProblemAPNPartII — PR Integrate AlphaProof Nexus proof for Erdős #12 (parts i, ii) #20835 (closes Integrate AlphaProof Nexus proof for Erdős #12 (parts i, ii) #20733)
• ./proofs/scripts/docker-build.sh Proofs.Erdos125PositiveLowerDensity — PR Integrate AlphaProof Nexus port for Erdős #125 (positive_lower_density variant) #20834 (closes Integrate AlphaProof Nexus proof for Erdős #125 (positive_lower_density variant) #20734) — has 14 sorries (tracked separately)
• ./proofs/scripts/docker-build.sh Proofs.Erdos138Problem — PR research(erdos-138): integrate AlphaProof Nexus difference-variant proof #20836 (closes Integrate AlphaProof Nexus proof for Erdős #138 (difference variant) #20735) — already verified during sweep
• ./proofs/scripts/docker-build.sh Proofs.Erdos26APN_Tenenbaum — PR research(erdos-26): integrate AlphaProof Nexus Tenenbaum-variant proof #20837 (closes Integrate AlphaProof Nexus proof for Erdős #26 (Tenenbaum variant) #20736)
• ./proofs/scripts/docker-build.sh Proofs.Erdos741ProblemAPNPartI — PR research(erdos-741): integrate AlphaProof Nexus parts i + ii #20838 (closes Integrate AlphaProof Nexus proof for Erdős #741 (parts i, ii) #20737)
• ./proofs/scripts/docker-build.sh Proofs.Erdos741ProblemAPNPartII — PR research(erdos-741): integrate AlphaProof Nexus parts i + ii #20838 (closes Integrate AlphaProof Nexus proof for Erdős #741 (parts i, ii) #20737)
• ./proofs/scripts/docker-build.sh Proofs.Erdos152ProblemAPN — PR Integrate AlphaProof Nexus proof for Erdős #152 (weak form resolved) #20839 (closes Integrate AlphaProof Nexus proof for Erdős #152 (Isolated Elements in Sidon Sumsets) #20738)
• ./proofs/scripts/docker-build.sh Proofs.Erdos846ProblemAPN — PR research(erdos-846): integrate AlphaProof Nexus refutation #20840 (closes Integrate AlphaProof Nexus proof for Erdős #846 (Non-Trilinear Subsets of the Plane) #20739)

On failure

For each port that fails to elaborate:

1. File a child Doctor issue with the error excerpt.
2. The most likely failure class is leftover namespace-qualified references inside delta/simp_all/show/change/apply/exact calls (the recurring class that hit PRs research(erdos-138): integrate AlphaProof Nexus difference-variant proof #20836, research(erdos-741): integrate AlphaProof Nexus parts i + ii #20838, Integrate AlphaProof Nexus proof for Erdős #152 (weak form resolved) #20839 during the sweep — see #FUTURE for a structural fix).
3. Mathlib v4.26.0 name drift from the original DeepMind sources (Apache-2.0 from google-deepmind/alphaproof-nexus-results) is a secondary risk.

On success

For ports with 0 axioms / 0 sorries / 0 structure-encoded assumptions, promote meta.json status: axiomatized → verified (badge can stay wip until peer-reviewed). Candidates from the sweep:

• erdos-12 (Integrate AlphaProof Nexus proof for Erdős #12 (parts i, ii) #20733), erdos-26 Tenenbaum (Integrate AlphaProof Nexus proof for Erdős #26 (Tenenbaum variant) #20736), erdos-741 i+ii (Integrate AlphaProof Nexus proof for Erdős #741 (parts i, ii) #20737), erdos-152 weak form (Integrate AlphaProof Nexus proof for Erdős #152 (Isolated Elements in Sidon Sumsets) #20738), erdos-846 (Integrate AlphaProof Nexus proof for Erdős #846 (Non-Trilinear Subsets of the Plane) #20739)

Context

Sweep summary in PR descriptions of #20834, #20835, #20836, #20837, #20838, #20839, #20840.

[rjwalters]

Tooling proposal to prevent the recurring namespace-leftover Doctor cycles: #20847.