Shell index packaged as a fixed-size Fin type

Definition

shellFin

by xbgxjack · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

discrepancy-theoryentropy-method

The same shell index as $\mathrm{shellIdx}$ , repackaged as an element of the fixed finite type $\mathrm{Fin}(2m+3)$ (via a shift by $m+1$ and a safety modulus that is never actually triggered once $\Delta\ge 1/2$ ), so that it can be treated as a finite-alphabet random variable and fed to Shannon-entropy machinery such as the pigeonhole bound used in the entropy-method proof of Spencer's discrepancy theorem.

Definition code

import Mathlib
import Definitions.Def_shellIdx

noncomputable def shellFin {m : ℕ} (Δ : ℝ) (a : Fin m → ℝ) (ω : Fin m → Bool) : Fin (2*m+3) :=
  ⟨(shellIdx Δ a ω + (m+1)).toNat % (2*m+3), Nat.mod_lt _ (by omega)⟩

Source

T. Rothvoß, "Discrepancy theory, or: how much balance is possible?", MIT lecture notes, Section 4.1, https://math.mit.edu/classes/18.095/lect6/notes.pdf

Human review

Endorsed by Shuze Chen · Sep 11, 2026
Endorsed by xbgxjack · Sep 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph