MovingRootReconstruction.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The integer substitution is the giant in the original node coefficient

theorem OAI.Ostmann.reconstructedPivot_compensation line 13
Source documentation
The composite pivot reconstructed by the history system is the compensation product times the reconstructed giant.
```
theorem reconstructedPivot_compensation (I : Finset ℕ) (N s : ℤ) (U : ℕ)
    (h : validTransferredPivot I N (s * U)) :
    reconstructedPivot N s = reconstructedPivot N (s * U) * U := by
…
```
Mentions: OAI.Ostmann.validTransferredPivot, OAI.Ostmann.reconstructedPivot
theorem OAI.Ostmann.reconstructedGiant_eq_div line 24
theorem OAI.Ostmann.validTransferredGiant_of_composite line 31
Source documentation
Conversely the original composite-pivot integrality test gives exactly one positive giant in the retained integer range.
```
theorem validTransferredGiant_of_composite (I : Finset ℕ)
    (N s : ℤ) (P U : ℕ) (hs : s ≠ 0) (hP : 0 < P) (hU : 0 < U)
    (hdiv : U ∣ P) (hI : P / U ∈ I) (hrel : N = s * P) :
    validTransferredPivot I N (s * U) := by
…
```
Mentions: OAI.Ostmann.validTransferredPivot

theorem OAI.Ostmann.movingOriginalNode_reconstructed line 50

Source documentation

The node's original factor is exactly U φ(log p - G), where p is reconstructed from the same signed quotient as the integer off-diagonal.

theorem movingOriginalNode_reconstructed {σ : Type*}
    (value : σ → ℕ) (childBound pivotBound : ℕ → ℕ)
    (φ : ℝ → ℝ) (G : ℕ → ℝ) (I : Finset ℕ) (hI : ∀ p ∈ I, 0 < p)
    (x : MovingSlotState σ) (s v w : ℤ)
    (hU : 0 < x.compensation value)
    (h : validTransferredPivot I
      (v * (x.rightProduct value : ℤ) - w * (x.leftProduct value : ℤ))
      (s * x.compensation value)) :
    movingSlotCutoff value childBound pivotBound
      (movingCompensatedExtra value (movingOriginalNode value childBound pivotBound φ G))
        x s v w =
      (x.compensation value : ℝ) * φ
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.validTransferredPivot, OAI.Ostmann.movingSlotCutoff, OAI.Ostmann.movingCompensatedExtra, OAI.Ostmann.movingOriginalNode

theorem OAI.Ostmann.movingSampleRootFactor_reconstructed line 84

Source documentation

An unconditional node formula in terms of the reconstructed giant. All original frequency, range, and coprimality tests remain in the guard.

theorem movingSampleRootFactor_reconstructed {σ : Type*}
    (value : σ → ℕ) (childBound pivotBound : ℕ → ℕ)
    (φ : ℝ → ℝ) (G : ℕ → ℝ) (n : ℕ)
    (t : FrequencyTree ℤ (n + 1)) (CL CR u : List σ) (XL XR : ℕ) :
    let x := movingRootState n t CL CR u XL XR
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.movingRootState

theorem OAI.Ostmann.movingSampleRootFactor_guarded line 152

Source documentation

The full current-state support guard commutes with root extraction. Its subtree-frequency unit tests are not discarded by the integer change of variables.

theorem movingSampleRootFactor_guarded {σ : Type*}
    (value : σ → ℕ) (outside : List ℕ) (childBound pivotBound : ℕ → ℕ)
    (E : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ) (n : ℕ)
    (t : FrequencyTree ℤ (n + 1)) (CL CR u : List σ) (XL XR : ℕ) :
    movingSampleRootFactor value childBound pivotBound (movingGuardedExtra value outside E)
      n t CL CR u XL XR =
      if movingLocalSupport value outside (movingRootState n t CL CR u XL XR) then
        movingSampleRootFactor value childBound pivotBound E n t CL CR u XL XR else 0 := by
…

Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.FrequencyTree, OAI.Ostmann.movingSampleRootFactor, OAI.Ostmann.movingGuardedExtra, OAI.Ostmann.movingLocalSupport, OAI.Ostmann.movingRootState