OAI/NumberTheory/Ostmann/Arithmetic/MovingFormulaNodes.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Ostmann.MovingFormulaNode line 10
2. def OAI.Ostmann.MovingSlotData.formulaNodes line 14
3. theorem OAI.Ostmann.MovingSlotData.formulaNodes_length line 30
4. theorem OAI.Ostmann.movingSlotWeight_formulaNodes line 44

   Source documentation

   Every node formula is constructed before the top giants are evaluated. Nonzero original coefficients imply all its exact arithmetic guard and compensation-integrality tests, including both recursive branches.

   theorem movingSlotWeight_formulaNodes {σ : Type*}
       (value : σ → ℕ) (hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ)
       (F : MovingSlotState σ → ℤ → ℂ)
       (extra : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ)
       {n : ℕ} (T : MovingSlotData σ n) (t : FrequencyTree ℤ n) (hT : T.Follows t)
       (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 : ℚ))
       (hw : recursiveTransferWeight (movingSlotSystem value childBound pivotBound) F
         (movingSlotCutoff value childBound pivotBound extra) n ⟨n, T, XL, XR⟩ t ≠ 0) :
       ∀ f ∈ T.formulaNodes value hvalue childBound pivotBound hf L R,
         f.guard.ValidAt a ∧ f.newGiant.IntegralAt a := by
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.HistoryFormula, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.movingSlotSystem, OAI.Ostmann.movingSlotCutoff