OAI/GroupTheory/PolycyclicRecognition/Algebra/GoodFiniteWordVertices.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual good vertices of a successful finite block

  1. theorem OAI.PolycyclicRecognition.WordSheetsGood.take_prod_mem line 12
  2. def OAI.PolycyclicRecognition.finiteWordVertex line 22
  3. theorem OAI.PolycyclicRecognition.finiteWordVertex_zero line 25
  4. theorem OAI.PolycyclicRecognition.finiteWordVertex_last line 29
  5. theorem OAI.PolycyclicRecognition.finiteWordVertex_step line 34
  6. theorem OAI.PolycyclicRecognition.WordSheetsGood.finite_vertices line 41
  7. theorem OAI.PolycyclicRecognition.successful_sample_block_vertices line 47

    Source documentation

    A globally successful sample gives the genuine intermediate states of each block, starting after the product of all preceding blocks.

    theorem successful_sample_block_vertices {h m : ℕ}
    (A : Set G) (sample : ℕ → ℝ → G)
    (hsub : ∀ j s t, sample j s * (sample j t)⁻¹ = sample j (s - t))
    (x : G) (hx : x ∈ A) (t : Fin (h * m + h * m) → ℝ)
    (hs : SwitchSuccessful (fun _ => A) 0 (h * m) x
      (sampledSwitchParameters sample (h * m) t)) (i : Fin h) :
    let start := x * wordPrefix (sampledBlockProducts sample t) i.val
…

    Mentions: OAI.PolycyclicRecognition.SwitchSuccessful, OAI.PolycyclicRecognition.sampledSwitchParameters, OAI.PolycyclicRecognition.wordPrefix, OAI.PolycyclicRecognition.sampledBlockProducts