ContinuumMetricCollapseOpen
plain-language theorem explainer
Names the open continuum residual that some shape-regular refinement family exhibits metric collapse of the certificate residual: normalized distance to the metric image tends to zero while the response-difference norm stays away from zero. Gravity analysts in Campaign G4/G5 cite it as the collapse terminal of the frozen trichotomy. It is a bare existential Prop, not a proved claim.
Claim. There exists a shape-regular refinement family $F$ such that the normalized separation of $F$ tends to $0$ as the refinement level tends to infinity, while the edge norm of the response difference of $F$ does not tend to $0$.
background
Campaign G4/G5 studies continuum promotion of the order-sensitive residual. The finite Boolean fact that the certificate residual lies outside the metric edge image is already imported; the continuum step replaces that non-membership by a normalized-separation trichotomy under a shape-regular refinement family.
A refinement family packages, at each level $n$, a response difference, a metric projection, and a positive level norm (shape regularity). Normalized separation measures how far the response difference sits from the metric image, scaled by that level norm. The frozen trichotomy has three terminals: survive (positive liminf of normalized distance), metric collapse (normalized distance $\to 0$ while the response norm does not), and lattice washout (response norm $\to 0$).
Metric collapse is the middle terminal: Tendsto of normalized separation to $0$ at atTop, conjoined with failure of the edge-norm of the response difference to tend to $0$. The geometric mesh Tendsto baseline (Arc 2 step 9) is required before any terminal may be claimed.
proof idea
Definitional, not a proof. The declaration is the Prop that there exists a refinement family $F$ satisfying the metric-collapse predicate: normalized separation tends to $0$ along levels, and the edge norm of the response difference does not. No witness is constructed; the body is the existential wrapper around that predicate.
why it matters
Holds a named slot in the honesty layer of continuum promotion. The module records continuum survival, collapse, and washout for the certificate pair as OPEN residual Props (uninhabited), and states explicitly that continuum promotion is not earned from the finite outside-image theorem. Forbidden move: promoting the finite Boolean residual to continuum novelty.
No downstream consumers yet. The declaration freezes the collapse branch of the trichotomy so later mesh-limit work can inhabit or refute it without redefining the terminal. It sits next to the signed alpha-genesis residual against CODATA only as ambient certificate context, not as a numerical claim about $\alpha$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.