OAI/NumberTheory/Ostmann/Arithmetic/MovingPairwiseSupport.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.MovingSlotData.currentSlots line 10
2. def OAI.Ostmann.MovingSlotData.CurrentPairwise line 14
3. theorem OAI.Ostmann.parent_current_perm line 18
4. theorem OAI.Ostmann.child_current_perm line 28
5. theorem OAI.Ostmann.moving_node_pairwise_iff line 41

   Source documentation

   The local equivalence is stated on the actual child states. Slot coherence is available for every buildMovingSlotData by construction.

   theorem moving_node_pairwise_iff {σ : Type*} (value : σ → ℕ) {n : ℕ}
       (s : ℤ) (CL CR U : List σ) (left right : MovingSlotData σ n)
       (hcoh : (.node s CL CR U left right : MovingSlotData σ (n + 1)).RegularCoherent)
       (XL XR : ℕ)
       (hold : (.node s CL CR U left right : MovingSlotData σ (n + 1)).CurrentPairwise value XL XR)
       (hv : IsCoprime left.frequency (XL * MovingSlotReversal.naturalProduct value CL : ℤ))
       (hw : IsCoprime right.frequency (XR * MovingSlotReversal.naturalProduct value CR : ℤ))
       (hI : (MovingSlotData.step s CL CR U left right false).IntegralAt value (XL, XR)) :
       let p := (MovingSlotData.step s CL CR U left right false).naturalPivot value XL XR
   …

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

6. def OAI.Ostmann.MovingSlotData.CrossFrequencyUnits line 69

   Source documentation

   Cross-branch frequency tests are retained explicitly at every node.

   def MovingSlotData.CrossFrequencyUnits {σ : Type*} (value : σ → ℕ) :
       {n : ℕ} → MovingSlotData σ n → ℕ → ℕ → Prop
     | _, .leaf _ _, _, _ => True
     | _, .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

7. def OAI.Ostmann.MovingSlotData.FullPairwise line 78
8. def OAI.Ostmann.MovingSlotData.NewCompensationUnits line 85
9. theorem OAI.Ostmann.MovingSlotData.fullPairwise_iff line 96

   Source documentation

   Full pairwise coprimality down the original moving tree is equivalent to top coprimality and the new compensation tests. Integral reconstruction and all cross-frequency tests remain hypotheses on these exact states.

   theorem MovingSlotData.fullPairwise_iff {σ : Type*} (value : σ → ℕ) {n : ℕ}
       (T : MovingSlotData σ n) (hcoh : T.RegularCoherent) (XL XR : ℕ)
       (hI : T.Integral value XL XR) (hfreq : T.CrossFrequencyUnits value XL XR) :
       T.FullPairwise value XL XR ↔ T.CurrentPairwise value XL XR ∧ T.NewCompensationUnits value XL XR := by
   …

   Mentions: OAI.Ostmann.MovingSlotData