PROVED (LEAN), the site's label. The exact finite simple-graph inequality follows from Norin–Sun's stronger bipartite-deletion bound. The frontmatter standing is derived from the accepted claim page Norin and Sun's theorem, whose acceptance evidence is the site's and the refereed uptake; the public Lean proof of their theorem is linked from that page and described below, with its provenance; the corpus has not built it, and no refereed publication of the proof itself is recorded.