CartanPolarConeModels.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Published inputs for the finite polar-cone models

This record only groups the already stated nilpotent existence, integration and exponential Haar inputs. It contains no metric or profile conclusion. It is instantiated separately for each ray or two-ray cone used below.

structure OAI.PolycyclicRecognition.CartanWordModel.PolarConeModelInputs line 29
Source documentation
The six published inputs actually used to realize a specified cone. Lee's nilpotent existence/integration and Le Donne's exponential Haar statements retain their original Lean propositions.
```
structure PolarConeModelInputs : Prop where
…
```
def OAI.PolycyclicRecognition.CartanWordModel.PolarConeModelInputs.model line 51
Source documentation
Choose only the concrete measured cone required by the application.
```
def PolarConeModelInputs.model : M.MeasuredCone F C :=
…
```
theorem OAI.PolycyclicRecognition.CartanWordModel.PolarConeModelInputs.model_haarQ line 56
theorem OAI.PolycyclicRecognition.CartanWordModel.PolarConeModelInputs.model_haarI line 62