latticeSpacing_pos
plain-language theorem explainer
The theorem asserts that the lattice spacing a = L/N is strictly positive whenever the box side L is a positive real and the site count N is a positive integer. Researchers building discrete-to-continuum limits in Recognition Science cite it to keep the spacing parameter inside the positive reals during convergence arguments. The proof is a one-line term that applies the division-positivity lemma directly to the definition a = L/N.
Claim. Let $L > 0$ be real and let $N$ be a positive integer. Then the lattice spacing $a = L/N$ satisfies $a > 0$.
background
The Discrete-to-Continuum Bridge module connects the RS discrete lattice theory to the IM continuum GR by the chain J-cost lattice to quadratic defect to lattice Laplacian to Ricci scalar to Einstein tensor. The sibling definition latticeSpacing sets the lattice spacing to $a = L/N$ for a box of side L containing N sites. Upstream, the structure as from ContinuumBridge identifies the Laplacian action with a weighted sum over simplices: (1/2) Σ w_ij (ε_i − ε_j)² = (1/κ) Σ δ_h A_h.
proof idea
The proof is a one-line term that invokes div_pos on the hypothesis 0 < L together with the cast of 0 < N into the reals.
why it matters
This result supplies the basic positivity required for the Tier 1 proved statements in the bridge, including the Minkowski flat limit and Laplacian convergence at O(a²) with coupling κ = 8φ⁵ and D = 3. It precedes the full DiscreteContinuumBridge certificate and the weak-field limit to the Poisson equation. No open questions are directly addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.