RefinementFamily
plain-language theorem explainer
A shape-regular refinement family packages a level-indexed response difference on 16×16 edges, a metric projection operator, and a strictly positive level norm. Gravity analysts cite it to state continuum survival, metric collapse, or lattice washout for the order-sensitive residual. Pure interface definition: four fields, no proof obligations beyond positivity of the norm.
Claim. A shape-regular refinement family is a tuple $(\Delta, P, \nu)$ where $\Delta_n : \mathrm{Fin}\,16 \times \mathrm{Fin}\,16 \to \mathbb{R}$ is the response difference at refinement level $n$, $P_n$ is a metric projection sending any $16\times 16$ real matrix to one, and $\nu(n) > 0$ is a level norm for every $n \in \mathbb{N}$.
background
Campaign G4/G5 promotes the finite order-sensitive residual to a continuum trichotomy. The finite stage already shows the certificate residual lies outside the metric edge image. Continuum language needs a refinement family so that survival, collapse, and washout can be stated as filter limits.
The response difference at each level is the pointwise difference of two history-response matrices on $\mathrm{Fin},16$ edges (imported from the order-sensitive 4D history response). The metric projection is the continuum stand-in for membership in the metric edge image. The level norm supplies the denominator for normalized separation and is required to stay strictly positive (shape regularity), so the normalized distance is well-defined at every finite stage.
Module honesty: continuum terminals remain OPEN residual Props; the geometric mesh Tendsto baseline is still required before any terminal is claimed.
proof idea
No proof. The declaration is a structure with four fields: a level-indexed response difference, a level-indexed metric projection, a level norm, and the shape-regularity axiom that the level norm is positive at every $n$. Downstream definitions read these fields directly; nothing is derived here.
why it matters
Names the interface on which the frozen continuum trichotomy is written. Downstream, normalized separation, Survives, MetricCollapse, and LatticeWashout are defined relative to a refinement family; collapse and washout are proved incompatible by definition. The three OPEN residuals (continuum survival, metric collapse, lattice washout) are existential statements over this type. Continuum promotion is explicitly not earned from the finite outside-image theorem alone. Sits in the gravity analysis chain that lifts Boolean non-membership in the metric edge image to a normalized-separation residual under mesh refinement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.