spacing_monotone
plain-language theorem explainer
Finer lattice refinements (larger site count N) yield smaller spacing a = L/N for fixed box side L > 0. Anyone building the N→∞ continuum bridge from discrete RS ledger sites to a Lorentzian manifold cites this monotonicity. The proof is a direct application of the standard real-division inequality under a nonnegative numerator and positive denominators.
Claim. For any box length $L > 0$ and natural numbers $N_1, N_2$ with $0 < N_1 \le N_2$, the lattice spacings satisfy $L/N_2 \le L/N_1$.
background
The module ContinuumManifoldEmergence is the zero-parameter bridge from discrete Recognition Science ledger sites to Lorentzian spacetime. The chain runs J-cost lattice → quadratic cost → Laplacian → Lorentzian interval → Minkowski flat limit → curved metric from defect → Einstein equations. Architecture step 5 introduces a finite N-site lattice in a box of side L with spacing a = L/N.
Upstream, UnifiedLatticeManifoldCorrespondence defines lattice spacing at refinement level N by spacing(R, N) = R.L / N. The continuum program needs that refining the lattice (raising N) shrinks a, so that for any target resolution ε > 0 one can choose N large enough that a < ε (the next theorem in the file).
Local conventions: L is a positive real box length; N ranges over positive naturals; division is real division after Nat.cast. No Recognition-specific cost or forcing hypothesis enters this inequality; it is pure real arithmetic supporting the continuum limit.
proof idea
Term/tactic hybrid, two lines. Apply Mathlib's div_le_div_of_nonneg_left with numerator nonnegativity from hL.le (L > 0) and left-denominator positivity from Nat.cast_pos on h₁ (N₁ > 0). The remaining goal is the denominator comparison N₁ ≤ N₂ after casting to ℝ, discharged by Nat.cast_le on the hypothesis h. No RS-specific lemmas are required.
why it matters
Monotonicity of spacing is the elementary comparison step inside the N→∞ continuum bridge. Without it, one cannot guarantee that refining the ledger lattice drives a = L/N toward zero, which is the discrete-to-continuum hypothesis feeding Laplacian convergence (from ContinuumLimit) and the flat Minkowski limit.
The module frames this as foundational rather than phenomenological: Lorentzian signature, c = 1 voxel/tick, spatial metric from J''(1) = 1, and D = 3 are forced elsewhere in the chain; spacing monotonicity is the arithmetic glue that lets finite-N lattices approach that continuum. The immediate successor in the file is the arbitrary-resolution theorem (for any ε > 0 choose N with L/N < ε). No downstream consumers are recorded yet (used_by empty), so this is infrastructure for the continuum certificate rather than a leaf cited by gravity phenomenology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.