GraphFillingDisks.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Actual filling contours for mixed real and masked period graphs. Only the graph fibers at free points and the original marked band intervals enter the collision argument. Empty fibers outside a mask are allowed.

theorem OAI.CircleDomainRigidity.FiniteTransfer.reciprocalGraphLevel_unique_of_subsingleton line 15
theorem OAI.CircleDomainRigidity.FiniteTransfer.latticeBandIncidence_of_reciprocalGraphLevel line 22
theorem OAI.CircleDomainRigidity.FiniteTransfer.no_two_flagged_graph_grids_outside_terminals line 41
theorem OAI.CircleDomainRigidity.FiniteTransfer.lower_obstacle_singleton_of_compatible_graphs line 70

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_filling_disks_of_compatible_graphs line 142

Source documentation

Compact band grids admit filling disks by free-point compatibility and the selected collision terminals.

theorem exists_filling_disks_of_compatible_graphs
    (hsard : SmoothPlanarSard) (hschoenflies : PlanarSchoenflies)
    (G : Set Sphere) (π : Sphere → Sphere) (hπ : Continuous π)
    (hclosed : IsClosedMap π) (hsurj : Surjective π)
    (hr : ∀ x y, π x = π y ↔
      x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x))
    {n N : ℕ} {P S : Type*} (R : Fin n → Set (Sphere × UnitAddCircle)) (hR : ∀ i, IsClosed (R i))
    (σ : S → Sphere) (a b : Fin n → S → ℝ) (θ : Fin n → ℝ)
    (pairs : P → Fin n × Fin n)
    (hpairs : ∀ i j : Fin n, i ≠ j → ∃ p, pairs p = (i, j) ∨ pairs p = (j, i))
    (F : Set S)
    (hband : ∀ i s, {t : UnitAddCircle | (σ s, t) ∈ R i} ⊆
…

Mentions: OAI.CircleDomainRigidity.SmoothPlanarSard, OAI.CircleDomainRigidity.PlanarSchoenflies, OAI.CircleDomainRigidity.Sphere