OAI/NumberTheory/TwoPoint/Walks/ProhibitedWordCircuit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The surviving-site mask for every departure of one closed word is an actual small circuit. Each complemented prohibited DNF keeps its original prime input occurrences.

  1. def OAI.TwoPointCorrelations.prohibitedWordKeepCircuit line 17
  2. lemma OAI.TwoPointCorrelations.prohibitedWordKeepCircuit_eval line 22
  3. lemma OAI.TwoPointCorrelations.prohibitedWordKeepCircuit_depth line 36
  4. lemma OAI.TwoPointCorrelations.prohibitedWordKeepCircuit_size line 44
  5. lemma OAI.TwoPointCorrelations.prohibitedWordKeepCircuit_size_budget line 57
  6. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.prohibited_input_mem line 89

    Source documentation

    Every literal in the numerical prohibited-word DNF uses a prime in its actual tuple-or-padding pool.

    lemma ProhibitedPrimeFamily.prohibited_input_mem {h J M : ℕ}
    (data : ProhibitedPrimeFamily h J M) (s : ℕ)
    (i : ProhibitedInputs data.pairs h s) : i.2.2.val ∈ data.P ∪ data.Q := by
…

    Mentions: OAI.TwoPointCorrelations.ProhibitedPrimeFamily, OAI.TwoPointCorrelations.ProhibitedInputs

  7. def OAI.TwoPointCorrelations.ProhibitedPrimeFamily.prohibitedLiteral line 97
  8. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.prohibitedLiteral_integer_input line 105