ModularCompensatedPrecision.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Prefix precision after retaining only the frequency congruences

The frequency model in the arithmetic replacement divides by compensation factors modulo the remaining power. Its equations are congruences, with one power lost at each branch level.

def OAI.Ostmann.PivotDependencyScheme.modularCompensatedEquations 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.modularCompensatedEquations {N : ℕ} (D : PivotDependencyScheme N)
    (M : ℤ) (k : ℕ) (U L R p : Fin N → ℤ) : Prop :=
…
```
Mentions: OAI.Ostmann.PivotDependencyScheme
theorem OAI.Ostmann.PivotDependencyScheme.modular_compensated_pivot_prefix_precision line 23

theorem OAI.Ostmann.PivotDependencyScheme.modular_compensated_coefficients_prefix_precision line 73

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.modular_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.modularCompensatedEquations R k U L₁ R₁ p₁) (heq₂ : D.modularCompensatedEquations R k 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