OAI/NumberTheory/Ostmann/Arithmetic/MovingArithmeticSupport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.MovingSlotReversal.giantFormula_of_composite line 10
2. def OAI.Ostmann.MovingSlotData.ArithmeticSupport line 31

   Source documentation

   This support is exactly the original node validity together with the sampled compensation division. It also specifies the actual child giants.

   def MovingSlotData.ArithmeticSupport {σ : Type*} (value : σ → ℕ)
       (childBound pivotBound : ℕ → ℕ) :
       {n : ℕ} → MovingSlotData σ n → ℕ → ℕ → Prop
     | _, .leaf _ _, _, _ => True
     | n + 1, .node s CL CR u left right, XL, XR =>
         ∃ Q : ℕ, ValidTransferNode (movingSlotSystem value childBound pivotBound)
             ⟨n + 1, .node s CL CR u left right, XL, XR⟩ s left.frequency right.frequency Q ∧
           MovingSlotReversal.naturalProduct value u ∣ Q ∧
           left.ArithmeticSupport value childBound pivotBound (Q / MovingSlotReversal.naturalProduct value u) XL ∧
           right.ArithmeticSupport value childBound pivotBound (Q / MovingSlotReversal.naturalProduct value u) XR
   
   /-- The finite list of rational formulas characterizes every original

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

3. theorem OAI.Ostmann.MovingSlotData.formulaNodes_iff line 45

   Source documentation

   The finite list of rational formulas characterizes every original arithmetic condition. In particular the reverse implication retains the compensation divisibility; no new support assumption is introduced.

   theorem MovingSlotData.formulaNodes_iff {σ : Type*} (value : σ → ℕ)
       (hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ) {n : ℕ}
       (T : MovingSlotData σ n) (hf : T.Frequencies (· ≠ 0)) (XL XR : ℕ)
       (L R : HistoryFormula Bool) (a : Bool → ℤ)
       (hL : L.value (fun b => (a b : ℚ)) = (XL : ℚ))
       (hR : R.value (fun b => (a b : ℚ)) = (XR : ℚ)) :
       (∀ f ∈ T.formulaNodes value hvalue childBound pivotBound hf L R,
         f.guard.ValidAt a ∧ f.newGiant.IntegralAt a) ↔
         T.ArithmeticSupport value childBound pivotBound XL XR := by
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.HistoryFormula