MetricCollapse
plain-language theorem explainer
Metric collapse is the continuum terminal where a shape-regular refinement family's normalized distance to the metric image vanishes at infinity, while the response-difference edge norm stays away from zero. Gravity analysts on the G4/G5 continuum-promotion campaign cite it as one arm of the frozen trichotomy (survive / collapse / washout). The declaration is a pure definitional Prop pairing two filter limits; nothing is proved here.
Claim. For a shape-regular refinement family $F$, metric collapse holds when the normalized separation of the response difference from its metric projection tends to $0$ as the refinement level $n\to\infty$, yet the squared Frobenius edge norm of that response difference does not tend to $0$.
background
Campaign G4/G5 replaces finite Boolean non-membership in the metric edge image by a normalized-separation trichotomy under a shape-regular refinement family. The three frozen continuum 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 a level-indexed response difference on the $16\times 16$ edge patch, a metric projection of that field, a positive level norm (shape regularity), and the derived quantities used below. The edge norm is the squared Frobenius norm $\sum_{i,j} F_{ij}^2$ on the patch. Normalized separation is that residual-to-projection edge norm divided by the response-difference edge norm itself.
The module records continuum survival, collapse, and washout for the certificate pair as open residual Props. Continuum promotion is explicitly not earned from the finite outside-image theorem; a geometric mesh Tendsto baseline is required first.
proof idea
Definitional, not a proof. The Prop is the conjunction of two filter statements: Tendsto of normalized separation along atTop into a neighborhood of 0, and the negation of Tendsto of the response-difference edge norm into a neighborhood of 0. No lemmas are applied; the body simply names those two continuum conditions.
why it matters
This is the middle arm of the frozen continuum trichotomy that structures Campaign G4/G5. Downstream, collapse_not_washout uses the second conjunct to show collapse and lattice washout are incompatible by definition (the washout hypothesis is exactly the negated tendsto). ContinuumMetricCollapseOpen packages existence of some refinement family satisfying metric collapse as an open residual Prop: inhabiting it would be a genuine continuum terminal claim for the certificate residual.
In the Recognition gravity stack this sits after the finite residual is already known to lie outside the metric edge image. The honesty clause of the module forbids promoting that finite Boolean fact to continuum novelty. Until a shape-regular mesh baseline (Arc 2 step 9) is in place, no terminal, including collapse, is claimed for the discovery pair.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.