edgeNorm
plain-language theorem explainer
Squared Frobenius norm of a 16×16 real edge field on the recognition patch: sum of squared entries. Gravity analysts cite it to normalize residual distance to the metric image and to state continuum washout versus collapse. The body is the plain double sum; no lemmas.
Claim. For an edge field $F$ on the $16\times 16$ patch (maps $\{0,\ldots,15\}^2\to\mathbb{R}$), the edge norm is $\|F\|_{2}^{2}:=\sum_{i,j} F_{ij}^{2}$.
background
Campaign G4/G5 studies continuum promotion of the order-sensitive residual. The finite Boolean fact that a certificate response difference lies outside MetricEdgeImage is already imported; the module replaces that with a normalized-separation trichotomy under a shape-regular refinement family.
An edge field here is a real 16×16 array on the discrete patch (Fin 16 indexing). The squared Frobenius norm of that array is the natural scale for residual size: it vanishes exactly when the field is identically zero and is homogeneous of degree two under real scaling.
Downstream, continuum terminals are phrased with this scale. Lattice washout is Tendsto of the response-difference norm to 0; metric collapse is Tendsto of normalized separation to 0 while that norm does not; survival is a positive liminf of the same normalized distance.
proof idea
Definition only: expand the squared Frobenius norm as the double sum $\sum_i\sum_j (F,i,j)^2$ over Fin 16. No lemmas, no tactics, no hypotheses. Marked noncomputable because the ambient real analysis stack is.
why it matters
Local measuring stick for the G4/G5 trichotomy. normalizedSeparation divides the residual (response difference minus its metric projection) by this norm, so the continuum distance is scale-free. LatticeWashout is exactly Tendsto of edgeNorm of the response difference to 0 at infinity; MetricCollapse pairs vanishing normalized separation with failure of that washout Tendsto.
The module freezes the honesty boundary: continuum survival, collapse, and washout remain OPEN residual Props; continuum promotion is explicitly not earned from the finite outside-image theorem. This def supplies the common scale those OPEN statements need once the geometric mesh Tendsto baseline (Arc 2 step 9) is available. It does not itself touch T0–T8 or the RCL; it is analysis scaffolding inside the gravity residual campaign.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.