A square model for polygon cells

This file supplies the geometric cut-and-paste model used by Gallier--Xu P2. The closed unit square is treated as a convex disk. Its boundary is parameterized explicitly by radial projection of the Euclidean circle, and an arbitrary homeomorphism from the circle to the frontier of a bounded convex disk is extended across PolygonCell.

def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.maxAbs (z : ℂ) : ℝ

The sup norm of a complex number, used as the gauge of the centered square.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.maxAbs z = max |z.re| |z.im|

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.maxAbs_zero : maxAbs 0 = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.maxAbs_nonneg (z : ℂ) : 0 ≤ maxAbs z

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.abs_re_le_maxAbs (z : ℂ) : |z.re| ≤ maxAbs z

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.abs_im_le_maxAbs (z : ℂ) : |z.im| ≤ maxAbs z

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.maxAbs_eq_zero_iff {z : ℂ} : maxAbs z = 0 ↔ z = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.maxAbs_pos {z : ℂ} (hz : z ≠ 0) : 0 < maxAbs z

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.maxAbs_le_norm (z : ℂ) : maxAbs z ≤ ‖z‖

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.maxAbs_smul_of_nonneg (c : ℝ) (hc : 0 ≤ c) (z : ℂ) : maxAbs (c • z) = c * maxAbs z

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.maxAbs_add_le (z w : ℂ) : maxAbs (z + w) ≤ maxAbs z + maxAbs w

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.maxAbs_div_of_pos (z : ℂ) {r : ℝ} (hr : 0 < r) : maxAbs (z / ↑r) = maxAbs z / r

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.norm_le_sqrtTwo_mul_maxAbs (z : ℂ) : ‖z‖ ≤ √2 * maxAbs z

def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.square : Set ℂ

The centered closed unit square.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.square = {z : ℂ | LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.maxAbs z ≤ 1}

def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.boundary : Set ℂ

The geometric boundary of the centered square.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.boundary = {z : ℂ | LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.maxAbs z = 1}

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.continuous_maxAbs : Continuous maxAbs

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.isClosed_square : IsClosed square

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.zero_mem_square : 0 ∈ square

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.ball_zero_one_subset_square : Metric.ball 0 1 ⊆ square

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.square_mem_nhds_zero : square ∈ nhds 0

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.convex_square : Convex ℝ square

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.isBounded_square : Bornology.IsBounded square

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.interior_square_nonempty : (interior square).Nonempty

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.interior_square : interior square = {z : ℂ | maxAbs z < 1}

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.frontier_square : frontier square = boundary

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.radialToBoundary (z : ℂ) (_hz : z ≠ 0) : ℂ

Radial projection of a nonzero point to the square boundary.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.radialToBoundary z _hz = z / ↑(LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.maxAbs z)

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.radialToBoundary_maxAbs (z : ℂ) (hz : z ≠ 0) : maxAbs (radialToBoundary z hz) = 1

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.circleBoundaryHomeomorph : Circle ≃ₜ ↑boundary

The radial homeomorphism from the Euclidean unit circle to the centered square boundary.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.circleBoundaryHomeomorph_val (z : Circle) : ↑(circleBoundaryHomeomorph z) = radialToBoundary ↑z ⋯

Extending a chosen square-boundary parameterization

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.exists_squareAmbientHomeomorph : ∃ (h : ℂ ≃ₜ ℂ), ⇑h '' square = Metric.closedBall 0 1 ∧ ⇑h '' boundary = Metric.sphere 0 1

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.squareAmbientHomeomorph : ℂ ≃ₜ ℂ

A fixed ambient straightening of the centered square to the Euclidean unit disk.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.squareAmbientHomeomorph = Classical.choose LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.exists_squareAmbientHomeomorph

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.squareAmbientHomeomorph_image_square : ⇑squareAmbientHomeomorph '' square = Metric.closedBall 0 1

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.squareAmbientHomeomorph_image_boundary : ⇑squareAmbientHomeomorph '' boundary = Metric.sphere 0 1

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.squareCellHomeomorph (n : ℕ) : ↑square ≃ₜ PolygonCell n

Restrict the fixed ambient straightening to the closed square.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.boundaryCircleHomeomorph : ↑boundary ≃ₜ Circle

The fixed square straightening restricted to its frontier.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.boundaryInclusion : C(↑boundary, ↑square)

Include the square frontier into the closed square.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.squareCellHomeomorph_boundary (n : ℕ) (z : ↑boundary) : (squareCellHomeomorph n) (boundaryInclusion z) = (PolygonCell.ofCircle n) (boundaryCircleHomeomorph z)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.cellSquareHomeomorph {n : ℕ} (b : Circle ≃ₜ ↑boundary) : PolygonCell n ≃ₜ ↑square

Extend any selected parameterization of the square frontier across a polygon cell.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.cellSquareHomeomorph_ofCircle {n : ℕ} (b : Circle ≃ₜ ↑boundary) (z : Circle) : (cellSquareHomeomorph b) ((PolygonCell.ofCircle n) z) = boundaryInclusion (b z)

The convex extension agrees exactly with the prescribed boundary parameterization.

A distinguished polygon side on the right side of the square

def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalSideWeights (l : ℕ) : List ℕ

Boundary weights for a polygon whose final side is distinguished.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalSideWeights l = List.replicate l 3 ++ [l]

def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstSideWeights (r : ℕ) : List ℕ

Boundary weights for a polygon whose first side is distinguished.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstSideWeights r = r :: List.replicate r 3

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalSideWeights_length (l : ℕ) : (finalSideWeights l).length = l + 1

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstSideWeights_length (r : ℕ) : (firstSideWeights r).length = r + 1

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalSideWeights_sum (l : ℕ) : (finalSideWeights l).sum = 4 * l

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstSideWeights_sum (r : ℕ) : (firstSideWeights r).sum = 4 * r

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalSideWeights_positive {l : ℕ} (hl : 0 < l) : WeightedCircle.Positive (finalSideWeights l)

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstSideWeights_positive {r : ℕ} (hr : 0 < r) : WeightedCircle.Positive (firstSideWeights r)

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalSideWeights_ne_nil {l : ℕ} (_hl : 0 < l) : finalSideWeights l ≠ []

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstSideWeights_ne_nil {r : ℕ} (_hr : 0 < r) : firstSideWeights r ≠ []

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.quarterRotation : Circle ≃ₜ Circle

Rotate the circle counterclockwise by π / 4.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.quarterRotation = Homeomorph.mulLeft (Circle.exp (Real.pi / 4))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalSideBoundaryHomeomorph (l : ℕ) (hl : 0 < l) : Circle ≃ₜ ↑boundary

Put the final side of an (l+1)-gon on the right side of the square.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstSideBoundaryHomeomorph (r : ℕ) (hr : 0 < r) : Circle ≃ₜ ↑boundary

Put the first side of an (r+1)-gon on the same square side, but with reversed traversal.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.abs_sin_le_cos_of_mem_Icc {θ : ℝ} (hθ : θ ∈ Set.Icc (-(Real.pi / 4)) (Real.pi / 4)) : |Real.sin θ| ≤ Real.cos θ

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.radialToBoundary_re_eq_one_of_angle {θ : ℝ} (hθ : θ ∈ Set.Icc (-(Real.pi / 4)) (Real.pi / 4)) : (radialToBoundary ↑(Circle.exp θ) ⋯).re = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalSideWeights_take_last (l : ℕ) : List.take l (finalSideWeights l) = List.replicate l 3

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalSideWeights_get_last (l : ℕ) : (finalSideWeights l).get ⟨l, ⋯⟩ = l

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstSideWeights_get_zero (r : ℕ) : (firstSideWeights r).get ⟨0, ⋯⟩ = r

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalSideWeightedCircle_apply (l : ℕ) (hl : 0 < l) (t : ↑unitInterval) : (WeightedCircle.circleHomeomorph (finalSideWeights l) ⋯ ⋯) (Circle.exp (PolygonCell.sideAngle (Fin.last l) t)) = Circle.exp (2 * Real.pi / (4 * ↑l) * (3 * ↑l + ↑l * ↑t))

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstSideWeightedCircle_apply (r : ℕ) (hr : 0 < r) (t : ↑unitInterval) : (WeightedCircle.circleHomeomorph (firstSideWeights r) ⋯ ⋯) (Circle.exp (PolygonCell.sideAngle 0 t)) = Circle.exp (2 * Real.pi / (4 * ↑r) * (↑r * ↑t))

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalSideBoundaryHomeomorph_apply (l : ℕ) (hl : 0 < l) (t : ↑unitInterval) : (finalSideBoundaryHomeomorph l hl) (Circle.exp (PolygonCell.sideAngle (Fin.last l) t)) = circleBoundaryHomeomorph (Circle.exp (-(Real.pi / 4) + Real.pi / 2 * ↑t))

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstSideBoundaryHomeomorph_apply (r : ℕ) (hr : 0 < r) (t : ↑unitInterval) : (firstSideBoundaryHomeomorph r hr) (Circle.exp (PolygonCell.sideAngle 0 t)) = circleBoundaryHomeomorph (Circle.exp (Real.pi / 4 - Real.pi / 2 * ↑t))

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalSide_eq_firstSide_symm (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (t : ↑unitInterval) : (finalSideBoundaryHomeomorph l hl) (Circle.exp (PolygonCell.sideAngle (Fin.last l) t)) = (firstSideBoundaryHomeomorph r hr) (Circle.exp (PolygonCell.sideAngle 0 (unitInterval.symm t)))

The two fresh sides have exactly the same point of the local square after reversing the right-child parameter.

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalSideBoundaryHomeomorph_re (l : ℕ) (hl : 0 < l) (t : ↑unitInterval) : (↑((finalSideBoundaryHomeomorph l hl) (Circle.exp (PolygonCell.sideAngle (Fin.last l) t)))).re = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstSideBoundaryHomeomorph_re (r : ℕ) (hr : 0 < r) (t : ↑unitInterval) : (↑((firstSideBoundaryHomeomorph r hr) (Circle.exp (PolygonCell.sideAngle 0 t)))).re = 1

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalSideCellHomeomorph (l : ℕ) (hl : 0 < l) : PolygonCell (l + 1) ≃ₜ ↑square

Square model for the selected child of a nondegenerate P2 split.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstSideCellHomeomorph (r : ℕ) (hr : 0 < r) : PolygonCell (r + 1) ≃ₜ ↑square

Square model for the right child of a nondegenerate P2 split.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalSideCellHomeomorph_side (l : ℕ) (hl : 0 < l) (t : ↑unitInterval) : (finalSideCellHomeomorph l hl) ((PolygonCell.side (Fin.last l)) t) = boundaryInclusion ((finalSideBoundaryHomeomorph l hl) (Circle.exp (PolygonCell.sideAngle (Fin.last l) t)))

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstSideCellHomeomorph_side (r : ℕ) (hr : 0 < r) (t : ↑unitInterval) : (firstSideCellHomeomorph r hr) ((PolygonCell.side 0) t) = boundaryInclusion ((firstSideBoundaryHomeomorph r hr) (Circle.exp (PolygonCell.sideAngle 0 t)))

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalSideCell_eq_firstSideCell_symm (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (t : ↑unitInterval) : ↑((finalSideCellHomeomorph l hl) ((PolygonCell.side (Fin.last l)) t)) = ↑((firstSideCellHomeomorph r hr) ((PolygonCell.side 0) (unitInterval.symm t)))

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalSideCellHomeomorph_side_re (l : ℕ) (hl : 0 < l) (t : ↑unitInterval) : (↑((finalSideCellHomeomorph l hl) ((PolygonCell.side (Fin.last l)) t))).re = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstSideCellHomeomorph_side_re (r : ℕ) (hr : 0 < r) (t : ↑unitInterval) : (↑((firstSideCellHomeomorph r hr) ((PolygonCell.side 0) t))).re = 1

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalSideBoundaryHomeomorph_zero_im (l : ℕ) (hl : 0 < l) : (↑((finalSideBoundaryHomeomorph l hl) (Circle.exp (PolygonCell.sideAngle (Fin.last l) 0)))).im = -1

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalSideBoundaryHomeomorph_one_im (l : ℕ) (hl : 0 < l) : (↑((finalSideBoundaryHomeomorph l hl) (Circle.exp (PolygonCell.sideAngle (Fin.last l) 1)))).im = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.exists_finalSideCellHomeomorph_side_of_re_eq_one (l : ℕ) (hl : 0 < l) (z : ↑square) (hz : (↑z).re = 1) : ∃ (t : ↑unitInterval), (finalSideCellHomeomorph l hl) ((PolygonCell.side (Fin.last l)) t) = z

The distinguished final side covers every point of the local square's right edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.exists_firstSideCellHomeomorph_side_of_re_eq_one (r : ℕ) (hr : 0 < r) (z : ↑square) (hz : (↑z).re = 1) : ∃ (t : ↑unitInterval), (firstSideCellHomeomorph r hr) ((PolygonCell.side 0) t) = z

The distinguished first side covers every point of the local square's right edge.

Gluing two square models along their right sides

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.leftPlacement : C(↑square, ↑square)

Place a local square as the left half of the outer square.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.rightPlacement : C(↑square, ↑square)

Place a local square, reflected horizontally, as the right half of the outer square.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.leftPlacement_re (z : ↑square) : (↑(leftPlacement z)).re = ((↑z).re - 1) / 2

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.leftPlacement_im (z : ↑square) : (↑(leftPlacement z)).im = (↑z).im

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.rightPlacement_re (z : ↑square) : (↑(rightPlacement z)).re = (1 - (↑z).re) / 2

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.rightPlacement_im (z : ↑square) : (↑(rightPlacement z)).im = (↑z).im

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.leftPlacement_injective : Function.Injective ⇑leftPlacement

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.rightPlacement_injective : Function.Injective ⇑rightPlacement

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.leftPlacement_re_nonpos (z : ↑square) : (↑(leftPlacement z)).re ≤ 0

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.rightPlacement_re_nonneg (z : ↑square) : 0 ≤ (↑(rightPlacement z)).re

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.leftPlacement_eq_rightPlacement_of_re_eq_one (z w : ↑square) (hreZ : (↑z).re = 1) (hreW : (↑w).re = 1) (him : (↑z).im = (↑w).im) : leftPlacement z = rightPlacement w

The two placements agree on their common local right side.

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.exists_leftPlacement_of_re_nonpos (z : ↑square) (hz : (↑z).re ≤ 0) : ∃ (w : ↑square), leftPlacement w = z

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.exists_rightPlacement_of_re_nonneg (z : ↑square) (hz : 0 ≤ (↑z).re) : ∃ (w : ↑square), rightPlacement w = z

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.leftPlacement_or_rightPlacement (z : ↑square) : (∃ (w : ↑square), leftPlacement w = z) ∨ ∃ (w : ↑square), rightPlacement w = z

Gluing two square disks along their distinguished sides

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.SquarePair : Type

The disjoint union of the two local square disks.

Equations

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

inductive LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.SeamGenerator : SquarePair → SquarePair → Prop

The generating seam relation: the right side of the left local square is glued, point for point, to the right side of the horizontally reflected right local square.

• glue (z w : ↑square) (hz : (↑z).re = 1) (hw : (↑w).re = 1) (him : (↑z).im = (↑w).im) : SeamGenerator (Sum.inl z) (Sum.inr w)

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.seamSetoid : Setoid SquarePair

The equivalence relation generated by the common side of the two square disks.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.seamSetoid = Relation.EqvGen.setoid LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.SeamGenerator

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.SquareGluing : Type

The topological quotient obtained by gluing the two local square disks along the seam.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.SquareGluing = Quotient LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.seamSetoid

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.squarePairMerge : SquarePair → ↑square

Merge the two local squares into the left and right halves of one outer square.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.continuous_squarePairMerge : Continuous squarePairMerge

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.squarePairMerge_eq_of_seamGenerator {x y : SquarePair} (hxy : SeamGenerator x y) : squarePairMerge x = squarePairMerge y

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.squarePairMerge_respects {x y : SquarePair} (hxy : Relation.EqvGen SeamGenerator x y) : squarePairMerge x = squarePairMerge y

The merge map is constant on the equivalence closure of the seam relation.

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.square_re_le_one (z : ↑square) : (↑z).re ≤ 1

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.squarePairMerge_eqvGen_inl_inr (z w : ↑square) (hzw : squarePairMerge (Sum.inl z) = squarePairMerge (Sum.inr w)) : Relation.EqvGen SeamGenerator (Sum.inl z) (Sum.inr w)

Equality between opposite merged summands can only occur on the declared seam.

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.squarePairMerge_eqvGen_of_eq {x y : SquarePair} (hxy : squarePairMerge x = squarePairMerge y) : Relation.EqvGen SeamGenerator x y

No identifications are hidden by the planar merge: equality after merging is exactly generated by equality inside one summand and the declared seam relation.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.squareGluingMap : C(SquareGluing, ↑square)

The continuous map induced on the quotient by merging the two local squares.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.squareGluingMap_mk (x : SquarePair) : squareGluingMap (Quotient.mk'' x) = squarePairMerge x

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.squareGluingMap_injective : Function.Injective ⇑squareGluingMap

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.squareGluingMap_surjective : Function.Surjective ⇑squareGluingMap

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.isCompact_square : IsCompact square

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.squareGluingHomeomorph : SquareGluing ≃ₜ ↑square

Gluing two square disks along the selected sides is again a closed disk.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.squareGluingHomeomorph = LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.squareGluingHomeomorph._proof_4.homeoOfEquivCompactToT2

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.squareGluingHomeomorph_apply (q : SquareGluing) : squareGluingHomeomorph q = squareGluingMap q

Transporting the seam model to two nondegenerate polygon cells

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.ChildPair (l r : ℕ) : Type

The two polygon cells occurring in a nondegenerate, positively oriented P2 split.

Equations

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

inductive LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.ChildSeamGenerator (l r : ℕ) (hl : 0 < l) (hr : 0 < r) : ChildPair l r → ChildPair l r → Prop

The geometric seam relation on the two child cells, expressed through their square models. This formulation records the entire common edge and is convenient for quotient-kernel arguments.

• glue {l r : ℕ} {hl : 0 < l} {hr : 0 < r} (z : PolygonCell (l + 1)) (w : PolygonCell (r + 1)) (hz : (↑((finalSideCellHomeomorph l hl) z)).re = 1) (hw : (↑((firstSideCellHomeomorph r hr) w)).re = 1) (him : (↑((finalSideCellHomeomorph l hl) z)).im = (↑((firstSideCellHomeomorph r hr) w)).im) : ChildSeamGenerator l r hl hr (Sum.inl z) (Sum.inr w)

The equivalence relation generated by identifying the two child-cell seam edges.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.childSeamSetoid (l r : ℕ) (hl : 0 < l) (hr : 0 < r) : Setoid (ChildPair l r)

The setoid generated by identifying the two child-cell seam edges.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.childSeamSetoid l r hl hr = Relation.EqvGen.setoid (LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.ChildSeamGenerator l r hl hr)

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.ChildGluing (l r : ℕ) (hl : 0 < l) (hr : 0 < r) : Type

The quotient of the two child polygon cells by their complete common side.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.ChildGluing l r hl hr = Quotient (LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.childSeamSetoid l r hl hr)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.childPairSquarePairHomeomorph (l r : ℕ) (hl : 0 < l) (hr : 0 < r) : ChildPair l r ≃ₜ SquarePair

Straighten both P2 child cells simultaneously to their local square models.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.childPairSquarePairHomeomorph_inl (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (z : PolygonCell (l + 1)) : (childPairSquarePairHomeomorph l r hl hr) (Sum.inl z) = Sum.inl ((finalSideCellHomeomorph l hl) z)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.childPairSquarePairHomeomorph_inr (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (z : PolygonCell (r + 1)) : (childPairSquarePairHomeomorph l r hl hr) (Sum.inr z) = Sum.inr ((firstSideCellHomeomorph r hr) z)

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.childSeamGenerator_map (l r : ℕ) (hl : 0 < l) (hr : 0 < r) {x y : ChildPair l r} (hxy : ChildSeamGenerator l r hl hr x y) : SeamGenerator ((childPairSquarePairHomeomorph l r hl hr) x) ((childPairSquarePairHomeomorph l r hl hr) y)

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.childSeamGenerator_comap (l r : ℕ) (hl : 0 < l) (hr : 0 < r) {x y : ChildPair l r} (hxy : SeamGenerator ((childPairSquarePairHomeomorph l r hl hr) x) ((childPairSquarePairHomeomorph l r hl hr) y)) : ChildSeamGenerator l r hl hr x y

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.childSeam_eqvGen_iff (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (x y : ChildPair l r) : Relation.EqvGen (ChildSeamGenerator l r hl hr) x y ↔ Relation.EqvGen SeamGenerator ((childPairSquarePairHomeomorph l r hl hr) x) ((childPairSquarePairHomeomorph l r hl hr) y)

The simultaneous child straightening identifies exactly the two generated seam relations.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.childGluingHomeomorph (l r : ℕ) (hl : 0 < l) (hr : 0 < r) : ChildGluing l r hl hr ≃ₜ ↑square

The actual two-child polygon quotient of a nondegenerate P2 cut is a closed disk.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.PolygonCell.side_injective_of_two_le {n : ℕ} (hn : 2 ≤ n) (i : Fin n) : Function.Injective ⇑(PolygonCell.side i)

A marked side of a polygon with at least two sides has no parameter self-overlap.

inductive LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.ParamChildSeamGenerator (l r : ℕ) : ChildPair l r → ChildPair l r → Prop

The parameter-level fresh-edge identification used by a positive P2 split.

• glue {l r : ℕ} (t : ↑unitInterval) : ParamChildSeamGenerator l r (Sum.inl ((PolygonCell.side (Fin.last l)) t)) (Sum.inr ((PolygonCell.side 0) (unitInterval.symm t)))

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.paramChildSeamGenerator_to_childSeam (l r : ℕ) (hl : 0 < l) (hr : 0 < r) {x y : ChildPair l r} (hxy : ParamChildSeamGenerator l r x y) : ChildSeamGenerator l r hl hr x y

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.childSeamGenerator_to_paramEqvGen (l r : ℕ) (hl : 0 < l) (hr : 0 < r) {x y : ChildPair l r} (hxy : ChildSeamGenerator l r hl hr x y) : Relation.EqvGen (ParamChildSeamGenerator l r) x y

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.paramChildSeam_eqvGen_iff (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (x y : ChildPair l r) : Relation.EqvGen (ParamChildSeamGenerator l r) x y ↔ Relation.EqvGen (ChildSeamGenerator l r hl hr) x y

The square-model seam is exactly the equivalence closure of the fresh-side parameter map.

The parameter-independent seam equivalence relation used by the quotient comparison.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.paramChildSeamSetoid (l r : ℕ) : Setoid (ChildPair l r)

The setoid used by the parameter-independent quotient comparison.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.paramChildSeamSetoid l r = Relation.EqvGen.setoid (LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.ParamChildSeamGenerator l r)

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.ParamChildGluing (l r : ℕ) : Type

The quotient of the parameterized child pair by its seam relation.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.ParamChildGluing l r = Quotient (LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.paramChildSeamSetoid l r)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.paramChildGluingHomeomorph (l r : ℕ) (hl : 0 < l) (hr : 0 < r) : ParamChildGluing l r ≃ₜ ↑square

Two nondegenerate P2 child polygons, glued by the precise reversed fresh-edge parameter, form a closed disk.

Equations

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

The external boundary arcs of the glued child disk

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalOldArcLocal (l : ℕ) (hl : 0 < l) : C(↑(Set.Icc 0 ↑l), ↑square)

The old-boundary arc of the selected child, before placing its square on the left.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstOldArcLocal (r : ℕ) (hr : 0 < r) : C(↑(Set.Icc 0 ↑r), ↑square)

The old-boundary arc of the right child, before its horizontal reflection.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalOldArcLocal_apply (l : ℕ) (hl : 0 < l) (s : ↑(Set.Icc 0 ↑l)) : (finalOldArcLocal l hl) s = (finalSideCellHomeomorph l hl) ((PolygonCell.ofCircle (l + 1)) (Circle.exp (2 * Real.pi * ↑s / (↑l + 1))))

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstOldArcLocal_apply (r : ℕ) (hr : 0 < r) (s : ↑(Set.Icc 0 ↑r)) : (firstOldArcLocal r hr) s = (firstSideCellHomeomorph r hr) ((PolygonCell.ofCircle (r + 1)) (Circle.exp (2 * Real.pi * (1 + ↑s) / (↑r + 1))))

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalOldArcLocal_re_eq_one_iff_endpoint (l : ℕ) (hl : 0 < l) (s : ↑(Set.Icc 0 ↑l)) : (↑((finalOldArcLocal l hl) s)).re = 1 ↔ ↑s = 0 ∨ ↑s = ↑l

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalOldArcLocal_zero_im (l : ℕ) (hl : 0 < l) : (↑((finalOldArcLocal l hl) ⟨0, ⋯⟩)).im = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalOldArcLocal_last_im (l : ℕ) (hl : 0 < l) : (↑((finalOldArcLocal l hl) ⟨↑l, ⋯⟩)).im = -1

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalOldArcLocal_abs_im_eq_one_of_re_eq_one (l : ℕ) (hl : 0 < l) (s : ↑(Set.Icc 0 ↑l)) (hs : (↑((finalOldArcLocal l hl) s)).re = 1) : |(↑((finalOldArcLocal l hl) s)).im| = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstOldArcLocal_re_eq_one_iff_endpoint (r : ℕ) (hr : 0 < r) (s : ↑(Set.Icc 0 ↑r)) : (↑((firstOldArcLocal r hr) s)).re = 1 ↔ ↑s = 0 ∨ ↑s = ↑r

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstOldArcLocal_zero_im (r : ℕ) (hr : 0 < r) : (↑((firstOldArcLocal r hr) ⟨0, ⋯⟩)).im = -1

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstOldArcLocal_last_im (r : ℕ) (hr : 0 < r) : (↑((firstOldArcLocal r hr) ⟨↑r, ⋯⟩)).im = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstOldArcLocal_abs_im_eq_one_of_re_eq_one (r : ℕ) (hr : 0 < r) (s : ↑(Set.Icc 0 ↑r)) (hs : (↑((firstOldArcLocal r hr) s)).re = 1) : |(↑((firstOldArcLocal r hr) s)).im| = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalOldArcLocal_mem_boundary (l : ℕ) (hl : 0 < l) (s : ↑(Set.Icc 0 ↑l)) : ↑((finalOldArcLocal l hl) s) ∈ boundary

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstOldArcLocal_mem_boundary (r : ℕ) (hr : 0 < r) (s : ↑(Set.Icc 0 ↑r)) : ↑((firstOldArcLocal r hr) s) ∈ boundary

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.leftPlacement_mem_boundary_of_mem_boundary (z : ↑square) (hz : ↑z ∈ boundary) (hseam : (↑z).re = 1 → |(↑z).im| = 1) : ↑(leftPlacement z) ∈ boundary

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.rightPlacement_mem_boundary_of_mem_boundary (z : ↑square) (hz : ↑z ∈ boundary) (hseam : (↑z).re = 1 → |(↑z).im| = 1) : ↑(rightPlacement z) ∈ boundary

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalOldArc (l : ℕ) (hl : 0 < l) : C(↑(Set.Icc 0 ↑l), ↑boundary)

The selected child's old boundary, placed on the outer square frontier.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstOldArc (r : ℕ) (hr : 0 < r) : C(↑(Set.Icc 0 ↑r), ↑boundary)

The right child's old boundary, reflected and placed on the outer square frontier.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalOldArc_val (l : ℕ) (hl : 0 < l) (s : ↑(Set.Icc 0 ↑l)) : ↑((finalOldArc l hl) s) = ↑(leftPlacement ((finalOldArcLocal l hl) s))

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstOldArc_val (r : ℕ) (hr : 0 < r) (s : ↑(Set.Icc 0 ↑r)) : ↑((firstOldArc r hr) s) = ↑(rightPlacement ((firstOldArcLocal r hr) s))

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalOldArc_zero_re (l : ℕ) (hl : 0 < l) : (↑((finalOldArc l hl) ⟨0, ⋯⟩)).re = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalOldArc_zero_im (l : ℕ) (hl : 0 < l) : (↑((finalOldArc l hl) ⟨0, ⋯⟩)).im = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalOldArc_last_re (l : ℕ) (hl : 0 < l) : (↑((finalOldArc l hl) ⟨↑l, ⋯⟩)).re = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalOldArc_last_im (l : ℕ) (hl : 0 < l) : (↑((finalOldArc l hl) ⟨↑l, ⋯⟩)).im = -1

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstOldArc_zero_re (r : ℕ) (hr : 0 < r) : (↑((firstOldArc r hr) ⟨0, ⋯⟩)).re = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstOldArc_zero_im (r : ℕ) (hr : 0 < r) : (↑((firstOldArc r hr) ⟨0, ⋯⟩)).im = -1

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstOldArc_last_re (r : ℕ) (hr : 0 < r) : (↑((firstOldArc r hr) ⟨↑r, ⋯⟩)).re = 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstOldArc_last_im (r : ℕ) (hr : 0 < r) : (↑((firstOldArc r hr) ⟨↑r, ⋯⟩)).im = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalOldArc_re_nonpos (l : ℕ) (hl : 0 < l) (s : ↑(Set.Icc 0 ↑l)) : (↑((finalOldArc l hl) s)).re ≤ 0

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstOldArc_re_nonneg (r : ℕ) (hr : 0 < r) (s : ↑(Set.Icc 0 ↑r)) : 0 ≤ (↑((firstOldArc r hr) s)).re

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalOldArc_re_eq_zero_iff_endpoint (l : ℕ) (hl : 0 < l) (s : ↑(Set.Icc 0 ↑l)) : (↑((finalOldArc l hl) s)).re = 0 ↔ ↑s = 0 ∨ ↑s = ↑l

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstOldArc_re_eq_zero_iff_endpoint (r : ℕ) (hr : 0 < r) (s : ↑(Set.Icc 0 ↑r)) : (↑((firstOldArc r hr) s)).re = 0 ↔ ↑s = 0 ∨ ↑s = ↑r

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalOldArc_injective (l : ℕ) (hl : 0 < l) : Function.Injective ⇑(finalOldArc l hl)

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstOldArc_injective (r : ℕ) (hr : 0 < r) : Function.Injective ⇑(firstOldArc r hr)

The outer boundary assembled from the two old-boundary arcs

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.leftPerimeter (z : ↑boundary) : ℝ

A continuous coordinate, from 0 to 3, along the left half of the square boundary. It starts at the midpoint of the top edge, passes the two left corners, and ends at the midpoint of the bottom edge.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.leftPerimeter z = -(↑z).re + (1 - (↑z).im) / 2 + (1 - (↑z).im) * (1 + (↑z).re)

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.continuous_leftPerimeter : Continuous leftPerimeter

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.boundary_left_cases (z : ↑boundary) (hz : (↑z).re ≤ 0) : (↑z).re = -1 ∨ (↑z).im = 1 ∨ (↑z).im = -1

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.boundary_right_cases (z : ↑boundary) (hz : 0 ≤ (↑z).re) : (↑z).re = 1 ∨ (↑z).im = 1 ∨ (↑z).im = -1

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.leftPerimeter_mem_Icc (z : ↑boundary) (hz : (↑z).re ≤ 0) : leftPerimeter z ∈ Set.Icc 0 3

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.leftPerimeter_injective {z w : ↑boundary} (hz : (↑z).re ≤ 0) (hw : (↑w).re ≤ 0) (hzw : leftPerimeter z = leftPerimeter w) : z = w

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.rightPerimeter (z : ↑boundary) : ℝ

The analogous coordinate on the right half, oriented from bottom to top.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.rightPerimeter z = LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.leftPerimeter ⟨-↑z, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.continuous_rightPerimeter : Continuous rightPerimeter

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.rightPerimeter_mem_Icc (z : ↑boundary) (hz : 0 ≤ (↑z).re) : rightPerimeter z ∈ Set.Icc 0 3

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.rightPerimeter_injective {z w : ↑boundary} (hz : 0 ≤ (↑z).re) (hw : 0 ≤ (↑w).re) (hzw : rightPerimeter z = rightPerimeter w) : z = w

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.leftPerimeter_finalOldArc_zero (l : ℕ) (hl : 0 < l) : leftPerimeter ((finalOldArc l hl) ⟨0, ⋯⟩) = 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.leftPerimeter_finalOldArc_last (l : ℕ) (hl : 0 < l) : leftPerimeter ((finalOldArc l hl) ⟨↑l, ⋯⟩) = 3

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.rightPerimeter_firstOldArc_zero (r : ℕ) (hr : 0 < r) : rightPerimeter ((firstOldArc r hr) ⟨0, ⋯⟩) = 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.rightPerimeter_firstOldArc_last (r : ℕ) (hr : 0 < r) : rightPerimeter ((firstOldArc r hr) ⟨↑r, ⋯⟩) = 3

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.exists_finalOldArc_of_re_nonpos (l : ℕ) (hl : 0 < l) (z : ↑boundary) (hz : (↑z).re ≤ 0) : ∃ (s : ↑(Set.Icc 0 ↑l)), (finalOldArc l hl) s = z

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.exists_firstOldArc_of_re_nonneg (r : ℕ) (hr : 0 < r) (z : ↑boundary) (hz : 0 ≤ (↑z).re) : ∃ (s : ↑(Set.Icc 0 ↑r)), (firstOldArc r hr) s = z

def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalArcParameter (l r : ℕ) : ↑(Set.Icc 0 (↑l + ↑r)) → ↑(Set.Icc 0 ↑l)

Clip a parameter for the combined outer boundary to the left child's old arc.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalArcParameter l r x = ⟨min ↑x ↑l, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.continuous_finalArcParameter (l r : ℕ) : Continuous (finalArcParameter l r)

def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstArcParameter (l r : ℕ) : ↑(Set.Icc 0 (↑l + ↑r)) → ↑(Set.Icc 0 ↑r)

Clip and translate a combined parameter to the right child's old arc.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.firstArcParameter l r x = ⟨max (↑x - ↑l) 0, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.continuous_firstArcParameter (l r : ℕ) : Continuous (firstArcParameter l r)

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.finalOldArc_last_eq_firstOldArc_zero (l r : ℕ) (hl : 0 < l) (hr : 0 < r) : (finalOldArc l hl) ⟨↑l, ⋯⟩ = (firstOldArc r hr) ⟨0, ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerArc (l r : ℕ) (hl : 0 < l) (hr : 0 < r) : C(↑(Set.Icc 0 (↑l + ↑r)), ↑boundary)

The full outer boundary path: the selected child's old sides followed by the right child's old sides. Its two endpoints both map to the top midpoint.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerArc_apply_of_le (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (x : ↑(Set.Icc 0 (↑l + ↑r))) (hx : ↑x ≤ ↑l) : (outerArc l r hl hr) x = (finalOldArc l hl) ⟨↑x, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerArc_apply_of_not_le (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (x : ↑(Set.Icc 0 (↑l + ↑r))) (hx : ¬↑x ≤ ↑l) : (outerArc l r hl hr) x = (firstOldArc r hr) ⟨↑x - ↑l, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerArc_zero (l r : ℕ) (hl : 0 < l) (hr : 0 < r) : (outerArc l r hl hr) ⟨0, ⋯⟩ = (finalOldArc l hl) ⟨0, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerArc_split (l r : ℕ) (hl : 0 < l) (hr : 0 < r) : (outerArc l r hl hr) ⟨↑l, ⋯⟩ = (finalOldArc l hl) ⟨↑l, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerArc_last (l r : ℕ) (hl : 0 < l) (hr : 0 < r) : (outerArc l r hl hr) ⟨↑l + ↑r, ⋯⟩ = (firstOldArc r hr) ⟨↑r, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerArc_endpoints (l r : ℕ) (hl : 0 < l) (hr : 0 < r) : (outerArc l r hl hr) ⟨0, ⋯⟩ = (outerArc l r hl hr) ⟨↑l + ↑r, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerArc_surjective (l r : ℕ) (hl : 0 < l) (hr : 0 < r) : Function.Surjective ⇑(outerArc l r hl hr)

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerArc_cross_endpoints (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (x y : ↑(Set.Icc 0 (↑l + ↑r))) (hx : ↑x ≤ ↑l) (hy : ¬↑y ≤ ↑l) (hxy : (outerArc l r hl hr) x = (outerArc l r hl hr) y) : ↑x = 0 ∧ ↑y = ↑l + ↑r

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerArc_eq_imp_endpointIdent (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (x y : ↑(Set.Icc 0 (↑l + ↑r))) (hxy : (outerArc l r hl hr) x = (outerArc l r hl hr) y) : x = y ∨ ↑x = 0 ∧ ↑y = ↑l + ↑r ∨ ↑x = ↑l + ↑r ∧ ↑y = 0

def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerEndpointParameter (l r : ℕ) : C(↑(Set.Icc 0 (0 + (↑l + ↑r))), ↑(Set.Icc 0 (↑l + ↑r)))

Remove the syntactic leading zero from the endpoint interval used by AddCircle.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerEndpointParameter l r = { toFun := fun (x : ↑(Set.Icc 0 (0 + (↑l + ↑r)))) => ⟨↑x, ⋯⟩, continuous_toFun := ⋯ }

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerEndpointArc (l r : ℕ) (hl : 0 < l) (hr : 0 < r) : C(↑(Set.Icc 0 (0 + (↑l + ↑r))), ↑boundary)

The outer path with the syntactic endpoint interval used by AddCircle.EndpointIdent.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerEndpointArc_apply (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (x : ↑(Set.Icc 0 (0 + (↑l + ↑r)))) : (outerEndpointArc l r hl hr) x = (outerArc l r hl hr) ⟨↑x, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerArc_endpointIdent (l r : ℕ) (hl : 0 < l) (hr : 0 < r) [Fact (0 < ↑l + ↑r)] (x y : ↑(Set.Icc 0 (0 + (↑l + ↑r)))) (hxy : AddCircle.EndpointIdent (↑l + ↑r) 0 x y) : (outerEndpointArc l r hl hr) x = (outerEndpointArc l r hl hr) y

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerBoundaryQuotMap (l r : ℕ) (hl : 0 < l) (hr : 0 < r) [Fact (0 < ↑l + ↑r)] : C(Quot (AddCircle.EndpointIdent (↑l + ↑r) 0), ↑boundary)

The pasted outer path after identifying its top endpoints.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerBoundaryQuotMap_mk (l r : ℕ) (hl : 0 < l) (hr : 0 < r) [Fact (0 < ↑l + ↑r)] (x : ↑(Set.Icc 0 (0 + (↑l + ↑r)))) : (outerBoundaryQuotMap l r hl hr) (Quot.mk (AddCircle.EndpointIdent (↑l + ↑r) 0) x) = (outerEndpointArc l r hl hr) x

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerBoundaryQuotMap_surjective (l r : ℕ) (hl : 0 < l) (hr : 0 < r) [Fact (0 < ↑l + ↑r)] : Function.Surjective ⇑(outerBoundaryQuotMap l r hl hr)

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerBoundaryQuotMap_injective (l r : ℕ) (hl : 0 < l) (hr : 0 < r) [Fact (0 < ↑l + ↑r)] : Function.Injective ⇑(outerBoundaryQuotMap l r hl hr)

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerBoundaryQuotMap_bijective (l r : ℕ) (hl : 0 < l) (hr : 0 < r) [Fact (0 < ↑l + ↑r)] : Function.Bijective ⇑(outerBoundaryQuotMap l r hl hr)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerBoundaryQuotHomeomorph (l r : ℕ) (hl : 0 < l) (hr : 0 < r) [Fact (0 < ↑l + ↑r)] : Quot (AddCircle.EndpointIdent (↑l + ↑r) 0) ≃ₜ ↑boundary

The endpoint quotient of the pasted old-boundary path is exactly the square boundary.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerBoundaryQuotHomeomorph l r hl hr = ⋯.homeoOfEquivCompactToT2

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerBoundaryQuotHomeomorph_mk (l r : ℕ) (hl : 0 < l) (hr : 0 < r) [Fact (0 < ↑l + ↑r)] (x : ↑(Set.Icc 0 (0 + (↑l + ↑r)))) : (outerBoundaryQuotHomeomorph l r hl hr) (Quot.mk (AddCircle.EndpointIdent (↑l + ↑r) 0) x) = (outerEndpointArc l r hl hr) x

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerAddCircleHomeomorph (l r : ℕ) (hl : 0 < l) (hr : 0 < r) : AddCircle (↑l + ↑r) ≃ₜ ↑boundary

The additive circle parameterized by the old sides is the outer square boundary.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerBoundaryHomeomorph (l r : ℕ) (hl : 0 < l) (hr : 0 < r) : Circle ≃ₜ ↑boundary

The exact boundary parameterization used to extend the old sides across the selected source polygon.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerAddCircleHomeomorph_apply_of_mem_Ico (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (x : ℝ) (hx : x ∈ Set.Ico 0 (↑l + ↑r)) : (outerAddCircleHomeomorph l r hl hr) ↑x = (outerArc l r hl hr) ⟨x, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerBoundaryHomeomorph_exp_of_mem_Ico (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (x : ℝ) (hx : x ∈ Set.Ico 0 (↑l + ↑r)) : (outerBoundaryHomeomorph l r hl hr) (Circle.exp (2 * Real.pi / (↑l + ↑r) * x)) = (outerArc l r hl hr) ⟨x, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerBoundaryHomeomorph_exp_of_mem_Icc (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (x : ℝ) (hx : x ∈ Set.Icc 0 (↑l + ↑r)) : (outerBoundaryHomeomorph l r hl hr) (Circle.exp (2 * Real.pi / (↑l + ↑r) * x)) = (outerArc l r hl hr) ⟨x, hx⟩

def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.polygonSideParameter {n : ℕ} (i : Fin n) (t : ↑unitInterval) : ↑(Set.Icc 0 ↑n)

The combined real parameter of a polygon side.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.polygonSideParameter i t = ⟨↑↑i + ↑t, ⋯⟩

def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.sourceSideParameter (l r : ℕ) (i : Fin (l + r)) (t : ↑unitInterval) : ↑(Set.Icc 0 (↑l + ↑r))

The same parameter with the split side count displayed as a sum in ℝ.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.sourceSideParameter l r i t = ⟨↑↑i + ↑t, ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.sourceCellHomeomorph (l r : ℕ) (hl : 0 < l) (hr : 0 < r) : PolygonCell (l + r) ≃ₜ ↑square

Extend the exact outer-boundary parameterization across the unsplit source polygon.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.sourceCellHomeomorph_ofCircle_exp (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (x : ℝ) (hx : x ∈ Set.Icc 0 (↑l + ↑r)) : (sourceCellHomeomorph l r hl hr) ((PolygonCell.ofCircle (l + r)) (Circle.exp (2 * Real.pi / (↑l + ↑r) * x))) = boundaryInclusion ((outerArc l r hl hr) ⟨x, hx⟩)

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.sourceCellHomeomorph_side (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (i : Fin (l + r)) (t : ↑unitInterval) : (sourceCellHomeomorph l r hl hr) ((PolygonCell.side i) t) = boundaryInclusion ((outerArc l r hl hr) (sourceSideParameter l r i t))

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.boundaryInclusion_finalOldArc_polygonSide (l : ℕ) (hl : 0 < l) (i : Fin l) (t : ↑unitInterval) : boundaryInclusion ((finalOldArc l hl) (polygonSideParameter i t)) = leftPlacement ((finalSideCellHomeomorph l hl) ((PolygonCell.side (Fin.castAdd 1 i)) t))

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.boundaryInclusion_firstOldArc_polygonSide (r : ℕ) (hr : 0 < r) (i : Fin r) (t : ↑unitInterval) : boundaryInclusion ((firstOldArc r hr) (polygonSideParameter i t)) = rightPlacement ((firstSideCellHomeomorph r hr) ((PolygonCell.side (i.addNat 1)) t))

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerArc_source_left_side (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (i : Fin l) (t : ↑unitInterval) : (outerArc l r hl hr) (sourceSideParameter l r (Fin.castAdd r i) t) = (finalOldArc l hl) (polygonSideParameter i t)

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.outerArc_source_right_side (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (i : Fin r) (t : ↑unitInterval) : (outerArc l r hl hr) (sourceSideParameter l r (Fin.natAdd l i) t) = (firstOldArc r hr) (polygonSideParameter i t)

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.sourceCellHomeomorph_left_side (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (i : Fin l) (t : ↑unitInterval) : (sourceCellHomeomorph l r hl hr) ((PolygonCell.side (Fin.castAdd r i)) t) = leftPlacement ((finalSideCellHomeomorph l hl) ((PolygonCell.side (Fin.castAdd 1 i)) t))

On every old left side, the unsplit source polygon map agrees exactly with the corresponding placed child side.

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.sourceCellHomeomorph_right_side (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (i : Fin r) (t : ↑unitInterval) : (sourceCellHomeomorph l r hl hr) ((PolygonCell.side (Fin.natAdd l i)) t) = rightPlacement ((firstSideCellHomeomorph r hr) ((PolygonCell.side (i.addNat 1)) t))

On every old right side, the unsplit source polygon map agrees exactly with the corresponding reflected and placed child side.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.paramChildGluingHomeomorph_mk_inl (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (z : PolygonCell (l + 1)) : (paramChildGluingHomeomorph l r hl hr) (Quotient.mk'' (Sum.inl z)) = leftPlacement ((finalSideCellHomeomorph l hl) z)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.paramChildGluingHomeomorph_mk_inr (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (z : PolygonCell (r + 1)) : (paramChildGluingHomeomorph l r hl hr) (Quotient.mk'' (Sum.inr z)) = rightPlacement ((firstSideCellHomeomorph r hr) z)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.sourceChildGluingHomeomorph (l r : ℕ) (hl : 0 < l) (hr : 0 < r) : PolygonCell (l + r) ≃ₜ ParamChildGluing l r

The complete local P2 equivalence: one unsplit polygon is homeomorphic to the quotient of the two child polygons by their reversed fresh-side identification.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.sourceChildGluingHomeomorph_left_side (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (i : Fin l) (t : ↑unitInterval) : (sourceChildGluingHomeomorph l r hl hr) ((PolygonCell.side (Fin.castAdd r i)) t) = Quotient.mk'' (Sum.inl ((PolygonCell.side (Fin.castAdd 1 i)) t))

The local P2 homeomorphism sends every left source side to the corresponding selected-child side class.

theorem LeanEval.Topology.ClassificationOfSurfaces.DiskSquare.sourceChildGluingHomeomorph_right_side (l r : ℕ) (hl : 0 < l) (hr : 0 < r) (i : Fin r) (t : ↑unitInterval) : (sourceChildGluingHomeomorph l r hl hr) ((PolygonCell.side (Fin.natAdd l i)) t) = Quotient.mk'' (Sum.inr ((PolygonCell.side (i.addNat 1)) t))

The local P2 homeomorphism sends every right source side to the corresponding right-child side class.