module module moderate

`IndisputableMonolith.Cosmology.RegularNeighborhoodBoundary`

Defines integer Betti data and Euler quantities for a compact 3D region and its regular neighborhood boundary, so characteristic algebra stays exact. Cosmology and 3-manifold arguments that need genus, boundary components, or CW Euler numbers cite these. The module is mostly definitions plus a few equational lemmas equating genus to first Betti number and relating region and boundary Euler characteristics.

claimFor a compact 3D region, package Betti numbers as an integer triple $(b_0,b_1,b_2)$, define the region Euler characteristic, and for a regular neighborhood boundary define component count, Euler characteristic, genus, and CW counts (vertices, edges, faces) with Euler number. The module asserts $\chi(\partial)=2\chi(\mathrm{region})$, genus equals $b_1$ of the boundary, and the CW Euler number equals the topological boundary Euler number.

background

Recognition Science forces $D=3$ spatial dimensions (forcing chain T8), so compact spatial regions are 3-manifolds (or 3D complexes) whose topology enters cosmology bookkeeping. This module supplies the discrete topological ledger for such a region and for a regular neighborhood of its boundary.

The central object is an integer Betti triple so that Euler characteristic $\chi=b_0-b_1+b_2$ is literal integer arithmetic rather than a real-valued placeholder. From that one defines the region Euler number, then boundary-side quantities: number of regular boundary components, boundary Euler characteristic, genus, and a CW presentation (vertices, edges, faces) with its own Euler number.

The setting is pure combinatorial topology over Mathlib; no metric, curvature, or field equations appear here. The point is to keep genus and Euler identities available as exact equalities downstream in cosmology arguments that count handles, voids, or boundary sheets.

proof idea

Definition-heavy module. Betti triple, region Euler, boundary component count, boundary Euler, genus, and CW vertex/edge/face counts are introduced as data or simple formulas. Three equational results close the ledger: genus equals the first Betti number of the boundary; boundary Euler equals twice the region Euler; CW Euler equals the topological boundary Euler. Those are algebraic identities from the integer packaging, not deep existence proofs.

why it matters in Recognition Science

Gives cosmology code a single place for 3D region and regular-boundary topology in integer form, matching the RS insistence on $D=3$. Downstream cosmology developments that need handle counts, void counts, or boundary genus can quote the genus–$b_1$ match and the factor-of-two Euler relation without re-deriving classical 3-manifold identities. No parent theorems are wired in the graph yet; the module is infrastructure for later cosmology claims that consume regular-neighborhood boundary data.

scope and limits

Does not construct a geometric regular neighborhood in a Riemannian 3-manifold.
Does not prove existence or uniqueness of CW structures on the boundary.
Does not address noncompact, singular, or non-orientable regions.
Does not connect Betti data to curvature, stress-energy, or observational cosmology.
Does not import or cite upstream RS forcing lemmas beyond the ambient D=3 setting.

declarations in this module (176)

structure BettiTriple L91
def regionEuler L98
def regularBoundaryComponents L102
def regularBoundaryEuler L106
def regularBoundaryGenus L110
def regularBoundaryCWVertices L117
def regularBoundaryCWEdges L121
def regularBoundaryCWFaces L125
def regularBoundaryCWEuler L129
theorem regularBoundaryGenus_eq_b1 L135
theorem regularBoundaryEuler_eq_two_regionEuler L141
theorem regularBoundaryCWEuler_eq_regularBoundaryEuler L147
theorem regularBoundaryCWEuler_eq_two_regionEuler L154
theorem components_minus_regionEuler_eq_b1 L160
structure IsRegularBoundaryOf L166
theorem genus_eq_b1_of_isRegularBoundaryOf L175
structure SingularGraphComponent L184
def halfVertexComponentDelta L191
def singularGraphHalfVertexDelta L195
def halfVertexCorrectedEuler L199
def HalfVertexQuotientCloses L204
theorem halfVertexCorrectedEuler_eq_cw_of_delta_eq_required L210
def singularV2E1 L221
def singularV4E3 L225
structure CorrectedBoundaryComponent L232
def correctedComponentCount L237
def correctedComponentEuler L241
def correctedComponentGenusFromHalfEuler L246
def ComponentAssemblyCloses L250
theorem correctedComponentGenus_eq_b1_of_componentAssemblyCloses L258
def sphereComponent L268
def torusComponent L272
def genus125Component L277
def horizonAnnulusHandleCorrectedComponents L281
def dyadicSpongeR20CorrectedComponents L285
structure PolygonGluingComponent L292
def PolygonComponentEulerOk L302
def PolygonComponentLinksCyclic L306
def polygonComponentToCorrected L310
def polygonComponentsToCorrected L314
def PolygonGluingCloses L319
theorem polygonGluedGenus_eq_b1_of_polygonGluingCloses L327
def horizonPolygonTorusComponent L336
def horizonPolygonSphereComponent L341
def horizonAnnulusHandlePolygonComponents L346
def dyadicPolygonGenus125Component L350
def dyadicPolygonSmallSphereComponent L355
def dyadicPolygonMediumSphereComponent L360
def dyadicPolygonLargeSphereComponent L365
def dyadicSpongeR20PolygonComponents L371
structure OrientedPolygonGluingComponent L382
def OrientedPolygonComponentOk L390
def orientedPolygonToPolygon L394
def orientedPolygonsToPolygons L398
def OrientedPolygonGluingCloses L404
theorem orientedPolygonGluedGenus_eq_b1_of_orientedPolygonGluingCloses L411
def horizonOrientedTorusComponent L421
def horizonOrientedSphereComponent L426
def horizonAnnulusHandleOrientedPolygonComponents L431
def dyadicOrientedGenus125Component L435
def dyadicOrientedSmallSphereComponent L440
def dyadicOrientedMediumSphereComponent L445
def dyadicOrientedLargeSphereComponent L450
def dyadicSpongeR20OrientedPolygonComponents L455
structure StandardSurfaceType L464
def standardSurfaceEuler L469
def PolygonComponentHasSurfaceType L474
def surfaceTypeGenusTotal L479
def surfaceTypeCount L483
def surfaceTypeEulerTotal L487
def orientedPolygonEulerList L491
def surfaceTypeEulerList L495
def orientedPolygonEulerTotal L499
theorem surfaceTypeEulerTotal_eq_count_genus L504
theorem correctedComponentCount_orientedPolygons L517
def SurfaceTypeClassificationCloses L527
theorem surfaceTypeGenusTotal_eq_b1_of_surfaceTypeClassificationCloses L537
theorem surfaceType_length_eq_orientedPolygon_length_of_surfaceTypeClassificationCloses L546
theorem orientedPolygonEulerList_eq_surfaceTypeEulerList_of_zip L560
theorem orientedPolygonEulerList_eq_surfaceTypeEulerList_of_surfaceTypeClassificationCloses L587

… and 96 more