Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

OAI.BalancedTransport.balanced_three_stack_realization

Open

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

The theorem states that there exist velocity fields U(M,w), force coefficients f₀(M,w) and f₁(M,w), material flows X(M,w), and a globally 1-periodic velocity field R(M) for each finite deterministic tape machine M, with the following properties for every finite input word w. On nonnegative time and ℝ³, U, f₀ and f₁ are smooth and vanish outside a common spatial compact set independent of time; every mixed space-time derivative of U is uniformly bounded. Moreover, f₀ = ∂ₜU + (U·∇)U and f₁ = −ΔU. All three families are uniformly effective from the encoded machine and input: algorithms approximate every mixed derivative component at rational space-time points within 2⁻ⁿ, provide global integer bounds on these derivatives, and provide integer support radii. The velocity is 1-periodic after time 1 and satisfies U(M,w)(t,x) = R(M)(t,x) for every t ≥ 1, so its later field depends only on M. The flow satisfies X(0,a) = a and ∂ₜX(t,a) = U(t,X(t,a)); its trajectory starting at (4,0,0) enters (−1,2)³ at some nonnegative time exactly when M halts on w, meaning that a configuration with no next transition is reached after finitely many machine steps. For every viscosity ν > 0, the force f = f₀ + νf₁ is smooth, has uniformly bounded mixed derivatives, and is 1-periodic after time 1; U with pressure zero solves the incompressible Navier–Stokes equation ∂ₜU + (U·∇)U = νΔU + f with U(0,·) = 0. This velocity is unique among smooth zero-data solutions in the comparison class, and every such solution has spatially constant pressure. The comparison class requires the velocity and all spatial derivatives through order two to be continuous in time as L² functions, the velocity to be continuously differentiable in time in L², velocity and first spatial derivatives to be bounded on each finite time slab, and pressure, after subtracting a time-dependent scalar, together with its first spatial derivatives to be continuous in time in L²; (U,0) belongs to this class. Finally, derivative approximations and global derivative bounds for f are computable when ν is computable, and computable relative to any rational name of ν whose nth approximation has error at most 2⁻ⁿ.

Preamble
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/BalancedThreeStack.lean; bytes 7344..8661
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib
import Definitions.Def_BalancedThreeStack

namespace OAI

namespace BalancedTransport

Formal statement
theorem balanced_three_stack_realization :
    ∃ U f₀ f₁ : Family Velocity,
    ∃ X : Family MaterialFlow,
    ∃ repeated : FiniteMachine → Velocity,
      EffectiveFamily U ∧ EffectiveFamily f₀ ∧ EffectiveFamily f₁ ∧
      (∀ M, Function.Periodic (repeated M) 1) ∧
      ∀ (M : FiniteMachine) (w : Input M),
        Smooth (U M w) ∧ Smooth (f₀ M w) ∧ Smooth (f₁ M w) ∧
        f₀ M w = inertialCoefficient (U M w) ∧
        f₁ M w = viscousCoefficient (U M w) ∧
        CommonCompactSupport (U M w) (f₀ M w) (f₁ M w) ∧
        BoundedMixed (U M w) ∧
        PeriodicAfterOne (U M w) ∧
        (∀ t, 1 ≤ t → ∀ x, U M w t x = repeated M t x) ∧
        ComparisonClass (U M w) (fun _ _ => 0) ∧
        IsMaterialFlow (U M w) (X M w) ∧
        ((∃ t : ℝ, 0 ≤ t ∧ X M w t fixedLabel ∈ observer) ↔ Halts M w) ∧
        ∀ ν : ℝ, 0 < ν →
          let f := affineForce (f₀ M w) (f₁ M w) ν
          ZeroDataSolution ν f (U M w) (fun _ _ => 0) ∧
          Smooth f ∧ BoundedMixed f ∧ PeriodicAfterOne f ∧
          UniqueInComparison ν f (U M w) ∧
          (ComputableReal ν → EffectiveFieldIn ∅ f) ∧
          (∀ name : ℕ → ℚ, RealName name ν → EffectiveFieldIn {nameOracle name} f) := by
  sorry

end BalancedTransport
end OAI
Source
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/BalancedThreeStack.lean
Human review
  • Endorsed by Community (Bot) · Oct 7, 2026

    Confirmed by the moderator at approval.

  • Endorsed by marwahaha · Oct 7, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me