IndisputableMonolith.Cosmology.RegularNeighborhoodBoundary

   1import Mathlib
   2
   3/-!
   4# Cosmology: regular-neighborhood boundary genus bridge (Phases 27, 28, 31, 35, 37, 39, 40, 41, 42, 43, 44, 46, 47)
   5
   6## Status: PARTIAL THEOREM through Phase 44; CONDITIONAL THEOREM at Phase 47 (0 sorry, 0 new axiom).
   7
   8Phase 25 measured the raw cubical boundary surface of the positive excursion set `{q > 0}` and
   9found real nonmanifold edges in the horizon-annulus handle. Phase 26 therefore switched to the
  10canonical desingularized readout: the boundary of a regular neighborhood of the exact positive
  11region.
  12
  13This module proves the algebraic bridge used by
  14`scripts/cosmogenesis/foam_interface_desingularized.py`. If a compact 3D cubical region has Betti
  15triple `(b₀,b₁,b₂)` and its regular-neighborhood boundary has
  16
  17* boundary components `b₀ + b₂`,
  18* boundary Euler characteristic `2 * (b₀ - b₁ + b₂)`,
  19* genus computed by `components - χ(region)`,
  20
  21then the total desingularized boundary genus is exactly `b₁`.
  22
  23Phase 31 adds the algebraic half of the Phase-30 vertex-link half-quotient. If the raw singular
  24boundary has already had its four-face edges paired, and the singular-edge components supply a
  25half-vertex quotient equal to the missing vertex budget, then the corrected Euler characteristic
  26equals the canonical CW Euler characteristic. The embedded digital-cubical collapse remains OPEN:
  27this file proves the arithmetic bridge and the horizon/dyadic numeric certificates, not the
  28geometric realization theorem.
  29
  30Phase 35 adds the algebraic bridge for the Phase-34 component assembly. If the corrected
  31edge-paired face components have the canonical component count and Euler half-sum, then their
  32total genus is forced to be `b₁`. This still does not prove homeomorphism of the corrected
  33component cellulations to the regular-neighborhood boundary components.
  34
  35Phase 37 adds the algebraic wrapper for the Phase-36 polygon-gluing witness. If a finite polygon
  36gluing supplies binary edge gluing, cyclic quotient-vertex links, and the same corrected component
  37Euler data, then it reduces to the Phase-35 component assembly theorem. This is still a finite
  38combinatorial certificate, not the final regular-neighborhood homeomorphism theorem.
  39
  40Phase 39 adds the algebraic wrapper for the Phase-38 orientability witness. If every polygon
  41component has a full face-orientation assignment with zero contradictions, the oriented certificate
  42inherits the Phase-37 polygon-gluing genus theorem. This records the orientability gate without
  43promoting it to the missing homeomorphism theorem.
  44
  45Phase 40 adds the standard-surface classification wrapper. It records the surface type forced by
  46each oriented polygon component's Euler characteristic, e.g. sphere, torus, and genus-125 surface.
  47This classifies the components abstractly; the embedded homeomorphism to the regular-neighborhood
  48boundary remains the open geometric theorem.
  49
  50Phase 41 tightens the classification wrapper into a full surface-type inventory: the assigned
  51standard surface list must have the same component count as the oriented polygon list, its total
  52Euler characteristic is derived from the standard formula, and the resulting count, Euler, and
  53genus match the regular-neighborhood boundary invariants. The embedded homeomorphism theorem
  54remains open.
  55
  56Phase 42 adds the ordered componentwise Euler-signature bridge. The assigned standard-surface list
  57is not merely right in aggregate: component-by-component, the oriented polygon Euler list equals the
  58standard-surface Euler list. This is still algebraic inventory matching, not the embedded
  59homeomorphism theorem.
  60
  61Phase 43 names the finite component pairing itself. The paired list is the ordered zip between
  62oriented polygon components and standard regular-boundary surface types; every pair is checked for
  63orientation success and Euler match, and the paired inventory has the regular-boundary component,
  64Euler, and genus totals. The actual embedded map remains the open geometric theorem.
  65
  66Phase 44 names the embedded-map obligations that must replace the abstract Phase-43 pairing. A
  67candidate map must be incidence-preserving, bijective on quotient cells, vertex-link preserving,
  68and orientation-preserving. This module proves that such obligations reduce to the existing
  69component-pairing inventory. It does not construct the geometric maps.
  70
  71Phase 46 replaces the abstract Phase-44 obligation `Prop` fields with concrete decidable
  72closed-orientable-surface conditions (`CombinatorialClosedOrientableSurface`: Euler-ok, cyclic links,
  73oriented, and the closed quadrangulation identity `edges = 2*faces`). The horizon and dyadic targets
  74satisfy them by `native_decide`, so the obligation packages close on real combinatorial content rather
  75than placeholders. The embedded homeomorphism still requires the classification of closed surfaces.
  76
  77Phase 47 makes that last dependency a first-class object. `ClosedSurfaceClassification R` names the
  78classification of closed surfaces as an explicit hypothesis on an abstract realization relation `R`
  79(geometric realization homeomorphic to the standard surface), never as an axiom. Conditional on it, the
  80horizon torus/sphere and all dyadic components are realized by their standard surfaces
  81(`horizonAnnulusHandle_realizesStandard`, `dyadicSpongeR20_realizesStandard`). These are CONDITIONAL
  82THEOREMs: the chain from recognition foam to a per-component homeomorphism is complete modulo the one
  83named classical input, with no new axiom.
  84-/
  85
  86namespace IndisputableMonolith
  87namespace Cosmology
  88namespace RegularNeighborhoodBoundary
  89
  90/-- Betti data of a compact 3D region, represented in integers so Euler algebra is literal. -/
  91structure BettiTriple where
  92  b0 : ℤ
  93  b1 : ℤ
  94  b2 : ℤ
  95deriving Repr, DecidableEq
  96
  97/-- Euler characteristic of a 3D region from its Betti triple: `χ = b₀ - b₁ + b₂`. -/
  98def regionEuler (B : BettiTriple) : ℤ :=
  99  B.b0 - B.b1 + B.b2
 100
 101/-- The regular-neighborhood boundary component count predicted by Alexander duality intuition. -/
 102def regularBoundaryComponents (B : BettiTriple) : ℤ :=
 103  B.b0 + B.b2
 104
 105/-- The regular-neighborhood boundary Euler characteristic: doubled region Euler characteristic. -/
 106def regularBoundaryEuler (B : BettiTriple) : ℤ :=
 107  2 * regionEuler B
 108
 109/-- Total genus of the regular-neighborhood boundary, using `χ(boundary) = 2χ(region)`. -/
 110def regularBoundaryGenus (B : BettiTriple) : ℤ :=
 111  regularBoundaryComponents B - regionEuler B
 112
 113/-- A canonical CW model for the desingularized regular boundary: one zero-cell and one
 114two-cell per boundary component, and `2*b₁` one-cells carrying the total handle rank. This is
 115the topological cell-count model behind the Phase-28 certificate, not an embedded cubical
 116sheet-splitting construction. -/
 117def regularBoundaryCWVertices (B : BettiTriple) : ℤ :=
 118  regularBoundaryComponents B
 119
 120/-- One-cells in the canonical regular-boundary CW model. -/
 121def regularBoundaryCWEdges (B : BettiTriple) : ℤ :=
 122  2 * B.b1
 123
 124/-- Two-cells in the canonical regular-boundary CW model. -/
 125def regularBoundaryCWFaces (B : BettiTriple) : ℤ :=
 126  regularBoundaryComponents B
 127
 128/-- Euler characteristic of the canonical regular-boundary CW model. -/
 129def regularBoundaryCWEuler (B : BettiTriple) : ℤ :=
 130  regularBoundaryCWVertices B - regularBoundaryCWEdges B + regularBoundaryCWFaces B
 131
 132/-- **THEOREM (regular-boundary genus bridge).** Once the regular-neighborhood boundary
 133components and Euler characteristic are identified, the total desingularized boundary genus is
 134exactly the region's first Betti number. -/
 135theorem regularBoundaryGenus_eq_b1 (B : BettiTriple) :
 136    regularBoundaryGenus B = B.b1 := by
 137  unfold regularBoundaryGenus regularBoundaryComponents regionEuler
 138  ring
 139
 140/-- Equivalent doubled form, useful when avoiding integer division in downstream certificates. -/
 141theorem regularBoundaryEuler_eq_two_regionEuler (B : BettiTriple) :
 142    regularBoundaryEuler B = 2 * regionEuler B := by
 143  rfl
 144
 145/-- **THEOREM (canonical CW model realizes the doubled Euler law).** The Phase-28 CW boundary
 146model has Euler characteristic `2 * χ(region)`. -/
 147theorem regularBoundaryCWEuler_eq_regularBoundaryEuler (B : BettiTriple) :
 148    regularBoundaryCWEuler B = regularBoundaryEuler B := by
 149  unfold regularBoundaryCWEuler regularBoundaryCWVertices regularBoundaryCWEdges
 150    regularBoundaryCWFaces regularBoundaryEuler regularBoundaryComponents regionEuler
 151  ring
 152
 153/-- The canonical CW model has Euler characteristic `2 * χ(region)` in expanded form. -/
 154theorem regularBoundaryCWEuler_eq_two_regionEuler (B : BettiTriple) :
 155    regularBoundaryCWEuler B = 2 * regionEuler B := by
 156  rw [regularBoundaryCWEuler_eq_regularBoundaryEuler, regularBoundaryEuler_eq_two_regionEuler]
 157
 158/-- The Euler-form surface identity: `components - χ(boundary)/2 = b₁`, encoded without division
 159by using the already-halved `χ(region)` from the doubled-boundary theorem. -/
 160theorem components_minus_regionEuler_eq_b1 (B : BettiTriple) :
 161    regularBoundaryComponents B - regionEuler B = B.b1 := by
 162  simpa [regularBoundaryGenus] using regularBoundaryGenus_eq_b1 B
 163
 164/-- A boundary report satisfies the regular-neighborhood bridge for a region. This is the
 165geometry-facing predicate: future work must prove it for the concrete digital construction. -/
 166structure IsRegularBoundaryOf (B : BettiTriple) where
 167  components : ℤ
 168  euler : ℤ
 169  genus : ℤ
 170  components_eq : components = regularBoundaryComponents B
 171  euler_eq : euler = regularBoundaryEuler B
 172  genus_eq : genus = regularBoundaryGenus B
 173
 174/-- **THEOREM.** Any boundary report satisfying the regular-neighborhood bridge has genus `b₁`. -/
 175theorem genus_eq_b1_of_isRegularBoundaryOf {B : BettiTriple} (S : IsRegularBoundaryOf B) :
 176    S.genus = B.b1 := by
 177  rw [S.genus_eq, regularBoundaryGenus_eq_b1]
 178
 179/-! ## Phase 30/31: singular-edge half-vertex quotient. -/
 180
 181/-- One connected component of the singular-edge graph after the Phase-29 four-face edge pairing
 182step. `vertices` and `edges` are recorded only as cell counts; this is not yet an embedded
 183geometric construction. -/
 184structure SingularGraphComponent where
 185  vertices : ℕ
 186  edges : ℕ
 187deriving Repr, DecidableEq
 188
 189/-- The Phase-30 vertex-link quotient contribution of one singular component: one vertex lift per
 190pair of singular vertices in that component. -/
 191def halfVertexComponentDelta (C : SingularGraphComponent) : ℕ :=
 192  C.vertices / 2
 193
 194/-- Total half-vertex delta over all singular-edge components. -/
 195def singularGraphHalfVertexDelta (Cs : List SingularGraphComponent) : ℕ :=
 196  (Cs.map halfVertexComponentDelta).sum
 197
 198/-- Euler characteristic after Phase-29 edge splitting and the Phase-30 half-vertex correction. -/
 199def halfVertexCorrectedEuler (edgeOnlyEuler : ℤ) (Cs : List SingularGraphComponent) : ℤ :=
 200  edgeOnlyEuler + singularGraphHalfVertexDelta Cs
 201
 202/-- The half-vertex quotient closes when the corrected raw-boundary Euler characteristic equals the
 203canonical Phase-28 regular-boundary CW Euler characteristic. -/
 204def HalfVertexQuotientCloses (B : BettiTriple) (edgeOnlyEuler : ℤ)
 205    (Cs : List SingularGraphComponent) : Prop :=
 206  halfVertexCorrectedEuler edgeOnlyEuler Cs = regularBoundaryCWEuler B
 207
 208/-- Algebraic bridge for the Phase-30 quotient: once the half-vertex delta is exactly the missing
 209vertex budget, the corrected edge-paired Euler count is the canonical CW Euler count. -/
 210theorem halfVertexCorrectedEuler_eq_cw_of_delta_eq_required
 211    (B : BettiTriple) (edgeOnlyEuler : ℤ) (Cs : List SingularGraphComponent)
 212    (requiredDelta : ℕ)
 213    (hDelta : singularGraphHalfVertexDelta Cs = requiredDelta)
 214    (hBudget : edgeOnlyEuler + (requiredDelta : ℤ) = regularBoundaryCWEuler B) :
 215    HalfVertexQuotientCloses B edgeOnlyEuler Cs := by
 216  unfold HalfVertexQuotientCloses halfVertexCorrectedEuler
 217  rw [hDelta]
 218  exact hBudget
 219
 220/-- Singular component with two vertices and one singular edge. -/
 221def singularV2E1 : SingularGraphComponent :=
 222  { vertices := 2, edges := 1 }
 223
 224/-- Singular component with four vertices and three singular edges. -/
 225def singularV4E3 : SingularGraphComponent :=
 226  { vertices := 4, edges := 3 }
 227
 228/-! ## Phase 34/35: corrected component assembly. -/
 229
 230/-- One connected component of the corrected boundary after edge pairing and local vertex-link
 231collapse. The component is represented only by its Euler characteristic. -/
 232structure CorrectedBoundaryComponent where
 233  euler : ℤ
 234deriving Repr, DecidableEq
 235
 236/-- Number of corrected boundary components. -/
 237def correctedComponentCount (Cs : List CorrectedBoundaryComponent) : ℤ :=
 238  Cs.length
 239
 240/-- Total Euler characteristic over corrected boundary components. -/
 241def correctedComponentEuler (Cs : List CorrectedBoundaryComponent) : ℤ :=
 242  (Cs.map CorrectedBoundaryComponent.euler).sum
 243
 244/-- Genus total read from component count and a supplied half-Euler value. The half-Euler is kept
 245explicit to avoid hiding the doubled-boundary theorem behind integer division. -/
 246def correctedComponentGenusFromHalfEuler (Cs : List CorrectedBoundaryComponent) (halfEuler : ℤ) : ℤ :=
 247  correctedComponentCount Cs - halfEuler
 248
 249/-- A corrected component list has the regular-neighborhood component assembly data for a region. -/
 250def ComponentAssemblyCloses (B : BettiTriple) (Cs : List CorrectedBoundaryComponent)
 251    (halfEuler : ℤ) : Prop :=
 252  correctedComponentCount Cs = regularBoundaryComponents B ∧
 253  correctedComponentEuler Cs = 2 * halfEuler ∧
 254  halfEuler = regionEuler B
 255
 256/-- Algebraic bridge for Phase 34: once the corrected component count and Euler half-sum match the
 257regular-neighborhood data, the total component genus is exactly `b₁`. -/
 258theorem correctedComponentGenus_eq_b1_of_componentAssemblyCloses
 259    (B : BettiTriple) (Cs : List CorrectedBoundaryComponent) (halfEuler : ℤ)
 260    (h : ComponentAssemblyCloses B Cs halfEuler) :
 261    correctedComponentGenusFromHalfEuler Cs halfEuler = B.b1 := by
 262  rcases h with ⟨hCount, _hEuler, hHalf⟩
 263  unfold correctedComponentGenusFromHalfEuler
 264  rw [hCount, hHalf]
 265  exact components_minus_regionEuler_eq_b1 B
 266
 267/-- A sphere component has Euler characteristic two. -/
 268def sphereComponent : CorrectedBoundaryComponent :=
 269  { euler := 2 }
 270
 271/-- A torus component has Euler characteristic zero. -/
 272def torusComponent : CorrectedBoundaryComponent :=
 273  { euler := 0 }
 274
 275/-- The dyadic probe's large corrected component has Euler characteristic `-248`, i.e. genus `125`
 276when it is closed and orientable. -/
 277def genus125Component : CorrectedBoundaryComponent :=
 278  { euler := -248 }
 279
 280/-- Phase-34 corrected components for the horizon-annulus target: one torus plus one sphere. -/
 281def horizonAnnulusHandleCorrectedComponents : List CorrectedBoundaryComponent :=
 282  [torusComponent, sphereComponent]
 283
 284/-- Phase-34 corrected components for the dyadic sponge: one genus-125 component plus 52 spheres. -/
 285def dyadicSpongeR20CorrectedComponents : List CorrectedBoundaryComponent :=
 286  [genus125Component] ++ List.replicate 52 sphereComponent
 287
 288/-! ## Phase 36/37: finite polygon-gluing surface witness. -/
 289
 290/-- One polygon-glued surface component from Phase 36. The fields record the quotient vertex count,
 291split-edge count, face count, Euler count, and local vertex-link audit. -/
 292structure PolygonGluingComponent where
 293  vertices : ℤ
 294  edges : ℤ
 295  faces : ℤ
 296  euler : ℤ
 297  vertexLinks : ℕ
 298  vertexLinkCycles : ℕ
 299deriving Repr, DecidableEq
 300
 301/-- The component's cell counts compute the recorded Euler characteristic. -/
 302def PolygonComponentEulerOk (C : PolygonGluingComponent) : Prop :=
 303  C.vertices - C.edges + C.faces = C.euler
 304
 305/-- Every quotient vertex has a single cyclic link. -/
 306def PolygonComponentLinksCyclic (C : PolygonGluingComponent) : Prop :=
 307  C.vertexLinkCycles = C.vertexLinks
 308
 309/-- Forget the polygon-level audit down to the corrected-boundary component used in Phase 35. -/
 310def polygonComponentToCorrected (C : PolygonGluingComponent) : CorrectedBoundaryComponent :=
 311  { euler := C.euler }
 312
 313/-- Forget a list of polygon-glued components to its Euler-only corrected-component list. -/
 314def polygonComponentsToCorrected (Cs : List PolygonGluingComponent) : List CorrectedBoundaryComponent :=
 315  Cs.map polygonComponentToCorrected
 316
 317/-- A finite polygon-gluing witness closes when all component cell Euler counts are correct, all
 318quotient vertex links are cyclic, and the forgotten Euler data closes the Phase-35 assembly. -/
 319def PolygonGluingCloses (B : BettiTriple) (Cs : List PolygonGluingComponent)
 320    (halfEuler : ℤ) : Prop :=
 321  (∀ C ∈ Cs, PolygonComponentEulerOk C) ∧
 322  (∀ C ∈ Cs, PolygonComponentLinksCyclic C) ∧
 323  ComponentAssemblyCloses B (polygonComponentsToCorrected Cs) halfEuler
 324
 325/-- Algebraic bridge for Phase 36: polygon gluing with valid Euler counts and cyclic vertex links
 326inherits the Phase-35 total-genus theorem. -/
 327theorem polygonGluedGenus_eq_b1_of_polygonGluingCloses
 328    (B : BettiTriple) (Cs : List PolygonGluingComponent) (halfEuler : ℤ)
 329    (h : PolygonGluingCloses B Cs halfEuler) :
 330    correctedComponentGenusFromHalfEuler (polygonComponentsToCorrected Cs) halfEuler = B.b1 := by
 331  rcases h with ⟨_hEuler, _hLinks, hAssembly⟩
 332  exact correctedComponentGenus_eq_b1_of_componentAssemblyCloses B
 333    (polygonComponentsToCorrected Cs) halfEuler hAssembly
 334
 335/-- The polygon-glued torus component from Phase 36 horizon `R = 20`. -/
 336def horizonPolygonTorusComponent : PolygonGluingComponent :=
 337  { vertices := 1632, edges := 3264, faces := 1632, euler := 0,
 338    vertexLinks := 1632, vertexLinkCycles := 1632 }
 339
 340/-- The polygon-glued sphere component from Phase 36 horizon `R = 20`. -/
 341def horizonPolygonSphereComponent : PolygonGluingComponent :=
 342  { vertices := 2484, edges := 4964, faces := 2482, euler := 2,
 343    vertexLinks := 2484, vertexLinkCycles := 2484 }
 344
 345/-- The Phase-36 horizon polygon-gluing components. -/
 346def horizonAnnulusHandlePolygonComponents : List PolygonGluingComponent :=
 347  [horizonPolygonTorusComponent, horizonPolygonSphereComponent]
 348
 349/-- The large genus-125 component from the Phase-36 dyadic polygon gluing. -/
 350def dyadicPolygonGenus125Component : PolygonGluingComponent :=
 351  { vertices := 8740, edges := 17976, faces := 8988, euler := -248,
 352    vertexLinks := 8740, vertexLinkCycles := 8740 }
 353
 354/-- A six-face cube-sphere component in the dyadic Phase-36 polygon gluing. -/
 355def dyadicPolygonSmallSphereComponent : PolygonGluingComponent :=
 356  { vertices := 8, edges := 12, faces := 6, euler := 2,
 357    vertexLinks := 8, vertexLinkCycles := 8 }
 358
 359/-- A twenty-two-face sphere component in the dyadic Phase-36 polygon gluing. -/
 360def dyadicPolygonMediumSphereComponent : PolygonGluingComponent :=
 361  { vertices := 24, edges := 44, faces := 22, euler := 2,
 362    vertexLinks := 24, vertexLinkCycles := 24 }
 363
 364/-- A thirty-face sphere component in the dyadic Phase-36 polygon gluing. -/
 365def dyadicPolygonLargeSphereComponent : PolygonGluingComponent :=
 366  { vertices := 32, edges := 60, faces := 30, euler := 2,
 367    vertexLinks := 32, vertexLinkCycles := 32 }
 368
 369/-- The Phase-36 dyadic polygon-gluing components: one genus-125 component, 48 small spheres, 3
 370medium spheres, and 1 large sphere. -/
 371def dyadicSpongeR20PolygonComponents : List PolygonGluingComponent :=
 372  [dyadicPolygonGenus125Component] ++
 373    List.replicate 48 dyadicPolygonSmallSphereComponent ++
 374    List.replicate 3 dyadicPolygonMediumSphereComponent ++
 375    [dyadicPolygonLargeSphereComponent]
 376
 377/-! ## Phase 38/39: orientability witness over polygon gluing. -/
 378
 379/-- One oriented polygon-gluing component from Phase 38. The `polygon` field carries the cell and
 380link audit from Phase 36; `facesAssigned` and `orientationContradictions` record the face-sign
 381constraint solve. -/
 382structure OrientedPolygonGluingComponent where
 383  polygon : PolygonGluingComponent
 384  facesAssigned : ℤ
 385  orientationContradictions : ℕ
 386deriving Repr, DecidableEq
 387
 388/-- The orientation solver succeeds on a polygon component when it assigns every face and finds no
 389sign contradiction. -/
 390def OrientedPolygonComponentOk (C : OrientedPolygonGluingComponent) : Prop :=
 391  C.facesAssigned = C.polygon.faces ∧ C.orientationContradictions = 0
 392
 393/-- Forget the orientability audit down to the Phase-36 polygon component. -/
 394def orientedPolygonToPolygon (C : OrientedPolygonGluingComponent) : PolygonGluingComponent :=
 395  C.polygon
 396
 397/-- Forget an oriented polygon component list to its polygon-gluing component list. -/
 398def orientedPolygonsToPolygons (Cs : List OrientedPolygonGluingComponent) :
 399    List PolygonGluingComponent :=
 400  Cs.map orientedPolygonToPolygon
 401
 402/-- An oriented polygon-gluing witness closes when all orientation solves succeed and the forgotten
 403polygon components close the Phase-37 polygon-gluing bridge. -/
 404def OrientedPolygonGluingCloses (B : BettiTriple)
 405    (Cs : List OrientedPolygonGluingComponent) (halfEuler : ℤ) : Prop :=
 406  (∀ C ∈ Cs, OrientedPolygonComponentOk C) ∧
 407  PolygonGluingCloses B (orientedPolygonsToPolygons Cs) halfEuler
 408
 409/-- Algebraic bridge for Phase 38: once the orientability audit succeeds, the oriented
 410polygon-gluing witness inherits the Phase-37 total-genus theorem. -/
 411theorem orientedPolygonGluedGenus_eq_b1_of_orientedPolygonGluingCloses
 412    (B : BettiTriple) (Cs : List OrientedPolygonGluingComponent) (halfEuler : ℤ)
 413    (h : OrientedPolygonGluingCloses B Cs halfEuler) :
 414    correctedComponentGenusFromHalfEuler
 415      (polygonComponentsToCorrected (orientedPolygonsToPolygons Cs)) halfEuler = B.b1 := by
 416  rcases h with ⟨_hOrient, hPolygon⟩
 417  exact polygonGluedGenus_eq_b1_of_polygonGluingCloses B
 418    (orientedPolygonsToPolygons Cs) halfEuler hPolygon
 419
 420/-- Oriented horizon torus component from Phase 38. -/
 421def horizonOrientedTorusComponent : OrientedPolygonGluingComponent :=
 422  { polygon := horizonPolygonTorusComponent, facesAssigned := 1632,
 423    orientationContradictions := 0 }
 424
 425/-- Oriented horizon sphere component from Phase 38. -/
 426def horizonOrientedSphereComponent : OrientedPolygonGluingComponent :=
 427  { polygon := horizonPolygonSphereComponent, facesAssigned := 2482,
 428    orientationContradictions := 0 }
 429
 430/-- Phase-38 oriented horizon polygon components. -/
 431def horizonAnnulusHandleOrientedPolygonComponents : List OrientedPolygonGluingComponent :=
 432  [horizonOrientedTorusComponent, horizonOrientedSphereComponent]
 433
 434/-- Oriented dyadic genus-125 polygon component from Phase 38. -/
 435def dyadicOrientedGenus125Component : OrientedPolygonGluingComponent :=
 436  { polygon := dyadicPolygonGenus125Component, facesAssigned := 8988,
 437    orientationContradictions := 0 }
 438
 439/-- Oriented dyadic six-face sphere component from Phase 38. -/
 440def dyadicOrientedSmallSphereComponent : OrientedPolygonGluingComponent :=
 441  { polygon := dyadicPolygonSmallSphereComponent, facesAssigned := 6,
 442    orientationContradictions := 0 }
 443
 444/-- Oriented dyadic twenty-two-face sphere component from Phase 38. -/
 445def dyadicOrientedMediumSphereComponent : OrientedPolygonGluingComponent :=
 446  { polygon := dyadicPolygonMediumSphereComponent, facesAssigned := 22,
 447    orientationContradictions := 0 }
 448
 449/-- Oriented dyadic thirty-face sphere component from Phase 38. -/
 450def dyadicOrientedLargeSphereComponent : OrientedPolygonGluingComponent :=
 451  { polygon := dyadicPolygonLargeSphereComponent, facesAssigned := 30,
 452    orientationContradictions := 0 }
 453
 454/-- Phase-38 oriented dyadic polygon components. -/
 455def dyadicSpongeR20OrientedPolygonComponents : List OrientedPolygonGluingComponent :=
 456  [dyadicOrientedGenus125Component] ++
 457    List.replicate 48 dyadicOrientedSmallSphereComponent ++
 458    List.replicate 3 dyadicOrientedMediumSphereComponent ++
 459    [dyadicOrientedLargeSphereComponent]
 460
 461/-! ## Phase 40: standard oriented surface classification. -/
 462
 463/-- The standard closed orientable surface classified by its genus. -/
 464structure StandardSurfaceType where
 465  genus : ℤ
 466deriving Repr, DecidableEq
 467
 468/-- Euler characteristic of a standard closed orientable surface of genus `g`: `2 - 2g`. -/
 469def standardSurfaceEuler (S : StandardSurfaceType) : ℤ :=
 470  2 - 2 * S.genus
 471
 472/-- A polygon component has a standard surface type when its Euler characteristic matches the
 473standard orientable formula and its orientation certificate succeeds. -/
 474def PolygonComponentHasSurfaceType
 475    (C : OrientedPolygonGluingComponent) (S : StandardSurfaceType) : Prop :=
 476  OrientedPolygonComponentOk C ∧ C.polygon.euler = standardSurfaceEuler S
 477
 478/-- Total genus across a list of standard surface types. -/
 479def surfaceTypeGenusTotal (Ss : List StandardSurfaceType) : ℤ :=
 480  (Ss.map StandardSurfaceType.genus).sum
 481
 482/-- Number of assigned standard surface types, read as an integer for Euler algebra. -/
 483def surfaceTypeCount (Ss : List StandardSurfaceType) : ℤ :=
 484  Ss.length
 485
 486/-- Total Euler characteristic across the assigned standard surface types. -/
 487def surfaceTypeEulerTotal (Ss : List StandardSurfaceType) : ℤ :=
 488  (Ss.map standardSurfaceEuler).sum
 489
 490/-- Ordered Euler signature of the oriented polygon components. -/
 491def orientedPolygonEulerList (Cs : List OrientedPolygonGluingComponent) : List ℤ :=
 492  Cs.map (fun C => C.polygon.euler)
 493
 494/-- Ordered Euler signature of the assigned standard surface types. -/
 495def surfaceTypeEulerList (Ss : List StandardSurfaceType) : List ℤ :=
 496  Ss.map standardSurfaceEuler
 497
 498/-- Total Euler characteristic of the oriented polygon components. -/
 499def orientedPolygonEulerTotal (Cs : List OrientedPolygonGluingComponent) : ℤ :=
 500  (orientedPolygonEulerList Cs).sum
 501
 502/-- A list of standard closed orientable surfaces has total Euler characteristic
 503`2 * component_count - 2 * total_genus`. -/
 504theorem surfaceTypeEulerTotal_eq_count_genus (Ss : List StandardSurfaceType) :
 505    surfaceTypeEulerTotal Ss = 2 * surfaceTypeCount Ss - 2 * surfaceTypeGenusTotal Ss := by
 506  induction Ss with
 507  | nil =>
 508      unfold surfaceTypeEulerTotal surfaceTypeCount surfaceTypeGenusTotal
 509      norm_num
 510  | cons S rest ih =>
 511      unfold surfaceTypeEulerTotal surfaceTypeCount surfaceTypeGenusTotal at *
 512      simp [standardSurfaceEuler, ih]
 513      ring
 514
 515/-- Forgetting oriented polygons to corrected components preserves list length, written in integer
 516form for the inventory algebra. -/
 517theorem correctedComponentCount_orientedPolygons (Cs : List OrientedPolygonGluingComponent) :
 518    correctedComponentCount (polygonComponentsToCorrected (orientedPolygonsToPolygons Cs)) =
 519      Cs.length := by
 520  unfold correctedComponentCount polygonComponentsToCorrected orientedPolygonsToPolygons
 521    polygonComponentToCorrected orientedPolygonToPolygon
 522  simp
 523
 524/-- Standard-surface classification closes when the oriented polygon certificate closes, every
 525component is assigned the matching standard surface type, the type count matches the component
 526count, and the type-genus total equals `b₁`. -/
 527def SurfaceTypeClassificationCloses (B : BettiTriple)
 528    (Cs : List OrientedPolygonGluingComponent) (Ss : List StandardSurfaceType)
 529    (halfEuler : ℤ) : Prop :=
 530  OrientedPolygonGluingCloses B Cs halfEuler ∧
 531  surfaceTypeCount Ss = correctedComponentCount (polygonComponentsToCorrected (orientedPolygonsToPolygons Cs)) ∧
 532  (∀ P ∈ Cs.zip Ss, PolygonComponentHasSurfaceType P.1 P.2) ∧
 533  surfaceTypeGenusTotal Ss = B.b1
 534
 535/-- Algebraic bridge for Phase 40: once the oriented polygon components are classified by standard
 536surface type, the total standard genus is the region's `b₁`. -/
 537theorem surfaceTypeGenusTotal_eq_b1_of_surfaceTypeClassificationCloses
 538    (B : BettiTriple) (Cs : List OrientedPolygonGluingComponent)
 539    (Ss : List StandardSurfaceType) (halfEuler : ℤ)
 540    (h : SurfaceTypeClassificationCloses B Cs Ss halfEuler) :
 541    surfaceTypeGenusTotal Ss = B.b1 := by
 542  exact h.2.2.2
 543
 544/-- A closed standard-surface classification has the same number of assigned surface types as
 545oriented polygon components. -/
 546theorem surfaceType_length_eq_orientedPolygon_length_of_surfaceTypeClassificationCloses
 547    (B : BettiTriple) (Cs : List OrientedPolygonGluingComponent)
 548    (Ss : List StandardSurfaceType) (halfEuler : ℤ)
 549    (h : SurfaceTypeClassificationCloses B Cs Ss halfEuler) :
 550    Ss.length = Cs.length := by
 551  have hCount : surfaceTypeCount Ss =
 552      correctedComponentCount (polygonComponentsToCorrected (orientedPolygonsToPolygons Cs)) := h.2.1
 553  unfold surfaceTypeCount at hCount
 554  rw [correctedComponentCount_orientedPolygons] at hCount
 555  exact Int.ofNat.inj hCount
 556
 557/-- If every zipped component/type pair has matching Euler characteristic and the lists have equal
 558length, then the ordered polygon Euler signature equals the ordered standard-surface Euler
 559signature. -/
 560theorem orientedPolygonEulerList_eq_surfaceTypeEulerList_of_zip
 561    (Cs : List OrientedPolygonGluingComponent) (Ss : List StandardSurfaceType)
 562    (hLen : Cs.length = Ss.length)
 563    (hEach : ∀ P ∈ Cs.zip Ss, PolygonComponentHasSurfaceType P.1 P.2) :
 564    orientedPolygonEulerList Cs = surfaceTypeEulerList Ss := by
 565  induction Cs generalizing Ss with
 566  | nil =>
 567      cases Ss with
 568      | nil => rfl
 569      | cons S rest => simp at hLen
 570  | cons C Cs ih =>
 571      cases Ss with
 572      | nil => simp at hLen
 573      | cons S Ss =>
 574          have hHead : C.polygon.euler = standardSurfaceEuler S := by
 575            exact (hEach (C, S) (by simp)).2
 576          have hTailLen : Cs.length = Ss.length := by
 577            exact Nat.succ.inj hLen
 578          have hTailEach : ∀ P ∈ Cs.zip Ss, PolygonComponentHasSurfaceType P.1 P.2 := by
 579            intro P hP
 580            exact hEach P (by simp [hP])
 581          change C.polygon.euler :: orientedPolygonEulerList Cs =
 582            standardSurfaceEuler S :: surfaceTypeEulerList Ss
 583          rw [hHead, ih Ss hTailLen hTailEach]
 584
 585/-- Phase 42 componentwise bridge: a closed standard-surface classification gives the same ordered
 586Euler signature for the oriented polygon components and the assigned standard surfaces. -/
 587theorem orientedPolygonEulerList_eq_surfaceTypeEulerList_of_surfaceTypeClassificationCloses
 588    (B : BettiTriple) (Cs : List OrientedPolygonGluingComponent)
 589    (Ss : List StandardSurfaceType) (halfEuler : ℤ)
 590    (h : SurfaceTypeClassificationCloses B Cs Ss halfEuler) :
 591    orientedPolygonEulerList Cs = surfaceTypeEulerList Ss := by
 592  exact orientedPolygonEulerList_eq_surfaceTypeEulerList_of_zip Cs Ss
 593    (surfaceType_length_eq_orientedPolygon_length_of_surfaceTypeClassificationCloses
 594      B Cs Ss halfEuler h).symm h.2.2.1
 595
 596/-- The oriented polygon Euler total equals the standard-surface Euler total under a closed
 597classification. -/
 598theorem orientedPolygonEulerTotal_eq_surfaceTypeEulerTotal_of_surfaceTypeClassificationCloses
 599    (B : BettiTriple) (Cs : List OrientedPolygonGluingComponent)
 600    (Ss : List StandardSurfaceType) (halfEuler : ℤ)
 601    (h : SurfaceTypeClassificationCloses B Cs Ss halfEuler) :
 602    orientedPolygonEulerTotal Cs = surfaceTypeEulerTotal Ss := by
 603  unfold orientedPolygonEulerTotal surfaceTypeEulerTotal
 604  rw [orientedPolygonEulerList_eq_surfaceTypeEulerList_of_surfaceTypeClassificationCloses
 605    B Cs Ss halfEuler h]
 606  rfl
 607
 608/-- Phase 41 inventory bridge: a closed standard-surface classification has the same component
 609count as the regular-neighborhood boundary. -/
 610theorem surfaceTypeCount_eq_regularBoundaryComponents_of_surfaceTypeClassificationCloses
 611    (B : BettiTriple) (Cs : List OrientedPolygonGluingComponent)
 612    (Ss : List StandardSurfaceType) (halfEuler : ℤ)
 613    (h : SurfaceTypeClassificationCloses B Cs Ss halfEuler) :
 614    surfaceTypeCount Ss = regularBoundaryComponents B := by
 615  rcases h with ⟨hOrient, hCount, _hEach, _hGenus⟩
 616  rcases hOrient with ⟨_hOrientOk, hPolygon⟩
 617  rcases hPolygon with ⟨_hEuler, _hLinks, hAssembly⟩
 618  exact hCount.trans hAssembly.1
 619
 620/-- Phase 41 inventory bridge: the assigned standard-surface Euler total matches the canonical
 621regular-neighborhood boundary Euler characteristic. -/
 622theorem surfaceTypeEulerTotal_eq_regularBoundaryEuler_of_surfaceTypeClassificationCloses
 623    (B : BettiTriple) (Cs : List OrientedPolygonGluingComponent)
 624    (Ss : List StandardSurfaceType) (halfEuler : ℤ)
 625    (h : SurfaceTypeClassificationCloses B Cs Ss halfEuler) :
 626    surfaceTypeEulerTotal Ss = regularBoundaryEuler B := by
 627  have hCount := surfaceTypeCount_eq_regularBoundaryComponents_of_surfaceTypeClassificationCloses
 628    B Cs Ss halfEuler h
 629  have hGenus := surfaceTypeGenusTotal_eq_b1_of_surfaceTypeClassificationCloses
 630    B Cs Ss halfEuler h
 631  rw [surfaceTypeEulerTotal_eq_count_genus, hCount, hGenus]
 632  unfold regularBoundaryEuler regularBoundaryComponents regionEuler
 633  ring
 634
 635/-- Phase 41: the classified surface-type inventory matches the regular-neighborhood boundary
 636in component count, Euler characteristic, and total genus. -/
 637theorem surfaceTypeInventory_matches_regularBoundary_of_surfaceTypeClassificationCloses
 638    (B : BettiTriple) (Cs : List OrientedPolygonGluingComponent)
 639    (Ss : List StandardSurfaceType) (halfEuler : ℤ)
 640    (h : SurfaceTypeClassificationCloses B Cs Ss halfEuler) :
 641    surfaceTypeCount Ss = regularBoundaryComponents B ∧
 642    surfaceTypeEulerTotal Ss = regularBoundaryEuler B ∧
 643    surfaceTypeGenusTotal Ss = B.b1 :=
 644  ⟨surfaceTypeCount_eq_regularBoundaryComponents_of_surfaceTypeClassificationCloses
 645      B Cs Ss halfEuler h,
 646    surfaceTypeEulerTotal_eq_regularBoundaryEuler_of_surfaceTypeClassificationCloses
 647      B Cs Ss halfEuler h,
 648    surfaceTypeGenusTotal_eq_b1_of_surfaceTypeClassificationCloses B Cs Ss halfEuler h⟩
 649
 650/-- Phase 42: componentwise plus aggregate inventory matching. This is the strongest algebraic
 651surface-inventory statement in this file; the embedded homeomorphism remains the separate geometric
 652premise. -/
 653theorem componentwiseSurfaceInventory_matches_regularBoundary_of_surfaceTypeClassificationCloses
 654    (B : BettiTriple) (Cs : List OrientedPolygonGluingComponent)
 655    (Ss : List StandardSurfaceType) (halfEuler : ℤ)
 656    (h : SurfaceTypeClassificationCloses B Cs Ss halfEuler) :
 657    orientedPolygonEulerList Cs = surfaceTypeEulerList Ss ∧
 658    orientedPolygonEulerTotal Cs = regularBoundaryEuler B ∧
 659    surfaceTypeCount Ss = regularBoundaryComponents B ∧
 660    surfaceTypeGenusTotal Ss = B.b1 := by
 661  have hList := orientedPolygonEulerList_eq_surfaceTypeEulerList_of_surfaceTypeClassificationCloses
 662    B Cs Ss halfEuler h
 663  have hTotal := orientedPolygonEulerTotal_eq_surfaceTypeEulerTotal_of_surfaceTypeClassificationCloses
 664    B Cs Ss halfEuler h
 665  have hSurfaceEuler :=
 666    surfaceTypeEulerTotal_eq_regularBoundaryEuler_of_surfaceTypeClassificationCloses B Cs Ss halfEuler h
 667  exact ⟨hList, hTotal.trans hSurfaceEuler,
 668    surfaceTypeCount_eq_regularBoundaryComponents_of_surfaceTypeClassificationCloses B Cs Ss halfEuler h,
 669    surfaceTypeGenusTotal_eq_b1_of_surfaceTypeClassificationCloses B Cs Ss halfEuler h⟩
 670
 671/-! ## Phase 43: finite component pairing toward the embedded map. -/
 672
 673/-- A finite pairing between one corrected oriented polygon component and one standard
 674regular-boundary surface component. -/
 675abbrev ComponentPair : Type :=
 676  OrientedPolygonGluingComponent × StandardSurfaceType
 677
 678/-- The ordered component pairing used by the current certificates. The later geometric theorem
 679must replace this abstract pairing with an embedded map. -/
 680def componentPairing (Cs : List OrientedPolygonGluingComponent)
 681    (Ss : List StandardSurfaceType) : List ComponentPair :=
 682  Cs.zip Ss
 683
 684/-- A paired component is valid when the polygon orientation certificate succeeds and the polygon
 685Euler characteristic equals the target standard-surface Euler characteristic. -/
 686def ComponentPairOk (P : ComponentPair) : Prop :=
 687  OrientedPolygonComponentOk P.1 ∧ P.1.polygon.euler = standardSurfaceEuler P.2
 688
 689/-- The target genus carried by a component pairing. -/
 690def componentPairGenus (P : ComponentPair) : ℤ :=
 691  P.2.genus
 692
 693/-- Total target genus of a finite component pairing. -/
 694def componentPairingGenusTotal (Ps : List ComponentPair) : ℤ :=
 695  (Ps.map componentPairGenus).sum
 696
 697/-- Total target Euler characteristic of a finite component pairing. -/
 698def componentPairingEulerTotal (Ps : List ComponentPair) : ℤ :=
 699  (Ps.map (fun P => standardSurfaceEuler P.2)).sum
 700
 701/-- A component pairing closes when it comes from the standard-surface classification, every pair
 702is locally valid, and its regular-boundary inventory matches component count, Euler, and genus. -/
 703def ComponentPairingCloses (B : BettiTriple)
 704    (Cs : List OrientedPolygonGluingComponent) (Ss : List StandardSurfaceType)
 705    (halfEuler : ℤ) : Prop :=
 706  SurfaceTypeClassificationCloses B Cs Ss halfEuler ∧
 707  (∀ P ∈ componentPairing Cs Ss, ComponentPairOk P) ∧
 708  surfaceTypeCount Ss = regularBoundaryComponents B ∧
 709  componentPairingEulerTotal (componentPairing Cs Ss) = regularBoundaryEuler B ∧
 710  componentPairingGenusTotal (componentPairing Cs Ss) = B.b1
 711
 712/-- The genus total of the component pairing is the genus total of its target surface list when the
 713source and target lists have the same length. -/
 714theorem componentPairingGenusTotal_eq_surfaceTypeGenusTotal
 715    (Cs : List OrientedPolygonGluingComponent) (Ss : List StandardSurfaceType)
 716    (hLen : Cs.length = Ss.length) :
 717    componentPairingGenusTotal (componentPairing Cs Ss) = surfaceTypeGenusTotal Ss := by
 718  induction Cs generalizing Ss with
 719  | nil =>
 720      cases Ss with
 721      | nil => rfl
 722      | cons S Ss => simp at hLen
 723  | cons C Cs ih =>
 724      cases Ss with
 725      | nil => simp at hLen
 726      | cons S Ss =>
 727          have hTailLen : Cs.length = Ss.length := Nat.succ.inj hLen
 728          change S.genus + componentPairingGenusTotal (componentPairing Cs Ss) =
 729            S.genus + surfaceTypeGenusTotal Ss
 730          rw [ih Ss hTailLen]
 731
 732/-- The Euler total of the component pairing is the Euler total of its target surface list when the
 733source and target lists have the same length. -/
 734theorem componentPairingEulerTotal_eq_surfaceTypeEulerTotal
 735    (Cs : List OrientedPolygonGluingComponent) (Ss : List StandardSurfaceType)
 736    (hLen : Cs.length = Ss.length) :
 737    componentPairingEulerTotal (componentPairing Cs Ss) = surfaceTypeEulerTotal Ss := by
 738  induction Cs generalizing Ss with
 739  | nil =>
 740      cases Ss with
 741      | nil => rfl
 742      | cons S Ss => simp at hLen
 743  | cons C Cs ih =>
 744      cases Ss with
 745      | nil => simp at hLen
 746      | cons S Ss =>
 747          have hTailLen : Cs.length = Ss.length := Nat.succ.inj hLen
 748          change standardSurfaceEuler S + componentPairingEulerTotal (componentPairing Cs Ss) =
 749            standardSurfaceEuler S + surfaceTypeEulerTotal Ss
 750          rw [ih Ss hTailLen]
 751
 752/-- Phase 43 pairing bridge: a closed standard-surface classification gives a closed finite
 753component pairing. This still does not construct the embedded homeomorphism. -/
 754theorem componentPairingCloses_of_surfaceTypeClassificationCloses
 755    (B : BettiTriple) (Cs : List OrientedPolygonGluingComponent)
 756    (Ss : List StandardSurfaceType) (halfEuler : ℤ)
 757    (h : SurfaceTypeClassificationCloses B Cs Ss halfEuler) :
 758    ComponentPairingCloses B Cs Ss halfEuler := by
 759  have hLen : Cs.length = Ss.length :=
 760    (surfaceType_length_eq_orientedPolygon_length_of_surfaceTypeClassificationCloses
 761      B Cs Ss halfEuler h).symm
 762  have hPairs : ∀ P ∈ componentPairing Cs Ss, ComponentPairOk P := by
 763    intro P hP
 764    exact h.2.2.1 P hP
 765  have hCount := surfaceTypeCount_eq_regularBoundaryComponents_of_surfaceTypeClassificationCloses
 766    B Cs Ss halfEuler h
 767  have hEuler : componentPairingEulerTotal (componentPairing Cs Ss) = regularBoundaryEuler B := by
 768    rw [componentPairingEulerTotal_eq_surfaceTypeEulerTotal Cs Ss hLen]
 769    exact surfaceTypeEulerTotal_eq_regularBoundaryEuler_of_surfaceTypeClassificationCloses
 770      B Cs Ss halfEuler h
 771  have hGenus : componentPairingGenusTotal (componentPairing Cs Ss) = B.b1 := by
 772    rw [componentPairingGenusTotal_eq_surfaceTypeGenusTotal Cs Ss hLen]
 773    exact surfaceTypeGenusTotal_eq_b1_of_surfaceTypeClassificationCloses B Cs Ss halfEuler h
 774  exact ⟨h, hPairs, hCount, hEuler, hGenus⟩
 775
 776/-! ## Phase 44: embedded component-map obligations. -/
 777
 778/-- A candidate embedded map from one corrected oriented polygon component to one standard
 779regular-boundary surface component.
 780
 781The four proposition fields are the geometric work still owed by the embedded theorem. They are
 782kept as obligations rather than booleans so this file cannot silently declare them true. -/
 783structure EmbeddedComponentMapObligation where
 784  source : OrientedPolygonGluingComponent
 785  target : StandardSurfaceType
 786  incidencePreserving : Prop
 787  quotientCellBijective : Prop
 788  vertexLinksPreserved : Prop
 789  orientationPreserving : Prop
 790
 791/-- Forget an embedded-map obligation to the Phase-43 component pair it is supposed to realize. -/
 792def embeddedComponentMapPair (M : EmbeddedComponentMapObligation) : ComponentPair :=
 793  (M.source, M.target)
 794
 795/-- The ordered list of component pairs carried by embedded-map obligations. -/
 796def embeddedComponentMapPairing (Ms : List EmbeddedComponentMapObligation) : List ComponentPair :=
 797  Ms.map embeddedComponentMapPair
 798
 799/-- A candidate embedded component map is locally valid exactly when the Phase-43 component pair is
 800valid and all four geometric map obligations are present. -/
 801def EmbeddedComponentMapObligationOk (M : EmbeddedComponentMapObligation) : Prop :=
 802  ComponentPairOk (embeddedComponentMapPair M) ∧
 803  M.incidencePreserving ∧
 804  M.quotientCellBijective ∧
 805  M.vertexLinksPreserved ∧
 806  M.orientationPreserving
 807
 808/-- Embedded-map obligations close when every candidate map satisfies the local geometric
 809obligations and the underlying Phase-43 component pairing closes. -/
 810def EmbeddedComponentMapObligationsClose (B : BettiTriple)
 811    (Ms : List EmbeddedComponentMapObligation) (halfEuler : ℤ) : Prop :=
 812  (∀ M ∈ Ms, EmbeddedComponentMapObligationOk M) ∧
 813  ComponentPairingCloses B
 814    (Ms.map EmbeddedComponentMapObligation.source)
 815    (Ms.map EmbeddedComponentMapObligation.target)
 816    halfEuler
 817
 818/-- The embedded-map obligation pairing is definitionally the component pairing between its source
 819and target lists. -/
 820theorem embeddedComponentMapPairing_eq_componentPairing
 821    (Ms : List EmbeddedComponentMapObligation) :
 822    embeddedComponentMapPairing Ms =
 823      componentPairing
 824        (Ms.map EmbeddedComponentMapObligation.source)
 825        (Ms.map EmbeddedComponentMapObligation.target) := by
 826  induction Ms with
 827  | nil => rfl
 828  | cons M Ms ih =>
 829      change embeddedComponentMapPair M :: embeddedComponentMapPairing Ms =
 830        embeddedComponentMapPair M ::
 831          componentPairing
 832            (Ms.map EmbeddedComponentMapObligation.source)
 833            (Ms.map EmbeddedComponentMapObligation.target)
 834      rw [ih]
 835
 836/-- Phase 44 reduction: if embedded component-map obligations close, the underlying finite
 837component pairing closes. The real embedded homeomorphism theorem must still prove the obligations
 838from geometry. -/
 839theorem componentPairingCloses_of_embeddedComponentMapObligationsClose
 840    (B : BettiTriple) (Ms : List EmbeddedComponentMapObligation) (halfEuler : ℤ)
 841    (h : EmbeddedComponentMapObligationsClose B Ms halfEuler) :
 842    ComponentPairingCloses B
 843      (Ms.map EmbeddedComponentMapObligation.source)
 844      (Ms.map EmbeddedComponentMapObligation.target)
 845      halfEuler := h.2
 846
 847/-- Phase 44 local readout: a closed embedded-map obligation package supplies every local
 848incidence, bijection, link, and orientation obligation for each candidate component map. -/
 849theorem embeddedComponentMapObligationOk_of_embeddedComponentMapObligationsClose
 850    (B : BettiTriple) (Ms : List EmbeddedComponentMapObligation) (halfEuler : ℤ)
 851    (h : EmbeddedComponentMapObligationsClose B Ms halfEuler)
 852    (M : EmbeddedComponentMapObligation) (hM : M ∈ Ms) :
 853    EmbeddedComponentMapObligationOk M := h.1 M hM
 854
 855/-- Phase 44 inventory readout: any closed embedded-map obligation package inherits the
 856regular-boundary Euler and genus inventory from its Phase-43 component pairing. -/
 857theorem embeddedComponentMapInventory_matches_regularBoundary
 858    (B : BettiTriple) (Ms : List EmbeddedComponentMapObligation) (halfEuler : ℤ)
 859    (h : EmbeddedComponentMapObligationsClose B Ms halfEuler) :
 860    componentPairingEulerTotal
 861        (componentPairing
 862          (Ms.map EmbeddedComponentMapObligation.source)
 863          (Ms.map EmbeddedComponentMapObligation.target)) = regularBoundaryEuler B ∧
 864    componentPairingGenusTotal
 865        (componentPairing
 866          (Ms.map EmbeddedComponentMapObligation.source)
 867          (Ms.map EmbeddedComponentMapObligation.target)) = B.b1 := by
 868  rcases h.2 with ⟨_hClass, _hPairs, _hCount, hEuler, hGenus⟩
 869  exact ⟨hEuler, hGenus⟩
 870
 871/-- The standard sphere. -/
 872def standardSphere : StandardSurfaceType :=
 873  { genus := 0 }
 874
 875/-- The standard torus. -/
 876def standardTorus : StandardSurfaceType :=
 877  { genus := 1 }
 878
 879/-- The standard closed orientable surface of genus `125`. -/
 880def standardGenus125Surface : StandardSurfaceType :=
 881  { genus := 125 }
 882
 883/-- Standard surface types for the horizon-annulus polygon components. -/
 884def horizonAnnulusHandleSurfaceTypes : List StandardSurfaceType :=
 885  [standardTorus, standardSphere]
 886
 887/-- Standard surface types for the dyadic sponge polygon components. -/
 888def dyadicSpongeR20SurfaceTypes : List StandardSurfaceType :=
 889  [standardGenus125Surface] ++ List.replicate 52 standardSphere
 890
 891/-! ## Numeric certificates for Phase 26/28/30 artifacts. -/
 892
 893/-- Phase-26 horizon-annulus handle at `R = 20` and `R = 32`: two components, one tunnel, no void. -/
 894def horizonAnnulusHandleBetti : BettiTriple :=
 895  { b0 := 2, b1 := 1, b2 := 0 }
 896
 897/-- The desingularized horizon-annulus boundary has two components. -/
 898theorem horizonAnnulusHandle_regularBoundaryComponents :
 899    regularBoundaryComponents horizonAnnulusHandleBetti = 2 := by
 900  native_decide
 901
 902/-- The desingularized horizon-annulus boundary has total genus one. -/
 903theorem horizonAnnulusHandle_regularBoundaryGenus :
 904    regularBoundaryGenus horizonAnnulusHandleBetti = 1 := by
 905  native_decide
 906
 907/-- The Phase-28 canonical CW boundary model of the horizon-annulus handle has Euler
 908characteristic `2`. -/
 909theorem horizonAnnulusHandle_regularBoundaryCWEuler :
 910    regularBoundaryCWEuler horizonAnnulusHandleBetti = 2 := by
 911  native_decide
 912
 913/-- Phase-30 singular-edge graph for the horizon-annulus target: `64` two-vertex components. -/
 914def horizonAnnulusHandleSingularComponents : List SingularGraphComponent :=
 915  List.replicate 64 singularV2E1
 916
 917/-- The horizon-annulus half-vertex quotient supplies exactly the missing `64` vertices. -/
 918theorem horizonAnnulusHandle_halfVertexDelta :
 919    singularGraphHalfVertexDelta horizonAnnulusHandleSingularComponents = 64 := by
 920  native_decide
 921
 922/-- The Phase-29 edge-only Euler count `-62`, corrected by the Phase-30 half-vertex delta `64`,
 923recovers the canonical CW Euler count `2`. -/
 924theorem horizonAnnulusHandle_halfVertexCorrectedEuler :
 925    halfVertexCorrectedEuler (-62) horizonAnnulusHandleSingularComponents =
 926      regularBoundaryCWEuler horizonAnnulusHandleBetti := by
 927  native_decide
 928
 929/-- The algebraic Phase-31 certificate: the half-vertex quotient closes the horizon-annulus CW Euler
 930budget under the recorded Phase-30 singular-component data. -/
 931theorem horizonAnnulusHandle_halfVertexQuotientCloses :
 932    HalfVertexQuotientCloses horizonAnnulusHandleBetti (-62)
 933      horizonAnnulusHandleSingularComponents := by
 934  unfold HalfVertexQuotientCloses
 935  native_decide
 936
 937/-- Phase-26 dyadic sponge probe at `R = 20`: `(b₀,b₁,b₂) = (50,125,3)`. -/
 938def dyadicSpongeR20Betti : BettiTriple :=
 939  { b0 := 50, b1 := 125, b2 := 3 }
 940
 941/-- The regular-neighborhood boundary of the dyadic sponge has `50 + 3 = 53` components. -/
 942theorem dyadicSpongeR20_regularBoundaryComponents :
 943    regularBoundaryComponents dyadicSpongeR20Betti = 53 := by
 944  native_decide
 945
 946/-- The regular-neighborhood boundary of the dyadic sponge has total genus `125`. -/
 947theorem dyadicSpongeR20_regularBoundaryGenus :
 948    regularBoundaryGenus dyadicSpongeR20Betti = 125 := by
 949  native_decide
 950
 951/-- The Phase-28 canonical CW boundary model of the dyadic sponge has Euler characteristic
 952`-144`, equal to `2 * (50 - 125 + 3)`. -/
 953theorem dyadicSpongeR20_regularBoundaryCWEuler :
 954    regularBoundaryCWEuler dyadicSpongeR20Betti = -144 := by
 955  native_decide
 956
 957/-- Phase-30 singular-edge graph for the dyadic sponge: `24` components of type `V2_E1` and
 958`21` components of type `V4_E3`. -/
 959def dyadicSpongeR20SingularComponents : List SingularGraphComponent :=
 960  List.replicate 24 singularV2E1 ++ List.replicate 21 singularV4E3
 961
 962/-- The dyadic sponge half-vertex quotient is `24*1 + 21*2 = 66`, exactly the required vertex
 963delta from Phase 30. -/
 964theorem dyadicSpongeR20_halfVertexDelta :
 965    singularGraphHalfVertexDelta dyadicSpongeR20SingularComponents = 66 := by
 966  native_decide
 967
 968/-- The Phase-29 dyadic edge-only Euler count `-210`, corrected by the Phase-30 half-vertex delta
 969`66`, recovers the canonical CW Euler count `-144`. -/
 970theorem dyadicSpongeR20_halfVertexCorrectedEuler :
 971    halfVertexCorrectedEuler (-210) dyadicSpongeR20SingularComponents =
 972      regularBoundaryCWEuler dyadicSpongeR20Betti := by
 973  native_decide
 974
 975/-- The algebraic Phase-31 certificate: the half-vertex quotient closes the dyadic-sponge CW Euler
 976budget under the recorded Phase-30 singular-component data. -/
 977theorem dyadicSpongeR20_halfVertexQuotientCloses :
 978    HalfVertexQuotientCloses dyadicSpongeR20Betti (-210)
 979      dyadicSpongeR20SingularComponents := by
 980  unfold HalfVertexQuotientCloses
 981  native_decide
 982
 983/-! ## Numeric certificates for Phase 34/35 component assembly. -/
 984
 985/-- The Phase-34 horizon component split has two components. -/
 986theorem horizonAnnulusHandle_correctedComponentCount :
 987    correctedComponentCount horizonAnnulusHandleCorrectedComponents =
 988      regularBoundaryComponents horizonAnnulusHandleBetti := by
 989  native_decide
 990
 991/-- The Phase-34 horizon component Euler sum is `2`, twice the region Euler half-sum `1`. -/
 992theorem horizonAnnulusHandle_correctedComponentEuler :
 993    correctedComponentEuler horizonAnnulusHandleCorrectedComponents = 2 * regionEuler horizonAnnulusHandleBetti := by
 994  native_decide
 995
 996/-- The Phase-35 algebraic certificate: the horizon component assembly closes. -/
 997theorem horizonAnnulusHandle_componentAssemblyCloses :
 998    ComponentAssemblyCloses horizonAnnulusHandleBetti horizonAnnulusHandleCorrectedComponents 1 := by
 999  unfold ComponentAssemblyCloses
1000  native_decide
1001
1002/-- The corrected horizon components have total genus one. -/
1003theorem horizonAnnulusHandle_correctedComponentGenus :
1004    correctedComponentGenusFromHalfEuler horizonAnnulusHandleCorrectedComponents 1 = 1 := by
1005  native_decide
1006
1007/-- The Phase-34 dyadic component split has `53` components. -/
1008theorem dyadicSpongeR20_correctedComponentCount :
1009    correctedComponentCount dyadicSpongeR20CorrectedComponents =
1010      regularBoundaryComponents dyadicSpongeR20Betti := by
1011  native_decide
1012
1013/-- The Phase-34 dyadic component Euler sum is `-144`, twice the region Euler half-sum `-72`. -/
1014theorem dyadicSpongeR20_correctedComponentEuler :
1015    correctedComponentEuler dyadicSpongeR20CorrectedComponents = 2 * regionEuler dyadicSpongeR20Betti := by
1016  native_decide
1017
1018/-- The Phase-35 algebraic certificate: the dyadic component assembly closes. -/
1019theorem dyadicSpongeR20_componentAssemblyCloses :
1020    ComponentAssemblyCloses dyadicSpongeR20Betti dyadicSpongeR20CorrectedComponents (-72) := by
1021  unfold ComponentAssemblyCloses
1022  native_decide
1023
1024/-- The corrected dyadic components have total genus `125`. -/
1025theorem dyadicSpongeR20_correctedComponentGenus :
1026    correctedComponentGenusFromHalfEuler dyadicSpongeR20CorrectedComponents (-72) = 125 := by
1027  native_decide
1028
1029/-! ## Numeric certificates for Phase 36/37 polygon gluing. -/
1030
1031/-- The Phase-36 horizon polygon components have the recorded Euler counts and cyclic vertex links,
1032and reduce to the Phase-35 horizon component assembly. -/
1033theorem horizonAnnulusHandle_polygonGluingCloses :
1034    PolygonGluingCloses horizonAnnulusHandleBetti horizonAnnulusHandlePolygonComponents 1 := by
1035  unfold PolygonGluingCloses ComponentAssemblyCloses PolygonComponentEulerOk
1036    PolygonComponentLinksCyclic polygonComponentsToCorrected polygonComponentToCorrected
1037    correctedComponentCount correctedComponentEuler regularBoundaryComponents regionEuler
1038  native_decide
1039
1040/-- The Phase-37 algebraic bridge reads total horizon genus one from the polygon-gluing witness. -/
1041theorem horizonAnnulusHandle_polygonGluedGenus :
1042    correctedComponentGenusFromHalfEuler
1043      (polygonComponentsToCorrected horizonAnnulusHandlePolygonComponents) 1 = 1 := by
1044  native_decide
1045
1046/-- The Phase-36 dyadic polygon components have the recorded Euler counts and cyclic vertex links,
1047and reduce to the Phase-35 dyadic component assembly. -/
1048theorem dyadicSpongeR20_polygonGluingCloses :
1049    PolygonGluingCloses dyadicSpongeR20Betti dyadicSpongeR20PolygonComponents (-72) := by
1050  unfold PolygonGluingCloses ComponentAssemblyCloses PolygonComponentEulerOk
1051    PolygonComponentLinksCyclic polygonComponentsToCorrected polygonComponentToCorrected
1052    correctedComponentCount correctedComponentEuler regularBoundaryComponents regionEuler
1053  native_decide
1054
1055/-- The Phase-37 algebraic bridge reads total dyadic genus `125` from the polygon-gluing witness. -/
1056theorem dyadicSpongeR20_polygonGluedGenus :
1057    correctedComponentGenusFromHalfEuler
1058      (polygonComponentsToCorrected dyadicSpongeR20PolygonComponents) (-72) = 125 := by
1059  native_decide
1060
1061/-! ## Numeric certificates for Phase 38/39 orientability. -/
1062
1063/-- The Phase-38 horizon orientation assignment covers every face with zero contradictions and
1064inherits the Phase-37 polygon-gluing closure. -/
1065theorem horizonAnnulusHandle_orientedPolygonGluingCloses :
1066    OrientedPolygonGluingCloses horizonAnnulusHandleBetti
1067      horizonAnnulusHandleOrientedPolygonComponents 1 := by
1068  unfold OrientedPolygonGluingCloses OrientedPolygonComponentOk PolygonGluingCloses
1069    ComponentAssemblyCloses PolygonComponentEulerOk PolygonComponentLinksCyclic
1070    orientedPolygonsToPolygons orientedPolygonToPolygon polygonComponentsToCorrected
1071    polygonComponentToCorrected correctedComponentCount correctedComponentEuler
1072    regularBoundaryComponents regionEuler
1073  native_decide
1074
1075/-- The oriented Phase-38 horizon polygon components read total genus one. -/
1076theorem horizonAnnulusHandle_orientedPolygonGluedGenus :
1077    correctedComponentGenusFromHalfEuler
1078      (polygonComponentsToCorrected
1079        (orientedPolygonsToPolygons horizonAnnulusHandleOrientedPolygonComponents)) 1 = 1 := by
1080  native_decide
1081
1082/-- The Phase-38 dyadic orientation assignment covers every face with zero contradictions and
1083inherits the Phase-37 polygon-gluing closure. -/
1084theorem dyadicSpongeR20_orientedPolygonGluingCloses :
1085    OrientedPolygonGluingCloses dyadicSpongeR20Betti
1086      dyadicSpongeR20OrientedPolygonComponents (-72) := by
1087  unfold OrientedPolygonGluingCloses OrientedPolygonComponentOk PolygonGluingCloses
1088    ComponentAssemblyCloses PolygonComponentEulerOk PolygonComponentLinksCyclic
1089    orientedPolygonsToPolygons orientedPolygonToPolygon polygonComponentsToCorrected
1090    polygonComponentToCorrected correctedComponentCount correctedComponentEuler
1091    regularBoundaryComponents regionEuler
1092  native_decide
1093
1094/-- The oriented Phase-38 dyadic polygon components read total genus `125`. -/
1095theorem dyadicSpongeR20_orientedPolygonGluedGenus :
1096    correctedComponentGenusFromHalfEuler
1097      (polygonComponentsToCorrected
1098        (orientedPolygonsToPolygons dyadicSpongeR20OrientedPolygonComponents)) (-72) = 125 := by
1099  native_decide
1100
1101/-! ## Numeric certificates for Phase 40 standard-surface classification. -/
1102
1103/-- The oriented Phase-38 horizon components classify as torus plus sphere. -/
1104theorem horizonAnnulusHandle_surfaceTypeClassificationCloses :
1105    SurfaceTypeClassificationCloses horizonAnnulusHandleBetti
1106      horizonAnnulusHandleOrientedPolygonComponents horizonAnnulusHandleSurfaceTypes 1 := by
1107  unfold SurfaceTypeClassificationCloses PolygonComponentHasSurfaceType
1108    OrientedPolygonGluingCloses OrientedPolygonComponentOk PolygonGluingCloses
1109    ComponentAssemblyCloses PolygonComponentEulerOk PolygonComponentLinksCyclic
1110    orientedPolygonsToPolygons orientedPolygonToPolygon polygonComponentsToCorrected
1111    polygonComponentToCorrected correctedComponentCount correctedComponentEuler
1112    regularBoundaryComponents regionEuler surfaceTypeGenusTotal standardSurfaceEuler
1113  native_decide
1114
1115/-- The standard-surface genus total for the horizon components is one. -/
1116theorem horizonAnnulusHandle_surfaceTypeGenusTotal :
1117    surfaceTypeGenusTotal horizonAnnulusHandleSurfaceTypes = 1 := by
1118  native_decide
1119
1120/-- Phase-42 horizon certificate: the ordered polygon Euler signature matches the ordered
1121standard-surface Euler signature, and the aggregate inventory matches the regular boundary. -/
1122theorem horizonAnnulusHandle_componentwiseSurfaceInventory :
1123    orientedPolygonEulerList horizonAnnulusHandleOrientedPolygonComponents =
1124      surfaceTypeEulerList horizonAnnulusHandleSurfaceTypes ∧
1125    orientedPolygonEulerTotal horizonAnnulusHandleOrientedPolygonComponents =
1126      regularBoundaryEuler horizonAnnulusHandleBetti ∧
1127    surfaceTypeCount horizonAnnulusHandleSurfaceTypes =
1128      regularBoundaryComponents horizonAnnulusHandleBetti ∧
1129    surfaceTypeGenusTotal horizonAnnulusHandleSurfaceTypes = horizonAnnulusHandleBetti.b1 := by
1130  exact componentwiseSurfaceInventory_matches_regularBoundary_of_surfaceTypeClassificationCloses
1131    horizonAnnulusHandleBetti horizonAnnulusHandleOrientedPolygonComponents
1132    horizonAnnulusHandleSurfaceTypes 1 horizonAnnulusHandle_surfaceTypeClassificationCloses
1133
1134/-- Phase-43 horizon certificate: the ordered torus/sphere component pairing closes. -/
1135theorem horizonAnnulusHandle_componentPairingCloses :
1136    ComponentPairingCloses horizonAnnulusHandleBetti
1137      horizonAnnulusHandleOrientedPolygonComponents horizonAnnulusHandleSurfaceTypes 1 := by
1138  exact componentPairingCloses_of_surfaceTypeClassificationCloses
1139    horizonAnnulusHandleBetti horizonAnnulusHandleOrientedPolygonComponents
1140    horizonAnnulusHandleSurfaceTypes 1 horizonAnnulusHandle_surfaceTypeClassificationCloses
1141
1142/-- The oriented Phase-38 dyadic components classify as one genus-125 surface plus 52 spheres. -/
1143theorem dyadicSpongeR20_surfaceTypeClassificationCloses :
1144    SurfaceTypeClassificationCloses dyadicSpongeR20Betti
1145      dyadicSpongeR20OrientedPolygonComponents dyadicSpongeR20SurfaceTypes (-72) := by
1146  unfold SurfaceTypeClassificationCloses PolygonComponentHasSurfaceType
1147    OrientedPolygonGluingCloses OrientedPolygonComponentOk PolygonGluingCloses
1148    ComponentAssemblyCloses PolygonComponentEulerOk PolygonComponentLinksCyclic
1149    orientedPolygonsToPolygons orientedPolygonToPolygon polygonComponentsToCorrected
1150    polygonComponentToCorrected correctedComponentCount correctedComponentEuler
1151    regularBoundaryComponents regionEuler surfaceTypeGenusTotal standardSurfaceEuler
1152  native_decide
1153
1154/-- The standard-surface genus total for the dyadic components is `125`. -/
1155theorem dyadicSpongeR20_surfaceTypeGenusTotal :
1156    surfaceTypeGenusTotal dyadicSpongeR20SurfaceTypes = 125 := by
1157  native_decide
1158
1159/-- Phase-42 dyadic certificate: the ordered polygon Euler signature matches the ordered
1160standard-surface Euler signature, and the aggregate inventory matches the regular boundary. -/
1161theorem dyadicSpongeR20_componentwiseSurfaceInventory :
1162    orientedPolygonEulerList dyadicSpongeR20OrientedPolygonComponents =
1163      surfaceTypeEulerList dyadicSpongeR20SurfaceTypes ∧
1164    orientedPolygonEulerTotal dyadicSpongeR20OrientedPolygonComponents =
1165      regularBoundaryEuler dyadicSpongeR20Betti ∧
1166    surfaceTypeCount dyadicSpongeR20SurfaceTypes =
1167      regularBoundaryComponents dyadicSpongeR20Betti ∧
1168    surfaceTypeGenusTotal dyadicSpongeR20SurfaceTypes = dyadicSpongeR20Betti.b1 := by
1169  exact componentwiseSurfaceInventory_matches_regularBoundary_of_surfaceTypeClassificationCloses
1170    dyadicSpongeR20Betti dyadicSpongeR20OrientedPolygonComponents
1171    dyadicSpongeR20SurfaceTypes (-72) dyadicSpongeR20_surfaceTypeClassificationCloses
1172
1173/-- Phase-43 dyadic certificate: the ordered genus-125-plus-spheres component pairing closes. -/
1174theorem dyadicSpongeR20_componentPairingCloses :
1175    ComponentPairingCloses dyadicSpongeR20Betti
1176      dyadicSpongeR20OrientedPolygonComponents dyadicSpongeR20SurfaceTypes (-72) := by
1177  exact componentPairingCloses_of_surfaceTypeClassificationCloses
1178    dyadicSpongeR20Betti dyadicSpongeR20OrientedPolygonComponents
1179    dyadicSpongeR20SurfaceTypes (-72) dyadicSpongeR20_surfaceTypeClassificationCloses
1180
1181/-- Old foam law obstruction from Phase 30: its half-vertex delta is strictly below the required
1182vertex budget, so the local target-class quotient cannot be promoted to a universal theorem. -/
1183theorem oldFoamR8_halfVertexDelta_lt_required : (28 : ℕ) < 788 := by
1184  native_decide
1185
1186/-- Old layered law obstruction from Phase 30: its half-vertex delta is strictly below the required
1187vertex budget, so those dust-law singularities remain a separate geometric problem. -/
1188theorem oldLayeredR8_halfVertexDelta_lt_required : (336 : ℕ) < 756 := by
1189  native_decide
1190
1191/-! ## Phase 46: concrete closed-orientable-surface obligations.
1192
1193Phase 44 carried the four embedded-map obligations as opaque `Prop` fields, so an obligation package
1194could be satisfied by trivial propositions and the Phase-45 numeric content stayed in Python. Phase
119546 replaces those placeholders with concrete decidable combinatorial-surface conditions read from the
1196Phase-36 polygon quotient and the Phase-38 orientation solve, and proves the horizon and dyadic
1197targets satisfy them in Lean.
1198
1199The conditions are exactly the hypotheses of a closed connected orientable combinatorial surface of
1200genus `g`: every edge is shared by two quadrilateral faces (closed, no boundary), the cell counts
1201give the target Euler characteristic, every quotient vertex link is a single cycle (manifold points),
1202and the face-orientation solve succeeds (orientable). The remaining OPEN step is the classification of
1203closed surfaces, namely that a closed connected orientable combinatorial 2-manifold of genus `g` is
1204homeomorphic to the standard genus-`g` surface. That classification is not in Mathlib and is not
1205assumed here. -/
1206
1207/-- Closed quadrangulation: every surface edge is shared by exactly two quadrilateral faces, so the
1208four-edges-per-face incidence count `4 * faces` equals the two-faces-per-edge count `2 * edges`, that
1209is `edges = 2 * faces`. This is the combinatorial no-boundary condition. -/
1210def PolygonComponentClosedQuadrangulation (C : PolygonGluingComponent) : Prop :=
1211  C.edges = 2 * C.faces
1212
1213/-- A concrete combinatorial closed orientable surface witness on one oriented polygon component: the
1214cell counts give the recorded Euler characteristic, every quotient vertex link is a single cycle, the
1215face-orientation solve succeeds, and every edge is shared by exactly two faces. These are the
1216decidable replacements for the opaque Phase-44 obligation propositions. -/
1217def CombinatorialClosedOrientableSurface (C : OrientedPolygonGluingComponent) : Prop :=
1218  PolygonComponentEulerOk C.polygon ∧
1219  PolygonComponentLinksCyclic C.polygon ∧
1220  OrientedPolygonComponentOk C ∧
1221  PolygonComponentClosedQuadrangulation C.polygon
1222
1223/-- Build a Phase-44 embedded-map obligation whose four propositions are the concrete
1224closed-orientable-surface conditions instead of placeholders. -/
1225def concreteObligation (C : OrientedPolygonGluingComponent) (S : StandardSurfaceType) :
1226    EmbeddedComponentMapObligation :=
1227  { source := C
1228    target := S
1229    incidencePreserving := PolygonComponentClosedQuadrangulation C.polygon
1230    quotientCellBijective :=
1231      PolygonComponentEulerOk C.polygon ∧ C.polygon.euler = standardSurfaceEuler S
1232    vertexLinksPreserved := PolygonComponentLinksCyclic C.polygon
1233    orientationPreserving := OrientedPolygonComponentOk C }
1234
1235/-- The standard surface target is forced by the Euler characteristic: two standard surfaces with the
1236same Euler characteristic are equal. The classification target is therefore determined, not chosen. -/
1237theorem standardSurfaceType_unique_of_euler (S S' : StandardSurfaceType)
1238    (h : standardSurfaceEuler S = standardSurfaceEuler S') : S = S' := by
1239  have hgen : S.genus = S'.genus := by
1240    have h' := h
1241    unfold standardSurfaceEuler at h'
1242    omega
1243  cases S
1244  cases S'
1245  simp_all
1246
1247/-- Phase 46 local bridge: a concrete closed-orientable-surface witness together with the target Euler
1248match supplies every Phase-44 obligation for the concrete obligation, with no placeholder left. -/
1249theorem concreteObligationOk_of_surface (C : OrientedPolygonGluingComponent)
1250    (S : StandardSurfaceType) (hsurf : CombinatorialClosedOrientableSurface C)
1251    (heuler : C.polygon.euler = standardSurfaceEuler S) :
1252    EmbeddedComponentMapObligationOk (concreteObligation C S) := by
1253  rcases hsurf with ⟨hEuler, hLinks, hOrient, hClosed⟩
1254  exact ⟨⟨hOrient, heuler⟩, hClosed, ⟨hEuler, heuler⟩, hLinks, hOrient⟩
1255
1256/-- The concrete obligation list from zipped component and surface lists. -/
1257def concreteObligations (Cs : List OrientedPolygonGluingComponent)
1258    (Ss : List StandardSurfaceType) : List EmbeddedComponentMapObligation :=
1259  (Cs.zip Ss).map (fun P => concreteObligation P.1 P.2)
1260
1261/-- The concrete obligation sources recover the component list when the lists have equal length. -/
1262theorem concreteObligations_map_source (Cs : List OrientedPolygonGluingComponent)
1263    (Ss : List StandardSurfaceType) (hLen : Cs.length = Ss.length) :
1264    (concreteObligations Cs Ss).map EmbeddedComponentMapObligation.source = Cs := by
1265  induction Cs generalizing Ss with
1266  | nil => rfl
1267  | cons C Cs ih =>
1268      cases Ss with
1269      | nil => simp at hLen
1270      | cons S Ss =>
1271          have hTail : Cs.length = Ss.length := Nat.succ.inj hLen
1272          change C :: (concreteObligations Cs Ss).map EmbeddedComponentMapObligation.source
1273            = C :: Cs
1274          rw [ih Ss hTail]
1275
1276/-- The concrete obligation targets recover the surface list when the lists have equal length. -/
1277theorem concreteObligations_map_target (Cs : List OrientedPolygonGluingComponent)
1278    (Ss : List StandardSurfaceType) (hLen : Cs.length = Ss.length) :
1279    (concreteObligations Cs Ss).map EmbeddedComponentMapObligation.target = Ss := by
1280  induction Cs generalizing Ss with
1281  | nil =>
1282      cases Ss with
1283      | nil => rfl
1284      | cons S Ss => simp at hLen
1285  | cons C Cs ih =>
1286      cases Ss with
1287      | nil => simp at hLen
1288      | cons S Ss =>
1289          have hTail : Cs.length = Ss.length := Nat.succ.inj hLen
1290          change S :: (concreteObligations Cs Ss).map EmbeddedComponentMapObligation.target
1291            = S :: Ss
1292          rw [ih Ss hTail]
1293
1294/-- Phase 46 list bridge: when every paired component is a concrete closed orientable surface and the
1295underlying Phase-43 pairing closes, the concrete obligation package closes in the Phase-44 sense, with
1296no placeholder obligation. -/
1297theorem embeddedComponentMapObligationsClose_of_concrete
1298    (B : BettiTriple) (Cs : List OrientedPolygonGluingComponent)
1299    (Ss : List StandardSurfaceType) (halfEuler : ℤ) (hLen : Cs.length = Ss.length)
1300    (hSurf : ∀ P ∈ Cs.zip Ss, CombinatorialClosedOrientableSurface P.1)
1301    (hPair : ComponentPairingCloses B Cs Ss halfEuler) :
1302    EmbeddedComponentMapObligationsClose B (concreteObligations Cs Ss) halfEuler := by
1303  refine ⟨?_, ?_⟩
1304  · intro M hM
1305    rcases List.mem_map.1 hM with ⟨P, hP, rfl⟩
1306    have hsurf := hSurf P hP
1307    have hpair : ComponentPairOk P := hPair.2.1 P hP
1308    exact concreteObligationOk_of_surface P.1 P.2 hsurf hpair.2
1309  · rw [concreteObligations_map_source Cs Ss hLen,
1310      concreteObligations_map_target Cs Ss hLen]
1311    exact hPair
1312
1313/-- The horizon torus component is a concrete closed orientable surface. -/
1314theorem horizonOrientedTorus_combinatorialSurface :
1315    CombinatorialClosedOrientableSurface horizonOrientedTorusComponent := by
1316  unfold CombinatorialClosedOrientableSurface PolygonComponentEulerOk PolygonComponentLinksCyclic
1317    OrientedPolygonComponentOk PolygonComponentClosedQuadrangulation
1318  native_decide
1319
1320/-- The horizon sphere component is a concrete closed orientable surface. -/
1321theorem horizonOrientedSphere_combinatorialSurface :
1322    CombinatorialClosedOrientableSurface horizonOrientedSphereComponent := by
1323  unfold CombinatorialClosedOrientableSurface PolygonComponentEulerOk PolygonComponentLinksCyclic
1324    OrientedPolygonComponentOk PolygonComponentClosedQuadrangulation
1325  native_decide
1326
1327/-- The dyadic genus-125 component is a concrete closed orientable surface. -/
1328theorem dyadicOrientedGenus125_combinatorialSurface :
1329    CombinatorialClosedOrientableSurface dyadicOrientedGenus125Component := by
1330  unfold CombinatorialClosedOrientableSurface PolygonComponentEulerOk PolygonComponentLinksCyclic
1331    OrientedPolygonComponentOk PolygonComponentClosedQuadrangulation
1332  native_decide
1333
1334/-- The dyadic six-face sphere component is a concrete closed orientable surface. -/
1335theorem dyadicOrientedSmallSphere_combinatorialSurface :
1336    CombinatorialClosedOrientableSurface dyadicOrientedSmallSphereComponent := by
1337  unfold CombinatorialClosedOrientableSurface PolygonComponentEulerOk PolygonComponentLinksCyclic
1338    OrientedPolygonComponentOk PolygonComponentClosedQuadrangulation
1339  native_decide
1340
1341/-- The dyadic twenty-two-face sphere component is a concrete closed orientable surface. -/
1342theorem dyadicOrientedMediumSphere_combinatorialSurface :
1343    CombinatorialClosedOrientableSurface dyadicOrientedMediumSphereComponent := by
1344  unfold CombinatorialClosedOrientableSurface PolygonComponentEulerOk PolygonComponentLinksCyclic
1345    OrientedPolygonComponentOk PolygonComponentClosedQuadrangulation
1346  native_decide
1347
1348/-- The dyadic thirty-face sphere component is a concrete closed orientable surface. -/
1349theorem dyadicOrientedLargeSphere_combinatorialSurface :
1350    CombinatorialClosedOrientableSurface dyadicOrientedLargeSphereComponent := by
1351  unfold CombinatorialClosedOrientableSurface PolygonComponentEulerOk PolygonComponentLinksCyclic
1352    OrientedPolygonComponentOk PolygonComponentClosedQuadrangulation
1353  native_decide
1354
1355/-- Every horizon oriented polygon component is a concrete closed orientable surface. -/
1356theorem horizonAnnulusHandle_all_combinatorialSurface :
1357    ∀ C ∈ horizonAnnulusHandleOrientedPolygonComponents,
1358      CombinatorialClosedOrientableSurface C := by
1359  intro C hC
1360  simp only [horizonAnnulusHandleOrientedPolygonComponents, List.mem_cons,
1361    List.not_mem_nil, or_false] at hC
1362  rcases hC with rfl | rfl
1363  · exact horizonOrientedTorus_combinatorialSurface
1364  · exact horizonOrientedSphere_combinatorialSurface
1365
1366/-- Every dyadic-sponge oriented polygon component is a concrete closed orientable surface. -/
1367theorem dyadicSpongeR20_all_combinatorialSurface :
1368    ∀ C ∈ dyadicSpongeR20OrientedPolygonComponents,
1369      CombinatorialClosedOrientableSurface C := by
1370  intro C hC
1371  simp only [dyadicSpongeR20OrientedPolygonComponents, List.mem_append, List.mem_cons,
1372    List.mem_replicate, List.not_mem_nil, or_false] at hC
1373  rcases hC with ((rfl | ⟨_, rfl⟩) | ⟨_, rfl⟩) | rfl
1374  · exact dyadicOrientedGenus125_combinatorialSurface
1375  · exact dyadicOrientedSmallSphere_combinatorialSurface
1376  · exact dyadicOrientedMediumSphere_combinatorialSurface
1377  · exact dyadicOrientedLargeSphere_combinatorialSurface
1378
1379/-- The horizon torus Phase-44 obligation is concretely satisfied: each obligation field is backed by
1380the closed-orientable-surface witness rather than by a placeholder. -/
1381theorem horizonOrientedTorus_concreteObligationOk :
1382    EmbeddedComponentMapObligationOk
1383      (concreteObligation horizonOrientedTorusComponent standardTorus) :=
1384  concreteObligationOk_of_surface horizonOrientedTorusComponent standardTorus
1385    horizonOrientedTorus_combinatorialSurface (by native_decide)
1386
1387/-- Phase-46 horizon capstone: the torus-plus-sphere obligation package closes with concrete
1388closed-orientable-surface obligations, not Phase-44 placeholders. The embedded homeomorphism still
1389requires the classification of closed surfaces. -/
1390theorem horizonAnnulusHandle_concreteEmbeddedObligationsClose :
1391    EmbeddedComponentMapObligationsClose horizonAnnulusHandleBetti
1392      (concreteObligations horizonAnnulusHandleOrientedPolygonComponents
1393        horizonAnnulusHandleSurfaceTypes) 1 := by
1394  apply embeddedComponentMapObligationsClose_of_concrete
1395  · native_decide
1396  · intro P hP
1397    obtain ⟨c, s⟩ := P
1398    exact horizonAnnulusHandle_all_combinatorialSurface c (List.of_mem_zip hP).1
1399  · exact horizonAnnulusHandle_componentPairingCloses
1400
1401/-- Phase-46 dyadic capstone: the genus-125-plus-spheres obligation package closes with concrete
1402closed-orientable-surface obligations, not Phase-44 placeholders. The embedded homeomorphism still
1403requires the classification of closed surfaces. -/
1404theorem dyadicSpongeR20_concreteEmbeddedObligationsClose :
1405    EmbeddedComponentMapObligationsClose dyadicSpongeR20Betti
1406      (concreteObligations dyadicSpongeR20OrientedPolygonComponents
1407        dyadicSpongeR20SurfaceTypes) (-72) := by
1408  apply embeddedComponentMapObligationsClose_of_concrete
1409  · native_decide
1410  · intro P hP
1411    obtain ⟨c, s⟩ := P
1412    exact dyadicSpongeR20_all_combinatorialSurface c (List.of_mem_zip hP).1
1413  · exact dyadicSpongeR20_componentPairingCloses
1414
1415/-! ## Phase 47: conditional homeomorphism under the classification of closed surfaces.
1416
1417Phase 46 proved every target component is a concrete closed orientable combinatorial surface whose
1418Euler characteristic matches its standard surface. The only remaining step to a homeomorphism is the
1419classification of closed surfaces: a closed connected orientable combinatorial 2-manifold of genus `g`
1420is homeomorphic to the standard genus-`g` surface. That classical result is not in Mathlib.
1421
1422This phase makes the dependency explicit without assuming it as an axiom. It parameterizes over an
1423abstract realization relation `R` (read: the geometric realization of the component is homeomorphic to
1424the standard surface) and over the classification as a hypothesis on `R`. Every theorem below is a
1425CONDITIONAL THEOREM, conditional on the classification of closed surfaces, with no new axiom and no
1426placeholder. Once the classification ships for the recognition-foam realization, instantiating `R`
1427makes the conclusions unconditional. -/
1428
1429/-- The classification of closed surfaces, stated as a named hypothesis on an abstract realization
1430relation `R`. `R C S` reads "the geometric realization of the corrected polygon component `C` is
1431homeomorphic to the standard surface `S`." The hypothesis says every concrete closed orientable
1432combinatorial surface whose Euler characteristic matches a standard surface is realized by it. This is
1433the classical classification of closed surfaces, held here as an explicit hypothesis, never an axiom. -/
1434def ClosedSurfaceClassification
1435    (R : OrientedPolygonGluingComponent → StandardSurfaceType → Prop) : Prop :=
1436  ∀ (C : OrientedPolygonGluingComponent) (S : StandardSurfaceType),
1437    CombinatorialClosedOrientableSurface C → C.polygon.euler = standardSurfaceEuler S → R C S
1438
1439/-- Conditional homeomorphism, one component: under the classification of closed surfaces, a concrete
1440closed orientable combinatorial surface with the matching Euler characteristic is realized by its
1441standard surface. -/
1442theorem realizesStandard_of_surface
1443    (R : OrientedPolygonGluingComponent → StandardSurfaceType → Prop)
1444    (hClass : ClosedSurfaceClassification R)
1445    (C : OrientedPolygonGluingComponent) (S : StandardSurfaceType)
1446    (hsurf : CombinatorialClosedOrientableSurface C)
1447    (heuler : C.polygon.euler = standardSurfaceEuler S) :
1448    R C S :=
1449  hClass C S hsurf heuler
1450
1451/-- Conditional homeomorphism, whole package: under the classification of closed surfaces, every paired
1452component of a closed concrete obligation package is realized by its standard surface. The per-pair
1453Euler match is taken from the Phase-43 component pairing inside the closure. -/
1454theorem concreteObligations_realizeStandard
1455    (R : OrientedPolygonGluingComponent → StandardSurfaceType → Prop)
1456    (hClass : ClosedSurfaceClassification R)
1457    (B : BettiTriple) (Cs : List OrientedPolygonGluingComponent)
1458    (Ss : List StandardSurfaceType) (halfEuler : ℤ)
1459    (hSurf : ∀ P ∈ Cs.zip Ss, CombinatorialClosedOrientableSurface P.1)
1460    (hPair : ComponentPairingCloses B Cs Ss halfEuler) :
1461    ∀ P ∈ Cs.zip Ss, R P.1 P.2 := by
1462  intro P hP
1463  exact hClass P.1 P.2 (hSurf P hP) (hPair.2.1 P hP).2
1464
1465/-- Phase-47 horizon capstone (CONDITIONAL THEOREM): under the classification of closed surfaces, the
1466horizon regular-neighborhood boundary is realized component by component, the torus component by the
1467standard torus and the sphere component by the standard sphere. -/
1468theorem horizonAnnulusHandle_realizesStandard
1469    (R : OrientedPolygonGluingComponent → StandardSurfaceType → Prop)
1470    (hClass : ClosedSurfaceClassification R) :
1471    R horizonOrientedTorusComponent standardTorus ∧
1472      R horizonOrientedSphereComponent standardSphere :=
1473  ⟨hClass _ _ horizonOrientedTorus_combinatorialSurface (by native_decide),
1474   hClass _ _ horizonOrientedSphere_combinatorialSurface (by native_decide)⟩
1475
1476/-- Phase-47 dyadic capstone (CONDITIONAL THEOREM): under the classification of closed surfaces, every
1477component of the dyadic-sponge regular-neighborhood boundary is realized by its standard surface (one
1478genus-125 surface and 52 spheres). -/
1479theorem dyadicSpongeR20_realizesStandard
1480    (R : OrientedPolygonGluingComponent → StandardSurfaceType → Prop)
1481    (hClass : ClosedSurfaceClassification R) :
1482    ∀ P ∈ dyadicSpongeR20OrientedPolygonComponents.zip dyadicSpongeR20SurfaceTypes, R P.1 P.2 :=
1483  concreteObligations_realizeStandard R hClass dyadicSpongeR20Betti
1484    dyadicSpongeR20OrientedPolygonComponents dyadicSpongeR20SurfaceTypes (-72)
1485    (by
1486      intro P hP
1487      obtain ⟨c, s⟩ := P
1488      exact dyadicSpongeR20_all_combinatorialSurface c (List.of_mem_zip hP).1)
1489    dyadicSpongeR20_componentPairingCloses
1490
1491end RegularNeighborhoodBoundary
1492end Cosmology
1493end IndisputableMonolith
1494