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

Proved

OAI.BinaryCoordinateSweeps.constant_sweep_mixing

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.constant_sweep_mixing of lean/OAI/Probability/BinarySweep/Mixing/BinaryMixingBounds.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, open Young):

theorem constant_sweep_mixing : ConstantSweepMixingTarget

Definitions. The statement is written with OAI.BinaryCoordinateSweeps.ConstantSweepMixingTarget (definitions bundle OAIB3Bs000 of this split).

Used by. The proof of OAI.binary_sweep_contraction_and_mixing of this split imports it.

Preamble

import Mathlib
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
open Young

theorem constant_sweep_mixing : ConstantSweepMixingTarget := 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/Mixing/BinaryMixingBounds.lean (declaration OAI.BinaryCoordinateSweeps.constant_sweep_mixing)

View graph