IndisputableMonolith.Cosmology.FiniteCellBoundary

   1import Mathlib
   2
   3/-!
   4# Finite recognition cell boundary commitments (engineering scaffold)
   5
   6Python exact cells in `scripts/cosmogenesis/cell{1d,2d,3d,voxel}.py` mirror these boundary tags.
   7No new axioms; certificate targets for periodic ring and open patch serialization.
   8-/
   9
  10namespace IndisputableMonolith
  11namespace Cosmology
  12namespace FiniteCellBoundary
  13
  14/-- Periodic 1D ring: sites `Fin n` with wrap posting. -/
  15structure PeriodicRing (n : Nat) where
  16  n_pos : 0 < n
  17
  18/-- Open 2D patch: finite grid without wrap. -/
  19structure OpenPatch (nx ny : Nat) where
  20  nx_pos : 0 < nx
  21  ny_pos : 0 < ny
  22
  23/-- Bounded 3D voxel without wrap. -/
  24structure BoundedVoxel (nx ny nz : Nat) where
  25  nx_pos : 0 < nx
  26  ny_pos : 0 < ny
  27  nz_pos : 0 < nz
  28
  29theorem periodic_ring_n_pos {n : Nat} (c : PeriodicRing n) : 0 < n := c.n_pos
  30
  31end FiniteCellBoundary
  32end Cosmology
  33end IndisputableMonolith
  34