Carrier coordinates for canonical normal-form words

This file computes the closed-disk boundary coordinates of every canonical word position. It reconciles the canonical positive boundary-block ordering with the trusted Eval relations' negative angles using Fin.rev and integral periodicity. The resulting theorems send each of the five canonical pairing families into the corresponding trusted equivalence closure.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableOccurrencePoint (p n : ℕ) (i : Fin (orientableBoundaryWord p n).length) (t : ↑unitInterval) : (orientableCellComplex p n).PolygonalPreRealization

The point on occurrence i of the canonical orientable one-face presentation.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableCarrier_occurrencePoint (p n : ℕ) (i : Fin (orientableBoundaryWord p n).length) (t : ↑unitInterval) : (SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (orientableBoundaryWord p n)) (orientableOccurrencePoint p n i t) = Complex.ClosedUnitDisc.bdyPtOfReal ((↑↑i + ↑t) / ↑(orientableBoundaryWord p n).length)

The carrier bridge sends occurrence i to the boundary parameter (i+t)/|word|.

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableCarrier_handle_a_pos {p n : ℕ} (i : Fin p) (t : ↑unitInterval) : (SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (orientableBoundaryWord p n)) (orientableOccurrencePoint p n (orientableHandlePosition p n i 0) t) = Complex.ClosedUnitDisc.bdyPtOfReal ((4 * ↑↑i + ↑t) / (4 * ↑p + 3 * ↑n))

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableCarrier_handle_a_neg {p n : ℕ} (i : Fin p) (t : ↑unitInterval) : (SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (orientableBoundaryWord p n)) (orientableOccurrencePoint p n (orientableHandlePosition p n i 2) (unitInterval.symm t)) = Complex.ClosedUnitDisc.bdyPtOfReal ((4 * ↑↑i + 3 - ↑t) / (4 * ↑p + 3 * ↑n))

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableCarrier_handle_b_pos {p n : ℕ} (i : Fin p) (t : ↑unitInterval) : (SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (orientableBoundaryWord p n)) (orientableOccurrencePoint p n (orientableHandlePosition p n i 1) t) = Complex.ClosedUnitDisc.bdyPtOfReal ((4 * ↑↑i + 1 + ↑t) / (4 * ↑p + 3 * ↑n))

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableCarrier_handle_b_neg {p n : ℕ} (i : Fin p) (t : ↑unitInterval) : (SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (orientableBoundaryWord p n)) (orientableOccurrencePoint p n (orientableHandlePosition p n i 3) (unitInterval.symm t)) = Complex.ClosedUnitDisc.bdyPtOfReal ((4 * ↑↑i + 4 - ↑t) / (4 * ↑p + 3 * ↑n))

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableCarrier_boundary_c_pos {p n : ℕ} (j : Fin n) (t : ↑unitInterval) : (SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (orientableBoundaryWord p n)) (orientableOccurrencePoint p n (orientableBoundaryPosition p n j 0) t) = Complex.ClosedUnitDisc.bdyPtOfReal ((4 * ↑p + 3 * ↑↑j + ↑t) / (4 * ↑p + 3 * ↑n))

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableCarrier_boundary_h_pos {p n : ℕ} (j : Fin n) (t : ↑unitInterval) : (SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (orientableBoundaryWord p n)) (orientableOccurrencePoint p n (orientableBoundaryPosition p n j 1) t) = Complex.ClosedUnitDisc.bdyPtOfReal ((4 * ↑p + 3 * ↑↑j + 1 + ↑t) / (4 * ↑p + 3 * ↑n))

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableCarrier_boundary_c_neg {p n : ℕ} (j : Fin n) (t : ↑unitInterval) : (SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (orientableBoundaryWord p n)) (orientableOccurrencePoint p n (orientableBoundaryPosition p n j 2) (unitInterval.symm t)) = Complex.ClosedUnitDisc.bdyPtOfReal ((4 * ↑p + 3 * ↑↑j + 3 - ↑t) / (4 * ↑p + 3 * ↑n))

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.fin_rev_cast_real {n : ℕ} (j : Fin n) : ↑↑j.rev = ↑n - ↑↑j - 1

Reversing a finite index converts its real value to n - j - 1.

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundary_trustedSource_eq_carrier_c_neg {p n : ℕ} (j : Fin n) (t : ↑unitInterval) : Complex.ClosedUnitDisc.bdyPtOfReal (-(3 * ↑↑j.rev + ↑t) / (4 * ↑p + 3 * ↑n)) = (SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (orientableBoundaryWord p n)) (orientableOccurrencePoint p n (orientableBoundaryPosition p n j 2) (unitInterval.symm t))

Trusted boundary source Fin.rev j is the second canonical cⱼ side, modulo one turn.

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableBoundary_trustedTarget_eq_carrier_c_pos {p n : ℕ} (j : Fin n) (t : ↑unitInterval) : Complex.ClosedUnitDisc.bdyPtOfReal (-(3 * ↑↑j.rev + 3 - ↑t) / (4 * ↑p + 3 * ↑n)) = (SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (orientableBoundaryWord p n)) (orientableOccurrencePoint p n (orientableBoundaryPosition p n j 0) t)

Trusted boundary target Fin.rev j is the first canonical cⱼ side, modulo one turn.

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableCarrier_handle_a_eqvGen {p n : ℕ} (i : Fin p) (t : ↑unitInterval) : Relation.EqvGen (OrientableRel p n) ((SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (orientableBoundaryWord p n)) (orientableOccurrencePoint p n (orientableHandlePosition p n i 0) t)) ((SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (orientableBoundaryWord p n)) (orientableOccurrencePoint p n (orientableHandlePosition p n i 2) (unitInterval.symm t)))

Every canonical aᵢ side pairing maps into the trusted orientable equivalence closure.

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableCarrier_handle_b_eqvGen {p n : ℕ} (i : Fin p) (t : ↑unitInterval) : Relation.EqvGen (OrientableRel p n) ((SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (orientableBoundaryWord p n)) (orientableOccurrencePoint p n (orientableHandlePosition p n i 1) t)) ((SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (orientableBoundaryWord p n)) (orientableOccurrencePoint p n (orientableHandlePosition p n i 3) (unitInterval.symm t)))

Every canonical bᵢ side pairing maps into the trusted orientable equivalence closure.

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.orientableCarrier_boundary_c_eqvGen {p n : ℕ} (j : Fin n) (t : ↑unitInterval) : Relation.EqvGen (OrientableRel p n) ((SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (orientableBoundaryWord p n)) (orientableOccurrencePoint p n (orientableBoundaryPosition p n j 0) t)) ((SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (orientableBoundaryWord p n)) (orientableOccurrencePoint p n (orientableBoundaryPosition p n j 2) (unitInterval.symm t)))

Every canonical cⱼ side pairing maps into the trusted orientable equivalence closure.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableOccurrencePoint (p n : ℕ) (i : Fin (nonOrientableBoundaryWord p n).length) (t : ↑unitInterval) : (nonOrientableCellComplex p n).PolygonalPreRealization

The point on occurrence i of the canonical nonorientable one-face presentation.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCarrier_occurrencePoint (p n : ℕ) (i : Fin (nonOrientableBoundaryWord p n).length) (t : ↑unitInterval) : (SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (nonOrientableBoundaryWord p n)) (nonOrientableOccurrencePoint p n i t) = Complex.ClosedUnitDisc.bdyPtOfReal ((↑↑i + ↑t) / ↑(nonOrientableBoundaryWord p n).length)

The nonorientable carrier bridge sends occurrence i to (i+t)/|word|.

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCarrier_crosscap_a_first {p n : ℕ} (i : Fin p) (t : ↑unitInterval) : (SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (nonOrientableBoundaryWord p n)) (nonOrientableOccurrencePoint p n (nonOrientableCrosscapPosition p n i 0) t) = Complex.ClosedUnitDisc.bdyPtOfReal ((2 * ↑↑i + ↑t) / (2 * ↑p + 3 * ↑n))

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCarrier_crosscap_a_second {p n : ℕ} (i : Fin p) (t : ↑unitInterval) : (SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (nonOrientableBoundaryWord p n)) (nonOrientableOccurrencePoint p n (nonOrientableCrosscapPosition p n i 1) t) = Complex.ClosedUnitDisc.bdyPtOfReal ((2 * ↑↑i + 1 + ↑t) / (2 * ↑p + 3 * ↑n))

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCarrier_boundary_c_pos {p n : ℕ} (j : Fin n) (t : ↑unitInterval) : (SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (nonOrientableBoundaryWord p n)) (nonOrientableOccurrencePoint p n (nonOrientableBoundaryPosition p n j 0) t) = Complex.ClosedUnitDisc.bdyPtOfReal ((2 * ↑p + 3 * ↑↑j + ↑t) / (2 * ↑p + 3 * ↑n))

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCarrier_boundary_h_pos {p n : ℕ} (j : Fin n) (t : ↑unitInterval) : (SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (nonOrientableBoundaryWord p n)) (nonOrientableOccurrencePoint p n (nonOrientableBoundaryPosition p n j 1) t) = Complex.ClosedUnitDisc.bdyPtOfReal ((2 * ↑p + 3 * ↑↑j + 1 + ↑t) / (2 * ↑p + 3 * ↑n))

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCarrier_boundary_c_neg {p n : ℕ} (j : Fin n) (t : ↑unitInterval) : (SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (nonOrientableBoundaryWord p n)) (nonOrientableOccurrencePoint p n (nonOrientableBoundaryPosition p n j 2) (unitInterval.symm t)) = Complex.ClosedUnitDisc.bdyPtOfReal ((2 * ↑p + 3 * ↑↑j + 3 - ↑t) / (2 * ↑p + 3 * ↑n))

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundary_trustedSource_eq_carrier_c_neg {p n : ℕ} (j : Fin n) (t : ↑unitInterval) : Complex.ClosedUnitDisc.bdyPtOfReal (-(3 * ↑↑j.rev + ↑t) / (2 * ↑p + 3 * ↑n)) = (SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (nonOrientableBoundaryWord p n)) (nonOrientableOccurrencePoint p n (nonOrientableBoundaryPosition p n j 2) (unitInterval.symm t))

Trusted boundary source Fin.rev j is the second nonorientable cⱼ side.

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableBoundary_trustedTarget_eq_carrier_c_pos {p n : ℕ} (j : Fin n) (t : ↑unitInterval) : Complex.ClosedUnitDisc.bdyPtOfReal (-(3 * ↑↑j.rev + 3 - ↑t) / (2 * ↑p + 3 * ↑n)) = (SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (nonOrientableBoundaryWord p n)) (nonOrientableOccurrencePoint p n (nonOrientableBoundaryPosition p n j 0) t)

Trusted boundary target Fin.rev j is the first nonorientable cⱼ side.

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCarrier_crosscap_a_eqvGen {p n : ℕ} (i : Fin p) (t : ↑unitInterval) : Relation.EqvGen (NonOrientableRel p n) ((SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (nonOrientableBoundaryWord p n)) (nonOrientableOccurrencePoint p n (nonOrientableCrosscapPosition p n i 0) t)) ((SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (nonOrientableBoundaryWord p n)) (nonOrientableOccurrencePoint p n (nonOrientableCrosscapPosition p n i 1) t))

Every canonical crosscap pairing maps into the trusted nonorientable closure.

theorem LeanEval.Topology.ClassificationOfSurfaces.NormalForm.nonOrientableCarrier_boundary_c_eqvGen {p n : ℕ} (j : Fin n) (t : ↑unitInterval) : Relation.EqvGen (NonOrientableRel p n) ((SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (nonOrientableBoundaryWord p n)) (nonOrientableOccurrencePoint p n (nonOrientableBoundaryPosition p n j 0) t)) ((SurfaceCellComplex.oneFacePolygonalPreRealizationHomeomorph (nonOrientableBoundaryWord p n)) (nonOrientableOccurrencePoint p n (nonOrientableBoundaryPosition p n j 2) (unitInterval.symm t)))

Every canonical boundary-seam pairing maps into the trusted nonorientable closure.