tick_has_2cube
plain-language theorem explainer
The tick phase type satisfies the condition of having exactly eight elements. Researchers in Recognition Science cite this when establishing that the eight-tick period belongs to the family of 2³-structures shared with the Pauli group and other domains. The proof unfolds the relevant cardinality predicate and applies a decision tactic to confirm the finite count.
Claim. Let $T$ be the type of tick phases with eight discrete elements. Then the cardinality of $T$ equals $2^3$.
background
This module collects instances of the cardinality 8 = 2³ across Recognition Science domains, viewing it as the maximal periodic structure for spatial dimension 3. The predicate asserting 2³-structure on a finite type T requires that its cardinality equals 8. The type of tick phases is an inductive type with eight constructors t0 to t7, which automatically derives a finite type instance.
proof idea
The proof is a one-line wrapper. It unfolds the 2³-structure predicate to the statement that the cardinality of the tick phase type equals 8, then invokes the decide tactic to compute and verify this equality from the inductive definition.
why it matters
This declaration provides a canonical instance for the cross-domain 2³-universality. It is invoked in the equicardinality theorem between Pauli elements and tick phases, and is recorded in the universality certificate that aggregates all such instances. Within the framework it realizes the eight-tick octave and contributes to the forcing chain step that yields three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.