Matrix-Tree Obstruction for Half-Collinear Graviton Vertices
In the half-collinear single-minus graviton recursion of Guevara, Lupsasca, Skinner, Strominger and Weil, the multipoint vertex weights depend on global cut tests, which blocks a direct matrix-tree formula outside a restricted decay region. The paper's footnote 4 states the obstruction and its conclusion leaves the general simplification to future work. This result identifies those cut tests as exactly positive-flow conditions, making each retarded vertex a weighted enumerator of directed spanning-tree root cones containing a kinematic netflow vector, so the directed Matrix-Tree Theorem applies whenever the feasible trees form a complete arborescence family.
- Result
- Proved(see note)
- Status
- Partial result
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Scattering amplitudes; directed spanning trees
- Posed by
- Alfredo Guevara, Alexandru Lupsasca, David Skinner, Andrew Strominger, Kevin Weil
- Year posed
- 2026
- Years open
- 0y
- Solved
- 2026-08-09
- Model
- OpenAI Codex (GPT-5 family)
- Vendor
- OpenAI
- Collaborators
- James Peebles, James Kehoe
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Significance
- 8 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Answers the obstruction rather than the whole question: it says exactly when the Matrix-Tree Theorem can be applied and classifies the chambers, and gives a compact five-graviton formula outside the decay region. Simplifying the general solution, which is what the source paper left to future work, remains open.
What the AI did
From the submission: under human direction, OpenAI Codex proposed the root-cone interpretation, developed the proof, wrote the exact enumeration and verification programs, found the non-decay five-point chamber identity, and drafted the manuscript. A separate model acting as referee reconstructed the published recursion and re-derived the principal claims with fresh code.
Verification
The conceptual cut, flow and root-cone equivalence is formalized in Lean 4 with no sorry and no custom axioms; principal declarations are guarded by assert_no_sorry with axioms printed, and CI runs lake build --wfail plus leanchecker. Curator check: the linked run completed successfully and the 293-line formalization contains no sorry, admit or native_decide and declares no axioms of its own. The label covers the formalized core only. The chamber counts, determinant identities, realizability count and five-point formula are exact-code checked, not Lean-checked. Nobody independent has audited the informal-to-formal correspondence, and no domain expert has endorsed the result. The work is self-published rather than submitted to a venue.
Sources
- Lean proofPassing verification workflow
- CodeRepository
Submitted by PluckyCobra527 on