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

237 declarations, 2 contain sorry, 0 declared as axioms

Area-controlled end replacement and Schwarzschild equality examples.

  1. abbrev OAI.CKSMetricGluing.InnerField line 110

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:110 (same declaration text).

  2. abbrev OAI.CKSMetricGluing.SmoothMetric line 115

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:115 (same declaration text).

  3. def OAI.CKSMetricGluing.innerSection line 117

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:117 (same declaration text).

  4. abbrev OAI.CKSAngularGeometry.I line 131

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:131 (same declaration text).

  5. def OAI.CKSCalculus.D line 143

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:143 (same declaration text).

  6. abbrev OAI.CKSRound.Idx line 153

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:153 (same declaration text).

  7. abbrev OAI.CKSRound.Mat line 155

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:155 (same declaration text).

  8. structure OAI.CKSRound.MetricJet line 157

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:157 (same declaration text).

  9. def OAI.CKSRound.MetricJet.gamma line 170

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:170 (same declaration text).

  10. def OAI.CKSRound.MetricJet.dInv line 173

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:173 (same declaration text).

  11. def OAI.CKSRound.MetricJet.dGamma line 176

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:176 (same declaration text).

  12. def OAI.CKSRound.MetricJet.ricci line 180

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:180 (same declaration text).

  13. def OAI.CKSRound.MetricJet.scalar line 184

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:184 (same declaration text).

  14. structure OAI.CKSRound.TensorJet line 194

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:194 (same declaration text).

  15. def OAI.CKSRound.MetricJet.trace line 206

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:206 (same declaration text).

  16. def OAI.CKSRound.MetricJet.normSq line 209

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:209 (same declaration text).

  17. def OAI.CKSRound.MetricJet.dTrace line 212

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:212 (same declaration text).

  18. def OAI.CKSRound.MetricJet.tensorDivergence line 215

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:215 (same declaration text).

  19. def OAI.CKSRound.MetricJet.energy line 219

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:219 (same declaration text).

  20. def OAI.CKSRound.MetricJet.momentum line 222

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:222 (same declaration text).

  21. abbrev OAI.CKSRealizedRound.Point line 234

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:234 (same declaration text).

  22. def OAI.CKSRealizedRound.basis line 236

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:236 (same declaration text).

  23. def OAI.CKSLocalBending.momentumSq line 246

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:246 (same declaration text).

  24. def OAI.CKSLocalBending.DEC line 249

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:249 (same declaration text).

  25. abbrev OAI.CKSAngularGeometry.Point line 261

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:261 (same declaration text).

  26. def OAI.CKSAngularGeometry.basis line 263

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:263 (same declaration text).

  27. abbrev OAI.CKSAngularGeometry.AmbientMat line 274

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:274 (same declaration text).

  28. abbrev OAI.CKSAngularGeometry.PhysicalPoint line 285

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:285 (same declaration text).

  29. abbrev OAI.CKSMixedGeometry.I line 296

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:296 (same declaration text).

  30. abbrev OAI.CKSMixedGeometry.A line 298

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:298 (same declaration text).

  31. abbrev OAI.CKSMixedGeometry.Point line 300

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:300 (same declaration text).

  32. def OAI.CKSMixedGeometry.basis line 302

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:302 (same declaration text).

  33. def OAI.CKSMixedGeometry.radialFactor line 315

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:315 (same declaration text).

  34. def OAI.CKSMixedGeometry.scaledD line 319

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:319 (same declaration text).

  35. def OAI.CKSMixedGeometry.scaledIter line 322

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:322 (same declaration text).

  36. abbrev OAI.CKSMixedGeometry.Angle line 335

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:335 (same declaration text).

  37. def OAI.CKSMixedGeometry.angularProjection line 337

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:337 (same declaration text).

  38. def OAI.CKSMixedGeometry.ScaledComponentBound line 340

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:340 (same declaration text).

  39. abbrev OAI.CKSInducedSphere.Ix line 352

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:352 (same declaration text).

  40. abbrev OAI.CKSSphericalHarmonics.Ambient line 362

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:362 (same declaration text).

  41. abbrev OAI.CKSSphericalHarmonics.Sphere line 364

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:364 (same declaration text).

  42. abbrev OAI.CKSSphericalHarmonics.surfaceMeasure line 375

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:375 (same declaration text).

  43. def OAI.CKSSphericalHarmonics.SmoothSphere line 389

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:389 (same declaration text).

  44. abbrev OAI.CKSInducedSphere.E line 410

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:410 (same declaration text).

  45. def OAI.CKSInducedSphere.e line 423

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:423 (same declaration text).

  46. def OAI.CKSInducedSphere.pd line 425

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:425 (same declaration text).

  47. abbrev OAI.CKSLorentz.E line 436

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:436 (same declaration text).

  48. abbrev OAI.CKSLorentz.V line 438

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:438 (same declaration text).

  49. abbrev OAI.CKSLorentz.Sphere line 440

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:440 (same declaration text).

  50. def OAI.CKSLorentz.ordinaryLeadingComponent line 453

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:453 (same declaration text).

  51. structure OAI.CKSMixedGeometry.SourceRemainderOn line 466

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:466 (same declaration text).

  52. structure OAI.CKSLorentz.SourceCKSComponents line 479

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:479 (same declaration text).

  53. def OAI.CKSLorentz.angularRadialTail line 494

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:494 (same declaration text).

  54. structure OAI.CKSLorentz.SmoothAngularPatch line 507

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:507 (same declaration text).

  55. def OAI.CKSLorentz.SmoothAngularPatch.param line 526

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:526 (same declaration text).

  56. def OAI.CKSLorentz.SmoothAngularPatch.sphereRegion line 528

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:528 (same declaration text).

  57. structure OAI.CKSLorentz.CKSTensorPatch line 540

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:540 (same declaration text).

  58. abbrev OAI.CKSLorentz.SpatialBilinear line 585

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:585 (same declaration text).

  59. abbrev OAI.CKSLorentz.SpatialTensor line 590

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:590 (same declaration text).

  60. def OAI.CKSLorentz.polarParam line 594

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:594 (same declaration text).

  61. def OAI.CKSLorentz.polarTensorComponents line 598

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:598 (same declaration text).

  62. def OAI.CKSLorentz.CKSTensorPatch.Realizes line 603

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:603 (same declaration text).

  63. abbrev OAI.CKSLorentz.AngularMatrix line 616

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:616 (same declaration text).

  64. def OAI.CKSLorentz.angularMetricTrace line 618

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:618 (same declaration text).

  65. def OAI.CKSLorentz.angularRoundMetric line 620

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:620 (same declaration text).

  66. def OAI.CKSLorentz.nullDirection line 639

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:639 (same declaration text).

  67. def OAI.CKSLorentz.rawCharge line 641

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:641 (same declaration text).

  68. def OAI.CKSLorentz.bondiCharge line 643

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:643 (same declaration text).

  69. def OAI.CKSLorentz.hyperbolicField line 670

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:670 (same declaration text).

  70. def OAI.CKSLorentz.sourceSpatial line 683

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:683 (same declaration text).

  71. def OAI.CKSADM.normal line 730

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:730 (same declaration text).

  72. def OAI.CKSADM.spatialInfinity line 741

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:741 (same declaration text).

  73. def OAI.CKSADM.TailRegular line 743

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:743 (same declaration text).

  74. def OAI.CKSADM.Decay line 746

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:746 (same declaration text).

  75. def OAI.CKSADM.SymbolN line 749

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:749 (same declaration text).

  76. def OAI.CKSADM.Symbol line 753

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:753 (same declaration text).

  77. def OAI.CKSAngularGeometry.physicalMetricJet line 765

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:765 (same declaration text).

  78. def OAI.CKSAngularGeometry.physicalTensorJet line 770

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:770 (same declaration text).

  79. abbrev OAI.CKSCartesianOuter.toPoint line 784

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:784 (same declaration text).

  80. def OAI.CKSLorentz.cksChartMassAspect line 794

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:794 (same declaration text).

  81. def OAI.CKSLorentz.spatialCoefficients line 808

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:808 (same declaration text).

  82. def OAI.CKSLorentz.spatialDEC line 813

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:813 (same declaration text).

  83. def OAI.CKSLorentz.CKSTensorPatch.RepresentsMassAspect line 825

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:825 (same declaration text).

  84. def OAI.CKSLorentz.spatialCartesian line 837

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:837 (same declaration text).

  85. def OAI.CKSLorentz.spatialADMEnergy line 852

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:852 (same declaration text).

  86. def OAI.CKSLorentz.spatialADMMomentum line 859

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:859 (same declaration text).

  87. def OAI.CKSLorentz.spatialEnergy line 874

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:874 (same declaration text).

  88. abbrev OAI.CKSReplacementCompleteness.Metric line 890

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:890 (same declaration text).

  89. def OAI.CKSReplacementCompleteness.metricSpace line 896

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:896 (same declaration text).

  90. def OAI.CKSReplacementCompleteness.IsComplete line 901

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:901 (same declaration text).

  91. abbrev OAI.CKSGeometricCuts.E3 line 913

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:913 (same declaration text).

  92. abbrev OAI.CKSGeometricCuts.H3 line 917

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:917 (same declaration text).

  93. abbrev OAI.CKSGeometricCuts.I3 line 919

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:919 (same declaration text).

  94. structure OAI.CKSGeometricCuts.OuterDomain line 931

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:931 (same declaration text).

  95. def OAI.CKSSpatialManifold.endInner line 976

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:976 (same declaration text).

  96. def OAI.CKSSpatialManifold.PhysicalDECAt line 998

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:998 (same declaration text).

  97. def OAI.CKSSpatialManifold.PhysicalDEC line 1009

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1009 (same declaration text).

  98. abbrev OAI.CKSIntrinsicGeometry.H3 line 1023

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1023 (same declaration text).

  99. abbrev OAI.CKSIntrinsicGeometry.I3 line 1025

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1025 (same declaration text).

  100. abbrev OAI.CKSBoundarySurface.E2 line 1036

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1036 (same declaration text).

  101. abbrev OAI.CKSBoundarySurface.E3 line 1038

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1038 (same declaration text).

  102. abbrev OAI.CKSBoundarySurface.H3 line 1042

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1042 (same declaration text).

  103. abbrev OAI.CKSBoundarySurface.I2 line 1044

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1044 (same declaration text).

  104. abbrev OAI.CKSBoundarySurface.I3 line 1046

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1046 (same declaration text).

  105. def OAI.CKSBoundarySurface.insertNormalZero line 1061

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1061 (same declaration text).

  106. def OAI.CKSBoundarySurface.liftPlane line 1063

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1063 (same declaration text).

  107. def OAI.CKSBoundarySurface.tangentialCoordinates line 1086

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1086 (same declaration text).

  108. def OAI.CKSBoundarySurface.dropPlane line 1088

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1088 (same declaration text).

  109. def OAI.CKSBoundarySurface.liftHalf line 1117

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1117 (same declaration text).

  110. abbrev OAI.CKSSchwarzschild.Radial line 1132

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1132 (same declaration text).

  111. abbrev OAI.CKSSchwarzschild.Sphere line 1134

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1134 (same declaration text).

  112. abbrev OAI.CKSSchwarzschild.Exterior line 1136

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1136 (same declaration text).

  113. def OAI.CKSSchwarzschild.join line 1152

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1152 (same declaration text).

  114. def OAI.CKSSchwarzschild.halfProduct line 1162

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1162 (same declaration text).

  115. def OAI.CKSSchwarzschild.productChart line 1178

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1178 (same declaration text).

  116. instance OAI.CKSSchwarzschild.exteriorChartedSpace line 1181

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1181 (same declaration text).

  117. instance OAI.CKSSchwarzschild.exteriorIsManifold line 1206

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1206 (same declaration text).

  118. def OAI.CKSSchwarzschild.height line 1267

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1267 (same declaration text).

  119. def OAI.CKSSchwarzschild.radius line 1280

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1280 (same declaration text).

  120. def OAI.CKSSchwarzschild.directionAmbient line 1284

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1284 (same declaration text).

  121. def OAI.CKSSchwarzschild.position line 1286

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1286 (same declaration text).

  122. def OAI.CKSSchwarzschild.velocity line 1297

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1297 (same declaration text).

  123. def OAI.CKSSchwarzschild.lapseSquared line 1301

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1301 (same declaration text).

  124. def OAI.CKSSchwarzschild.lapse line 1305

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1305 (same declaration text).

  125. def OAI.CKSSchwarzschild.euclideanForm line 1317

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1317 (same declaration text).

  126. def OAI.CKSSchwarzschild.radialUnit line 1319

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1319 (same declaration text).

  127. def OAI.CKSSchwarzschild.radialForm line 1323

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1323 (same declaration text).

  128. def OAI.CKSSchwarzschild.cartMetric line 1337

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1337 (same declaration text).

  129. def OAI.CKSSchwarzschild.cartTensor line 1346

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1346 (same declaration text).

  130. def OAI.CKSSchwarzschild.metricInner line 1356

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1356 (same declaration text).

  131. def OAI.CKSSchwarzschild.tensorInner line 1358

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1358 (same declaration text).

  132. abbrev OAI.CKSIntrinsicConstraints.E line 1369

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1369 (same declaration text).

  133. abbrev OAI.CKSIntrinsicConstraints.H line 1373

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1373 (same declaration text).

  134. abbrev OAI.CKSIntrinsicConstraints.I line 1375

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1375 (same declaration text).

  135. def OAI.CKSIntrinsicConstraints.coordinateMomentumNorm line 1389

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1389 (same declaration text).

  136. structure OAI.CKSIntrinsicConstraints.ConstraintChart line 1406

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1406 (same declaration text).

  137. def OAI.CKSIntrinsicConstraints.ConstraintChart.energy line 1428

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1428 (same declaration text).

  138. def OAI.CKSIntrinsicConstraints.ConstraintChart.momentumNorm line 1431

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1431 (same declaration text).

  139. abbrev OAI.CKSIntrinsicVolume.E line 1445

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1445 (same declaration text).

  140. abbrev OAI.CKSIntrinsicVolume.H line 1447

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1447 (same declaration text).

  141. abbrev OAI.CKSIntrinsicVolume.I line 1449

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1449 (same declaration text).

  142. abbrev OAI.CKSIntrinsicVolume.basis line 1451

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1451 (same declaration text).

  143. abbrev OAI.CKSIntrinsicVolume.Metric line 1480

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1480 (same declaration text).

  144. def OAI.CKSIntrinsicVolume.chartFrame line 1482

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1482 (same declaration text).

  145. def OAI.CKSIntrinsicVolume.chartMatrix line 1485

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1485 (same declaration text).

  146. def OAI.CKSIntrinsicVolume.chartDensity line 1494

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1494 (same declaration text).

  147. def OAI.CKSIntrinsicVolume.localVolume line 1509

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1509 (same declaration text).

  148. def OAI.CKSIntrinsicVolume.IsVolume line 1514

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1514 (same declaration text).

  149. def OAI.CKSIntrinsicVolume.riemannianVolume line 1530

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1530 (same declaration text).

  150. abbrev OAI.CKSBoundarySurface.Boundary line 1545

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1545 (same declaration text).

  151. def OAI.CKSBoundarySurface.boundaryInverse line 1562

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1562 (same declaration text).

  152. def OAI.CKSBoundarySurface.boundaryChart line 1612

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1612 (same declaration text).

  153. instance OAI.CKSBoundarySurface.boundaryChartedSpace line 1713

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1713 (same declaration text).

  154. instance OAI.CKSBoundarySurface.boundaryIsManifold line 1729

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1729 (same declaration text).

  155. abbrev OAI.CKSSurfaceVolume.E line 1833

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1833 (same declaration text).

  156. abbrev OAI.CKSSurfaceVolume.H line 1835

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1835 (same declaration text).

  157. abbrev OAI.CKSSurfaceVolume.I line 1837

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1837 (same declaration text).

  158. abbrev OAI.CKSSurfaceVolume.basis line 1839

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1839 (same declaration text).

  159. abbrev OAI.CKSSurfaceVolume.Metric line 1851

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1851 (same declaration text).

  160. def OAI.CKSSurfaceVolume.chartFrame line 1883

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1883 (same declaration text).

  161. def OAI.CKSSurfaceVolume.chartMatrix line 1886

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1886 (same declaration text).

  162. def OAI.CKSSurfaceVolume.chartDensity line 1896

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1896 (same declaration text).

  163. def OAI.CKSSurfaceVolume.localVolume line 1910

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1910 (same declaration text).

  164. def OAI.CKSSurfaceVolume.IsVolume line 1915

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1915 (same declaration text).

  165. def OAI.CKSSurfaceVolume.riemannianVolume line 1927

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1927 (same declaration text).

  166. abbrev OAI.CKSInducedArea.E2 line 1941

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1941 (same declaration text).

  167. abbrev OAI.CKSInducedArea.I2 line 1943

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1943 (same declaration text).

  168. abbrev OAI.CKSInducedArea.E3 line 1945

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1945 (same declaration text).

  169. abbrev OAI.CKSInducedArea.Inner2 line 1988

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:1988 (same declaration text).

  170. abbrev OAI.CKSInducedArea.Smooth3 line 2006

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:2006 (same declaration text).

  171. abbrev OAI.CKSInducedArea.Bil2 line 2022

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:2022 (same declaration text).

  172. abbrev OAI.CKSInducedArea.Bil3 line 2026

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:2026 (same declaration text).

  173. def OAI.CKSInducedArea.inducedInner line 2044

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:2044 (same declaration text).

  174. def OAI.CKSInducedArea.bilinearTriv line 2324

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:2324 (same declaration text).

  175. instance OAI.CKSInducedArea.bilinearTriv_atlas line 2332

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:2332 (same declaration text).

  176. def OAI.CKSInducedArea.inducedMetric line 2541

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:2541 (same declaration text).

  177. abbrev OAI.CKSEmbeddingDerivative.E line 2701

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:2701 (same declaration text).

  178. abbrev OAI.CKSEmbeddingDerivative.H line 2705

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:2705 (same declaration text).

  179. abbrev OAI.CKSEmbeddingDerivative.I line 2707

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:2707 (same declaration text).

  180. instance OAI.CKSFullCutArea.domainTopology line 2721

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:2721 (same declaration text).

  181. instance OAI.CKSFullCutArea.domainCharts line 2723

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:2723 (same declaration text).

  182. instance OAI.CKSFullCutArea.domainSmooth line 2725

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:2725 (same declaration text).

  183. abbrev OAI.CKSFullCutArea.Surface line 2727

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:2727 (same declaration text).

  184. def OAI.CKSFullCutArea.cutInclusion line 2729

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:2729 (same declaration text).

  185. instance OAI.CKSFullCutArea.domainSecondCountable line 2745

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:2745 (same declaration text).

  186. abbrev OAI.CKSFullCutArea.SmoothMetric line 2748

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:2748 (same declaration text).

  187. def OAI.CKSFullCutArea.cutMetric line 2753

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:2753 (same declaration text).

  188. def OAI.CKSFullCutArea.area line 2915

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:2915 (same declaration text).

  189. def OAI.CKSFullCutArea.minEnclosingArea line 2920

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:2920 (same declaration text).

  190. def OAI.CKSIntrinsicConstraints.IntegrableConstraints line 2949

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:2949 (same declaration text).

  191. def OAI.CKSSourceExterior.Orientable line 3000

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3000 (same declaration text).

  192. structure OAI.CKSSourceExterior.CoordinateEnd line 3010

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3010 (same declaration text).

  193. structure OAI.CKSSourceExterior.CKSData line 3025

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3025 (same declaration text).

  194. instance OAI.CKSSchwarzschild.exteriorConnected line 3051

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3051 (same declaration text).

  195. def OAI.CKSSourceExterior.cutArea line 3070

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3070 (same declaration text).

  196. def OAI.CKSSourceExterior.minimumEnclosingArea line 3075

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3075 (same declaration text).

  197. def OAI.CKSSourceExterior.constraintsIntegrable line 3080

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3080 (same declaration text).

  198. def OAI.CKSSchwarzschild.covariantPair line 3096

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3096 (same declaration text).

  199. abbrev OAI.CKSSchwarzschild.Spacetime line 3118

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3118 (same declaration text).

  200. abbrev OAI.CKSSchwarzschild.SpacetimeBilinear line 3120

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3120 (same declaration text).

  201. def OAI.CKSSchwarzschild.timeForm line 3126

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3126 (same declaration text).

  202. def OAI.CKSSchwarzschild.spacePart line 3128

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3128 (same declaration text).

  203. def OAI.CKSSchwarzschild.radiusForm line 3130

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3130 (same declaration text).

  204. def OAI.CKSSchwarzschild.schwarzschildH line 3132

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3132 (same declaration text).

  205. def OAI.CKSSchwarzschild.advancedMetric line 3150

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3150 (same declaration text).

  206. def OAI.CKSSchwarzschild.advancedSlope line 3169

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3169 (same declaration text).

  207. def OAI.CKSSchwarzschild.advancedTime line 3171

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3171 (same declaration text).

  208. def OAI.CKSSchwarzschild.advancedGraph line 3175

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3175 (same declaration text).

  209. def OAI.CKSSchwarzschild.futureNormal line 3177

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3177 (same declaration text).

  210. def OAI.CKSSchwarzschild.graphTangent line 3180

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3180 (same declaration text).

  211. structure OAI.CKSSchwarzschild.HorizonRegularGraph line 3198

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3198 (same declaration text).

  212. def OAI.CKSSchwarzschild.christoffelPair line 3251

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3251 (same declaration text).

  213. def OAI.CKSSchwarzschild.firstFrame line 3255

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3255 (same declaration text).

  214. def OAI.CKSSchwarzschild.secondResidual line 3259

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3259 (same declaration text).

  215. def OAI.CKSSchwarzschild.secondFrame line 3264

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3264 (same declaration text).

  216. theorem OAI.CKSSourceExterior.area_controlled_end_replacement Challenge statement: Spacetime Penrose inequalities: enclosing area, charge, rotation, and anti-de Sitter extensions sorry line 3312

    L4DEL explanation

    The formalization replaces a three-dimensional Cha–Khuri–Sakovich hyperboloidal end by asymptotically flat ends while preserving each fixed compact interior, completeness, and the dominant energy condition. For strictly future-timelike initial-data charge, the ADM masses approach the invariant Bondi mass and the loss of enclosing area tends to zero. The Comparator also includes canonical Schwarzschild equality examples at every positive mass, with $m_{\mathrm{Bondi}}=m$ and enclosing area $16\pi m^2$. The paper's general Bondi–Penrose inequality for possibly disconnected weakly trapped boundaries remains unformalized. The implementation retains a conditional inequality for the connected marginal-boundary case, assuming the asymptotically flat exterior Penrose inequality. This supporting result is not selected as a substitute for the paper's main inequality.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.Geometry.Relativity.CKS.ComparatorMain as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Geometry/Relativity/CKS/SourceReplacement.lean:19 (different declaration text). Qualify references as OAI.CKSSourceExterior.area_controlled_end_replacement@path.

    theorem area_controlled_end_replacement
    (g : OAI.CKSMetricGluing.SmoothMetric OAI.CKSGeometricCuts.I3 (M := N)) (K : OAI.CKSMetricGluing.InnerField OAI.CKSGeometricCuts.I3 (M := N))
…

    Mentions: OAI.CKSMetricGluing.SmoothMetric, OAI.CKSGeometricCuts.I3, OAI.CKSMetricGluing.InnerField

  217. def OAI.CKSMain.secondForm line 3367

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3326 (same declaration text).

  218. def OAI.CKSMain.meanCurvature line 3372

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3331 (same declaration text).

  219. def OAI.CKSMain.tangentialTrace line 3377

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3336 (same declaration text).

  220. structure OAI.CKSMain.BoundaryGeometry line 3394

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3353 (same declaration text).

  221. def OAI.CKSMain.BoundaryGeometry.parameter line 3404

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3363 (same declaration text).

  222. def OAI.CKSMain.BoundaryGeometry.thetaPlus line 3408

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3367 (same declaration text).

  223. def OAI.CKSMain.MarginalBoundary line 3416

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3375 (same declaration text).

  224. def OAI.CKSMain.bondiMass line 3419

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3378 (same declaration text).

  225. abbrev OAI.CKSMain.CoefficientAtlas line 3447

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3406 (same declaration text).

  226. structure OAI.CKSMain.InteriorSurface line 3466

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3425 (same declaration text).

  227. def OAI.CKSMain.InteriorSurface.parameter line 3495

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3454 (same declaration text).

  228. def OAI.CKSMain.InteriorSurface.mean line 3498

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3457 (same declaration text).

  229. def OAI.CKSMain.InteriorSurface.trace line 3503

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3462 (same declaration text).

  230. def OAI.CKSMain.InteriorSurface.thetaPlus line 3507

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3466 (same declaration text).

  231. def OAI.CKSMain.InteriorSurface.thetaMinus line 3509

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3468 (same declaration text).

  232. def OAI.CKSMain.InteriorSurface.SeparatesAway line 3511

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3470 (same declaration text).

  233. def OAI.CKSMain.InteriorSurface.ComponentwiseApparent line 3516

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3475 (same declaration text).

  234. def OAI.CKSMain.NoAdditionalHorizons line 3532

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3491 (same declaration text).

  235. structure OAI.CKSMain.MainHypotheses line 3538

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3497 (same declaration text).

  236. def OAI.CKSMain.SchwarzschildExample line 3568

    Also declared: OAI/Geometry/Relativity/CKS/ComparatorDefinitions.lean:3527 (same declaration text).

  237. theorem OAI.CKSMain.schwarzschild_equality_examples Challenge statement: Spacetime Penrose inequalities: enclosing area, charge, rotation, and anti-de Sitter extensions sorry line 3591

    L4DEL explanation

    The formalization replaces a three-dimensional Cha–Khuri–Sakovich hyperboloidal end by asymptotically flat ends while preserving each fixed compact interior, completeness, and the dominant energy condition. For strictly future-timelike initial-data charge, the ADM masses approach the invariant Bondi mass and the loss of enclosing area tends to zero. The Comparator also includes canonical Schwarzschild equality examples at every positive mass, with $m_{\mathrm{Bondi}}=m$ and enclosing area $16\pi m^2$. The paper's general Bondi–Penrose inequality for possibly disconnected weakly trapped boundaries remains unformalized. The implementation retains a conditional inequality for the connected marginal-boundary case, assuming the asymptotically flat exterior Penrose inequality. This supporting result is not selected as a substitute for the paper's main inequality.

    1. This is an exact comparator target linked by the pinned repository's formalization note for this result.
    2. The repository's comparator configuration selects OAI.Geometry.Relativity.CKS.ComparatorMain as the released solution module checked against this declaration.

    Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)

    Distinct definitions of this name: OAI/Geometry/Relativity/CKS/ComparatorMain.lean:12 (same statement text; different proof or body). Qualify references as OAI.CKSMain.schwarzschild_equality_examples@path.

    theorem schwarzschild_equality_examples (m : ℝ) (hm : 0 < m) :
    SchwarzschildExample.{v} m hm := by
…