CartanPivotCancellation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Cancellation of the scalar height action at the probe pivot

After conjugating back by the Cartan pivot, only its polynomial residual action remains. The root-space calculation is extended to the generated nilpotent ideal, so mixed bracket words are included.

theorem OAI.PolycyclicRecognition.cartanIdealWeightDilation_apply_root line 21
theorem OAI.PolycyclicRecognition.cartan_residual_commutes_dilation line 27
theorem OAI.PolycyclicRecognition.cartan_adjoint_neg_dilation line 45
Source documentation
The height dilation cancels exactly, with no estimate on its size.
```
theorem cartan_adjoint_neg_dilation (h : H) (v : cartanRootIdeal H) :
    cartanIdealAdjointAutomorphism T H (-h) (cartanIdealWeightDilation T H h v) =
      cartanIdealResidualAutomorphism T H (-h) v := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.cartanIdealAdjointAutomorphism, OAI.PolycyclicRecognition.cartanIdealWeightDilation, OAI.PolycyclicRecognition.cartanIdealResidualAutomorphism