TemplateConeTraceSeparation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual transformed pure-word traces determine the offset

theorem OAI.PolycyclicRecognition.eq_of_transformed_pure_word_trace_inequalities line 19

Source documentation

Apply the forward and reversed volume tests to the same transformed ray quotient and to each independent two-ray quotient. The positive pure-word multiplicities then force equality of the original offsets.

theorem eq_of_transformed_pure_word_trace_inequalities
    (D : SupportDatum W I B) (A : templateSymmetryGroup D)
    (hne : ∀ i, D.weight i ≠ 0) (j : I)
    (cRay : I → ℕ) (cTwo : I → I → ℕ)
    (houtRay : ∀ i, (D.weight i).toContinuousLinearMap ∉
      transformedPolarCone (closedWeightRay (D.weight j).toContinuousLinearMap
        (by simpa using hne j)) A.val → cRay i = 0)
    (hinRay : ∀ i, (D.weight i).toContinuousLinearMap ∈
      transformedPolarCone (closedWeightRay (D.weight j).toContinuousLinearMap
        (by simpa using hne j)) A.val → 0 < cRay i)
    (houtTwo : ∀ k (h : LinearIndependent ℝ
        ![(D.weight j).toContinuousLinearMap, (D.weight k).toContinuousLinearMap]),
…

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