OAI/NumberTheory/TwoPoint/Walks/WitnessPrimeSystems.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TwoPointCorrelations.internal_prime_system line 15

   Source documentation

   Bundle an actual fresh-active family into the finite system used by reciprocal elimination.

   theorem internal_prime_system {κ : Type} [Fintype κ] [LinearOrder κ]
       {ι : Type*} [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) :
       ∃ S : OrderedPrimeSystem ι, S.size = Fintype.card κ ∧
         S.Holds (fun z => (value z : ℤ)) := by
   …

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

2. theorem OAI.TwoPointCorrelations.witness_prime_system line 42

   Source documentation

   The actual four-way selection theorem. It assumes the numerical minimality and privacy properties of the witness cover, and constructs all congruences and their later-variable exclusions inside the proof.

   theorem witness_prime_system {n K h s J : ℕ} {supply : ℕ → ℕ → Prop}
       {ι : 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)
       (mark : Fin n → ι) (attachment position : Fin n → ℕ)
       (hsize : 8 * K ≤ n)
       (hminimal : ∀ i, MinimalWord (ForwardProhibited h s supply) (word i).word)
       (hsq : ∀ i t, t ∈ (word i).word → Squarefree t.tuple)
       (hcard : ∀ i t, t ∈ (word i).word → t.tuple.primeFactors.card = J)
       (hsupport : ∀ i p j, TuplePrimeAt (word i).word p j →
         ¬p ∣ h ∧ ∀ t ∈ (word i).word, ¬p ∣ t.padding)
   …

   Mentions: OAI.TwoPointCorrelations.LabeledPrimeWord, OAI.TwoPointCorrelations.MinimalWord, OAI.TwoPointCorrelations.ForwardProhibited, OAI.TwoPointCorrelations.TuplePrimeAt