OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanTiledSourceChains.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual chains on the quotient/kernel source cell

  1. def OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.sourceChains line 59

    Source documentation

    Pull the stored chains back along the actual source coordinates. No selection of new generator words is needed on the probability cell.

    def TiledProbeChainData.sourceChains (k : Fin 3) :
    M.BoxProbeChains T F hunimod eW bN (E k) ambient t scale
      (fun n (y : Y n) => D.probe n k (ψ n y)) :=
…