Quadratic packing polynomials

DefinitionLattice points of a sector#✓fully proved

For a real number \(\alpha\), let \(S(\alpha) = \{(x, y) \in \mathbb{R}^2 : 0 \le y \le \alpha x\}\) be the sector of slope \(\alpha\). Its lattice points are \(I(\alpha) = S(\alpha) \cap \mathbb{Z}^2\), viewed as a subset of \(\mathbb{R}^2\).

public def sectorLatticePoints (α : ℝ) : Set (ℝ × ℝ) :=
  {p | ∃ x y : ℤ, p = ((x : ℝ), (y : ℝ)) ∧ 0 ≤ (y : ℝ) ∧ (y : ℝ) ≤ α * x}

Sources

• Brandt and Gjaldbæk, Classification of Quadratic Packing Polynomials on Sectors of R^2, INTEGERS 25 (2025), Article A81, Section 1 (definition of S(α) and I(α)).

Used by 12

Used byThe slope-\(12/7\) example on the sheared sector · Sheared criterion for quadratic packing polynomials · Constant term of a quadratic packing polynomial on a rational sector · First step value and sheared form of a quadratic packing polynomial · Step-difference form of a quadratic packing polynomial on a rational sector · Stanton's form of a quadratic packing polynomial on a rational sector · Form of a quadratic packing polynomial on a sector (Gjaldbæk) · Staircase congruence for quadratic packing polynomials · Height of the first step of the k-th staircase · Staircases of a rational sector · The origin is a lattice point of every sector · The origin lies on the zeroth staircase

TheoremThe origin is a lattice point of every sector#✓fully proved

For every real number \(\alpha\), the origin \((0, 0)\) lies in the set \(I(\alpha)\) of lattice points of the sector of slope \(\alpha\).

public theorem zero_mem_sectorLatticePoints (α : ℝ) : ((0 : ℝ), (0 : ℝ)) ∈ sectorLatticePoints α

Sources

• Brandt and Gjaldbæk, Classification of Quadratic Packing Polynomials on Sectors of R^2, INTEGERS 25 (2025), Article A81, Section 1 (definition of I(α)).

Uses 1 · Used by 1

Statement usesLattice points of a sector

Used byThe origin lies on the zeroth staircase

DefinitionQuadratic packing polynomial#✓fully proved

A real function \(P(x, y)\) of two real variables is a quadratic packing polynomial (QPP) on a set \(S \subseteq \mathbb{R}^2\) if it is a polynomial of total degree two, that is, \(P(x, y) = a x^2 + b x y + c y^2 + d x + e y + f\) for some real \(a, b, c, d, e, f\) with \(a, b, c\) not all zero, and \(P\) maps \(S\) bijectively onto the set \(\mathbb{N}_0 = \{0, 1, 2, \dots\}\) of natural numbers.

public def IsQuadraticPackingPolynomial (S : Set (ℝ × ℝ)) (P : ℝ → ℝ → ℝ) : Prop :=
  (∃ a b c d e f : ℝ, (a ≠ 0 ∨ b ≠ 0 ∨ c ≠ 0) ∧
      ∀ x y, P x y = a * x ^ 2 + b * x * y + c * y ^ 2 + d * x + e * y + f) ∧
    Set.BijOn (fun p : ℝ × ℝ => P p.1 p.2) S (Set.range ((↑) : ℕ → ℝ))

Sources

• Brandt and Gjaldbæk, Classification of Quadratic Packing Polynomials on Sectors of R^2, INTEGERS 25 (2025), Article A81, Definition 1.

Used by 10

Used byQuadratic packing polynomials take natural-number values · The slope-\(12/7\) example on the sheared sector · Sheared criterion for quadratic packing polynomials · Constant term of a quadratic packing polynomial on a rational sector · First step value and sheared form of a quadratic packing polynomial · Step-difference form of a quadratic packing polynomial on a rational sector · Stanton's form of a quadratic packing polynomial on a rational sector · Form of a quadratic packing polynomial on a sector (Gjaldbæk) · Staircase congruence for quadratic packing polynomials · Height of the first step of the k-th staircase

TheoremQuadratic packing polynomials take natural-number values#✓fully proved

If \(P\) is a quadratic packing polynomial on a set \(S \subseteq \mathbb{R}^2\), then for every point \((x, y) \in S\) the value \(P(x, y)\) is a natural number.

public theorem IsQuadraticPackingPolynomial.exists_nat_eq {S : Set (ℝ × ℝ)}
    {P : ℝ → ℝ → ℝ} (hP : IsQuadraticPackingPolynomial S P) {p : ℝ × ℝ} (hp : p ∈ S) :
    ∃ N : ℕ, (N : ℝ) = P p.1 p.2

Sources

• Brandt and Gjaldbæk, Classification of Quadratic Packing Polynomials on Sectors of R^2, INTEGERS 25 (2025), Article A81, Definition 1.

Uses 1

Statement usesQuadratic packing polynomial

DefinitionStaircases of a rational sector#✓fully proved

For natural numbers \(m, n, i\), let \(l = \gcd(m - 1, n)\). The \(i\)-th staircase of the sector of slope \(n/m\) is \(J_i = \{(x, y) \in I(n/m) : nx - (m - 1)y = li\}\), where \(I(n/m)\) is the set of lattice points of that sector.

If \(m = 0\), the slope \(n/m\) is read as \(0\) and \(l\) as \(\gcd(0, n) = n\).

public def sectorStaircase (m n i : ℕ) : Set (ℝ × ℝ) :=
  {p | p ∈ sectorLatticePoints ((n : ℝ) / m) ∧
    (n : ℝ) * p.1 - ((m : ℝ) - 1) * p.2 = (Nat.gcd (m - 1) n : ℝ) * i}

Sources

• Brandt and Gjaldbæk, Classification of Quadratic Packing Polynomials on Sectors of R^2, INTEGERS 25 (2025), Article A81, Section 2 (definition of the staircases J_i).

Uses 1 · Used by 4

Statement usesLattice points of a sector

Used byStaircase congruence for quadratic packing polynomials · First height of a staircase · The zeroth staircase starts at height zero · The origin lies on the zeroth staircase

TheoremThe origin lies on the zeroth staircase#✓fully proved

For all natural numbers \(m, n\), the origin \((0, 0)\) lies on the staircase \(J_0\) of the sector of slope \(n/m\).

public theorem zero_mem_sectorStaircase_zero (m n : ℕ) :
    ((0 : ℝ), (0 : ℝ)) ∈ sectorStaircase m n 0

Sources

• Brandt and Gjaldbæk, Classification of Quadratic Packing Polynomials on Sectors of R^2, INTEGERS 25 (2025), Article A81, Section 2 (definition of the staircases J_i).

Uses 3 · Used by 1

Statement usesStaircases of a rational sector

Proof usesLattice points of a sector · The origin is a lattice point of every sector

Used byThe zeroth staircase starts at height zero

DefinitionFirst height of a staircase#✓fully proved

For natural numbers \(m, n, i\), the first height \(\bar y_i\) of the staircase \(J_i\) of the sector of slope \(n/m\) is the least \(y\)-coordinate of a point of \(J_i\), that is, the height of its first step; it is \(0\) if \(J_i\) is empty.

public noncomputable def staircaseFirstHeight (m n i : ℕ) : ℕ :=
  sInf {y : ℕ | ∃ x : ℝ, (x, (y : ℝ)) ∈ sectorStaircase m n i}

Sources

• Brandt and Gjaldbæk, Classification of Quadratic Packing Polynomials on Sectors of R^2, INTEGERS 25 (2025), Article A81, Section 3 (definition of ȳ_i).

Uses 1 · Used by 4

Statement usesStaircases of a rational sector

Used bySheared criterion for quadratic packing polynomials · First step value and sheared form of a quadratic packing polynomial · Height of the first step of the k-th staircase · The zeroth staircase starts at height zero

TheoremThe zeroth staircase starts at height zero#✓fully proved

For all natural numbers \(m, n\), the first height of the staircase \(J_0\) of the sector of slope \(n/m\) is \(\bar y_0 = 0\); indeed the origin lies on \(J_0\).

public theorem staircaseFirstHeight_zero (m n : ℕ) : staircaseFirstHeight m n 0 = 0

Sources

• Brandt and Gjaldbæk, Classification of Quadratic Packing Polynomials on Sectors of R^2, INTEGERS 25 (2025), Article A81, Section 3 (definition of ȳ_i).

Uses 3

Statement usesFirst height of a staircase

Proof usesStaircases of a rational sector · The origin lies on the zeroth staircase

DefinitionStep difference#✓fully proved

For natural numbers \(m, n\) and a real function \(P(x, y)\) of two real variables, let \(l = \gcd(m \mathbin{\dot-} 1, n)\), where \(m \mathbin{\dot-} 1\) is subtraction truncated at \(0\) (so \(l = n\) when \(m = 0\)). The step difference of \(P\) for the sector of slope \(n/m\) is \(k = P((m - 1)/l, n/l) - P(0, 0)\), with \(m - 1\) here the real difference and division by \(l = 0\) read as \(0\): the change \(P(x + (m - 1)/l, y + n/l) - P(x, y)\) of \(P\) between consecutive steps of a staircase of the sector, evaluated at the base point \((0, 0)\).

For every polynomial of Stanton's form (Theorem 2 of the source) this difference does not depend on the base point, which is how the source defines \(k\).

public noncomputable def consecutiveStepDifference (m n : ℕ) (P : ℝ → ℝ → ℝ) : ℝ :=
  P (((m : ℝ) - 1) / Nat.gcd (m - 1) n) ((n : ℝ) / Nat.gcd (m - 1) n) - P 0 0

Sources

• Brandt and Gjaldbæk, Classification of Quadratic Packing Polynomials on Sectors of R^2, INTEGERS 25 (2025), Article A81, Section 2 (definition of k).

Used by 6

Used byStep difference of the slope-\(12/7\) example · Constant term of a quadratic packing polynomial on a rational sector · First step value and sheared form of a quadratic packing polynomial · Step-difference form of a quadratic packing polynomial on a rational sector · Staircase congruence for quadratic packing polynomials · Height of the first step of the k-th staircase

TheoremStep difference of the slope-\(12/7\) example#✓fully proved

Let \(P(x, y) = 6(x - y/2)(x - y/2 - 3/2) + x + y + 2\). For \(m = 7\) and \(n = 12\) (the sector of slope \(12/7\)), the step difference of \(P\) is \(k = 3\): with \(l = \gcd(6, 12) = 6\), one has \(P(1, 2) - P(0, 0) = 3\).

public theorem consecutiveStepDifference_example_twelve_sevenths :
    consecutiveStepDifference 7 12
      (fun x y => 6 * (x - y / 2) * (x - y / 2 - 3 / 2) + x + y + 2) = 3

Sources

• Brandt and Gjaldbæk, Classification of Quadratic Packing Polynomials on Sectors of R^2, INTEGERS 25 (2025), Article A81, Example 10.

Uses 1

Statement usesStep difference

TheoremForm of a quadratic packing polynomial on a sector (Gjaldbæk)#●ready to prove

Let \(\alpha > 0\) be a real number and let \(P\) be a quadratic packing polynomial on the lattice sector \(I(\alpha)\). Then there are integers \(A, B, C, D, E, F\) with \(A > 0\), \(B^2 = AC\) and \(\alpha = A/(1 - B)\) such that for all real \(x, y\)

\[P(x, y) = \tfrac{A}{2} x(x - 1) + Bxy + \tfrac{C}{2} y(y - 1) + Dx + Ey + F.\]

In particular \(\alpha\) is rational.

public theorem_wanted quadraticPackingPolynomial_sector_form {α : ℝ} (hα : 0 < α)
    {P : ℝ → ℝ → ℝ} (hP : IsQuadraticPackingPolynomial (sectorLatticePoints α) P) :
    ∃ A B C D E F : ℤ,
      (∀ x y, P x y = (A : ℝ) / 2 * x * (x - 1) + B * x * y + (C : ℝ) / 2 * y * (y - 1) +
        D * x + E * y + F) ∧
      0 < A ∧ B ^ 2 = A * C ∧ α = (A : ℝ) / (1 - B)

Sources

• Brandt and Gjaldbæk, Classification of Quadratic Packing Polynomials on Sectors of R^2, INTEGERS 25 (2025), Article A81, Theorem 1.

Uses 2

Statement usesQuadratic packing polynomial · Lattice points of a sector

TheoremStanton's form of a quadratic packing polynomial on a rational sector#●ready to prove

Let \(m, n\) be coprime positive integers and let \(P\) be a quadratic packing polynomial on the lattice points \(I(n/m)\) of the sector of slope \(n/m\). Then \(n\) divides \((m - 1)^2\), and there are integers \(D, E, F\) such that for all real \(x, y\)

\[ P(x, y) = \frac{n}{2} \left(x - \frac{m - 1}{n} y\right)^2 + \left(D - \frac{n}{2}\right) x + \left(E - \frac{(m - 1)^2}{2n}\right) y + F. \]

public theorem_wanted quadraticPackingPolynomial_rational_sector_form {m n : ℕ} (hm : 0 < m)
    (hn : 0 < n) (hmn : Nat.Coprime m n) {P : ℝ → ℝ → ℝ}
    (hP : IsQuadraticPackingPolynomial (sectorLatticePoints ((n : ℝ) / m)) P) :
    (n : ℤ) ∣ ((m : ℤ) - 1) ^ 2 ∧
      ∃ D E F : ℤ, ∀ x y, P x y =
        (n : ℝ) / 2 * (x - ((m : ℝ) - 1) / n * y) ^ 2 + (D - (n : ℝ) / 2) * x +
          (E - (((m : ℝ) - 1) ^ 2 / n) / 2) * y + F

Sources

• Brandt and Gjaldbæk, Classification of Quadratic Packing Polynomials on Sectors of R^2, INTEGERS 25 (2025), Article A81, Theorem 2.

Uses 2

Statement usesQuadratic packing polynomial · Lattice points of a sector

TheoremThe slope-\(12/7\) example on the sheared sector#●ready to prove

Let \(M(x, y) = (x - y/2, y)\) and let \(\hat I(12/7) = M(I(12/7))\) be the image under \(M\) of the lattice points \(I(12/7)\) of the sector of slope \(12/7\). Then \(\hat P(x, y) = 6x(x - 3/2) + x + \frac{3}{2} y + 2\) is a quadratic packing polynomial on \(\hat I(12/7)\).

public theorem_wanted isQuadraticPackingPolynomial_sheared_example_twelve_sevenths :
    IsQuadraticPackingPolynomial
      ((fun p : ℝ × ℝ => (p.1 - 1 / 2 * p.2, p.2)) '' sectorLatticePoints ((12 : ℝ) / 7))
      (fun x y => 6 * x * (x - 3 / 2) + x + 3 / 2 * y + 2)

Sources

• Brandt and Gjaldbæk, Classification of Quadratic Packing Polynomials on Sectors of R^2, INTEGERS 25 (2025), Article A81, Example 10 and Figure 3.

Uses 2

Statement usesQuadratic packing polynomial · Lattice points of a sector

TheoremFirst step value and sheared form of a quadratic packing polynomial#●ready to prove

Let \(m, n\) be coprime positive integers, let \(l = \gcd(m - 1, n)\), and let \(P\) be a quadratic packing polynomial on the lattice points \(I(n/m)\) of the sector of slope \(n/m\) whose step difference for \(m, n\) is a positive integer \(k\). Put \(F = P(0, 0)\) and \(\hat P(x, y) = P(x + \frac{m - 1}{n} y, y)\), and let \(\bar y_k\) be the height of the first step of the \(k\)-th staircase of the sector. Then \(\hat P(k/(n/l), \bar y_k) = F + k\), and for all real \(x, y\) one has \(\hat P(x, y) = \frac{n}{2} x (x - 1) + D x + \frac{k}{n/l} y + F\) with \(D = n/l - (kl - n)/2 - \bar y_k\).

The step difference is taken as a natural number; by Theorem 1 of the source it is an integer for every quadratic packing polynomial.

public theorem_wanted quadraticPackingPolynomial_first_step_value {m n k : ℕ} (hm : 0 < m)
    (hn : 0 < n) (hmn : Nat.Coprime m n) {P : ℝ → ℝ → ℝ}
    (hP : IsQuadraticPackingPolynomial (sectorLatticePoints ((n : ℝ) / m)) P)
    (hk : 0 < k) (hkP : consecutiveStepDifference m n P = k) :
    let l : ℝ := Nat.gcd (m - 1) n
    let Phat : ℝ → ℝ → ℝ := fun x y => P (x + ((m : ℝ) - 1) / n * y) y
    Phat (k / (n / l)) (staircaseFirstHeight m n k) = P 0 0 + k ∧
      ∀ x y, Phat x y = (n : ℝ) / 2 * x * (x - 1) +
        (n / l - (k * l - n) / 2 - staircaseFirstHeight m n k) * x + k / (n / l) * y + P 0 0

Sources

• Brandt and Gjaldbæk, Classification of Quadratic Packing Polynomials on Sectors of R^2, INTEGERS 25 (2025), Article A81, Lemma 1.

Uses 4

Statement usesQuadratic packing polynomial · Step difference · Lattice points of a sector · First height of a staircase

TheoremStaircase congruence for quadratic packing polynomials#●ready to prove

Let \(m, n\) be positive coprime integers, let \(P\) be a quadratic packing polynomial on the lattice sector \(I(n/m)\), and suppose that the step difference of \(P\) equals a positive integer \(k\). Then for every natural number \(i\), every point \(p\) of the staircase \(J_i\) and every point \(q\) of the staircase \(J_{i+k}\), the difference \(P(q) - P(p)\) is an integer multiple of \(k\).

public theorem_wanted quadraticPackingPolynomial_staircase_congruence {m n k : ℕ} (hm : 0 < m)
    (hn : 0 < n) (hmn : Nat.Coprime m n) {P : ℝ → ℝ → ℝ}
    (hP : IsQuadraticPackingPolynomial (sectorLatticePoints ((n : ℝ) / m)) P)
    (hk : 0 < k) (hkP : consecutiveStepDifference m n P = k) (i : ℕ) {p q : ℝ × ℝ}
    (hp : p ∈ sectorStaircase m n i) (hq : q ∈ sectorStaircase m n (i + k)) :
    ∃ z : ℤ, P q.1 q.2 - P p.1 p.2 = z * k

Sources

• Brandt and Gjaldbæk, Classification of Quadratic Packing Polynomials on Sectors of R^2, INTEGERS 25 (2025), Article A81, Lemma 2.

Uses 4

Statement usesQuadratic packing polynomial · Step difference · Lattice points of a sector · Staircases of a rational sector

TheoremHeight of the first step of the k-th staircase#●ready to prove

Let \(m, n\) be positive coprime integers and \(l = \gcd(m - 1, n)\), let \(P\) be a quadratic packing polynomial on the lattice sector \(I(n/m)\), and suppose that the step difference of \(P\) equals a positive integer \(k\). Then the first height of the staircase \(J_k\) is \(\bar y_k = n/l - 1\).

public theorem_wanted quadraticPackingPolynomial_staircaseFirstHeight {m n k : ℕ} (hm : 0 < m)
    (hn : 0 < n) (hmn : Nat.Coprime m n) {P : ℝ → ℝ → ℝ}
    (hP : IsQuadraticPackingPolynomial (sectorLatticePoints ((n : ℝ) / m)) P)
    (hk : 0 < k) (hkP : consecutiveStepDifference m n P = k) :
    staircaseFirstHeight m n k = n / Nat.gcd (m - 1) n - 1

Sources

• Brandt and Gjaldbæk, Classification of Quadratic Packing Polynomials on Sectors of R^2, INTEGERS 25 (2025), Article A81, Lemma 3.

Uses 4

Statement usesQuadratic packing polynomial · Step difference · Lattice points of a sector · First height of a staircase

TheoremSheared criterion for quadratic packing polynomials#●ready to prove

Let \(m, n\) be coprime positive integers, let \(l = \gcd(m - 1, n)\), and assume that \(n/l\) divides \(l\). Let \(k\) be a positive integer with \(k \equiv (m - 1)/l \pmod{n/l}\), let \(F\) be a real number, and let \(\hat P(x, y) = \frac{n}{2} x \left(x - \frac{k}{n/l}\right) + x + \frac{k}{n/l} y + F\). Let \(M(x, y) = (x - \frac{m - 1}{n} y, y)\) and let \(\hat I(n/m) = M(I(n/m))\) be the image under \(M\) of the lattice points \(I(n/m)\) of the sector of slope \(n/m\). Then \(\hat P\) is a quadratic packing polynomial on \(\hat I(n/m)\) if and only if \(\{\hat P(i/(n/l), \bar y_i) : 0 \le i < k\} = \{0, 1, \dots, k - 1\}\), where \(\bar y_i\) is the height of the first step of the \(i\)-th staircase of the sector of slope \(n/m\).

The divisibility \(n/l \mid l\) is a standing assumption of the source, made explicit here.

public theorem_wanted isQuadraticPackingPolynomial_sheared_iff {m n k : ℕ} (hm : 0 < m)
    (hn : 0 < n) (hmn : Nat.Coprime m n) (hl : n / Nat.gcd (m - 1) n ∣ Nat.gcd (m - 1) n)
    (hk : 0 < k) (hkm : k ≡ (m - 1) / Nat.gcd (m - 1) n [MOD n / Nat.gcd (m - 1) n])
    (F : ℝ) :
    let l : ℝ := Nat.gcd (m - 1) n
    let Phat : ℝ → ℝ → ℝ := fun x y => (n : ℝ) / 2 * x * (x - k / (n / l)) + x + k / (n / l) * y + F
    IsQuadraticPackingPolynomial
        ((fun p : ℝ × ℝ => (p.1 - ((m : ℝ) - 1) / n * p.2, p.2)) ''
          sectorLatticePoints ((n : ℝ) / m)) Phat ↔
      (fun i : ℕ => Phat (i / (n / l)) (staircaseFirstHeight m n i)) '' Set.Iio k =
        ((↑) : ℕ → ℝ) '' Set.Iio k

Sources

• Brandt and Gjaldbæk, Classification of Quadratic Packing Polynomials on Sectors of R^2, INTEGERS 25 (2025), Article A81, Lemma 4.

Uses 3

Statement usesQuadratic packing polynomial · Lattice points of a sector · First height of a staircase

TheoremConstant term of a quadratic packing polynomial on a rational sector#●ready to prove

Let \(m, n\) be coprime positive integers, let \(l = \gcd(m - 1, n)\), and let \(P\) be a quadratic packing polynomial on the lattice points \(I(n/m)\) of the sector of slope \(n/m\). If the step difference of \(P\) for \(m, n\) is a positive integer \(k\), then \(P(0, 0) = \frac{l^2}{n} (k - 1)(k + 1)/12\).

public theorem_wanted quadraticPackingPolynomial_constant_term {m n k : ℕ} (hm : 0 < m)
    (hn : 0 < n) (hmn : Nat.Coprime m n) {P : ℝ → ℝ → ℝ}
    (hP : IsQuadraticPackingPolynomial (sectorLatticePoints ((n : ℝ) / m)) P)
    (hk : 0 < k) (hkP : consecutiveStepDifference m n P = k) :
    P 0 0 = ((Nat.gcd (m - 1) n : ℝ) ^ 2 / n) * (k - 1) * (k + 1) / 12

Sources

• Brandt and Gjaldbæk, Classification of Quadratic Packing Polynomials on Sectors of R^2, INTEGERS 25 (2025), Article A81, Lemma 5.

Uses 3

Statement usesQuadratic packing polynomial · Step difference · Lattice points of a sector

TheoremStep-difference form of a quadratic packing polynomial on a rational sector#●ready to prove

Let \(m, n\) be coprime positive integers, let \(l = \gcd(m - 1, n)\), and let \(P\) be a quadratic packing polynomial on the lattice points \(I(n/m)\) of the sector of slope \(n/m\) whose step difference for \(m, n\) is a positive integer \(k\). Then \(n/l\) divides \(l\), \(k \equiv (m - 1)/l \pmod{n/l}\), and for all real \(x, y\) one has \(P(x + \frac{m - 1}{n} y, y) = \frac{n}{2} x \left(x - \frac{k}{n/l}\right) + x + \frac{k}{n/l} y + P(0, 0)\).

public theorem_wanted quadraticPackingPolynomial_necessary_form {m n k : ℕ} (hm : 0 < m)
    (hn : 0 < n) (hmn : Nat.Coprime m n) {P : ℝ → ℝ → ℝ}
    (hP : IsQuadraticPackingPolynomial (sectorLatticePoints ((n : ℝ) / m)) P)
    (hk : 0 < k) (hkP : consecutiveStepDifference m n P = k) :
    n / Nat.gcd (m - 1) n ∣ Nat.gcd (m - 1) n ∧
      k ≡ (m - 1) / Nat.gcd (m - 1) n [MOD n / Nat.gcd (m - 1) n] ∧
      ∀ x y, P (x + ((m : ℝ) - 1) / n * y) y =
        (n : ℝ) / 2 * x * (x - k / (n / (Nat.gcd (m - 1) n : ℝ))) + x +
          k / (n / (Nat.gcd (m - 1) n : ℝ)) * y + P 0 0

Sources

• Brandt and Gjaldbæk, Classification of Quadratic Packing Polynomials on Sectors of R^2, INTEGERS 25 (2025), Article A81, Proposition 1.

Uses 3

Statement usesQuadratic packing polynomial · Step difference · Lattice points of a sector

10 fully proved9 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.