InternalRelationSelection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Actual active witness intervals give a triangular system on the ambient labels.

theorem OAI.TwoPointCorrelations.LabeledPrimeWord.active_relation_with_control line 18

Source documentation

Record also an occurrence of the controlling prime. This proves that later fresh labels cannot occur as an earlier controlling modulus.

theorem active_relation_with_control (w : LabeledPrimeWord ι) (h : ℕ) (value : ι → ℕ)
    (hinj : Function.Injective value) (hprime : ∀ j, (value j).Prime)
    (hw : w.Realizes value) (y : ι) (hy : ActivePrime h w.word (value y)) :
    ∃ c a b r, c ≠ y ∧ a ≤ b ∧ b ≤ w.word.length ∧
      TuplePrimeAt w.word (value c) r ∧
      primeRelationEvent (w.intervalRelation h a b) y c (fun j => (value j : ℤ)) := by
…

Mentions: OAI.TwoPointCorrelations.LabeledPrimeWord, OAI.TwoPointCorrelations.ActivePrime, OAI.TwoPointCorrelations.TuplePrimeAt, OAI.TwoPointCorrelations.primeRelationEvent

theorem OAI.TwoPointCorrelations.select_internal_relations line 43

Source documentation

A family of active primes absent from all earlier witnesses gives actual interval relations, ordered independently of the names of the selected labels. The conclusion includes the controlling-prime exclusion.

theorem select_internal_relations {κ ι : Type*} [Fintype κ] [LinearOrder κ]
    [DecidableEq ι] (word : κ → LabeledPrimeWord ι) (h : ℕ) (value : ι → ℕ)
    (hinj : Function.Injective value) (hprime : ∀ j, (value j).Prime)
    (hw : ∀ i, (word i).Realizes value)
    (hsq : ∀ i t, t ∈ (word i).word → Squarefree t.tuple)
    (active : κ → ℕ) (hactive : ∀ i, ActivePrime h (word i).word (active i))
    (hfresh : ∀ i j, i < j → active j ∉ wordPrimeSupport (word i).word) :
    ∃ selected control : κ → ι, ∃ left right : κ → ℕ,
      Function.Injective selected ∧
      (∀ i, value (selected i) = active i) ∧
      (∀ i, control i ≠ selected i ∧ left i ≤ right i ∧ right i ≤ (word i).word.length ∧
        primeRelationEvent ((word i).intervalRelation h (left i) (right i))
…

Mentions: OAI.TwoPointCorrelations.LabeledPrimeWord, OAI.TwoPointCorrelations.ActivePrime, OAI.TwoPointCorrelations.wordPrimeSupport, OAI.TwoPointCorrelations.primeRelationEvent