The initial distinguished outer graph is a simple cycle

Reverse finite transfer ultimately needs only the local fact that at most two distinguished outer edges meet at a vertex. Schoenflies.GeneratedStructure.outerEdgesFormCycle propagates the stronger and more natural invariant that the complete outer edge set is one simple cycle. This module supplies its base case for the concrete initial hexagon.

Blueprint

• Schoenflies.outerEdgesFormCycle_initialStructure — the distinguished outer graph of the initial matched cellulation is its six-edge simple cycle.

theorem Schoenflies.initOuter_isLink_edge (i : Fin 6) : initOuter.IsLink (InitialCell.edge i) (InitialCell.vert i) (InitialCell.vert (i + 1))

One oriented side of the initial hexagonal outer graph.

theorem Schoenflies.initOuter_inc_iff {e x : InitialCell} : initOuter.Inc e x ↔ e ∈ InitialCell.outerEdges ∧ (x = e.ends.1 ∨ x = e.ends.2)

Incidence in the initial outer graph is membership among an outer edge's two ends.

theorem Schoenflies.isPath_initOuter_complement : initOuter.IsPath (InitialCell.vert 0) [InitialCell.edge 5, InitialCell.edge 4, InitialCell.edge 3, InitialCell.edge 2, InitialCell.edge 1] (InitialCell.vert 1)

The five-edge complementary path to outer edge zero.

theorem Schoenflies.outerEdgesFormCycle_initialStructure : initialStructure.OuterEdgesFormCycle

The initial distinguished outer edge set is exactly the six-edge hexagonal cycle.