Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.ContinuumOrderSensitiveResidual4D

show as:
view Lean formalization →

Module for continuum residuals of order-sensitive edge currents on the Freudenthal 4D patch. It defines edge-field norms, refinement families, and three continuum predicates (survival, metric collapse, lattice washout), plus the promotion gate that unlocks coefficient forcing. Gravity analysts on campaign G cite it. Mostly definitional scaffolding with a few finite-image lemmas and open continuum claims.

claimOn the sixteen-site Freudenthal patch, define the squared Frobenius edge-field norm $\|F\|_F^2$, refinement families, and normalized separation. Package continuum survival, metric collapse, and lattice washout as predicates on residual edge currents; record when a nonzero continuum residual is earned so that a dimensionless order-sensitive coefficient may be forced.

background

Order-sensitive gravity (frozen plan OrderSensitive_Gravity_Proposition_20260802) reads a Loom configuration through a depth-two commutator and seats the result as an edge-current response on the Freudenthal cover (upstream OrderSensitiveHistoryResponse4D, claims G2/G3). The linearized metric image of such a current is the strain of some $\mathrm{Mat}_4$ perturbation on the sixteen-site patch (MetricEdgeImage4D).

This module sits between that discrete response and continuum coefficient extraction. It needs a scale-invariant residual measure: the squared Frobenius norm of the edge field, a notion of refinement family, and normalized separation between residual and metric image. Three continuum fates are named: the residual survives refinement, collapses into the metric image, or washes out as a pure lattice artifact.

Certificate data from Loom supply the concrete automorphism and base-homomorphism tables used to ground the discrete side; they are imported only as frozen measurement input.

proof idea

Definition-heavy module, not a single theorem. It introduces edgeNorm, RefinementFamily, and normalizedSeparation, then the three continuum predicates Survives, MetricCollapse, and LatticeWashout. Proved pieces are local and finite: finite_outside_metric_image and collapse_not_washout relate metric-image membership to the washout/collapse dichotomy. The continuum claims themselves (ContinuumSurvivalOpen, ContinuumMetricCollapseOpen, ContinuumWashoutOpen) remain open interfaces. continuumPromotionEarned packages the gate condition that a nonzero continuum residual has been established.

why it matters in Recognition Science

Campaign G6 coefficient forcing (OrderSensitiveCoefficientForce4D) is explicitly gated: "A dimensionless normalization-invariant coefficient may be derived only after a nonzero continuum residual is earned." This module is that gate. Without a residual that survives continuum refinement and is not pure metric image or lattice washout, no order-sensitive gravity coefficient may be extracted.

It closes the discrete-to-continuum seam between the G2/G3 history-response and metric-edge-image layers and the G6 forcing layer. In the broader Recognition gravity program it is the residual hygiene step: only residuals that pass continuum promotion may feed dimensionless constants. The open continuum predicates mark the remaining analytic work before the gate can fire unconditionally.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (14)