Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.FiniteCellBoundary

show as:
view Lean formalization →

Defines finite spatial cells for Recognition cosmology: a periodic 1D ring on Fin n with wrap-around posting, plus open patches and bounded voxels. Cosmology arguments that need a discrete torus or a finite support window cite these types. The module is mostly structure and positivity lemmas, not a deep proof chain.

claimA periodic one-dimensional ring is the finite site set $\mathrm{Fin}\, n$ ($n > 0$) with wrap-around neighbor posting. Companion objects are open patches and bounded voxels used as finite support windows on the discrete lattice.

background

Recognition cosmology works on discrete recognition lattices rather than continuum manifolds. Finite-cell models replace infinite spatial slices by compact discrete domains so that posting, flux, and boundary terms stay well-defined and summable.

The central object is a periodic 1D ring: sites indexed by $\mathrm{Fin}, n$ with modular (wrap) adjacency. Open patches and bounded voxels supply non-periodic finite windows when a full torus is too strong. The only external import is Mathlib; positivity of the ring length is recorded as a small lemma on $n$.

proof idea

This is a definition module. It introduces the ring, patch, and voxel structures, together with a short positivity fact that the ring cardinality is positive. There is no multi-step forcing or analytic argument here.

why it matters in Recognition Science

Finite cells are the discrete stage on which Recognition cosmology states local conservation, boundary flux, and eight-tick scheduling without continuum limits. Downstream cosmology developments that need a compact spatial support or a periodic identification import these types. In the broader RS chain the constructions sit under the discrete geometry that accompanies T7 (eight-tick octave) and T8 ($D=3$), giving concrete finite models rather than continuum placeholders. No parent theorem is wired in the current graph edges; the module is infrastructure for later cosmology claims.

scope and limits

declarations in this module (4)