Subdividing finite plane complexes by affine lines

Moise Chapter 2 cuts a polygonal region by the finitely many lines containing its edges. This file develops that construction from its local primitive: when an affine functional has opposite signs at the endpoints of an edge, its zero gives the new subdivision vertex on that edge.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.affineBasisOfTriangle (p : Fin 3 → Plane) (hp : AffineIndependent ℝ p) : AffineBasis (Fin 3) ℝ Plane

Three affinely independent points form an affine basis of the plane.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.affineBasisOfTriangle p hp = { toFun := p, ind' := hp, tot' := ⋯ }

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.triangleAffineEquiv (p q : Fin 3 → Plane) (hp : AffineIndependent ℝ p) (hq : AffineIndependent ℝ q) : Plane ≃ᵃ[ℝ] Plane

The affine equivalence carrying one ordered nondegenerate plane triangle to another.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.triangleAffineEquiv_apply (p q : Fin 3 → Plane) (hp : AffineIndependent ℝ p) (hq : AffineIndependent ℝ q) (i : Fin 3) : (triangleAffineEquiv p q hp hq) (p i) = q i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.triangleAffineEquiv_image_convexHull (p q : Fin 3 → Plane) (hp : AffineIndependent ℝ p) (hq : AffineIndependent ℝ q) : ⇑(triangleAffineEquiv p q hp hq) '' (convexHull ℝ) (Set.range p) = (convexHull ℝ) (Set.range q)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.triangleAffineEquiv_apply_lineMap (p q : Fin 3 → Plane) (hp : AffineIndependent ℝ p) (hq : AffineIndependent ℝ q) (i j : Fin 3) (c : ℝ) : (triangleAffineEquiv p q hp hq) ((AffineMap.lineMap (p i) (p j)) c) = (AffineMap.lineMap (q i) (q j)) c

The affine equivalence between ordered triangles carries corresponding line-map points to corresponding line-map points.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.affineIndependent_plane_triple_of_det_ne_zero {p₀ p₁ p₂ : Plane} (hdet : (p₁ - p₀).ofLp 0 * (p₂ - p₀).ofLp 1 - (p₁ - p₀).ofLp 1 * (p₂ - p₀).ofLp 0 ≠ 0) : AffineIndependent ℝ ![p₀, p₁, p₂]

The determinant criterion for three points in the Euclidean plane.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.convexHull_inter_affine_zero_of_nonneg (s : Finset Plane) (f : Plane →ᵃ[ℝ] ℝ) (hf : ∀ x ∈ s, 0 ≤ f x) : (convexHull ℝ) ↑s ∩ {x : Plane | f x = 0} = (convexHull ℝ) ↑({x ∈ s | f x = 0})

An affine supporting hyperplane cuts a finite convex hull in precisely the hull of the vertices lying on that hyperplane.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.convexHull_inter_affine_zero_of_nonneg_set (s : Set Plane) (f : Plane →ᵃ[ℝ] ℝ) (hf : ∀ x ∈ s, 0 ≤ f x) : (convexHull ℝ) s ∩ {x : Plane | f x = 0} = (convexHull ℝ) (s ∩ {x : Plane | f x = 0})

Set-valued version of the supporting-hyperplane face formula. Convex-hull membership uses only finitely many points, so the finite formula above applies to each witness.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.convexHull_inter_of_affine_separation (s t u : Finset Plane) (f : Plane →ᵃ[ℝ] ℝ) (hs : ∀ x ∈ s, 0 ≤ f x) (ht : ∀ x ∈ t, f x ≤ 0) (hszero : {x ∈ s | f x = 0} = u) (htzero : {x ∈ t | f x = 0} = u) : (convexHull ℝ) ↑s ∩ (convexHull ℝ) ↑t = (convexHull ℝ) ↑u

Two finite convex hulls lying on opposite sides of an affine hyperplane intersect in their common zero face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.convexHull_image_inter_of_affine_separation {V : Type u_1} [DecidableEq V] (position : V → Plane) : Function.Injective position → ∀ (s t : Finset V) (f : Plane →ᵃ[ℝ] ℝ) (hs : ∀ v ∈ s, 0 ≤ f (position v)) (ht : ∀ v ∈ t, f (position v) ≤ 0) (hszero : ∀ v ∈ s, f (position v) = 0 ↔ v ∈ s ∩ t) (htzero : ∀ v ∈ t, f (position v) = 0 ↔ v ∈ s ∩ t), (convexHull ℝ) (position '' ↑s) ∩ (convexHull ℝ) (position '' ↑t) = (convexHull ℝ) (position '' ↑(s ∩ t))

Vertex-indexed form of convexHull_inter_of_affine_separation. This is the form used when checking the maximal triangles of a mesh.

The reference split of a triangle

def LeanEval.Topology.ClassificationOfSurfaces.Moise.planePoint (x y : ℝ) : Plane

A point of the Euclidean plane with the displayed Cartesian coordinates.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.planePoint x y = !₂[x, y]

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.planePoint_apply_zero (x y : ℝ) : (planePoint x y).ofLp 0 = x

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.planePoint_apply_one (x y : ℝ) : (planePoint x y).ofLp 1 = y

def LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceSplitPosition (a b : ℝ) : Fin 5 → Plane

Vertices of the reference line split: the standard triangle vertices followed by one point on each edge issuing from the origin.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceSplitTriangles : Finset (Finset (Fin 5))

The referenceSplitTriangles declaration.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceSplitTriangles = {{0, 3, 4}, {1, 2, 3}, {2, 3, 4}}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceSplitPosition_injective {a b : ℝ} (ha0 : 0 < a) (ha1 : a < 1) (hb0 : 0 < b) (hb1 : b < 1) : Function.Injective (referenceSplitPosition a b)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceSplit_triangle0_affineIndependent {a b : ℝ} (ha0 : 0 < a) (hb0 : 0 < b) : AffineIndependent ℝ ![planePoint 0 0, planePoint a 0, planePoint 0 b]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceSplit_triangle1_affineIndependent {a : ℝ} (ha1 : a < 1) : AffineIndependent ℝ ![planePoint a 0, planePoint 1 0, planePoint 0 1]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceSplit_triangle2_affineIndependent {a b : ℝ} (ha0 : 0 < a) (hb1 : b < 1) : AffineIndependent ℝ ![planePoint a 0, planePoint 0 1, planePoint 0 b]

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.cartesianX : Plane →ᵃ[ℝ] ℝ

The first Cartesian coordinate, regarded as an affine functional.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.cartesianX = (LinearMap.proj 0 ∘ₗ ↑(WithLp.linearEquiv 2 ℝ (Fin 2 → ℝ))).toAffineMap

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.cartesianY : Plane →ᵃ[ℝ] ℝ

The second Cartesian coordinate, regarded as an affine functional.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.cartesianY = (LinearMap.proj 1 ∘ₗ ↑(WithLp.linearEquiv 2 ℝ (Fin 2 → ℝ))).toAffineMap

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.cartesianX_apply (p : Plane) : cartesianX p = p.ofLp 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.cartesianY_apply (p : Plane) : cartesianY p = p.ofLp 1

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceOuterAffine (a b : ℝ) : Plane →ᵃ[ℝ] ℝ

The affine line through the two new edge points in the reference split.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceDiagonalAffine (a : ℝ) : Plane →ᵃ[ℝ] ℝ

The affine line through (a,0) and (0,1) in the reference split.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceVertexAffine (a b : ℝ) : Plane →ᵃ[ℝ] ℝ

A line through (a,0) lying strictly between the other two rays of the reference split. Its second coefficient is chosen between a and a / b.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceOuterAffine_planePoint (a b x y : ℝ) : (referenceOuterAffine a b) (planePoint x y) = a⁻¹ * x + b⁻¹ * y - 1

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceDiagonalAffine_planePoint (a x y : ℝ) : (referenceDiagonalAffine a) (planePoint x y) = x + a * y - a

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceVertexAffine_planePoint (a b x y : ℝ) : (referenceVertexAffine a b) (planePoint x y) = x + a * (1 + b) / (2 * b) * y - a

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceSplitMesh (a b : ℝ) (ha0 : 0 < a) (ha1 : a < 1) (hb0 : 0 < b) (hb1 : b < 1) : TriangleMesh

The three triangles produced when a line meets the two edges issuing from the origin of the standard triangle.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.mem_convexHull_range_fin3_of_weights (p : Fin 3 → Plane) (x : Plane) (w : Fin 3 → ℝ) (hw : ∀ (i : Fin 3), 0 ≤ w i) (hsum : w 0 + w 1 + w 2 = 1) (hx : w 0 • p 0 + w 1 • p 1 + w 2 • p 2 = x) : x ∈ (convexHull ℝ) (Set.range p)

A three-term nonnegative affine combination belongs to the corresponding triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.mem_standardTriangle_iff (x : Plane) : x ∈ (convexHull ℝ) (Set.range ![planePoint 0 0, planePoint 1 0, planePoint 0 1]) ↔ 0 ≤ x.ofLp 0 ∧ 0 ≤ x.ofLp 1 ∧ x.ofLp 0 + x.ofLp 1 ≤ 1

Cartesian membership criterion for the standard closed triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceSplit_union (a b : ℝ) (ha0 : 0 < a) (ha1 : a < 1) (hb0 : 0 < b) (hb1 : b < 1) : ⋃ t ∈ referenceSplitTriangles, (convexHull ℝ) (referenceSplitPosition a b '' ↑t) = (convexHull ℝ) (Set.range ![planePoint 0 0, planePoint 1 0, planePoint 0 1])

The three reference triangles cover exactly the standard triangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceSplitMesh_support (a b : ℝ) (ha0 : 0 < a) (ha1 : a < 1) (hb0 : 0 < b) (hb1 : b < 1) : (referenceSplitMesh a b ha0 ha1 hb0 hb1).toPlaneComplex.support = (convexHull ℝ) (Set.range ![planePoint 0 0, planePoint 1 0, planePoint 0 1])

The reference line split preserves the support of the standard triangle.

The reference split through one vertex

def LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceEdgeSplitPosition (c : ℝ) : Fin 4 → Plane

The referenceEdgeSplitPosition declaration.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceEdgeSplitTriangles : Finset (Finset (Fin 4))

The referenceEdgeSplitTriangles declaration.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceEdgeSplitTriangles = {{0, 2, 3}, {1, 2, 3}}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceEdgeSplitPosition_injective {c : ℝ} (hc0 : 0 < c) (hc1 : c < 1) : Function.Injective (referenceEdgeSplitPosition c)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceEdgeSplitMesh (c : ℝ) (hc0 : 0 < c) (hc1 : c < 1) : TriangleMesh

The two-triangle reference mesh used when the cutting line passes through vertex 2.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceEdgeSplit_union (c : ℝ) (hc0 : 0 < c) (hc1 : c < 1) : ⋃ t ∈ referenceEdgeSplitTriangles, (convexHull ℝ) (referenceEdgeSplitPosition c '' ↑t) = (convexHull ℝ) (Set.range ![planePoint 0 0, planePoint 1 0, planePoint 0 1])

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.referenceEdgeSplitMesh_support (c : ℝ) (hc0 : 0 < c) (hc1 : c < 1) : (referenceEdgeSplitMesh c hc0 hc1).toPlaneComplex.support = (convexHull ℝ) (Set.range ![planePoint 0 0, planePoint 1 0, planePoint 0 1])

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.affineCutPoint (f : Plane →ᵃ[ℝ] ℝ) (p q : Plane) : Plane

The point where the affine functional f vanishes along the oriented edge from p to q. The useful case is f p > 0 > f q.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.affineCutPoint f p q = (AffineMap.lineMap p q) (f p / (f p - f q))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.affineCutPoint.parameter_pos (f : Plane →ᵃ[ℝ] ℝ) (p q : Plane) (hp : 0 < f p) (hq : f q < 0) : 0 < f p / (f p - f q)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.affineCutPoint.parameter_lt_one (f : Plane →ᵃ[ℝ] ℝ) (p q : Plane) (hp : 0 < f p) (hq : f q < 0) : f p / (f p - f q) < 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.affineCutPoint.parameter_mem_Icc (f : Plane →ᵃ[ℝ] ℝ) (p q : Plane) (hp : 0 < f p) (hq : f q < 0) : f p / (f p - f q) ∈ Set.Icc 0 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.affineCutPoint.mem_segment (f : Plane →ᵃ[ℝ] ℝ) (p q : Plane) (hp : 0 < f p) (hq : f q < 0) : affineCutPoint f p q ∈ segment ℝ p q

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.affineCutPoint.apply_eq_zero (f : Plane →ᵃ[ℝ] ℝ) (p q : Plane) (hp : 0 < f p) (hq : f q < 0) : f (affineCutPoint f p q) = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.affineCutPoint.ne_left (f : Plane →ᵃ[ℝ] ℝ) (p q : Plane) (hp : 0 < f p) (hq : f q < 0) : affineCutPoint f p q ≠ p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.affineCutPoint.ne_right (f : Plane →ᵃ[ℝ] ℝ) (p q : Plane) (hp : 0 < f p) (hq : f q < 0) : affineCutPoint f p q ≠ q

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.affineCutPoint.eq_reverse (f : Plane →ᵃ[ℝ] ℝ) (p q : Plane) (hp : 0 < f p) (hq : f q < 0) : affineCutPoint f p q = affineCutPoint f q p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.affineCutPoint.eq_of_mem_segment_of_apply_eq_zero (f : Plane →ᵃ[ℝ] ℝ) (p q : Plane) (hp : 0 < f p) (hq : f q < 0) {x : Plane} (hx : x ∈ segment ℝ p q) (hfx : f x = 0) : x = affineCutPoint f p q

The cut point is the unique zero of f on an oppositely signed edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.affineCutPoint.neg (f : Plane →ᵃ[ℝ] ℝ) (p q : Plane) : affineCutPoint (-f) p q = affineCutPoint f p q

Negating the affine functional does not change its geometric cut point.

The transported split of an arbitrary triangle

def LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTrianglePosition : Fin 3 → Plane

The ordered vertices of the standard triangle.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTrianglePosition_affineIndependent : AffineIndependent ℝ standardTrianglePosition

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.triangleCutParameter (f : Plane →ᵃ[ℝ] ℝ) (p q : Plane) : ℝ

The parameter at which a line cuts the edge from the positive vertex to a negative vertex.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.triangleCutParameter f p q = f p / (f p - f q)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.triangleLineSplitMesh (p : Fin 3 → Plane) (hp : AffineIndependent ℝ p) (f : Plane →ᵃ[ℝ] ℝ) (hp0 : 0 < f (p 0)) (hp1 : f (p 1) < 0) (hp2 : f (p 2) < 0) : TriangleMesh

The reference split transported to an arbitrary ordered triangle. The first vertex is on the positive side of the line and the other two are on its negative side.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.triangleLineSplitMesh_support (p : Fin 3 → Plane) (hp : AffineIndependent ℝ p) (f : Plane →ᵃ[ℝ] ℝ) (hp0 : 0 < f (p 0)) (hp1 : f (p 1) < 0) (hp2 : f (p 2) < 0) : (triangleLineSplitMesh p hp f hp0 hp1 hp2).toPlaneComplex.support = (convexHull ℝ) (Set.range p)

Splitting a triangle along an affine line preserves its support.

Coherent cut vertices for a finite mesh

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.Triangle (M : TriangleMesh) : Type

The maximal triangles, packaged with their membership proof.

Equations

• M.Triangle = ↥M.triangles

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.triangleEquiv (M : TriangleMesh) (t : M.Triangle) : ↥↑t ≃ Fin 3

A proof-independent ordering of the three vertices of a maximal triangle.

Equations

• M.triangleEquiv t = Fintype.equivFinOfCardEq ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.orderedVertex (M : TriangleMesh) (t : M.Triangle) : Fin 3 → M.Vertex

A proof-independent ordering of the three vertices of a maximal triangle.

Equations

• M.orderedVertex t i = ↑((M.triangleEquiv t).symm i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.orderedVertex_injective (M : TriangleMesh) (t : M.Triangle) : Function.Injective (M.orderedVertex t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.range_orderedVertex (M : TriangleMesh) (t : M.Triangle) : Set.range (M.orderedVertex t) = ↑↑t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.orderedVertex_mem (M : TriangleMesh) (t : M.Triangle) (i : Fin 3) : M.orderedVertex t i ∈ ↑t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.orderedVertex_affineIndependent (M : TriangleMesh) (t : M.Triangle) : AffineIndependent ℝ (M.position ∘ M.orderedVertex t)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.crossingPairs (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) : Finset (M.Vertex × M.Vertex)

Ordered pairs of old vertices whose values under f have opposite signs. Both orientations are retained; their geometric cut positions are equal and are deduplicated in refinementPoints.

Equations

• M.crossingPairs f = {uv ∈ Finset.univ ×ˢ Finset.univ | f (M.position uv.1) * f (M.position uv.2) < 0}

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.pairCutPosition (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (u v : M.Vertex) : Plane

The geometric zero of f on an oppositely signed pair of old vertices.

Equations

• M.pairCutPosition f u v = LeanEval.Topology.ClassificationOfSurfaces.Moise.affineCutPoint f (M.position u) (M.position v)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.refinementPoints (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) : Finset Plane

All old vertex positions together with all possible cut positions. Using geometric points as the new vertex labels automatically identifies the cut computed from the two orientations of one edge, and the same edge as seen from its two incident triangles.

Equations

• M.refinementPoints f = Finset.image M.position Finset.univ ∪ Finset.image (fun (uv : M.Vertex × M.Vertex) => M.pairCutPosition f uv.1 uv.2) (M.crossingPairs f)

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.RefinedVertex (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) : Type

Vertex type used by the coherent refinement.

Equations

• M.RefinedVertex f = ↥(M.refinementPoints f)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.oldRefinedVertex (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : M.Vertex) : M.RefinedVertex f

An old vertex as a vertex of the coherent refinement.

Equations

• M.oldRefinedVertex f v = ⟨M.position v, ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.cutRefinedVertex (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (u v : M.Vertex) (huv : f (M.position u) * f (M.position v) < 0) : M.RefinedVertex f

The cut point of an oppositely signed pair as a vertex of the coherent refinement.

Equations

• M.cutRefinedVertex f u v huv = ⟨M.pairCutPosition f u v, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.oldRefinedVertex_val (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : M.Vertex) : ↑(M.oldRefinedVertex f v) = M.position v

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.cutRefinedVertex_val (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (u v : M.Vertex) (huv : f (M.position u) * f (M.position v) < 0) : ↑(M.cutRefinedVertex f u v huv) = M.pairCutPosition f u v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.pairCutPosition_eq_reverse (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (u v : M.Vertex) (huv : f (M.position u) * f (M.position v) < 0) : M.pairCutPosition f u v = M.pairCutPosition f v u

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.pairCutPosition_apply_eq_zero (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (u v : M.Vertex) (huv : f (M.position u) * f (M.position v) < 0) : f (M.pairCutPosition f u v) = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.crossingPairs_neg (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) : M.crossingPairs (-f) = M.crossingPairs f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.refinementPoints_neg (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) : M.refinementPoints (-f) = M.refinementPoints f

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.refinedVertexNegEquiv (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) : M.RefinedVertex (-f) ≃ M.RefinedVertex f

Identifying the coherent vertex pools for f and -f; geometrically this is the identity.

Equations

• M.refinedVertexNegEquiv f = { toFun := fun (v : M.RefinedVertex (-f)) => ⟨↑v, ⋯⟩, invFun := fun (v : M.RefinedVertex f) => ⟨↑v, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.refinedVertexNegEquiv_val (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : M.RefinedVertex (-f)) : ↑((M.refinedVertexNegEquiv f) v) = ↑v

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictModelVertex (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) (h0 : 0 < f (M.position (M.orderedVertex t 0))) (h1 : f (M.position (M.orderedVertex t 1)) < 0) (h2 : f (M.position (M.orderedVertex t 2)) < 0) : Fin 5 → M.RefinedVertex f

The five vertices of the strict +-- model in the coherent global vertex pool.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictModelPosition (p : Fin 3 → Plane) (f : Plane →ᵃ[ℝ] ℝ) : Fin 5 → Plane

The geometric five-point list underlying a strict split.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictModelVertex_val (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) (h0 : 0 < f (M.position (M.orderedVertex t 0))) (h1 : f (M.position (M.orderedVertex t 1)) < 0) (h2 : f (M.position (M.orderedVertex t 2)) < 0) (i : Fin 5) : ↑(M.strictModelVertex f t h0 h1 h2 i) = strictModelPosition (M.position ∘ M.orderedVertex t) f i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictModelPosition_eq_affineReference (f : Plane →ᵃ[ℝ] ℝ) (p : Fin 3 → Plane) (hp : AffineIndependent ℝ p) : 0 < f (p 0) → f (p 1) < 0 → f (p 2) < 0 → ∀ (i : Fin 5), strictModelPosition p f i = (triangleAffineEquiv standardTrianglePosition p standardTrianglePosition_affineIndependent hp) (referenceSplitPosition (triangleCutParameter f (p 0) (p 1)) (triangleCutParameter f (p 0) (p 2)) i)

Geometric identification of the strict five-point list with the affine image of the reference split.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictLocalEmbedding (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) (h0 : 0 < f (M.position (M.orderedVertex t 0))) (h1 : f (M.position (M.orderedVertex t 1)) < 0) (h2 : f (M.position (M.orderedVertex t 2)) < 0) : Fin 5 ↪ M.RefinedVertex f

The strict local model embedded into the shared refinement vertex type.

Equations

• M.strictLocalEmbedding f t h0 h1 h2 = { toFun := M.strictModelVertex f t h0 h1 h2, inj' := ⋯ }

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictLocalMesh (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) (h0 : 0 < f (M.position (M.orderedVertex t 0))) (h1 : f (M.position (M.orderedVertex t 1)) < 0) (h2 : f (M.position (M.orderedVertex t 2)) < 0) : TriangleMesh

The strict local split, now using the coherent global vertex pool.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictLocalMesh_support (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) (h0 : 0 < f (M.position (M.orderedVertex t 0))) (h1 : f (M.position (M.orderedVertex t 1)) < 0) (h2 : f (M.position (M.orderedVertex t 2)) < 0) : (M.strictLocalMesh f t h0 h1 h2).toPlaneComplex.support = (convexHull ℝ) (M.position '' ↑↑t)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictNegativeLocalMesh (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) (h0 : f (M.position (M.orderedVertex t 0)) < 0) (h1 : 0 < f (M.position (M.orderedVertex t 1))) (h2 : 0 < f (M.position (M.orderedVertex t 2))) : TriangleMesh

The strict -++ local split, obtained by applying the +-- model to -f and identifying the two coherent vertex pools.

Equations

• M.strictNegativeLocalMesh f t h0 h1 h2 = (M.strictLocalMesh (-f) t ⋯ ⋯ ⋯).reindex Subtype.val ⋯ (M.refinedVertexNegEquiv f).toEmbedding ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictNegativeLocalMesh_support (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) (h0 : f (M.position (M.orderedVertex t 0)) < 0) (h1 : 0 < f (M.position (M.orderedVertex t 1))) (h2 : 0 < f (M.position (M.orderedVertex t 2))) : (M.strictNegativeLocalMesh f t h0 h1 h2).toPlaneComplex.support = (convexHull ℝ) (M.position '' ↑↑t)

The same strict model for an arbitrary ordering of three vertices.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictVertices (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (h0 : 0 < f (M.position (v 0))) (h1 : f (M.position (v 1)) < 0) (h2 : f (M.position (v 2)) < 0) : Fin 5 → M.RefinedVertex f

The strictVertices declaration.

Equations

• M.strictVertices f v h0 h1 h2 = ![M.oldRefinedVertex f (v 0), M.oldRefinedVertex f (v 1), M.oldRefinedVertex f (v 2), M.cutRefinedVertex f (v 0) (v 1) ⋯, M.cutRefinedVertex f (v 0) (v 2) ⋯]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictVertices_val (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (h0 : 0 < f (M.position (v 0))) (h1 : f (M.position (v 1)) < 0) (h2 : f (M.position (v 2)) < 0) (i : Fin 5) : ↑(M.strictVertices f v h0 h1 h2 i) = strictModelPosition (M.position ∘ v) f i

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictVerticesEmbedding (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (hv : AffineIndependent ℝ (M.position ∘ v)) (h0 : 0 < f (M.position (v 0))) (h1 : f (M.position (v 1)) < 0) (h2 : f (M.position (v 2)) < 0) : Fin 5 ↪ M.RefinedVertex f

The strictVerticesEmbedding declaration.

Equations

• M.strictVerticesEmbedding f v hv h0 h1 h2 = { toFun := M.strictVertices f v h0 h1 h2, inj' := ⋯ }

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictMeshFor (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (hv : AffineIndependent ℝ (M.position ∘ v)) (h0 : 0 < f (M.position (v 0))) (h1 : f (M.position (v 1)) < 0) (h2 : f (M.position (v 2)) < 0) : TriangleMesh

The strictMeshFor declaration.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictMeshFor_support (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (hv : AffineIndependent ℝ (M.position ∘ v)) (h0 : 0 < f (M.position (v 0))) (h1 : f (M.position (v 1)) < 0) (h2 : f (M.position (v 2)) < 0) : (M.strictMeshFor f v hv h0 h1 h2).toPlaneComplex.support = (convexHull ℝ) (Set.range (M.position ∘ v))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictNegativeMeshFor (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (hv : AffineIndependent ℝ (M.position ∘ v)) (h0 : f (M.position (v 0)) < 0) (h1 : 0 < f (M.position (v 1))) (h2 : 0 < f (M.position (v 2))) : TriangleMesh

The strictNegativeMeshFor declaration.

Equations

• M.strictNegativeMeshFor f v hv h0 h1 h2 = (M.strictMeshFor (-f) v hv ⋯ ⋯ ⋯).reindex Subtype.val ⋯ (M.refinedVertexNegEquiv f).toEmbedding ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictNegativeMeshFor_support (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (hv : AffineIndependent ℝ (M.position ∘ v)) (h0 : f (M.position (v 0)) < 0) (h1 : 0 < f (M.position (v 1))) (h2 : 0 < f (M.position (v 2))) : (M.strictNegativeMeshFor f v hv h0 h1 h2).toPlaneComplex.support = (convexHull ℝ) (Set.range (M.position ∘ v))

The two-triangle model when vertex 2 lies on the cutting line.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edgeModelPosition (p : Fin 3 → Plane) (f : Plane →ᵃ[ℝ] ℝ) : Fin 4 → Plane

The edgeModelPosition declaration.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edgeModelPosition p f = ![p 0, p 1, p 2, LeanEval.Topology.ClassificationOfSurfaces.Moise.affineCutPoint f (p 0) (p 1)]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edgeModelPosition_eq_affineReference (f : Plane →ᵃ[ℝ] ℝ) (p : Fin 3 → Plane) (hp : AffineIndependent ℝ p) : 0 < f (p 0) → f (p 1) < 0 → ∀ (i : Fin 4), edgeModelPosition p f i = (triangleAffineEquiv standardTrianglePosition p standardTrianglePosition_affineIndependent hp) (referenceEdgeSplitPosition (triangleCutParameter f (p 0) (p 1)) i)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edgeVertices (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (h0 : 0 < f (M.position (v 0))) (h1 : f (M.position (v 1)) < 0) : Fin 4 → M.RefinedVertex f

The edgeVertices declaration.

Equations

• M.edgeVertices f v h0 h1 = ![M.oldRefinedVertex f (v 0), M.oldRefinedVertex f (v 1), M.oldRefinedVertex f (v 2), M.cutRefinedVertex f (v 0) (v 1) ⋯]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edgeVertices_val (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (h0 : 0 < f (M.position (v 0))) (h1 : f (M.position (v 1)) < 0) (i : Fin 4) : ↑(M.edgeVertices f v h0 h1 i) = edgeModelPosition (M.position ∘ v) f i

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edgeVerticesEmbedding (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (hv : AffineIndependent ℝ (M.position ∘ v)) (h0 : 0 < f (M.position (v 0))) (h1 : f (M.position (v 1)) < 0) : Fin 4 ↪ M.RefinedVertex f

The edgeVerticesEmbedding declaration.

Equations

• M.edgeVerticesEmbedding f v hv h0 h1 = { toFun := M.edgeVertices f v h0 h1, inj' := ⋯ }

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edgeMeshFor (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (hv : AffineIndependent ℝ (M.position ∘ v)) (h0 : 0 < f (M.position (v 0))) (h1 : f (M.position (v 1)) < 0) : TriangleMesh

The edgeMeshFor declaration.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edgeMeshFor_support (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (hv : AffineIndependent ℝ (M.position ∘ v)) (h0 : 0 < f (M.position (v 0))) (h1 : f (M.position (v 1)) < 0) : (M.edgeMeshFor f v hv h0 h1).toPlaneComplex.support = (convexHull ℝ) (Set.range (M.position ∘ v))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edgeNegativeMeshFor (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (hv : AffineIndependent ℝ (M.position ∘ v)) (h0 : f (M.position (v 0)) < 0) (h1 : 0 < f (M.position (v 1))) : TriangleMesh

The edgeNegativeMeshFor declaration.

Equations

• M.edgeNegativeMeshFor f v hv h0 h1 = (M.edgeMeshFor (-f) v hv ⋯ ⋯).reindex Subtype.val ⋯ (M.refinedVertexNegEquiv f).toEmbedding ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edgeNegativeMeshFor_support (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (hv : AffineIndependent ℝ (M.position ∘ v)) (h0 : f (M.position (v 0)) < 0) (h1 : 0 < f (M.position (v 1))) : (M.edgeNegativeMeshFor f v hv h0 h1).toPlaneComplex.support = (convexHull ℝ) (Set.range (M.position ∘ v))

Choosing the local model from the signs

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.orderedVertex_perm_affineIndependent (M : TriangleMesh) (t : M.Triangle) (σ : Equiv.Perm (Fin 3)) : AffineIndependent ℝ (M.position ∘ M.orderedVertex t ∘ ⇑σ)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.range_orderedVertex_perm (M : TriangleMesh) (t : M.Triangle) (σ : Equiv.Perm (Fin 3)) : Set.range (M.position ∘ M.orderedVertex t ∘ ⇑σ) = M.position '' ↑↑t

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.PositiveStrictOrdering (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) : Type

A vertex ordering with one positive value followed by two negative values.

• perm : Equiv.Perm (Fin 3)

  The perm declaration.

• positive : 0 < f (M.position (M.orderedVertex t (self.perm 0)))
• negative_one : f (M.position (M.orderedVertex t (self.perm 1))) < 0
• negative_two : f (M.position (M.orderedVertex t (self.perm 2))) < 0

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.NegativeStrictOrdering (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) : Type

A vertex ordering with one negative value followed by two positive values.

• perm : Equiv.Perm (Fin 3)

  The perm declaration.

• negative : f (M.position (M.orderedVertex t (self.perm 0))) < 0
• positive_one : 0 < f (M.position (M.orderedVertex t (self.perm 1)))
• positive_two : 0 < f (M.position (M.orderedVertex t (self.perm 2)))

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.PositiveEdgeOrdering (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) : Type

A vertex ordering with one positive, one negative, and one zero value.

• perm : Equiv.Perm (Fin 3)

  The perm declaration.

• positive : 0 < f (M.position (M.orderedVertex t (self.perm 0)))
• negative : f (M.position (M.orderedVertex t (self.perm 1))) < 0
• zero : f (M.position (M.orderedVertex t (self.perm 2))) = 0

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.NegativeEdgeOrdering (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) : Type

A vertex ordering with one negative, one positive, and one zero value.

• perm : Equiv.Perm (Fin 3)

  The perm declaration.

• negative : f (M.position (M.orderedVertex t (self.perm 0))) < 0
• positive : 0 < f (M.position (M.orderedVertex t (self.perm 1)))
• zero : f (M.position (M.orderedVertex t (self.perm 2))) = 0

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.oldVerticesEmbedding (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (hv : AffineIndependent ℝ (M.position ∘ v)) : Fin 3 ↪ M.RefinedVertex f

The oldVerticesEmbedding declaration.

Equations

• M.oldVerticesEmbedding f v hv = { toFun := fun (i : Fin 3) => M.oldRefinedVertex f (v i), inj' := ⋯ }

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.unchangedMeshFor (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (hv : AffineIndependent ℝ (M.position ∘ v)) : TriangleMesh

The unchangedMeshFor declaration.

Equations

• M.unchangedMeshFor f v hv = (LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.single (M.position ∘ v) hv).reindex Subtype.val ⋯ (M.oldVerticesEmbedding f v hv) ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.unchangedMeshFor_support (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (hv : AffineIndependent ℝ (M.position ∘ v)) : (M.unchangedMeshFor f v hv).toPlaneComplex.support = (convexHull ℝ) (Set.range (M.position ∘ v))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.localRefinementMesh (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) : TriangleMesh

The canonical local refinement mesh for one old triangle.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.localRefinementMesh_support (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) : (M.localRefinementMesh f t).toPlaneComplex.support = (convexHull ℝ) (M.position '' ↑↑t)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.IsMonochromatic (N : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) : Prop

Every maximal triangle lies wholly on one closed side of the cutting line.

Equations

• N.IsMonochromatic f = ∀ s ∈ N.triangles, (∀ v ∈ s, 0 ≤ f (N.position v)) ∨ ∀ v ∈ s, f (N.position v) ≤ 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.IsMonochromatic.of_neg (f : Plane →ᵃ[ℝ] ℝ) {N : TriangleMesh} (hN : N.IsMonochromatic (-f)) : N.IsMonochromatic f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.IsMonochromatic.reindex {N : TriangleMesh} {V' : Type} [Fintype V'] [DecidableEq V'] (position' : V' → Plane) (hposition_injective : Function.Injective position') (e : N.Vertex ↪ V') (hposition : ∀ (v : N.Vertex), position' (e v) = N.position v) (g : Plane →ᵃ[ℝ] ℝ) (hN : N.IsMonochromatic g) : (N.reindex position' hposition_injective e hposition).IsMonochromatic g

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictVertices_f (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (h0 : 0 < f (M.position (v 0))) (h1 : f (M.position (v 1)) < 0) (h2 : f (M.position (v 2)) < 0) (i : Fin 5) : f ↑(M.strictVertices f v h0 h1 h2 i) = ![f (M.position (v 0)), f (M.position (v 1)), f (M.position (v 2)), 0, 0] i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edgeVertices_f (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (h0 : 0 < f (M.position (v 0))) (h1 : f (M.position (v 1)) < 0) (hzero : f (M.position (v 2)) = 0) (i : Fin 4) : f ↑(M.edgeVertices f v h0 h1 i) = ![f (M.position (v 0)), f (M.position (v 1)), 0, 0] i

def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.RefinedTrianglesMonochromatic (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (T : Finset (Finset (M.RefinedVertex f))) : Prop

Monochromaticity stated directly for triangles in the shared refined vertex pool.

Equations

• M.RefinedTrianglesMonochromatic f T = ∀ s ∈ T, (∀ x ∈ s, 0 ≤ f ↑x) ∨ ∀ x ∈ s, f ↑x ≤ 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictTriangles_monochromatic (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (hv : AffineIndependent ℝ (M.position ∘ v)) (h0 : 0 < f (M.position (v 0))) (h1 : f (M.position (v 1)) < 0) (h2 : f (M.position (v 2)) < 0) : M.RefinedTrianglesMonochromatic f (Finset.image (fun (t : Finset (Fin 5)) => Finset.map (M.strictVerticesEmbedding f v hv h0 h1 h2) t) referenceSplitTriangles)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edgeTriangles_monochromatic (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (hv : AffineIndependent ℝ (M.position ∘ v)) (h0 : 0 < f (M.position (v 0))) (h1 : f (M.position (v 1)) < 0) (hzero : f (M.position (v 2)) = 0) : M.RefinedTrianglesMonochromatic f (Finset.image (fun (t : Finset (Fin 4)) => Finset.map (M.edgeVerticesEmbedding f v hv h0 h1) t) referenceEdgeSplitTriangles)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictPatternTriangles {V : Type u_1} [DecidableEq V] (z : Fin 5 → V) : Finset (Finset V)

The abstract three-triangle combinatorial pattern of a strict cut.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictPatternTriangles z = {{z 0, z 3, z 4}, {z 1, z 2, z 3}, {z 2, z 3, z 4}}

def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edgePatternTriangles {V : Type u_1} [DecidableEq V] (z : Fin 4 → V) : Finset (Finset V)

The abstract two-triangle combinatorial pattern of a cut through vertex 2.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edgePatternTriangles z = {{z 0, z 2, z 3}, {z 1, z 2, z 3}}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.exists_index_of_mem_strictPattern {V : Type u_1} [DecidableEq V] (z : Fin 5 → V) {s : Finset V} (hs : s ∈ strictPatternTriangles z) {x : V} (hx : x ∈ s) : ∃ (i : Fin 5), x = z i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.exists_index_of_mem_edgePattern {V : Type u_1} [DecidableEq V] (z : Fin 4 → V) {s : Finset V} (hs : s ∈ edgePatternTriangles z) {x : V} (hx : x ∈ s) : ∃ (i : Fin 4), x = z i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictMeshFor_triangles (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (hv : AffineIndependent ℝ (M.position ∘ v)) (h0 : 0 < f (M.position (v 0))) (h1 : f (M.position (v 1)) < 0) (h2 : f (M.position (v 2)) < 0) : (M.strictMeshFor f v hv h0 h1 h2).triangles = strictPatternTriangles (M.strictVertices f v h0 h1 h2)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edgeMeshFor_triangles (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (hv : AffineIndependent ℝ (M.position ∘ v)) (h0 : 0 < f (M.position (v 0))) (h1 : f (M.position (v 1)) < 0) : (M.edgeMeshFor f v hv h0 h1).triangles = edgePatternTriangles (M.edgeVertices f v h0 h1)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictNegativeMeshFor_monochromatic (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (hv : AffineIndependent ℝ (M.position ∘ v)) (h0 : f (M.position (v 0)) < 0) (h1 : 0 < f (M.position (v 1))) (h2 : 0 < f (M.position (v 2))) : M.RefinedTrianglesMonochromatic f (M.strictNegativeMeshFor f v hv h0 h1 h2).triangles

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edgeNegativeMeshFor_monochromatic (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (v : Fin 3 → M.Vertex) (hv : AffineIndependent ℝ (M.position ∘ v)) (h0 : f (M.position (v 0)) < 0) (h1 : 0 < f (M.position (v 1))) (h2 : f (M.position (v 2)) = 0) : M.RefinedTrianglesMonochromatic f (M.edgeNegativeMeshFor f v hv h0 h1).triangles

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictPattern_monochromatic_positive (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (z : Fin 5 → M.RefinedVertex f) (h0 : 0 ≤ f ↑(z 0)) (h1 : f ↑(z 1) ≤ 0) (h2 : f ↑(z 2) ≤ 0) (h3 : f ↑(z 3) = 0) (h4 : f ↑(z 4) = 0) : M.RefinedTrianglesMonochromatic f (strictPatternTriangles z)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.strictPattern_monochromatic_negative (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (z : Fin 5 → M.RefinedVertex f) (h0 : f ↑(z 0) ≤ 0) (h1 : 0 ≤ f ↑(z 1)) (h2 : 0 ≤ f ↑(z 2)) (h3 : f ↑(z 3) = 0) (h4 : f ↑(z 4) = 0) : M.RefinedTrianglesMonochromatic f (strictPatternTriangles z)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edgePattern_monochromatic_positive (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (z : Fin 4 → M.RefinedVertex f) (h0 : 0 ≤ f ↑(z 0)) (h1 : f ↑(z 1) ≤ 0) (h2 : f ↑(z 2) = 0) (h3 : f ↑(z 3) = 0) : M.RefinedTrianglesMonochromatic f (edgePatternTriangles z)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.edgePattern_monochromatic_negative (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (z : Fin 4 → M.RefinedVertex f) (h0 : f ↑(z 0) ≤ 0) (h1 : 0 ≤ f ↑(z 1)) (h2 : f ↑(z 2) = 0) (h3 : f ↑(z 3) = 0) : M.RefinedTrianglesMonochromatic f (edgePatternTriangles z)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.localOldVertex (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) (i : Fin 3) : M.RefinedVertex f

The old vertex numbered i in a triangle, regarded as a refined vertex.

Equations

• M.localOldVertex f t i = M.oldRefinedVertex f (M.orderedVertex t i)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.localCutVertex (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) (i j : Fin 3) (hij : f (M.position (M.orderedVertex t i)) * f (M.position (M.orderedVertex t j)) < 0) : M.RefinedVertex f

The cut vertex on the pair of locally numbered vertices i,j.

Equations

• M.localCutVertex f t i j hij = M.cutRefinedVertex f (M.orderedVertex t i) (M.orderedVertex t j) hij

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.localOldVertex_val (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) (i : Fin 3) : ↑(M.localOldVertex f t i) = M.position (M.orderedVertex t i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.localCutVertex_apply_eq_zero (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) (i j : Fin 3) (hij : f (M.position (M.orderedVertex t i)) * f (M.position (M.orderedVertex t j)) < 0) : f ↑(M.localCutVertex f t i j hij) = 0

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.localRefinementTriangles (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) : Finset (Finset (M.RefinedVertex f))

Canonical local triangulation after cutting one old triangle by f. There are three triangles when one vertex is strictly separated from the other two, two triangles when the line passes through one vertex and cuts the opposite edge, and the old triangle when the line already meets it in a face.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.localRefinementTriangles_monochromatic (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) : M.RefinedTrianglesMonochromatic f (M.localRefinementTriangles f t)

Cutting one old triangle by an affine line produces triangles contained in the two closed half-planes.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.refinedMeshTriangles (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (N : TriangleMesh) (h : N.Vertex = M.RefinedVertex f) : Finset (Finset (M.RefinedVertex f))

View a mesh whose vertex type is identified with the refined vertex pool as a family of triangles on that fixed pool.

Equations

• M.refinedMeshTriangles f N h = h ▸ N.triangles

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.localMeshTriangles (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) : Finset (Finset (M.RefinedVertex f))

The maximal triangles selected by the certified local model, exposed on the fixed shared vertex pool.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.card_of_mem_localMeshTriangles (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) {s : Finset (M.RefinedVertex f)} (hs : s ∈ M.localMeshTriangles f t) : s.card = 3

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.affineIndependent_of_mem_localMeshTriangles (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) {s : Finset (M.RefinedVertex f)} (hs : s ∈ M.localMeshTriangles f t) : AffineIndependent ℝ fun (v : ↥s) => ↑↑v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.localMeshTriangles_monochromatic (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) : M.RefinedTrianglesMonochromatic f (M.localMeshTriangles f t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.local_child_vertex_old_or_zero (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) {s : Finset (M.RefinedVertex f)} (hs : s ∈ M.localMeshTriangles f t) {x : M.RefinedVertex f} (hx : x ∈ s) : (∃ v ∈ ↑t, ↑x = M.position v) ∨ f ↑x = 0

A vertex used by a local line refinement is either an old vertex of its parent triangle or lies on the cutting line.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.localMeshTriangles_support (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) : ⋃ s ∈ M.localMeshTriangles f t, (convexHull ℝ) (Subtype.val '' ↑s) = (convexHull ℝ) (M.position '' ↑↑t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.localMeshTriangles_inter (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) {s u : Finset (M.RefinedVertex f)} (hs : s ∈ M.localMeshTriangles f t) (hu : u ∈ M.localMeshTriangles f t) : (convexHull ℝ) (Subtype.val '' ↑s) ∩ (convexHull ℝ) (Subtype.val '' ↑u) = (convexHull ℝ) (Subtype.val '' ↑(s ∩ u))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.convexHull_child_subset_parent (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) {s : Finset (M.RefinedVertex f)} (hs : s ∈ M.localMeshTriangles f t) : (convexHull ℝ) (Subtype.val '' ↑s) ⊆ (convexHull ℝ) (M.position '' ↑↑t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.child_vertex_mem_parent (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) {s : Finset (M.RefinedVertex f)} (hs : s ∈ M.localMeshTriangles f t) {v : M.RefinedVertex f} (hv : v ∈ s) : ↑v ∈ (convexHull ℝ) (M.position '' ↑↑t)

Barycentric traces on old parent edges

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.oppositeCoord (M : TriangleMesh) (t : M.Triangle) (k : Fin 3) : Plane →ᵃ[ℝ] ℝ

The barycentric coordinate opposite the k-th edge of an old triangle.

Equations

• M.oppositeCoord t k = (LeanEval.Topology.ClassificationOfSurfaces.Moise.affineBasisOfTriangle (M.position ∘ M.orderedVertex t) ⋯).coord k

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.oppositeCoord_vertex (M : TriangleMesh) (t : M.Triangle) (k i : Fin 3) : (M.oppositeCoord t k) (M.position (M.orderedVertex t i)) = if k = i then 1 else 0

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.oppositeEdgePoints (M : TriangleMesh) (t : M.Triangle) (k : Fin 3) : Finset Plane

The two old geometric vertices of the edge opposite k.

Equations

• M.oppositeEdgePoints t k = Finset.image (M.position ∘ M.orderedVertex t) (Finset.univ.erase k)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.oppositeEdgePoints_subset_parentPoints (M : TriangleMesh) (t : M.Triangle) (k : Fin 3) : M.oppositeEdgePoints t k ⊆ Finset.image (M.position ∘ M.orderedVertex t) Finset.univ

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.oppositeCoord_nonneg_of_mem_parent (M : TriangleMesh) (t : M.Triangle) (k : Fin 3) {x : Plane} (hx : x ∈ (convexHull ℝ) (M.position '' ↑↑t)) : 0 ≤ (M.oppositeCoord t k) x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.parent_inter_oppositeCoord_zero (M : TriangleMesh) (t : M.Triangle) (k : Fin 3) : (convexHull ℝ) (M.position '' ↑↑t) ∩ {x : Plane | (M.oppositeCoord t k) x = 0} = (convexHull ℝ) ↑(M.oppositeEdgePoints t k)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.childEdgeTrace (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) (k : Fin 3) (s : Finset (M.RefinedVertex f)) : Finset (M.RefinedVertex f)

Vertices of a child triangle lying on the old edge opposite k.

Equations

• M.childEdgeTrace f t k s = {v ∈ s | (M.oppositeCoord t k) ↑v = 0}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.child_inter_oppositeEdge (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) (k : Fin 3) {s : Finset (M.RefinedVertex f)} (hs : s ∈ M.localMeshTriangles f t) : (convexHull ℝ) (Subtype.val '' ↑s) ∩ (convexHull ℝ) ↑(M.oppositeEdgePoints t k) = (convexHull ℝ) (Subtype.val '' ↑(M.childEdgeTrace f t k s))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.exists_oppositeEdgePoints_eq (M : TriangleMesh) (t : M.Triangle) {e : Finset M.Vertex} (het : e ⊆ ↑t) (hecard : e.card = 2) : ∃ (k : Fin 3), M.oppositeEdgePoints t k = Finset.image M.position e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.affine_apply_injectiveOn_segment {g : Plane →ᵃ[ℝ] ℝ} {p q : Plane} (hpq : g p ≠ g q) : Set.InjOn (⇑g) (segment ℝ p q)

An affine functional taking different values at the endpoints of a segment is injective on that segment.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.eq_endpoint_of_mem_segment_apply_zero_of_mul_nonneg {g : Plane →ᵃ[ℝ] ℝ} {p q x : Plane} (hprod : 0 ≤ g p * g q) (hnotboth : ¬(g p = 0 ∧ g q = 0)) (hx : x ∈ segment ℝ p q) (hzero : g x = 0) : x = p ∨ x = q

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.affineIndependent_subset_pair {p q : Plane} (hpq : p ≠ q) {s : Set Plane} (hs : s ⊆ {p, q}) : AffineIndependent ℝ Subtype.val

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.old_vertex_mem_of_oppositeCoord_zero (M : TriangleMesh) (t : M.Triangle) (k : Fin 3) {e : Finset M.Vertex} (hedge : M.oppositeEdgePoints t k = Finset.image M.position e) {v : M.Vertex} (hvt : v ∈ ↑t) (hzero : (M.oppositeCoord t k) (M.position v) = 0) : v ∈ e

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.trace_vertex_old_edge_or_zero (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) (k : Fin 3) {e : Finset M.Vertex} (hedge : M.oppositeEdgePoints t k = Finset.image M.position e) {s : Finset (M.RefinedVertex f)} (hs : s ∈ M.localMeshTriangles f t) {x : M.RefinedVertex f} (hx : x ∈ M.childEdgeTrace f t k s) : (∃ v ∈ e, ↑x = M.position v) ∨ f ↑x = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.trace_vertex_mem_oppositeEdgeHull (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) (k : Fin 3) {s : Finset (M.RefinedVertex f)} (hs : s ∈ M.localMeshTriangles f t) {x : M.RefinedVertex f} (hx : x ∈ M.childEdgeTrace f t k s) : ↑x ∈ (convexHull ℝ) ↑(M.oppositeEdgePoints t k)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.trace_vertex_eq_endpoint_or_cut (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) (k : Fin 3) {a b : M.Vertex} (hab : a ≠ b) (hedge : M.oppositeEdgePoints t k = Finset.image M.position {a, b}) {s : Finset (M.RefinedVertex f)} (hs : s ∈ M.localMeshTriangles f t) (ha : 0 < f (M.position a)) (hb : f (M.position b) < 0) {x : M.RefinedVertex f} (hx : x ∈ M.childEdgeTrace f t k s) : x = M.oldRefinedVertex f a ∨ x = M.oldRefinedVertex f b ∨ x = M.cutRefinedVertex f a b ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.trace_vertex_eq_endpoint_of_mul_nonneg (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) (k : Fin 3) {a b : M.Vertex} (hab : a ≠ b) (hedge : M.oppositeEdgePoints t k = Finset.image M.position {a, b}) {s : Finset (M.RefinedVertex f)} (hs : s ∈ M.localMeshTriangles f t) (hprod : 0 ≤ f (M.position a) * f (M.position b)) (hnotboth : ¬(f (M.position a) = 0 ∧ f (M.position b) = 0)) {x : M.RefinedVertex f} (hx : x ∈ M.childEdgeTrace f t k s) : x = M.oldRefinedVertex f a ∨ x = M.oldRefinedVertex f b

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.orderedVertex_eq_endpoint_of_ne_opposite (M : TriangleMesh) (t : M.Triangle) (k j : Fin 3) {a b : M.Vertex} (hedge : M.oppositeEdgePoints t k = Finset.image M.position {a, b}) (hjk : j ≠ k) : M.orderedVertex t j = a ∨ M.orderedVertex t j = b

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.trace_vertex_eq_endpoint_of_edge_in_line (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) (k : Fin 3) {a b : M.Vertex} : a ≠ b → ∀ (hedge : M.oppositeEdgePoints t k = Finset.image M.position {a, b}) {s : Finset (M.RefinedVertex f)} (hs : s ∈ M.localMeshTriangles f t) (ha : f (M.position a) = 0) (hb : f (M.position b) = 0) {x : M.RefinedVertex f} (hx : x ∈ M.childEdgeTrace f t k s), x = M.oldRefinedVertex f a ∨ x = M.oldRefinedVertex f b

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.childEdgeTrace_monochromatic (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) (k : Fin 3) {s : Finset (M.RefinedVertex f)} (hs : s ∈ M.localMeshTriangles f t) : (∀ x ∈ M.childEdgeTrace f t k s, 0 ≤ f ↑x) ∨ ∀ x ∈ M.childEdgeTrace f t k s, f ↑x ≤ 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.convexHull_inter_of_signed_three_point_subsets (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) {a b z : M.RefinedVertex f} (ha : 0 < f ↑a) (hb : f ↑b < 0) (hz : f ↑z = 0) {A B : Finset (M.RefinedVertex f)} (hAclass : ∀ x ∈ A, x = a ∨ x = b ∨ x = z) (hBclass : ∀ x ∈ B, x = a ∨ x = b ∨ x = z) (hAmono : (∀ x ∈ A, 0 ≤ f ↑x) ∨ ∀ x ∈ A, f ↑x ≤ 0) (hBmono : (∀ x ∈ B, 0 ≤ f ↑x) ∨ ∀ x ∈ B, f ↑x ≤ 0) : (convexHull ℝ) (Subtype.val '' ↑A) ∩ (convexHull ℝ) (Subtype.val '' ↑B) = (convexHull ℝ) (Subtype.val '' ↑(A ∩ B))

The finite one-dimensional calculation behind compatibility on a cut edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.convexHull_inter_of_two_point_subsets (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) {a b : M.RefinedVertex f} (hab : ↑a ≠ ↑b) {A B : Finset (M.RefinedVertex f)} (hA : ∀ x ∈ A, x = a ∨ x = b) (hB : ∀ x ∈ B, x = a ∨ x = b) : (convexHull ℝ) (Subtype.val '' ↑A) ∩ (convexHull ℝ) (Subtype.val '' ↑B) = (convexHull ℝ) (Subtype.val '' ↑(A ∩ B))

def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.TransverseToEdges (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) : Prop

The cutting line contains no old edge of the mesh.

Equations

• M.TransverseToEdges f = ∀ (t : M.Triangle) (i j : Fin 3), i ≠ j → ¬(f (M.position (M.orderedVertex t i)) = 0 ∧ f (M.position (M.orderedVertex t j)) = 0)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.lineRefinementTriangles_inter_of_parent_inter_card_two (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (T U : M.Triangle) (hcard : (↑T ∩ ↑U).card = 2) {s q : Finset (M.RefinedVertex f)} (hs : s ∈ M.localMeshTriangles f T) (hq : q ∈ M.localMeshTriangles f U) : (convexHull ℝ) (Subtype.val '' ↑s) ∩ (convexHull ℝ) (Subtype.val '' ↑q) = (convexHull ℝ) (Subtype.val '' ↑(s ∩ q))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.vertexSupportCoord (M : TriangleMesh) (t : M.Triangle) (i : Fin 3) : Plane →ᵃ[ℝ] ℝ

A nonnegative affine functional vanishing only at the i-th old vertex.

Equations

• M.vertexSupportCoord t i = AffineMap.const ℝ LeanEval.Topology.ClassificationOfSurfaces.Moise.Plane 1 - M.oppositeCoord t i

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.vertexSupportCoord_vertex (M : TriangleMesh) (t : M.Triangle) (i j : Fin 3) : (M.vertexSupportCoord t i) (M.position (M.orderedVertex t j)) = if i = j then 0 else 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.vertexSupportCoord_nonneg_of_mem_parent (M : TriangleMesh) (t : M.Triangle) (i : Fin 3) {x : Plane} (hx : x ∈ (convexHull ℝ) (M.position '' ↑↑t)) : 0 ≤ (M.vertexSupportCoord t i) x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.parent_inter_vertexSupportCoord_zero (M : TriangleMesh) (t : M.Triangle) (i : Fin 3) : (convexHull ℝ) (M.position '' ↑↑t) ∩ {x : Plane | (M.vertexSupportCoord t i) x = 0} = {M.position (M.orderedVertex t i)}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.old_vertex_mem_child_of_position_mem (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (t : M.Triangle) (i : Fin 3) {s : Finset (M.RefinedVertex f)} (hs : s ∈ M.localMeshTriangles f t) (hmem : M.position (M.orderedVertex t i) ∈ (convexHull ℝ) (Subtype.val '' ↑s)) : M.oldRefinedVertex f (M.orderedVertex t i) ∈ s

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.lineRefinementTriangles_inter_of_parent_inter_card_zero (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (T U : M.Triangle) (hcard : (↑T ∩ ↑U).card = 0) {s q : Finset (M.RefinedVertex f)} (hs : s ∈ M.localMeshTriangles f T) (hq : q ∈ M.localMeshTriangles f U) : (convexHull ℝ) (Subtype.val '' ↑s) ∩ (convexHull ℝ) (Subtype.val '' ↑q) = (convexHull ℝ) (Subtype.val '' ↑(s ∩ q))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.lineRefinementTriangles_inter_of_parent_inter_card_one (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) (T U : M.Triangle) (hcard : (↑T ∩ ↑U).card = 1) {s q : Finset (M.RefinedVertex f)} (hs : s ∈ M.localMeshTriangles f T) (hq : q ∈ M.localMeshTriangles f U) : (convexHull ℝ) (Subtype.val '' ↑s) ∩ (convexHull ℝ) (Subtype.val '' ↑q) = (convexHull ℝ) (Subtype.val '' ↑(s ∩ q))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.lineRefinementTriangles (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) : Finset (Finset (M.RefinedVertex f))

All maximal triangles of the coherent line refinement.

Equations

• M.lineRefinementTriangles f = Finset.univ.biUnion fun (t : M.Triangle) => M.localMeshTriangles f t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.mem_lineRefinementTriangles_iff (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) {s : Finset (M.RefinedVertex f)} : s ∈ M.lineRefinementTriangles f ↔ ∃ (t : M.Triangle), s ∈ M.localMeshTriangles f t

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.card_of_mem_lineRefinementTriangles (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) {s : Finset (M.RefinedVertex f)} (hs : s ∈ M.lineRefinementTriangles f) : s.card = 3

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.affineIndependent_of_mem_lineRefinementTriangles (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) {s : Finset (M.RefinedVertex f)} (hs : s ∈ M.lineRefinementTriangles f) : AffineIndependent ℝ fun (v : ↥s) => ↑↑v

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.lineRefinementTriangles_support (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) : ⋃ s ∈ M.lineRefinementTriangles f, (convexHull ℝ) (Subtype.val '' ↑s) = M.toPlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.lineRefinementTriangles_inter (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) {s q : Finset (M.RefinedVertex f)} (hs : s ∈ M.lineRefinementTriangles f) (hq : q ∈ M.lineRefinementTriangles f) : (convexHull ℝ) (Subtype.val '' ↑s) ∩ (convexHull ℝ) (Subtype.val '' ↑q) = (convexHull ℝ) (Subtype.val '' ↑(s ∩ q))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.lineRefinementMesh (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) : TriangleMesh

Subdivision of a finite triangle mesh by one affine line transverse to its old edges.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.lineRefinementMesh_support (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) : (M.lineRefinementMesh f).toPlaneComplex.support = M.toPlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.lineRefinementMesh_subdivides (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) : (M.lineRefinementMesh f).toPlaneComplex.Subdivides M.toPlaneComplex

Cutting every triangle of a mesh by one affine line gives a subdivision of the original plane complex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.lineRefinementMesh_isMonochromatic (M : TriangleMesh) (f : Plane →ᵃ[ℝ] ℝ) : (M.lineRefinementMesh f).IsMonochromatic f

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.lineRefinementMesh_preserves_monochromatic (M : TriangleMesh) (f g : Plane →ᵃ[ℝ] ℝ) (hM : M.IsMonochromatic g) : (M.lineRefinementMesh f).IsMonochromatic g

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.refineByLines : TriangleMesh → List (Plane →ᵃ[ℝ] ℝ) → TriangleMesh

Successively subdivide a mesh by a finite list of affine lines.

Equations

• x✝.refineByLines [] = x✝
• x✝.refineByLines (g :: gs) = (x✝.lineRefinementMesh g).refineByLines gs

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.refineByLines_support (M : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) : (M.refineByLines lines).toPlaneComplex.support = M.toPlaneComplex.support

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.refineByLines_subdivides (M : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) : (M.refineByLines lines).toPlaneComplex.Subdivides M.toPlaneComplex

Successive line cuts remain a subdivision of the original mesh.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.refineByLines_preserves_monochromatic (M : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) (g : Plane →ᵃ[ℝ] ℝ) (hM : M.IsMonochromatic g) : (M.refineByLines lines).IsMonochromatic g

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.TriangleMesh.refineByLines_isMonochromatic_of_mem (M : TriangleMesh) (lines : List (Plane →ᵃ[ℝ] ℝ)) {g : Plane →ᵃ[ℝ] ℝ} (hg : g ∈ lines) : (M.refineByLines lines).IsMonochromatic g