Cardinality of coordinate-rotation orbits

Embed coordinate-rotation cycles in the full normalized Markoff orbit and compare their cardinalities.

noncomputable def BGS.Markoff.normalizedSurfaceRotationCycle {R : Type u} [Field R] [DecidableEq R] (x : NormalizedMarkoffSurface R) : Finset (NormalizedMarkoffSurface R)

The finite segment of normalized surface iterates cut out by the matrix rotation order.

Equations

• BGS.Markoff.normalizedSurfaceRotationCycle x = Finset.image (fun (n : ℕ) => BGS.Markoff.normalizedRotate1Surface^[n] x) (Finset.range (BGS.Markoff.rotationOrder (↑x).u1))

theorem BGS.Markoff.normalizedSurfaceRotationCycle_subset_normalizedGammaOrbit {R : Type u} [Field R] [DecidableEq R] [Invertible 3] (x : NormalizedMarkoffSurface R) : ↑(normalizedSurfaceRotationCycle x) ⊆ normalizedGammaOrbit x

Every point of the normalized rotation cycle belongs to the full transported Gamma orbit.

theorem BGS.Markoff.normalizedSurfaceRotationCycle_image_val {R : Type u} [Field R] [DecidableEq R] (x : NormalizedMarkoffSurface R) : Finset.image Subtype.val (normalizedSurfaceRotationCycle x) = normalizedRotationCycle (↑x).u1 ↑x

Forgetting the surface proof identifies the surface cycle with the existing point cycle.

theorem BGS.Markoff.normalizedSurfaceRotationCycle_card {R : Type u} [Field R] [DecidableEq R] (x : NormalizedMarkoffSurface R) : (normalizedSurfaceRotationCycle x).card = (normalizedRotationCycle (↑x).u1 ↑x).card

Surface and point rotation cycles have the same cardinality.

theorem BGS.Markoff.normalizedRotationCycle_card_le_normalizedGammaOrbit_ncard {R : Type u} [Field R] [Invertible 3] [Finite R] (x : NormalizedMarkoffSurface R) : (normalizedRotationCycle (↑x).u1 ↑x).card ≤ (normalizedGammaOrbit x).ncard

A normalized rotation cycle injects into the full Gamma orbit, so its cardinality is an honest lower bound for the orbit cardinality.