no_shorter_cycle
plain-language theorem explainer
No bijective cycle of length T exists from Fin T to Fin 8 whenever T is less than 8. Researchers establishing the minimal period for Gray-code cube traversals in discrete ledgers cite this result to close the uniqueness argument for the eight-tick structure. The proof is a short tactic sequence that assumes a bijection, equates cardinalities via Fintype.card_of_bijective, and obtains an immediate contradiction with omega.
Claim. $T < 8$ implies there is no bijective map from a set of cardinality $T$ to a set of cardinality $8$, for any natural number $T$.
background
The Ledger Uniqueness module resolves why the RS ledger must employ an 8-tick cycle by showing that shorter periods cannot complete a Gray-code traversal of the 3D cube. The module's setting is Gap 9, which forces uniqueness of the cycle length once ledger compatibility and Gray-code constraints are imposed. Upstream results supply the definition of T as the natural-number period and the combinatorial notion of compatibility used in related SAT and mechanism-design statements.
proof idea
The tactic proof introduces T and the hypothesis T < 8, then assumes a bijective cycle. It applies Fintype.card_of_bijective to obtain equality of cardinalities between Fin T and Fin 8, simplifies the resulting equation, and invokes omega to derive the contradiction.
why it matters
This result supplies the minimality half of the eight-tick claim, feeding directly into the module's main theorem that any discrete conservative system is isomorphic to the RS ledger with φ, Q₃, and the 8-tick cycle. It corresponds to the T7 eight-tick octave step in the forcing chain and closes the combinatorial objection listed in the module doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.