PeriodicRing
plain-language theorem explainer
A one-field certificate that a natural number n labels a periodic 1D recognition ring: n sites on Fin n with wrap-around posting, and n must be strictly positive. Cosmology cell-boundary and serialization code cites it as the Lean mirror of the Python 1D exact cell. There is no proof body; the structure itself is the commitment.
Claim. A periodic one-dimensional ring of size $n\in\mathbb{N}$ is a witness that $0<n$. Sites are the finite type with $n$ elements, and posting wraps around the ring.
background
The module records finite recognition cell boundary commitments as engineering scaffold. Python exact cells in the cosmogenesis scripts mirror these boundary tags; the Lean side supplies certificate targets for periodic ring and open patch serialization, with no new axioms.
A periodic 1D ring is the discrete circle of $n$ sites (type-theoretically Fin n) on which recognition posts wrap. The only datum required is positivity of $n$, so empty rings are excluded. Sibling tags cover the open 2D patch (finite grid without wrap) and bounded voxels; together they classify the cell geometries used in cosmogenesis.
Upstream dimension constants fix spatial $D=3$ via the forcing chain (T8), but this structure is dimension-agnostic: it only packages the 1D periodic boundary case.
proof idea
No proof. The declaration is a structure with a single field asserting $0<n$. Inhabitants are built by supplying that inequality; the downstream extractor simply projects the field.
why it matters
Gives the typed boundary tag for 1D periodic recognition cells so serialization and certificate pipelines can name the geometry without ad-hoc naturals. The immediate consumer is the field projection that recovers positivity from any such ring. In the broader Recognition picture this sits under the finite-cell engineering layer that supports eight-tick and $D=3$ forcing downstream, not as a step of T0–T8 itself. It closes no open physics question; it standardizes the 1D wrap boundary that the Python cosmogenesis cells already implement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.