OAI/NumberTheory/TwoPoint/Walks/WitnessSelection.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Selecting a triangular family of witness relations

The finite split in the singleton argument is performed on actual numerical witness words. The comparison alternatives retain the neighboring witness, its control prime, the selected internal departure, and the nonzero private prime contribution at that departure.

  1. def OAI.TwoPointCorrelations.freshActiveBefore line 19
  2. def OAI.TwoPointCorrelations.freshActiveAfter line 23
  3. theorem OAI.TwoPointCorrelations.select_witness_relations line 29

    Source documentation

    The internal active alternative and the two ordered comparison alternatives needed for successive elimination.

    theorem select_witness_relations {n K h s J : ℕ} {supply : ℕ → ℕ → Prop}
    (word : Fin n → List SignedStep) (mark : Fin n → ℕ)
    (attachment position : Fin n → ℕ)
    (hsize : 8 * K ≤ n)
    (hminimal : ∀ i, MinimalWord (ForwardProhibited h s supply) (word i))
    (hsq : ∀ i t, t ∈ word i → Squarefree t.tuple)
    (hcard : ∀ i t, t ∈ word i → t.tuple.primeFactors.card = J)
    (hsupport : ∀ i p j, TuplePrimeAt (word i) p j →
      ¬p ∣ h ∧ ∀ t ∈ word i, ¬p ∣ t.padding)
    (hmark : ∀ i, mark i ∈ wordPrimeSupport (word i))
    (hprivate : ∀ i j, j ≠ i → mark i ∉ wordPrimeSupport (word j)) :
    ∃ R : Finset (Fin n), K ≤ R.card ∧
…

    Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.MinimalWord, OAI.TwoPointCorrelations.ForwardProhibited, OAI.TwoPointCorrelations.TuplePrimeAt, OAI.TwoPointCorrelations.wordPrimeSupport

  4. lemma OAI.TwoPointCorrelations.wordPrimeContribution_zero_of_not_mem line 112
  5. lemma OAI.TwoPointCorrelations.ActivePrime.mem_wordPrimeSupport line 123
  6. theorem OAI.TwoPointCorrelations.select_fresh_before_labels line 134

    Source documentation

    Fresh active labels can be chosen injectively. Earlier internal relations contain none of the later chosen variables.

    theorem select_fresh_before_labels {n h : ℕ} (word : Fin n → List SignedStep)
    (R : Finset (Fin n)) (hsq : ∀ i t, t ∈ word i → Squarefree t.tuple)
    (hfresh : ∀ i ∈ R, freshActiveBefore h word i) :
    ∃ z : R → ℕ, Function.Injective z ∧
      (∀ i : R, ActivePrime h (word i) (z i)) ∧
      ∀ i j : R, i.val < j.val → z j ∉ wordPrimeSupport (word i) := by
…

    Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.freshActiveBefore, OAI.TwoPointCorrelations.ActivePrime, OAI.TwoPointCorrelations.wordPrimeSupport

  7. theorem OAI.TwoPointCorrelations.select_fresh_after_labels line 153

    Source documentation

    The reversed order gives the other internal triangular system.

    theorem select_fresh_after_labels {n h : ℕ} (word : Fin n → List SignedStep)
    (R : Finset (Fin n)) (hsq : ∀ i t, t ∈ word i → Squarefree t.tuple)
    (hfresh : ∀ i ∈ R, freshActiveAfter h word i) :
    ∃ z : R → ℕ, Function.Injective z ∧
      (∀ i : R, ActivePrime h (word i) (z i)) ∧
      ∀ i j : R, j.val < i.val → z j ∉ wordPrimeSupport (word i) := by
…

    Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.freshActiveAfter, OAI.TwoPointCorrelations.ActivePrime, OAI.TwoPointCorrelations.wordPrimeSupport

  8. lemma OAI.TwoPointCorrelations.shared_prime_ne_private line 173

    Source documentation

    A prime shared by two different witnesses is none of their family's private marked primes. This includes the comparison's controlling prime.

    lemma shared_prime_ne_private {n : ℕ} (word : Fin n → List SignedStep)
    (mark : Fin n → ℕ)
    (hprivate : ∀ i j, j ≠ i → mark i ∉ wordPrimeSupport (word j))
    {i j : Fin n} (hij : i ≠ j) {z : ℕ}
    (hi : z ∈ wordPrimeSupport (word i)) (hj : z ∈ wordPrimeSupport (word j)) :
    ∀ k, z ≠ mark k := by
…

    Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.wordPrimeSupport

  9. lemma OAI.TwoPointCorrelations.earlier_comparison_excludes_later line 187

    Source documentation

    In the earlier-comparison case, every later selected private label is absent from both witness prefixes and from the entire main segment.

    lemma earlier_comparison_excludes_later {n : ℕ} (word : Fin n → List SignedStep)
    (mark : Fin n → ℕ) (attachment position : Fin n → ℕ)
    (horder : Monotone attachment)
    (hprivate : ∀ i j, j ≠ i → mark i ∉ wordPrimeSupport (word j))
    {i j k : Fin n} (hji : j < i) (hik : i < k) (hpos : attachment k ≤ position k) :
    mark k ∉ wordPrimeSupport (word i) ∧ mark k ∉ wordPrimeSupport (word j) ∧
      ∀ v ∈ Ico (attachment j) (attachment i), v ≠ position k := by
…

    Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.wordPrimeSupport

  10. lemma OAI.TwoPointCorrelations.later_comparison_excludes_earlier line 202

    Source documentation

    In the later-comparison case, reverse attachment order gives the same absence for every still-to-be-eliminated private variable.

    lemma later_comparison_excludes_earlier {n : ℕ} (word : Fin n → List SignedStep)
    (mark : Fin n → ℕ) (attachment position : Fin n → ℕ)
    (horder : Monotone attachment)
    (hprivate : ∀ i j, j ≠ i → mark i ∉ wordPrimeSupport (word j))
    {i j k : Fin n} (hij : i < j) (hki : k < i) (hpos : position k < attachment k) :
    mark k ∉ wordPrimeSupport (word i) ∧ mark k ∉ wordPrimeSupport (word j) ∧
      ∀ v ∈ Ico (attachment i) (attachment j), v ≠ position k := by
…

    Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.wordPrimeSupport

  11. lemma OAI.TwoPointCorrelations.PositiveWord.comparison_relation line 217

    Source documentation

    Positivity at two departures in the same configuration gives the exact comparison congruence used by the selected triangular systems.

    lemma PositiveWord.comparison_relation {h p ri rj : ℕ} {xi xj : ℤ}
    {wi wj : List SignedStep} (hi : PositiveWord h xi wi) (hj : PositiveWord h xj wj)
    (hpi : TuplePrimeAt wi p ri) (hpj : TuplePrimeAt wj p rj) :
    (p : ℤ) ∣ (xi + wordDisplacement h (wi.take ri)) -
      (xj + wordDisplacement h (wj.take rj)) :=
…

    Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.PositiveWord, OAI.TwoPointCorrelations.TuplePrimeAt, OAI.TwoPointCorrelations.wordDisplacement

  12. lemma OAI.TwoPointCorrelations.wordPrimeContribution_zero_of_avoids line 224
  13. lemma OAI.TwoPointCorrelations.wordPrimeContribution_zero_of_unique_position line 233
  14. lemma OAI.TwoPointCorrelations.PositiveWord.main_comparison_relation line 241
  15. lemma OAI.TwoPointCorrelations.earlier_comparison_private_contribution line 256

    Source documentation

    The private selected prime has exactly its designated nonzero prefix contribution in an earlier comparison; all other contributions vanish.

    lemma earlier_comparison_private_contribution {n h : ℕ}
    (main : List SignedStep) (word : Fin n → List SignedStep) (mark : Fin n → ℕ)
    (attachment position : Fin n → ℕ)
    (hsq : ∀ i t, t ∈ word i → Squarefree t.tuple)
    (hprivate : ∀ i j, j ≠ i → mark i ∉ wordPrimeSupport (word j))
    (hmain : ∀ i v, TuplePrimeAt main (mark i) v → v = position i)
    {i j : Fin n} (hji : j < i) (hpos : attachment i ≤ position i)
    (ri rj : ℕ) :
    wordPrimeContribution h main (mark i) (attachment j) (attachment i) +
      wordPrimeContribution h (word i) (mark i) 0 ri -
      wordPrimeContribution h (word j) (mark i) 0 rj =
      wordPrimeContribution h (word i) (mark i) 0 ri := by
…

    Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.wordPrimeSupport, OAI.TwoPointCorrelations.TuplePrimeAt, OAI.TwoPointCorrelations.wordPrimeContribution

  16. lemma OAI.TwoPointCorrelations.later_comparison_private_contribution line 280

    Source documentation

    The later comparison changes the selected prefix's sign, preserving its nonvanishing modulo the controlling prime.

    lemma later_comparison_private_contribution {n h : ℕ}
    (main : List SignedStep) (word : Fin n → List SignedStep) (mark : Fin n → ℕ)
    (attachment position : Fin n → ℕ)
    (hsq : ∀ i t, t ∈ word i → Squarefree t.tuple)
    (hprivate : ∀ i j, j ≠ i → mark i ∉ wordPrimeSupport (word j))
    (hmain : ∀ i v, TuplePrimeAt main (mark i) v → v = position i)
    {i j : Fin n} (hij : i < j) (hpos : position i < attachment i)
    (ri rj : ℕ) :
    wordPrimeContribution h main (mark i) (attachment i) (attachment j) +
      wordPrimeContribution h (word j) (mark i) 0 rj -
      wordPrimeContribution h (word i) (mark i) 0 ri =
      -wordPrimeContribution h (word i) (mark i) 0 ri := by
…

    Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.wordPrimeSupport, OAI.TwoPointCorrelations.TuplePrimeAt, OAI.TwoPointCorrelations.wordPrimeContribution