diff --git a/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md b/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md index a77286fb8..bc0e1f881 100644 --- a/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md +++ b/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md @@ -4,7 +4,7 @@ | Source | Path | Role | |---|---|---| -| SP | `reviews/d1_cap_elder_partner_second_pass_claude_20260930/REVIEW.md` | the line-numbered reconstruction of CAP §§2–5. L13, L16, L17 and L19–L22 are proved here. Since v1.5, L1, L2, L5, L7 (maximum and uniqueness), L8, L11's chain rule and L18 are also proved, from SP's normalization and L4's output (`ridge_capHyp_normalized`, `ridge_capHyp_sp`, `ridge_capHyp_of_slices`). Since v1.6, L3–L4 are proved from SP's (H1) and the third-derivative bounds on the transverse Hessian (`ridge_capHyp_H1`). Since v1.7, L7's existence and implicit-function regularity of `h` are proved (`ridge_exists`, `ridge_differentiable`). Since v1.8, L3–L4 are proved on a collar of `D` and the route up to L12 (`hconv`) is composed from SP's source data there (`ridge_capHyp_source`). Inputs that remain: L6 and L9–L12, and the source data themselves (I3). | +| SP | `reviews/d1_cap_elder_partner_second_pass_claude_20260930/REVIEW.md` | the line-numbered reconstruction of CAP §§2–5. L13, L16, L17 and L19–L22 are proved here. Since v1.5, L1, L2, L5, L7 (maximum and uniqueness), L8, L11's chain rule and L18 are also proved, from SP's normalization and L4's output (`ridge_capHyp_normalized`, `ridge_capHyp_sp`, `ridge_capHyp_of_slices`). Since v1.6, L3–L4 are proved from SP's (H1) and the third-derivative bounds on the transverse Hessian (`ridge_capHyp_H1`). Since v1.7, L7's existence and implicit-function regularity of `h` are proved (`ridge_exists`, `ridge_differentiable`). Since v1.8, L3–L4 are proved on a collar of `D` and the route up to L12 (`hconv`) is composed from SP's source data there (`ridge_capHyp_source`). Since v1.9, L6 and L9–L12 are proved and `ridge_capHyp_C3` derives `hconv` from the `C³` data. Inputs that remain: SP's `f_xxx ≥ 7/4` (L4, from L2 and (H2)) and the source data themselves (I3). | | CAP | `imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md` | the deterministic theorem that SP reconstructs | The source setting (SP §2) is as follows: @@ -79,6 +79,15 @@ The source setting (SP §2) is as follows: | `transverse_hessian_le_D` | as `transverse_hessian_le`, on the collar, with `0 < ε ≤ r/2` ⇒ `H(p) ≤ −(λ − 5rm)` | SP L4 ("on `D`, `|Δx| + ‖Δy‖ ≤ 9r/2 < 5r`") | On the collar `|x + r/2| ≤ 3r`, so the increment is at most `5r`; `ε ≤ r/2` is exactly what keeps SP's `5r`. | | `slices_strongConcave_D` | every slice over the collar is `(λ − 5rm)`-strongly concave on `B̄(0, 2r)` | SP L4 (`δ = λ − 5rm` on `D`) | Covers the open `U = (−2r − ε, 2r + ε) ⊇ [−2r, 2r]` that L7 needs. | | `ridge_capHyp_source` | `[FiniteDimensional ℝ E]`, on the collar `× B̄(0, 2r)`: joint derivative `Df`, strict derivative `DG` of `∂_y f = Df ∘ inr`, transverse Hessian `H` with L3's bounds `m`, (H1) `8rm² < λ` with `H(M) ≤ −λ`, pins `Df(∓r/2, 0) = 0`, the convexity pairs for `∂_x f(·, 0)` on `[−r/2, r/2]` and for `∂_y f(·, 0)` on the collar, gap `f(M) − f(S) = r³/6` ⇒ (i) a ridge exists on `U`; (ii) for every ridge on `U` (critical point in `B̄(0, 2r)`) with `hconv` for `F x = ∂_x f(x, h x)`: `h(∓r/2) = 0`, and (C1)–(C3), (C2⁺) on the cap with `M = (−r/2, 0)`, `z = (2r, h(2r))`, `b = f(M)`, `s = f(S)` | SP §2 normalization, (H1), L1–L5, L7, L8, L11, L16–L20; with L12 as `hconv` | The composition (I3). L5 on the collar gives `‖∂_y f(x, 0)‖ ≤ 3mr² < 2rδ` (`δ > 11rm`). That supplies `ridge_exists`, and through L8 the open-ball condition of `ridge_differentiable`. Uniqueness at the critical pins gives `h(∓r/2) = 0`. `DG ∘ inr = H` holds by uniqueness of derivatives, so it is negative definite. The strict hypothesis `DG` is SP's `f ∈ C²` near the ridge. `hconv` is stated for the ridge it quantifies over, which is unique. | +| `convex_deriv_sign`, `two_node_deriv_bound`, `slice_gradient_deriv_bound` | weak `|u''| ≤ m` (L5's convexity pair), `u(∓r/2) = 0`, `u' = d` at `x` ⇒ `|d| ≤ m · max(|x|, r/2)`; for `w` with derivative `w'`: `‖w'(x)‖ ≤ m · max(|x|, r/2)` | SP L6 (CAP (7): `‖w'(x)‖ ≤ (m/r)∫_a^c |x − t| dt ≤ 2mr`) | SP averages `w'(x) − w'(t)` over the pin interval. Lean uses chord slopes instead: the chord through the pins has slope `0`, which bounds `u'` outside `[a, c]` by `m|x|`, and the chord to `c` with L5's `|u(x)|` bound gives `mr/2` inside. The maximum on `[−2r, 2r]` is SP's `2mr`. | +| `schur_max` | bilinear `Q` with `Q (0, v) (0, v) ≤ −δ‖v‖²`, `Q (1, η) ∘ inr = 0` ⇒ `δ‖η‖ ≤ ‖Q (1, 0) ∘ inr‖`; `Q (1, η) (1, η) = Q (1, η) (1, 0)`; if symmetric, `Q (1, ζ) (1, ζ) ≤ Q (1, η) (1, η)` | SP L9 (`‖h'‖ ≤ ‖∂_x∇_y f‖/δ`); L15's Schur complement | No inverse is formed. `δ‖η‖² ≤ −Q(0, η)(0, η) = Q(1, 0)(0, η)` gives L9, and completing the square gives the maximum. | +| `ridge_second_identity` | the ridge equation near `x`, `h' ` at `x`, `D2f` at `(x, h x)` ⇒ `D2f (1, h') ∘ inr = 0` | SP L11 (first identity `∂_x∇_y f + D_y²f h' = 0`) | The derivative of a function that vanishes near `x`. | +| `transverse_hessian_eq` | `H` the `y`-derivative of `∂_y f`, `D2f` the derivative of `Df` ⇒ `H v w = D2f (0, v) (0, w)` | — | Uniqueness of derivatives; ties v1.8's `H` to `D2f`. | +| `trilinear_lower`, `l12_lower` | the combined block bound ⇒ `T (1, b) (1, b) (1, a) ≥ f_xxx − m((1 + ‖b‖)²(1 + ‖a‖) − 1)`; with `f_xxx ≥ 7/4`, `‖a‖, ‖b‖ ≤ u` and `l12_constants` ⇒ `≥ 1/4` | SP L12 (each correction term `≤ m‖h'‖^j`, adverse part `≤ m u (3 + 3u + u²)`) | The combined bound `|T(v₁, v₂, v₃) − s₁s₂s₃ f_xxx| ≤ m(∏(|sᵢ| + ‖yᵢ‖) − ∏|sᵢ|)` is equivalent to SP's seven blocks `f_xxy, f_xyy, f_yyy` (in each slot order) having norm `≤ m`, by multilinear expansion. | +| `l12_constants`, `l9_arith` | `m ≥ 2`, `δ > rm(8m − 5)`, `s = mr/δ`, `u = 2s + 2s²` ⇒ `7/4 − m((1 + u)³ − 1) ≥ 1/4`; and `δ‖h'‖ ≤ 2mr + m‖h‖`, `δ‖h‖ ≤ 2mr²` ⇒ `‖h'‖ ≤ u` | SP L9 (`u = 2/k + 2/k²`), L10 (`mu ≤ 48/121`), L12 (`2554128/1771561`) | `s < 1/(8m − 5) ≤ 1/11` plays SP's `1/k`; `ms ≤ 2/11`, `u ≤ 24/121`, `mu ≤ 48/121`, and `(48/121)(3 + 72/121 + 576/14641) < 3/2`. | +| `dx_grad_increment` | along `s ↦ (x, s y)`, `|T (1, 0) (0, v) (0, y)| ≤ m‖v‖‖y‖` ⇒ `‖∂_x∇_y f(x, y) − ∂_x∇_y f(x, 0)‖ ≤ m‖y‖` | SP L9 ("`‖∂_x∇_y f(x, h)‖ ≤ ‖w'(x)‖ + m‖h‖`, L3 in `y`") | Scalar mean value inequality per direction `v`. | +| `ridge_hconv` | on the ridge over `[−2r, 2r]`: `D2f` symmetric with `δ`-negative transverse part, `‖h'‖ ≤ u`, `s ↦ D²f(s, h s)[(1, b), (1, b)]` with derivative `≥ 1/4` for `‖b‖ ≤ u`, the ridge equation on an open `U ⊇ [−2r, 2r]` ⇒ `ConvexOn [−2r, 2r] (F − (x + r/2)(x − r/2)/8)`, `F x = Df (x, h x) (1, 0)` | SP L11 (CAP (11)), L12, and `hconv` itself | SP computes `F''` from the second ridge identity, which needs `h ∈ C²`. Lean shows instead that `F' − x/4` is monotone: `F'(x₂) − F'(x₁) ≥ D²f(x₂)[(1, η), (1, η)] − D²f(x₁)[(1, η), (1, η)]` (`schur_max`, `η = h'(x₁)`), and the mean value inequality bounds the right side using `T[(1, η), (1, η), (1, h'(s))]` with `η = h'(x₁)` frozen. This is a mixed form, not CAP (11)'s `T[v, v, v]` with `v = (1, h')`; the two agree at `s = x₁`. SP's CAP (12) block estimate bounds both by the same constant, `f_xxx − m((1 + u)³ − 1)` (`trilinear_lower`, `l12_lower`). | +| `ridge_source_facts`, `ridge_capHyp_C3` | `ridge_capHyp_source`'s hypotheses, plus on the collar: `D2f` (derivative of `Df`), `T3 p a b` (derivative of `p ↦ D2f p a b`), the combined block bound `m`; and `f_xxx ≥ 7/4` on `D = [−2r, 2r] × B̄(0, 2r)` ⇒ `ridge_capHyp_source`'s conclusion without `hconv` | SP §2, (H1), L1–L12, L16–L20; L4's `f_xxx ≥ 7/4` as input, on SP's domain `D` | `f_xxx ≥ 7/4` is required only on `D`, where SP's L4 proves it (Codex 4175121617): the proof uses it at the ridge points over `[−2r, 2r]`. `ridge_source_facts` packages v1.8's ridge facts (split for the kernel's heartbeat budget). The second-derivative symmetry comes from Mathlib (`second_derivative_symmetric_of_eventually`). The third derivatives are taken as derivatives of the scalar maps `p ↦ D²f p [a, b]`, which is weaker than differentiability of `D2f` as an operator-valued map. | | `sp_curved_side_constants` | `r > 0`, `m ≥ 2`, `δ > r m (8m - 5)`, `0 ≤ ω ≤ 2 m r²` ⇒ `ω ≤ 2rδ` and `2δ · r³/6 < (2rδ - ω)²` | SP L2 (`m ≥ 2`), L4 (`δ > rmk`, `k = 8m - 5`), L5 (`‖w‖ ≤ (15/8) m r² < 2 m r²`), L18 (`4400r³/121 > r³/6`) | So SP's own constants meet `hωr` and `hcurv` at SP's gap `b - s = r³/6`. | | `CapHyp.congr` | from `g = f` on `closure C` and along one ridge `γ₀`, `CapHyp g C M z b s` | the audit's exterior-invariance corollary (Math-#193 deliverable 2) | `closure C ⊇ C ∪ frontier C`. In SP, `C` is closed. | @@ -111,7 +120,7 @@ Each necessity theorem is one conjunction, so it certifies its own premises, not The ridge toy has `δ = 2`, below SP's `δ > rm(8m − 5) = 22`. So `spToyF (x, y) = x³/3 − x/4 − 12y²` is added: there `m = 2` (`f_xxx = 2`), `δ = 24`, `w = 0` and the gap is exactly `r³/6`. `spToy_capHyp` shows that every hypothesis of `ridge_capHyp_sp` holds there, so SP's normalized hypotheses are jointly satisfiable. `spToy_normalized` does the same for `ridge_capHyp_normalized`, with `G0 = x² − 1/4`, `|G0''| = 2 = m` and gap exactly `1/6`. -`spToyF` has `λ = 24 < 8rm² = 32`, so it does not meet (H1). `h1ToyF (x, y) = x³/3 − x/4 − 20y²` (v1.6) has a constant transverse Hessian `−40`, so `λ = 40 > 32`, its Hessian increments vanish and the gap is exactly `1/6`. `h1Toy_capHyp` shows that every hypothesis of `ridge_capHyp_H1` holds there. `h1Toy_ridge_differentiable` (v1.7) states every hypothesis of `ridge_differentiable` at `h1ToyF`, with `h = 0`, transverse gradient `−40y`, its derivative `−40 · snd`, `δ = 40` and `U = (−3, 3)`, as conjuncts of its proposition, and derives that theorem's conclusion from them. `h1Toy_source` (v1.8) meets every hypothesis of `ridge_capHyp_source` on the collar `ε = 1/2`, with joint derivative `(x² − 1/4, −40y)`, transverse derivative `−40 · snd` and `H = −40`, and the theorem then yields its ridge and, for `h = 0` (`F = x² − 1/4` meets L12), its cap at `M = (−1/2, 0)`. +`spToyF` has `λ = 24 < 8rm² = 32`, so it does not meet (H1). `h1ToyF (x, y) = x³/3 − x/4 − 20y²` (v1.6) has a constant transverse Hessian `−40`, so `λ = 40 > 32`, its Hessian increments vanish and the gap is exactly `1/6`. `h1Toy_capHyp` shows that every hypothesis of `ridge_capHyp_H1` holds there. `h1Toy_ridge_differentiable` (v1.7) states every hypothesis of `ridge_differentiable` at `h1ToyF`, with `h = 0`, transverse gradient `−40y`, its derivative `−40 · snd`, `δ = 40` and `U = (−3, 3)`, as conjuncts of its proposition, and derives that theorem's conclusion from them. `h1Toy_source` (v1.8) meets every hypothesis of `ridge_capHyp_source` on the collar `ε = 1/2`, with joint derivative `(x² − 1/4, −40y)`, transverse derivative `−40 · snd` and `H = −40`, and the theorem then yields its ridge and, for `h = 0` (`F = x² − 1/4` meets L12), its cap at `M = (−1/2, 0)`. `h1Toy_C3` (v1.9) meets every hypothesis of `ridge_capHyp_C3`, with `D²f = diag(2x, −40)` and third derivatives `T a b = 2a₁b₁ · fst` (only `f_xxx = 2 ≥ 7/4` is nonzero), and the theorem yields its ridge and cap with no `hconv` supplied. The toy lives on `ℝ`, which is not compact. So the older-peak theorems (`older_peak`, `elder_death_level_peak`) have no concrete instance exhibited in Lean. Their extra hypotheses (compact, locally connected, continuous `f`) hold on the @@ -126,7 +135,7 @@ illustrates the hypotheses; it is not a model of the planar cap. |---|---|---|---| | I1 | Coordinates: SP's cap is `[-2r, r/2] × B̄(0, 2r)` in a frame `φ` of the periodic lift, and SP's "boundary" is the topological frontier. The transport to the torus (`CapHyp.toTorus`) and the face list (`frontier_cylinder`) are proved; the transport needs no embedding radius | SP §2 | Only the identification of SP's objects with these Lean objects remains. | | I2 | Persistence bookkeeping: in H0 superlevel persistence with distinct critical values, the class born at a local maximum `M` dies at the largest level at which its component contains a strictly higher local maximum (the elder rule) | SP L22, P §8 | This is the definition of the elder pairing. On a compact, locally connected space, Lean proves that this level is `s` (`elder_death_level_peak`). Only the identification of the persistence module's pairing with that definition is informal. | -| I3 | The analytic steps that produce the inputs of `ridge_capHyp_H1` from `G_r`: (H1) `λ > 8rm²`; the slice derivatives and Hessians on the cap, with the third-derivative blocks `∂_x D_y² f` (along `y = 0`) and `D_y³ f` (along rays) bounded by `m`. These bounds are L3's input; L3's increment step itself is proved (`hessian_increment`); `m` as a bound on the third derivatives, which gives the convexity pairs for `G0 = ∂_x f(·, 0)` (L1's input `|g_0'''| ≤ m`) and for `w` (L5's input `‖w''‖ ≤ m`); the critical pins `G0(∓r/2) = 0` and `h(∓r/2) = 0`; L6 (the `w'` bound); for L7, the strict differentiability of the transverse gradient along the ridge (from `f ∈ C²` near `D`), the identification of `G` with the slice gradient on a neighbourhood of each ridge point `(x, h x)`, `x ∈ [−2r, 2r]` (`hG`); the negative definiteness `(DG x ∘ inr) v v ≤ −δ‖v‖²` along the ridge for `x ∈ [−2r, 2r]` (`hneg`), whereas `transverse_hessian_le` gives `H ≤ −(λ − 5rm)` only on the cap (`x ∈ [−2r, r/2]`) and only for the slice Hessians `H`, which no declaration identifies with `DG x ∘ inr` (since v1.8, `ridge_capHyp_source` derives `hG` from the joint derivative on an open neighbourhood, and `hneg` from `transverse_hessian_le_D` on the collar with `DG ∘ inr = H` along the ridge; `hGs` stays a source-data hypothesis on the collar); with existence and regularity of `h` themselves proved since v1.7; the source data of `ridge_capHyp_source` on the collar `[−2r − ε, 2r + ε] × B̄(0, 2r)`: the derivatives `Df`, `DG`, `H` and the bounds `m` there. SP has `f ∈ C⁴` near `D` and bounds the third derivatives on `D`; on a thin enough collar a bound `m + η` holds by continuity and (H1) stays strict for small `η`. Lean does not prove this step; and L9–L12 (`‖h'‖` and the `F''` bound giving `hconv`) | SP §2 (H1), L6, L7, L9–L12; CAP §§2–5 | These are checked with exact constants by SP's script, not in Lean. Since v1.8 the extension of L4 to the collar and the composition of the L7 lemmas with the cap are proved. Since v1.8, Lean composes L1–L5, L7, L8 and L11 with the cap from the source data on a collar (`ridge_capHyp_source`). Since v1.7, Lean proves L7's existence and regularity of `h`. Since v1.6, Lean proves L3–L4 (from (H1) and the increment bound). Since v1.5, Lean proves L1, L2, L5, L7's maximum and uniqueness, L8, L11's chain rule and L18 from those outputs, and checks SP's constants in the curvature step. L13, L16, L17, L19 and L20 were already proved in v1.4. | +| I3 | The analytic steps that produce the inputs of `ridge_capHyp_H1` from `G_r`: (H1) `λ > 8rm²`; the slice derivatives and Hessians on the cap, with the third-derivative blocks `∂_x D_y² f` (along `y = 0`) and `D_y³ f` (along rays) bounded by `m`. These bounds are L3's input; L3's increment step itself is proved (`hessian_increment`); `m` as a bound on the third derivatives, which gives the convexity pairs for `G0 = ∂_x f(·, 0)` (L1's input `|g_0'''| ≤ m`) and for `w` (L5's input `‖w''‖ ≤ m`); the critical pins `G0(∓r/2) = 0` and `h(∓r/2) = 0`; L6 (the `w'` bound; proved since v1.9); for L7, the strict differentiability of the transverse gradient along the ridge (from `f ∈ C²` near `D`), the identification of `G` with the slice gradient on a neighbourhood of each ridge point `(x, h x)`, `x ∈ [−2r, 2r]` (`hG`); the negative definiteness `(DG x ∘ inr) v v ≤ −δ‖v‖²` along the ridge for `x ∈ [−2r, 2r]` (`hneg`), whereas `transverse_hessian_le` gives `H ≤ −(λ − 5rm)` only on the cap (`x ∈ [−2r, r/2]`) and only for the slice Hessians `H`, which no declaration identifies with `DG x ∘ inr` (since v1.8, `ridge_capHyp_source` derives `hG` from the joint derivative on an open neighbourhood, and `hneg` from `transverse_hessian_le_D` on the collar with `DG ∘ inr = H` along the ridge; `hGs` stays a source-data hypothesis on the collar); with existence and regularity of `h` themselves proved since v1.7; the source data of `ridge_capHyp_source` on the collar `[−2r − ε, 2r + ε] × B̄(0, 2r)`: the derivatives `Df`, `DG`, `H` and the bounds `m` there. SP has `f ∈ C⁴` near `D` and bounds the third derivatives on `D`; on a thin enough collar a bound `m + η` holds by continuity and (H1) stays strict for small `η`. Lean does not prove this step. Of SP's steps L1–L12, only L4's `f_xxx ≥ 7/4` on `D` (from L2's second statement and (H2)) remains an input. The source data listed in this row stay hypotheses on the collar: the block bound `m`; the convexity pair for `G0`, which also carries the upper bound `|f_xxx| ≤ m` along the pin interval, since `ridge_capHyp_C3`'s block bound `hT` excludes `f_xxx`; the convexity pair for `w`; the L3 bounds `Hx`, `Hr`; (H1); the pins; and `DG`. | SP §2 (H1), L6, L7, L9–L12; CAP §§2–5 | These are checked with exact constants by SP's script. Since v1.9, Lean proves L6, L9 and L12 with SP's constants and derives `hconv` (`ridge_capHyp_C3`); `f_xxx ≥ 7/4` stays an input. Since v1.8 the extension of L4 to the collar and the composition of the L7 lemmas with the cap are proved. Since v1.8, Lean composes L1–L5, L7, L8 and L11 with the cap from the source data on a collar (`ridge_capHyp_source`). Since v1.7, Lean proves L7's existence and regularity of `h`. Since v1.6, Lean proves L3–L4 (from (H1) and the increment bound). Since v1.5, Lean proves L1, L2, L5, L7's maximum and uniqueness, L8, L11's chain rule and L18 from those outputs, and checks SP's constants in the curvature step. L13, L16, L17, L19 and L20 were already proved in v1.4. | | I4 | Theorem A, measurability, `Q^W(G_r^c) ≤ C r³` | P §§7–8, C1, G1 | probability | ## 5. Review contract @@ -143,5 +152,5 @@ row of §4, it says whether the interface is stated correctly. A changed Lean source, toolchain or pin makes an earlier review stale. -v1.5 is additive: it inserts the sections `Slice` and the slice-route toy, and updates the file's header comment. The 53 v1.4 declarations and their statements are unchanged, as the diff against v1.4 shows. The v1.4 alignment review ([5396110365](https://github.com/d6g8k5htny-coder/Math-/pull/246#pullrequestreview-5396110365), `ALIGNED_SCOPED`) therefore still covers the v1.4 rows once a reviewer confirms by diff that they are unchanged. A delta review assesses the new rows: the fourteen slice rows of §2, the v1.5 toy paragraphs of §3 and the revised I3. v1.6 adds five further §2 rows (`strongConcaveOn_of_hessian` to `ridge_capHyp_H1`), the `h1ToyF` paragraph of §3 and a further revision of I3; its 74 v1.5 declarations are unchanged. v1.7 adds six §2 rows (`slice_critical_unique` to `ridge_exists`), the `h1Toy_ridge_differentiable` sentence of §3 and a further revision of I3; its 81 v1.6 declarations are unchanged. v1.8 adds four §2 rows (`hessian_increment_D` to `ridge_capHyp_source`), the `h1Toy_source` sentence of §3 and a further revision of I3; its 88 v1.7 declarations are unchanged. A same-provider read, including any Claude +v1.5 is additive: it inserts the sections `Slice` and the slice-route toy, and updates the file's header comment. The 53 v1.4 declarations and their statements are unchanged, as the diff against v1.4 shows. The v1.4 alignment review ([5396110365](https://github.com/d6g8k5htny-coder/Math-/pull/246#pullrequestreview-5396110365), `ALIGNED_SCOPED`) therefore still covers the v1.4 rows once a reviewer confirms by diff that they are unchanged. A delta review assesses the new rows: the fourteen slice rows of §2, the v1.5 toy paragraphs of §3 and the revised I3. v1.6 adds five further §2 rows (`strongConcaveOn_of_hessian` to `ridge_capHyp_H1`), the `h1ToyF` paragraph of §3 and a further revision of I3; its 74 v1.5 declarations are unchanged. v1.7 adds six §2 rows (`slice_critical_unique` to `ridge_exists`), the `h1Toy_ridge_differentiable` sentence of §3 and a further revision of I3; its 81 v1.6 declarations are unchanged. v1.8 adds four §2 rows (`hessian_increment_D` to `ridge_capHyp_source`), the `h1Toy_source` sentence of §3 and a further revision of I3; its 88 v1.7 declarations are unchanged. v1.9 adds nine §2 rows (`convex_deriv_sign` to `ridge_capHyp_C3`, fourteen theorems), the `h1Toy_C3` sentence of §3 and a further revision of the SP row and I3; its 93 v1.8 declarations are unchanged. A same-provider read, including any Claude read, gives zero independence credit. A build or merge is not an alignment review. diff --git a/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean b/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean index 35f1e1255..1827ca31e 100644 --- a/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean +++ b/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean @@ -16,12 +16,14 @@ is one instance. Only the older-peak theorems add compactness, local connectedness and continuity of `f`, all of which hold on the torus. - What this file does NOT formalize: the analytic steps L6 and L9–L12 (the `w'` bound and the - quantitative `‖h'‖` and `F''` bounds; they enter `ridge_capHyp_H1` as `hconv`). L1–L5, L7 (existence, + Up to v1.8 the analytic steps L6 and L9–L12 (the `w'` bound and the quantitative `‖h'‖` and `F''` + bounds) entered `ridge_capHyp_H1` as `hconv`. L1–L5, L7 (existence, uniqueness and implicit-function regularity of the ridge `h`: `ridge_exists`, `ridge_differentiable`), L8, L11's chain rule, L13 and L16–L20 are proved, and since v1.8 `ridge_capHyp_source` composes them from source data on a collar `[-2r - ε, 2r + ε]` of `D` - (the source data themselves are hypotheses). Also not formalized: the + (the source data themselves are hypotheses). Since v1.9, L6 and L9–L12 are proved too, and + `ridge_capHyp_C3` derives `hconv`; SP's `f_xxx ≥ 7/4` (L4, from L2 and (H2)) stays an input. + Also not formalized: the identification of the H0 persistence pairing with the elder rule (L22, P §8); the unstable-branch analysis (L23); and every probabilistic statement. -/ @@ -1714,6 +1716,689 @@ theorem ridge_capHyp_source [FiniteDimensional ℝ E] {f : ℝ × E → ℝ} rw [hha, hhc] at key exact ⟨hha, hhc, key⟩ + +/-! ### L6, L9 and L12 (v1.9) + +The last analytic input of the cap, L12's convexity `hconv`, is derived here. L6 bounds `w'` by +chord slopes of L5's convexity pair (no integral), L9 bounds `h'` through the differentiated ridge +equation, and L12 uses that `F' = D²f[(1, h'), (1, 0)]` is the maximum of `ζ ↦ D²f[(1, ζ), (1, ζ)]`, +so that no second derivative of `h` is needed. `ridge_capHyp_C3` composes them with +`ridge_capHyp_source`. -/ + +/-- A convex function with equal values at `a < c` has derivative `≥ 0` to the right of `c` and +`≤ 0` to the left of `a`. -/ +theorem convex_deriv_sign {φ : ℝ → ℝ} {D : Set ℝ} {a c x d : ℝ} (hφ : ConvexOn ℝ D φ) + (haD : a ∈ D) (hcD : c ∈ D) (hac : a < c) (heq : φ a = φ c) (hx : x ∈ D) + (hd : HasDerivAt φ d x) : (c ≤ x → 0 ≤ d) ∧ (x ≤ a → d ≤ 0) := by + have h0 : (φ c - φ a) / (c - a) = 0 := by rw [heq, sub_self, zero_div] + constructor + · intro hcx + have hax : a < x := hac.trans_le hcx + have h1 : (φ c - φ a) / (c - a) ≤ (φ x - φ a) / (x - a) := + hφ.secant_mono haD hcD hx hac.ne' hax.ne' hcx + have h2 := hφ.slope_le_of_hasDerivAt haD hx hax hd + rw [slope_def_field] at h2 + linarith + · intro hxa + rcases hxa.eq_or_lt with h | h + · subst h + have h2 := hφ.le_slope_of_hasDerivAt hx hcD hac hd + rw [slope_def_field] at h2 + linarith + · have h1 : (φ a - φ x) / (a - x) ≤ (φ c - φ a) / (c - a) := + hφ.slope_mono_adjacent hx hcD h hac + have h2 := hφ.le_slope_of_hasDerivAt hx haD h hd + rw [slope_def_field] at h2 + linarith + +/-- **L6 (scalar).** If `u + (m/2)t²` is convex and `u - (m/2)t²` concave on `D` (weakly +`|u''| ≤ m`), `u(∓r/2) = 0` and `u` has derivative `d` at `x ∈ D`, then `|d| ≤ m · max(|x|, r/2)`. +Outside the pins the chord through them has slope `0`; between them the chord to the nearer pin and +L5's bound on `u(x)` give `mr/2`. -/ +theorem two_node_deriv_bound {u : ℝ → ℝ} {D : Set ℝ} {r m x d : ℝ} (hr : 0 < r) (hm : 0 ≤ m) + (hcv : ConvexOn ℝ D (fun t => u t + m / 2 * t ^ 2)) + (hcc : ConcaveOn ℝ D (fun t => u t - m / 2 * t ^ 2)) + (haD : -r / 2 ∈ D) (hcD : r / 2 ∈ D) (ha : u (-r / 2) = 0) (hc : u (r / 2) = 0) + (hx : x ∈ D) (hd : HasDerivAt u d x) : |d| ≤ m * max |x| (r / 2) := by + have hac : -r / 2 < r / 2 := by linarith + have hq : HasDerivAt (fun t : ℝ => m / 2 * t ^ 2) (m * x) x := by + convert (hasDerivAt_pow 2 x).const_mul (m / 2) using 1 + push_cast + ring + have hg : HasDerivAt (fun t => u t + m / 2 * t ^ 2) (d + m * x) x := hd.add hq + have hcv' : ConvexOn ℝ D (fun t => -u t + m / 2 * t ^ 2) := + hcc.neg.congr fun t _ => by simp only [Pi.neg_apply]; ring + have hk : HasDerivAt (fun t => -u t + m / 2 * t ^ 2) (-d + m * x) x := hd.neg.add hq + have hgeq : (fun t => u t + m / 2 * t ^ 2) (-r / 2) = (fun t => u t + m / 2 * t ^ 2) (r / 2) := by + simp only [ha, hc]; ring + have hkeq : (fun t => -u t + m / 2 * t ^ 2) (-r / 2) = + (fun t => -u t + m / 2 * t ^ 2) (r / 2) := by + simp only [ha, hc]; ring + obtain ⟨g1, g2⟩ := convex_deriv_sign hcv haD hcD hac hgeq hx hg + obtain ⟨k1, k2⟩ := convex_deriv_sign hcv' haD hcD hac hkeq hx hk + rcases le_or_gt (r / 2) x with hcx | hxc + · have h1 := g1 hcx + have h2 := k1 hcx + have hxpos : 0 ≤ x := by linarith + rw [abs_of_nonneg hxpos] + calc |d| ≤ m * x := abs_le.mpr ⟨by linarith, by linarith⟩ + _ ≤ m * max x (r / 2) := mul_le_mul_of_nonneg_left (le_max_left _ _) hm + rcases le_or_gt x (-r / 2) with hxa | hax + · have h1 := g2 hxa + have h2 := k2 hxa + have hxneg : x ≤ 0 := by linarith + rw [abs_of_nonpos hxneg] + calc |d| ≤ m * -x := abs_le.mpr ⟨by linarith, by linarith⟩ + _ ≤ m * max (-x) (r / 2) := mul_le_mul_of_nonneg_left (le_max_left _ _) hm + · -- between the pins + have hu := two_node_bound hcv hcc haD hcD hac ha hc hx + have hP : (x - -r / 2) * (x - r / 2) ≤ 0 := + mul_nonpos_of_nonneg_of_nonpos (by linarith) (by linarith) + rw [abs_of_nonpos hP] at hu + have hcx : 0 < r / 2 - x := by linarith + have hs1 := hcv.le_slope_of_hasDerivAt hx hcD hxc hg + have hs2 := hcv'.le_slope_of_hasDerivAt hx hcD hxc hk + rw [slope_def_field, le_div_iff₀ hcx] at hs1 hs2 + simp only [hc] at hs1 hs2 + have hu1 := (abs_le.mp hu).1 + have hu2 := (abs_le.mp hu).2 + have key1 : d * (r / 2 - x) ≤ m / 2 * r * (r / 2 - x) := by nlinarith + have key2 : -d * (r / 2 - x) ≤ m / 2 * r * (r / 2 - x) := by nlinarith + have hd1 := le_of_mul_le_mul_right key1 hcx + have hd2 := le_of_mul_le_mul_right key2 hcx + calc |d| ≤ m / 2 * r := abs_le.mpr ⟨by linarith, hd1⟩ + _ = m * (r / 2) := by ring + _ ≤ m * max |x| (r / 2) := mul_le_mul_of_nonneg_left (le_max_right _ _) hm + + +/-- **L6 (CAP (7)).** For the slice derivatives `w t` at `y = 0` with derivative `w' x` at `x`, under +L5's hypotheses: `‖w' x‖ ≤ m · max(|x|, r/2)`; on `[-2r, 2r]` this is SP's `‖w'‖ ≤ 2mr`. -/ +theorem slice_gradient_deriv_bound {w : ℝ → E →L[ℝ] ℝ} {w' : E →L[ℝ] ℝ} {D : Set ℝ} {r m x : ℝ} + (hr : 0 < r) (hm : 0 ≤ m) + (hcv : ∀ v : E, ConvexOn ℝ D (fun t => w t v + m * ‖v‖ / 2 * t ^ 2)) + (hcc : ∀ v : E, ConcaveOn ℝ D (fun t => w t v - m * ‖v‖ / 2 * t ^ 2)) + (haD : -r / 2 ∈ D) (hcD : r / 2 ∈ D) (ha : w (-r / 2) = 0) (hc : w (r / 2) = 0) + (hx : x ∈ D) (hd : HasDerivAt w w' x) : ‖w'‖ ≤ m * max |x| (r / 2) := by + refine ContinuousLinearMap.opNorm_le_bound _ (by positivity) fun v => ?_ + have hdv : HasDerivAt (fun t => w t v) (w' v) x := by + simpa using hd.clm_apply (hasDerivAt_const x v) + have h := two_node_deriv_bound (u := fun t => w t v) (m := m * ‖v‖) hr (by positivity) (hcv v) + (hcc v) haD hcD (by simp [ha]) (by simp [hc]) hx hdv + rw [Real.norm_eq_abs] + calc |w' v| ≤ m * ‖v‖ * max |x| (r / 2) := h + _ = m * max |x| (r / 2) * ‖v‖ := by ring + +/-- **L9 and the Schur maximum.** Let `Q` be a bilinear form on `ℝ × E` with `δ`-negative definite +transverse part, and let `η` satisfy the differentiated ridge equation `Q (1, η) (0, ·) = 0`. Then +`δ ‖η‖ ≤ ‖Q (1, 0) (0, ·)‖` (L9: `‖h'‖ ≤ ‖∂_x ∇_y f‖ / δ`), `Q (1, η) (1, η) = Q (1, η) (1, 0)`, and, +if `Q` is symmetric, `Q (1, ζ) (1, ζ) ≤ Q (1, η) (1, η)` for every `ζ`: the Schur complement +`F' = f_xx + f_xy[h']` is the maximum of `ζ ↦ D²f[(1, ζ), (1, ζ)]`. -/ +theorem schur_max {Q : ℝ × E →L[ℝ] ℝ × E →L[ℝ] ℝ} {δ : ℝ} {η : E} (hδ : 0 < δ) + (hneg : ∀ v : E, Q (0, v) (0, v) ≤ -δ * ‖v‖ ^ 2) + (hridge : (Q (1, η)).comp (ContinuousLinearMap.inr ℝ ℝ E) = 0) : + δ * ‖η‖ ≤ ‖(Q (1, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)‖ ∧ + Q (1, η) (1, η) = Q (1, η) (1, 0) ∧ + ((∀ v w, Q v w = Q w v) → ∀ ζ : E, Q (1, ζ) (1, ζ) ≤ Q (1, η) (1, η)) := by + have h0 : ∀ v : E, Q (1, η) (0, v) = 0 := fun v => by + simpa using congrArg (fun L : E →L[ℝ] ℝ => L v) hridge + have hsplit : ∀ ζ : E, ((1 : ℝ), ζ) = ((1 : ℝ), (0 : E)) + ((0 : ℝ), ζ) := fun ζ => by simp + refine ⟨?_, ?_, ?_⟩ + · have h1 : Q (1, 0) (0, η) + Q (0, η) (0, η) = 0 := by + have := h0 η + rw [hsplit η, map_add, add_apply] at this + exact this + have h2 : Q (1, 0) (0, η) ≤ ‖(Q (1, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)‖ * ‖η‖ := by + have := ((Q (1, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)).le_opNorm η + have h3 : ((Q (1, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)) η = Q (1, 0) (0, η) := by simp + rw [h3] at this + exact (le_abs_self _).trans (by simpa [Real.norm_eq_abs] using this) + have h4 := hneg η + have h5 : δ * ‖η‖ * ‖η‖ ≤ ‖(Q (1, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)‖ * ‖η‖ := by + nlinarith + rcases (norm_nonneg η).eq_or_lt with h | h + · rw [← h, mul_zero]; exact norm_nonneg _ + · exact le_of_mul_le_mul_right h5 h + · have e : Q (1, η) (1, η) = Q (1, η) ((1, 0) + (0, η)) := by rw [← hsplit η] + rw [e, map_add, h0 η, add_zero] + · intro hsym ζ + have hz : ((1 : ℝ), ζ) = ((1 : ℝ), η) + ((0 : ℝ), ζ - η) := by simp + have h1 := h0 (ζ - η) + have h2 : Q (0, ζ - η) (1, η) = 0 := by rw [hsym]; exact h1 + have h3 := hneg (ζ - η) + rw [hz, map_add, map_add, add_apply, add_apply, h1, h2] + nlinarith [sq_nonneg ‖ζ - η‖] + +/-- **The correction terms of L12.** Let `T a b v` be the third derivative of `f` (the derivative of +`D²f[a, b]` in direction `v`). If every block other than `f_xxx` has norm at most `m`, in the combined +form below, then `T (1, b) (1, b) (1, a) ≥ f_xxx - m((1 + ‖b‖)²(1 + ‖a‖) - 1)`. With `‖a‖, ‖b‖ ≤ u` +this is SP's adverse bound `m u (3 + 3u + u²)`. -/ +theorem trilinear_lower {T : ℝ × E → ℝ × E → ℝ × E →L[ℝ] ℝ} {m : ℝ} + (hT : ∀ (s₁ s₂ s₃ : ℝ) (y₁ y₂ y₃ : E), + |T (s₁, y₁) (s₂, y₂) (s₃, y₃) - s₁ * s₂ * s₃ * T (1, 0) (1, 0) (1, 0)| ≤ + m * ((|s₁| + ‖y₁‖) * (|s₂| + ‖y₂‖) * (|s₃| + ‖y₃‖) - |s₁| * |s₂| * |s₃|)) + (a b : E) : + T (1, 0) (1, 0) (1, 0) - m * ((1 + ‖b‖) * (1 + ‖b‖) * (1 + ‖a‖) - 1) ≤ T (1, b) (1, b) (1, a) := by + have h := (abs_le.mp (hT 1 1 1 b b a)).1 + simp only [abs_one, one_mul, mul_one] at h + linarith + +/-- **SP's constants close L12.** With `m ≥ 2`, `δ > rm(8m - 5)` and `u = 2s + 2s²`, `s = mr/δ` +(L9's bound on `‖h'‖`): `7/4 - m((1 + u)³ - 1) ≥ 1/4`. SP's exact value at `k = 11` is +`7/4 - 2554128/1771561 = 0.308… > 1/4`. -/ +theorem l12_constants {r m δ : ℝ} (hr : 0 < r) (hm : 2 ≤ m) (hδ : r * m * (8 * m - 5) < δ) : + 1 / 4 ≤ 7 / 4 - m * ((1 + (2 * (m * r / δ) + 2 * (m * r / δ) ^ 2)) ^ 3 - 1) := by + have hrm : 0 < r * m := mul_pos hr (by linarith) + have h11 : 11 * (r * m) ≤ r * m * (8 * m - 5) := by nlinarith + have hδ0 : 0 < δ := by linarith + set s := m * r / δ with hs + have hs0 : 0 ≤ s := by positivity + have hs1 : s ≤ 1 / 11 := by + rw [hs, div_le_iff₀ hδ0]; nlinarith + have hms : m * s ≤ 2 / 11 := by + have : m * s = m * m * r / δ := by rw [hs]; ring + rw [this, div_le_iff₀ hδ0] + nlinarith [mul_nonneg (mul_nonneg hr.le (by linarith : (0 : ℝ) ≤ m)) (by linarith : (0 : ℝ) ≤ m - 2)] + set u := 2 * s + 2 * s ^ 2 with hu + have hu0 : 0 ≤ u := by positivity + have hu1 : u ≤ 24 / 121 := by rw [hu]; nlinarith + have hmu : m * u ≤ 48 / 121 := by + have : m * u = 2 * (m * s) * (1 + s) := by rw [hu]; ring + rw [this] + have h1 : 1 + s ≤ 12 / 11 := by linarith + have h2 : 0 ≤ m * s := by positivity + nlinarith + have hexp : m * ((1 + u) ^ 3 - 1) = (m * u) * (3 + 3 * u + u ^ 2) := by ring + rw [hexp] + have h3 : 3 + 3 * u + u ^ 2 ≤ 3 + 3 * (24 / 121) + (24 / 121) ^ 2 := by nlinarith + have h4 : (m * u) * (3 + 3 * u + u ^ 2) ≤ (48 / 121) * (3 + 3 * (24 / 121) + (24 / 121) ^ 2) := + mul_le_mul hmu h3 (by positivity) (by norm_num) + norm_num at h4 ⊢ + linarith + +/-- **The transverse Hessian is the transverse block of `D²f`.** If `y ↦ ∂_y f (x, y)` has +derivative `H` at `y₀` and `Df` has derivative `D2f` at `(x, y₀)`, then +`H v w = D²f (x, y₀) [(0, v), (0, w)]`. -/ +theorem transverse_hessian_eq {Df : ℝ × E → ℝ × E →L[ℝ] ℝ} {D2f : ℝ × E →L[ℝ] ℝ × E →L[ℝ] ℝ} + {H : E →L[ℝ] E →L[ℝ] ℝ} {x : ℝ} {y₀ : E} + (hH : HasFDerivAt (fun y => (Df (x, y)).comp (ContinuousLinearMap.inr ℝ ℝ E)) H y₀) + (hD2 : HasFDerivAt Df D2f (x, y₀)) (v w : E) : H v w = D2f (0, v) (0, w) := by + have h1 := hH.clm_apply (hasFDerivAt_const w y₀) + have h2 := (hD2.comp y₀ (hasFDerivAt_prodMk_right x y₀)).clm_apply + (hasFDerivAt_const ((0 : ℝ), w) y₀) + have h3 := h1.unique h2 + have := congrArg (fun L : E →L[ℝ] ℝ => L v) h3 + simpa using this + +/-- **The differentiated ridge equation.** If `∂_y f (t, h t) = 0` for `t` near `x`, `h` has +derivative `h'` at `x` and `Df` has derivative `D2f` at `(x, h x)`, then +`D²f (x, h x) [(1, h'), (0, ·)] = 0`, i.e. `∂_x ∇_y f + D_y² f · h' = 0` (L11's first identity). -/ +theorem ridge_second_identity {Df : ℝ × E → ℝ × E →L[ℝ] ℝ} + {D2f : ℝ × E →L[ℝ] ℝ × E →L[ℝ] ℝ} {h : ℝ → E} {h' : E} {x : ℝ} + (hridge : ∀ᶠ t in 𝓝 x, (Df (t, h t)).comp (ContinuousLinearMap.inr ℝ ℝ E) = 0) + (hh : HasDerivAt h h' x) (hD2 : HasFDerivAt Df D2f (x, h x)) : + (D2f (1, h')).comp (ContinuousLinearMap.inr ℝ ℝ E) = 0 := by + have hp : HasDerivAt (fun t => (t, h t)) ((1 : ℝ), h') x := (hasDerivAt_id x).prodMk hh + have h1 : HasDerivAt (fun t => Df (t, h t)) (D2f (1, h')) x := hD2.comp_hasDerivAt x hp + have h2 : HasDerivAt (fun t => (Df (t, h t)).comp (ContinuousLinearMap.inr ℝ ℝ E)) + ((D2f (1, h')).comp (ContinuousLinearMap.inr ℝ ℝ E)) x := by + have := h1.clm_comp (hasDerivAt_const x (ContinuousLinearMap.inr ℝ ℝ E)) + simpa using this + have h3 : HasDerivAt (fun t => (Df (t, h t)).comp (ContinuousLinearMap.inr ℝ ℝ E)) 0 x := + (hasDerivAt_const x (0 : E →L[ℝ] ℝ)).congr_of_eventuallyEq hridge + exact h2.unique h3 + +/-- **L12 (CAP (11)–(12)): the convexity input `hconv`.** Along the ridge, let `Df`, `D2f` be the +first two derivatives of `f`, with `D2f` symmetric and its transverse part `δ`-negative definite, +`‖h'‖ ≤ u`, and for every `‖b‖ ≤ u` let `s ↦ D²f(s, h s)[(1, b), (1, b)]` have derivative `≥ 1/4` +(SP: `f_xxx ≥ 7/4` minus the adverse part `m u (3 + 3u + u²)`; see `trilinear_lower`). Then +`F - (x + r/2)(x - r/2)/8`, `F x = ∂_x f (x, h x)`, is convex on `[-2r, 2r]`. No second derivative of +`h` is used: `F' = D²f[(1, h'), (1, 0)]` is the maximum of `ζ ↦ D²f[(1, ζ), (1, ζ)]` (`schur_max`), +so `F'(x₂) - F'(x₁) ≥ D²f(x₂)[(1, η), (1, η)] - D²f(x₁)[(1, η), (1, η)] ≥ (x₂ - x₁)/4` with +`η = h'(x₁)`. -/ +theorem ridge_hconv {Df : ℝ × E → ℝ × E →L[ℝ] ℝ} {D2f : ℝ × E → ℝ × E →L[ℝ] ℝ × E →L[ℝ] ℝ} + {Φ : ℝ → E → ℝ} {h h' : ℝ → E} {U : Set ℝ} {r δ u : ℝ} (hδ : 0 < δ) (hU : IsOpen U) + (hIU : Icc (-2 * r) (2 * r) ⊆ U) + (hridge : ∀ x ∈ U, (Df (x, h x)).comp (ContinuousLinearMap.inr ℝ ℝ E) = 0) + (hh : ∀ x ∈ Icc (-2 * r) (2 * r), HasDerivAt h (h' x) x) + (hD2 : ∀ x ∈ Icc (-2 * r) (2 * r), HasFDerivAt Df (D2f (x, h x)) (x, h x)) + (hsym : ∀ x ∈ Icc (-2 * r) (2 * r), ∀ v w, D2f (x, h x) v w = D2f (x, h x) w v) + (hneg : ∀ x ∈ Icc (-2 * r) (2 * r), ∀ v : E, D2f (x, h x) (0, v) (0, v) ≤ -δ * ‖v‖ ^ 2) + (hu : ∀ x ∈ Icc (-2 * r) (2 * r), ‖h' x‖ ≤ u) + (hΦ : ∀ x ∈ Icc (-2 * r) (2 * r), ∀ b : E, + HasDerivAt (fun s => D2f (s, h s) (1, b) (1, b)) (Φ x b) x) + (hΦb : ∀ x ∈ Icc (-2 * r) (2 * r), ∀ b : E, ‖b‖ ≤ u → 1 / 4 ≤ Φ x b) : + ConvexOn ℝ (Icc (-2 * r) (2 * r)) + (fun x => Df (x, h x) (1, 0) - (x + r / 2) * (x - r / 2) / 8) := by + have hid : ∀ x ∈ Icc (-2 * r) (2 * r), + (D2f (x, h x) (1, h' x)).comp (ContinuousLinearMap.inr ℝ ℝ E) = 0 := fun x hx => + ridge_second_identity (Filter.eventually_of_mem (hU.mem_nhds (hIU hx)) hridge) (hh x hx) + (hD2 x hx) + have hF : ∀ x ∈ Icc (-2 * r) (2 * r), + HasDerivAt (fun t => Df (t, h t) (1, 0) - (t + r / 2) * (t - r / 2) / 8) + (D2f (x, h x) (1, h' x) (1, 0) - x / 4) x := by + intro x hx + have hp : HasDerivAt (fun t => (t, h t)) ((1 : ℝ), h' x) x := (hasDerivAt_id x).prodMk (hh x hx) + have h1 : HasDerivAt (fun t => Df (t, h t)) (D2f (x, h x) (1, h' x)) x := + (hD2 x hx).comp_hasDerivAt x hp + have h2 : HasDerivAt (fun t => Df (t, h t) (1, 0)) (D2f (x, h x) (1, h' x) (1, 0)) x := by + simpa using h1.clm_apply (hasDerivAt_const x ((1 : ℝ), (0 : E))) + have h3 : HasDerivAt (fun t : ℝ => (t + r / 2) * (t - r / 2) / 8) (x / 4) x := by + have := ((hasDerivAt_pow 2 x).div_const 8).sub_const (r ^ 2 / 32) + convert this using 1 + · funext t + ring + · push_cast + ring + exact h2.sub h3 + have hmono : MonotoneOn (fun x => D2f (x, h x) (1, h' x) (1, 0) - x / 4) + (Icc (-2 * r) (2 * r)) := by + intro x1 hx1 x2 hx2 hle + have hφ : ∀ t ∈ Icc (-2 * r) (2 * r), + HasDerivAt (fun s => D2f (s, h s) (1, h' x1) (1, h' x1) - s / 4) + (Φ t (h' x1) - 1 / 4) t := fun t ht => + (hΦ t ht (h' x1)).sub ((hasDerivAt_id t).div_const 4) + have hφmono : MonotoneOn (fun s => D2f (s, h s) (1, h' x1) (1, h' x1) - s / 4) + (Icc (-2 * r) (2 * r)) := by + refine monotoneOn_of_deriv_nonneg (convex_Icc _ _) + (fun t ht => (hφ t ht).continuousAt.continuousWithinAt) + (fun t ht => (hφ t (interior_subset ht)).differentiableAt.differentiableWithinAt) ?_ + intro t ht + rw [(hφ t (interior_subset ht)).deriv] + have := hΦb t (interior_subset ht) (h' x1) (hu x1 hx1) + linarith + have h12 := hφmono hx1 hx2 hle + obtain ⟨-, he1, -⟩ := schur_max hδ (hneg x1 hx1) (hid x1 hx1) + obtain ⟨-, he2, hmax2⟩ := schur_max hδ (hneg x2 hx2) (hid x2 hx2) + have hm2 := hmax2 (hsym x2 hx2) (h' x1) + simp only at h12 ⊢ + rw [← he1, ← he2] + linarith + refine MonotoneOn.convexOn_of_deriv (convex_Icc _ _) + (fun x hx => (hF x hx).continuousAt.continuousWithinAt) + (fun x hx => (hF x (interior_subset hx)).differentiableAt.differentiableWithinAt) ?_ + intro x1 hx1 x2 hx2 hle + rw [(hF x1 (interior_subset hx1)).deriv, (hF x2 (interior_subset hx2)).deriv] + exact hmono (interior_subset hx1) (interior_subset hx2) hle + + +/-- **L3 in `y` for `∂_x ∇_y f`.** If along the segment `s ↦ (x, s • y)` the third derivatives +satisfy `|T (1, 0) (0, v) (0, y)| ≤ m ‖v‖ ‖y‖` (the block `f_xyy`), then +`‖∂_x ∇_y f (x, y) - ∂_x ∇_y f (x, 0)‖ ≤ m ‖y‖`. -/ +theorem dx_grad_increment {D2f : ℝ × E → ℝ × E →L[ℝ] ℝ × E →L[ℝ] ℝ} + {T3 : ℝ × E → ℝ × E → ℝ × E → ℝ × E →L[ℝ] ℝ} {x m : ℝ} {y : E} (hm : 0 ≤ m) + (hD3 : ∀ s ∈ Icc (0 : ℝ) 1, ∀ a b : ℝ × E, + HasFDerivAt (fun q => D2f q a b) (T3 (x, s • y) a b) (x, s • y)) + (hT : ∀ s ∈ Icc (0 : ℝ) 1, ∀ v : E, |T3 (x, s • y) (1, 0) (0, v) (0, y)| ≤ m * ‖v‖ * ‖y‖) : + ‖(D2f (x, y) (1, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E) - + (D2f (x, 0) (1, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)‖ ≤ m * ‖y‖ := by + refine ContinuousLinearMap.opNorm_le_bound _ (by positivity) fun v => ?_ + have hφ : ∀ s ∈ Icc (0 : ℝ) 1, HasDerivAt (fun s : ℝ => D2f (x, s • y) (1, 0) (0, v)) + (T3 (x, s • y) (1, 0) (0, v) (0, y)) s := by + intro s hs + have hp : HasDerivAt (fun s : ℝ => (x, s • y)) ((0 : ℝ), y) s := by + simpa using (hasDerivAt_const s x).prodMk ((hasDerivAt_id s).smul_const y) + exact (hD3 s hs (1, 0) (0, v)).comp_hasDerivAt s hp + have hφb : ∀ s ∈ Icc (0 : ℝ) 1, ‖T3 (x, s • y) (1, 0) (0, v) (0, y)‖ ≤ m * ‖v‖ * ‖y‖ := + fun s hs => by rw [Real.norm_eq_abs]; exact hT s hs v + have := (convex_Icc (0 : ℝ) 1).norm_image_sub_le_of_norm_hasDerivWithin_le + (fun s hs => (hφ s hs).hasDerivWithinAt) hφb (left_mem_Icc.mpr zero_le_one) + (right_mem_Icc.mpr zero_le_one) + simp only [one_smul, zero_smul, sub_zero, norm_one, mul_one] at this + simp only [sub_apply, ContinuousLinearMap.comp_apply, + ContinuousLinearMap.inr_apply] + calc ‖(D2f (x, y)) (1, 0) (0, v) - (D2f (x, 0)) (1, 0) (0, v)‖ ≤ m * ‖v‖ * ‖y‖ := this + _ = m * ‖y‖ * ‖v‖ := by ring + +/-- **L9's arithmetic.** From `δ ‖h'‖ ≤ ‖∂_x∇_y f(x, h)‖ ≤ 2mr + m‖h‖` and `δ ‖h‖ ≤ 2mr²`: +`‖h'‖ ≤ 2s + 2s²` with `s = mr/δ` (SP: `u = 2/k + 2/k²`). -/ +theorem l9_arith {δ m r a b c : ℝ} (hδ : 0 < δ) (hm : 0 ≤ m) (ha : δ * a ≤ c) + (hc : c ≤ 2 * m * r + m * b) (hb : δ * b ≤ 2 * m * r ^ 2) : + a ≤ 2 * (m * r / δ) + 2 * (m * r / δ) ^ 2 := by + have key : δ * δ * a ≤ 2 * m * r * δ + 2 * m * m * r ^ 2 := by nlinarith + have hrhs : 2 * (m * r / δ) + 2 * (m * r / δ) ^ 2 = + (2 * m * r * δ + 2 * m * m * r ^ 2) / (δ * δ) := by + field_simp + rw [hrhs, le_div_iff₀ (by positivity)] + linarith + +/-- **L12's bound at one point.** With the combined block bound, `f_xxx ≥ 7/4`, `‖a‖, ‖b‖ ≤ u` +and `7/4 - m((1 + u)³ - 1) ≥ 1/4` (`l12_constants`): `T (1, b) (1, b) (1, a) ≥ 1/4`. -/ +theorem l12_lower {T : ℝ × E → ℝ × E → ℝ × E →L[ℝ] ℝ} {m u : ℝ} {a b : E} (hm : 0 ≤ m) + (hT : ∀ (s₁ s₂ s₃ : ℝ) (y₁ y₂ y₃ : E), + |T (s₁, y₁) (s₂, y₂) (s₃, y₃) - s₁ * s₂ * s₃ * T (1, 0) (1, 0) (1, 0)| ≤ + m * ((|s₁| + ‖y₁‖) * (|s₂| + ‖y₂‖) * (|s₃| + ‖y₃‖) - |s₁| * |s₂| * |s₃|)) + (hxxx : 7 / 4 ≤ T (1, 0) (1, 0) (1, 0)) (hc : 1 / 4 ≤ 7 / 4 - m * ((1 + u) ^ 3 - 1)) + (ha : ‖a‖ ≤ u) (hb : ‖b‖ ≤ u) : 1 / 4 ≤ T (1, b) (1, b) (1, a) := by + have h1 := trilinear_lower hT a b + have hnb := norm_nonneg b + have hna := norm_nonneg a + have hb1 : 1 + ‖b‖ ≤ 1 + u := by linarith + have ha1 : 1 + ‖a‖ ≤ 1 + u := by linarith + have h4 : (1 + ‖b‖) * (1 + ‖b‖) * (1 + ‖a‖) ≤ (1 + u) ^ 3 := by + have e : (1 + u) ^ 3 = (1 + u) * (1 + u) * (1 + u) := by ring + rw [e] + exact mul_le_mul (mul_le_mul hb1 hb1 (by linarith) (by linarith)) ha1 (by linarith) + (mul_nonneg (by linarith) (by linarith)) + have h5 := mul_le_mul_of_nonneg_left (sub_le_sub_right h4 1) hm + linarith + +/-- **The ridge facts from SP's source data.** Under the hypotheses of `ridge_capHyp_source`, for a +ridge `h` on the collar: `m ≥ 2`, `δ = λ - 5rm > rm(8m - 5)`, `h x` lies in the open ball and +`δ ‖h x‖ ≤ 2mr²` on `[-2r, 2r]` (L5 and L8), `h` is differentiable there (L7), and the transverse +Hessian along the ridge is `δ`-negative definite (L4). -/ +theorem ridge_source_facts [FiniteDimensional ℝ E] {f : ℝ × E → ℝ} + {Df : ℝ × E → ℝ × E →L[ℝ] ℝ} {DG : ℝ × E → ℝ × E →L[ℝ] E →L[ℝ] ℝ} + {H : ℝ × E → E →L[ℝ] E →L[ℝ] ℝ} {Hx : ℝ → E →L[ℝ] E →L[ℝ] ℝ} + {Hr : ℝ × E → ℝ → E →L[ℝ] E →L[ℝ] ℝ} {r m lam ε : ℝ} (hr : 0 < r) (hε : 0 < ε) + (hεr : ε ≤ r / 2) + (hDf : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), HasFDerivAt f (Df p) p) + (hGs : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + HasStrictFDerivAt (fun q => (Df q).comp (ContinuousLinearMap.inr ℝ ℝ E)) (DG p) p) + (hH : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + HasFDerivAt (fun y => (Df (p.1, y)).comp (ContinuousLinearMap.inr ℝ ℝ E)) (H p) p.2) + (hHx : ∀ x ∈ Icc (-2 * r - ε) (2 * r + ε), HasDerivAt (fun t => H (t, 0)) (Hx x) x) + (hHxb : ∀ x ∈ Icc (-2 * r - ε) (2 * r + ε), ‖Hx x‖ ≤ m) + (hHr : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + ∀ s ∈ Icc (0 : ℝ) 1, HasDerivAt (fun s : ℝ => H (p.1, s • p.2)) (Hr p s) s) + (hHrb : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + ∀ s ∈ Icc (0 : ℝ) 1, ‖Hr p s‖ ≤ m * ‖p.2‖) + (hlam : ∀ v : E, H (-r / 2, 0) v v ≤ -lam * ‖v‖ ^ 2) (hH1 : 8 * r * m ^ 2 < lam) + (hM : Df (-r / 2, 0) = 0) (hS : Df (r / 2, 0) = 0) + (hG0cv : ConvexOn ℝ (Icc (-r / 2) (r / 2)) (fun t => Df (t, 0) (1, 0) + m / 2 * t ^ 2)) + (hG0cc : ConcaveOn ℝ (Icc (-r / 2) (r / 2)) (fun t => Df (t, 0) (1, 0) - m / 2 * t ^ 2)) + (hwcv : ∀ v : E, ConvexOn ℝ (Icc (-2 * r - ε) (2 * r + ε)) + (fun t => Df (t, 0) (0, v) + m * ‖v‖ / 2 * t ^ 2)) + (hwcc : ∀ v : E, ConcaveOn ℝ (Icc (-2 * r - ε) (2 * r + ε)) + (fun t => Df (t, 0) (0, v) - m * ‖v‖ / 2 * t ^ 2)) + (hnorm : f (-r / 2, 0) - f (r / 2, 0) = r ^ 3 / 6) {h : ℝ → E} + (hhU : ∀ x ∈ Ioo (-2 * r - ε) (2 * r + ε), h x ∈ Metric.closedBall (0 : E) (2 * r) ∧ + HasFDerivAt (fun y => f (x, y)) (0 : E →L[ℝ] ℝ) (h x)) : + 2 ≤ m ∧ r * m * (8 * m - 5) < lam - 5 * r * m ∧ + (∀ x ∈ Icc (-2 * r) (2 * r), h x ∈ Metric.ball (0 : E) (2 * r)) ∧ + (∀ x ∈ Icc (-2 * r) (2 * r), (lam - 5 * r * m) * ‖h x‖ ≤ 2 * m * r ^ 2) ∧ + (∃ h' : ℝ → E, ∀ x ∈ Icc (-2 * r) (2 * r), HasDerivAt h (h' x) x) ∧ + (∀ x ∈ Icc (-2 * r) (2 * r), ∀ v : E, H (x, h x) v v ≤ -(lam - 5 * r * m) * ‖v‖ ^ 2) := by + have hUX : Ioo (-2 * r - ε) (2 * r + ε) ⊆ Icc (-2 * r - ε) (2 * r + ε) := Ioo_subset_Icc_self + have hcapX : Icc (-2 * r) (r / 2) ⊆ Icc (-2 * r - ε) (2 * r + ε) := + Icc_subset_Icc (by linarith) (by linarith) + have hIU : Icc (-2 * r) (2 * r) ⊆ Ioo (-2 * r - ε) (2 * r + ε) := + fun t ht => ⟨by linarith [ht.1], by linarith [ht.2]⟩ + have h0Y : (0 : E) ∈ Metric.closedBall (0 : E) (2 * r) := Metric.mem_closedBall_self (by positivity) + -- the slice derivatives are the transverse parts of `Df` + have hD : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + HasFDerivAt (fun y => f (p.1, y)) ((Df p).comp (ContinuousLinearMap.inr ℝ ℝ E)) p.2 := by + rintro ⟨x, y⟩ hp + exact slice_hasFDerivAt (hDf (x, y) hp) + -- L1–L2: `m ≥ 2` + have hg0 : ∀ x ∈ Icc (-r / 2) (r / 2), + HasDerivAt (fun x => f (x, 0)) (Df (x, 0) (1, 0)) x := by + intro x hx + have hx' : (x, (0 : E)) ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r) := + ⟨⟨by linarith [hx.1], by linarith [hx.2]⟩, h0Y⟩ + have hp : HasDerivAt (fun t : ℝ => (t, (0 : E))) ((1 : ℝ), (0 : E)) x := + (hasDerivAt_id x).prodMk (hasDerivAt_const x (0 : E)) + exact (hDf _ hx').comp_hasDerivAt x hp + have hG0a : Df (-r / 2, 0) (1, 0) = 0 := by simp [hM] + have hG0c : Df (r / 2, 0) (1, 0) = 0 := by simp [hS] + have hm : 2 ≤ m := hermite_m_ge_two (g := fun x => f (x, 0)) hr hg0 hG0cv hG0cc hG0a hG0c hnorm + have hm0 : 0 ≤ m := by linarith + -- L3–L4 on the full domain + have hlip := hessian_increment_D hr hε hHx hHxb hHr hHrb + have hneg := transverse_hessian_le_D hm0 hε hεr hlip hlam + have hconcX := slices_strongConcave_D hm0 hε hεr hD hH hlip hlam + have h11 : 11 * (r * m) < lam - 5 * r * m := by + nlinarith [mul_nonneg (mul_nonneg hr.le hm0) (sub_nonneg.2 hm)] + have hrm : 0 < r * m := mul_pos hr (by linarith) + have hδ0 : 0 < lam - 5 * r * m := by linarith + -- L5 on the full domain: `‖w x‖ ≤ 3mr² < 2rδ` + have hwv : ∀ (t : ℝ) (v : E), + ((Df (t, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)) v = Df (t, 0) (0, v) := fun t v => by simp + have hwcv' : ∀ v : E, ConvexOn ℝ (Icc (-2 * r - ε) (2 * r + ε)) + (fun t => ((Df (t, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)) v + m * ‖v‖ / 2 * t ^ 2) := + fun v => (hwcv v).congr fun t _ => by simp only [hwv] + have hwcc' : ∀ v : E, ConcaveOn ℝ (Icc (-2 * r - ε) (2 * r + ε)) + (fun t => ((Df (t, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)) v - m * ‖v‖ / 2 * t ^ 2) := + fun v => (hwcc v).congr fun t _ => by simp only [hwv] + have hwa : (Df (-r / 2, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E) = 0 := by simp [hM] + have hwc : (Df (r / 2, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E) = 0 := by simp [hS] + have hwlt : ∀ x ∈ Icc (-2 * r - ε) (2 * r + ε), + ‖(Df (x, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)‖ < (lam - 5 * r * m) * (2 * r) := by + intro x hx + have h1 := slice_gradient_bound (w := fun t => (Df (t, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)) + hm0 hwcv' hwcc' (show -r / 2 ∈ Icc (-2 * r - ε) (2 * r + ε) from ⟨by linarith, by linarith⟩) + (show r / 2 ∈ Icc (-2 * r - ε) (2 * r + ε) from ⟨by linarith, by linarith⟩) (by linarith) + hwa hwc hx + have h2 : |(x - -r / 2) * (x - r / 2)| ≤ 6 * r ^ 2 := by + have hxx : 0 ≤ (x - (-2 * r - ε)) * (2 * r + ε - x) := + mul_nonneg (by linarith [hx.1]) (by linarith [hx.2]) + have hee : 0 ≤ (r / 2 - ε) * (9 * r / 2 + ε) := + mul_nonneg (by linarith) (by linarith) + rw [abs_le]; constructor <;> nlinarith [sq_nonneg x, sq_nonneg r] + have h3 : ‖(Df (x, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)‖ ≤ 3 * m * r ^ 2 := + calc ‖(Df (x, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)‖ + ≤ m / 2 * |(x - -r / 2) * (x - r / 2)| := h1 + _ ≤ m / 2 * (6 * r ^ 2) := by gcongr + _ = 3 * m * r ^ 2 := by ring + have h4 : 22 * r * (r * m) < (lam - 5 * r * m) * (2 * r) := by nlinarith + nlinarith + have hslice0 : ∀ x ∈ Icc (-2 * r - ε) (2 * r + ε), + HasFDerivAt (fun y => f (x, y)) ((Df (x, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)) 0 := + fun x hx => hD (x, 0) ⟨hx, h0Y⟩ + have hball : ∀ x ∈ Ioo (-2 * r - ε) (2 * r + ε), h x ∈ Metric.closedBall (0 : E) (2 * r) := + fun x hx => (hhU x hx).1 + have hcrit : ∀ x ∈ Ioo (-2 * r - ε) (2 * r + ε), + HasFDerivAt (fun y => f (x, y)) (0 : E →L[ℝ] ℝ) (h x) := fun x hx => (hhU x hx).2 + -- L8: the ridge is in the open ball on `[-2r, 2r]` + have hint : ∀ x ∈ Icc (-2 * r) (2 * r), h x ∈ Metric.ball (0 : E) (2 * r) := by + intro x hx + have hxU := hIU hx + have h8 := slice_ridge_bound (hconcX x (hUX hxU)) h0Y (hball x hxU) (hcrit x hxU) + (hslice0 x (hUX hxU)) + have h9 := hwlt x (hUX hxU) + rw [Metric.mem_ball, dist_zero_right] + have : (lam - 5 * r * m) * ‖h x‖ < (lam - 5 * r * m) * (2 * r) := by linarith + exact lt_of_mul_lt_mul_left this hδ0.le + have hridgeX : ∀ x ∈ Icc (-2 * r) (2 * r), + (x, h x) ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r) := + fun x hx => ⟨hUX (hIU hx), hball x (hIU hx)⟩ + -- L7 regularity: the transverse part of `DG` is `H`, negative definite + have hDGH : ∀ x ∈ Icc (-2 * r) (2 * r), + DG (x, h x) ∘L ContinuousLinearMap.inr ℝ ℝ E = H (x, h x) := by + intro x hx + have h1 : HasFDerivAt (fun y => (Df (x, y)).comp (ContinuousLinearMap.inr ℝ ℝ E)) + ((DG (x, h x)).comp (ContinuousLinearMap.inr ℝ ℝ E)) (h x) := + (hGs _ (hridgeX x hx)).hasFDerivAt.comp (h x) (hasFDerivAt_prodMk_right x (h x)) + exact h1.unique (hH _ (hridgeX x hx)) + have hnegR : ∀ x ∈ Icc (-2 * r) (2 * r), ∀ v : E, + (DG (x, h x) ∘L ContinuousLinearMap.inr ℝ ℝ E) v v ≤ -(lam - 5 * r * m) * ‖v‖ ^ 2 := by + intro x hx v + rw [hDGH x hx] + exact hneg _ (hridgeX x hx) v + have hG : ∀ x ∈ Icc (-2 * r) (2 * r), ∀ᶠ v in 𝓝 (x, h x), + HasFDerivAt (fun y => f (v.1, y)) ((Df v).comp (ContinuousLinearMap.inr ℝ ℝ E)) v.2 := by + intro x hx + have hopen : IsOpen (Ioo (-2 * r - ε) (2 * r + ε) ×ˢ Metric.ball (0 : E) (2 * r)) := + isOpen_Ioo.prod Metric.isOpen_ball + filter_upwards [hopen.mem_nhds ⟨hIU hx, hint x hx⟩] with v hv + exact hD v ⟨hUX hv.1, Metric.ball_subset_closedBall hv.2⟩ + have hstrict := ridge_differentiable (f := f) + (G := fun q => (Df q).comp (ContinuousLinearMap.inr ℝ ℝ E)) (DG := fun x => DG (x, h x)) + (h := h) (U := Ioo (-2 * r - ε) (2 * r + ε)) hδ0 isOpen_Ioo hIU + (fun x hx => hconcX x (hUX hx)) hball hcrit hint hG + (fun x hx => hGs _ (hridgeX x hx)) hnegR + have hmemA : -r / 2 ∈ Icc (-2 * r - ε) (2 * r + ε) := ⟨by linarith, by linarith⟩ + have hmemC : r / 2 ∈ Icc (-2 * r - ε) (2 * r + ε) := ⟨by linarith, by linarith⟩ + have hw2 : ∀ x ∈ Icc (-2 * r) (2 * r), + ‖(Df (x, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)‖ ≤ 2 * m * r ^ 2 := by + intro x hx + have h1 := slice_gradient_bound + (w := fun t => (Df (t, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)) hm0 hwcv' hwcc' hmemA hmemC + (by linarith) hwa hwc (hUX (hIU hx)) + have h2 : |(x - -r / 2) * (x - r / 2)| ≤ 4 * r ^ 2 := by + have hxx : 0 ≤ (x - -2 * r) * (2 * r - x) := + mul_nonneg (by linarith [hx.1]) (by linarith [hx.2]) + rw [abs_le]; constructor <;> nlinarith [sq_nonneg x, sq_nonneg r] + calc ‖(Df (x, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)‖ + ≤ m / 2 * |(x - -r / 2) * (x - r / 2)| := h1 + _ ≤ m / 2 * (4 * r ^ 2) := by gcongr + _ = 2 * m * r ^ 2 := by ring + refine ⟨hm, by nlinarith, hint, fun x hx => + (slice_ridge_bound (hconcX x (hUX (hIU hx))) h0Y (hball x (hIU hx)) (hcrit x (hIU hx)) + (hslice0 x (hUX (hIU hx)))).trans (hw2 x hx), + ⟨_, fun x hx => (hstrict x hx).hasFDerivAt.hasDerivAt⟩, + fun x hx v => hneg _ (hridgeX x hx) v⟩ + + +/-- **The cap from SP's `C³` source data (L1–L20 composed; L12 proved).** As +`ridge_capHyp_source`, with L12's `hconv` derived instead of assumed. Additionally assume, on the +collar: a second derivative `D2f` of `f`, third derivatives `T3 p a b` of `p ↦ D²f p [a, b]`, every +third-derivative block other than `f_xxx` of norm at most `m` (combined form), and `f_xxx ≥ 7/4` on +`D = [-2r, 2r] × B̄(0, 2r)` (SP's L4, from L2 and (H2), on SP's domain). Then the ridge exists, and every ridge has `h(∓r/2) = 0` and yields +(C1)–(C3) and (C2⁺) on the cap. Inside: L5 gives `‖w‖ ≤ 2mr²` on `[-2r, 2r]`, L8 `‖h‖ ≤ 2mr²/δ`, L6 +`‖w'‖ ≤ 2mr`, L3 in `y` `‖∂_x∇_y f(x, h)‖ ≤ ‖w'‖ + m‖h‖`, L9 `‖h'‖ ≤ 2s + 2s²` with `s = mr/δ`, +`trilinear_lower` and `l12_constants` give `F'' ≥ 1/4` in the form of `ridge_hconv`. -/ +theorem ridge_capHyp_C3 [FiniteDimensional ℝ E] {f : ℝ × E → ℝ} + {Df : ℝ × E → ℝ × E →L[ℝ] ℝ} {D2f : ℝ × E → ℝ × E →L[ℝ] ℝ × E →L[ℝ] ℝ} + {T3 : ℝ × E → ℝ × E → ℝ × E → ℝ × E →L[ℝ] ℝ} + {DG : ℝ × E → ℝ × E →L[ℝ] E →L[ℝ] ℝ} + {H : ℝ × E → E →L[ℝ] E →L[ℝ] ℝ} {Hx : ℝ → E →L[ℝ] E →L[ℝ] ℝ} + {Hr : ℝ × E → ℝ → E →L[ℝ] E →L[ℝ] ℝ} {r m lam ε : ℝ} (hr : 0 < r) (hε : 0 < ε) + (hεr : ε ≤ r / 2) + (hDf : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), HasFDerivAt f (Df p) p) + (hD2 : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), HasFDerivAt Df (D2f p) p) + (hD3 : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), ∀ a b : ℝ × E, HasFDerivAt (fun q => D2f q a b) (T3 p a b) p) + (hT : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), ∀ (s₁ s₂ s₃ : ℝ) (y₁ y₂ y₃ : E), + |T3 p (s₁, y₁) (s₂, y₂) (s₃, y₃) - s₁ * s₂ * s₃ * T3 p (1, 0) (1, 0) (1, 0)| ≤ + m * ((|s₁| + ‖y₁‖) * (|s₂| + ‖y₂‖) * (|s₃| + ‖y₃‖) - |s₁| * |s₂| * |s₃|)) + (hxxx : ∀ p ∈ Icc (-2 * r) (2 * r) ×ˢ Metric.closedBall (0 : E) (2 * r), + 7 / 4 ≤ T3 p (1, 0) (1, 0) (1, 0)) + (hGs : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + HasStrictFDerivAt (fun q => (Df q).comp (ContinuousLinearMap.inr ℝ ℝ E)) (DG p) p) + (hH : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + HasFDerivAt (fun y => (Df (p.1, y)).comp (ContinuousLinearMap.inr ℝ ℝ E)) (H p) p.2) + (hHx : ∀ x ∈ Icc (-2 * r - ε) (2 * r + ε), HasDerivAt (fun t => H (t, 0)) (Hx x) x) + (hHxb : ∀ x ∈ Icc (-2 * r - ε) (2 * r + ε), ‖Hx x‖ ≤ m) + (hHr : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + ∀ s ∈ Icc (0 : ℝ) 1, HasDerivAt (fun s : ℝ => H (p.1, s • p.2)) (Hr p s) s) + (hHrb : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + ∀ s ∈ Icc (0 : ℝ) 1, ‖Hr p s‖ ≤ m * ‖p.2‖) + (hlam : ∀ v : E, H (-r / 2, 0) v v ≤ -lam * ‖v‖ ^ 2) (hH1 : 8 * r * m ^ 2 < lam) + (hM : Df (-r / 2, 0) = 0) (hS : Df (r / 2, 0) = 0) + (hG0cv : ConvexOn ℝ (Icc (-r / 2) (r / 2)) (fun t => Df (t, 0) (1, 0) + m / 2 * t ^ 2)) + (hG0cc : ConcaveOn ℝ (Icc (-r / 2) (r / 2)) (fun t => Df (t, 0) (1, 0) - m / 2 * t ^ 2)) + (hwcv : ∀ v : E, ConvexOn ℝ (Icc (-2 * r - ε) (2 * r + ε)) + (fun t => Df (t, 0) (0, v) + m * ‖v‖ / 2 * t ^ 2)) + (hwcc : ∀ v : E, ConcaveOn ℝ (Icc (-2 * r - ε) (2 * r + ε)) + (fun t => Df (t, 0) (0, v) - m * ‖v‖ / 2 * t ^ 2)) + (hnorm : f (-r / 2, 0) - f (r / 2, 0) = r ^ 3 / 6) : + (∃ h : ℝ → E, ∀ x ∈ Ioo (-2 * r - ε) (2 * r + ε), h x ∈ Metric.ball (0 : E) (2 * r) ∧ + HasFDerivAt (fun y => f (x, y)) (0 : E →L[ℝ] ℝ) (h x)) ∧ + ∀ h : ℝ → E, (∀ x ∈ Ioo (-2 * r - ε) (2 * r + ε), + h x ∈ Metric.closedBall (0 : E) (2 * r) ∧ + HasFDerivAt (fun y => f (x, y)) (0 : E →L[ℝ] ℝ) (h x)) → + h (-r / 2) = 0 ∧ h (r / 2) = 0 ∧ + CapHyp f (Icc (-2 * r) (r / 2) ×ˢ Metric.closedBall (0 : E) (2 * r)) (-r / 2, 0) + (2 * r, h (2 * r)) (f (-r / 2, 0)) (f (r / 2, 0)) ∧ + ∀ x ∈ frontier (Icc (-2 * r) (r / 2) ×ˢ Metric.closedBall (0 : E) (2 * r)), + x ≠ (r / 2, 0) → f x < f (r / 2, 0) := by + obtain ⟨hex, hcapS⟩ := ridge_capHyp_source hr hε hεr hDf hGs hH hHx hHxb hHr hHrb hlam hH1 hM hS + hG0cv hG0cc hwcv hwcc hnorm + refine ⟨hex, fun h hhU => hcapS h hhU ?_⟩ + obtain ⟨hm, hδ, hint, hh8, ⟨h', hhd⟩, hnegH⟩ := ridge_source_facts hr hε hεr hDf hGs hH hHx hHxb + hHr hHrb hlam hH1 hM hS hG0cv hG0cc hwcv hwcc hnorm hhU + have hm0 : 0 ≤ m := by linarith + have hδ0 : 0 < lam - 5 * r * m := by + have : 0 < r * m * (8 * m - 5) := mul_pos (mul_pos hr (by linarith)) (by linarith) + linarith + have hUX : Ioo (-2 * r - ε) (2 * r + ε) ⊆ Icc (-2 * r - ε) (2 * r + ε) := Ioo_subset_Icc_self + have hIU : Icc (-2 * r) (2 * r) ⊆ Ioo (-2 * r - ε) (2 * r + ε) := + fun t ht => ⟨by linarith [ht.1], by linarith [ht.2]⟩ + have h0Y : (0 : E) ∈ Metric.closedBall (0 : E) (2 * r) := Metric.mem_closedBall_self (by positivity) + have hball : ∀ x ∈ Ioo (-2 * r - ε) (2 * r + ε), h x ∈ Metric.closedBall (0 : E) (2 * r) := + fun x hx => (hhU x hx).1 + have hridgeX : ∀ x ∈ Icc (-2 * r) (2 * r), + (x, h x) ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r) := + fun x hx => ⟨hUX (hIU hx), hball x (hIU hx)⟩ + have hridgeU : ∀ x ∈ Ioo (-2 * r - ε) (2 * r + ε), + (Df (x, h x)).comp (ContinuousLinearMap.inr ℝ ℝ E) = 0 := fun x hx => + (slice_hasFDerivAt (hDf _ ⟨hUX hx, hball x hx⟩)).unique (hhU x hx).2 + have hD2r : ∀ x ∈ Icc (-2 * r) (2 * r), HasFDerivAt Df (D2f (x, h x)) (x, h x) := + fun x hx => hD2 _ (hridgeX x hx) + have hsym : ∀ x ∈ Icc (-2 * r) (2 * r), ∀ v w, D2f (x, h x) v w = D2f (x, h x) w v := by + intro x hx v w + have hopen : IsOpen (Ioo (-2 * r - ε) (2 * r + ε) ×ˢ Metric.ball (0 : E) (2 * r)) := + isOpen_Ioo.prod Metric.isOpen_ball + have hev : ∀ᶠ q in 𝓝 (x, h x), HasFDerivAt f (Df q) q := by + filter_upwards [hopen.mem_nhds ⟨hIU hx, hint x hx⟩] with q hq + exact hDf q ⟨hUX hq.1, Metric.ball_subset_closedBall hq.2⟩ + exact second_derivative_symmetric_of_eventually hev (hD2r x hx) v w + have hnegD : ∀ x ∈ Icc (-2 * r) (2 * r), ∀ v : E, + D2f (x, h x) (0, v) (0, v) ≤ -(lam - 5 * r * m) * ‖v‖ ^ 2 := by + intro x hx v + rw [← transverse_hessian_eq (hH _ (hridgeX x hx)) (hD2r x hx) v v] + exact hnegH x hx v + -- L6: `‖w' x‖ ≤ 2mr` + have hwcv' : ∀ v : E, ConvexOn ℝ (Icc (-2 * r - ε) (2 * r + ε)) + (fun t => ((Df (t, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)) v + m * ‖v‖ / 2 * t ^ 2) := + fun v => (hwcv v).congr fun t _ => by simp + have hwcc' : ∀ v : E, ConcaveOn ℝ (Icc (-2 * r - ε) (2 * r + ε)) + (fun t => ((Df (t, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)) v - m * ‖v‖ / 2 * t ^ 2) := + fun v => (hwcc v).congr fun t _ => by simp + have hw6 : ∀ x ∈ Icc (-2 * r) (2 * r), + ‖(D2f (x, 0) (1, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)‖ ≤ 2 * m * r := by + intro x hx + have hp : HasDerivAt (fun t : ℝ => (t, (0 : E))) ((1 : ℝ), (0 : E)) x := + (hasDerivAt_id x).prodMk (hasDerivAt_const x (0 : E)) + have h1 : HasDerivAt (fun t => Df (t, 0)) (D2f (x, 0) (1, 0)) x := + (hD2 _ ⟨hUX (hIU hx), h0Y⟩).comp_hasDerivAt x hp + have hd : HasDerivAt (fun t => (Df (t, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)) + ((D2f (x, 0) (1, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)) x := by + simpa using h1.clm_comp (hasDerivAt_const x (ContinuousLinearMap.inr ℝ ℝ E)) + have h2 := slice_gradient_deriv_bound hr hm0 hwcv' hwcc' + (show -r / 2 ∈ Icc (-2 * r - ε) (2 * r + ε) from ⟨by linarith, by linarith⟩) + (show r / 2 ∈ Icc (-2 * r - ε) (2 * r + ε) from ⟨by linarith, by linarith⟩) + (by simp [hM]) (by simp [hS]) (hUX (hIU hx)) hd + have h3 : max |x| (r / 2) ≤ 2 * r := + max_le (abs_le.mpr ⟨by linarith [hx.1], by linarith [hx.2]⟩) (by linarith) + calc ‖(D2f (x, 0) (1, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)‖ ≤ m * max |x| (r / 2) := h2 + _ ≤ m * (2 * r) := mul_le_mul_of_nonneg_left h3 hm0 + _ = 2 * m * r := by ring + -- L3 in `y`, then L9 + have hu : ∀ x ∈ Icc (-2 * r) (2 * r), ‖h' x‖ ≤ + 2 * (m * r / (lam - 5 * r * m)) + 2 * (m * r / (lam - 5 * r * m)) ^ 2 := by + intro x hx + have hseg : ∀ s ∈ Icc (0 : ℝ) 1, + (x, s • h x) ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r) := by + intro s hs + have hhY : ‖h x‖ ≤ 2 * r := by + simpa [Metric.mem_closedBall, dist_zero_right] using hball x (hIU hx) + refine ⟨hUX (hIU hx), ?_⟩ + rw [Metric.mem_closedBall, dist_zero_right, norm_smul, Real.norm_eq_abs, abs_of_nonneg hs.1] + nlinarith [hs.2, norm_nonneg (h x)] + have hinc := dx_grad_increment (D2f := D2f) (T3 := T3) (x := x) (y := h x) hm0 + (fun s hs => hD3 _ (hseg s hs)) + (fun s hs v => by + have := hT _ (hseg s hs) 1 0 0 0 v (h x) + simpa [mul_assoc] using this) + have hBn : ‖(D2f (x, h x) (1, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)‖ ≤ + 2 * m * r + m * ‖h x‖ := + (norm_le_norm_add_norm_sub' _ _).trans (add_le_add (hw6 x hx) hinc) + have hid := ridge_second_identity + (Filter.eventually_of_mem (isOpen_Ioo.mem_nhds (hIU hx)) hridgeU) (hhd x hx) (hD2r x hx) + obtain ⟨h9, -, -⟩ := schur_max hδ0 (hnegD x hx) hid + exact l9_arith hδ0 hm0 h9 hBn (hh8 x hx) + -- L12 + have hc := l12_constants hr hm hδ + have hΦ : ∀ x ∈ Icc (-2 * r) (2 * r), ∀ b : E, + HasDerivAt (fun s => D2f (s, h s) (1, b) (1, b)) (T3 (x, h x) (1, b) (1, b) (1, h' x)) x := by + intro x hx b + have hp : HasDerivAt (fun s => (s, h s)) ((1 : ℝ), h' x) x := (hasDerivAt_id x).prodMk (hhd x hx) + exact (hD3 _ (hridgeX x hx) (1, b) (1, b)).comp_hasDerivAt x hp + exact ridge_hconv (Φ := fun x b => T3 (x, h x) (1, b) (1, b) (1, h' x)) hδ0 isOpen_Ioo hIU + hridgeU hhd hD2r hsym hnegD hu hΦ + (fun x hx b hb => l12_lower hm0 (hT _ (hridgeX x hx)) (hxxx _ ⟨hx, hball x (hIU hx)⟩) hc + (hu x hx) hb) + end Slice /-! ### A concrete instance and the necessity of each hypothesis @@ -2388,4 +3073,149 @@ theorem h1Toy_source : simp only [smul_eq_mul] simp +/-- **`ridge_capHyp_C3` is not vacuous.** `h1ToyF` meets every hypothesis of `ridge_capHyp_C3` +on the collar `ε = 1/2`: besides the data of `h1Toy_source`, second derivative +`D²f = diag(2x, -40)`, third derivatives `T a b = 2 a₁ b₁ · fst` (only `f_xxx = 2 ≥ 7/4` is nonzero, +so every other block vanishes). The theorem then gives the ridge and the cap with `M = (-1/2, 0)`, +with L12 derived rather than supplied. -/ +theorem h1Toy_C3 : + (∃ h : ℝ → ℝ, ∀ x ∈ Ioo (-2 * 1 - 1 / 2 : ℝ) (2 * 1 + 1 / 2), h x ∈ Metric.ball (0 : ℝ) (2 * 1) ∧ + HasFDerivAt (fun y => h1ToyF (x, y)) (0 : ℝ →L[ℝ] ℝ) (h x)) ∧ + CapHyp h1ToyF (Icc (-2 * 1) (1 / 2) ×ˢ Metric.closedBall (0 : ℝ) (2 * 1)) (-1 / 2, 0) + (2 * 1, 0) (h1ToyF (-1 / 2, 0)) (h1ToyF (1 / 2, 0)) := by + have hDf : ∀ p : ℝ × ℝ, HasFDerivAt h1ToyF ((p.1 ^ 2 - 1 / 4) • ContinuousLinearMap.fst ℝ ℝ ℝ + + (-40 * p.2) • ContinuousLinearMap.snd ℝ ℝ ℝ) p := by + intro p + have hf : HasFDerivAt (fun q : ℝ × ℝ => q.1) (ContinuousLinearMap.fst ℝ ℝ ℝ) p := + hasFDerivAt_fst + have hs : HasFDerivAt (fun q : ℝ × ℝ => q.2) (ContinuousLinearMap.snd ℝ ℝ ℝ) p := + hasFDerivAt_snd + have h1 := HasFDerivAt.sub (HasFDerivAt.sub + (HasFDerivAt.const_mul (HasFDerivAt.pow hf 3) (1 / 3)) (HasFDerivAt.const_mul hf (1 / 4))) + (HasFDerivAt.const_mul (HasFDerivAt.pow hs 2) 20) + convert h1 using 1 + · funext q + simp only [h1ToyF, Pi.sub_apply] + ring + · ext <;> simp; ring + have hGs : ∀ p : ℝ × ℝ, HasStrictFDerivAt (fun q : ℝ × ℝ => ((q.1 ^ 2 - 1 / 4) • + ContinuousLinearMap.fst ℝ ℝ ℝ + (-40 * q.2) • ContinuousLinearMap.snd ℝ ℝ ℝ).comp + (ContinuousLinearMap.inr ℝ ℝ ℝ)) + (((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ) ∘L ContinuousLinearMap.snd ℝ ℝ ℝ) p := by + intro p + convert (((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ) ∘L + ContinuousLinearMap.snd ℝ ℝ ℝ).hasStrictFDerivAt (x := p) using 1 + funext q + ext + simp + have hH : ∀ p : ℝ × ℝ, HasFDerivAt (fun y => ((p.1 ^ 2 - 1 / 4) • ContinuousLinearMap.fst ℝ ℝ ℝ + + (-40 * y) • ContinuousLinearMap.snd ℝ ℝ ℝ).comp (ContinuousLinearMap.inr ℝ ℝ ℝ)) + ((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ) p.2 := by + intro p + convert ((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ).hasFDerivAt (x := p.2) using 1 + funext y + ext + simp + have hf : ∀ p : ℝ × ℝ, HasFDerivAt (fun q : ℝ × ℝ => q.1) (ContinuousLinearMap.fst ℝ ℝ ℝ) p := + fun p => hasFDerivAt_fst + have hs : ∀ p : ℝ × ℝ, HasFDerivAt (fun q : ℝ × ℝ => q.2) (ContinuousLinearMap.snd ℝ ℝ ℝ) p := + fun p => hasFDerivAt_snd + have hD2 : ∀ p : ℝ × ℝ, HasFDerivAt (fun q : ℝ × ℝ => (q.1 ^ 2 - 1 / 4) • + ContinuousLinearMap.fst ℝ ℝ ℝ + (-40 * q.2) • ContinuousLinearMap.snd ℝ ℝ ℝ) + (((2 * p.1) • ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight (ContinuousLinearMap.fst ℝ ℝ ℝ) + + ((-40 : ℝ) • ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight (ContinuousLinearMap.snd ℝ ℝ ℝ)) p := by + intro p + have h1 : HasFDerivAt (fun q : ℝ × ℝ => q.1 ^ 2 - 1 / 4) ((2 * p.1) • ContinuousLinearMap.fst ℝ ℝ ℝ) + p := by + have := (HasFDerivAt.pow (hf p) 2).sub_const (1 / 4) + convert this using 1 + ext <;> simp + have h2 : HasFDerivAt (fun q : ℝ × ℝ => -40 * q.2) ((-40 : ℝ) • ContinuousLinearMap.snd ℝ ℝ ℝ) p := + HasFDerivAt.const_mul (hs p) (-40) + exact (h1.smul_const (ContinuousLinearMap.fst ℝ ℝ ℝ)).add + (h2.smul_const (ContinuousLinearMap.snd ℝ ℝ ℝ)) + have hD3 : ∀ p : ℝ × ℝ, ∀ a b : ℝ × ℝ, HasFDerivAt (fun q : ℝ × ℝ => + ((((2 * q.1) • ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight (ContinuousLinearMap.fst ℝ ℝ ℝ) + + ((-40 : ℝ) • ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight (ContinuousLinearMap.snd ℝ ℝ ℝ)) a) b) + ((2 * a.1 * b.1) • ContinuousLinearMap.fst ℝ ℝ ℝ) p := by + intro p a b + have := (HasFDerivAt.const_mul (hf p) (2 * a.1 * b.1)).add_const (-40 * a.2 * b.2) + convert this using 1 + funext q + simp + ring + have hT : ∀ p : ℝ × ℝ, ∀ (s₁ s₂ s₃ : ℝ) (y₁ y₂ y₃ : ℝ), + |((2 * (s₁, y₁).1 * (s₂, y₂).1) • ContinuousLinearMap.fst ℝ ℝ ℝ) (s₃, y₃) - + s₁ * s₂ * s₃ * ((2 * ((1 : ℝ), (0 : ℝ)).1 * ((1 : ℝ), (0 : ℝ)).1) • + ContinuousLinearMap.fst ℝ ℝ ℝ) (1, 0)| ≤ + 2 * ((|s₁| + ‖y₁‖) * (|s₂| + ‖y₂‖) * (|s₃| + ‖y₃‖) - |s₁| * |s₂| * |s₃|) := by + intro p s₁ s₂ s₃ y₁ y₂ y₃ + have h0 : ((2 * (s₁, y₁).1 * (s₂, y₂).1) • ContinuousLinearMap.fst ℝ ℝ ℝ) (s₃, y₃) - + s₁ * s₂ * s₃ * ((2 * ((1 : ℝ), (0 : ℝ)).1 * ((1 : ℝ), (0 : ℝ)).1) • + ContinuousLinearMap.fst ℝ ℝ ℝ) (1, 0) = 0 := by + simp + ring + rw [h0, abs_zero] + have a1 : |s₁| ≤ |s₁| + ‖y₁‖ := le_add_of_nonneg_right (norm_nonneg _) + have a2 : |s₂| ≤ |s₂| + ‖y₂‖ := le_add_of_nonneg_right (norm_nonneg _) + have a3 : |s₃| ≤ |s₃| + ‖y₃‖ := le_add_of_nonneg_right (norm_nonneg _) + have := mul_le_mul (mul_le_mul a1 a2 (abs_nonneg _) (by positivity)) a3 (abs_nonneg _) + (by positivity) + linarith + have hsrc := ridge_capHyp_C3 (E := ℝ) (f := h1ToyF) + (Df := fun p => (p.1 ^ 2 - 1 / 4) • ContinuousLinearMap.fst ℝ ℝ ℝ + + (-40 * p.2) • ContinuousLinearMap.snd ℝ ℝ ℝ) + (D2f := fun p => ((2 * p.1) • ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight + (ContinuousLinearMap.fst ℝ ℝ ℝ) + + ((-40 : ℝ) • ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight (ContinuousLinearMap.snd ℝ ℝ ℝ)) + (T3 := fun _ a b => (2 * a.1 * b.1) • ContinuousLinearMap.fst ℝ ℝ ℝ) + (DG := fun _ => ((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ) ∘L ContinuousLinearMap.snd ℝ ℝ ℝ) + (H := fun _ => (-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ) (Hx := fun _ => 0) + (Hr := fun _ _ => 0) (r := 1) (m := 2) (lam := 40) (ε := 1 / 2) one_pos (by norm_num) + (by norm_num) (fun p _ => hDf p) (fun p _ => hD2 p) (fun p _ a b => hD3 p a b) + (fun p _ => hT p) (fun p _ => by norm_num) (fun p _ => hGs p) (fun p _ => hH p) + (fun x _ => hasDerivAt_const x ((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ)) + (fun x _ => by simp only [ContinuousLinearMap.opNorm_zero]; norm_num) + (fun p _ s _ => hasDerivAt_const s ((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ)) + (fun p _ s _ => by simp only [ContinuousLinearMap.opNorm_zero]; positivity) + (fun v => by + simp only [smul_apply, ContinuousLinearMap.mul_apply', smul_eq_mul, Real.norm_eq_abs, sq_abs] + nlinarith [sq_nonneg v]) + (by norm_num) (by ext <;> norm_num) (by ext <;> norm_num) ?_ ?_ ?_ ?_ + (by simp only [h1ToyF]; norm_num) + · obtain ⟨hex, hcap⟩ := hsrc + have hcrit0 : ∀ x : ℝ, HasFDerivAt (fun y => h1ToyF (x, y)) (0 : ℝ →L[ℝ] ℝ) 0 := by + intro x + have := slice_hasFDerivAt (hDf (x, 0)) + convert this using 1 + ext + simp + obtain ⟨-, -, hC, -⟩ := hcap (fun _ => 0) (fun x _ => ⟨by simp, hcrit0 x⟩) + exact ⟨hex, hC⟩ + · have hc : ConvexOn ℝ univ (fun x : ℝ => (2 : ℝ) • x ^ 2 + (-1 / 4 : ℝ)) := + ((even_two.convexOn_pow).smul (by norm_num)).add (convexOn_const _ convex_univ) + refine (hc.subset (subset_univ _) (convex_Icc _ _)).congr ?_ + intro x _ + simp only [smul_eq_mul] + simp + ring + · refine (concaveOn_const (-1 / 4 : ℝ) (convex_Icc _ _)).congr ?_ + intro x _ + simp + ring + · intro v + have hc : ConvexOn ℝ univ (fun t : ℝ => ‖v‖ • t ^ 2) := + (even_two.convexOn_pow).smul (norm_nonneg v) + refine (hc.subset (subset_univ _) (convex_Icc _ _)).congr ?_ + intro t _ + simp only [smul_eq_mul] + simp + · intro v + have hc : ConcaveOn ℝ univ (fun t : ℝ => -(‖v‖ • t ^ 2)) := + ((even_two.convexOn_pow).smul (norm_nonneg v)).neg + refine (hc.subset (subset_univ _) (convex_Icc _ _)).congr ?_ + intro t _ + simp only [smul_eq_mul] + simp + end CapFirstExit diff --git a/frontiers/cap_first_exit_lean_20261002/MANIFEST.json b/frontiers/cap_first_exit_lean_20261002/MANIFEST.json index 22694a48a..f025648bd 100644 --- a/frontiers/cap_first_exit_lean_20261002/MANIFEST.json +++ b/frontiers/cap_first_exit_lean_20261002/MANIFEST.json @@ -101,6 +101,20 @@ "CapFirstExit.transverse_hessian_le_D", "CapFirstExit.slices_strongConcave_D", "CapFirstExit.ridge_capHyp_source", + "CapFirstExit.convex_deriv_sign", + "CapFirstExit.two_node_deriv_bound", + "CapFirstExit.slice_gradient_deriv_bound", + "CapFirstExit.schur_max", + "CapFirstExit.trilinear_lower", + "CapFirstExit.l12_constants", + "CapFirstExit.transverse_hessian_eq", + "CapFirstExit.ridge_second_identity", + "CapFirstExit.ridge_hconv", + "CapFirstExit.dx_grad_increment", + "CapFirstExit.l9_arith", + "CapFirstExit.l12_lower", + "CapFirstExit.ridge_source_facts", + "CapFirstExit.ridge_capHyp_C3", "CapFirstExit.toyF", "CapFirstExit.toyRidge", "CapFirstExit.toy_ridge_ge", @@ -125,7 +139,8 @@ "CapFirstExit.h1ToyF", "CapFirstExit.h1Toy_capHyp", "CapFirstExit.h1Toy_ridge_differentiable", - "CapFirstExit.h1Toy_source" + "CapFirstExit.h1Toy_source", + "CapFirstExit.h1Toy_C3" ], "expected_axioms": { "CapFirstExit.path_meets_frontier": [ @@ -468,6 +483,76 @@ "Quot.sound", "propext" ], + "CapFirstExit.convex_deriv_sign": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.two_node_deriv_bound": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.slice_gradient_deriv_bound": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.schur_max": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.trilinear_lower": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.l12_constants": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.transverse_hessian_eq": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.ridge_second_identity": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.ridge_hconv": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.dx_grad_increment": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.l9_arith": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.l12_lower": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.ridge_source_facts": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.ridge_capHyp_C3": [ + "Classical.choice", + "Quot.sound", + "propext" + ], "CapFirstExit.toyF": [ "Classical.choice", "Quot.sound", @@ -592,6 +677,11 @@ "Classical.choice", "Quot.sound", "propext" + ], + "CapFirstExit.h1Toy_C3": [ + "Classical.choice", + "Quot.sound", + "propext" ] }, "files": [ @@ -602,18 +692,18 @@ }, { "path": "ALIGNMENT.md", - "bytes": 30447, - "sha256": "56e26e4df8a971f079df05228fb252b0dcacf2fab605bcc5991312ce60ef2196" + "bytes": 36191, + "sha256": "207ed65f5aadcebf134eee6e6fa73232250530feb6026fdcd98e0013a2606265" }, { "path": "CapFirstExit.lean", - "bytes": 132854, - "sha256": "c68114a718bff7736dadad0f0d96eeba468cea0819f7dfb81729fbf0d4ca80ff" + "bytes": 184692, + "sha256": "668c9a40be828f319a612616e8613559903ebb47eaeeab9b514c819fc111c6f8" }, { "path": "README.md", - "bytes": 16494, - "sha256": "5b52fd6160139a30944faf6e0da1eb44772f2b623888331ebc618111320b6f15" + "bytes": 19226, + "sha256": "12fa296202a7593bcf5bacfb17cd795c28999f3dcabc83981a866a0c14f814ef" }, { "path": "gate.py", @@ -637,8 +727,8 @@ }, { "path": "test_gate.py", - "bytes": 6274, - "sha256": "000fe2c5c1daf29a2de30bf0522e737426b5b6eb623e5ad619b82fce93714d3c" + "bytes": 6275, + "sha256": "de4cbcad950d42d4b0fd87c4556929a518504af5e82c1806bec80780b6b7b1b8" } ] } diff --git a/frontiers/cap_first_exit_lean_20261002/README.md b/frontiers/cap_first_exit_lean_20261002/README.md index 3691b0423..1642e8f0f 100644 --- a/frontiers/cap_first_exit_lean_20261002/README.md +++ b/frontiers/cap_first_exit_lean_20261002/README.md @@ -38,7 +38,12 @@ Since v1.8, `ridge_capHyp_source` composes these steps from SP's source data on - L8's interior bound, and the implicit-function regularity of `h` on `[−2r, 2r]`; - L11, and then (C1)–(C3) and (C2⁺) on the cap. -The estimates L6 and L9–L12 (which give `hconv`) remain hypotheses. +Since v1.9, `ridge_capHyp_C3` also derives L12's `hconv`, from the second and third derivatives of `f` on the collar: +- L6: chord slopes of L5's convexity pair give `‖w'‖ ≤ m · max(|x|, r/2) ≤ 2mr`. +- L9: the differentiated ridge equation gives `‖h'‖ ≤ 2s + 2s²`, with `s = mr/δ`. +- L12: `F' = D²f[(1, h'), (1, 0)]` is the maximum of `ζ ↦ D²f[(1, ζ), (1, ζ)]`, so `F' − x/4` is monotone with no second derivative of `h`. With SP's constants, `F'' ≥ 7/4 − 48/121 · (3 + 72/121 + 576/14641) > 1/4`. + +What remains an input is `f_xxx ≥ 7/4` on `D = [−2r, 2r] × B̄(0, 2r)` (SP's L4, from L2 and (H2), on SP's own domain), together with the source data. In the topological theorems, `X` is any topological space, and nothing is assumed about `f` outside `C` except along the single ridge path. @@ -85,6 +90,13 @@ single ridge path. | `hessian_increment_D`, `transverse_hessian_le_D`, `slices_strongConcave_D` | L3–L4 on a collar of SP's `D`: on the collar `x ∈ [−2r − ε, 2r + ε]`, `0 < ε ≤ r/2`, the increment is at most `3r + 2r = 5r` (SP: `9r/2 < 5r` on `D`), so every slice is `(λ − 5rm)`-strongly concave | | `ridge_capHyp_source` | the composed source route (v1.8). From the source data on the collar it proves that a ridge exists on `(−2r − ε, 2r + ε)`. For any such ridge with L12's `hconv`, it proves `h(∓r/2) = 0` and the cap with `M = (−r/2, 0)` and `S = (r/2, 0)`. Inside: L5 gives `‖w‖ ≤ 3mr² < 2rδ`, L8 gives the open ball, `DG ∘ inr = H` is negative definite, the IFT gives `h'`, and then L11 and `ridge_capHyp_H1` follow | | `h1Toy_source` | `h1ToyF` meets every hypothesis of `ridge_capHyp_source` (`ε = 1/2`, joint derivative `(x² − 1/4, −40y)`); the theorem gives its ridge and its cap | +| `convex_deriv_sign`, `two_node_deriv_bound`, `slice_gradient_deriv_bound` | L6 (v1.9). If `u` vanishes at `∓r/2` and `|u''| ≤ m` holds in the weak form, then `|u'(x)| ≤ m · max(|x|, r/2)`. Outside the pins the chord through them has slope `0`; between them the chord to a pin and L5 give `mr/2`. For the slice derivatives at `y = 0` this is SP's `‖w'‖ ≤ 2mr` on `[−2r, 2r]` | +| `schur_max` | L9 and the Schur maximum. Take a bilinear `Q` on `ℝ × E` with `δ`-negative-definite transverse part, and `η` with `Q (1, η) (0, ·) = 0`. Then `δ‖η‖ ≤ ‖Q (1, 0) (0, ·)‖`, and `Q (1, η) (1, η) = Q (1, η) (1, 0)`. If `Q` is symmetric, `Q (1, ζ) (1, ζ) ≤ Q (1, η) (1, η)` for every `ζ` | +| `ridge_second_identity`, `transverse_hessian_eq` | the differentiated ridge equation `D²f[(1, h'), (0, ·)] = 0` (L11's first identity), and `H = D²f[(0, ·), (0, ·)]` | +| `trilinear_lower`, `l12_lower`, `l12_constants`, `l9_arith`, `dx_grad_increment` | L12's correction terms, `f_xxx − m((1 + ‖b‖)²(1 + ‖a‖) − 1)`. SP's constants: `m ≥ 2` and `δ > rm(8m − 5)` give `7/4 − m((1 + u)³ − 1) ≥ 1/4` for `u = 2s + 2s²`. Also L9's arithmetic, and L3 in `y` for `∂_x ∇_y f` | +| `ridge_hconv` | L12 as `hconv`. Along the ridge, assume `D²f` is symmetric with negative-definite transverse part, `‖h'‖ ≤ u`, and `s ↦ D²f(s, h s)[(1, b), (1, b)]` has derivative `≥ 1/4` for `‖b‖ ≤ u`. Then `F − (x + r/2)(x − r/2)/8` is convex on `[−2r, 2r]`. For `η = h'(x₁)`: `F'(x₂) − F'(x₁) ≥ D²f(x₂)[(1, η), (1, η)] − D²f(x₁)[(1, η), (1, η)] ≥ (x₂ − x₁)/4` | +| `ridge_source_facts`, `ridge_capHyp_C3` | the cap from SP's `C³` source data (v1.9). It assumes `ridge_capHyp_source`'s data, `D²f` and the third derivatives on the collar, the block bound `m`, and `f_xxx ≥ 7/4` on `D`. It proves that a ridge exists, that `h(∓r/2) = 0`, and the cap with `M = (−r/2, 0)`, deriving L12's `hconv` rather than assuming it | +| `h1Toy_C3` | `h1ToyF` meets every hypothesis of `ridge_capHyp_C3`: `D²f = diag(2x, −40)`, and only `f_xxx = 2` is nonzero among the third derivatives. The theorem gives its ridge and its cap without a supplied `hconv` | | `sp_curved_side_constants` | SP's constants (`m ≥ 2`, `δ > rm(8m − 5)`, `ω ≤ 2mr²`, gap `r³/6`) satisfy `ω ≤ 2rδ` and the curvature condition | | `ridgeToy_joint`, `ridgeToy_slices` | the ridge toy (`δ = 2`, `ω = 0`) meets every input of the slice route, which re-derives (C1)–(C3) and (C2⁺) | | `ridgeToy_capHyp`, `ridgeToy_saddle_strict` | SP's normalization at `r = 1` (`f = x³/3 − x/4 − y²`, gap exactly `r³/6`) satisfies every ridge hypothesis, so they are jointly satisfiable | @@ -107,13 +119,12 @@ that step. This packet does not formalize: -- the analytic steps L6 (the `w'` bound) and L9–L12 (the `‖h'‖` and `F''` bounds), which give `hconv`. Since v1.7, the - existence and implicit-function regularity of the ridge `h` are proved (`ridge_exists`, `ridge_differentiable`). - The remaining inputs enter `ridge_capHyp_H1`, `ridge_capHyp_of_slices` and - `ridge_inputs_of_joint` as hypotheses, together with the Hessian data and the third-derivative bounds `m` that L1, - L3 and L5 consume. L1–L5, L7's maximum and uniqueness, L8, L11's chain rule, L13 and L16–L20 are proved from them; -- the source data themselves. `ridge_capHyp_source` takes, as hypotheses, the derivatives `Df`, `DG` and `H` and the - third-derivative bounds `m` on the collar `[−2r − ε, 2r + ε] × B̄(0, 2r)`. SP has `f ∈ C⁴` near `D` and bounds the +- SP's L4 bound `f_xxx ≥ 7/4` on `D`, which SP derives from L2's second statement (some point has `f_xxx = 2`) and + (H2) `rn ≤ 1/20` with the fourth-derivative bound `n`. It is a hypothesis of `ridge_capHyp_C3`. Since v1.9, L6 and + L9–L12 are proved (`ridge_hconv`, `ridge_capHyp_C3`), and so are L1–L5, L7 (existence, uniqueness and regularity of + `h`), L8, L11, L13 and L16–L20; +- the source data themselves. `ridge_capHyp_source` and `ridge_capHyp_C3` take, as hypotheses, the derivatives `Df`, + `DG`, `H`, `D2f` and the third derivatives, with the bounds `m`, on the collar `[−2r − ε, 2r + ε] × B̄(0, 2r)`. SP has `f ∈ C⁴` near `D` and bounds the third derivatives on `D`. On a thin enough collar the bound `m + η` holds by continuity, and (H1) stays strict for small `η`; Lean does not prove this step; - the match between the source's coordinates and the Lean objects: that SP's cap is `[-2r, r/2] × B̄(0, 2r)` in a @@ -154,7 +165,7 @@ The source gate checks: bound); - rebuilds the package fresh; - replays the module with `leanchecker`; -- prints the axioms of all 93 declarations, requiring exactly the manifest's report: each uses only `propext`, +- prints the axioms of all 108 declarations, requiring exactly the manifest's report: each uses only `propext`, `Classical.choice`, `Quot.sound`; - runs three negative controls (an injected `sorry`, a custom axiom, and `native_decide`). The audit must reject each. diff --git a/frontiers/cap_first_exit_lean_20261002/test_gate.py b/frontiers/cap_first_exit_lean_20261002/test_gate.py index 53706a426..44426c56f 100644 --- a/frontiers/cap_first_exit_lean_20261002/test_gate.py +++ b/frontiers/cap_first_exit_lean_20261002/test_gate.py @@ -16,7 +16,7 @@ class SourceGate(unittest.TestCase): def test_tree_passes(self): m = gate.source_check() - self.assertEqual(len(m["targets"]), 93) + self.assertEqual(len(m["targets"]), 108) self.assertEqual(m['scientific_effect'], 'NONE') def copy(self):