MovingRepresentativeSquares.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform square-exclusion loss for each sampled representative prime

abbrev OAI.Ostmann.MovingRepresentativeOccurrences line 10
theorem OAI.Ostmann.movingRepresentativeOccurrences_card line 15
Source documentation
Repetition across nodes costs only the actual number of occurrences.
```
theorem movingRepresentativeOccurrences_card {σ : Type*} {n : ℕ}
    (T : MovingSlotData σ n) (rep : σ) :
    Fintype.card (MovingRepresentativeOccurrences T rep) ≤ 2 ^ n - 1 := by
…
```
Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingRepresentativeOccurrences

theorem OAI.Ostmann.moving_representative_square_loss line 26

Source documentation

All unit and nonzero-row requirements for a representative's lift count follow from the sampled prime types, not from an assumed line system.

theorem moving_representative_square_loss {σ : Type*} (tier : σ → ℕ)
    (value : σ → ℕ) (hprime : ∀ i, (value i).Prime)
    (hdisjoint : ∀ i j, tier i ≠ tier j → value i ≠ value j)
    {n : ℕ} (T : MovingSlotData σ n) (hlevels : T.Levels tier) (rep : σ)
    (hfreq : T.Frequencies (fun s => (s : ZMod (value rep)) ≠ 0))
    (x₀ y₀ : ZMod (value rep)) (hy : y₀ ≠ 0)
    (hbase : ∀ j : MovingRepresentativeOccurrences T rep,
      let o := T.occurrences.get j.val
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingRepresentativeOccurrences