Prove2Me

Claim 9 — choice-pair domination and external separation

Proved
FoucaudIdentification.DiameterTwo.claim_9

by Shuze Chen · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theorygraph-theoryp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let P satisfy Property 5, S be a solution of the ambient interval graph G, and {u,v} a choice pair with S∩D(uv)=SD. Each of u and v is dominated, separated from every vertex in D(uv), and separated from every vertex whose interval intersects no interval of D(uv). Each witness belongs to S, as in the printed conclusion; no claim that all witnesses belong to SD is added.

Differences from the source:

  • encoding: arbitrary finite simple graphs → simple graphs on Fin n, with n ranging over all natural numbers; reason: finite relabeling preserves every source instance, including the empty graph
  • encoding: a graph distinguishing problem based on domination and separation → two explicit relations, with solutions defined by domination and separation of all distinct pairs; reason: Property 5 and the dominating-gadget conditions are stated separately; no computation-time premise is added
  • encoding: an ambient interval graph with the displayed gadgets → an explicit interval representation and injective induced-copy maps satisfying the printed placement conditions; reason: the representations and maps expose the source geometry and do not assume the later cost or correctness conclusions
Preamble
import Definitions.Def_FoucaudIdentification_DiameterTwo_ChoicePair
Formal statement
namespace FoucaudIdentification.DiameterTwo

theorem claim_9 (P : DistinguishingProblem) (hP : SatisfiesProperty5 P)
    (d n : ℕ) (G : SimpleGraph (Fin n)) (I : IntervalModel (Fin n)) (hI : I.represents G)
    (c : ChoicePair P d n G I) (S : Finset (Fin n)) (hS : P.solution G S)
    (hstd : S ∩ c.gadget.vertices = c.gadget.standardSet) :
    ∀ u ∈ c.ends,
      (∃ x ∈ S, P.dom G x u) ∧
      (∀ v ∈ c.gadget.vertices, ∃ x ∈ S, P.sep G x u v) ∧
      (∀ v, (∀ y ∈ c.gadget.vertices, ¬ I.meets v y) →
        ∃ x ∈ S, P.sep G x u v) := by sorry

end FoucaudIdentification.DiameterTwo
Source
Foucaud et al., arXiv:1405.2424v3, Claim 9, p. 6. https://arxiv.org/abs/1405.2424v3
Human review

  • Endorsed by Community (Bot) · Oct 31, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Shuze Chen · Oct 31, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph