OAI.BinaryCoordinateSweeps.real_grid_bound: intermediate lemma from OpenAI, Row–column symmetry and contraction of coordinate sweeps

Proved

OAI.BinaryCoordinateSweeps.real_grid_bound

by dbenbenn · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

openai-math

An intermediate lemma of the split of OpenAI's proof of OAI.binary_sweep_contraction_and_mixing, carved from OpenAI's openai/math development for this platform. The statement and its proof are OpenAI's (OpenAI, Row–column symmetry and contraction of coordinate sweeps, OpenAI Math Release, September 26, 2026, result family 238, github.com/openai/math, Apache License 2.0); in Lean it is the declaration OAI.BinaryCoordinateSweeps.real_grid_bound of lean/OAI/Probability/BinarySweep/GridBounds/EmptyGrid.lean at commit adc7f12, ported to Lean 4.33.1 and Mathlib 0df444a.

The statement, as published (namespace OAI.BinaryCoordinateSweeps, with open scoped BigOperators Classical):

theorem real_grid_bound : ∃ r : ℕ, 0 < r ∧ ∃ q : ℕ, 0 < q ∧
    ∃ a : ℝ, 0 < a ∧ ∀b : ℕ, 1 ≤ b → ∀bits : Fin b → ℕ,
    (∀j, r ≤ bits j ∧ bits j ≤ 2*r) → ∀D : ℕ,
    ∀ρ : Representation ℂ (Equiv.Perm (GridSlot bits)) (RepSpace D),
    ρ.IsIrreducible → IsUnitaryRep ρ → ∀z : ℝ, 0 ≤ z → z ≤ a →
    ‖complexGridAverage bits ρ (z:ℂ)‖ ≤ (D:ℝ)^(-c0/(2*q))

Definitions. The statement is written with OAI.BinaryCoordinateSweeps.GridSlot, OAI.BinaryCoordinateSweeps.c0 and OAI.BinaryCoordinateSweeps.complexGridAverage (definitions bundle OAIB3Bs000 of this split); OAI.BinaryCoordinateSweeps.IsUnitaryRep and OAI.BinaryCoordinateSweeps.RepSpace (the published bundle Def_BinarySweep).

Used by. The proofs of OAI.BinaryCoordinateSweeps.constant_sweep_mixing and OAI.binary_sweep_contraction_and_mixing of this split import it.

Preamble

import Mathlib
import Definitions.Def_BinarySweep
import Definitions.Def_OAIB3Bs000

Formal statement

section

set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

noncomputable section
open scoped BigOperators Classical

namespace BinaryCoordinateSweeps

variable {b : ℕ} (bits : Fin b → ℕ)

theorem real_grid_bound : ∃ r : ℕ, 0 < r ∧ ∃ q : ℕ, 0 < q ∧
    ∃ a : ℝ, 0 < a ∧ ∀b : ℕ, 1 ≤ b → ∀bits : Fin b → ℕ,
    (∀j, r ≤ bits j ∧ bits j ≤ 2*r) → ∀D : ℕ,
    ∀ρ : Representation ℂ (Equiv.Perm (GridSlot bits)) (RepSpace D),
    ρ.IsIrreducible → IsUnitaryRep ρ → ∀z : ℝ, 0 ≤ z → z ≤ a →
    ‖complexGridAverage bits ρ (z:ℂ)‖ ≤ (D:ℝ)^(-c0/(2*q)) := by
  sorry

end BinaryCoordinateSweeps

end

end OAI
end

Source

OpenAI, Row–column symmetry and contraction of coordinate sweeps, OpenAI Math Release, September 26, 2026, https://github.com/openai/math (result family 238; paper: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Row-column-symmetry-and-contraction-of-coordinate-sweeps-September-26-2026/paper.pdf; Apache License 2.0); Lean: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Probability/BinarySweep/GridBounds/EmptyGrid.lean (declaration OAI.BinaryCoordinateSweeps.real_grid_bound)

View graph