MovingFullResidues.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The full moving support as one explicit residue mask

def OAI.Ostmann.movingSquareLineSupport line 10
theorem OAI.Ostmann.movingSquareLineSupport_modEq line 17
def OAI.Ostmann.movingFullResidueSupport line 34
Source documentation
All terms here are periodic; the mutual top-giant gcd is kept outside.
```
noncomputable def movingFullResidueSupport {σ : Type*} (value : σ → ℕ) (outside : List ℕ)
    {n : ℕ} (T : MovingSlotData σ n) (XL XR : ℤ) : Prop :=
…
```
Mentions: OAI.Ostmann.MovingSlotData
theorem OAI.Ostmann.movingFullResidueSupport_modEq line 39

theorem OAI.Ostmann.movingFullSupport_residue_iff line 53

Source documentation

The manuscript's pairwise, outside-list and all-subtree-frequency tests are identified exactly, on the integral support already forced by the weight.

theorem movingFullSupport_residue_iff {σ : Type*} (tier : σ → ℕ) (value : σ → ℕ)
    (hprime : ∀ i, (value i).Prime) (hdisjoint : ∀ i j, tier i ≠ tier j → value i ≠ value j)
    (outside : List ℕ) {n : ℕ} (T : MovingSlotData σ n)
    (hlevels : T.Levels tier) (hcoh : T.RegularCoherent) (hc : T.CompensationPrimeData value)
    (hf : T.Frequencies (· ≠ 0))
    (hsmall : ∀ i, T.Frequencies (fun s => IsCoprime s (value i : ℤ)))
    (hfmod : ∀ i, T.Frequencies (fun s => (s : ZMod (value i)) ≠ 0))
    (XL XR a b : ℕ) (M : ℤ) (hI : T.Integral value XL XR)
    (hunit : movingGiantUnitPeriod value outside T ∣ M)
    (hsquare : ∀ o ∈ T.occurrences, ∀ i ∈ o.current.compensationSlots, (value i ^ 2 : ℤ) ∣ M)
    (hL : (XL : ℤ) ≡ (a : ℤ) [ZMOD M]) (hR : (XR : ℤ) ≡ (b : ℤ) [ZMOD M]) :
    (movingFullOutsidePairwise value outside T XL XR ∧ movingNaturalGiantUnits value outside T XL XR) ↔
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingGiantUnitPeriod, OAI.Ostmann.movingFullOutsidePairwise, OAI.Ostmann.movingNaturalGiantUnits