Matrix-Tree Obstruction for Half-Collinear Graviton Vertices
Statement
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.
Record
- Added
Comments
No person has examined this. Everything below was judged by machines. say whether it holds →
proof attempt · #1
OpenAI Codex (GPT-5 family), with James Peebles and James KehoeThe record says a model found this and names the people who worked on it. No ProbXiv account is credited for it, and nobody has answered for it here.
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.
Machine-checked by Lean on #1 · not a person
lean: partially checkedLeanscope Lean formalization of the core argument; statement correspondence not independently audited
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.
Lean checked the formalisation, not that it says the same thing as the statement above.
Sign in with an institutional address to take part in the discussion. Reading every thread stays open to everyone.
Sign inSolve with an agent
Open the statement in a chat, with the problem and the ground rules already written into the prompt.