ComparatorChallenges/NavierStokesVelocity.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

202 declarations, 2 contain sorry, 0 declared as axioms

  1. abbrev OAI.VelocityDetection.Coord line 10

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Model.lean:10 (same declaration text).

  2. abbrev OAI.VelocityDetection.ScalarField line 12

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Model.lean:12 (same declaration text).

  3. abbrev OAI.VelocityDetection.VectorField line 14

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Model.lean:14 (same declaration text).

  4. theorem OAI.VelocityDetection.neZeroTwo line 16

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Model.lean:16 (same declaration text).

  5. theorem OAI.VelocityDetection.neZeroThree line 18

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Model.lean:18 (same declaration text).

  6. theorem OAI.VelocityDetection.neZeroFive line 20

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Model.lean:20 (same declaration text).

  7. def OAI.VelocityDetection.spatialD line 22

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Model.lean:22 (same declaration text).

  8. def OAI.VelocityDetection.timeD line 25

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Model.lean:25 (same declaration text).

  9. def OAI.VelocityDetection.laplacian line 28

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Model.lean:28 (same declaration text).

  10. def OAI.VelocityDetection.advection line 31

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Model.lean:31 (same declaration text).

  11. def OAI.VelocityDetection.divergence line 34

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Model.lean:34 (same declaration text).

  12. def OAI.VelocityDetection.NavierStokes line 37

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Model.lean:37 (same declaration text).

  13. def OAI.VelocityDetection.horizontal line 45

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Model.lean:45 (same declaration text).

  14. inductive OAI.VelocityDetection.Stacks.Move line 55

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Stacks.lean:10 (same declaration text).

  15. def OAI.VelocityDetection.Stacks.update line 61

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Stacks.lean:16 (same declaration text).

  16. structure OAI.VelocityDetection.Stacks.Rule line 67

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Stacks.lean:98 (same declaration text).

  17. structure OAI.VelocityDetection.Stacks.Configuration line 72

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Stacks.lean:103 (same declaration text).

  18. def OAI.VelocityDetection.Stacks.applyRule line 78

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Stacks.lean:109 (same declaration text).

  19. def OAI.VelocityDetection.Stacks.address line 82

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Stacks.lean:186 (same declaration text).

  20. def OAI.VelocityDetection.Stacks.capacity line 84

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Stacks.lean:238 (same declaration text).

  21. def OAI.VelocityDetection.Expanding.lambda line 94

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Expanding.lean:10 (same declaration text).

  22. def OAI.VelocityDetection.Expanding.initialRadius line 96

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Expanding.lean:12 (same declaration text).

  23. def OAI.VelocityDetection.Expanding.radius line 99

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Expanding.lean:15 (same declaration text).

  24. def OAI.VelocityDetection.Observation.join line 110

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Observation.lean:11 (same declaration text).

  25. def OAI.VelocityDetection.Observation.torusEvent line 112

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Observation.lean:17 (same declaration text).

  26. def OAI.VelocityDetection.Observation.upperHalfPlane line 117

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Observation.lean:22 (same declaration text).

  27. def OAI.VelocityDetection.Observation.planeMass line 119

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Observation.lean:24 (same declaration text).

  28. def OAI.VelocityDetection.Observation.planeEvent line 124

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Observation.lean:29 (same declaration text).

  29. abbrev OAI.VelocityDetection.SmoothProfiles.step line 137

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothProfiles.lean:12 (same declaration text).

  30. def OAI.VelocityDetection.TranslationGates.window line 150

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TranslationGates.lean:14 (same declaration text).

  31. def OAI.VelocityDetection.CenterPaths.ramp line 164

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/CenterPaths.lean:14 (same declaration text).

  32. def OAI.VelocityDetection.CenterPaths.theta line 166

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/CenterPaths.lean:30 (same declaration text).

  33. def OAI.VelocityDetection.CenterPaths.privateRow line 168

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/CenterPaths.lean:32 (same declaration text).

  34. def OAI.VelocityDetection.CenterPaths.center line 170

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/CenterPaths.lean:34 (same declaration text).

  35. def OAI.VelocityDetection.UniformDerivatives.Bounded line 188

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/UniformDerivatives.lean:15 (same declaration text).

  36. def OAI.VelocityDetection.Stacks.lookup line 203

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/StacksLookup.lean:14 (same declaration text).

  37. def OAI.VelocityDetection.TailSpace.compatible line 218

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TailSpace.lean:14 (same declaration text).

  38. abbrev OAI.VelocityDetection.Cylinder.Space line 248

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Cylinder.lean:14 (same declaration text).

  39. abbrev OAI.VelocityDetection.Cylinder.Vect line 250

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Cylinder.lean:16 (same declaration text).

  40. def OAI.VelocityDetection.Cylinder.measure line 252

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Cylinder.lean:18 (same declaration text).

  41. def OAI.VelocityDetection.Cylinder.periodic line 254

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Cylinder.lean:20 (same declaration text).

  42. def OAI.VelocityDetection.Cylinder.frame line 256

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Cylinder.lean:22 (same declaration text).

  43. def OAI.VelocityDetection.Cylinder.D line 258

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Cylinder.lean:24 (same declaration text).

  44. structure OAI.VelocityDetection.Cylinder.SliceH2 line 260

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Cylinder.lean:255 (same declaration text).

  45. structure OAI.VelocityDetection.Cylinder.PressureH1 line 267

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Cylinder.lean:262 (same declaration text).

  46. theorem OAI.VelocityDetection.Cylinder.twoAtLeastTwo line 273

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Cylinder.lean:372 (same declaration text).

  47. abbrev OAI.VelocityDetection.Cylinder.LpSpace line 275

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Cylinder.lean:374 (same declaration text).

  48. abbrev OAI.VelocityDetection.Cylinder.L2Space line 278

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Cylinder.lean:377 (same declaration text).

  49. def OAI.VelocityDetection.Cylinder.dt line 282

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/CylinderEnergy.lean:307 (same declaration text).

  50. theorem OAI.VelocityDetection.Cylinder.spaceOuterMeasureClass line 285

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/CylinderEnergy.lean:310 (same declaration text).

  51. def OAI.VelocityDetection.Cylinder.continuousL2On line 288

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/CylinderEnergy.lean:313 (same declaration text).

  52. def OAI.VelocityDetection.Cylinder.continuousH2On line 294

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/CylinderEnergy.lean:319 (same declaration text).

  53. def OAI.VelocityDetection.Cylinder.continuousH1On line 300

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/CylinderEnergy.lean:325 (same declaration text).

  54. def OAI.VelocityDetection.Cylinder.C1L2On line 304

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/CylinderEnergy.lean:329 (same declaration text).

  55. structure OAI.VelocityDetection.Cylinder.ComparisonClass line 315

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/CylinderEnergy.lean:340 (same declaration text).

  56. def OAI.VelocityDetection.Cylinder.join line 337

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/CylinderEnergy.lean:393 (same declaration text).

  57. def OAI.VelocityDetection.TailSpace.evalLinear line 353

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TailDifferentiability.lean:24 (same declaration text).

  58. def OAI.VelocityDetection.TailSpace.eval line 358

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TailDifferentiability.lean:29 (same declaration text).

  59. structure OAI.VelocityDetection.History.Configuration line 380

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/History.lean:17 (same declaration text).

  60. def OAI.VelocityDetection.History.radix line 402

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/History.lean:39 (same declaration text).

  61. def OAI.VelocityDetection.History.tag line 404

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/History.lean:41 (same declaration text).

  62. def OAI.VelocityDetection.History.applyRule line 408

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/History.lean:54 (same declaration text).

  63. def OAI.VelocityDetection.History.packedState line 413

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/History.lean:173 (same declaration text).

  64. def OAI.VelocityDetection.History.address line 415

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/History.lean:185 (same declaration text).

  65. abbrev OAI.VelocityDetection.History.Box line 418

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/History.lean:213 (same declaration text).

  66. def OAI.VelocityDetection.History.config line 420

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/History.lean:215 (same declaration text).

  67. def OAI.VelocityDetection.History.Active line 423

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/History.lean:228 (same declaration text).

  68. def OAI.VelocityDetection.History.rule line 425

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/History.lean:234 (same declaration text).

  69. def OAI.VelocityDetection.History.target line 428

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/History.lean:241 (same declaration text).

  70. def OAI.VelocityDetection.History.sourceAddress line 431

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/History.lean:244 (same declaration text).

  71. def OAI.VelocityDetection.History.targetAddress line 433

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/History.lean:246 (same declaration text).

  72. def OAI.VelocityDetection.TapeCodes.word line 451

    Distinct definitions of this name: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TapeCodes.lean:19 (same statement text; different proof or body). Qualify references as OAI.VelocityDetection.TapeCodes.word@path.

  73. def OAI.VelocityDetection.TapeCodes.half sorry line 453

    Distinct definitions of this name: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TapeCodes.lean:32 (same statement text; different proof or body). Qualify references as OAI.VelocityDetection.TapeCodes.half@path.

  74. def OAI.VelocityDetection.TapeCodes.tape line 456

    Distinct definitions of this name: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TapeCodes.lean:55 (same statement text; different proof or body). Qualify references as OAI.VelocityDetection.TapeCodes.tape@path.

  75. def OAI.VelocityDetection.TapeCodes.rule line 459

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TapeCodes.lean:63 (same declaration text).

  76. def OAI.VelocityDetection.TapeCodes.table line 464

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TapeCodes.lean:68 (same declaration text).

  77. def OAI.VelocityDetection.Prelude.rule line 484

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Prelude.lean:19 (same declaration text).

  78. def OAI.VelocityDetection.Prelude.table' line 487

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Prelude.lean:22 (same declaration text).

  79. def OAI.VelocityDetection.Prelude.initial line 491

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/Prelude.lean:29 (same declaration text).

  80. def OAI.VelocityDetection.MachineHistory.table line 509

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/MachineHistory.lean:20 (same declaration text).

  81. def OAI.VelocityDetection.MachineHistory.initial line 513

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/MachineHistory.lean:24 (same declaration text).

  82. abbrev OAI.VelocityDetection.Effective.Poly line 524

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothExpressions.lean:12 (same declaration text).

  83. def OAI.VelocityDetection.Effective.poly line 526

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothExpressions.lean:14 (same declaration text).

  84. def OAI.VelocityDetection.Effective.nextPoly line 530

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothExpressions.lean:18 (same declaration text).

  85. def OAI.VelocityDetection.Effective.flat line 534

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothExpressions.lean:22 (same declaration text).

  86. def OAI.VelocityDetection.Effective.polyBound line 537

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothExpressions.lean:46 (same declaration text).

  87. inductive OAI.VelocityDetection.Effective.Expr line 541

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothExpressions.lean:100 (same declaration text).

  88. def OAI.VelocityDetection.Effective.Expr.eval line 560

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothExpressions.lean:119 (same declaration text).

  89. def OAI.VelocityDetection.Effective.Expr.diff line 569

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothExpressions.lean:137 (same declaration text).

  90. def OAI.VelocityDetection.Effective.Expr.jet line 578

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothExpressions.lean:202 (same declaration text).

  91. structure OAI.VelocityDetection.Effective.Ball line 590

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothExpressions.lean:220 (same declaration text).

  92. def OAI.VelocityDetection.Effective.polyEval line 595

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothExpressions.lean:228 (same declaration text).

  93. def OAI.VelocityDetection.Effective.expSum line 599

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothExpressions.lean:240 (same declaration text).

  94. def OAI.VelocityDetection.Effective.expError line 601

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothExpressions.lean:242 (same declaration text).

  95. def OAI.VelocityDetection.Effective.flatRound line 603

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothExpressions.lean:263 (same declaration text).

  96. def OAI.VelocityDetection.Effective.Ball.atom line 618

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothExpressions.lean:375 (same declaration text).

  97. def OAI.VelocityDetection.Effective.Ball.add line 620

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothExpressions.lean:377 (same declaration text).

  98. def OAI.VelocityDetection.Effective.Ball.neg line 622

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothExpressions.lean:379 (same declaration text).

  99. def OAI.VelocityDetection.Effective.Ball.mul line 624

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothExpressions.lean:381 (same declaration text).

  100. def OAI.VelocityDetection.Effective.Ball.inv line 627

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothExpressions.lean:384 (same declaration text).

  101. def OAI.VelocityDetection.Effective.Ball.invSafe line 630

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothExpressions.lean:387 (same declaration text).

  102. def OAI.VelocityDetection.Effective.Ball.flat line 632

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothExpressions.lean:389 (same declaration text).

  103. def OAI.VelocityDetection.Effective.Expr.round line 645

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/RationalEvaluation.lean:67 (same declaration text).

  104. def OAI.VelocityDetection.Effective.Expr.safe line 654

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/RationalEvaluation.lean:76 (same declaration text).

  105. def OAI.VelocityDetection.Effective.coordinateD line 671

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/RationalEvaluation.lean:131 (same declaration text).

  106. def OAI.VelocityDetection.Effective.mixedD line 674

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/RationalEvaluation.lean:134 (same declaration text).

  107. def OAI.VelocityDetection.Effective.accuracy line 678

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/RationalEvaluation.lean:183 (same declaration text).

  108. def OAI.VelocityDetection.Effective.Names line 680

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/RationalEvaluation.lean:185 (same declaration text).

  109. def OAI.VelocityDetection.Effective.inputBall line 683

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/RationalEvaluation.lean:188 (same declaration text).

  110. def OAI.VelocityDetection.Effective.trial line 686

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/RationalEvaluation.lean:208 (same declaration text).

  111. abbrev OAI.VelocityDetection.PeriodicSpace.Torus line 700

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/PeriodicSpace.lean:11 (same declaration text).

  112. def OAI.VelocityDetection.PeriodicSpace.cover line 702

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/PeriodicSpace.lean:15 (same declaration text).

  113. def OAI.VelocityDetection.SmoothBump.profile line 713

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/SmoothBump.lean:12 (same declaration text).

  114. abbrev OAI.VelocityDetection.TorusClass.Space line 723

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TorusClass.lean:10 (same declaration text).

  115. def OAI.VelocityDetection.TorusClass.measure line 725

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TorusClass.lean:14 (same declaration text).

  116. def OAI.VelocityDetection.TorusClass.periodic line 727

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TorusClass.lean:21 (same declaration text).

  117. def OAI.VelocityDetection.TorusClass.frame line 729

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TorusClass.lean:23 (same declaration text).

  118. def OAI.VelocityDetection.TorusClass.D line 731

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TorusClass.lean:25 (same declaration text).

  119. def OAI.VelocityDetection.TorusClass.dt line 733

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TorusClassContinuousOnEnergy.lean:285 (same declaration text).

  120. structure OAI.VelocityDetection.TorusClass.ComparisonClass line 736

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TorusClassContinuousOnEnergy.lean:288 (same declaration text).

  121. def OAI.VelocityDetection.MachineTorus.initialAddress line 767

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/MachineTorus.lean:15 (same declaration text).

  122. instance OAI.VelocityDetection.Effective.Expr.(instance at line 779) line 779
  123. instance OAI.VelocityDetection.Effective.Expr.(instance at line 781) line 781
  124. instance OAI.VelocityDetection.Effective.Expr.(instance at line 783) line 783
  125. instance OAI.VelocityDetection.Effective.Expr.(instance at line 785) line 785
  126. instance OAI.VelocityDetection.Effective.Expr.(instance at line 787) line 787
  127. instance OAI.VelocityDetection.Effective.Expr.(instance at line 789) line 789
  128. instance OAI.VelocityDetection.Effective.Expr.(instance at line 791) line 791
  129. def OAI.VelocityDetection.Effective.Expr.subst line 793

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:97 (same declaration text).

  130. def OAI.VelocityDetection.Effective.Expr.sumList line 802

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:123 (same declaration text).

  131. def OAI.VelocityDetection.Effective.Expr.sumFin line 806

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:139 (same declaration text).

  132. def OAI.VelocityDetection.Effective.Expr.unaryD line 808

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:152 (same declaration text).

  133. def OAI.VelocityDetection.Effective.Recipe.glue line 820

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:189 (same declaration text).

  134. def OAI.VelocityDetection.Effective.Recipe.step line 822

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:196 (same declaration text).

  135. def OAI.VelocityDetection.Effective.Recipe.pulse line 824

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:207 (same declaration text).

  136. def OAI.VelocityDetection.Effective.Recipe.window line 826

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:217 (same declaration text).

  137. def OAI.VelocityDetection.Effective.Recipe.windowD line 828

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:219 (same declaration text).

  138. def OAI.VelocityDetection.Effective.Recipe.theta line 830

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:236 (same declaration text).

  139. def OAI.VelocityDetection.Effective.Recipe.center line 833

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:249 (same declaration text).

  140. def OAI.VelocityDetection.Effective.Recipe.gate line 838

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:266 (same declaration text).

  141. def OAI.VelocityDetection.Effective.Recipe.impulse line 847

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:289 (same declaration text).

  142. def OAI.VelocityDetection.Effective.Recipe.packet line 851

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:304 (same declaration text).

  143. def OAI.VelocityDetection.Effective.Expr.activeSum line 864

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:325 (same declaration text).

  144. abbrev OAI.VelocityDetection.Effective.ArrayRecipe.Code line 882

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:373 (same declaration text).

  145. def OAI.VelocityDetection.Effective.ArrayRecipe.K line 884

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:375 (same declaration text).

  146. def OAI.VelocityDetection.Effective.ArrayRecipe.D line 886

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:377 (same declaration text).

  147. def OAI.VelocityDetection.Effective.ArrayRecipe.radius line 888

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:379 (same declaration text).

  148. def OAI.VelocityDetection.Effective.ArrayRecipe.spacing line 891

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:382 (same declaration text).

  149. def OAI.VelocityDetection.Effective.ArrayRecipe.duration line 893

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:384 (same declaration text).

  150. def OAI.VelocityDetection.Effective.ArrayRecipe.start line 896

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:387 (same declaration text).

  151. def OAI.VelocityDetection.Effective.ArrayRecipe.sign line 900

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:421 (same declaration text).

  152. abbrev OAI.VelocityDetection.Effective.ArrayRecipe.Instruction line 903

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:429 (same declaration text).

  153. def OAI.VelocityDetection.Effective.ArrayRecipe.path line 905

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:431 (same declaration text).

  154. def OAI.VelocityDetection.Effective.ArrayRecipe.gate line 910

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:458 (same declaration text).

  155. def OAI.VelocityDetection.Effective.ArrayRecipe.stage line 914

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:485 (same declaration text).

  156. def OAI.VelocityDetection.Effective.ArrayRecipe.field line 917

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:498 (same declaration text).

  157. def OAI.VelocityDetection.Effective.ChartRecipe.scale line 930

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ExpressionAlgebra.lean:523 (same declaration text).

  158. def OAI.VelocityDetection.Effective.ChartRecipe.radius line 932

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ChartExpressions.lean:19 (same declaration text).

  159. def OAI.VelocityDetection.Effective.ChartRecipe.targetHeight line 934

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ChartExpressions.lean:25 (same declaration text).

  160. def OAI.VelocityDetection.Effective.ChartRecipe.path line 937

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ChartExpressions.lean:45 (same declaration text).

  161. def OAI.VelocityDetection.Effective.ChartRecipe.gate line 944

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ChartExpressions.lean:74 (same declaration text).

  162. def OAI.VelocityDetection.Effective.ChartRecipe.stage line 949

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ChartExpressions.lean:98 (same declaration text).

  163. def OAI.VelocityDetection.Effective.ChartRecipe.prefixCode line 952

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ChartExpressions.lean:111 (same declaration text).

  164. def OAI.VelocityDetection.Effective.ChartRecipe.duration line 954

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ChartExpressions.lean:123 (same declaration text).

  165. def OAI.VelocityDetection.Effective.ChartRecipe.localTime line 959

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ChartExpressions.lean:143 (same declaration text).

  166. def OAI.VelocityDetection.Effective.ChartRecipe.weight line 963

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ChartExpressions.lean:147 (same declaration text).

  167. def OAI.VelocityDetection.Effective.ChartRecipe.clock line 966

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ChartExpressions.lean:150 (same declaration text).

  168. def OAI.VelocityDetection.Effective.ChartRecipe.rawField line 969

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ChartExpressions.lean:198 (same declaration text).

  169. def OAI.VelocityDetection.Effective.ChartRecipe.initial line 974

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ChartExpressions.lean:219 (same declaration text).

  170. def OAI.VelocityDetection.Effective.ChartRecipe.rawSource line 977

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ChartExpressions.lean:226 (same declaration text).

  171. def OAI.VelocityDetection.Effective.periodize line 992

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ChartExpressions.lean:299 (same declaration text).

  172. def OAI.VelocityDetection.Effective.ChartRecipe.fieldBlock line 1008

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ChartExpressions.lean:340 (same declaration text).

  173. def OAI.VelocityDetection.Effective.ChartRecipe.sourceBlock line 1010

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ChartExpressions.lean:342 (same declaration text).

  174. def OAI.VelocityDetection.Effective.ChartRecipe.field line 1012

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ChartExpressions.lean:393 (same declaration text).

  175. def OAI.VelocityDetection.Effective.ChartRecipe.source line 1014

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ChartExpressions.lean:395 (same declaration text).

  176. def OAI.VelocityDetection.Effective.residualCode line 1025

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ForceExpressions.lean:12 (same declaration text).

  177. def OAI.VelocityDetection.Effective.ArrayRecipe.initialCode line 1040

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ForceExpressions.lean:63 (same declaration text).

  178. def OAI.VelocityDetection.Effective.ArrayRecipe.source line 1043

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ForceExpressions.lean:66 (same declaration text).

  179. def OAI.VelocityDetection.Effective.forceFunction line 1056

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ForceExpressions.lean:99 (same declaration text).

  180. inductive OAI.VelocityDetection.Effective.MachineRecipe.Domain line 1070

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ForceExpressions.lean:113 (same declaration text).

  181. def OAI.VelocityDetection.Effective.MachineRecipe.field line 1073

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ForceExpressions.lean:116 (same declaration text).

  182. def OAI.VelocityDetection.Effective.MachineRecipe.source line 1078

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ForceExpressions.lean:121 (same declaration text).

  183. def OAI.VelocityDetection.Effective.MachineRecipe.force line 1082

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ForceExpressions.lean:125 (same declaration text).

  184. def OAI.VelocityDetection.Effective.MachineRecipe.timeCutoff line 1097

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ForceExpressions.lean:243 (same declaration text).

  185. def OAI.VelocityDetection.Effective.MachineRecipe.spaceCutoff line 1101

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ForceExpressions.lean:247 (same declaration text).

  186. def OAI.VelocityDetection.Effective.MachineRecipe.runTrial line 1105

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ForceExpressions.lean:270 (same declaration text).

  187. structure OAI.VelocityDetection.Effective.RationalBox line 1118

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ForceExpressions.lean:420 (same declaration text).

  188. def OAI.VelocityDetection.Effective.RationalBox.carrier line 1132

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ForceExpressions.lean:434 (same declaration text).

  189. def OAI.VelocityDetection.Effective.RationalBox.cell line 1134

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/ForceExpressions.lean:438 (same declaration text).

  190. def OAI.VelocityDetection.Effective.RationalBox.boundTrial line 1138

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/EffectivePrescriptions.lean:31 (same declaration text).

  191. def OAI.VelocityDetection.Effective.MachineRecipe.boxTimeCutoff line 1152

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/EffectivePrescriptions.lean:74 (same declaration text).

  192. def OAI.VelocityDetection.Effective.MachineRecipe.boxSpaceCutoff line 1156

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/EffectivePrescriptions.lean:78 (same declaration text).

  193. def OAI.VelocityDetection.Effective.MachineRecipe.runBoundTrial line 1160

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/EffectivePrescriptions.lean:105 (same declaration text).

  194. structure OAI.VelocityDetection.Effective.MachineRecipe.Program line 1171

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/EffectivePrescriptions.lean:132 (same declaration text).

  195. def OAI.VelocityDetection.Effective.MachineRecipe.compile line 1176

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/EffectivePrescriptions.lean:137 (same declaration text).

  196. def OAI.VelocityDetection.Effective.MachineRecipe.Program.valueTrial line 1187

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/EffectivePrescriptions.lean:148 (same declaration text).

  197. def OAI.VelocityDetection.Effective.MachineRecipe.Program.boundTrial line 1191

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/EffectivePrescriptions.lean:152 (same declaration text).

  198. def OAI.VelocityDetection.Effective.MachineRecipe.Program.evaluate line 1195

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/EffectivePrescriptions.lean:156 (same declaration text).

  199. def OAI.VelocityDetection.Effective.MachineRecipe.Program.derivativeBounds line 1198

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/EffectivePrescriptions.lean:159 (same declaration text).

  200. def OAI.VelocityDetection.Effective.MachineRecipe.Program.Represents line 1201

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/EffectivePrescriptions.lean:162 (same declaration text).

  201. def OAI.VelocityDetection.Effective.ComputableReal line 1220

    Also declared: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/EffectivePrescriptions.lean:202 (same declaration text).

  202. theorem OAI.VelocityDetection.main_result Challenge statement: Pointwise and integral velocity-field detection of halting sorry line 1232

    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.VelocityDetection.Main as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/MathematicalPhysics/NavierStokes/VelocityDetection/MainResult.lean:11 (same statement text; different proof or body). Qualify references as OAI.VelocityDetection.main_result@path.

    theorem main_result :
    ∃ B : ℕ, 0 < B ∧
      (∀ s : ℝ, |deriv (deriv SmoothBump.profile) s| ≤ (B:ℝ)) ∧
    ∀ (ν : ℝ), 0 < ν → ComputableReal ν →
    ∀ (b N : ℕ) [NeZero b] [NeZero N]
      (M : TM0.Machine (Fin b) (Fin N)) (w : List (Fin b)),
    ∃ (Ftor Fcyl : ℝ → VectorField 3),
      (compile B M w).Represents .torus Ftor ∧
      (compile B M w).Represents .cylinder Fcyl ∧
      (ContDiff ℝ ∞ (uncurry (Ftor ν)) ∧
        (∀ t, FactorsThrough (Ftor ν t) PeriodicSpace.cover) ∧
        (∃ K : Set (Coord 2), IsCompact K ∧ (∀ X ∈ K, ∀ i, X i ∈ Ioo (0:ℝ) 1) ∧
…

    Mentions: OAI.VelocityDetection.SmoothBump.profile, OAI.VelocityDetection.VectorField, OAI.VelocityDetection.PeriodicSpace.cover, OAI.VelocityDetection.Coord