Pith. sign in
module module moderate

IndisputableMonolith.Gravity.SevenGaps.Gap2ContinuumMeasureResidualDAG

show as:
view Lean formalization →

Status DAG for Gap-2 residual claims on the measure and continuum sides of the discrete path-sum. It packages typed residuals for gauge-counting blockers, history presentation, Cauchy/oscillatory-tail equivalence, cap-shell compatibility, and substrate tails, plus a decoy that zero phase is not an oscillatory tail. Gravity auditors cite it as the R1 measure residual ledger. Structure is a binding/status module over imported blocker and bridge theorems, not a new analytic derivation.

claimThe Gap-2 residual DAG records that normalized gauge counting holds for the counting mass $\mu(K)=1/|\mathrm{Aut}\,K|$ and fails for the quotient-uniform decoy; continuum residuals equate Cauchy behavior of the shell path sum with an oscillatory tail, assert cap-shell carrier compatibility, and mark substrate oscillatory-tail status, with a decoy that the zero phase is not an oscillatory tail.

background

Seven Gaps is the discrete quantum-gravity campaign whose path-sum configuration space is organized by exact complexity shells and a Gaussian UV regulator $\exp(-\rho n^2)$. PathSumMeasure postulates the symmetry factor $\mu(K)=1/|\mathrm{Aut},K|$; ExactShellGaugePreflight derives that mass from pure gauge counting without mentioning $\mu$ or $\mathrm{Aut}$ in the mass definition. ExactShellGaugeUV proves shell-resummed convergence for every $\rho>0$.

CapShellBridge supplies the carrier equivalence behind cap-shell compatibility: at cap $B$, a bounded complex has unique exact complexity $\max(n_V,n_E,n_T)\le B$, and exact shells $n\le B$ reattach as bounded complexes. Gap2MeasureStatusBinding flips measure-side ledger Bools once gauge counting is discharged from history. This module sits on those imports as the residual DAG for R1 (measure) and continuum residual types.

proof idea

Definition and status-binding module, not a standalone analytic proof. It declares typed residual constructors (measure gauge-counting blocker, history presentation, continuum Cauchy $\Leftrightarrow$ oscillatory tail, cap-shell compatibility, substrate oscillatory tail) and concrete residual terms that point at imported blocker/bridge packages. A decoy residual records that zero phase is not an oscillatory tail. Gap2ResidualDAGStatus / gap2ResidualDAGStatus aggregate the Bool ledger. Argument structure is import-and-bind: discharge or block each residual by reference to ExactShellGaugePreflight, GaugeHistoryMeasure, CapShellBridge, Zq continuum blockers, and related Gap-2 tail/fiber packages.

why it matters in Recognition Science

Closes the R1 measure residual surface in the Seven Gaps ledger: normalized gauge counting for the counting mass, with an explicit fail path for the quotient-uniform decoy. Downstream consumers are expected to be full-theory ledger flips and Gap-2 continuum closure routes (FullTheoryLedger pillar flags; measure status binding already ties substrate and preflight Bools to history discharge). Continuum residuals keep Cauchy/tail, cap-shell, and substrate claims in one DAG so auditors can see which continuum blockers remain open versus certified. No used_by edges yet; the module is a status sink for the measure/continuum half of Gap 2 rather than a theorem feeder with live dependents in the graph snapshot.

scope and limits

depends on (12)

Lean names referenced from this declaration's body.

declarations in this module (16)