`ComparatorChallenges/WeakHessian.lean`

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

Annotation provenance. This overlay contains 120 curated AI-written annotations and 1273 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 9 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. Those 9 annotations were revised on 2026-10-14 to bind all of them to exact page-one quotations from 6 pinned OpenAI manuscripts, the matching pinned formalization notes, and named historical primary sources; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. The 3 manuscript-grounded matrix-multiplication annotations were composed from pinned OpenAI manuscripts and named historical sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Six additional target-specific annotations for Catalan's constant, the irrationality exponent of pi, dyadic Erdos similarity, Unique Games, quintic Lienard systems, and Yau nodal growth were composed from pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and named historical sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for Seymour's second-neighborhood conjecture, Cannon's conjecture, Koebe circle-domain uniformization, and circle-domain rigidity were composed from 4 pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and named historical primary sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for simple Lebesgue spectrum on the three-torus, Rokhlin multiple mixing, the nine-dimensional Borsuk counterexample, and Tingley's sphere-isometry problem were composed from 4 pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and named historical primary sources in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for the Abhyankar-Sathaye counterexample, the circulant Hadamard conjecture, the Eilenberg-Ganea counterexample, and short Egyptian fractions were composed from 4 pinned OpenAI manuscripts, exact page-one quotations, exact Lean statements, and quotations from Sathaye, Turyn with Storer, Eilenberg with Ganea, and Erdos in a Codex session on 2026-10-14; no human review is claimed, and the exact runtime model identifier was not exposed to the artifact generator. Four additional target-specific annotations for the complete Crouzeix inequality, unrestricted Euclidean five-coloring, the general Mahler conjecture, and Thompson F nonamenability were composed on 2026-10-14 from exact Lean statements, 4 pinned OpenAI manuscripts, the matching formalization notes, and linked historical sources by Crouzeix, de Grey, Mahler, Cannon, Floyd, and Parry; no human review is claimed. Four additional target-specific annotations for algorithmic strong thin trees, Barnette's Hamiltonian-cycle conjecture, the explicit Artin CAT(0) counterexample, and generalized amplitude-damping capacity were composed on 2026-10-14 from exact Lean statements, 4 pinned OpenAI manuscripts, matching formalization notes, and linked historical sources by Anari with Goddyn, Arts with Hopman and Timmermans, Charney, and Khatri with Sharma and Wilde; no human review is claimed. Fourteen solution-level annotations for Seymour's second-neighborhood theorem were added on 2026-10-14 from the pinned 15-page manuscript, covering the exact-neighborhood model, minimal-counterexample reduction, subset deficit, transitive blowup, pruning, extremal contradiction, and proof-bearing final theorem. The subset and blowup annotations also bind exact quotations from Tyler Seacrest (2019) and Brantner, Brockman, Kay, and Snively (2009); no human review is claimed. Thirty-seven declaration-level annotations were added on 2026-10-14 for the rest of ComparatorChallenges/AlgorithmicThinTrees.lean, covering its multigraph semantics, stack-machine cost model, explicit and binary-multiplicity encodings, output certificate, and complete algorithmic proposition. They are bound to the pinned OpenAI manuscript and linked earlier thin-tree sources by Luis Goddyn, Nima Anari, and Shayan Oveis Gharan; the annotation explicitly preserves that the concluding comparator theorem still has body by sorry, and no human review is claimed. Thirty-one supporting declarations in ComparatorChallenges/UniqueGamesTheorem.lean were upgraded or added on 2026-10-14, completing curated coverage of all thirty-two declarations in that file. The annotations cover the finite game model, Boolean formula and parser, binary-vector translations, explicit output serialization, finite-alphabet machine contract, and gap theorem; they distinguish manuscript-backed mathematics from Lean-specific canonical parsing and unary game output encoding, bind exact OpenAI manuscript quotations, and credit Subhash Khot through his 2010 survey. The comparator theorem remains explicitly labeled as having body by sorry; no human review is claimed. The source-derived generator was hardened on 2026-10-14 so a formalization note covering multiple comparator results no longer copies its combined Scope prose onto each declaration; those targets now use declaration-specific source comments when available and otherwise remain explicitly bounded to the exact Lean statement. The remaining source-derived annotations were generated mechanically from pinned formalization notes and source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the source prose.

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

46 declarations, 1 contain sorry, 0 declared as axioms

abbrev OAI.WeakHessian.Time line 12
Also declared: OAI/Geometry/WeakHessian/Model.lean:12 (same declaration text).
def OAI.WeakHessian.timeZero line 14
Also declared: OAI/Geometry/WeakHessian/Model.lean:14 (same declaration text).
def OAI.WeakHessian.timeOne line 15
Also declared: OAI/Geometry/WeakHessian/Model.lean:15 (same declaration text).
def OAI.WeakHessian.clampTime line 17
Also declared: OAI/Geometry/WeakHessian/Model.lean:17 (same declaration text).
abbrev OAI.WeakHessian.Curve line 22
Also declared: OAI/Geometry/WeakHessian/Model.lean:22 (same declaration text).
instance OAI.WeakHessian.curveMeasurableSpace line 24
Also declared: OAI/Geometry/WeakHessian/Model.lean:24 (same declaration text).
instance OAI.WeakHessian.curveBorelSpace line 26
Also declared: OAI/Geometry/WeakHessian/Model.lean:26 (same declaration text).
def OAI.WeakHessian.evalReal line 28
Also declared: OAI/Geometry/WeakHessian/Model.lean:28 (same declaration text).
def OAI.WeakHessian.IsGeodesic The constant-speed minimizing parametrization, including constant curves line 31
Source documentation
The constant-speed minimizing parametrization, including constant curves.
L4DEL explanation
The constant-speed minimizing parametrization, including constant curves.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Geometry/WeakHessian/Model.lean:31 (same declaration text).
```
def IsGeodesic (γ : Curve X) : Prop :=
…
```
Mentions: OAI.WeakHessian.Curve
def OAI.WeakHessian.metricSpeed Metric speed line 36
Source documentation
Metric speed. Limsup agrees a.e. with the metric derivative on AC² curves.
L4DEL explanation
Metric speed. Limsup agrees a.e. with the metric derivative on AC² curves.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Geometry/WeakHessian/Model.lean:36 (same declaration text).
```
def metricSpeed (γ : Curve X) (t : ℝ) : ℝ≥0∞ :=
…
```
Mentions: OAI.WeakHessian.Curve
def OAI.WeakHessian.IsAC2 Absolute continuity with a square-integrable metric control line 41
Source documentation
Absolute continuity with a square-integrable metric control.
L4DEL explanation
Absolute continuity with a square-integrable metric control.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Geometry/WeakHessian/Model.lean:41 (same declaration text).
```
def IsAC2 (γ : Curve X) : Prop :=
…
```
Mentions: OAI.WeakHessian.Curve
def OAI.WeakHessian.IsTestPlan A 2-test plan: bounded compression and finite average kinetic energy line 50
Source documentation
A 2-test plan: bounded compression and finite average kinetic energy.
L4DEL explanation
A 2-test plan: bounded compression and finite average kinetic energy.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Geometry/WeakHessian/Model.lean:50 (same declaration text).
```
def IsTestPlan (m : Measure X) (π : Measure (Curve X)) : Prop :=
…
```
Mentions: OAI.WeakHessian.Curve
def OAI.WeakHessian.BoundedTracks Uniform bounded spatial support; used only to define the local Sobolev class line 58
Source documentation
Uniform bounded spatial support; used only to define the local Sobolev class.
L4DEL explanation
Uniform bounded spatial support; used only to define the local Sobolev class.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Geometry/WeakHessian/Model.lean:58 (same declaration text).
```
def BoundedTracks (π : Measure (Curve X)) : Prop :=
…
```
Mentions: OAI.WeakHessian.Curve
def OAI.WeakHessian.LocallyL2 line 61
Also declared: OAI/Geometry/WeakHessian/Model.lean:61 (same declaration text).
def OAI.WeakHessian.IsLocalWeakUpperGradient Local weak upper gradients, in the integrated test-plan definition line 65
Source documentation
Local weak upper gradients, in the integrated test-plan definition.
L4DEL explanation
Local weak upper gradients, in the integrated test-plan definition.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Geometry/WeakHessian/Model.lean:65 (same declaration text).
```
def IsLocalWeakUpperGradient (m : Measure X) (f D : X → ℝ) : Prop :=
…
```
def OAI.WeakHessian.IsMinimalLocalWeakUpperGradient line 72
Also declared: OAI/Geometry/WeakHessian/Model.lean:72 (same declaration text).
def OAI.WeakHessian.weakGradient A representative of the minimal weak upper gradient (zero off its domain) line 77
Source documentation
A representative of the minimal weak upper gradient (zero off its domain).
L4DEL explanation
A representative of the minimal weak upper gradient (zero off its domain).
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Geometry/WeakHessian/Model.lean:77 (same declaration text).
```
def weakGradient (m : Measure X) (f : X → ℝ) : X → ℝ :=
…
```
def OAI.WeakHessian.LocalSobolev line 81
Also declared: OAI/Geometry/WeakHessian/Model.lean:81 (same declaration text).
def OAI.WeakHessian.Sobolev line 84
Also declared: OAI/Geometry/WeakHessian/Model.lean:84 (same declaration text).
def OAI.WeakHessian.gamma Polarization of the minimal weak gradient on an infinitesimally Hilbertian space line 88
Source documentation
Polarization of the minimal weak gradient on an infinitesimally Hilbertian space.
L4DEL explanation
Polarization of the minimal weak gradient on an infinitesimally Hilbertian space.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Geometry/WeakHessian/Model.lean:88 (same declaration text).
```
def gamma (m : Measure X) (f g : X → ℝ) (x : X) : ℝ :=
…
```
def OAI.WeakHessian.IsLaplacian Weak nonpositive generator convention, without a global L² assumption on F line 93
Source documentation
Weak nonpositive generator convention, without a global L² assumption on F.
L4DEL explanation
Weak nonpositive generator convention, without a global L² assumption on F.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Geometry/WeakHessian/Model.lean:93 (same declaration text).
```
def IsLaplacian (m : Measure X) (u L : X → ℝ) : Prop :=
…
```
def OAI.WeakHessian.InLaplacianDomain line 98
Also declared: OAI/Geometry/WeakHessian/Model.lean:98 (same declaration text).
def OAI.WeakHessian.laplacian line 101
Also declared: OAI/Geometry/WeakHessian/Model.lean:101 (same declaration text).
def OAI.WeakHessian.BoundedFunction line 104
Also declared: OAI/Geometry/WeakHessian/Model.lean:104 (same declaration text).
def OAI.WeakHessian.GloballyLipschitz line 106
Also declared: OAI/Geometry/WeakHessian/Model.lean:106 (same declaration text).
def OAI.WeakHessian.IsTestFunction Bounded globally Lipschitz Laplacian-domain functions with Sobolev Laplacian line 109
Source documentation
Bounded globally Lipschitz Laplacian-domain functions with Sobolev Laplacian.
L4DEL explanation
Bounded globally Lipschitz Laplacian-domain functions with Sobolev Laplacian.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Geometry/WeakHessian/Model.lean:109 (same declaration text).
```
def IsTestFunction (m : Measure X) (g : X → ℝ) : Prop :=
…
```
def OAI.WeakHessian.weakHessian The weak Hessian, with ∇_(∇g)∇g = ∇(Γ(g)/2) line 114
Source documentation
The weak Hessian, with ∇_(∇g)∇g = ∇(Γ(g)/2).
L4DEL explanation
The weak Hessian, with ∇_(∇g)∇g = ∇(Γ(g)/2).
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Geometry/WeakHessian/Model.lean:114 (same declaration text).
```
def weakHessian (m : Measure X) (F g h : X → ℝ) : ℝ :=
…
```
def OAI.WeakHessian.WeakHessianUpperBound line 118
Also declared: OAI/Geometry/WeakHessian/Model.lean:118 (same declaration text).
def OAI.WeakHessian.localSlope Asymptotic Lipschitz slope; zero at an isolated point line 125
Source documentation
Asymptotic Lipschitz slope; zero at an isolated point.
L4DEL explanation
Asymptotic Lipschitz slope; zero at an isolated point.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Geometry/WeakHessian/Model.lean:125 (same declaration text).
```
def localSlope (f : X → ℝ) (x : X) : ℝ≥0∞ :=
…
```
def OAI.WeakHessian.cheegerEnergy Cheeger energy is the L² relaxation of one half the squared local slope line 129
Source documentation
Cheeger energy is the L² relaxation of one half the squared local slope.
L4DEL explanation
Cheeger energy is the L² relaxation of one half the squared local slope.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Geometry/WeakHessian/Model.lean:129 (same declaration text).
```
def cheegerEnergy (m : Measure X) (f : X → ℝ) : ℝ≥0∞ :=
…
```
def OAI.WeakHessian.QuadraticCheegerEnergy line 138
Also declared: OAI/Geometry/WeakHessian/Model.lean:138 (same declaration text).
def OAI.WeakHessian.sigmaCoeff The unreduced Lott–Sturm–Villani distortion coefficient σ line 144
Source documentation
The unreduced Lott–Sturm–Villani distortion coefficient σ.
L4DEL explanation
The unreduced Lott–Sturm–Villani distortion coefficient σ.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Geometry/WeakHessian/Model.lean:144 (same declaration text).
```
def sigmaCoeff (K N t θ : ℝ) : ℝ≥0∞ :=
…
```
def OAI.WeakHessian.tauCoeff The τ coefficient (not the reduced σ coefficient) in CD(K,N) line 157
Source documentation
The τ coefficient (not the reduced σ coefficient) in CD(K,N).
L4DEL explanation
The τ coefficient (not the reduced σ coefficient) in CD(K,N).
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Geometry/WeakHessian/Model.lean:157 (same declaration text).
```
def tauCoeff (K N t θ : ℝ) : ℝ≥0∞ :=
…
```
def OAI.WeakHessian.HasSecondMoment line 160
Also declared: OAI/Geometry/WeakHessian/Model.lean:160 (same declaration text).
def OAI.WeakHessian.IsCoupling line 163
Also declared: OAI/Geometry/WeakHessian/Model.lean:163 (same declaration text).
def OAI.WeakHessian.QuadraticTransportCost line 166
Also declared: OAI/Geometry/WeakHessian/Model.lean:166 (same declaration text).
def OAI.WeakHessian.IsOptimalCoupling line 169
Also declared: OAI/Geometry/WeakHessian/Model.lean:169 (same declaration text).
def OAI.WeakHessian.endpointCoupling line 173
Also declared: OAI/Geometry/WeakHessian/Model.lean:173 (same declaration text).
def OAI.WeakHessian.interpolation line 176
Also declared: OAI/Geometry/WeakHessian/Model.lean:176 (same declaration text).
def OAI.WeakHessian.renyiIntegral The positive of minus the N-Rényi entropy; singular mass contributes zero line 180
Source documentation
The positive of minus the N-Rényi entropy; singular mass contributes zero.
L4DEL explanation
The positive of minus the N-Rényi entropy; singular mass contributes zero.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Geometry/WeakHessian/Model.lean:180 (same declaration text).
```
def renyiIntegral (m μ : Measure X) (N : ℝ) : ℝ≥0∞ :=
…
```
def OAI.WeakHessian.CurvatureDimension Unreduced CD(K,N), written with the standard dynamical optimal-plan formula line 184
Source documentation
Unreduced CD(K,N), written with the standard dynamical optimal-plan formula.
L4DEL explanation
Unreduced CD(K,N), written with the standard dynamical optimal-plan formula.
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Geometry/WeakHessian/Model.lean:184 (same declaration text).
```
def CurvatureDimension (m : Measure X) (K N : ℝ) : Prop :=
…
```
def OAI.WeakHessian.RCD line 200
Also declared: OAI/Geometry/WeakHessian/Model.lean:200 (same declaration text).
def OAI.WeakHessian.FullSupport line 203
Also declared: OAI/Geometry/WeakHessian/Model.lean:203 (same declaration text).
def OAI.WeakHessian.FiniteOnBoundedSets line 206
Also declared: OAI/Geometry/WeakHessian/Model.lean:206 (same declaration text).
def OAI.WeakHessian.CurveSecondDerivativeBound The literal second-distributional-derivative conclusion on (0,1) line 210
Source documentation
The literal second-distributional-derivative conclusion on (0,1).
L4DEL explanation
The literal second-distributional-derivative conclusion on (0,1).
1. This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Also declared: OAI/Geometry/WeakHessian/Model.lean:210 (same declaration text).
```
def CurveSecondDerivativeBound (F G : X → ℝ) (σ : Curve X) : Prop :=
…
```
Mentions: OAI.WeakHessian.Curve
theorem OAI.WeakHessian.every_geodesic Challenge statement: Gigli’s characterization of Alexandrov curvature sorry line 220
Source documentation
A weak upper Hessian bound controls the second distributional derivative along every constant-speed minimizing geodesic.
L4DEL explanation
The formalization transfers a weak Hessian upper bound to every prescribed minimizing geodesic in an $\mathrm{RCD}(K,N)$ space with finite $N>1$. If a bounded globally Lipschitz function $F$ has weak Hessian bounded above by $G$ times the metric, where $G$ is bounded and continuous, then every constant-speed geodesic $\gamma:[0,1]\to X$ satisfies $(F\circ\gamma)''\le G(\gamma)\,d(\gamma(0),\gamma(1))^2$ in the distributional sense. Constant geodesics are included. The space is complete and separable with full support and measure finite on bounded sets; compactness and metric nonbranching are not assumed.
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.WeakHessian.Main as the released solution module checked against this declaration.
Sources and attribution: Pinned Lean source (fd4aeeb2ee4f)
Distinct definitions of this name: OAI/Geometry/WeakHessian/Main.lean:38 (same statement text; different proof or body). Qualify references as OAI.WeakHessian.every_geodesic@path.
```
theorem every_geodesic [CompleteSpace X] [TopologicalSpace.SeparableSpace X]
    (m : Measure X) (K N : ℝ) (hN : 1 < N)
    (hfull : FullSupport m) (hfinite : FiniteOnBoundedSets m) (hrcd : RCD m K N)
    (F G : X → ℝ) (hFbound : BoundedFunction F) (hFlip : GloballyLipschitz F)
    (hGbound : BoundedFunction G) (hGcont : Continuous G)
    (hHess : WeakHessianUpperBound m F G)
    (σ : Curve X) (hσ : IsGeodesic σ) : CurveSecondDerivativeBound F G σ := by
…
```
Mentions: OAI.WeakHessian.FullSupport, OAI.WeakHessian.FiniteOnBoundedSets, OAI.WeakHessian.RCD, OAI.WeakHessian.BoundedFunction, OAI.WeakHessian.GloballyLipschitz, OAI.WeakHessian.WeakHessianUpperBound, OAI.WeakHessian.Curve, OAI.WeakHessian.IsGeodesic, OAI.WeakHessian.CurveSecondDerivativeBound