Prove2Me

Pointwise spatial bounds for the hyperbolic QQ-form of the height equation

Proved
OAI.SmoothLocal.HighEquation.exists_finite_actual_Q_spatial_pointwise_bound

by wurtle · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-geometryisometric-immersion

Notation. S=[−3,3]2S=[-3,3]^2 is the model square; a metric is a smooth positive matrix field gg; zz is a scalar height; H=∇g2zH=\nabla_g^2z is its covariant Hessian; KgK_g is the Gaussian curvature; E=det⁡g (1−∣dz∣g2)E=\det g\,(1-|dz|_g^2); q=Hxy/Hyyq=H_{xy}/H_{yy} is the Hessian quotient; κ(x2−h(y))\kappa(x^2-h(y)) is the model curvature; the patch box and the central box are the squares [−1/10,1/10]2[-1/10,1/10]^2 and [−1/5,1/5]2[-1/5,1/5]^2; the sheared coordinates are ξ=x, θ=y+q0x\xi=x,\ \theta=y+q_0x, with sheared height zsz_s; LL and v∗v_* are the class width and speed of (4.2); g~τ\tilde g_\tau is the test metric (4.12) built from g∗g_*; a bounded admissible height of bound MM is an admissible height with (4.1).

Fix a shrinking slab: endpoints xℓ,xrx_\ell,x_r, a speed, a time length TT, and a length floor below the slab's width at all times. For each order NN there is a constant BB such that the following holds. Let gg, zz be smooth on a coordinate rectangle containing the slab, satisfying the Darboux equation with Hxx≠0H_{xx}\ne0 on the rectangle, and suppose on the slab that QQ has its second-jet coefficient S1≥s0>0S_1\ge s_0>0, with ∣P1∣+S1≤|P_1|+\sqrt{S_1}\le speed, that the coordinates are bounded by RR, that gijg_{ij} has derivatives bounded by GG through order max⁡(9,N+3)\max(9,N+3) and zz by ZZ through order 88, ∣det⁡g∣≥d|\det g|\ge d, and ∣Hxx∣≥c|H_{xx}|\ge c. If all derivatives of zz through order max⁡(8,N+2)\max(8,N+2) are at most AA on the initial cut y=ay=a, then at every later time t∈[a,b]t\in[a,b] and every xx in the shrunken interval,

∣∂xn(∂iz)(x,t)∣≤B(i∈{1,2}, n≤N).\big|\partial_x^n(\partial_iz)(x,t)\big|\le B\qquad(i\in\{1,2\},\ n\le N).

This is the propagation of smooth tangential data along the hyperbolic region.

Formalization Note. This is the upstream Lean declaration OAI.SmoothLocal.HighEquation.exists_finite_actual_Q_spatial_pointwise_bound in lean/OAI/Geometry/IsometricImmersion/Darboux/QFiniteActual.lean, stated verbatim; the Lean statement is authoritative for the precise hypotheses. It is an intermediate result of OpenAI's formalization.

Preamble
import Mathlib
import Definitions.Def_IsometricImmersion
import Definitions.Def_SmoothLocalIsometricSupport

namespace OAI

noncomputable section
open Set
open scoped ContDiff Topology NNReal

namespace SmoothLocal.HighEquation
open SmoothLocal.Geometry SmoothLocal.Weighted SmoothLocal.ODE SmoothLocal.Hyperbolic
Formal statement
theorem exists_finite_actual_Q_spatial_pointwise_bound
    (G R Z s0 speed xl xr T lengthFloor : ℝ) (A : ℝ≥0)
    (hG : 0 ≤ G) (hR : 0 ≤ R) (hZ : 0 ≤ Z) (hs0 : 0 < s0)
    (hspeed : 0 ≤ speed) (hT : 0 ≤ T) (hlen : 0 < lengthFloor)
    (hwidth : lengthFloor ≤ xr - xl - 2 * speed * T)
    {d c : ℝ} (hd : 0 < d) (hc : 0 < c) (N : ℕ) :
    ∃ B : ℝ, 0 ≤ B ∧
      ∀ (g : MetricField) (z : Coord → ℝ) (radius lo hi a b : ℝ),
      SmoothPositiveOn g (coordinateRectangle radius lo hi) →
      ContDiffOn ℝ ∞ z (coordinateRectangle radius lo hi) →
      (∀ p ∈ coordinateRectangle radius lo hi,
        (covHessian g z p).det = gaussianCurvature g p * heightEnergy g z p) →
      (∀ p ∈ coordinateRectangle radius lo hi, covHessian g z p 0 0 ≠ 0) →
      0 < radius → a ≤ b → b - a ≤ T →
      -radius < xl → xr < radius → a ∈ Ioo lo hi → b ∈ Ioo lo hi →
      (∀ p ∈ shrinkingSlab xl xr a b speed, s0 ≤ heightQCoefficient g z 5 p) →
      (∀ p ∈ shrinkingSlab xl xr a b speed,
        |heightQCoefficient g z 4 p| + Real.sqrt (heightQCoefficient g z 5 p) ≤ speed) →
      (∀ p ∈ shrinkingSlab xl xr a b speed, |p 0| ≤ R ∧ |p 1| ≤ R) →
      (∀ i j, CoordinateBound (fun p => g p i j) (shrinkingSlab xl xr a b speed) (max 9 (N + 3)) G) →
      CoordinateBound z (shrinkingSlab xl xr a b speed) 8 Z →
      (∀ p ∈ shrinkingSlab xl xr a b speed, d ≤ |(g p).det|) →
      (∀ p ∈ shrinkingSlab xl xr a b speed, c ≤ |covHessian g z p 0 0|) →
      (∀ ds : List (Fin 2), ds.length ≤ max 8 (N + 2) → ∀ x ∈ Icc xl xr,
        |iteratedCoordPartial ds z (coordinatePoint x a)| ≤ (A : ℝ)) →
      ∀ t ∈ Icc a b, ∀ x ∈ Icc (inwardLeft xl a speed t) (inwardRight xr a speed t),
        ∀ i : Fin 2, ∀ n ≤ N,
          |spatialJet (spatialFirstJet z i) n (coordinatePoint x t)| ≤ B := by
  sorry

end SmoothLocal.HighEquation
end
end OAI
Source
OpenAI, A Smooth Metric with No Local Isometric Immersion into Three-Space, September 24, 2026, https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Smooth-Metric-with-No-Local-Isometric-Immersion-into-Three-Space-September-24-2026/paper.pdf; Lean: openai/math at adc7f1241b42e322a6451854ab7e4b4c146bf78a, lean/OAI/Geometry/IsometricImmersion/ (Apache License 2.0), file lean/OAI/Geometry/IsometricImmersion/Darboux/QFiniteActual.lean; Section 4.2, Lemma 4.1 and (4.15)

View graph