CartanPolarConeKernel.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Removing the polar cone vertex without changing the mixed ideal

The polar template uses a closed cone containing zero. The cone quotient must kill the zero generalized weight space to descend the overlapping Cartan factors. Salience and the nonzero generator weights supply this bridge for the same mixed ideal.

theorem OAI.PolycyclicRecognition.closedWeightRay_salient line 23
theorem OAI.PolycyclicRecognition.closedTwoWeightCone_salient line 37
theorem OAI.PolycyclicRecognition.transformedPolarCone_salient line 51
theorem OAI.PolycyclicRecognition.CartanWordModel.coneWordIdeal_eq_of_generator_membership line 76
def OAI.PolycyclicRecognition.CartanWordModel.positiveHeightConePreimage line 85
Source documentation
Pullback cone with its zero height functional removed.
```
def positiveHeightConePreimage (K : ProperCone ℝ (StrongDual ℝ W)) : Set (H →ₗ[ℝ] ℝ) :=
…
```
theorem OAI.PolycyclicRecognition.CartanWordModel.heightConePreimage_add line 90
theorem OAI.PolycyclicRecognition.CartanWordModel.positiveHeightConePreimage_add line 97
theorem OAI.PolycyclicRecognition.CartanWordModel.zero_not_mem_positiveHeightConePreimage line 110
theorem OAI.PolycyclicRecognition.CartanWordModel.coneWordIdeal_positiveHeight_eq line 116
Source documentation
Removing the vertex does not remove any of the nonzero generator weights.
```
theorem coneWordIdeal_positiveHeight_eq (K : ProperCone ℝ (StrongDual ℝ W)) :
    M.coneWordIdeal (positiveHeightConePreimage T eW K) =
      M.coneWordIdeal (heightConePreimage T eW K) := by
…
```
Mentions: OAI.PolycyclicRecognition.CartanWordModel.positiveHeightConePreimage, OAI.PolycyclicRecognition.CartanWordModel.heightConePreimage
theorem OAI.PolycyclicRecognition.CartanWordModel.zero_genWeightSpace_le_polarConeIdeal line 129
Source documentation
The closed polar cone gives the same zero-weight-killing ideal needed to descend the action from the overlapping actual Cartan factors.
```
theorem zero_genWeightSpace_le_polarConeIdeal (K : ProperCone ℝ (StrongDual ℝ W))
    (hK : (K : ConvexCone ℝ (StrongDual ℝ W)).Salient) :
    (genWeightSpace (cartanRootIdeal H) (0 : H → ℝ)).toSubmodule ≤
      (M.coneWordIdeal (heightConePreimage T eW K)).toSubmodule := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.CartanWordModel.heightConePreimage