CartanNormalizedNeighborStep.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The original neighboring step in the inward-pivot coordinates

This identifies the actual inside-letter flow used by the polar partition. Its exponential rate is proportional to the enlargement parameter; the original subexponential radius is absorbed in one vanishing rate.

theorem OAI.PolycyclicRecognition.normalized_neighbor_amplitude_le line 20

theorem OAI.PolycyclicRecognition.CartanWordModel.normalized_neighbor_step line 46

Source documentation

Pulling the given group step back by the actual dilation gives precisely the exponential of the rescaled original letter.

theorem normalized_neighbor_step
    (S : H → MulAut F.N.carrier)
    (hS : ∀ h v, S h (F.ExpN (F.N.equiv v)) =
      F.ExpN (F.N.equiv (cartanIdealWeightDilation T H h v)))
    (h : H) (i : Fin M.letterCount) (time : ℝ) (step : F.N.carrier)
    (hstep : F.inclusionN step = Exp (time •
      (M.letter i : GroupLieAlgebra (𝓘(ℝ, EG)) G))) :
    (S h).symm step = F.ExpN (F.N.equiv
      ((Real.exp (-M.weight i h) * time) • M.letter i)) := by
…

Mentions: OAI.PolycyclicRecognition.cartanIdealWeightDilation

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_normalized_neighbor_rate line 68

Source documentation

The actual normalized neighbor step satisfies the small-rate bound required by the inside-letter tiling, with no extra amplitude hypothesis.

theorem exists_normalized_neighbor_rate
    (S : H → MulAut F.N.carrier)
    (hS : ∀ h v, S h (F.ExpN (F.N.equiv v)) =
      F.ExpN (F.N.equiv (cartanIdealWeightDilation T H h v)))
    (i : Fin M.letterCount) (pivot : H) (c B δ : ℝ)
    (scale R time : ℕ → ℝ) (hscale : ∀ n, 0 < scale n)
    (hR : HasSubexponentialUpperBoundSeq scale R)
    (step : ℕ → F.N.carrier)
    (hstep : ∀ n, F.inclusionN (step n) = Exp (time n •
      (M.letter i : GroupLieAlgebra (𝓘(ℝ, EG)) G)))
    (htime : ∀ n, |time n| ≤ R n * Real.exp
      ((M.weight i pivot + δ * B) * scale n)) :
…

Mentions: OAI.PolycyclicRecognition.cartanIdealWeightDilation, OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq