ConeTraceSeparation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The ray and two-ray trace tests determine the offset

After the volume comparison in both directions, the ray trace and all independent two-ray traces vanish. Positivity of their coefficients then forces every generator weight to vanish on the offset.

theorem OAI.PolycyclicRecognition.eq_zero_of_ray_two_ray_trace_tests line 20

Source documentation

One ray test and one test for each independent generator weight suffice. Dependent weights require no additional test.

theorem eq_zero_of_ray_two_ray_trace_tests
    (α : W →ₗ[ℝ] ℝ) (hα : α ≠ 0) (β : I → W →ₗ[ℝ] ℝ)
    (hsep : ∀ w : W, (∀ i, β i w = 0) → w = 0)
    (ray : W →ₗ[ℝ] ℝ) (test : I → W →ₗ[ℝ] ℝ)
    (hray : ∃ c : ℝ, 0 < c ∧ ray = c • α)
    (htest : ∀ i, LinearIndependent ℝ ![α, β i] →
      ∃ c d : ℝ, 0 < c ∧ 0 < d ∧ test i = c • α + d • β i)
    (w : W) (hr : ray w = 0)
    (ht : ∀ i, LinearIndependent ℝ ![α, β i] → test i w = 0) : w = 0 := by
…

theorem OAI.PolycyclicRecognition.eq_of_ray_two_ray_trace_inequalities line 49

Source documentation

Applying the same volume test to the reversed pair converts the two inequalities into equality before the trace-separation argument.

theorem eq_of_ray_two_ray_trace_inequalities
    (α : W →ₗ[ℝ] ℝ) (hα : α ≠ 0) (β : I → W →ₗ[ℝ] ℝ)
    (hsep : ∀ w : W, (∀ i, β i w = 0) → w = 0)
    (ray : W →ₗ[ℝ] ℝ) (test : I → W →ₗ[ℝ] ℝ)
    (hray : ∃ c : ℝ, 0 < c ∧ ray = c • α)
    (htest : ∀ i, LinearIndependent ℝ ![α, β i] →
      ∃ c d : ℝ, 0 < c ∧ 0 < d ∧ test i = c • α + d • β i)
    (x y : W) (hr : ray (y - x) ≤ 0) (hr' : ray (x - y) ≤ 0)
    (ht : ∀ i, LinearIndependent ℝ ![α, β i] → test i (y - x) ≤ 0)
    (ht' : ∀ i, LinearIndependent ℝ ![α, β i] → test i (x - y) ≤ 0) : x = y := by
…