ComparatorChallenges/BalancedThreeStack.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: OpenAI's pinned repository says an unreleased internal model produced the manuscripts and supporting proof artifacts. The collection builds on the mathematics community's accumulated problems, results, language, and formal libraries; each manuscript's BibTeX and bibliography are the authority for individual scholarly credit.

Project sources: Pinned openai/math documentation, Pinned formalization catalogue

52 declarations, 1 contain sorry, 0 declared as axioms

  1. inductive OAI.BalancedTransport.Recorder.Direction line 7

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:8 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:8 (same declaration text).

  2. instance OAI.BalancedTransport.Recorder.(instance at line 11) line 11
  3. structure OAI.BalancedTransport.Recorder.Transition line 14

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:12 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:15 (same declaration text).

  4. structure OAI.BalancedTransport.FiniteMachine line 20

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:18 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:26 (same declaration text).

  5. abbrev OAI.BalancedTransport.Input line 28

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:26 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:34 (same declaration text).

  6. structure OAI.BalancedTransport.TapeConfiguration line 30

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:28 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:36 (same declaration text).

  7. def OAI.BalancedTransport.initialConfiguration line 35

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:33 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:41 (same declaration text).

  8. def OAI.BalancedTransport.machineStep line 38

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:36 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:44 (same declaration text).

  9. def OAI.BalancedTransport.Halts line 43

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:41 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:49 (same declaration text).

  10. def OAI.BalancedTransport.Recorder.Direction.number line 47

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:45 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:53 (same declaration text).

  11. def OAI.BalancedTransport.FiniteMachine.code line 52

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:50 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:58 (same declaration text).

  12. def OAI.BalancedTransport.inputCode line 58

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:56 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:64 (same declaration text).

  13. abbrev OAI.BalancedTransport.Space line 61

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:59 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:67 (same declaration text).

  14. abbrev OAI.BalancedTransport.Field line 62

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:60 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:69 (same declaration text).

  15. abbrev OAI.BalancedTransport.Velocity line 63

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:61 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:71 (same declaration text).

  16. abbrev OAI.BalancedTransport.Pressure line 64

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:62 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:73 (same declaration text).

  17. abbrev OAI.BalancedTransport.Family line 65

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:63 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:75 (same declaration text).

  18. abbrev OAI.BalancedTransport.MaterialFlow line 66

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:64 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:77 (same declaration text).

  19. abbrev OAI.BalancedTransport.MultiIndex line 67

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:65 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:79 (same declaration text).

  20. abbrev OAI.BalancedTransport.RationalPoint line 68

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:66 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:81 (same declaration text).

  21. def OAI.BalancedTransport.timeD line 77

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:75 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:92 (same declaration text).

  22. def OAI.BalancedTransport.spaceD line 80

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:78 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:95 (same declaration text).

  23. def OAI.BalancedTransport.mixedD line 83

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:81 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:98 (same declaration text).

  24. def OAI.BalancedTransport.spatialD line 88

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:86 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:103 (same declaration text).

  25. def OAI.BalancedTransport.Smooth line 92

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:90 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:107 (same declaration text).

  26. def OAI.BalancedTransport.BoundedMixed line 95

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:93 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:110 (same declaration text).

  27. def OAI.BalancedTransport.CH line 98

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:96 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:113 (same declaration text).

  28. def OAI.BalancedTransport.C1L2 line 104

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:102 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:119 (same declaration text).

  29. def OAI.BalancedTransport.div line 112

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:110 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:127 (same declaration text).

  30. def OAI.BalancedTransport.laplacian line 115

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:113 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:130 (same declaration text).

  31. def OAI.BalancedTransport.convection line 118

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:116 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:133 (same declaration text).

  32. def OAI.BalancedTransport.gradient line 121

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:119 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:136 (same declaration text).

  33. def OAI.BalancedTransport.affineForce line 124

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:122 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:139 (same declaration text).

  34. def OAI.BalancedTransport.inertialCoefficient line 127

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:125 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:142 (same declaration text).

  35. def OAI.BalancedTransport.viscousCoefficient line 130

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:128 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:145 (same declaration text).

  36. def OAI.BalancedTransport.ZeroDataSolution line 133

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:131 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:148 (same declaration text).

  37. def OAI.BalancedTransport.BoundedOnFiniteSlabs line 141

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:139 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:156 (same declaration text).

  38. def OAI.BalancedTransport.ComparisonClass line 146

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:144 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:161 (same declaration text).

  39. def OAI.BalancedTransport.UniqueInComparison line 150

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:148 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:165 (same declaration text).

  40. def OAI.BalancedTransport.CommonCompactSupport line 155

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:153 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:170 (same declaration text).

  41. def OAI.BalancedTransport.PeriodicAfterOne line 159

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:157 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:174 (same declaration text).

  42. def OAI.BalancedTransport.IsMaterialFlow line 162

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:160 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:177 (same declaration text).

  43. def OAI.BalancedTransport.fixedLabel line 166

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:164 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:181 (same declaration text).

  44. def OAI.BalancedTransport.observer line 168

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:166 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:183 (same declaration text).

  45. def OAI.BalancedTransport.rationalSpace line 171

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:169 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:186 (same declaration text).

  46. def OAI.BalancedTransport.error line 173

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:171 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:188 (same declaration text).

  47. def OAI.BalancedTransport.EffectiveFamily line 175

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:173 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:190 (same declaration text).

  48. def OAI.BalancedTransport.EffectiveFieldIn line 188

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:186 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:203 (same declaration text).

  49. def OAI.BalancedTransport.RealName line 197

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:195 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:212 (same declaration text).

  50. def OAI.BalancedTransport.ComputableReal line 200

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:198 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:215 (same declaration text).

  51. def OAI.BalancedTransport.nameOracle line 203

    Also declared: ComparatorChallenges/ForcedNavierStokesComputation.lean:201 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Model.lean:218 (same declaration text).

  52. theorem OAI.BalancedTransport.balanced_three_stack_realization Challenge statement: Finite computation in a balanced zero-data fluid flow sorry line 211

    L4DEL explanation

    This declaration is an exact comparator-selected statement. Read the Lean statement below for its mathematical content.

    1. The linked formalization note covers 6 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
    2. The repository's comparator configuration selects OAI.MathematicalPhysics.NavierStokes.BalancedTransport.MainResult as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: ComparatorChallenges/ForcedNavierStokesComputation.lean:206 (same declaration text), OAI/MathematicalPhysics/NavierStokes/BalancedTransport/MainResult.lean:12 (same statement text; different proof or body). Qualify references as OAI.BalancedTransport.balanced_three_stack_realization@path.

    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) ∧
…

    Mentions: OAI.BalancedTransport.Family, OAI.BalancedTransport.Velocity, OAI.BalancedTransport.MaterialFlow, OAI.BalancedTransport.FiniteMachine, OAI.BalancedTransport.EffectiveFamily, OAI.BalancedTransport.Input, OAI.BalancedTransport.Smooth, OAI.BalancedTransport.inertialCoefficient, OAI.BalancedTransport.viscousCoefficient, OAI.BalancedTransport.CommonCompactSupport, OAI.BalancedTransport.BoundedMixed