OAI/NumberTheory/Ostmann/Arithmetic/MovingFullSupport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.coprime_naturalProduct line 11
2. theorem OAI.Ostmann.movingNaturalGiantUnits_cross line 20
3. theorem OAI.Ostmann.MovingSlotData.currentPairwise_iff line 41
4. def OAI.Ostmann.movingRegularOutsidePairwise line 53

   Source documentation

   The outside list is fixed while the current regular slots change. These small-slot tests are independent of both top giant values.

   def movingRegularOutsidePairwise {σ : Type*} (value : σ → ℕ) (outside : List ℕ) :
       {n : ℕ} → MovingSlotData σ n → Prop
     | _, T@(.leaf _ _) => (T.regularSlots.map value ++ outside).Pairwise Nat.Coprime
     | _, T@(.node _ _ _ _ left right) =>
         (T.regularSlots.map value ++ outside).Pairwise Nat.Coprime ∧
           movingRegularOutsidePairwise value outside left ∧ movingRegularOutsidePairwise value outside right
   
   /-- Literal pairwise support at every current state, including the fixed
   outside list from the manuscript's recursive average. -/

   Mentions: OAI.Ostmann.MovingSlotData

5. def OAI.Ostmann.movingFullOutsidePairwise line 62

   Source documentation

   Literal pairwise support at every current state, including the fixed outside list from the manuscript's recursive average.

   def movingFullOutsidePairwise {σ : Type*} (value : σ → ℕ) (outside : List ℕ) :
       {n : ℕ} → MovingSlotData σ n → ℕ → ℕ → Prop
     | _, T@(.leaf _ _), XL, XR => (T.currentSlots value XL XR ++ outside).Pairwise Nat.Coprime
     | _, T@(.node s CL CR U left right), XL, XR =>
         let p := (MovingSlotData.step s CL CR U left right false).naturalPivot value XL XR
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingSlotData.step

6. theorem OAI.Ostmann.currentOutsidePairwise_iff line 70
7. theorem OAI.Ostmann.movingFullOutsidePairwise_iff line 88
8. theorem OAI.Ostmann.movingFullOutsidePairwise_square_iff line 103

   Source documentation

   The only nonperiodic coprimality test left after descent is the mutual coprimality of the two top giants. All subtree and outside tests remain.

   theorem movingFullOutsidePairwise_square_iff {σ : Type*} (value : σ → ℕ) (outside : List ℕ)
       {n : ℕ} (T : MovingSlotData σ n) (hcoh : T.RegularCoherent)
       (hc : T.CompensationPrimeData value)
       (hsmall : ∀ i, T.Frequencies (fun s => IsCoprime s (value i : ℤ))) (XL XR : ℕ)
       (hI : T.Integral value XL XR) :
       (movingFullOutsidePairwise value outside T XL XR ∧ movingNaturalGiantUnits value outside T XL XR) ↔
         XL.Coprime XR ∧ movingRegularOutsidePairwise value outside T ∧
           T.PrimeSquareTests value XL XR ∧ movingNaturalGiantUnits value outside T XL XR := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingFullOutsidePairwise, OAI.Ostmann.movingNaturalGiantUnits, OAI.Ostmann.movingRegularOutsidePairwise