FiniteLabelReflection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A reflected direction for two distinct finite labels agreeing on a facet

The invariant Euclidean norm is pulled back from the finite orbit embedding, only inside the proof. The height space keeps its original norm and topology.

theorem OAI.PolycyclicRecognition.exists_reflected_direction_of_finite_labels_of_embedding line 24

Source documentation

Distinct finite labels fixing the same affine facet have an outward direction on which their images are opposite. The hypothesis here is just agreement of their linear parts along the facet kernel.

theorem exists_reflected_direction_of_finite_labels_of_embedding
    (Γ : Subgroup (W ≃ₗ[ℝ] W)) [Fintype Γ]
    (e : W →ₗ[ℝ] E) (he : Function.Injective e)
    (A C : Γ) (hne : A ≠ C) (ℓ : W →ₗ[ℝ] ℝ) (hℓ : ℓ ≠ 0)
    (hfix : ∀ w, ℓ w = 0 → A.val w = C.val w) :
    ∃ v : W, 0 < ℓ v ∧ C.val v = -A.val v := by
…

theorem OAI.PolycyclicRecognition.exists_reflected_direction_of_finite_labels line 70

Source documentation

No Euclidean structure on the height space is required: its finite dimension supplies the auxiliary injective map used in the proof.

theorem exists_reflected_direction_of_finite_labels
    (Γ : Subgroup (W ≃ₗ[ℝ] W)) [Finite Γ]
    (A C : Γ) (hne : A ≠ C) (ℓ : W →ₗ[ℝ] ℝ) (hℓ : ℓ ≠ 0)
    (hfix : ∀ w, ℓ w = 0 → A.val w = C.val w) :
    ∃ v : W, 0 < ℓ v ∧ C.val v = -A.val v := by
…