The two cellulation invariants that need the crosscut theorem

Schoenflies/GeneratedStructure.lean proves seven of the nine assertions of lem:cellulation-invariants — (ii), (iii), (iv), (v), (vi), (viii) and (ix), and (i) for the edge-subdivision constructor. The two it leaves open are exactly the two whose induction step is thm:general-crosscut:

• (vii) in each realization every 2-cell boundary is a Jordan curve and the open 2-cell is its bounded complementary region;
• (i) at the split constructor.

Both are proved here. Schoenflies.crosscut_theorem does not depend on main, and neither does anything in this module.

Realizations stay outside the inductive

Schoenflies.GeneratedStructure is purely abstract — it carries no realizations at all — while (i), (vii), (viii) and (ix) are statements about realizations. RefinementStars.lean bridges that by stating its lemmas for an arbitrary Realization satisfying IsCellDecomposition, and this module follows the same pattern: the induction over the constructors is replaced by two step theorems, one per constructor, each relating a realization of the refined structure to a realization of the old one. A consumer building a sequence of stages carries the realizations itself and applies the step theorem at each stage.

The alternative — realizations as fields of the inductive — was rejected for the reason RefinementStars.lean gives: the limit argument "forgets how the decompositions were constructed", so the abstract closure and the geometric invariants must be separable. It would also force every consumer to commit to two realizations at the moment it builds an abstract stage, which thm:finite-transfer does not do.

What assertion (vii) is stated against, and why not the boundary walk

The blueprint phrases (vii) as "every 2-cell boundary walk is realized by a Jordan curve". CellStructure.boundary : γ → List γ is a raw datum on which CellStructure imposes no axiom whatever: nothing says S.boundary F is a closed walk, nothing ties it to S.sub, and nothing ties it to F. A version of (vii) phrased against it therefore needs the separate boundary-cycle invariant that the finite-transfer construction maintains.

So (vii) is stated against the cells: Realization.faceBoundary F is the union of the open cells strictly below F, and IsCellDecomposition.faceBoundary_eq_frontier identifies it with frontier (R.cell F) as soon as the open 2-cell is open. Assertion (vii) then reads: that frontier is a Jordan curve, and R.cell F is its inside. This is the content every consumer uses — (viii) needs only openness of the 2-cell, lem:star-face-mesh needs only the closed 2-cells, and the limit map needs R.cell F = inside (…). Nothing downstream reads the cyclic order of the walk.

The orientation-aware update of subdivideEdge

CellStructure.subdivideEdge cannot compute a corrected boundary from an edge list alone: a walk traverses d.edge in a definite direction, while the same interior edge occurs in the two incident face boundaries with opposite orientations. SubdivData therefore carries the new boundary lists as data, together with SubstWalk proofs that each list replaces the old closed walk in the correct direction. SubstWalk.isWalk proves that every new boundary is again a closed walk.

Blueprint

• Schoenflies.CellStructure.Realization.cellUnion, Schoenflies.CellStructure.subcells, Schoenflies.CellStructure.Realization.faceBoundary — the realized point set of a set of abstract cells, and the boundary of a 2-cell read off the abstract data.
• Schoenflies.CellStructure.Realization.IsFaceJordan — assertion (vii) of lem:cellulation-invariants, for one realization.
• Schoenflies.CellStructure.Realization.IsCellDecomposition.face_eq_of_isFaceJordan, …sub_face_eq — assertion (viii) with its openness hypothesis discharged by (vii).
• Schoenflies.CellStructure.SubdivData.IsRefinement.isFaceJordan — (vii) is preserved by an edge subdivision.
• Schoenflies.CellStructure.SplitData.IsRefinement — the split analogue of SubdivData.IsRefinement, and …IsRefinement.isCellDecomposition — assertion (i) at the split constructor.
• Schoenflies.CellStructure.SplitData.IsRefinement.refines — the one-liner RefinementStars.lean asked for, next to SubdivData.IsRefinement.refines.
• Schoenflies.CellStructure.SplitData.IsCrosscutSplit, Schoenflies.CellStructure.SplitData.IsCrosscutSplit.isRefinement, Schoenflies.CellStructure.SplitData.IsCrosscutSplit.isFaceJordan — the geometric input of one split (the ear drawn as a crosscut of the old Jordan face), and the two invariants constructed from it by Schoenflies.crosscut_theorem. This is the blueprint's "Theorem thm:general-crosscut decomposes the old open 2-cell into the disjoint union of the two new open 2-cells and the open cells of the ear, and gives closure Rᵢ = Rᵢ ∪ P ∪ Bᵢ".
• Schoenflies.CellStructure.SubdivData.SubstWalk, Schoenflies.CellStructure.SubdivData.SubstWalk.isWalk, Schoenflies.CellStructure.SubdivData.boundary_isWalk — the orientation-aware boundary-walk update. Not a blueprint statement: the blueprint's operation 1 does not spell the update out, and this is what it has to be.

def Schoenflies.CellStructure.subcells {γ : Type u_1} (S : CellStructure γ) (τ : γ) : Set γ

The subcells of a cell: the index set of its closed cell in assertion (i).

Equations

• S.subcells τ = {σ : γ | σ ∈ S.cells ∧ S.sub σ τ}

theorem Schoenflies.CellStructure.mem_subcells_iff {γ : Type u_1} {S : CellStructure γ} {σ τ : γ} : σ ∈ S.subcells τ ↔ σ ∈ S.cells ∧ S.sub σ τ

theorem Schoenflies.CellStructure.subcells_subset_cells {γ : Type u_1} {S : CellStructure γ} {τ : γ} : S.subcells τ ⊆ S.cells

The realized point set of a set of cells

Every geometric statement of lem:cellulation-invariants is about a union of open cells: the closure of a cell, the boundary of a 2-cell, the realized ear, the realized boundary path. One notation serves them all.

def Schoenflies.CellStructure.Realization.cellUnion {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) (Cs : Set γ) : Set Plane

The realized point set of a set of abstract cells: the union of their open cells.

Equations

• R.cellUnion Cs = ⋃ σ ∈ Cs, R.cell σ

theorem Schoenflies.CellStructure.Realization.mem_cellUnion_iff {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {Cs : Set γ} {z : Plane} : z ∈ R.cellUnion Cs ↔ ∃ σ ∈ Cs, z ∈ R.cell σ

theorem Schoenflies.CellStructure.Realization.cellUnion_mono {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {Cs Ds : Set γ} (h : Cs ⊆ Ds) : R.cellUnion Cs ⊆ R.cellUnion Ds

theorem Schoenflies.CellStructure.Realization.cell_subset_cellUnion {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {σ : γ} {Cs : Set γ} (h : σ ∈ Cs) : R.cell σ ⊆ R.cellUnion Cs

theorem Schoenflies.CellStructure.Realization.cellUnion_union {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) (Cs Ds : Set γ) : R.cellUnion (Cs ∪ Ds) = R.cellUnion Cs ∪ R.cellUnion Ds

theorem Schoenflies.CellStructure.Realization.cellUnion_insert {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) (σ : γ) (Cs : Set γ) : R.cellUnion (insert σ Cs) = R.cell σ ∪ R.cellUnion Cs

@[simp]

theorem Schoenflies.CellStructure.Realization.cellUnion_empty {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) : R.cellUnion ∅ = ∅

@[simp]

theorem Schoenflies.CellStructure.Realization.cellUnion_singleton {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) (σ : γ) : R.cellUnion {σ} = R.cell σ

theorem Schoenflies.CellStructure.Realization.cellUnion_pair {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) (σ τ : γ) : R.cellUnion {σ, τ} = R.cell σ ∪ R.cell τ

theorem Schoenflies.CellStructure.Realization.cellUnion_subset {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {Cs : Set γ} {A : Set Plane} (h : ∀ σ ∈ Cs, R.cell σ ⊆ A) : R.cellUnion Cs ⊆ A

theorem Schoenflies.CellStructure.Realization.cellUnion_congr {γ : Type u_1} {S₁ S₂ : CellStructure γ} {R₁ : S₁.Realization} {R₂ : S₂.Realization} {Cs : Set γ} (h : ∀ σ ∈ Cs, R₁.cell σ = R₂.cell σ) : R₁.cellUnion Cs = R₂.cellUnion Cs

Two realizations — of the same structure or of two different ones over the same names — that agree cell by cell on a set of cells realize that set by the same point set.

def Schoenflies.CellStructure.Realization.faceBoundary {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) (F : γ) : Set Plane

The realized boundary of a 2-cell, read off the abstract data: the union of the open cells strictly below it. Under assertion (i) this is the topological frontier of the open 2-cell (IsCellDecomposition.faceBoundary_eq_frontier), which is what makes it the right thing for the blueprint's "boundary walk of F" without a walk being available.

Equations

• R.faceBoundary F = R.cellUnion (S.subcells F \ {F})

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.closure_cell_eq {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {τ : γ} (h : R.IsCellDecomposition D) (hτ : τ ∈ S.cells) : closure (R.cell τ) = R.cellUnion (S.subcells τ)

Assertion (i)'s closure clause, in cellUnion notation.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.mem_subcells_self {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {τ : γ} (h : R.IsCellDecomposition D) (hτ : τ ∈ S.cells) : τ ∈ S.subcells τ

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.closure_cell_eq_union {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {τ : γ} (h : R.IsCellDecomposition D) (hτ : τ ∈ S.cells) : closure (R.cell τ) = R.cell τ ∪ R.faceBoundary τ

A closed cell is its open cell together with the open cells strictly below it.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.disjoint_faceBoundary {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {τ : γ} (h : R.IsCellDecomposition D) (hτ : τ ∈ S.cells) : Disjoint (R.cell τ) (R.faceBoundary τ)

The open cells strictly below τ miss the open cell τ.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.faceBoundary_eq_frontier {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {τ : γ} (h : R.IsCellDecomposition D) (hτ : τ ∈ S.cells) (hopen : IsOpen (R.cell τ)) : R.faceBoundary τ = frontier (R.cell τ)

The realized boundary of an open cell is its frontier. The blueprint reads the boundary of a 2-cell off the cells below it; this says that reading agrees with the topology, which is what lets assertion (vii) be stated without the boundary-walk datum.

Assertion (vii)

"In each of the two realizations, every 2-cell boundary walk is realized by a Jordan curve, and the open 2-cell is the bounded complementary region of that curve."

Schoenflies.inside is the union of the bounded complementary components of a set, so "the bounded complementary region of the Jordan curve J" is literally inside J; and by Schoenflies.jordan_curve_theorem it is a single region.

structure Schoenflies.CellStructure.Realization.IsFaceJordan {γ : Type u_1} {S : CellStructure γ} (R : S.Realization) : Prop

Assertion (vii) of `lem:cellulation-invariants**, for one realization: every open 2-cell is the bounded complementary region of a Jordan curve, namely its own frontier.

Stated against frontier (R.cell F) rather than against the boundary walk; see the module docstring. Under assertion (i) the frontier is the union of the open cells strictly below F (IsCellDecomposition.faceBoundary_eq_frontier), which is the blueprint's boundary walk read as a set.

• isJordanCurve ⦃F : γ⦄ : F ∈ S.faces → IsJordanCurve (frontier (R.cell F))

  The boundary of every 2-cell is a Jordan curve.

• cell_eq_inside ⦃F : γ⦄ : F ∈ S.faces → R.cell F = inside (frontier (R.cell F))

  The open 2-cell is the bounded complementary region of that curve.

theorem Schoenflies.CellStructure.Realization.IsFaceJordan.isSeparating {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {F : γ} (hJ : R.IsFaceJordan) (hF : F ∈ S.faces) : IsSeparating (frontier (R.cell F))

Each 2-cell boundary separates the plane. This is where thm:jordan enters; it is independent of main.

theorem Schoenflies.CellStructure.Realization.IsFaceJordan.isOpen {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {F : γ} (hJ : R.IsFaceJordan) (hF : F ∈ S.faces) : IsOpen (R.cell F)

An open 2-cell is open. This is the clause lem:cellulation-invariants(viii) needs, and the only thing the blueprint's proof of (viii) really uses.

theorem Schoenflies.CellStructure.Realization.IsFaceJordan.isConnected {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {F : γ} (hJ : R.IsFaceJordan) (hF : F ∈ S.faces) : IsConnected (R.cell F)

theorem Schoenflies.CellStructure.Realization.IsFaceJordan.isBounded {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {F : γ} (hJ : R.IsFaceJordan) (hF : F ∈ S.faces) : Bornology.IsBounded (R.cell F)

theorem Schoenflies.CellStructure.Realization.IsFaceJordan.nonempty {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {F : γ} (hJ : R.IsFaceJordan) (hF : F ∈ S.faces) : (R.cell F).Nonempty

theorem Schoenflies.CellStructure.Realization.IsFaceJordan.isCompact_closure {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {F : γ} (hJ : R.IsFaceJordan) (hF : F ∈ S.faces) : IsCompact (closure (R.cell F))

A closed 2-cell is compact. lem:star-face-mesh measures diameters of closed 2-cells, and this is what makes those diameters finite without a hypothesis on the domain.

theorem Schoenflies.CellStructure.Realization.IsFaceJordan.faceBoundary_eq {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {F : γ} (hJ : R.IsFaceJordan) (h : R.IsCellDecomposition D) (hF : F ∈ S.faces) : R.faceBoundary F = frontier (R.cell F)

Assertion (vii) in the blueprint's own words: the union of the open cells strictly below a 2-cell is a Jordan curve, and the open 2-cell is its bounded complementary region.

theorem Schoenflies.CellStructure.Realization.IsFaceJordan.isJordanCurve_faceBoundary {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {F : γ} (hJ : R.IsFaceJordan) (h : R.IsCellDecomposition D) (hF : F ∈ S.faces) : IsJordanCurve (R.faceBoundary F)

theorem Schoenflies.CellStructure.Realization.IsFaceJordan.cell_eq_inside_faceBoundary {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {F : γ} (hJ : R.IsFaceJordan) (h : R.IsCellDecomposition D) (hF : F ∈ S.faces) : R.cell F = inside (R.faceBoundary F)

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.face_eq_of_isFaceJordan {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {F T : γ} (h : R.IsCellDecomposition D) (hJ : R.IsFaceJordan) (hF : F ∈ S.faces) (hT : T ∈ S.faces) (hsub : R.cell F ⊆ closure (R.cell T)) : F = T

Assertion (viii), with the openness hypothesis of IsCellDecomposition.face_eq discharged by assertion (vii): distinct open 2-cells are never comparable.

theorem Schoenflies.CellStructure.Realization.IsCellDecomposition.sub_face_eq {γ : Type u_1} {S : CellStructure γ} {R : S.Realization} {D : Set Plane} {F T : γ} (h : R.IsCellDecomposition D) (hJ : R.IsFaceJordan) (hF : F ∈ S.faces) (hT : T ∈ S.faces) (hsub : S.sub F T) : F = T

Assertion (viii) against the abstract relation.

Assertion (vii) is preserved by an edge subdivision

"An edge subdivision changes no 2-cell." Literally: the 2-cells of S.subdivideEdge d are those of S, and each is an old cell distinct from the subdivided edge, so SubdivData.IsRefinement leaves its open cell exactly where it was.

theorem Schoenflies.CellStructure.SubdivData.IsRefinement.cell_face_eq {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} {R' : (S.subdivideEdge d).Realization} {F : γ} (href : d.IsRefinement R R') (hF : F ∈ S.faces) : R'.cell F = R.cell F

theorem Schoenflies.CellStructure.SubdivData.IsRefinement.isFaceJordan {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} {R' : (S.subdivideEdge d).Realization} (href : d.IsRefinement R R') (hJ : R.IsFaceJordan) : R'.IsFaceJordan

Assertion (vii) is preserved by an edge subdivision.

theorem Schoenflies.CellStructure.SubdivData.IsRefinement.isCellDecomposition_and_isFaceJordan {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {R : S.Realization} {R' : (S.subdivideEdge d).Realization} (hS : S.CombInvariants) (href : d.IsRefinement R R') {D : Set Plane} (h : R.IsCellDecomposition D) (hJ : R.IsFaceJordan) : R'.IsCellDecomposition D ∧ R'.IsFaceJordan ∧ R'.Refines R d.parent

The induction step over the first constructor, in the shape a consumer building a sequence of stages wants: one edge subdivision carries (i), (vii) and Realization.Refines forward together. The mirror of SplitData.IsCrosscutSplit.isCellDecomposition_and_isFaceJordan.

The orientation of the boundary-walk update

CellStructure.subdivideEdge now takes the replacement boundary lists from SubdivData. SubstWalk is a relation rather than a function because the direction of a crossing is determined by the walk and not by the edge list. The data carries one corrected list for each face together with the fact that it replaces a closed old boundary walk.

theorem Schoenflies.CellStructure.SubdivData.exists_substWalk {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) {u v : γ} {W : List γ} (h : S.skel.IsWalk u W v) : ∃ (W' : List γ), d.SubstWalk u W W'

Every walk of the old skeleton has an orientation-aware replacement.

theorem Schoenflies.CellStructure.SubdivData.newVertex_mem_skeleton_vertexSet {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) : d.newVertex ∈ d.skeleton.vertexSet

theorem Schoenflies.CellStructure.SubdivData.SubstWalk.isWalk {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {u v : γ} {W W' : List γ} (hsub : d.SubstWalk u W W') (h : S.skel.IsWalk u W v) : d.skeleton.IsWalk u W' v

The corrected replacement really is a walk of the subdivided skeleton.

theorem Schoenflies.CellStructure.SubdivData.SubstWalk.eq_of_notMem {γ : Type u_1} {S : CellStructure γ} {d : S.SubdivData} {u : γ} {W W' : List γ} (hsub : d.SubstWalk u W W') (h : d.edge ∉ W) : W' = W

On a stretch that never crosses the subdivided edge, the corrected replacement leaves the edge list alone.

theorem Schoenflies.CellStructure.SubdivData.boundary_isWalk {γ : Type u_1} {S : CellStructure γ} (d : S.SubdivData) {F : γ} (hF : F ∈ S.faces) : ∃ (u : γ), d.skeleton.IsWalk u ((S.subdivideEdge d).boundary F) u

Every updated face boundary is a closed walk of the subdivided skeleton.

Assertion (i) at the split constructor

The split analogue of SubdivData.IsRefinement, and the propagation of assertion (i) across it. The blueprint's proof of this step is exactly

thm:general-crosscut decomposes the old open 2-cell into the disjoint union of the two new open 2-cells and the open cells of the ear, and gives closure Rᵢ = Rᵢ ∪ P ∪ Bᵢ.

so those two identities, together with the incidences along the ear, are the fields of SplitData.IsRefinement; SplitData.IsCrosscutSplit below constructs them from Schoenflies.crosscut_theorem.

def Schoenflies.CellStructure.SplitData.earNewCells {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : Set γ

The cells the ear creates: its interior vertices and its edges. The two ends of the ear are old vertices, and the blueprint is explicit that the split does not create them.

Equations

• d.earNewCells = d.ear.vertexSet \ {d.source, d.target} ∪ d.ear.edgeSet

theorem Schoenflies.CellStructure.SplitData.newCells_eq {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : d.newCells = d.earNewCells ∪ {d.face₁, d.face₂}

theorem Schoenflies.CellStructure.SplitData.earNewCells_subset_newCells {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : d.earNewCells ⊆ d.newCells

theorem Schoenflies.CellStructure.SplitData.earNewCells_subset_earCells {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : d.earNewCells ⊆ d.earCells

theorem Schoenflies.CellStructure.SplitData.mem_earNewCells_of_mem_ear_vertexSet {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {z : γ} (hz : z ∈ d.ear.vertexSet) (hs : z ≠ d.source) (ht : z ≠ d.target) : z ∈ d.earNewCells

theorem Schoenflies.CellStructure.SplitData.mem_earNewCells_of_mem_ear_edgeSet {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {f : γ} (hf : f ∈ d.ear.edgeSet) : f ∈ d.earNewCells

theorem Schoenflies.CellStructure.SplitData.mem_splitFace_cells_of_earNew {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {z : γ} (hz : z ∈ d.earNewCells) : z ∈ (S.splitFace d).cells

The subcells of each kind of cell after a split

theorem Schoenflies.CellStructure.SplitData.subRel_iff_of_mem_cells {γ : Type u_1} {S : CellStructure γ} (hS : S.CombInvariants) (d : S.SplitData) {σ τ : γ} (hτc : τ ∈ S.cells) (hτf : τ ≠ d.face) : d.subRel σ τ ↔ σ ∈ S.cells ∧ σ ≠ d.face ∧ S.sub σ τ

On old cells other than the split 2-cell the relation is unchanged, and only old cells lie below such a cell. This is SplitData.old_subRel_iff with the membership of σ derived rather than assumed, which is what the closure clause of assertion (i) needs.

theorem Schoenflies.CellStructure.SplitData.subcells_of_mem_cells {γ : Type u_1} {S : CellStructure γ} (hS : S.CombInvariants) (d : S.SplitData) {τ : γ} (hτc : τ ∈ S.cells) (hτf : τ ≠ d.face) : (S.splitFace d).subcells τ = S.subcells τ

The subcells of a surviving cell are its old subcells.

theorem Schoenflies.CellStructure.SplitData.subRel_earVertex_iff {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {z σ : γ} (hz : z ∈ d.ear.vertexSet) (hs : z ≠ d.source) (ht : z ≠ d.target) : d.subRel σ z ↔ σ = z

Nothing lies below an interior vertex of the ear but the vertex itself.

theorem Schoenflies.CellStructure.SplitData.subRel_earEdge_iff {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {f a b σ : γ} (hl : d.ear.IsLink f a b) : d.subRel σ f ↔ σ = f ∨ σ = a ∨ σ = b

The cells below an ear edge are it and its two endpoints.

theorem Schoenflies.CellStructure.SplitData.subcells_earVertex {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {z : γ} (hz : z ∈ d.ear.vertexSet) (hs : z ≠ d.source) (ht : z ≠ d.target) : (S.splitFace d).subcells z = {z}

theorem Schoenflies.CellStructure.SplitData.subcells_earEdge {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) {f a b : γ} (hl : d.ear.IsLink f a b) : (S.splitFace d).subcells f = {f, a, b}

theorem Schoenflies.CellStructure.SplitData.subcells_face₁ {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : (S.splitFace d).subcells d.face₁ = {d.face₁} ∪ d.earCells ∪ d.cells₁

theorem Schoenflies.CellStructure.SplitData.subcells_face₂ {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) : (S.splitFace d).subcells d.face₂ = {d.face₂} ∪ d.earCells ∪ d.cells₂

The refinement relation of one split

structure Schoenflies.CellStructure.SplitData.IsRefinement {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) (R : S.Realization) (R' : (S.splitFace d).Realization) : Prop

R' refines R along the split d. The fields are the blueprint's own sentences: the old open 2-cell is the disjoint union of the two new open 2-cells and the open cells of the ear; the closure of each new 2-cell is itself together with the ear and its own boundary path; and the ear's own cells are incident as a path.

Exactly as with SubdivData.IsRefinement, this is local data — it speaks only of the cells the split creates and of the split 2-cell — and IsRefinement.isCellDecomposition upgrades it to assertion (i) for the whole refined structure. IsCrosscutSplit.isRefinement constructs it from thm:general-crosscut.

• cell_eq ⦃σ : γ⦄ : σ ∈ S.cells → σ ≠ d.face → R'.cell σ = R.cell σ

  Surviving cells are unmoved.

• cell_face : R.cell d.face = R'.cell d.face₁ ∪ R'.cell d.face₂ ∪ R'.cellUnion d.earNewCells

  The old open 2-cell is the two new open 2-cells together with the open cells of the ear.

• nonempty ⦃σ : γ⦄ : σ ∈ d.newCells → (R'.cell σ).Nonempty

  The new open cells are nonempty.

• disjoint ⦃σ τ : γ⦄ : σ ∈ d.newCells → τ ∈ d.newCells → σ ≠ τ → Disjoint (R'.cell σ) (R'.cell τ)

  …and pairwise disjoint.

• closure_earVertex ⦃z : γ⦄ : z ∈ d.ear.vertexSet → z ≠ d.source → z ≠ d.target → closure (R'.cell z) = R'.cell z

  An interior vertex of the ear is a closed cell.

• closure_earEdge ⦃f a b : γ⦄ : d.ear.IsLink f a b → closure (R'.cell f) = R'.cell f ∪ (R'.cell a ∪ R'.cell b)

  The closure of an ear edge is it together with its two endpoints.

• closure_face₁ : closure (R'.cell d.face₁) = R'.cell d.face₁ ∪ R'.cellUnion d.earCells ∪ R'.cellUnion d.cells₁

  closure R₁ = R₁ ∪ P ∪ B₁.

• closure_face₂ : closure (R'.cell d.face₂) = R'.cell d.face₂ ∪ R'.cellUnion d.earCells ∪ R'.cellUnion d.cells₂

  closure R₂ = R₂ ∪ P ∪ B₂.

theorem Schoenflies.CellStructure.SplitData.IsRefinement.cell_subset_face {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {R' : (S.splitFace d).Realization} (href : d.IsRefinement R R') {σ : γ} (hσ : σ ∈ d.newCells) : R'.cell σ ⊆ R.cell d.face

Every cell the split creates lies inside the old open 2-cell.

theorem Schoenflies.CellStructure.SplitData.IsRefinement.isCellDecomposition {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {R' : (S.splitFace d).Realization} {D : Set Plane} (hS : S.CombInvariants) (href : d.IsRefinement R R') (h : R.IsCellDecomposition D) : R'.IsCellDecomposition D

Assertion (i) is preserved by a 2-cell split.

theorem Schoenflies.CellStructure.SplitData.IsRefinement.refines {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {R' : (S.splitFace d).Realization} {D : Set Plane} (hS : S.CombInvariants) (href : d.IsRefinement R R') (h : R.IsCellDecomposition D) : R'.Refines R d.parent

A 2-cell split is a refinement, in the sense of Realization.Refines. The one-liner RefinementStars.lean left for this module, beside SubdivData.IsRefinement.refines; it feeds SplitData.refines the argument h' that module could not construct.

The geometric input of one split, and the two invariants constructed from it

thm:general-crosscut is applied here, and only here. Its two standing hypotheses on main — thm:jordan and HasArcCollars — are both discharged: the first by Schoenflies.jordan_curve_theorem, the second by Schoenflies.IsCrosscut.hasArcCollars, which is why IsCrosscutSplit need not mention either.

structure Schoenflies.CellStructure.SplitData.IsCrosscutSplit {γ : Type u_1} {S : CellStructure γ} (d : S.SplitData) (R : S.Realization) (R' : (S.splitFace d).Realization) : Prop

The geometric input of one 2-cell split: the realized ear is a polygonal crosscut of the Jordan region realizing the split 2-cell, the two abstract boundary paths realize the two arcs that crosscut cuts the boundary curve into, and the two new open 2-cells are the two sides.

Everything the split needs downstream — assertion (i) at the new stage (IsCrosscutSplit.isRefinement) and assertion (vii) at the new stage (IsCrosscutSplit.isFaceJordan) — is constructed from this by Schoenflies.crosscut_theorem, not assumed.

The four clauses about the ear's own cells are the only thing left assumed: the crosscut theorem treats the ear as a single arc P and says nothing about how the ear's vertices and edges subdivide it. They are statements about the drawing of a path graph and belong with whichever module draws the ear.

• cell_eq ⦃σ : γ⦄ : σ ∈ S.cells → σ ≠ d.face → R'.cell σ = R.cell σ

  Surviving cells are unmoved.

• isCrosscut : IsCrosscut (frontier (R.cell d.face)) (R'.cellUnion d.earCells) (R.pos d.source) (R.pos d.target)

  The realized ear is a polygonal crosscut of the old Jordan face.

• isCutPair : IsCutPair (frontier (R.cell d.face)) (R.pos d.source) (R.pos d.target) (R.cellUnion d.cells₁) (R.cellUnion d.cells₂)

  The two boundary paths realize the two arcs of the old 2-cell boundary.

• cell_face₁ : R'.cell d.face₁ = inside (R.cellUnion d.cells₁ ∪ R'.cellUnion d.earCells)

  The first new open 2-cell is the side of the crosscut bounded by the first path.

• cell_face₂ : R'.cell d.face₂ = inside (R.cellUnion d.cells₂ ∪ R'.cellUnion d.earCells)

  The second new open 2-cell is the other side.

• cellUnion_earNewCells : R'.cellUnion d.earNewCells = R'.cellUnion d.earCells \ {R.pos d.source, R.pos d.target}

  The open cells of the ear are the crosscut with its two endpoints removed.

• earNonempty ⦃σ : γ⦄ : σ ∈ d.earNewCells → (R'.cell σ).Nonempty

  The open cells the ear creates are nonempty.

• earDisjoint ⦃σ τ : γ⦄ : σ ∈ d.earNewCells → τ ∈ d.earNewCells → σ ≠ τ → Disjoint (R'.cell σ) (R'.cell τ)

  …and pairwise disjoint.

• closure_earVertex ⦃z : γ⦄ : z ∈ d.ear.vertexSet → z ≠ d.source → z ≠ d.target → closure (R'.cell z) = R'.cell z

  An interior vertex of the ear is a closed cell.

• closure_earEdge ⦃f a b : γ⦄ : d.ear.IsLink f a b → closure (R'.cell f) = R'.cell f ∪ (R'.cell a ∪ R'.cell b)

  The closure of an ear edge is it together with its two endpoints.

theorem Schoenflies.CellStructure.SplitData.IsCrosscutSplit.cellUnion_cells₁ {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {R' : (S.splitFace d).Realization} (hc : d.IsCrosscutSplit R R') : R'.cellUnion d.cells₁ = R.cellUnion d.cells₁

The boundary paths are realized identically before and after the split: their cells are old cells, and none of them is the split 2-cell.

theorem Schoenflies.CellStructure.SplitData.IsCrosscutSplit.cellUnion_cells₂ {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {R' : (S.splitFace d).Realization} (hc : d.IsCrosscutSplit R R') : R'.cellUnion d.cells₂ = R.cellUnion d.cells₂

theorem Schoenflies.CellStructure.SplitData.IsCrosscutSplit.cell_earNew_subset {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {R' : (S.splitFace d).Realization} (hc : d.IsCrosscutSplit R R') {σ : γ} (hσ : σ ∈ d.earNewCells) : R'.cell σ ⊆ R'.cellUnion d.earCells \ {R.pos d.source, R.pos d.target}

Every open cell the ear creates lies in the open crosscut.

theorem Schoenflies.CellStructure.SplitData.IsCrosscutSplit.frontier_face₁ {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {R' : (S.splitFace d).Realization} (hc : d.IsCrosscutSplit R R') : frontier (R'.cell d.face₁) = R.cellUnion d.cells₁ ∪ R'.cellUnion d.earCells

The Jordan curve of the first new 2-cell is B₁ ∪ P.

theorem Schoenflies.CellStructure.SplitData.IsCrosscutSplit.frontier_face₂ {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {R' : (S.splitFace d).Realization} (hc : d.IsCrosscutSplit R R') : frontier (R'.cell d.face₂) = R.cellUnion d.cells₂ ∪ R'.cellUnion d.earCells

theorem Schoenflies.CellStructure.SplitData.IsCrosscutSplit.disjoint_faces {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {R' : (S.splitFace d).Realization} (hc : d.IsCrosscutSplit R R') : Disjoint (R'.cell d.face₁) (R'.cell d.face₂)

theorem Schoenflies.CellStructure.SplitData.IsCrosscutSplit.disjoint_face₁_earNew {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {R' : (S.splitFace d).Realization} (hc : d.IsCrosscutSplit R R') {σ : γ} (hσ : σ ∈ d.earNewCells) : Disjoint (R'.cell d.face₁) (R'.cell σ)

theorem Schoenflies.CellStructure.SplitData.IsCrosscutSplit.disjoint_face₂_earNew {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {R' : (S.splitFace d).Realization} (hc : d.IsCrosscutSplit R R') {σ : γ} (hσ : σ ∈ d.earNewCells) : Disjoint (R'.cell d.face₂) (R'.cell σ)

theorem Schoenflies.CellStructure.SplitData.IsCrosscutSplit.isRefinement {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {R' : (S.splitFace d).Realization} (hc : d.IsCrosscutSplit R R') (hJ : R.IsFaceJordan) : d.IsRefinement R R'

Assertion (i) at the split, constructed from thm:general-crosscut. The crosscut theorem decomposes the old open 2-cell into the two new open 2-cells and the open cells of the ear, and gives closure Rᵢ = Rᵢ ∪ P ∪ Bᵢ; those are exactly the fields of SplitData.IsRefinement that are not about the ear's own drawing.

The old instance of assertion (vii) is what identifies the old open 2-cell with the Jordan domain the crosscut cuts.

theorem Schoenflies.CellStructure.SplitData.IsCrosscutSplit.isFaceJordan {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {R' : (S.splitFace d).Realization} (hc : d.IsCrosscutSplit R R') (hJ : R.IsFaceJordan) : R'.IsFaceJordan

Assertion (vii) is preserved by a 2-cell split. The two new open 2-cells are the two sides of the crosscut, and thm:general-crosscut says each is the bounded complementary region of the Jordan curve Bᵢ ∪ P; every other 2-cell is unmoved.

theorem Schoenflies.CellStructure.SplitData.IsCrosscutSplit.isCellDecomposition_and_isFaceJordan {γ : Type u_1} {S : CellStructure γ} {d : S.SplitData} {R : S.Realization} {R' : (S.splitFace d).Realization} (hc : d.IsCrosscutSplit R R') (hS : S.CombInvariants) {D : Set Plane} (h : R.IsCellDecomposition D) (hJ : R.IsFaceJordan) : R'.IsCellDecomposition D ∧ R'.IsFaceJordan ∧ R'.Refines R d.parent

Both invariants at once: one 2-cell split of a realization satisfying (i) and (vii) produces a realization satisfying (i) and (vii), and the pair is a Realization.Refines. This is the whole induction step of lem:cellulation-invariants over the second constructor.