Automorphisms of star models

Proof of Proposition 4.1, Step 4 (periodic-mesh-calculations.tex): "For D and E, root the tree at the trivalent vertex; for odd A, root it at its middle vertex. Every tree automorphism fixes that root."

• With three arms, every automorphism fixes the centre (fixes_centre_three).
• For a path (one arm), an automorphism is the identity or the reversal of depths (path_aut); a reversal preserving the parity of depths fixes the middle vertex.

theorem MultiplicativeBasisDeformations.nbr_of_some {t : ℕ} {L : Fin t → ℕ} {i : Fin t} {k : Fin (L i + 1)} {y y' : StarV L} (hy : starAdj (some ⟨i, k⟩) y) (hy' : starAdj (some ⟨i, k⟩) y') (hd : starDepth y = starDepth y') : y = y'

A neighbour of an arm vertex has depth one less or one more, and is determined by its depth.

theorem MultiplicativeBasisDeformations.depth_nbr_of_some {t : ℕ} {L : Fin t → ℕ} {i : Fin t} {k : Fin (L i + 1)} {y : StarV L} (hy : starAdj (some ⟨i, k⟩) y) : starDepth y = ↑k ∨ starDepth y = ↑k + 2

theorem MultiplicativeBasisDeformations.fixes_centre_three {t : ℕ} {L : Fin t → ℕ} (ht : t = 3) (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), starAdj a b ↔ starAdj (ρ a) (ρ b)) : ρ none = none

With three arms, every automorphism fixes the centre.

def MultiplicativeBasisDeformations.ofDep (L : Fin 1 → ℕ) (d : ℕ) (hd : d ≤ L 0 + 1) : StarV L

The vertex of a path at a given depth.

theorem MultiplicativeBasisDeformations.starDepth_ofDep {L : Fin 1 → ℕ} (d : ℕ) (hd : d ≤ L 0 + 1) : starDepth (ofDep L d hd) = d

theorem MultiplicativeBasisDeformations.depth_le {L : Fin 1 → ℕ} (x : StarV L) : starDepth x ≤ L 0 + 1

theorem MultiplicativeBasisDeformations.depth_injective {L : Fin 1 → ℕ} : Function.Injective starDepth

theorem MultiplicativeBasisDeformations.adj_ofDep {L : Fin 1 → ℕ} (d : ℕ) (hd : d + 1 ≤ L 0 + 1) : starAdj (ofDep L d ⋯) (ofDep L (d + 1) hd)

theorem MultiplicativeBasisDeformations.path_aut {L : Fin 1 → ℕ} (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), starAdj a b ↔ starAdj (ρ a) (ρ b)) : (∀ (x : StarV L), starDepth (ρ x) = starDepth x) ∨ ∀ (x : StarV L), starDepth (ρ x) + starDepth x = L 0 + 1

Automorphisms of a path: the identity or the reversal of depths.

theorem MultiplicativeBasisDeformations.path_aut_fixed {L : Fin 1 → ℕ} (ρ : StarV L ≃ StarV L) (hρ : ∀ (a b : StarV L), starAdj a b ↔ starAdj (ρ a) (ρ b)) (hpar : ∀ (x : StarV L), starDepth (ρ x) % 2 = starDepth x % 2) : ∃ (x : StarV L), ρ x = x

A parity-preserving automorphism of a path fixes a vertex.