Canonical normal-form boundary words

This file gives finite signed-dart presentations for the orientable and nonorientable boundary words encoded by the vendored OrientableRel and NonOrientableRel. It records their exact lengths and edge multiplicities, then packages them as connected, incidence-valid one-face cell complexes.

For Eval-admissible parameters, the words are nonempty and therefore also satisfy SurfaceCellComplex.OccurrencePairingValid. These are combinatorial and polygonal-pairing certificates. Their faithful polygonal realizations are compared with the closed-disc quotients defined in LeanEval/ChallengeDeps.lean by the canonical realization layer.

theorem LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.wordEdgeOccurrences_card_eq_count_edgeName {Edge : Type} [DecidableEq Edge] (word : List (SignedDart Edge)) (e : Edge) : (wordEdgeOccurrences word e).card = List.count e (List.map SignedDart.edgeName word)

Counting boundary positions by edge name agrees with counting the edge names in the word.

inductive LeanEval.Topology.ClassificationOfSurfaces.NormalForm.OrientableEdge (p n : ℕ) : Type

Edge names in the canonical orientable normal-form word.

• a {p n : ℕ} : Fin p → OrientableEdge p n
• b {p n : ℕ} : Fin p → OrientableEdge p n
• c {p n : ℕ} : Fin n → OrientableEdge p n
• h {p n : ℕ} : Fin n → OrientableEdge p n

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.instDecidableEqOrientableEdge.decEq {p✝ n✝ : ℕ} (x✝ x✝¹ : OrientableEdge p✝ n✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.NormalForm.instDecidableEqOrientableEdge {p✝ n✝ : ℕ} : DecidableEq (OrientableEdge p✝ n✝)

Equations

• LeanEval.Topology.ClassificationOfSurfaces.NormalForm.instDecidableEqOrientableEdge = LeanEval.Topology.ClassificationOfSurfaces.NormalForm.instDecidableEqOrientableEdge.decEq

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.NormalForm.instReprOrientableEdge {p✝ n✝ : ℕ} : Repr (OrientableEdge p✝ n✝)

Equations

• LeanEval.Topology.ClassificationOfSurfaces.NormalForm.instReprOrientableEdge = { reprPrec := LeanEval.Topology.ClassificationOfSurfaces.NormalForm.instReprOrientableEdge.repr }

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.instReprOrientableEdge.repr {p✝ n✝ : ℕ} : OrientableEdge p✝ n✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.NormalForm.instFintypeOrientableEdge {p✝ n✝ : ℕ} : Fintype (OrientableEdge p✝ n✝)

Equations

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

inductive LeanEval.Topology.ClassificationOfSurfaces.NormalForm.NonOrientableEdge (p n : ℕ) : Type

Edge names in the canonical nonorientable normal-form word.

• a {p n : ℕ} : Fin p → NonOrientableEdge p n
• c {p n : ℕ} : Fin n → NonOrientableEdge p n
• h {p n : ℕ} : Fin n → NonOrientableEdge p n

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.NormalForm.instDecidableEqNonOrientableEdge {p✝ n✝ : ℕ} : DecidableEq (NonOrientableEdge p✝ n✝)

Equations

• LeanEval.Topology.ClassificationOfSurfaces.NormalForm.instDecidableEqNonOrientableEdge = LeanEval.Topology.ClassificationOfSurfaces.NormalForm.instDecidableEqNonOrientableEdge.decEq

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.instDecidableEqNonOrientableEdge.decEq {p✝ n✝ : ℕ} (x✝ x✝¹ : NonOrientableEdge p✝ n✝) : Decidable (x✝ = x✝¹)

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.instReprNonOrientableEdge.repr {p✝ n✝ : ℕ} : NonOrientableEdge p✝ n✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.NormalForm.instReprNonOrientableEdge {p✝ n✝ : ℕ} : Repr (NonOrientableEdge p✝ n✝)

Equations

• LeanEval.Topology.ClassificationOfSurfaces.NormalForm.instReprNonOrientableEdge = { reprPrec := LeanEval.Topology.ClassificationOfSurfaces.NormalForm.instReprNonOrientableEdge.repr }

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.NormalForm.instFintypeNonOrientableEdge {p✝ n✝ : ℕ} : Fintype (NonOrientableEdge p✝ n✝)

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableHandleBlock {p n : ℕ} (i : Fin p) : List (SurfaceCellComplex.SignedDart (OrientableEdge p n))

The commutator block aᵢ bᵢ aᵢ⁻¹ bᵢ⁻¹.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryBlock {p n : ℕ} (i : Fin n) : List (SurfaceCellComplex.SignedDart (OrientableEdge p n))

The boundary block cᵢ hᵢ cᵢ⁻¹ in the orientable word.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCrosscapBlock {p n : ℕ} (i : Fin p) : List (SurfaceCellComplex.SignedDart (NonOrientableEdge p n))

The square block aᵢ aᵢ in the nonorientable word.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryBlock {p n : ℕ} (i : Fin n) : List (SurfaceCellComplex.SignedDart (NonOrientableEdge p n))

The boundary block cᵢ hᵢ cᵢ⁻¹ in the nonorientable word.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryWord (p n : ℕ) : List (SurfaceCellComplex.SignedDart (OrientableEdge p n))

The canonical orientable signed boundary word.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryWord (p n : ℕ) : List (SurfaceCellComplex.SignedDart (NonOrientableEdge p n))

The canonical nonorientable signed boundary word.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryWord_length (p n : ℕ) : (orientableBoundaryWord p n).length = 4 * p + 3 * n

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryWord_length (p n : ℕ) : (nonOrientableBoundaryWord p n).length = 2 * p + 3 * n

Certified positions in the canonical words

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableHandlePosition (p n : ℕ) (i : Fin p) (k : Fin 4) : Fin (orientableBoundaryWord p n).length

Position k in handle block i inside the full orientable boundary word.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableHandlePosition p n i k = ⟨↑i * 4 + ↑k, ⋯⟩

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryPosition (p n : ℕ) (j : Fin n) (k : Fin 3) : Fin (orientableBoundaryWord p n).length

Position k in boundary block j inside the full orientable boundary word.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryPosition p n j k = ⟨4 * p + ↑j * 3 + ↑k, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableHandlePosition_val (p n : ℕ) (i : Fin p) (k : Fin 4) : ↑(orientableHandlePosition p n i k) = ↑i * 4 + ↑k

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryPosition_val (p n : ℕ) (j : Fin n) (k : Fin 3) : ↑(orientableBoundaryPosition p n j k) = 4 * p + ↑j * 3 + ↑k

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryWord_get_handle_block (p n : ℕ) (i : Fin p) (k : Fin 4) : (orientableBoundaryWord p n).get (orientableHandlePosition p n i k) = (orientableHandleBlock i).get k

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryWord_get_boundary_block (p n : ℕ) (j : Fin n) (k : Fin 3) : (orientableBoundaryWord p n).get (orientableBoundaryPosition p n j k) = (orientableBoundaryBlock j).get k

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryWord_get_handle_a_pos (p n : ℕ) (i : Fin p) : (orientableBoundaryWord p n).get (orientableHandlePosition p n i 0) = SurfaceCellComplex.SignedDart.pos (OrientableEdge.a i)

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryWord_get_handle_b_pos (p n : ℕ) (i : Fin p) : (orientableBoundaryWord p n).get (orientableHandlePosition p n i 1) = SurfaceCellComplex.SignedDart.pos (OrientableEdge.b i)

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryWord_get_handle_a_neg (p n : ℕ) (i : Fin p) : (orientableBoundaryWord p n).get (orientableHandlePosition p n i 2) = SurfaceCellComplex.SignedDart.neg (OrientableEdge.a i)

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryWord_get_handle_b_neg (p n : ℕ) (i : Fin p) : (orientableBoundaryWord p n).get (orientableHandlePosition p n i 3) = SurfaceCellComplex.SignedDart.neg (OrientableEdge.b i)

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryWord_get_boundary_c_pos (p n : ℕ) (j : Fin n) : (orientableBoundaryWord p n).get (orientableBoundaryPosition p n j 0) = SurfaceCellComplex.SignedDart.pos (OrientableEdge.c j)

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryWord_get_boundary_h_pos (p n : ℕ) (j : Fin n) : (orientableBoundaryWord p n).get (orientableBoundaryPosition p n j 1) = SurfaceCellComplex.SignedDart.pos (OrientableEdge.h j)

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryWord_get_boundary_c_neg (p n : ℕ) (j : Fin n) : (orientableBoundaryWord p n).get (orientableBoundaryPosition p n j 2) = SurfaceCellComplex.SignedDart.neg (OrientableEdge.c j)

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCrosscapPosition (p n : ℕ) (i : Fin p) (k : Fin 2) : Fin (nonOrientableBoundaryWord p n).length

Position k in crosscap block i inside the full nonorientable boundary word.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCrosscapPosition p n i k = ⟨↑i * 2 + ↑k, ⋯⟩

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryPosition (p n : ℕ) (j : Fin n) (k : Fin 3) : Fin (nonOrientableBoundaryWord p n).length

Position k in boundary block j inside the full nonorientable boundary word.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryPosition p n j k = ⟨2 * p + ↑j * 3 + ↑k, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCrosscapPosition_val (p n : ℕ) (i : Fin p) (k : Fin 2) : ↑(nonOrientableCrosscapPosition p n i k) = ↑i * 2 + ↑k

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryPosition_val (p n : ℕ) (j : Fin n) (k : Fin 3) : ↑(nonOrientableBoundaryPosition p n j k) = 2 * p + ↑j * 3 + ↑k

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryWord_get_crosscap_block (p n : ℕ) (i : Fin p) (k : Fin 2) : (nonOrientableBoundaryWord p n).get (nonOrientableCrosscapPosition p n i k) = (nonOrientableCrosscapBlock i).get k

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryWord_get_boundary_block (p n : ℕ) (j : Fin n) (k : Fin 3) : (nonOrientableBoundaryWord p n).get (nonOrientableBoundaryPosition p n j k) = (nonOrientableBoundaryBlock j).get k

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryWord_get_crosscap_a_first (p n : ℕ) (i : Fin p) : (nonOrientableBoundaryWord p n).get (nonOrientableCrosscapPosition p n i 0) = SurfaceCellComplex.SignedDart.pos (NonOrientableEdge.a i)

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryWord_get_crosscap_a_second (p n : ℕ) (i : Fin p) : (nonOrientableBoundaryWord p n).get (nonOrientableCrosscapPosition p n i 1) = SurfaceCellComplex.SignedDart.pos (NonOrientableEdge.a i)

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryWord_get_boundary_c_pos (p n : ℕ) (j : Fin n) : (nonOrientableBoundaryWord p n).get (nonOrientableBoundaryPosition p n j 0) = SurfaceCellComplex.SignedDart.pos (NonOrientableEdge.c j)

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryWord_get_boundary_h_pos (p n : ℕ) (j : Fin n) : (nonOrientableBoundaryWord p n).get (nonOrientableBoundaryPosition p n j 1) = SurfaceCellComplex.SignedDart.pos (NonOrientableEdge.h j)

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryWord_get_boundary_c_neg (p n : ℕ) (j : Fin n) : (nonOrientableBoundaryWord p n).get (nonOrientableBoundaryPosition p n j 2) = SurfaceCellComplex.SignedDart.neg (NonOrientableEdge.c j)

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryWord_edge_occurrences (p n : ℕ) (e : OrientableEdge p n) : (SurfaceCellComplex.wordEdgeOccurrences (orientableBoundaryWord p n) e).card = match e with | OrientableEdge.a a => 2 | OrientableEdge.b a => 2 | OrientableEdge.c a => 2 | OrientableEdge.h a => 1

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryWord_edge_occurrences (p n : ℕ) (e : NonOrientableEdge p n) : (SurfaceCellComplex.wordEdgeOccurrences (nonOrientableBoundaryWord p n) e).card = match e with | NonOrientableEdge.a a => 2 | NonOrientableEdge.c a => 2 | NonOrientableEdge.h a => 1

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableCellComplex (p n : ℕ) : SurfaceCellComplex

The one-face incidence presentation carried by the canonical orientable word.

Equations

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

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCellComplex (p n : ℕ) : SurfaceCellComplex

The one-face incidence presentation carried by the canonical nonorientable word.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableCellComplex_boundary (p n : ℕ) : (orientableCellComplex p n).boundary PUnit.unit = orientableBoundaryWord p n

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCellComplex_boundary (p n : ℕ) : (nonOrientableCellComplex p n).boundary PUnit.unit = nonOrientableBoundaryWord p n

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableCellComplex_faceBoundaryLength (p n : ℕ) : (orientableCellComplex p n).faceBoundaryLength PUnit.unit = 4 * p + 3 * n

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCellComplex_faceBoundaryLength (p n : ℕ) : (nonOrientableCellComplex p n).faceBoundaryLength PUnit.unit = 2 * p + 3 * n

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableCellComplex_isConnected (p n : ℕ) : (orientableCellComplex p n).IsConnected

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCellComplex_isConnected (p n : ℕ) : (nonOrientableCellComplex p n).IsConnected

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableCellComplex_isSurfaceValid (p n : ℕ) : (orientableCellComplex p n).IsSurfaceValid

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCellComplex_isSurfaceValid (p n : ℕ) : (nonOrientableCellComplex p n).IsSurfaceValid

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundaryWord_ne_nil {p n : ℕ} (h : 1 ≤ p ∨ 1 ≤ n) : orientableBoundaryWord p n ≠ []

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundaryWord_ne_nil {p n : ℕ} (h : 1 ≤ p) : nonOrientableBoundaryWord p n ≠ []

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableCellComplex_occurrencePairingValid {p n : ℕ} (h : 1 ≤ p ∨ 1 ≤ n) : (orientableCellComplex p n).OccurrencePairingValid

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCellComplex_occurrencePairingValid {p n : ℕ} (h : 1 ≤ p) : (nonOrientableCellComplex p n).OccurrencePairingValid

def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.canonicalCellComplex : NormalForm → SurfaceCellComplex

The canonical incidence presentation attached to a named normal form.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.NormalForm.sphere.canonicalCellComplex = LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.sphere
• (LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientable p n).canonicalCellComplex = LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableCellComplex p n
• (LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientable p n).canonicalCellComplex = LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCellComplex p n

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.canonicalCellComplex_isSurfaceValid (N : NormalForm) : N.canonicalCellComplex.IsSurfaceValid

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.canonicalCellComplex_isConnected (N : NormalForm) : N.canonicalCellComplex.IsConnected