MovingSpectatorCongruence.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Residue constancy of the actual moving spectator recursion

The extra denominator clears the integer divisions along both children. No coprimality between a spectator prime and a node frequency is required.

def OAI.Ostmann.movingSpectatorDenominator line 16
theorem OAI.Ostmann.movingSpectatorDenominator_ne_zero line 23

theorem OAI.Ostmann.MovingSlotReversal.pivot_modEq line 35

Source documentation

Exact division by the node denominator loses that factor of the input period. Both pivots are the original integer pivots.

theorem MovingSlotReversal.pivot_modEq {σ : Type*} (value : σ → ℕ)
    (hvalue : ∀ i, value i ≠ 0) (s : MovingSlotReversal σ)
    (hs : s.rootFrequency ≠ 0) (XL XR YL YR : ℕ) (m : ℤ)
    (hX : s.IntegralAt value (XL, XR)) (hY : s.IntegralAt value (YL, YR))
    (hL : (XL : ℤ) ≡ (YL : ℤ) [ZMOD
      s.rootFrequency * (naturalProduct value s.compensationSlots : ℤ) * m])
    (hR : (XR : ℤ) ≡ (YR : ℤ) [ZMOD
      s.rootFrequency * (naturalProduct value s.compensationSlots : ℤ) * m]) :
    (s.naturalPivot value XL XR : ℤ) ≡ (s.naturalPivot value YL YR : ℤ) [ZMOD m] := by
…

Mentions: OAI.Ostmann.MovingSlotReversal, OAI.Ostmann.MovingSlotReversal.naturalProduct

theorem OAI.Ostmann.movingSlotSpectator_modEq line 56

Source documentation

On integral histories, the full spectator function is constant on the cleared top residue class, including its zero-at-nonunit convention.

theorem movingSlotSpectator_modEq {σ : Type*} {q : ℕ} [Fact q.Prime]
    (value : σ → ℕ) (hvalue : ∀ i, value i ≠ 0)
    (g : ZMod q → ℂ) (D : (ZMod q)ˣ) {n : ℕ} (T : MovingSlotData σ n)
    (hf : T.Frequencies (· ≠ 0)) (XL XR YL YR : ℕ)
    (hX : T.Integral value XL XR) (hY : T.Integral value YL YR)
    (hL : (XL : ℤ) ≡ (YL : ℤ) [ZMOD (q : ℤ) * movingSpectatorDenominator value T])
    (hR : (XR : ℤ) ≡ (YR : ℤ) [ZMOD (q : ℤ) * movingSpectatorDenominator value T]) :
    movingSlotSpectator value g D T XL XR = movingSlotSpectator value g D T YL YR := by
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingSpectatorDenominator, OAI.Ostmann.movingSlotSpectator

theorem OAI.Ostmann.movingSpectatorDenominator_bound line 111

Source documentation

The extra modulus has only one frequency and one compensation product per internal node. Bulk-list lengths do not enter it.

theorem movingSpectatorDenominator_bound {σ : Type*} (value : σ → ℕ)
    {n : ℕ} (T : MovingSlotData σ n) (B : ℕ)
    (hf : T.Frequencies (fun s => s.natAbs ≤ B))
    (hU : T.CompensationBound value B) :
    (movingSpectatorDenominator value T).natAbs ≤ B ^ (2 * (2 ^ n - 1)) := by
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingSpectatorDenominator

theorem OAI.Ostmann.movingSlotSpectator_norm line 133