FiniteLattice
plain-language theorem explainer
A finite cubic spatial lattice is a positive integer N (sites per edge) together with a positive box side L. Spacing is a = L/N, site count is N³, and physical volume is L³. Anyone building the N→∞ continuum bridge from ledger sites to a Lorentzian manifold cites this carrier. The object is a plain structure with positivity witnesses; derived facts are one-line positivity and power lemmas.
Claim. A finite spatial lattice is a pair $(N,L)$ with $N\in\mathbb{N}$, $N>0$, $L\in\mathbb{R}$, $L>0$. Its lattice spacing is $a=L/N$, its number of spatial sites is $N^3$, and its physical volume is $L^3$. One has $a>0$, $a\neq 0$, and $L^3>0$.
background
The module builds the zero-parameter bridge from discrete Recognition Science ledger sites to Lorentzian spacetime: J-cost lattice to quadratic cost to Laplacian to Lorentzian interval, then curved metric from defect and Einstein equations. Architecture step 5 is exactly a finite N-site lattice in a box of side L with spacing a = L/N, before Laplacian convergence as N → ∞.
D = 3 spatial dimensions is already forced upstream (DimensionForcing), so the natural site count is N³ and the box volume is L³. A parallel spacing notion appears in UnifiedLatticeManifoldCorrespondence as spacing at refinement level N equal to L/N; the present structure packages the same geometric data with explicit positivity hypotheses on N and L.
Sibling material in the module fixes the Minkowski form η on ℝ^{1,3}, Lorentzian signature, and the causal trichotomy (timelike / spacelike / lightlike), so this lattice is the discrete spatial carrier sitting under that continuum limit.
proof idea
FiniteLattice is a structure, not a proved statement: four fields N, N_pos, L, L_pos. Spacing is the definition a = L/N. Positivity of spacing is div_pos on L_pos and Nat.cast_pos of N_pos; nonzero spacing is ne_of_gt of that positivity. Site count is the definition N^3. Physical volume is the noncomputable definition L^3; volume positivity is pow_pos on L_pos at exponent 3. No deep lemmas are required.
why it matters
This is the discrete spatial stage in the foundational continuum bridge: without a finite lattice carrier one cannot state Laplacian convergence, the flat Minkowski limit, or the later weak-field defect → curved Lorentzian → Einstein path. The module contrasts this zero-parameter story with the phenomenological ILG time-kernel: here Lorentzian signature, c = 1 voxel per tick, spatial metric from J''(1) = 1, and D = 3 are forced rather than fit.
It aligns with framework landmarks T7 (eight-tick octave / discrete tick structure) and T8 (D = 3), and with ContinuumLimit / DiscretenessForcing imports. No used_by edges are recorded yet; the structure is infrastructure for spacing monotonicity and the N → ∞ limit theorems that follow in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.