Strong Papadimitriou–Ratajczak Conjecture: Lean evidence

Exact recorded Lean statement

The declaration this evidence supports

theorem strong_pr_conjecture
    (hd : IsOriginalDrawing G Finset.univ p arc)
    (hcard : 4 ≤ (Finset.univ : Finset V).card)
    (hcuts : ∀ X : Finset V, X.card ≤ 2 → ConnectedOn G (Finset.univ \ X)) :
    ∃ (q : V → Plane)
    (F : List (NativeFaceBoundary G))
    (_ : IsNativeFaceFamily Finset.univ arc (mappedOriginalGraph G Finset.univ p) F)
    (o : {f : NativeFaceBoundary G // f ∈ F})
    (bodies : {f : NativeFaceBoundary G // f ∈ F} → Set Plane)
    (H : Plane ≃ₜ Plane),
    Function.Injective q
    ∧ IsOriginalDrawing G Finset.univ q (originalStraightArc q)
    ∧ (∀ s t : V, s ≠ t → ∃ a, G.Adj s a ∧ dist (q t) (q a) + 3 / 4 ≤ dist (q t) (q s))
    ∧ (∀ s t : V, s ≠ t → ∃ a, G.Adj s a ∧ 1 ≤ dist (q t) (q s)^2 - dist (q t) (q a)^2)
    ∧ (∀ (d : G.Dart) (v : V), q v ∈ segment ℝ (q d.fst) (q d.snd) ↔ v = d.fst ∨ v = d.snd)
    ∧ (∀ d e : G.Dart, d.edge ≠ e.edge → segment ℝ (q d.fst) (q d.snd) ∩ segment ℝ (q e.fst) (q
        e.snd) = q '' (({d.fst, d.snd} : Set V) ∩ {e.fst, e.snd}))
    ∧ ¬Bornology.IsBounded o.val.region
    ∧ (∀ f : {f : NativeFaceBoundary G // f ∈ F}, IsStrictConvexCycle q (if f = o then
        f.val.walk.reverse else f.val.walk) (bodies f))
    ∧ (∀ f : {f : NativeFaceBoundary G // f ∈ F}, H '' f.val.region = if f = o then (bodies f)ᶜ
        else interior (bodies f))
    ∧ (∀ (f : {f : NativeFaceBoundary G // f ∈ F}) z, z ∈ (if f = o then (bodies f)ᶜ else
        interior (bodies f)) → originalFace G Finset.univ q (originalStraightArc q) z = if f = o
        then (bodies f)ᶜ else interior (bodies f))
    ∧ (∀ v : V, H (p v) = q v)
    ∧ (∀ (d : G.Dart) (t : unitInterval), H (hd.dartPath d (Finset.mem_univ _) (Finset.mem_univ
        _) t) = Path.segment (q d.fst) (q d.snd) t)
    ∧ (∀ (η : C(unitInterval, Plane)) (hη : η 1 = η 0) (x : Plane) (hx : ∀ t, η t ≠ x),
        planeLoopWinding ((H : C(Plane, Plane)).comp η) (congrArg H hη) (H x) (fun t he => hx t
        (H.injective he)) = planeLoopWinding η hη x hx)
    ∧ ∀ d : G.Dart, IsStraightClockwiseSuccessor Finset.univ q d (nativeVertexPermutation F d)