metric_normalization
plain-language theorem explainer
The recognition cost satisfies J''(1) = 1, fixing the canonical scale so the spatial metric is the Euclidean Kronecker delta at each ledger site (to O(ε²)). Gravity and continuum-limit arguments cite this as the zero-parameter normalization of g_ij. The proof is a one-line term wrapper of the Cost.Convexity second-derivative identity.
Claim. Let $J(x) = \frac{x + x^{-1}}{2} - 1$ be the recognition cost on $(0,\infty)$. Then the second derivative at the identity ratio is unity: $J''(1) = 1$.
background
The module builds the zero-parameter bridge from discrete RS ledger sites to a Lorentzian continuum: J-cost lattice → quadratic cost → Laplacian → Lorentzian interval → Minkowski flat limit → curved metric from defect. Unlike the phenomenological ILG time-kernel, signature, c, and the spatial metric are forced rather than fitted.
The recognition cost is $J(x) = (x + x^{-1})/2 - 1$, equivalently $J_{\log}(t) = \cosh t - 1$ in log coordinates (a convex bowl at the identity). Strict convexity and the second-derivative evaluation at 1 are established in Cost.Convexity. In the continuum architecture, that second derivative supplies the quadratic form that becomes the Euclidean spatial metric on each site.
Upstream, deriv2_Jcost_one states exactly "$J''(1) = 1$". Dimension forcing (D = 3) and discreteness forcing sit in the same import cone; the present fact is the metric-scale half of the spatial side.
proof idea
One-line term proof: the claim is definitionally the already-proved Cost.Convexity lemma that the second derivative of Jcost at 1 equals 1 (itself obtained by rewriting the closed-form second derivative on $(0,\infty)$ and simplifying at the point 1). No extra algebra is done here.
why it matters
This is the forced spatial-metric normalization in the continuum bridge: with $J''(1) = 1$, the quadratic expansion of the cost yields $g_{ij} = \delta_{ij}$ at each site up to $O(\varepsilon^2)$, so the flat-space limit is standard Euclidean space rather than a rescaled copy. It sits under the module's proved list (spatial metric from J-cost; flat limit = Minkowski) and is consumed by the master continuum_limit_certificate, which packages Lorentzian signature, causal trichotomy, and related continuum fields.
Framework-wise it rides on T5 J-uniqueness ($J(x) = (x+x^{-1})/2-1$) and feeds the zero-parameter gravity path (coupling $\kappa = 8\varphi^5$ derived elsewhere). Without this scale fix, the Laplacian→∇² and weak-field defect→Einstein steps would carry an arbitrary conformal factor on space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.