Pith. sign in
module module moderate

IndisputableMonolith.Gravity.SevenGaps.Gap2ExactClassCarrierAttack

show as:
view Lean formalization →

Module for the Gap-2 exact-class carrier attack on the continuum R5 residual in Recognition gravity. It sits under the enriched-carrier phase layer and records that the older exact-path-class carrier route is superseded. Gravity auditors cite it when tracing how oscillatory-tail residuals are discharged below ExactPathClass. Structure is import-thin: one upstream phase module and a single audit consumer.

claimGap-2 carrier attack on the continuum residual $\mathrm{TypedResidual}_{\mathrm{continuum\_substrate\_oscillatoryTail}} := \exists\,\mathrm{phase},\;\mathrm{OscillatoryTail}(\mathrm{phase})\land\neg\mathrm{OscillatoryTail}(\mathrm{zeroPhase})$, treated below $\mathrm{ExactPathClass}$ via the enriched-carrier phase, with the prior exact-class carrier route marked superseded.

background

SevenGaps is the gravity ledger of open Recognition residuals. Gap 2 concerns continuum substrate structure, specifically whether an oscillatory tail can appear on a nontrivial phase while the zero phase has none.

Upstream, Wave C R5 (decision D-qg-c1-r4-enriched-carrier-20260722) implements an enriched-carrier phase strictly below ExactPathClass. That phase module states the residual as existence of a phase with OscillatoryTail that is not the zero phase.

This module is the exact-class carrier attack layer that consumes that enriched phase. The sibling flag superseded_by_enriched_carrier records that the older exact-path-class carrier route is retired in favor of the enriched construction.

proof idea

Definition and attack-routing module, not a standalone theorem file. It imports the enriched-carrier phase module and exposes the superseded_by_enriched_carrier marker so downstream audit can treat the exact-class carrier path as closed by the enriched route. No independent tactic proof body; the mathematical content lives in the upstream residual and phase definitions.

why it matters in Recognition Science

Closes the bookkeeping edge between the enriched-carrier R5 attack and the Gap-2 audit surface. Downstream, Gap2ExactClassCarrierAttackAudit imports this module to certify that the exact-class carrier attack is accounted for under the enriched phase. In the broader gravity program it keeps the continuum oscillatory-tail residual aligned with the Wave C decision trail rather than a stale ExactPathClass carrier proof obligation.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (1)