PlanarMultiwellScale.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A fixed planar excitation gap for exponentially many separated sites. The scale is chosen once from the isolated-well gap, independently of the number of sites and the input instance.

theorem OAI.ContinuumCoulomb.planarSiteDerivativeBound_tendsto line 15

theorem OAI.ContinuumCoulomb.exists_planar_multiwell_loss_threshold line 25

Source documentation

One fixed separation threshold controls both the IMS loss and the sum of cutoff tails for all site counts at most exp(19 D / 320).

theorem exists_planar_multiwell_loss_threshold {γ : ℝ} (hγ : 0 < γ) :
    ∃ R : ℝ, 8 ≤ R ∧ ∀ D : ℝ, R ≤ D → ∀ m : ℕ,
      (m : ℝ) ≤ Real.exp ((19/320 : ℝ) * D) →
      planarSiteDerivativeBound D ^ 2 +
        γ * m * planarSiteTailConstant * Real.exp (-(19/20 : ℝ) * (D/8)) ≤ γ / 2 := by
…

Mentions: OAI.ContinuumCoulomb.planarSiteDerivativeBound, OAI.ContinuumCoulomb.planarSiteTailConstant

theorem OAI.ContinuumCoulomb.exists_uniform_multiwell_scale line 59

Source documentation

A single polynomial exponent meets the fixed separation cutoff and supports every polynomial site count for every input size at least two.

theorem exists_uniform_multiwell_scale (A : ℕ) (R : ℝ) {c : ℝ} (hc : 0 < c) :
    ∃ k : ℕ, 0 < k ∧ ∀ N : ℝ, 2 ≤ N →
      R ≤ c * ((k : ℝ) * Real.log N) ∧
      N ^ A ≤ Real.exp ((19/320 : ℝ) * (c * ((k : ℝ) * Real.log N))) := by
…

theorem OAI.ContinuumCoulomb.planarWellSum_uniform_test_complement_gap line 90

Source documentation

Conditional only on the published isolated-well gap. The full spatial multiwell geometry and the aggregate tail error have already been bounded.

theorem planarWellSum_uniform_test_complement_gap
    (hpublished : PlanarSobolev.ManufacturedPlanarGroundGap) :
    ∃ γ R : ℝ, 0 < γ ∧ γ ≤ 1/4 ∧ 8 ≤ R ∧
      ∀ (m : ℕ) (D : ℝ), R ≤ D → (m : ℝ) ≤ Real.exp ((19/320 : ℝ) * D) →
      ∀ u : Fin m → PlanarPosition, (∀ i j, i ≠ j → D ≤ ‖u i-u j‖) →
      ∀ f : PlanarPosition → ℝ, ContDiff ℝ 1 f → HasCompactSupport f →
      (∀ i, (∫ x, f x * normalizedPlanarMode (x-u i)) = 0) →
      ((-1/2 : ℝ) + γ/2) * (∫ x, f x^2) ≤ planarTestForm (planarWellSum u) f := by
…

Mentions: OAI.ContinuumCoulomb.PlanarSobolev.ManufacturedPlanarGroundGap, OAI.ContinuumCoulomb.PlanarPosition, OAI.ContinuumCoulomb.normalizedPlanarMode, OAI.ContinuumCoulomb.planarTestForm, OAI.ContinuumCoulomb.planarWellSum

theorem OAI.ContinuumCoulomb.planarWellSum_polynomial_test_complement_gap line 109

Source documentation

Reduction-scale version: a fixed exponent works uniformly for all input sizes and every separated configuration with polynomially many sites.

theorem planarWellSum_polynomial_test_complement_gap
    (hpublished : PlanarSobolev.ManufacturedPlanarGroundGap)
    (A : ℕ) {c : ℝ} (hc : 0 < c) :
    ∃ γ : ℝ, 0 < γ ∧ ∃ k : ℕ, 0 < k ∧ ∀ N : ℝ, 2 ≤ N →
      ∀ m : ℕ, (m : ℝ) ≤ N ^ A → ∀ u : Fin m → PlanarPosition,
      (∀ i j, i ≠ j → c*((k : ℝ)*Real.log N) ≤ ‖u i-u j‖) →
      ∀ f : PlanarPosition → ℝ, ContDiff ℝ 1 f → HasCompactSupport f →
      (∀ i, (∫ x, f x*normalizedPlanarMode (x-u i)) = 0) →
      ((-1/2 : ℝ)+γ) * (∫ x, f x^2) ≤ planarTestForm (planarWellSum u) f := by
…