OAI.Problem336.HasFUSFLaw.finiteResponseBound: intermediate lemma from OpenAI, The free uniform spanning forest is a factor of IID

Proved

OAI.Problem336.HasFUSFLaw.finiteResponseBound

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.Problem336.fusf_is_factor_iid, carved from OpenAI's openai/math development for this platform. The statement and its proof are OpenAI's (OpenAI, The free uniform spanning forest is a factor of IID, OpenAI Math Release, September 25, 2026, result family 231, github.com/openai/math, Apache License 2.0); in Lean it is the declaration OAI.Problem336.HasFUSFLaw.finiteResponseBound of lean/OAI/Probability/SpanningForest/SpanningForest/FUSFPosteriorResponse.lean at commit adc7f12, ported to Lean 4.33.1 and Mathlib 0df444a.

The statement, as published (namespace OAI.Problem336, with open MeasureTheory Filter, open scoped Topology):

theorem HasFUSFLaw.finiteResponseBound
    {G : GraphCode} (hc : GraphConnected G)
    {μ : ProbabilityMeasure EdgeConfiguration}
    (hμ : HasFUSFLaw G (μ : Measure EdgeConfiguration) id)
    (S : EdgeCode → ℕ → Finset EdgeCode) :
    PosteriorDrift.FiniteResponseBound μ S (1 / 2 : ℝ)

Definitions. The statement is written with OAI.Problem336.PosteriorDrift.FiniteResponseBound (definitions bundle OAIS336000 of this split); OAI.Problem336.EdgeCode, OAI.Problem336.EdgeConfiguration, OAI.Problem336.GraphCode, OAI.Problem336.GraphConnected and OAI.Problem336.HasFUSFLaw (the published bundle Def_FreeUniformSpanningForest).

Used by. The proof of OAI.Problem336.FinalFactor.worksOnGraph of this split imports it.

Preamble

import Mathlib
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Algebra.Order.BigOperators.Ring.Finset
import Mathlib.Combinatorics.SimpleGraph.Paths
import Mathlib.Data.List.Nodup
import Mathlib.GroupTheory.FreeGroup.Basic
import Mathlib.LinearAlgebra.TensorProduct.Basic
import Mathlib.MeasureTheory.MeasurableSpace.Constructions
import Mathlib.MeasureTheory.MeasurableSpace.Embedding
import Mathlib.MeasureTheory.Measure.Typeclasses.Probability
import Definitions.Def_FreeUniformSpanningForest
import Definitions.Def_OAIS336000

Formal statement

section

attribute [-instance] _root_.OAI.Problem336.AllPairWiener.law_isProbabilityMeasure _root_.OAI.Problem336.FreeKernel.complete_closedGraphCycleSpace _root_.OAI.Problem336.FreeKernel.projection_closedGraphCycleSpace _root_.OAI.Problem336.finiteCodeEdgesFintype _root_.OAI.Problem336.finiteDimensional_finiteCycleSpace _root_.OAI.Problem336.finiteDimensional_finiteHilbertCycleSpace
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 MeasureTheory Filter
open scoped Topology

namespace Problem336

theorem HasFUSFLaw.finiteResponseBound
    {G : GraphCode} (hc : GraphConnected G)
    {μ : ProbabilityMeasure EdgeConfiguration}
    (hμ : HasFUSFLaw G (μ : Measure EdgeConfiguration) id)
    (S : EdgeCode → ℕ → Finset EdgeCode) :
    PosteriorDrift.FiniteResponseBound μ S (1 / 2 : ℝ) := by
  sorry

end Problem336

end

end OAI
end

Source

OpenAI, The free uniform spanning forest is a factor of IID, OpenAI Math Release, September 25, 2026, https://github.com/openai/math (result family 231; paper: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-free-uniform-spanning-forest-is-a-factor-of-IID-September-25-2026/The-free-uniform-spanning-forest-is-a-factor-of-IID-September-25-2026.pdf; Apache License 2.0); Lean: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Probability/SpanningForest/SpanningForest/FUSFPosteriorResponse.lean (declaration OAI.Problem336.HasFUSFLaw.finiteResponseBound)

View graph