OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanTiledSourceEndpoints.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.source_linked_endpoints line 61

   Source documentation

   The selected prefixes agree with the first probe, tile anchor and second probe in the original source-cell coordinates.

   theorem TiledProbeChainData.source_linked_endpoints
       (hchartN : ∀ v, chartN v = F.ExpN v)
       (k u : ℕ → F.N.carrier) (hφ : ∀ n z, ι (φ n z) = k n * ι z * (k n)⁻¹)
       (S : ℕ → MulAut F.N.carrier)
       (E' : Fin 3 → Set W) (γ : M.Bases) (t' : Fin M.letterCount → ℝ)
       (P : ∀ j, M.BoxProbeChains T F hunimod eW bN (E' j) γ t' scale
         (fun n (y : Y n) => S n (D.probe n j (ψ n y))))
       (origin base : ℕ → cartanRootIdeal H) (ε : ℕ → ℝ)
       (L : M.LinkedProbeChains T F hunimod eW bN E' γ t' scale
         (fun j n (y : Y n) => S n (D.probe n j (ψ n y))) P
         (fun n _ => origin n) (fun n _ => base n) ε)
       (horigin : ∀ n, F.ExpN (F.N.equiv (origin n)) = u n)
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal