normalizedSeparation
plain-language theorem explainer
Normalized separation is the ratio of squared Frobenius norms of the residual (response difference minus its metric projection) to the response difference itself, at refinement level n. Continuum gravity analysts cite it to state survival versus metric collapse for order-sensitive residuals under a shape-regular family. It is a pure definition: residual edge-norm over response edge-norm on the 16×16 patch.
Claim. Given a shape-regular refinement family $F$ and level $n\in\mathbb{N}$, write $\Delta_n$ for the response-difference edge field at $n$ and $P_n(\Delta_n)$ for its metric projection. With squared Frobenius edge norm $\|A\|_2^2=\sum_{i,j=0}^{15} A_{ij}^2$ on the $16\times 16$ patch, the normalized separation is $\|\Delta_n-P_n(\Delta_n)\|_2^2\,/\,\|\Delta_n\|_2^2$.
background
Campaign G4/G5 promotes the finite order-sensitive residual outside the metric edge image to a continuum trichotomy under a shape-regular refinement family. The three frozen terminals are: survive (positive liminf of normalized distance to the metric image), metric collapse (normalized distance tends to 0 while the response norm does not), and lattice washout (response norm tends to 0).
A refinement family packages, at each level $n$, a response-difference field $\Delta_n:\mathrm{Fin},16\times\mathrm{Fin},16\to\mathbb{R}$, a metric projection operator $P_n$ on such fields, and a positive level norm (shape regularity). Upstream, response difference is the pointwise gap of two history-response configurations on the same patch. The edge norm used here is the squared Frobenius sum $\sum_{i,j} F_{ij}^2$.
The module records continuum survival, collapse, and washout as open residual Props; the geometric mesh Tendsto baseline is required before any terminal is claimed, and continuum promotion is explicitly not earned from the finite Boolean outside-image theorem.
proof idea
Definition only: no proof obligations. At level $n$, form the residual edge field $\Delta_n-P_n(\Delta_n)$ by subtracting the metric projection of the response difference from the response difference itself, take its squared Frobenius edge norm, and divide by the edge norm of $\Delta_n$. The construction is noncomputable solely because it lives in $\mathbb{R}$ with real division and summation.
why it matters
This scalar is the quantitative backbone of the frozen continuum trichotomy. Downstream, Survives asserts existence of $\varepsilon>0$ such that eventually $\varepsilon\le$ normalized separation, while MetricCollapse asserts Tendsto of normalized separation to 0 together with non-Tendsto of the response edge norm to 0. Both Props are currently uninhabited open residuals; the finite outside-MetricEdgeImage fact is already proved and must not be silently promoted.
In the Recognition gravity stack this sits in the continuum-order-sensitive residual analysis (G4/G5), separating genuine new-sector survival from metric absorption or lattice washout before any continuum novelty claim. It does not touch T0–T8 forcing, RCL, or the mass ladder; it is local to residual geometry on the 4D history-response patch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.