Input

theorem EGZ.one_le_hollowConstant {p d : ℕ} (hp : Nat.Prime p) : 1 ≤ hollowConstant p d

A singleton is hollow, so the hollow constant is positive.

def EGZ.MainProof.hollowBound (d : ℕ) : ℕ

A convenient prime-independent upper bound for the hollow constant.

Equations

• EGZ.MainProof.hollowBound d = (2 * d - 1).choose d + 1

theorem EGZ.MainProof.hollowBound_pos (d : ℕ) : 0 < hollowBound d

theorem EGZ.MainProof.normalized_input_bounds {p d : ℕ} [NeZero p] (hp : Nat.Prime p) (hd : 0 < d) {ζ : ℝ} (hζ : 0 < ζ) (hζ1 : ζ ≤ 1) (f : FpCoord p d → ℕ) (hmass : natMass f = ⌈(↑(hollowConstant p d) + ζ) * ↑p⌉₊) : f ≠ 0 ∧ p ≤ natMass f ∧ (↑(hollowConstant p d) + ζ) * ↑p ≤ ↑(natMass f) ∧ ↑(natMass f) ≤ (↑(hollowBound d) + 2) * ↑p

Restricting to the ceiling length gives a uniform bound for input mass divided by the prime. This bound is needed before rounding the weights.