FacetReflectionTemplates.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual reflected source and target templates

Starting from distinct finite affine labels agreeing near a facet, construct an inward source segment and prove all the support identities in equation (reflection-doubling) of labels.tex.

theorem OAI.PolycyclicRecognition.exists_reflection_templates line 22

theorem OAI.PolycyclicRecognition.exists_relative_facet_neighborhood line 80

Source documentation

Near a point with only parallel active constraints, the entire contact hyperplane remains in the polyhedron.

theorem exists_relative_facet_neighborhood
    (α : J → W →ₗ[ℝ] ℝ) (c : J → ℝ) (p : W) (ℓ : W →ₗ[ℝ] ℝ)
    (hp : ∀ j, α j p ≤ c j)
    (hactive : ∀ j, α j p = c j → ∃ t : ℝ, 0 < t ∧ α j = t • ℓ) :
    ∃ ρ : ℝ, 0 < ρ ∧ ∀ q, ℓ q = ℓ p → ‖q - p‖ < ρ →
      ∀ j, α j q ≤ c j := by
…

theorem OAI.PolycyclicRecognition.affine_labels_eq_of_template_comparison line 104

Source documentation

The reflected source segment contradicts the support inequality obtained from actual coupled bundles. This is the finite-dimensional last step.

theorem affine_labels_eq_of_template_comparison
    (D : SupportDatum W I B) (A C : templateSymmetryGroup D)
    (ℓ : W →ₗ[ℝ] ℝ) (hℓ : ℓ ≠ 0) (b₁ b₂ p : W)
    (α : J → W →ₗ[ℝ] ℝ) (c : J → ℝ) (hp : ∀ j, α j p ≤ c j)
    (hactive : ∀ j, α j p = c j → ∃ t : ℝ, 0 < t ∧ α j = t • ℓ)
    {ρ : ℝ} (hρ : 0 < ρ)
    (hagree : ∀ q, ℓ q = ℓ p → ‖q - p‖ < ρ → A.val q + b₁ = C.val q + b₂)
    (hcompare : ∀ E : Set W, IsCompact E → Convex ℝ E →
      E ⊆ {x | ∀ j, α j x ≤ c j} → p ∈ E →
      D.templateSupport ((A.val '' ((fun x => x - p) '' E)) ∪
        (C.val '' ((fun x => x - p) '' E))) ≤ D.templateSupport E) : A = C := by
…

Mentions: OAI.PolycyclicRecognition.SupportDatum, OAI.PolycyclicRecognition.templateSymmetryGroup