IndisputableMonolith.Cosmology.FiniteCellBoundary
Defines finite discrete geometries used as cell boundaries in RS cosmology: a periodic 1D ring on Fin n with wrap-around posting, open patches, and bounded voxels. Cosmology constructions that need compact or truncated spatial cells cite these types. The module is largely definitional scaffolding over Mathlib finite types.
claimA periodic 1D ring is the site set $\mathrm{Fin}\, n$ ($n > 0$) with wrap-around neighbor posting. The module also introduces open patches and bounded voxels as finite cell geometries for discrete cosmology.
background
Recognition Science cosmology works on discrete recognition cells rather than continuum manifolds. Spatial structure is carried by finite index sets so that posting, flux, and boundary terms stay combinatorial.
This module supplies the elementary geometries: a periodic ring whose sites are $\mathrm{Fin}, n$ with modular wrap, open patches (non-periodic local windows), and bounded voxels (finite boxes with explicit boundary). The positivity lemma $n > 0$ for the ring is the only nontrivial side condition needed to keep the finite type inhabited.
The setting is preparatory for cell-boundary bookkeeping in discrete FLRW-style or ledger-based cosmological models inside the monolith.
proof idea
This is primarily a definition module. Types and structures (periodic ring, open patch, bounded voxel) are introduced over Mathlib finite types; the sole named lemma asserts positivity of the ring cardinality so wrap arithmetic is well-defined. No deep forcing or RCL argument lives here.
why it matters in Recognition Science
Finite cell boundaries let cosmological constructions stay inside finite combinatorial data while still modeling periodic or truncated space. Downstream cosmology developments that assemble discrete spatial slices, boundary fluxes, or voxel ledgers depend on these geometries as the ambient site sets. The module does not itself force $D=3$ or the eight-tick structure; it only supplies the finite stages on which those global constraints can later act.
scope and limits
- Does not derive continuum GR or FLRW metrics from the finite cells.
- Does not force spatial dimension $D=3$ or the eight-tick octave.
- Does not prove dynamical evolution or matter content on the cells.
- Does not connect ring geometry to the J-cost or RCL identities.