TriangularRealizationInput.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Published realization inputs for bounded-height packing

J. Dixmier, "L'application exponentielle dans les groupes de Lie résolubles", Bull. Soc. Math. France 85 (1957), 113–121, Theorem 3, p.120: https://www.numdam.org/item/10.24033/bsmf.1483.pdf We retain only the global homeomorphism consequence for real triangular adjoint action, for the intrinsic exponential.
A. Onshuus and S. Post, "A definability criterion for connected Lie groups", Bull. London Math. Soc. 54 (2022), 449–465, Proposition 2.4 and its proof: https://doi.org/10.1112/blms.12574 https://arxiv.org/html/1910.11287v2#S2 We retain a positive triangular realization unipotent on the canonical nilpotent Lie ideal. That ideal is the nilradical by the already proved kernelIdeal_nilpotent and nilpotent_ideal_le_kernelIdeal. The published Lie isomorphism gives the induced topology. Padding a faithful realization with a trivial summand allows a positive matrix size, including dimension zero.

The representation is unipotent on the canonical nilpotent Lie ideal. The resulting height-kernel realization supplies the algebraic data for bounded-height packing. Definability is not required.

def OAI.PolycyclicRecognition.DixmierExponentialInput line 37

Source documentation

The global-chart specialization of Dixmier's real-root criterion.

def DixmierExponentialInput
    {E G : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] [TopologicalSpace G] [ChartedSpace E G] [Group G]
    [LieGroup (𝓘(ℝ, E)) ⊤ G] [SimplyConnectedSpace G] : Prop :=
…

def OAI.PolycyclicRecognition.OnshuusPostRealizationInput line 53
Source documentation
The part of the published triangular realization needed by this proof. Unipotence is required only for exponentials of the actual canonical ideal.
```
def OnshuusPostRealizationInput [SimplyConnectedSpace G] : Prop :=
…
```
theorem OAI.PolycyclicRecognition.polynomialBoundedChainPacking_of_published_realization line 65
Source documentation
The canonical-height packing property now follows from the precise published exponential and representation inputs and the proved matrix packing estimates. No geometric packing premise remains.
```
theorem polynomialBoundedChainPacking_of_published_realization
    (dixmier : DixmierExponentialInput (E := E) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.DixmierExponentialInput