Stage 0: the initial pair as a GeneratedPair

Schoenflies/FiniteTransfer.lean defines Schoenflies.GeneratedPair, the object every stage of the Schönflies recursion is and that thm:finite-transfer consumes and produces. Nothing built one. This module builds the first: the initial matched pair of prop:initial-pair, which is generated from itself by the empty sequence of elementary operations.

What has to be shown

The two realizations, the skeleton homeomorphism and weak admissibility are all in Schoenflies/InitialPair.lean and Schoenflies/InitialPairFixed.lean already, or one step from what is there. The work is the two IsCellDecomposition fields — assertion (i) of lem:cellulation-invariants — and they are the same work twice, because both realizations have the same shape: a HexData whose six outer arcs form a Jordan curve and whose chord is a crosscut of it. So assertion (i) is proved once, for an arbitrary HexData carrying that crosscut configuration (Schoenflies.HexData.isCellDecomposition), and instantiated on each side. The same is true of weak admissibility (Schoenflies.HexData.isWeaklyAdmissible).

The four clauses go as follows.

• nonempty — the seven 0-cells are points; the seven open 1-cells are arcs minus their two endpoints (IsArcBetween.nonempty_diff); the two 2-cells are the two sides of the crosscut, nonempty by thm:general-crosscut.
• disjoint — fifteen cells, but only five kinds of pair. Two vertices are distinct points; a vertex misses every open edge it is not an end of (HexData.mem_outer_iff, .mem_chord_iff), and is an end of the ones it does meet; two open edges are disjoint by the two meeting conditions of HexData; every 1- or 0-cell lies on the skeleton and every 2-cell is inside the curve and off the crosscut; and the two 2-cells are the two sides of one crosscut.
• iUnion_eq — the 0-cells and open 1-cells reassemble the skeleton C ∪ P (HexData.iUnion_cellSet), and the two 2-cells exhaust D ∖ P (thm:general-crosscut), so together they are C ∪ D.
• closure_eq — a finite case check against Schoenflies.initSub, the base value of ≼_abs that the blueprint fixes. The four initSub_iff_* lemmas below read it off, and then the only topology needed is closure (A ∖ {p, q}) = A for an arc (IsArcBetween.closure_diff) and the closure of a crosscut side (Schoenflies.crosscut_cell_partition).

The input is InitialData, not AnchoredInitialData

AnchoredInitialData adds exactly two fields, a ∈ 𝒜 and b ∈ 𝒜. Nothing in GeneratedPair mentions the anchor set: the anchoring is what lets a later stage run a fresh crosscut into a or b, and it is read off AnchoredInitialData.stronglyAccessible_a at that point. So the pair is built from InitialData — the weaker input — and Schoenflies.AnchoredInitialData.generatedPair is the one-line specialisation for a consumer holding the anchored form.

Blueprint

• Schoenflies.combInvariants_initialStructure — lem:cellulation-invariants (iii), (v), (vi) and abstract (viii) for the base structure: the base case of Schoenflies.GeneratedStructure.combInvariants, which the whole recursion needs.
• Schoenflies.initSub_iff_vert, .._edge, .._chord, .._face — the base value of ≼_abs (tex 1590–1602) read as "the subcells of each cell are exactly these".
• Schoenflies.HexData.isCellDecomposition — lem:cellulation-invariants(i) for either realization of prop:initial-pair, with HexData.iUnion_cellSet, HexData.biUnion_of_three_edges and HexData.biUnion_faceCells as its two reassembly steps.
• Schoenflies.HexData.isWeaklyAdmissible — def:admissible-graph minus the connectedness clause, for either realization.
• Schoenflies.InitialData.generatedPair, Schoenflies.AnchoredInitialData.generatedPair — def:generated-structure at stage 0: prop:initial-pair is a generated matched cellulation.
• Schoenflies.HexData.isOpen_cellSet_face, Schoenflies.InitialData.isOpen_sourceRealization_cell_face, .isOpen_targetRealization_cell_face — openness of the two 2-cells: the hypothesis lem:cellulation-invariants(viii) takes and IsCellDecomposition does not record.
• Schoenflies.infinite_initialCell — the base case meets the recursion: thm:finite-transfer needs [Infinite γ], and InitialCell supplies it through its spare constructor aux.
• Schoenflies.modelCurve_union_inside — S ∪ Int(S) = Q, the closed target domain.
• Schoenflies.InitialData.generatedPair_src_isAdmissible, .generatedPair_tgt_isAdmissible — the strong form of def:admissible-graph on both sides, which the initial pair does satisfy (rem:intermediate-disconnection waives it only at intermediate stages).

The cells of the initial structure, and ≼_abs

initialStructure declares every one of InitialCell's four named constructors a cell. The fifth, InitialCell.aux, is the spare supply of fresh names that def:generated-structure needs and that thm:finite-transfer asks for as [Infinite γ]; no aux name is a cell.

recOnCells is the shape every clause of assertion (i) below uses: case analysis on a cell, with the spare names ruled out by the membership hypothesis the clause already carries.

theorem Schoenflies.aux_notMem_cells (n : ℕ) : InitialCell.aux n ∉ initialStructure.cells

The spare names are not cells: cells is vertices ∪ edges ∪ faces, and each of those is a range of one of the four named constructors.

theorem Schoenflies.mem_cells_initialStructure_of_vert (i : Fin 6) : InitialCell.vert i ∈ initialStructure.cells

theorem Schoenflies.mem_cells_initialStructure_of_edge (i : Fin 6) : InitialCell.edge i ∈ initialStructure.cells

theorem Schoenflies.mem_cells_initialStructure_of_chord : InitialCell.chord ∈ initialStructure.cells

theorem Schoenflies.mem_cells_initialStructure_of_face (k : Bool) : InitialCell.face k ∈ initialStructure.cells

theorem Schoenflies.mem_cellNames_of_vert (i : Fin 6) : InitialCell.vert i ∈ cellNames

The four named constructors are cell names.

theorem Schoenflies.mem_cellNames_of_edge (i : Fin 6) : InitialCell.edge i ∈ cellNames

theorem Schoenflies.mem_cellNames_chord : InitialCell.chord ∈ cellNames

theorem Schoenflies.mem_cellNames_of_face (k : Bool) : InitialCell.face k ∈ cellNames

theorem Schoenflies.mem_cells_of_mem_faceCells {k : Bool} {c : InitialCell} (h : c ∈ faceCells k) : c ∈ initialStructure.cells

Every cell of a 2-cell's boundary walk is a cell.

def Schoenflies.recOnCells {motive : InitialCell → Sort u_1} {c : InitialCell} (hc : c ∈ initialStructure.cells) (hv : (i : Fin 6) → motive (InitialCell.vert i)) (he : (i : Fin 6) → motive (InitialCell.edge i)) (hch : motive InitialCell.chord) (hf : (k : Bool) → motive (InitialCell.face k)) : motive c

Case analysis on a cell of the initial structure. The four named constructors exhaust the cells; the spare aux names are excluded by the membership hypothesis.

Equations

• Schoenflies.recOnCells hc_2 hv he hch hf = hv i
• Schoenflies.recOnCells hc_2 hv he hch hf = he i
• Schoenflies.recOnCells hc_2 hv he hch hf = hch
• Schoenflies.recOnCells hc_2 hv he hch hf = hf k
• Schoenflies.recOnCells hc_2 hv he hch hf = absurd hc_2 ⋯

theorem Schoenflies.face_notMem_faceCells {k l : Bool} : InitialCell.face k ∉ faceCells l

A face name is never a 0-cell or a 1-cell.

theorem Schoenflies.initSub_iff_vert {i : Fin 6} {c : InitialCell} : initSub c (InitialCell.vert i) ↔ c = InitialCell.vert i

The subcells of a 0-cell are itself alone.

theorem Schoenflies.initSub_iff_edge {i : Fin 6} {c : InitialCell} : initSub c (InitialCell.edge i) ↔ c = InitialCell.edge i ∨ c = InitialCell.vert i ∨ c = InitialCell.vert (i + 1)

The subcells of an outer 1-cell are itself and its two ends.

theorem Schoenflies.initSub_iff_chord {c : InitialCell} : initSub c InitialCell.chord ↔ c = InitialCell.chord ∨ c = InitialCell.vert 1 ∨ c = InitialCell.vert 4

The subcells of the crosscut are itself and its two ends.

theorem Schoenflies.initSub_iff_face {k : Bool} {c : InitialCell} : initSub c (InitialCell.face k) ↔ c = InitialCell.face k ∨ c ∈ faceCells k

The subcells of a 2-cell are itself together with the cells of its boundary walk.

The combinatorial invariants at the base

Schoenflies.GeneratedStructure.combInvariants propagates lem:cellulation-invariants (iii), (v), (vi) and abstract (viii) along the two elementary operations given the base case. This is the base case. Assertion (vi) is Schoenflies.outerEdgeUniqueFace_initialStructure, already on main; the other seven clauses are read off initSub.

theorem Schoenflies.combInvariants_initialStructure : initialStructure.CombInvariants

The combinatorial invariants hold for the initial structure. The base case of Schoenflies.GeneratedStructure.combInvariants, hence of GeneratedPair.combInvariants.

The open cells of a HexData

Everything assertion (i) needs about the fifteen realized open cells, stated for an arbitrary HexData so that the source and the target realization are served by one proof. Nothing in this section mentions the crosscut configuration; that enters only for the two 2-cells.

@[simp]

theorem Schoenflies.HexData.cellSet_vert (H : HexData) (i : Fin 6) : H.cellSet (InitialCell.vert i) = {H.pos i}

@[simp]

theorem Schoenflies.HexData.cellSet_edge (H : HexData) (i : Fin 6) : H.cellSet (InitialCell.edge i) = H.outer i '' unitInterval \ {H.pos i, H.pos (i + 1)}

@[simp]

theorem Schoenflies.HexData.cellSet_chord (H : HexData) : H.cellSet InitialCell.chord = H.chordSet \ {H.pos 1, H.pos 4}

@[simp]

theorem Schoenflies.HexData.cellSet_face (H : HexData) (k : Bool) : H.cellSet (InitialCell.face k) = inside (H.arcOf k ∪ H.chordSet)

theorem Schoenflies.HexData.cellSet_edge_subset (H : HexData) (i : Fin 6) : H.cellSet (InitialCell.edge i) ⊆ H.outer i '' unitInterval

theorem Schoenflies.HexData.cellSet_edge_subset_outerArcs (H : HexData) (i : Fin 6) : H.cellSet (InitialCell.edge i) ⊆ H.outerArcs

theorem Schoenflies.HexData.cellSet_chord_subset (H : HexData) : H.cellSet InitialCell.chord ⊆ H.chordSet

theorem Schoenflies.HexData.pos_mem_outerArcs (H : HexData) (i : Fin 6) : H.pos i ∈ H.outerArcs

theorem Schoenflies.HexData.nonempty_cellSet_edge (H : HexData) (i : Fin 6) : (H.cellSet (InitialCell.edge i)).Nonempty

The 1-cells are nonempty: an arc has more points than its two endpoints.

theorem Schoenflies.HexData.nonempty_cellSet_chord (H : HexData) : (H.cellSet InitialCell.chord).Nonempty

theorem Schoenflies.HexData.closure_cellSet_edge (H : HexData) (i : Fin 6) : closure (H.cellSet (InitialCell.edge i)) = H.outer i '' unitInterval

A closed 1-cell is the drawn edge: an arc is the closure of its interior.

theorem Schoenflies.HexData.closure_cellSet_chord (H : HexData) : closure (H.cellSet InitialCell.chord) = H.chordSet

theorem Schoenflies.HexData.pos_notMem_cellSet_edge (H : HexData) (k i : Fin 6) : H.pos k ∉ H.cellSet (InitialCell.edge i)

A 0-cell never lies on an open 1-cell. A vertex on a drawn outer edge is one of its two ends (HexData.mem_outer_iff), and the open edge is exactly the drawn edge without them.

theorem Schoenflies.HexData.pos_notMem_cellSet_chord (H : HexData) (k : Fin 6) : H.pos k ∉ H.cellSet InitialCell.chord

theorem Schoenflies.HexData.disjoint_cellSet_edge (H : HexData) {i j : Fin 6} (hij : i ≠ j) : Disjoint (H.cellSet (InitialCell.edge i)) (H.cellSet (InitialCell.edge j))

Two distinct open outer 1-cells are disjoint. The two edges meet only at points that are ends of both, and those are removed.

theorem Schoenflies.HexData.disjoint_cellSet_edge_chord (H : HexData) (i : Fin 6) : Disjoint (H.cellSet (InitialCell.edge i)) (H.cellSet InitialCell.chord)

The open crosscut misses every open outer 1-cell.

theorem Schoenflies.HexData.mem_cellSet_edge_or (H : HexData) {i : Fin 6} {z : Plane} (hz : z ∈ H.outer i '' unitInterval) : z ∈ H.cellSet (InitialCell.edge i) ∨ z = H.pos i ∨ z = H.pos (i + 1)

A point of a drawn outer edge is on the open edge or is one of its two ends.

theorem Schoenflies.HexData.mem_cellSet_chord_or (H : HexData) {z : Plane} (hz : z ∈ H.chordSet) : z ∈ H.cellSet InitialCell.chord ∨ z = H.pos 1 ∨ z = H.pos 4

A point of the crosscut is on the open crosscut or is one of its two ends.

theorem Schoenflies.HexData.iUnion_cellSet (H : HexData) : ⋃ (c : InitialCell), H.cellSet c = H.outerArcs ∪ H.chordSet ∪ (H.cellSet (InitialCell.face false) ∪ H.cellSet (InitialCell.face true))

The 0-cells and the open 1-cells reassemble the skeleton C ∪ P.

theorem Schoenflies.HexData.biUnion_of_three_edges (H : HexData) (F : Set InitialCell) {i j l : Fin 6} (hij : i + 1 = j) (hjl : j + 1 = l) (hmem : ∀ c ∈ F, c = InitialCell.vert i ∨ c = InitialCell.vert j ∨ c = InitialCell.vert l ∨ c = InitialCell.vert (l + 1) ∨ c = InitialCell.edge i ∨ c = InitialCell.edge j ∨ c = InitialCell.edge l ∨ c = InitialCell.chord) (hvi : InitialCell.vert i ∈ F) (hvj : InitialCell.vert j ∈ F) (hvl : InitialCell.vert l ∈ F) (hvl1 : InitialCell.vert (l + 1) ∈ F) (hei : InitialCell.edge i ∈ F) (hej : InitialCell.edge j ∈ F) (hel : InitialCell.edge l ∈ F) (hch : InitialCell.chord ∈ F) (hv1 : InitialCell.vert 1 ∈ F) (hv4 : InitialCell.vert 4 ∈ F) : ⋃ c ∈ F, H.cellSet c = H.outer i '' unitInterval ∪ (H.outer j '' unitInterval ∪ H.outer l '' unitInterval) ∪ H.chordSet

Three consecutive outer edges and the crosscut reassemble their union. The two 2-cells of the initial structure differ only in which three outer edges bound them, so the union over the cells of a boundary walk is computed once, for an arbitrary set F of cells presented as the four vertices, the three edges and the crosscut.

theorem Schoenflies.HexData.biUnion_faceCells (H : HexData) (k : Bool) : ⋃ c ∈ faceCells k, H.cellSet c = H.arcOf k ∪ H.chordSet

The cells of a 2-cell's boundary walk reassemble Aₖ ∪ P. The blueprint declares faceCells k to be the subcells of Rₖ; geometrically that union is exactly the boundary curve of Rₖ, which is what closure_eq has to match at a 2-cell.

Assertion (i) and def:admissible-graph, for either realization

Both realizations of prop:initial-pair are a HexData whose six outer arcs form a Jordan curve and whose chord is a crosscut of it. Everything that distinguishes assertion (i) from bookkeeping is thm:general-crosscut, in the packaged form Schoenflies.crosscut_cell_partition: the two 2-cells are open, nonempty, disjoint from each other and from the open crosscut, they exhaust D ∖ P together with it, and the closure of each is itself together with its own boundary curve.

theorem Schoenflies.HexData.isCellDecomposition (H : HexData) (hcross : IsCrosscut H.outerArcs H.chordSet (H.pos 1) (H.pos 4)) (hcut : IsCutPair H.outerArcs (H.pos 1) (H.pos 4) (H.arcOf false) (H.arcOf true)) (hcollars : HasArcCollars (inside H.outerArcs) H.chordSet) : H.realization.IsCellDecomposition (H.outerArcs ∪ inside H.outerArcs)

lem:cellulation-invariants(i) for a realization of the initial structure. The open cells are nonempty and pairwise disjoint, they cover C ∪ D, and every closed cell is the union of its open subcells for the base value of ≼_abs the blueprint fixes.

The three hypotheses are exactly thm:general-crosscut's: the chord is a crosscut of the outer cycle, the two boundary arcs are the two arcs it cuts the outer cycle into, and the crosscut has collars. On the source side they are InitialData.isCrosscut, .isCutPair and .hasArcCollarsSource; on the target side .isCrosscutTarget, .isCutPairTarget and .hasArcCollarsTarget.

theorem Schoenflies.HexData.isOpen_cellSet_face (H : HexData) (hcross : IsCrosscut H.outerArcs H.chordSet (H.pos 1) (H.pos 4)) (hcut : IsCutPair H.outerArcs (H.pos 1) (H.pos 4) (H.arcOf false) (H.arcOf true)) (hcollars : HasArcCollars (inside H.outerArcs) H.chordSet) (k : Bool) : IsOpen (H.cellSet (InitialCell.face k))

The two 2-cells are open. IsCellDecomposition does not record this, but IsCellDecomposition.face_eq — assertion (viii) — takes it as a hypothesis, and thm:general-crosscut hands it to the producer for free. Exported here so that no consumer has to rederive it at stage 0.

theorem Schoenflies.HexData.isFaceJordan (H : HexData) (hcross : IsCrosscut H.outerArcs H.chordSet (H.pos 1) (H.pos 4)) (hcut : IsCutPair H.outerArcs (H.pos 1) (H.pos 4) (H.arcOf false) (H.arcOf true)) : H.realization.IsFaceJordan

Assertion (vii) for the initial hexagonal cellulation. Each of its two faces was defined as the inside of the curve obtained by joining one boundary arc to the crosscut; the crosscut theorem says that curve is Jordan.

theorem Schoenflies.HexData.isWeaklyAdmissible (H : HexData) (hcross : IsCrosscut H.outerArcs H.chordSet (H.pos 1) (H.pos 4)) : H.realization.IsWeaklyAdmissible H.outerArcs (H.outerArcs ∪ inside H.outerArcs)

def:admissible-graph minus the connectedness clause, for a realization of the initial structure. The 2-connectivity is HexData.isTwoConnected_graph; the outer cycle is the union of the six outer arcs by construction; the one nonboundary edge is the crosscut, which is polygonal and has its interior in the open domain because it is a crosscut.

rem:intermediate-disconnection waives connectedness of the open nonboundary part at intermediate stages only. The initial pair does satisfy it — HexData.isConnected_nonboundary — and InitialData.generatedPair_isAdmissible records the strong form.

The closed square, as a domain

GeneratedPair asks for the closed target domain. Schoenflies.inside_modelCurve identifies the Jordan domain of S with the open square, so the closed domain S ∪ Int(S) is literally Q = [-1,1]².

theorem Schoenflies.modelCurve_union_inside : modelCurve ∪ inside modelCurve = Plane.closedSquare 0 1

S ∪ Int(S) = Q.

The initial pair is a GeneratedPair

Both realizations are instances of the two HexData theorems above; all that is left is to present the hypotheses in the shape they take, which on the source side means rewriting d.src.outerArcs to C and on the target side d.tgt.outerArcs to S.

theorem Schoenflies.InitialData.isCrosscut_src {C : Set Plane} (d : InitialData C) : IsCrosscut d.src.outerArcs d.src.chordSet (d.src.pos 1) (d.src.pos 4)

The crosscut configuration on the source side, with the outer cycle named as the HexData sees it.

theorem Schoenflies.InitialData.isCrosscut_tgt {C : Set Plane} (d : InitialData C) : IsCrosscut d.tgt.outerArcs d.tgt.chordSet (d.tgt.pos 1) (d.tgt.pos 4)

The crosscut configuration on the target side.

theorem Schoenflies.InitialData.src_isCellDecomposition {C : Set Plane} (d : InitialData C) : d.sourceRealization.IsCellDecomposition (C ∪ inside C)

Assertion (i) on the source side: the fifteen open cells of Γ decompose C ∪ D.

theorem Schoenflies.InitialData.tgt_isCellDecomposition {C : Set Plane} (d : InitialData C) : d.targetRealization.IsCellDecomposition (Plane.closedSquare 0 1)

Assertion (i) on the target side: the fifteen open cells of Γ' decompose Q.

theorem Schoenflies.InitialData.src_isWeaklyAdmissible {C : Set Plane} (d : InitialData C) : d.sourceRealization.IsWeaklyAdmissible C (C ∪ inside C)

def:admissible-graph (weak form) on the source side.

theorem Schoenflies.InitialData.tgt_isWeaklyAdmissible {C : Set Plane} (d : InitialData C) : d.targetRealization.IsWeaklyAdmissible modelCurve (Plane.closedSquare 0 1)

def:admissible-graph (weak form) on the target side.

theorem Schoenflies.InitialData.isOpen_sourceRealization_cell_face {C : Set Plane} (d : InitialData C) (k : Bool) : IsOpen (d.sourceRealization.cell (InitialCell.face k))

The two source 2-cells are open — the hypothesis IsCellDecomposition.face_eq takes and IsCellDecomposition does not record.

theorem Schoenflies.InitialData.isOpen_targetRealization_cell_face {C : Set Plane} (d : InitialData C) (k : Bool) : IsOpen (d.targetRealization.cell (InitialCell.face k))

The two target 2-cells are open.

noncomputable def Schoenflies.InitialData.generatedPair {C : Set Plane} (d : InitialData C) : GeneratedPair initialStructure C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)

Stage 0 of the Schönflies recursion. The initial matched pair of prop:initial-pair is a generated matched cellulation: it is generated from Schoenflies.initialStructure by the empty sequence of elementary operations (GeneratedStructure.base), its two realizations are the two realizations of prop:initial-pair, and the two cell decompositions are lem:cellulation-invariants(i) on each side.

This is the base case of the whole construction: thm:finite-transfer consumes a GeneratedPair and produces one, and this is the first.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Schoenflies.InitialData.generatedPair_str {C : Set Plane} (d : InitialData C) : d.generatedPair.str = initialStructure

@[simp]

theorem Schoenflies.InitialData.generatedPair_src {C : Set Plane} (d : InitialData C) : d.generatedPair.src = d.sourceRealization

@[simp]

theorem Schoenflies.InitialData.generatedPair_tgt {C : Set Plane} (d : InitialData C) : d.generatedPair.tgt = d.targetRealization

@[simp]

theorem Schoenflies.InitialData.generatedPair_homeo {C : Set Plane} (d : InitialData C) : d.generatedPair.homeo = d.skeletonHomeo

theorem Schoenflies.InitialData.generatedPair_combInvariants {C : Set Plane} (d : InitialData C) : d.generatedPair.str.CombInvariants

The combinatorial invariants at stage 0, read off the bundle: this is what GeneratedPair.combInvariants needs supplied at the base, and what every later stage inherits.

theorem Schoenflies.InitialData.generatedPair_src_isAdmissible {C : Set Plane} (d : InitialData C) : d.generatedPair.src.IsAdmissible C (C ∪ inside C)

The initial pair is admissible in the strong sense, on both sides. rem:intermediate-disconnection waives connectedness of the open nonboundary part at intermediate stages; at stage 0 it holds, the open nonboundary part being the open crosscut.

theorem Schoenflies.InitialData.generatedPair_tgt_isAdmissible {C : Set Plane} (d : InitialData C) : d.generatedPair.tgt.IsAdmissible modelCurve (Plane.closedSquare 0 1)

noncomputable def Schoenflies.AnchoredInitialData.generatedPair {C : Set Plane} {A : AnchorSet C} (D : AnchoredInitialData C A) : GeneratedPair initialStructure C (C ∪ inside C) modelCurve (Plane.closedSquare 0 1)

Stage 0 from the anchored initial pair. AnchoredInitialData adds only the clause a, b ∈ 𝒜, which no field of GeneratedPair mentions; it is what lets a later stage run a fresh crosscut into a or b (AnchoredInitialData.stronglyAccessible_a). So the pair is built from the underlying InitialData, and this is the specialisation for a consumer holding the anchored form.

Equations

• D.generatedPair = D.generatedPair

The base case meets the recursion

Schoenflies.finite_transfer_toward_square and Schoenflies.EarStep carry [Infinite γ], and FiniteTransfer.lean argues that without it EarStep is false: an ear insertion consumes fresh cell names for the ear's interior vertices, its edges and the two 2-cells the split creates, so a naming type that the current stage has exhausted refutes it.

The initial structure names fifteen cells. InitialCell therefore carries a fifth constructor, InitialCell.aux : ℕ → InitialCell, which is the spare supply and nothing else: no aux name is a cell, every aux name has empty open cell, and initSub relates none of them — the reflexive clause of ≼_abs is restricted to Schoenflies.cellNames precisely so that CombInvariants.sub_mem_left and .sub_mem_right, which say that ≼_abs relates cells to cells, stay true.

The alternative was a relabelling of a CellStructure and both of its realizations along an injection InitialCell ↪ γ into an infinite naming type. That is several hundred lines and buys nothing the spare constructor does not, since the base of GeneratedStructure is a parameter and stage 0 uses only the base constructor — no inductive derivation has to be transported.

instance Schoenflies.instInfiniteInitialCell : Infinite InitialCell

theorem Schoenflies.infinite_initialCell : Infinite InitialCell

The naming type of the initial structure is infinite, so the base case really can be fed to thm:finite-transfer, whose [Infinite γ] is not decoration: an ear insertion consumes fresh cell names, and on a finite naming type Schoenflies.EarStep is false. The supply is InitialCell.aux, and no aux name is a cell of initialStructure.

The interface, exercised

A machine-checked statement that stage 0 delivers exactly what thm:finite-transfer reads off a GeneratedPair: the abstract structure carries the combinatorial invariants, the source and target realizations are cell decompositions of the two closed domains, and both are admissible in the strong sense. Nothing below mentions how the pair was built.