CartanBridgeAbsorption.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Absorbing the conjugated bridge into the second-sheet ideal box

The logarithm of the second Cartan factor can be subexponentially large. Its small height, rather than a bound on its full logarithm, controls the exponential size of the conjugated bridge. Strict ideal widths absorb it.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_conjugated_bridge_ideal_bound line 35

Source documentation

A single subexponential ideal box contains the residual ideal coordinates after every sufficiently small bridge and every allowed second-sheet Cartan factor. The threshold is independent of the scale and of the chosen endpoints.

theorem exists_conjugated_bridge_ideal_bound
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    {I J : Type*} [Fintype I] [Fintype J]
    (bI : Basis I ℝ U) (bQ : Basis J ℝ ((cartanRootIdeal H) ⧸ (M.coneWordIdeal C).toSubmodule))
    (lift : J → cartanRootIdeal H) (hlift : ∀ j, (M.coneWordIdeal C).toSubmodule.mkQ (lift j) = bQ j)
    {N Q : Type*} [Group N] [Group Q]
    (ExpN : cartanRootIdeal H → N) (ExpQ : ((cartanRootIdeal H) ⧸ (M.coneWordIdeal C).toSubmodule) → Q)
    (π : N →* Q) (hπ : ∀ v, π (ExpN v) = ExpQ ((M.coneWordIdeal C).toSubmodule.mkQ v))
    (hinjQ : Function.Injective ExpQ) (hzeroQ : ExpQ 0 = 1)
    (hneg : ∀ v, ExpN (-v) = (ExpN v)⁻¹)
    {c : ℕ} (coeff : DynkinCoefficients c 2)
    (hcoeff : ∀ d w, |coeff d w| ≤ (2 : ℝ) ^ c)
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.DynkinCoefficients