CartanTiledProbeChains.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous actual chains for the three tiled probe sheets

structure OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData line 31

Source documentation

The joint sampler data, packaged before specializing the templates. This keeps dependent elimination small at the polar-template application.

structure TiledProbeChainData
    (ExpI : M.coneWordIdeal C → I)
    (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (E : Fin 3 → Set W) (β : Fin 3 → M.ConeIdealBases C)
    (ambient : M.Bases) (t : Fin M.letterCount → ℝ) (scale : ℕ → ℝ)
    (φ : ℕ → I ≃ₜ* I) (ι : I →* F.N.carrier)
    (tiles : ℕ → ℕ) (anchor : ∀ n, Fin (tiles n) → I) where
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_tiled_probe_chains line 60
Source documentation
The actual strict-width partitions produce all three measurable generator-chain families. The section and word bases are fixed before the scale sequence; each chain length and prefix bound is uniform in that sequence.
```
theorem exists_tiled_probe_chains
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput
theorem OAI.PolycyclicRecognition.CartanWordModel.nonempty_tiledProbeChainData line 146