OAI/NumberTheory/Ostmann/Arithmetic/MovingTransferSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.moving_reconstructed_node_valid line 14

   Source documentation

   The integer quotient satisfies the full rigidity guard. Its frequency unit is derived from prime sizes, rather than assumed as a new transfer input.

   theorem moving_reconstructed_node_valid {σ : Type*}
       (value : σ → ℕ) (childBound pivotBound : ℕ → ℕ)
       (x : MovingSlotState σ) (I : Finset ℕ) (s v w : ℤ) (V : ℕ)
       (hI : ∀ p ∈ I, 0 < p)
       (h : validTransferredPivot I
         (v * (x.rightProduct value : ℤ) - w * (x.leftProduct value : ℤ))
         (s * x.compensation value))
       (hV : s.natAbs ≤ V)
       (hlarge : ∀ q, q.Prime → q ∣ x.rightProduct value → V < q)
       (hpivot : ∀ p ∈ I, p * x.compensation value ≤ pivotBound x.depth)
       (hv : v.natAbs ≤ childBound x.depth) (hw : w.natAbs ≤ childBound x.depth)
       (hgap : 2 * pivotBound x.depth * childBound x.depth < x.rightProduct value)
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.validTransferredPivot

2. theorem OAI.Ostmann.pairwise_coprime_merge_shared line 57

   Source documentation

   The two branch priors already supply their internal and outside tests. The only new pairwise requirement is the cross-product coprimality.

   theorem pairwise_coprime_merge_shared (A B Y : List ℕ)
       (hA : (A ++ Y).Pairwise Nat.Coprime)
       (hB : (B ++ Y).Pairwise Nat.Coprime) (hAB : A.prod.Coprime B.prod) :
       (A ++ B ++ Y).Pairwise Nat.Coprime := by
   …

3. theorem OAI.Ostmann.moving_transferred_current_pairwise line 76

   Source documentation

   The root's pairwise test follows from the two old branch supports and the nonzero transfer equation, since every shared prime is too large to divide the new frequency.

   theorem moving_transferred_current_pairwise {σ : Type*}
       (value : σ → ℕ) (outside : List ℕ) {n : ℕ}
       (s : ℤ) (CL CR u : List σ) (l r : MovingSlotData σ n) (XL XR P : ℕ)
       (hs : s ≠ 0) (v w : ℤ)
       (hrel : v * ((XR * MovingSlotReversal.naturalProduct value CR : ℕ) : ℤ) -
         w * ((XL * MovingSlotReversal.naturalProduct value CL : ℕ) : ℤ) = s * P)
       (hleft : ((XL :: CL.map value) ++ outside).Pairwise Nat.Coprime)
       (hright : ((XR :: CR.map value) ++ outside).Pairwise Nat.Coprime)
       (hsmall : ∀ q, q.Prime → q ∣ XL * MovingSlotReversal.naturalProduct value CL →
         q ∣ XR * MovingSlotReversal.naturalProduct value CR → s.natAbs < q)
       (hunit : (XL * MovingSlotReversal.naturalProduct value CL).Coprime P) :
       ((MovingSlotData.node s CL CR u l r).currentSlots value XL XR ++ outside).Pairwise
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingSlotReversal.naturalProduct

4. theorem OAI.Ostmann.moving_local_support_of_large line 107

   Source documentation

   All current giant tests, including descendant frequencies, follow from pairwise support and the same large-prime separation used at the root.

   theorem moving_local_support_of_large {σ : Type*}
       (value : σ → ℕ) (outside : List ℕ) {n : ℕ}
       (T : MovingSlotData σ n) (XL XR : ℕ)
       (hp : (T.currentSlots value XL XR ++ outside).Pairwise Nat.Coprime)
       (hf : T.Frequencies (fun s => s ≠ 0 ∧
         ∀ q, q.Prime → q ∣ XL * XR → s.natAbs < q)) :
       movingLocalSupport value outside ⟨n, T, XL, XR⟩ := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingLocalSupport

5. theorem OAI.Ostmann.moving_local_support_prime_giants line 147

   Source documentation

   In the transfer application the surviving top giants are actual primes. All the additional descendant-frequency tests are therefore automatic.

   theorem moving_local_support_prime_giants {σ : Type*}
       (value : σ → ℕ) (outside : List ℕ) {n : ℕ}
       (T : MovingSlotData σ n) (XL XR V : ℕ)
       (hXL : XL.Prime) (hXR : XR.Prime) (hVL : V < XL) (hVR : V < XR)
       (hp : (T.currentSlots value XL XR ++ outside).Pairwise Nat.Coprime)
       (hf : T.Frequencies (fun s => s ≠ 0 ∧ s.natAbs ≤ V)) :
       movingLocalSupport value outside ⟨n, T, XL, XR⟩ := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingLocalSupport