ContinuumWashoutOpen
plain-language theorem explainer
Names the open continuum residual asserting lattice washout: some shape-regular refinement family has response-difference edge-norm tending to zero. Gravity analysts on Campaign G4/G5 cite it as the washout leg of the frozen survive/collapse/washout trichotomy. It is a bare existential Prop definition (uninhabited), not a proved terminal.
Claim. There exists a shape-regular refinement family $F$ such that the edge-norm of its response difference tends to $0$ as the refinement level tends to infinity (lattice washout).
background
Campaign G4/G5 promotes the finite order-sensitive certificate residual to continuum language. The finite stage already sits outside the metric edge image. Continuum claims are organized by a frozen trichotomy on a refinement level $n$ with response difference $\Delta_n$ and metric image $M_n$: survive (positive liminf of normalized distance to the metric image), metric collapse (normalized distance $\to 0$ while the response norm does not), and lattice washout (response norm $\to 0$).
A shape-regular refinement family packages, at each level $n$, a response difference, a metric projection, and a positive level norm. Lattice washout for such a family is the filter statement that the edge-norm of the response difference tends to $0$ along atTop. The geometric mesh Tendsto baseline (Arc 2 step 9) is required before any continuum terminal is claimed.
proof idea
Definitional unpacking only. The Prop is the existential of lattice washout over the refinement-family interface: some $F$ with edge-norm of $F$'s response difference tending to the neighborhood of $0$ at infinity. No tactics, no lemmas discharged.
why it matters
Records the washout terminal of the continuum trichotomy as an explicit OPEN residual. Module honesty forbids promoting the finite outside-image theorem to continuum novelty; continuum promotion is flagged as not earned. Sibling open Props cover survival and metric collapse. No downstream inhabitants yet: the declaration exists so later mesh-limit work can target a named terminal rather than an ad-hoc Tendsto goal. It sits in the gravity analysis stack beside discrete Lichnerowicz axis-sector convergence and four-tet signed-deficit status, but does not itself close those gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.