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

109 declarations, 1 contain sorry, 0 declared as axioms

  1. abbrev OAI.TriangularCovering.Space line 12

    Also declared: ComparatorChallenges/TriangularCovering.lean:11 (same declaration text), OAI/Geometry/TriangularCovering/Basic.lean:11 (same declaration text).

  2. def OAI.TriangularCovering.H line 14

    Also declared: ComparatorChallenges/TriangularCovering.lean:13 (same declaration text), OAI/Geometry/TriangularCovering/Basic.lean:13 (same declaration text).

  3. def OAI.TriangularCovering.point line 16

    Also declared: ComparatorChallenges/TriangularCovering.lean:15 (same declaration text), OAI/Geometry/TriangularCovering/Basic.lean:15 (same declaration text).

  4. def OAI.TriangularCovering.K line 18

    Also declared: ComparatorChallenges/TriangularCovering.lean:17 (same declaration text), OAI/Geometry/TriangularCovering/Basic.lean:18 (same declaration text).

  5. def OAI.TriangularCovering.projection line 21

    Also declared: ComparatorChallenges/TriangularCovering.lean:20 (same declaration text), OAI/Geometry/TriangularCovering/Basic.lean:22 (same declaration text).

  6. def OAI.TriangularCovering.area line 23

    Also declared: ComparatorChallenges/TriangularCovering.lean:22 (same declaration text), OAI/Geometry/TriangularCovering/Basic.lean:25 (same declaration text).

  7. def OAI.TriangularCovering.shadowArea line 25

    Also declared: ComparatorChallenges/TriangularCovering.lean:24 (same declaration text), OAI/Geometry/TriangularCovering/Basic.lean:27 (same declaration text).

  8. def OAI.TriangularCovering.A_min line 27

    Also declared: ComparatorChallenges/TriangularCovering.lean:26 (same declaration text), OAI/Geometry/TriangularCovering/Basic.lean:29 (same declaration text).

  9. structure OAI.TriangularCovering.TriCylinder line 29

    Also declared: ComparatorChallenges/TriangularCovering.lean:28 (same declaration text), OAI/Geometry/TriangularCovering/Basic.lean:32 (same declaration text).

  10. def OAI.TriangularCovering.TriCylinder.carrier line 41

    Also declared: ComparatorChallenges/TriangularCovering.lean:40 (same declaration text), OAI/Geometry/TriangularCovering/Basic.lean:45 (same declaration text).

  11. def OAI.TriangularCovering.Covers line 44

    Also declared: ComparatorChallenges/TriangularCovering.lean:43 (same declaration text), OAI/Geometry/TriangularCovering/Basic.lean:48 (same declaration text).

  12. def OAI.TriangularCovering.totalArea line 47

    Also declared: ComparatorChallenges/TriangularCovering.lean:46 (same declaration text), OAI/Geometry/TriangularCovering/Basic.lean:51 (same declaration text).

  13. def OAI.TriangularCovering.relativeCost line 50

    Also declared: ComparatorChallenges/TriangularCovering.lean:49 (same declaration text), OAI/Geometry/TriangularCovering/Basic.lean:54 (same declaration text).

  14. def OAI.TriangularCovering.n line 53

    Also declared: ComparatorChallenges/TriangularCovering.lean:52 (same declaration text), OAI/Geometry/TriangularCovering/Basic.lean:57 (same declaration text).

  15. def OAI.TriangularCovering.η line 67

    Also declared: OAI/Geometry/TriangularCovering/CoordinateCover.lean:11 (same declaration text).

  16. def OAI.TriangularCovering.alpha line 69

    Also declared: OAI/Geometry/TriangularCovering/CoordinateCover.lean:13 (same declaration text).

  17. def OAI.TriangularCovering.beta line 71

    Also declared: OAI/Geometry/TriangularCovering/CoordinateCover.lean:15 (same declaration text).

  18. def OAI.TriangularCovering.d line 73

    Also declared: OAI/Geometry/TriangularCovering/CoordinateCover.lean:17 (same declaration text).

  19. def OAI.TriangularCovering.cutoffCoeff line 75

    Also declared: OAI/Geometry/TriangularCovering/CoordinateCover.lean:40 (same declaration text).

  20. def OAI.TriangularCovering.step line 77

    Also declared: OAI/Geometry/TriangularCovering/CoordinateCover.lean:306 (same declaration text).

  21. def OAI.TriangularCovering.mesh line 79

    Also declared: OAI/Geometry/TriangularCovering/CoordinateCover.lean:308 (same declaration text).

  22. def OAI.TriangularCovering.cutoff line 81

    Also declared: OAI/Geometry/TriangularCovering/CoordinateCover.lean:374 (same declaration text).

  23. def OAI.TriangularCovering.speedSq line 83

    Also declared: OAI/Geometry/TriangularCovering/CoordinateCover.lean:491 (same declaration text).

  24. def OAI.TriangularCovering.normalizedTerm line 85

    Also declared: OAI/Geometry/TriangularCovering/CoordinateCover.lean:493 (same declaration text).

  25. def OAI.TriangularCovering.unit line 101

    Also declared: OAI/Geometry/TriangularCovering/Projection.lean:148 (same declaration text).

  26. def OAI.TriangularCovering.tiltV line 116

    Also declared: OAI/Geometry/TriangularCovering/CylinderFamily.lean:16 (same declaration text).

  27. def OAI.TriangularCovering.tiltW line 118

    Also declared: OAI/Geometry/TriangularCovering/CylinderFamily.lean:17 (same declaration text).

  28. def OAI.TriangularCovering.lowerVertices line 120

    Also declared: OAI/Geometry/TriangularCovering/CylinderFamily.lean:19 (same declaration text).

  29. def OAI.TriangularCovering.upperVertices line 123

    Also declared: OAI/Geometry/TriangularCovering/CylinderFamily.lean:21 (same declaration text).

  30. abbrev OAI.TriangularCovering.Planar.Coord line 139

    Also declared: OAI/Geometry/TriangularCovering/TriangleArea.lean:11 (same declaration text).

  31. def OAI.TriangularCovering.Planar.standard line 141

    Also declared: OAI/Geometry/TriangularCovering/TriangleArea.lean:13 (same declaration text).

  32. def OAI.TriangularCovering.Planar.vertices line 143

    Also declared: OAI/Geometry/TriangularCovering/TriangleArea.lean:15 (same declaration text).

  33. def OAI.TriangularCovering.triangle line 152

    Also declared: OAI/Geometry/TriangularCovering/TriangleArea.lean:91 (same declaration text).

  34. def OAI.TriangularCovering.lowerAngularIndex line 168

    Also declared: OAI/Geometry/CylinderCovering/Angular/ConstructionDefinitions.lean:11 (same declaration text).

  35. def OAI.TriangularCovering.upperAngularIndex line 171

    Also declared: OAI/Geometry/CylinderCovering/Angular/ConstructionDefinitions.lean:14 (same declaration text).

  36. def OAI.TriangularCovering.lowerAngularAxis line 174

    Also declared: OAI/Geometry/CylinderCovering/Angular/ConstructionDefinitions.lean:17 (same declaration text).

  37. def OAI.TriangularCovering.upperAngularAxis line 179

    Also declared: OAI/Geometry/CylinderCovering/Angular/ConstructionDefinitions.lean:22 (same declaration text).

  38. def OAI.TriangularCovering.lowerAngularBase line 184

    Also declared: OAI/Geometry/CylinderCovering/Angular/ConstructionDefinitions.lean:27 (same declaration text).

  39. def OAI.TriangularCovering.upperAngularBase line 190

    Also declared: OAI/Geometry/CylinderCovering/Angular/ConstructionDefinitions.lean:33 (same declaration text).

  40. def OAI.TriangularCovering.ExplicitAngularFamily line 196

    Also declared: OAI/Geometry/CylinderCovering/Angular/ConstructionDefinitions.lean:39 (same declaration text).

  41. def OAI.TriangularCovering.AngularAreaStatement line 203

    Also declared: OAI/Geometry/CylinderCovering/Angular/ConstructionDefinitions.lean:46 (same declaration text).

  42. def OAI.TriangularCovering.ExplicitAngularStatement line 211

    Also declared: OAI/Geometry/CylinderCovering/Angular/ConstructionDefinitions.lean:54 (same declaration text).

  43. abbrev OAI.RuledApproximation.Plane line 231

    Also declared: ComparatorChallenges/RuledCovering.lean:10 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:12 (same declaration text).

  44. abbrev OAI.RuledApproximation.Space line 232

    Also declared: ComparatorChallenges/RuledCovering.lean:11 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:13 (same declaration text).

  45. def OAI.RuledApproximation.vec2 line 233

    Also declared: ComparatorChallenges/RuledCovering.lean:13 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:15 (same declaration text).

  46. def OAI.RuledApproximation.vec3 line 234

    Also declared: ComparatorChallenges/RuledCovering.lean:14 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:16 (same declaration text).

  47. def OAI.RuledApproximation.axial line 235

    Also declared: ComparatorChallenges/RuledCovering.lean:15 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:17 (same declaration text).

  48. def OAI.RuledApproximation.IsParallelogram line 237

    Also declared: ComparatorChallenges/RuledCovering.lean:17 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:19 (same declaration text).

  49. structure OAI.RuledApproximation.Cylinder line 241

    Also declared: ComparatorChallenges/RuledCovering.lean:27 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:29 (same declaration text).

  50. def OAI.RuledApproximation.Cylinder.carrier line 248

    Also declared: ComparatorChallenges/RuledCovering.lean:34 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:36 (same declaration text).

  51. def OAI.RuledApproximation.Cylinder.area line 251

    Also declared: ComparatorChallenges/RuledCovering.lean:37 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:39 (same declaration text).

  52. def OAI.RuledApproximation.Cylinder.parallelogram line 253

    Also declared: ComparatorChallenges/RuledCovering.lean:39 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:41 (same declaration text).

  53. def OAI.RuledApproximation.Cylinder.openBounded line 255

    Also declared: ComparatorChallenges/RuledCovering.lean:43 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:45 (same declaration text).

  54. def OAI.RuledApproximation.familySet line 259

    Also declared: ComparatorChallenges/RuledCovering.lean:47 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:49 (same declaration text).

  55. def OAI.RuledApproximation.familyArea line 260

    Also declared: ComparatorChallenges/RuledCovering.lean:48 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:50 (same declaration text).

  56. def OAI.RuledApproximation.HasFiniteCover line 262

    Also declared: ComparatorChallenges/RuledCovering.lean:50 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:52 (same declaration text).

  57. def OAI.RuledApproximation.SmoothNear line 266

    Also declared: ComparatorChallenges/RuledCovering.lean:55 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:57 (same declaration text).

  58. def OAI.RuledApproximation.HyperbolicAt line 269

    Also declared: ComparatorChallenges/RuledCovering.lean:59 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:61 (same declaration text).

  59. def OAI.RuledApproximation.weight line 274

    Also declared: ComparatorChallenges/RuledCovering.lean:64 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:66 (same declaration text).

  60. def OAI.RuledApproximation.physicalWeight line 275

    Also declared: ComparatorChallenges/RuledCovering.lean:65 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:67 (same declaration text).

  61. def OAI.RuledApproximation.ruled line 278

    Also declared: ComparatorChallenges/RuledCovering.lean:68 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:70 (same declaration text).

  62. def OAI.RuledApproximation.physicalRuled line 282

    Also declared: ComparatorChallenges/RuledCovering.lean:72 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:74 (same declaration text).

  63. def OAI.RuledApproximation.HyperbolicStatement line 286

    Also declared: ComparatorChallenges/RuledCovering.lean:76 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:78 (same declaration text).

  64. def OAI.RuledApproximation.unitSquare line 293

    Also declared: ComparatorChallenges/RuledCovering.lean:124 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:126 (same declaration text).

  65. def OAI.RuledApproximation.IsSquareTile line 295

    Also declared: ComparatorChallenges/RuledCovering.lean:126 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:128 (same declaration text).

  66. def OAI.RuledApproximation.auxiliaryCylinder line 299

    Also declared: ComparatorChallenges/RuledCovering.lean:130 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:132 (same declaration text).

  67. def OAI.RuledApproximation.firstPhysicalMap line 302

    Also declared: ComparatorChallenges/RuledCovering.lean:133 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:135 (same declaration text).

  68. def OAI.RuledApproximation.secondPhysicalMap line 303

    Also declared: ComparatorChallenges/RuledCovering.lean:134 (same declaration text), OAI/Geometry/RuledCovering/Model.lean:136 (same declaration text).

  69. abbrev OAI.CylinderCovering.Space line 318

    Also declared: OAI/Geometry/CylinderCovering/Convexity/GlobalDefinitions.lean:12 (same declaration text).

  70. def OAI.CylinderCovering.IsRegularTetrahedron line 320

    Also declared: OAI/Geometry/CylinderCovering/Convexity/GlobalDefinitions.lean:14 (same declaration text).

  71. def OAI.CylinderCovering.shadowArea line 326

    Also declared: OAI/Geometry/CylinderCovering/Convexity/GlobalDefinitions.lean:20 (same declaration text).

  72. def OAI.CylinderCovering.minimumShadowArea line 329

    Also declared: OAI/Geometry/CylinderCovering/Convexity/GlobalDefinitions.lean:23 (same declaration text).

  73. def OAI.CylinderCovering.triangularCovers line 332

    Also declared: OAI/Geometry/CylinderCovering/Convexity/GlobalDefinitions.lean:26 (same declaration text).

  74. def OAI.CylinderCovering.triangularRelativeCost line 336

    Also declared: OAI/Geometry/CylinderCovering/Convexity/GlobalDefinitions.lean:30 (same declaration text).

  75. def OAI.CylinderCovering.relativeCost line 340

    Also declared: OAI/Geometry/CylinderCovering/Convexity/GlobalDefinitions.lean:34 (same declaration text).

  76. def OAI.CylinderCovering.AngularExplicitStatement line 344

    Also declared: OAI/Geometry/CylinderCovering/Convexity/GlobalDefinitions.lean:38 (same declaration text).

  77. def OAI.CylinderCovering.RegularTriangularCounterexampleStatement line 347

    Also declared: OAI/Geometry/CylinderCovering/Convexity/GlobalDefinitions.lean:41 (same declaration text).

  78. def OAI.CylinderCovering.RegularParallelogramCounterexampleStatement line 354

    Also declared: OAI/Geometry/CylinderCovering/Convexity/GlobalDefinitions.lean:48 (same declaration text).

  79. def OAI.CylinderCovering.RegularOpenCounterexampleStatement line 362

    Also declared: OAI/Geometry/CylinderCovering/Convexity/GlobalDefinitions.lean:56 (same declaration text).

  80. def OAI.RuledApproximation.NilpotentC1Statement line 382

    Also declared: OAI/Geometry/CylinderCovering/Ruled/C1Definitions.lean:10 (same declaration text).

  81. def OAI.CylinderCovering.RadialRiemann.step line 409

    Also declared: OAI/Geometry/CylinderCovering/Radial/RiemannDefinitions.lean:9 (same declaration text).

  82. def OAI.CylinderCovering.RadialRiemann.point line 411

    Also declared: OAI/Geometry/CylinderCovering/Radial/RiemannDefinitions.lean:11 (same declaration text).

  83. def OAI.CylinderCovering.RadialRiemann.cell line 413

    Also declared: OAI/Geometry/CylinderCovering/Radial/RiemannDefinitions.lean:13 (same declaration text).

  84. def OAI.CylinderCovering.RadialRiemann.IsTagged line 416

    Also declared: OAI/Geometry/CylinderCovering/Radial/RiemannDefinitions.lean:16 (same declaration text).

  85. def OAI.CylinderCovering.RadialRiemann.capMax line 419

    Also declared: OAI/Geometry/CylinderCovering/Radial/RiemannDefinitions.lean:19 (same declaration text).

  86. abbrev OAI.CylinderCovering.RadialSweep.Space line 435

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:13 (same declaration text).

  87. structure OAI.CylinderCovering.RadialSweep.Data line 437

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:15 (same declaration text).

  88. def OAI.CylinderCovering.RadialSweep.sweep line 463

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:41 (same declaration text).

  89. def OAI.CylinderCovering.RadialSweep.kappa line 468

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:46 (same declaration text).

  90. def OAI.CylinderCovering.RadialSweep.direction line 471

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:49 (same declaration text).

  91. def OAI.CylinderCovering.RadialSweep.weightedArea line 474

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:52 (same declaration text).

  92. def OAI.CylinderCovering.RadialSweep.scalarBound line 478

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:56 (same declaration text).

  93. def OAI.CylinderCovering.RadialSweep.radialError line 480

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:58 (same declaration text).

  94. def OAI.CylinderCovering.RadialSweep.collar line 482

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:60 (same declaration text).

  95. def OAI.CylinderCovering.RadialSweep.midpoint line 484

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:62 (same declaration text).

  96. def OAI.CylinderCovering.RadialSweep.leftTip line 487

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:65 (same declaration text).

  97. def OAI.CylinderCovering.RadialSweep.rightEdge line 489

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:67 (same declaration text).

  98. def OAI.CylinderCovering.RadialSweep.coordinateMap line 492

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:70 (same declaration text).

  99. def OAI.CylinderCovering.RadialSweep.frozenVertices line 494

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:72 (same declaration text).

  100. def OAI.CylinderCovering.RadialSweep.frozenTriangle line 503

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:81 (same declaration text).

  101. def OAI.CylinderCovering.RadialSweep.frozenBase line 506

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:84 (same declaration text).

  102. def OAI.CylinderCovering.RadialSweep.frozenArea line 509

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:87 (same declaration text).

  103. def OAI.CylinderCovering.RadialSweep.localSweep line 515

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:93 (same declaration text).

  104. def OAI.CylinderCovering.RadialSweep.actualBase line 520

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:98 (same declaration text).

  105. def OAI.CylinderCovering.RadialSweep.cylinder line 523

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:101 (same declaration text).

  106. def OAI.CylinderCovering.RadialSweep.actualCost line 526

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:104 (same declaration text).

  107. def OAI.CylinderCovering.RadialSweep.AlignedStatement line 529

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:107 (same declaration text).

  108. def OAI.CylinderCovering.RadialSweep.ActualSweepStatement line 540

    Also declared: OAI/Geometry/CylinderCovering/Radial/SweepDefinitions.lean:118 (same declaration text).

  109. theorem OAI.CylinderCovering.fourPaperMain Challenge statement: Cylinder-covering counterexamples and companion approximations sorry line 561

    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 3 distinct comparator results, so its combined Scope prose is not copied onto this declaration.
    2. The repository's comparator configuration selects OAI.Geometry.CylinderCovering.Main as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Geometry/CylinderCovering/Main.lean:44 (same statement text; different proof or body). Qualify references as OAI.CylinderCovering.fourPaperMain@path.

    theorem fourPaperMain :
    AngularExplicitStatement ∧
    RuledApproximation.HyperbolicStatement ∧
    RuledApproximation.NilpotentC1Statement ∧
    RegularParallelogramCounterexampleStatement ∧
    RegularOpenCounterexampleStatement ∧
    RadialSweep.AlignedStatement ∧
    RadialSweep.ActualSweepStatement := by
…

    Mentions: OAI.CylinderCovering.AngularExplicitStatement, OAI.RuledApproximation.HyperbolicStatement, OAI.RuledApproximation.NilpotentC1Statement, OAI.CylinderCovering.RegularParallelogramCounterexampleStatement, OAI.CylinderCovering.RegularOpenCounterexampleStatement, OAI.CylinderCovering.RadialSweep.AlignedStatement, OAI.CylinderCovering.RadialSweep.ActualSweepStatement