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

Proved

OAI.BinaryCoordinateSweeps.dense_induction_step_eventually

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.dense_induction_step_eventually of lean/OAI/Probability/BinarySweep/GridBounds/DenseClosing.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 Filter, open Young Irrep Representation GridSplit Signed):

theorem dense_induction_step_eventually (q : ℕ) (hq : 2≤q) : ∀ᶠ s : ℕ in atTop,
    ∀ m n h r : ℕ, ∀ bits : Fin (m+n) → ℕ, ∀ H : PathFamily bits h,
    gridSize bits=s →
    1≤Real.log (gridSize (leftBits bits)) → 1≤Real.log (gridSize (rightBits bits)) →
    Real.log (gridSize (leftBits bits))≤(4/5:ℝ)*Real.log s →
    Real.log (gridSize (rightBits bits))≤(4/5:ℝ)*Real.log s →
    (∀j, bits j≤2*r) → Real.log 4*(m+n)≤(1/1000:ℝ)*Real.log s →
    ∀ μ : YoungDiagram, ∀ e : Cell μ ≃ FreeSlot H 0,
    (s:ℝ)^(399/400:ℝ)≤diagramF μ → ∀z : ℝ,
    0≤z → z≤linePerturbationRadius r →
    EnumeratedMomentBound q (leftBits bits) z → EnumeratedMomentBound q (rightBits bits) z →
    evenMoment q (groupAverage ((hilbertSpecht μ).comp e.symm.permCongrHom.toMonoidHom)
      (fun a => (conditionalGroupLaw H z a:ℂ)))≤
      Real.exp (-cExponent s*diagramF μ+eExponent s*h*Real.log s-pathCost H)

Definitions. The statement is written with OAI.BinaryCoordinateSweeps.EnumeratedMomentBound, OAI.BinaryCoordinateSweeps.FreeSlot, OAI.BinaryCoordinateSweeps.GridSlot, OAI.BinaryCoordinateSweeps.PathFamily, OAI.BinaryCoordinateSweeps.cExponent, OAI.BinaryCoordinateSweeps.conditionalGroupLaw, OAI.BinaryCoordinateSweeps.diagramF, OAI.BinaryCoordinateSweeps.eExponent, OAI.BinaryCoordinateSweeps.freeSlotFintype, OAI.BinaryCoordinateSweeps.gridSize, OAI.BinaryCoordinateSweeps.linePerturbationRadius, OAI.BinaryCoordinateSweeps.pathCost, OAI.BinaryCoordinateSweeps.GridSplit.leftBits, OAI.BinaryCoordinateSweeps.GridSplit.rightBits, OAI.BinaryCoordinateSweeps.Irrep.evenMoment, OAI.BinaryCoordinateSweeps.Irrep.groupAverage, OAI.BinaryCoordinateSweeps.Young.Cell, OAI.BinaryCoordinateSweeps.Young.G, OAI.BinaryCoordinateSweeps.Young.SpechtHilbert, OAI.BinaryCoordinateSweeps.Young.Tabloid, OAI.BinaryCoordinateSweeps.Young.hilbertInner, OAI.BinaryCoordinateSweeps.Young.hilbertNormed, OAI.BinaryCoordinateSweeps.Young.hilbertSpecht and OAI.BinaryCoordinateSweeps.Young.instFintypeElemForallCellNatTabloid (definitions bundle OAIB3Bs000 of this split); OAI.BinaryCoordinateSweeps.Slot (the published bundle Def_BinarySweep).

Used by. The proof of OAI.BinaryCoordinateSweeps.real_grid_bound of this split imports it.

Preamble

import Mathlib
import Definitions.Def_BinarySweep
import Definitions.Def_OAIB3Bs000

Formal statement

section

attribute [-instance] _root_.OAI.BinaryCoordinateSweeps.Young.signTwist_irreducible _root_.OAI.BinaryCoordinateSweeps.finitePathFamily _root_.OAI.BinaryCoordinateSweeps.oneAxisOutsideEmpty
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
open Filter

namespace BinaryCoordinateSweeps
open Young Irrep Representation GridSplit Signed

theorem dense_induction_step_eventually (q : ℕ) (hq : 2≤q) : ∀ᶠ s : ℕ in atTop,
    ∀ m n h r : ℕ, ∀ bits : Fin (m+n) → ℕ, ∀ H : PathFamily bits h,
    gridSize bits=s →
    1≤Real.log (gridSize (leftBits bits)) → 1≤Real.log (gridSize (rightBits bits)) →
    Real.log (gridSize (leftBits bits))≤(4/5:ℝ)*Real.log s →
    Real.log (gridSize (rightBits bits))≤(4/5:ℝ)*Real.log s →
    (∀j, bits j≤2*r) → Real.log 4*(m+n)≤(1/1000:ℝ)*Real.log s →
    ∀ μ : YoungDiagram, ∀ e : Cell μ ≃ FreeSlot H 0,
    (s:ℝ)^(399/400:ℝ)≤diagramF μ → ∀z : ℝ,
    0≤z → z≤linePerturbationRadius r →
    EnumeratedMomentBound q (leftBits bits) z → EnumeratedMomentBound q (rightBits bits) z →
    evenMoment q (groupAverage ((hilbertSpecht μ).comp e.symm.permCongrHom.toMonoidHom)
      (fun a => (conditionalGroupLaw H z a:ℂ)))≤
      Real.exp (-cExponent s*diagramF μ+eExponent s*h*Real.log s-pathCost H) := 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/DenseClosing.lean (declaration OAI.BinaryCoordinateSweeps.dense_induction_step_eventually)

View graph