pauli_tick_equicardinal
plain-language theorem explainer
Pauli group elements and tick phases share cardinality 8. Cross-domain researchers cite this to confirm the 2^3 structure appears uniformly in signed Pauli operators and the fundamental temporal phases. The proof is a one-line application of the general equicardinality lemma for any two domains satisfying the 2-cube count property.
Claim. $|P| = |T|$ where $P$ is the set of eight signed Pauli matrices and $T$ is the set of eight discrete phases in the fundamental period.
background
The module collects instances of the count 8 = 2^3 across Recognition Science domains for spatial dimension D = 3. PauliElement is the inductive type with constructors plusI, minusI, plusX, minusX, plusY, minusY, plusZ, minusZ. TickPhase is the inductive type with constructors t0 through t7. The upstream lemma two_cube_equicardinal asserts that any two domains each satisfying HasTwoCubeCount have identical cardinality.
proof idea
one-line wrapper that applies two_cube_equicardinal to pauli_has_2cube and tick_has_2cube
why it matters
This result supports the C14 universality claim that the 2^3 count appears identically in the Pauli group and the 8-tick period. It aligns with the eight-tick octave (T7) and D = 3 from the forcing chain. No open questions are directly addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.