TickPhase
plain-language theorem explainer
TickPhase enumerates eight discrete phases that close the recognition cycle under the eight-tick octave. Attention models cite it to factor the state space as AttentionNetwork times this phase set, producing exactly 40 elements under the gap45 ceiling. The declaration is a direct inductive enumeration that derives decidable equality and finite cardinality with no additional lemmas.
Claim. Let $TickPhase$ be the inductive type generated by eight constructors $t_0, t_1, t_2, t_3, t_4, t_5, t_6, t_7$, equipped with decidable equality, representation, boolean equality, and finite type structure.
background
The Attention Space module defines the full state space as the product AttentionNetwork × TickPhase. The module document states that this product equals 5 × 8 = 40 and leaves exactly five overflow slots beneath the complexity ceiling gap45. TickPhase is imported from TwoCubeUniversality, where the same eight-element inductive type appears to support equicardinality with the Pauli group. This construction realizes the eight-tick octave (period 2³) required by the forcing chain for three spatial dimensions.
proof idea
The declaration is a direct inductive definition that enumerates the eight phases and invokes the deriving clause to obtain DecidableEq, Repr, BEq, and Fintype instances automatically.
why it matters
TickPhase supplies the 8-element factor needed by AttentionSpaceCert to certify that the attention state count is 40 with five overflow slots and that the phase cardinality equals 2³. It feeds the downstream results network_surj, tickCount, tick_eq_twoPowD, and pauli_tick_equicardinal. The structure closes the T7 step of the forcing chain and supports the module's prediction of 40 stable plateaus plus five transient ones in attentional-blink experiments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.