CartanPolarTiledSamplers.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Counted polar samplers from the actual inside-letter flow

structure OAI.PolycyclicRecognition.CartanWordModel.PolarTiledSamplerData line 39
Source documentation
A single source partition retains its exact count and all three actual samplers. The logarithmic chain coordinates are supplied by the proved box construction, not chosen as additional input.
```
structure PolarTiledSamplerData
    (ExpI : M.coneWordIdeal C → I) (ι : I →* F.N.carrier)
    (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (ε : ℝ) (β : M.ConeIdealBases C) (R : ℝ) (scale : ℕ → ℝ)
    (φ : ℕ → I ≃ₜ* I) where
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

theorem OAI.PolycyclicRecognition.CartanWordModel.PolarTiledSamplerData.largest_width_chains line 67

Source documentation

The largest normalized template is a common reference box for the three chains. This equality uses its actual polar support widths.

theorem PolarTiledSamplerData.largest_width_chains
    (ExpI : M.coneWordIdeal C → I) (ι : I →* F.N.carrier)
    (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    {ε : ℝ} (hε : 0 ≤ ε) (β : M.ConeIdealBases C) (R : ℝ) (scale : ℕ → ℝ)
    (φ : ℕ → I ≃ₜ* I)
    (D : M.PolarTiledSamplerData T F hunimod eW K ExpI ι bN ε β R scale φ) :
    Nonempty (∀ k, M.BoxProbeChains T F hunimod eW bN (normalizedPolarTemplates K ε k)
      D.ambient ((M.supportIn T hunimod eW).weightSupport (normalizedPolarTemplates K ε 1))
      scale (fun n => D.chain.probe n k)) := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.normalizedPolarTemplates

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_polar_tiled_samplers line 86
Source documentation
The published exponential inputs and the proved inside-letter tiling give actual counted samplers after deleting a finite initial segment of the scales. No partition, anchor, chain, or exceptional-scale replacement is assumed.
```
theorem exists_polar_tiled_samplers
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput