Synchronized polygonal arrangements with additional finite cuts

The relative Radó weld must cut the common old/new planar arrangement by finitely many additional lines coming from retained PL face certificates. Both sides must still be literal submeshes of one ambient triangle mesh. This file records that harmless extra-line generalization of PolygonalFamily.synchronizedArrangement.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.relativeSynchronizedArrangement {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) : TriangleMesh

Cut the polygon-family arrangement simultaneously by a target mesh and by an additional finite list of affine lines.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.relativeSynchronizedArrangement_support {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) : (relativeSynchronizedArrangement J N lines).toPlaneComplex.support = (arrangementMesh J).toPlaneComplex.support

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.IsSelectedRelativeSynchronizedTriangle {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (p : ι → Prop) (t : Finset (relativeSynchronizedArrangement J N lines).Vertex) : Prop

A relative synchronized chamber belongs to the selected polygonal side.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.selectedRelativeSynchronizedMesh {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (p : ι → Prop) : TriangleMesh

The selected polygonal member after all additional cuts.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.IsTargetRelativeSynchronizedTriangle {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (t : Finset (relativeSynchronizedArrangement J N lines).Vertex) : Prop

A relative synchronized chamber belongs to the prescribed target side exactly when its interior meets the target support.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.targetRelativeSynchronizedMesh {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) : TriangleMesh

The target member after all additional cuts.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.selectedRelativeSynchronizedMesh_triangle_mem {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (p : ι → Prop) {t : Finset (selectedRelativeSynchronizedMesh J N lines p).Vertex} : t ∈ (selectedRelativeSynchronizedMesh J N lines p).triangles ↔ t ∈ (relativeSynchronizedArrangement J N lines).triangles ∧ IsSelectedRelativeSynchronizedTriangle J N lines p t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.targetRelativeSynchronizedMesh_triangle_mem {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) {t : Finset (targetRelativeSynchronizedMesh J N lines).Vertex} : t ∈ (targetRelativeSynchronizedMesh J N lines).triangles ↔ t ∈ (relativeSynchronizedArrangement J N lines).triangles ∧ IsTargetRelativeSynchronizedTriangle J N lines t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.exists_arrangementTriangle_of_relativeSynchronized {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) {N : TriangleMesh} {lines : List (Plane →ᵃ[ℝ] ℝ)} {t : Finset (relativeSynchronizedArrangement J N lines).Vertex} (ht : t ∈ (relativeSynchronizedArrangement J N lines).triangles) : ∃ u ∈ (arrangementMesh J).triangles, (relativeSynchronizedArrangement J N lines).triangleCarrier t ⊆ (arrangementMesh J).triangleCarrier u

Every chamber after the extra cuts remains inside an original polygon-family arrangement triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.relativeSynchronizedTriangle_interior_side {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (i : ι) {t : Finset (relativeSynchronizedArrangement J N lines).Vertex} (ht : t ∈ (relativeSynchronizedArrangement J N lines).triangles) : interior ((relativeSynchronizedArrangement J N lines).triangleCarrier t) ⊆ (J i).interiorRegion ∨ interior ((relativeSynchronizedArrangement J N lines).triangleCarrier t) ⊆ (J i).exteriorRegion

Extra cuts preserve the one-sidedness of every chamber with respect to every polygon in the family.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.selectedRelativeSynchronizedMesh_support {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (p : ι → Prop) : (selectedRelativeSynchronizedMesh J N lines p).toPlaneComplex.support = selectedClosedRegion J p

Additional cuts do not alter the selected polygonal support.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.exists_targetTriangle_of_targetRelativeSynchronized {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) {t : Finset (targetRelativeSynchronizedMesh J N lines).Vertex} (ht : t ∈ (targetRelativeSynchronizedMesh J N lines).triangles) : ∃ u ∈ N.triangles, (relativeSynchronizedArrangement J N lines).triangleCarrier t ⊆ N.triangleCarrier u

Every retained target chamber lies in a triangle of the prescribed target mesh.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.targetRelativeSynchronizedMesh_support {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (hsub : N.toPlaneComplex.support ⊆ (arrangementMesh J).toPlaneComplex.support) : (targetRelativeSynchronizedMesh J N lines).toPlaneComplex.support = N.toPlaneComplex.support

If the target lies in the polygon-family arrangement, its relative synchronized member has exactly the prescribed support.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalFamily.relativeSynchronizedMeshes_joint_edge_valence {ι : Type u_1} [Fintype ι] (J : ι → PolygonalCircle) (N : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (p : ι → Prop) (e : Finset (relativeSynchronizedArrangement J N lines).Vertex) (he : e.card = 2) : {t ∈ (selectedRelativeSynchronizedMesh J N lines p).triangles ∪ (targetRelativeSynchronizedMesh J N lines).triangles | e ⊆ t}.card ≤ 2

The selected and target members inherit the ambient planar edge-incidence bound.