OAI.SharpNodal.Profiles.profile_small_affine_grid_gap: intermediate lemma from OpenAI, Sharp nodal length on smooth surfaces

An intermediate lemma of the split of OpenAI's proof of OAI.SharpNodal.Main, carved from OpenAI's openai/math development for this platform. The statement and its proof are OpenAI's (OpenAI, Sharp nodal length on smooth surfaces, OpenAI Math Release, September 23, 2026, result family 350, github.com/openai/math, Apache License 2.0); in Lean it is the declaration OAI.SharpNodal.Profiles.profile_small_affine_grid_gap of lean/OAI/Analysis/NodalLength/NodalLength/Persistence.lean at commit adc7f12, ported to Lean 4.33.1 and Mathlib 0df444a.

The statement, as published (namespace OAI.SharpNodal.Profiles, with open scoped ContDiff Bundle ENNReal, open Bundle Manifold MeasureTheory, open scoped ContDiff ENNReal Topology, open MeasureTheory Filter Set, open scoped Topology ENNReal, open MeasureTheory Filter Set, open scoped Topology ENNReal ContDiff, open MeasureTheory Filter Set, open scoped Topology ENNReal ContDiff, open MeasureTheory Filter Set, open scoped Topology ENNReal ContDiff, open MeasureTheory Filter Set, open scoped Topology ContDiff, open Filter Set, open scoped Topology ContDiff, open Filter Set, open scoped Topology ENNReal, open Filter Set MeasureTheory TopologicalSpace, open scoped Topology ContDiff, open Filter Set, open scoped Topology ENNReal, open Filter Set MeasureTheory TopologicalSpace, open scoped Topology ENNReal ContDiff, open Filter Set MeasureTheory TopologicalSpace, open scoped Topology ENNReal ContDiff, open Filter Set MeasureTheory, open scoped Topology ENNReal ContDiff, open Filter Set MeasureTheory, open scoped Topology ENNReal ContDiff, open Filter Set MeasureTheory, open scoped Topology ENNReal ContDiff, open Filter Set MeasureTheory, open scoped Topology ENNReal ContDiff, open Filter Set MeasureTheory Laplacian, open scoped Topology ENNReal ContDiff ComplexConjugate, open Filter Set MeasureTheory Laplacian, open scoped Topology ENNReal ContDiff ComplexConjugate, open Filter Set MeasureTheory Laplacian, open scoped Topology ENNReal NNReal, open Filter Set MeasureTheory, open scoped Topology ENNReal ContDiff, open Filter Set MeasureTheory, open scoped Topology ENNReal ContDiff, open Filter Set MeasureTheory, open scoped Topology ENNReal, open Set MeasureTheory Filter, open scoped Topology ENNReal, open Filter Set MeasureTheory, open scoped Topology ENNReal, open Filter Set MeasureTheory, open scoped Topology ENNReal, open Filter Set MeasureTheory, open scoped Topology ContDiff, open Filter Set MeasureTheory, open scoped Topology ContDiff Laplacian, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ContDiff, open Filter Set MeasureTheory, open scoped Topology ENNReal, open Filter Set MeasureTheory, open scoped Topology ENNReal ContDiff, open Filter Set MeasureTheory, open scoped Topology ENNReal ContDiff, open Filter Set MeasureTheory, open scoped Topology ENNReal ContDiff, open Filter Set MeasureTheory, open scoped Topology ENNReal ContDiff, open Filter Set MeasureTheory, open scoped Topology ENNReal ContDiff CompactlySupported, open Set MeasureTheory, open scoped Topology ENNReal ContDiff CompactlySupported, open Set MeasureTheory, open scoped Topology ENNReal ContDiff CompactlySupported, open Set MeasureTheory, open scoped Topology ContDiff, open Filter Set MeasureTheory, open scoped Topology ContDiff, open Filter Set MeasureTheory, open scoped Topology ContDiff, open Filter Set MeasureTheory, open scoped Topology ContDiff, open Filter Set MeasureTheory, open scoped Topology ContDiff, open Filter Set MeasureTheory, open scoped Topology ContDiff, open Filter Set MeasureTheory, open scoped Topology ContDiff Laplacian, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ContDiff Convolution, open Filter Set MeasureTheory, open scoped Topology ContDiff Convolution, open Filter Set MeasureTheory, open scoped Topology ContDiff Convolution, open Filter Set MeasureTheory, open scoped Topology ContDiff Convolution, open Filter Set MeasureTheory, open scoped Topology ContDiff Convolution, open Filter Set MeasureTheory, open scoped Topology ContDiff Convolution ENNReal, open Filter Set MeasureTheory, open scoped Topology ContDiff ENNReal, open Filter Set MeasureTheory, open scoped Topology ContDiff ENNReal, open Filter Set MeasureTheory, open scoped Topology ContDiff ENNReal, open Filter Set MeasureTheory, open scoped Topology ContDiff, open Filter Set MeasureTheory, open scoped Topology ContDiff, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ContDiff, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ContDiff, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ContDiff, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ContDiff, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ContDiff ENNReal, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ContDiff ENNReal, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ContDiff, open Filter Set MeasureTheory Function, open scoped Topology, open Filter Set MeasureTheory, open scoped Topology ENNReal, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ENNReal, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ENNReal ContDiff, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ENNReal ContDiff, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ENNReal, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ENNReal, open Filter Set MeasureTheory, open scoped Topology ENNReal, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ENNReal ContDiff, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ENNReal, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ENNReal ContDiff, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ENNReal ContDiff, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ENNReal ContDiff, open Filter Set MeasureTheory InnerProductSpace, open scoped BigOperators, open Filter Set MeasureTheory, open scoped BigOperators, open scoped Topology ContDiff, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ContDiff, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ContDiff, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ContDiff, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ContDiff Convolution, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ContDiff, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology ContDiff, open Filter Set MeasureTheory InnerProductSpace, open scoped Topology, open Filter Set MeasureTheory, open scoped Topology ContDiff, open Filter Set MeasureTheory InnerProductSpace, open Carleman):

theorem profile_small_affine_grid_gap {A : ℕ} (hA : 1<A) {R σ : ℝ} (hR : 1≤R) (hσ : 0<σ)
    {V : Plane → EReal} (hV : UpperSemicontinuous V)
    (hneg : ∀x∈Metric.ball (0:Plane) 1000,V x≤0)
    (htest : FullTestProperty (Metric.ball 0 1000) V)
    (hanchor : ∃a∈Metric.closedBall (0:Plane) 1,(-1:EReal)≤V a)
    (hnonconstant : ∃x∈Metric.ball (0:Plane) 2,∃y∈Metric.ball (0:Plane) 2,V x≠V y)
    (m₀ : ℕ) :
    ∃m≥m₀,∃p : Fin 2 → ℤ,∃c : Plane,∃e : ℝ,
      let r := ((A:ℝ)⁻¹)^m
      let y := extendedGridCenter r p
      0<‖c‖ ∧ ‖y‖+2*R*r<3 ∧ R*r<1/4 ∧ e<σ*r*‖c‖ ∧
      (⨆x∈Metric.closedBall y (R*r),V x-(inner ℝ c (x-y):EReal))≤
        (⨆x∈Metric.ball y r,V x-(inner ℝ c (x-y):EReal))+(e:EReal)

Definitions. The statement is written with OAI.SharpNodal.Profiles.FullTestProperty and OAI.SharpNodal.Profiles.extendedGridCenter (definitions bundle OAIQ4Nl000 of this split); OAI.SharpNodal.Plane (the published bundle Def_NodalLength).

Used by. The proof of OAI.SharpNodal.Profiles.uniform_persistence_alternative of this split imports it.