Arithmetic.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite-layer and weighted-variance inequalities

These inequalities supply the scalar calculations for completed surface cones in A Complete Local Domain without a Small Cohen–Macaulay Module (OpenAI, 2026).

theorem OAI.SmallCM.Arithmetic.layer_square_le line 21

Source documentation

The elementary finite-layer inequality in the proof of lem:lattice.

theorem layer_square_le (N : ℤ) (r : ℕ → ℤ) (n : ℕ)
    (hr : ∀ j < n, 0 ≤ r j) (hN : ∀ j < n, r j ≤ N) :
    (∑ j ∈ Finset.range n, r j) ^ 2 ≤
      N * ∑ j ∈ Finset.range n, (2 * (j : ℤ) + 1) * r j := by
…

theorem OAI.SmallCM.Arithmetic.layer_determinant_numerator_nonneg line 44

Source documentation

The scalar consequence of the rank bounds and first-degree bounds for quotient layers.

theorem layer_determinant_numerator_nonneg (N : ℤ) (hN : 0 ≤ N)
    (r c : ℕ → ℤ) (n : ℕ)
    (hr : ∀ j < n, 0 ≤ r j) (hrN : ∀ j < n, r j ≤ N)
    (hc : ∀ j < n, (j : ℤ) * r j ≤ c j) :
    0 ≤ N * (∑ j ∈ Finset.range n, (2 * c j + r j)) -
      (∑ j ∈ Finset.range n, r j) ^ 2 := by
…

theorem OAI.SmallCM.Arithmetic.weighted_square_expansion line 60

Source documentation

Expanding weighted square distances, without a normalization hypothesis.

theorem weighted_square_expansion {ι : Type*} (s : Finset ι)
    (w x : ι → ℝ) (a : ℝ) :
    (∑ i ∈ s, w i * (x i - a) ^ 2) =
      (∑ i ∈ s, w i * x i ^ 2) -
      2 * a * (∑ i ∈ s, w i * x i) + a ^ 2 * (∑ i ∈ s, w i) := by
…

theorem OAI.SmallCM.Arithmetic.weighted_variance_le_quarter line 75

Source documentation

The weighted variance bound for an interval of length one, used after the slope-balancing step.

theorem weighted_variance_le_quarter {ι : Type*} (s : Finset ι)
    (w x : ι → ℝ) (a : ℝ) (hw : ∀ i ∈ s, 0 ≤ w i)
    (hsum : ∑ i ∈ s, w i = 1)
    (hl : ∀ i ∈ s, a ≤ x i) (hu : ∀ i ∈ s, x i ≤ a + 1) :
    (∑ i ∈ s, w i * (x i - (∑ j ∈ s, w j * x j)) ^ 2) ≤ 1 / 4 := by
…

theorem OAI.SmallCM.Arithmetic.mixture_identity line 98

Source documentation

The finite weighted-mixture identity for normalized ranks and Chern characters.

theorem mixture_identity {ι : Type*} (s : Finset ι) (w m q : ι → ℝ)
    (hsum : ∑ i ∈ s, w i = 1) :
    2 * (∑ i ∈ s, w i * q i) - (∑ i ∈ s, w i * m i) ^ 2 =
      (∑ i ∈ s, w i * (2 * q i - m i ^ 2)) +
      (∑ i ∈ s, w i * (m i - (∑ j ∈ s, w j * m j)) ^ 2) := by
…

theorem OAI.SmallCM.Arithmetic.exponent_seven line 115

Source documentation

The numerical inequality for the exponent-seven polarization.

theorem exponent_seven :
    (5 : ℤ) * 7 ^ 3 = 1715 ∧
    (7 : ℤ) ^ 3 * (7 ^ 2 - 10) = 13377 ∧
    (6 : ℤ) * 1715 < 13377 := by
…