tick_eq_twoPowD
plain-language theorem explainer
The theorem establishes that the TickPhase inductive type has cardinality exactly 2^3. Researchers modeling cross-domain attention in Recognition Science cite it to anchor the eight-tick octave. The proof is a one-line decide tactic that evaluates the Fintype instance on the eight-constructor definition.
Claim. The inductive type consisting of eight phases $t_0$ through $t_7$ satisfies $|TickPhase| = 2^3$.
background
The Attention Space module factors the attentional state space as the product AttentionNetwork × TickPhase, giving 5 × 8 = 40 states inside the gap45 ceiling that leaves five overflow slots. TickPhase is defined as an inductive type with constructors t0 to t7 that derives DecidableEq, Repr, BEq, and Fintype. The same inductive definition appears upstream in TwoCubeUniversality, supporting the structural universality of the two-cube that underlies the eight-tick periodicity.
proof idea
The proof is a one-line wrapper that applies the decide tactic. This tactic directly computes Fintype.card from the derived Fintype instance on the inductive TickPhase type.
why it matters
The result supplies the tick_2cube field inside attentionSpaceCert, which bundles the certificates for the 40-state attention space plus overflow. It realizes the eight-tick octave (T7) from the forcing chain inside the C5 cross-domain claim. The parent attentionSpaceCert uses it to certify the factorization AttentionNetwork × TickPhase = 40.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.