Cosmology Finite Cell Boundary

Finite cell boundaries

A finite cell boundary is a definitional choice about what happens at the edge of a discrete grid. In a periodic ring, the last site wraps around to the first, so no edge exists. In an open patch or a bounded voxel, the grid simply stops, and the boundary is a real limit. The distinction matters because a ledger that records recognition events, a discrete record of what happened where, must know whether an event at the edge can post to a neighbor on the other side or must stop.

The framework's machine-checked library of formal theorems defines three boundary shapes. A periodic 1D ring is a structure on a natural number n with a proof that n is positive, so the ring is never empty. An open 2D patch is a finite grid with positive width and height, no wrap. A bounded 3D voxel is the same idea in three dimensions, with all three side lengths positive. Each structure carries its positivity condition as part of its definition, so any use of the shape already knows the grid is nonempty.

One theorem is proved about these shapes: a periodic ring on n sites always has n greater than zero. That fact is already in the structure, but the theorem makes it available as a named result. The module is an engineering scaffold, not a physical derivation. It sets up the boundary vocabulary that simulation code mirrors, with exact Python cells in script files matching these tags. No new axioms are introduced, and the certificate targets are for periodic ring and open patch serialization.

In Recognition Science, the framework models a finite universe as a grid of cells where recognition events are posted. The boundary choice determines whether the universe is a closed loop or a bounded region. The module does not prove that any particular boundary is physical; it defines the options and their basic consistency conditions. The payoff is that any later theorem about cosmology can state its boundary assumption precisely, and a reader can check whether the result applies to a wrapped ring or an open patch.

/-- Periodic 1D ring: sites `Fin n` with wrap posting. -/
structure PeriodicRing (n : Nat) where
  n_pos : 0 < n

/-- Open 2D patch: finite grid without wrap. -/
structure OpenPatch (nx ny : Nat) where
  nx_pos : 0 < nx
  ny_pos : 0 < ny

/-- Bounded 3D voxel without wrap. -/
structure BoundedVoxel (nx ny nz : Nat) where
  nx_pos : 0 < nx
  ny_pos : 0 < ny
  nz_pos : 0 < nz

theorem periodic_ring_n_pos {n : Nat} (c : PeriodicRing n) : 0 < n := c.n_pos

What this page does not claim

No claim that any particular boundary condition is physically required. No claim that the module derives cosmology from first principles. No claim that the Python scripts are formally verified against the Lean structures.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/FiniteCellBoundary.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: