CartanAmbientPacking.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Fixed-slice packing on the constructed ambient Cartan factors

The factor inclusions, normal action and published faithful realization now supply every group-theoretic premise of the fixed-slice lower counting lemma.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_ambient_fixedSlice_packing line 31
Source documentation
Actual ambient fixed-slice lower counting, with no assumed action identification, embedding or Haar invariance.
```
theorem exists_ambient_fixedSlice_packing
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput