OAI/NumberTheory/TwoPoint/Walks/ProhibitedCircuit.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

The actual deleted event is a finite depth-two DNF of prime tests.

  1. def OAI.TwoPointCorrelations.AC0Circuit.finiteDNF line 18

    Source documentation

    One conjunction for each accepted numerical word.

    noncomputable def finiteDNF {W : Type*} [Fintype W] (T : W → Type*) [∀ w, Fintype (T w)]
    {n : ℕ} (input : ∀ w, T w → Fin n) : AC0Circuit n :=
…

    Mentions: OAI.TwoPointCorrelations.AC0Circuit

  2. lemma OAI.TwoPointCorrelations.AC0Circuit.finiteDNF_eval line 24
  3. lemma OAI.TwoPointCorrelations.AC0Circuit.finiteDNF_depth line 37
  4. lemma OAI.TwoPointCorrelations.AC0Circuit.finiteDNF_size line 47
  5. abbrev OAI.TwoPointCorrelations.StepAlphabet line 58

    Source documentation

    Finite numerical alphabet: an orientation and an admissible tuple/padding pair.

    abbrev StepAlphabet (pairs : Finset (ℕ × ℕ)) := Bool × pairs
  6. def OAI.TwoPointCorrelations.decodeStep line 60
  7. abbrev OAI.TwoPointCorrelations.BoundedStepWords line 63
  8. def OAI.TwoPointCorrelations.decodeStepWord line 66
  9. lemma OAI.TwoPointCorrelations.decodeStepWord_length line 69
  10. lemma OAI.TwoPointCorrelations.stepWord_covered line 73
  11. abbrev OAI.TwoPointCorrelations.ProhibitedCatalog line 86
  12. abbrev OAI.TwoPointCorrelations.ProhibitedWordTests line 90
  13. abbrev OAI.TwoPointCorrelations.ProhibitedInputs line 96
  14. def OAI.TwoPointCorrelations.prohibitedInputIndex line 99
  15. def OAI.TwoPointCorrelations.prohibitedCircuit line 103
  16. def OAI.TwoPointCorrelations.prohibitedInputAt line 107
  17. lemma OAI.TwoPointCorrelations.prohibitedInputAt_index line 112
  18. lemma OAI.TwoPointCorrelations.squarefree_divisor_iff line 120
  19. lemma OAI.TwoPointCorrelations.positiveWord_iff_prime_tests line 134
  20. theorem OAI.TwoPointCorrelations.prohibitedCircuit_correct line 147

    Source documentation

    The circuit accepts precisely the manuscript's deleted event, not a larger class of arbitrary positive paths. Minimal words are preselected.

    theorem prohibitedCircuit_correct (pairs : Finset (ℕ × ℕ)) (h s : ℕ) (n : ℤ)
    (hsq : ∀ dq ∈ pairs, Squarefree (dq.2 * dq.1)) :
    (prohibitedCircuit pairs h s).eval (prohibitedInputAt pairs h s n) = true ↔
      ProhibitedSite h s (fun d q => (d, q) ∈ pairs) n := by
…

    Mentions: OAI.TwoPointCorrelations.prohibitedCircuit, OAI.TwoPointCorrelations.prohibitedInputAt, OAI.TwoPointCorrelations.ProhibitedSite

  21. theorem OAI.TwoPointCorrelations.prohibitedCircuit_depth line 176
  22. theorem OAI.TwoPointCorrelations.prohibitedCircuit_size line 179
  23. theorem OAI.TwoPointCorrelations.card_boundedStepWords_le line 184
  24. theorem OAI.TwoPointCorrelations.card_prohibitedWordTests_le line 199
  25. theorem OAI.TwoPointCorrelations.prohibitedCircuit_size_le line 219

    Source documentation

    An explicit size bound, including every input occurrence. The only numerical data are the finite step alphabet and its prime-factor cap.

    theorem prohibitedCircuit_size_le (pairs : Finset (ℕ × ℕ)) (h s M : ℕ)
    (hM : ∀ dq ∈ pairs, (dq.2 * dq.1).primeFactors.card ≤ M) :
    (prohibitedCircuit pairs h s).size ≤
      1 + ((s + 1) * (max 1 (2 * pairs.card)) ^ s) * (1 + s * M) := by
…

    Mentions: OAI.TwoPointCorrelations.prohibitedCircuit