Pith. sign in
module module moderate

IndisputableMonolith.Gravity.SevenGaps.Gap2SignatureBlockerAttack

show as:
view Lean formalization →

Defines the signature-fiber decomposition of shell classes used in the Gap-2 R4 blocker attack: classes in shell n with fixed signature s, their Burnside masses, and the fiberwise identity for exact shell amplitudes. Gravity and QG residual auditors cite it when routing oscillatory-tail and tick-phase arguments through Fin-8 signature strata. The module is mostly definitional equalities plus the fiberwise amplitude lemma that feeds the enriched-carrier phase attack.

claimFor each shell index $n$ and signature $s$, the signature fiber is the set of classes in shell $n$ with fixed signature $s$. Signature mass equals the corresponding Burnside mass (a pure power count). Shell mass is the sum of signature masses over $s$. The tick-phase predicate $\sigma_{\mathrm{tick}}$ is equivalent to the shell-signature tick condition, and the exact shell amplitude factors fiberwise over signatures.

background

Gap 2 in the Seven Gaps gravity program concerns residual oscillatory tails and tick-phase balance after the R2 cross-family correction. Upstream, Gap2TickPhaseTailBlocker hardens the R4 residual: an all-shell tick-fiber mass balance forces every exact shell amplitude to vanish, so contiguous-block sums vanish. RegulatorRemovalNoGo shows the Gaussian-regulated quotient path sum has no $\rho\to 0^+$ limit at zero phase, so zero-phase regulator removal is blocked at the kernel.

This module supplies the combinatorial substrate for a signature-stratified attack on that residual. Shell classes are partitioned by a Fin-8 (eight-tick) signature $s$. Signature fiber collects classes in shell $n$ with fixed $s$; signature mass is identified with a Burnside orbit count; shell mass is the sum of those masses. A tick-phase predicate on signatures is tied to the shell-signature tick condition used by the tail blocker.

The local setting is Wave C1 R4 hardening inside Recognition gravity: amplitudes and path-class masses must be tracked shell-by-shell and signature-by-signature before any continuum or enriched-carrier phase lift.

proof idea

Definition-heavy module with equational lemmas, not a single end-to-end theorem. Signature fiber is introduced as the class set at fixed shell and signature; an embedding and a map-equality identify it with the expected image. Burnside mass is defined as a pure power; signature mass is proved equal to that Burnside mass. Shell mass is rewritten as the sum of signature masses. Tick-phase predicates are shown equivalent (sigmaTick iff shell-signature tick). The main analytic step is the fiberwise identity: exact shell amplitude equals the sum (or matching assembly) of signature-fiber contributions, so later blockers can kill or balance amplitudes one signature at a time.

why it matters in Recognition Science

Feeds the Wave C R5 enriched-carrier phase attack (Gap2EnrichedCarrierPhase), which targets the continuum residual that some phase has an oscillatory tail while zero phase does not. Also imported by the axiom audit module that requires headline theorems to print only under [propext, Classical.choice, Quot.sound].

In the Recognition chain this sits under gravity residuals tied to the eight-tick octave (T7) and shell amplitudes after regulator no-gos. By making exact shell amplitude fiberwise in signature, it turns the R4 tick-phase tail blocker into a signature-stratified tool rather than a single global vanishing statement. Without this decomposition, the enriched-carrier phase decision cannot route oscillatory-tail witnesses below the exact path-class layer.

scope and limits

used by (2)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (22)