ComparisonRelationSelection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Exact triangular comparison systems selected from positive witness words.

theorem OAI.TwoPointCorrelations.select_earlier_comparison_relations line 13

Source documentation

Earlier partners give a comparison system ordered by increasing attachment, with the actual private labels as selected variables.

theorem select_earlier_comparison_relations {n h : ℕ} {ι : Type*} [DecidableEq ι]
    (main : LabeledPrimeWord ι) (word : Fin n → LabeledPrimeWord ι)
    (value : ι → ℕ) (hinj : Function.Injective value) (hprime : ∀ j, (value j).Prime)
    (hm : main.Realizes value) (hw : ∀ i, (word i).Realizes value)
    (hsq : ∀ i t, t ∈ (word i).word → Squarefree t.tuple)
    (mark : Fin n → ι) (attachment position : Fin n → ℕ)
    (horder : Monotone attachment) (hbound : ∀ i, attachment i ≤ main.word.length)
    (hprivate : ∀ i j, j ≠ i → value (mark i) ∉ wordPrimeSupport (word j).word)
    (hmain : ∀ i v, TuplePrimeAt main.word (value (mark i)) v → v = position i)
    (x : ℤ) (hpositive : ∀ i, PositiveWord h (x + wordDisplacement h
      (main.word.take (attachment i))) (word i).word)
    (R : Finset (Fin n)) (partner : R → Fin n) (hpartner : ∀ i, partner i < i.val)
…

Mentions: OAI.TwoPointCorrelations.LabeledPrimeWord, OAI.TwoPointCorrelations.wordPrimeSupport, OAI.TwoPointCorrelations.TuplePrimeAt, OAI.TwoPointCorrelations.PositiveWord, OAI.TwoPointCorrelations.wordDisplacement

theorem OAI.TwoPointCorrelations.select_later_comparison_relations line 85

Source documentation

Later partners give the same system in the reverse witness order. The selected contribution changes sign, which preserves nondivisibility.

theorem select_later_comparison_relations {n h : ℕ} {ι : Type*} [DecidableEq ι]
    (main : LabeledPrimeWord ι) (word : Fin n → LabeledPrimeWord ι)
    (value : ι → ℕ) (hinj : Function.Injective value) (hprime : ∀ j, (value j).Prime)
    (hm : main.Realizes value) (hw : ∀ i, (word i).Realizes value)
    (hsq : ∀ i t, t ∈ (word i).word → Squarefree t.tuple)
    (mark : Fin n → ι) (attachment position : Fin n → ℕ)
    (horder : Monotone attachment) (hbound : ∀ i, attachment i ≤ main.word.length)
    (hprivate : ∀ i j, j ≠ i → value (mark i) ∉ wordPrimeSupport (word j).word)
    (hmain : ∀ i v, TuplePrimeAt main.word (value (mark i)) v → v = position i)
    (x : ℤ) (hpositive : ∀ i, PositiveWord h (x + wordDisplacement h
      (main.word.take (attachment i))) (word i).word)
    (R : Finset (Fin n)) (partner : R → Fin n) (hpartner : ∀ i, i.val < partner i)
…