ExactShellTickPhaseSubstrate
plain-language theorem explainer
Packages a Fin-8 tick assignment on exact complexity path classes whose derived real phase escapes both certified dead classes (shell-constant and eventually-zero). Gap-2 gravity workers cite it as the R2 schema residual for tick-phase enrichment on exact shells. As a structure it only fixes field types; the analytic tail residual is deliberately left out.
Claim. An exact-shell tick-phase substrate is a triple consisting of a map $\tau$ sending each exact path class in shell $n$ to an element of $\{0,\ldots,7\}$, together with proofs that the derived real phase $2\pi\,\tau/8$ is not shell-constant and is not eventually zero as a phase field.
background
Wave C1 Gap 2 banks an exact-shell tick-phase enrichment schema. Exact path classes already quotient by global equivalence, so a tick map on those classes is well-posed by construction; no separate descent step is needed.
The eight-tick API supplies only a Fin-8 trace hypothesis (phases $k\pi/4$ for $k=0,\ldots,7$, period $2\pi$). It does not prove equidistribution. Two certified dead classes live upstream in the shell-balance blocker: shell-constant phase (constant on each shell) and eventually-zero phase. Escape from both is required before any cancellation story can start.
The derived real phase is the standard lift $2\pi\cdot\mathrm{tick}/8$ of the Fin-8 label. Contiguous late-block analytic cancellation is a separate open residual and is not packed into this structure.
proof idea
Structure definition, not a proved theorem. Three fields: a tick assignment on exact path classes, a proof that the derived phase is not shell-constant, and a proof that it is not eventually zero. The companion extractor simply returns the derived real phase of the stored tick map (one-line projection). No tactics or lemmas fire at this declaration.
why it matters
Fills the R2 schema residual in the Gap-2 residual DAG and the CORE 2 PHASE design: existence of an escaping tick-phase enrichment, without demanding analytic tails. Downstream, the schema package is exactly nonemptiness of this structure, and the concrete witness is the signature vertex-count mod 8 substrate, which clears both dead classes (its oscillatory tail stays open as R4).
Sits on the T7 eight-tick octave landmark: Fin-8 labels and eighth-root orthogonality later convert fiber-mass balance into shell-amplitude vanishing. Does not flip the continuum-and-measure gap; strengthened block cancellation remains the open analytic half.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.