CompensatedPivotPrecision.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exposed-prefix precision for the actual compensation-divided pivots

The new giant is N/(s U), where U is the product of the sampled compensation primes. Its being a unit at the frequency modulus costs no additional power of that modulus.

def OAI.Ostmann.PivotDependencyScheme.compensatedEquations line 17
Source documentation
The equation of the moving construction, keeping its compensation product instead of replacing the new giant by a composite pivot.
```
def PivotDependencyScheme.compensatedEquations {N : ℕ} (D : PivotDependencyScheme N)
    (U L R p : Fin N → ℤ) : Prop :=
…
```
Mentions: OAI.Ostmann.PivotDependencyScheme
theorem OAI.Ostmann.PivotDependencyScheme.compensated_pivot_prefix_precision line 23

theorem OAI.Ostmann.PivotDependencyScheme.compensated_coefficients_prefix_precision line 72

Source documentation

Before the current split is exposed, both coefficients are already known modulo its root frequency. This is the measurability step needed by the sequential uniform-root count.

theorem PivotDependencyScheme.compensated_coefficients_prefix_precision {N : ℕ}
    (D : PivotDependencyScheme N) (R k : ℕ) (U : Fin N → ℤ)
    (hU : ∀ i, IsCoprime (U i) (R : ℤ)) (j : Fin N)
    (hdepth : ∀ i, D.depth i ≤ k) (hs : ∀ i, (D.frequencies i).root ≠ 0)
    (hsR : ∀ i, (D.frequencies i).root.natAbs ∣ R)
    (L₁ R₁ p₁ L₂ R₂ p₂ : Fin N → ℤ)
    (heq₁ : D.compensatedEquations U L₁ R₁ p₁) (heq₂ : D.compensatedEquations U L₂ R₂ p₂)
    (hL : ∀ i, i.val < j.val → L₁ i ≡ L₂ i [ZMOD (R : ℤ) ^ (k + 2)])
    (hR : ∀ i, i.val < j.val → R₁ i ≡ R₂ i [ZMOD (R : ℤ) ^ (k + 2)]) :
    D.leftCoefficient p₁ j ≡ D.leftCoefficient p₂ j [ZMOD (D.frequencies j).root.natAbs] ∧
      D.rightCoefficient p₁ j ≡ D.rightCoefficient p₂ j [ZMOD (D.frequencies j).root.natAbs] := by
…

Mentions: OAI.Ostmann.PivotDependencyScheme