spatial_isotropy
plain-language theorem explainer
The log-coordinate recognition cost is even: J_log(−ε) equals J_log(ε) for every real displacement. Continuum-limit and gravity authors cite this to justify isotropic spatial metric coefficients and SO(3) rotational invariance on the lattice. The proof is a one-line application of the evenness of cosh.
Claim. For every real $\varepsilon$, $J_{\log}(-\varepsilon) = J_{\log}(\varepsilon)$, where $J_{\log}(t) := \cosh t - 1$. Thus the recognition cost is direction-independent on spatial neighbor pairs, forcing isotropic spatial metric coefficients and $SO(3)$ rotational invariance.
background
The module builds the zero-parameter bridge from discrete RS ledger sites to a Lorentzian continuum: J-cost lattice to quadratic cost to Laplacian to Minkowski interval, then curved metrics from defects. Lorentzian signature, light-cone structure, and the flat-space limit are proved unconditionally; spatial geometry is forced by $J''(1)=1$ and $D=3$ from DimensionForcing.
$J_{\log}$ is the cost in log coordinates: $J(e^t)=\cosh t-1$, a convex bowl minimized at $t=0$. Upstream, J_log_symmetric records that this bowl is even, via $\cosh(-t)=\cosh t$. Neighbor-pair costs therefore cannot prefer a spatial axis, which is the local content of spatial isotropy before the continuum limit is taken.
Sibling results in the same file fix the Minkowski form $\eta$ on $\mathbb{R}^{1,3}$, the sign pattern (temporal negative, spatial positive), and the causal trichotomy used by the master certificate.
proof idea
One-line term wrapper: the claim is exactly the universal statement of J_log_symmetric from DiscretenessForcing. That lemma unfolds $J_{\log}(t)=\cosh t-1$ and rewrites with Real.cosh_neg. No extra algebra or continuum hypotheses are needed.
why it matters
Isotropy is the geometric reason the three spatial signature lemmas can share one positive coefficient and why the continuum spatial metric is Euclidean rather than anisotropic. Downstream it is consumed by continuum_limit_certificate, the master ContinuumLimitCert packing temporal negativity, three spatial positivities, and causal trichotomy.
In the RS forcing chain this sits under the continuum bridge after T5 (J-uniqueness: $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$) and T8 ($D=3$). Evenness of $J_{\log}$ is what turns the unique cost into $SO(3)$-invariant neighbor weights on the voxel lattice, before Laplacian convergence and the weak-field path to Einstein equations. It is proved scaffolding for the zero-parameter gravity story, not a fit parameter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.