AncestorPivotPrecision.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Exposed products determine all earlier ancestor pivots

A nonbulk coefficient is its fixed label product times a specified set of inserted ancestor pivots. A division loses one power of the frequency product along its branch, rather than one power for every node already visited.

def OAI.Ostmann.ancestorCoefficient line 18
theorem OAI.Ostmann.ancestorCoefficient_modEq line 21
structure OAI.Ostmann.PivotDependencyScheme line 35
Source documentation
Only ancestors occur in a coefficient; their depth is strictly smaller. The order is the preorder in which split products are exposed.
```
structure PivotDependencyScheme (N : ℕ) where
…
```
def OAI.Ostmann.PivotDependencyScheme.leftCoefficient line 45
def OAI.Ostmann.PivotDependencyScheme.rightCoefficient line 48
def OAI.Ostmann.PivotDependencyScheme.equations line 52
Source documentation
The literal integer reversal equation, with the two selected bulk products.
```
def PivotDependencyScheme.equations {N : ℕ} (D : PivotDependencyScheme N)
    (L R p : Fin N → ℤ) : Prop :=
…
```
Mentions: OAI.Ostmann.PivotDependencyScheme

theorem OAI.Ostmann.PivotDependencyScheme.pivot_prefix_precision line 59

Source documentation

Among already exposed nodes, all reconstructed pivots are determined at a precision depending only on their own ancestor depth.

theorem PivotDependencyScheme.pivot_prefix_precision {N : ℕ} (D : PivotDependencyScheme N)
    (R k J : ℕ) (hdepth : ∀ j, D.depth j ≤ k)
    (hs : ∀ j, (D.frequencies j).root ≠ 0)
    (hsR : ∀ j, (D.frequencies j).root.natAbs ∣ R)
    (L₁ R₁ p₁ L₂ R₂ p₂ : Fin N → ℤ)
    (heq₁ : D.equations L₁ R₁ p₁) (heq₂ : D.equations L₂ R₂ p₂)
    (hL : ∀ j, j.val < J → L₁ j ≡ L₂ j [ZMOD (R : ℤ) ^ (k + 2)])
    (hR : ∀ j, j.val < J → R₁ j ≡ R₂ j [ZMOD (R : ℤ) ^ (k + 2)]) :
    ∀ j, j.val < J → p₁ j ≡ p₂ j [ZMOD (R : ℤ) ^ (k + 1 - D.depth j)] := by
…

Mentions: OAI.Ostmann.PivotDependencyScheme

theorem OAI.Ostmann.PivotDependencyScheme.coefficients_prefix_precision line 109

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.coefficients_prefix_precision {N : ℕ}
    (D : PivotDependencyScheme N) (R k : ℕ) (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.equations L₁ R₁ p₁) (heq₂ : D.equations 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