The Radó crossing weld and chart induction

This file completes the chart-induction framework developed in ChartInductionCore. It constructs the crossing weld, packages the one-chart induction step, and assembles the final triangulation.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.exists_crossing_weld_of_boundaryPreservingStraightening (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] (c : MoiseChart S) (hc : c.BoundaryFaithful) {T : PartialTriangulation S} {A : Set S} (hT : RadoInvariant T A) (hstraight : PartialTriangulation.BoundaryPreservingStraightening S T c) : have x := ⋯; have x := ⋯; ∃ (V : Type) (x : Fintype V) (x_1 : DecidableEq V) (F₁ : Finset (Finset V)) (F₂ : Finset (Finset V)) (e₁ : ↑(GeometricRealization V F₁) → S) (e₂ : ↑(GeometricRealization V F₂) → S), (∀ t ∈ F₁ ∪ F₂, t.card = 3) ∧ Topology.IsEmbedding e₁ ∧ Topology.IsEmbedding e₂ ∧ (∀ (x_2 : ↑(GeometricRealization V F₁)) (y : ↑(GeometricRealization V F₂)), ↑x_2 = ↑y → e₁ x_2 = e₂ y) ∧ (∀ (x_2 : ↑(GeometricRealization V F₁)) (y : ↑(GeometricRealization V F₂)), e₁ x_2 = e₂ y → ↑x_2 = ↑y) ∧ PartialTriangulation.BoundaryFacewiseRegularEmbedding F₁ e₁ ∧ PartialTriangulation.BoundaryFacewiseRegularEmbedding F₂ e₂ ∧ A ∪ c.core ⊆ interior (Set.range e₁ ∪ Set.range e₂)

Shared implementation of the Moise crossing weld once the chart straightening is certified to preserve the ambient manifold-boundary stratum.

In the genuine crossing case (the chart core is not yet covered, and the absorbed region is not inside the chart patch), the adjusted old complex and the chart patch admit a common welded presentation: a common vertex type carrying both face families, with embeddings that agree exactly on the shared realization, satisfy the combinatorial-surface bound jointly, and whose united image contains A ∪ c.core in its topological interior.

The proof straightens the old complex over the chart overlap by the locally finite controlled polygonal replacement over adaptiveOverlapGraphRealization with tolerance vanishing at the overlap frontier (replaceOnOpen/frontierGlue), refine the straightened trace and the fixed patch complex to a common plane subdivision (CommonSubdivision, Moise's conditions (e)-(h)), and read off the welded presentation. The finite compact-collar theorem cannot replace this vanishing-tolerance construction, because continuity across the overlap frontier depends on the error tending to zero there.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.exists_crossing_weld (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] (c : MoiseChart S) (hc : c.BoundaryFaithful) {T : PartialTriangulation S} {A : Set S} (hT : RadoInvariant T A) : ∃ (V : Type) (x : Fintype V) (x_1 : DecidableEq V) (F₁ : Finset (Finset V)) (F₂ : Finset (Finset V)) (e₁ : ↑(GeometricRealization V F₁) → S) (e₂ : ↑(GeometricRealization V F₂) → S), (∀ t ∈ F₁ ∪ F₂, t.card = 3) ∧ Topology.IsEmbedding e₁ ∧ Topology.IsEmbedding e₂ ∧ (∀ (x_2 : ↑(GeometricRealization V F₁)) (y : ↑(GeometricRealization V F₂)), ↑x_2 = ↑y → e₁ x_2 = e₂ y) ∧ (∀ (x_2 : ↑(GeometricRealization V F₁)) (y : ↑(GeometricRealization V F₂)), e₁ x_2 = e₂ y → ↑x_2 = ↑y) ∧ PartialTriangulation.BoundaryFacewiseRegularEmbedding F₁ e₁ ∧ PartialTriangulation.BoundaryFacewiseRegularEmbedding F₂ e₂ ∧ A ∪ c.core ⊆ interior (Set.range e₁ ∪ Set.range e₂)

The bordered crossing weld. The relative straightening preserves the ambient boundary stratum, and the synchronized source/target presentations retain it as a simplicial face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.moise_induction_step (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] (c : MoiseChart S) (hc : c.BoundaryFaithful) {T : PartialTriangulation S} {A : Set S} (hT : RadoInvariant T A) : ∃ (T' : PartialTriangulation S), RadoInvariant T' (A ∪ c.core)

Theorem boundary (Moise Ch. 8, Thm. 3, the induction step; bordered version).

Given a partial triangulation satisfying the Radó invariant for the absorbed region A, and one more boundary-faithful chart, the chart's core can be absorbed: there is a partial triangulation satisfying the invariant for A ∪ c.core.

Moise's proof of the step: work in the chart's model coordinates; take a polyhedral neighborhood of the part of the built complex meeting the chart (Thm. 8.2); adjust it by a PL approximation of the chart-transition homeomorphism (Thm. 6.3, pl_approximation_two_manifold) so that it meets a fine complex containing the model core simplicially (conditions (a)-(h)); glue (Thm. 7.6). The polygonal Jordan and Schoenflies theorems enter through Thm. 6.3.

Hypothesis refinement is expected here (see RadoInvariant); conclusion weakening is not.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.moise_triangulation_of_induction (S : Type u_1) [TopologicalSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] (hstep : ∀ (c : MoiseChart S), c.BoundaryFaithful → ∀ {T : PartialTriangulation S} {A : Set S}, RadoInvariant T A → ∃ (T' : PartialTriangulation S), RadoInvariant T' (A ∪ c.core)) : Nonempty (GeometricTriangulation S)

Shared finite Radó induction assembler. It turns any clean one-chart absorption step with the full RadoInvariant conclusion into an end-to-end geometric triangulation.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.moise_triangulation_of_boundaries (S : Type u_1) [TopologicalSpace S] [T2Space S] [ConnectedSpace S] [CompactSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] : Nonempty (GeometricTriangulation S)

The bordered Radó induction assembled from its boundary-preserving one-chart step.