diff --git a/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md b/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md index 9827bc03e..d7d7e401b 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`). Since v1.9, L6 and L9–L12 are proved and `ridge_capHyp_C3` derives `hconv` from the `C³` data. Since v2.0, L2's second statement and L4's `f_xxx ≥ 7/4` are proved from (H2) (`ridge_capHyp_C4`). Inputs that remain: 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. Since v2.0, L2's second statement and L4's `f_xxx ≥ 7/4` are proved from (H2) (`ridge_capHyp_C4`). Since v2.1, the six derivative-bound hypotheses are derived from the block bound and `|f_xxx| ≤ m` on the pin segment (`ridge_capHyp_C5`), and the quantitative bounds are assumed on `D` only, with the continuity step to the collar proved (`ridge_capHyp_D`). Inputs that remain: 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: @@ -92,6 +92,12 @@ The source setting (SP §2) is as follows: | `third_deriv_exists_two` | `g' = G`, `G' = G'`, `G'' = φ` continuous on `[−r/2, r/2]`, critical pins, gap `r³/6` ⇒ `∃ x₀ ∈ [−r/2, r/2], φ(x₀) ≥ 2` | SP L2, second statement ("by continuity some `x_0` has `f_xxx(x_0, 0) = 2`") | By contradiction. The maximum `M' < 2` of `φ` makes `G − (M'/2)t²` concave, and then the gap is `≤ M'r³/12 < r³/6`. Lean proves `≥ 2`, which is all L4 needs. | | `fxxx_lower` | `ψ` with derivative `Dψ` on `D = [−2r, 2r] × B̄(0, 2r)`, `|Dψ (1, 0)| ≤ n` and `‖Dψ ∘ inr‖ ≤ n` there, `ψ(x₀, 0) ≥ 2` with `x₀` in the pin interval, `rn ≤ 1/20` ⇒ `ψ ≥ 7/4` on `D` (the proof bounds `ψ ≥ 2 − 9rn/2`, and the statement exports `7/4`) | SP L4 ("`f_xxx ≥ 2 − 5rn ≥ 2 − 1/4 = 7/4` on `D`"), via L3's "moving first in `x` then in `y`" | `n` bounds the two fourth-order blocks `∂_x f_xxx` and `D_y f_xxx` separately, which is SP's `M₄`, on `D` only (Codex 4175200307: with the max product norm, block bounds `n` give only `‖Dψ‖ ≤ 2n`). The path `(x₀, 0) → (x, 0) → (x, y)` stays in `D`, with `|Δx| ≤ 5r/2` and `‖Δy‖ ≤ 2r`. | | `ridge_capHyp_C4` | `ridge_capHyp_C3`'s hypotheses with `f_xxx ≥ 7/4` on `D` replaced by: `Φ4 p` the derivative of `p ↦ f_xxx(p)` on `D`, with `|Φ4 (1, 0)| ≤ n` and `‖Φ4 ∘ inr‖ ≤ n` there, and (H2) `rn ≤ 1/20` ⇒ the same conclusion | SP §2 normalization, (H1), (H2), L1–L20 | The cap from SP's hypotheses, with no analytic step assumed. The fourth-order data enter only through `f_xxx`'s two blocks on `D`, which is all that SP uses of `M₄`. | +| `hessian_x_bound` | `y ↦ ∂_y f(t, y)` with derivative `H(t, 0)` at `0`, `Df` with derivative `D2f(t, 0)` at `(t, 0)` for `t ∈ J`, `J` uniquely differentiable at `x ∈ J`, `T3(x, 0)` the derivative of `D2f(·) a b` at `(x, 0)`, `|T3(x, 0)[(0, v), (0, w), (1, 0)]| ≤ m‖v‖‖w‖`, `t ↦ H(t, 0)` with derivative `Hx'` at `x` ⇒ `‖Hx'‖ ≤ m` | SP L3 ("`‖∂_x D_y² f‖ ≤ M₃`") | The proof identifies `Hx' v w` with the `T3` block by uniqueness of derivatives within `J` (`transverse_hessian_eq` on `J`). So collar endpoints are allowed. | +| `hessian_r_bound` | the same along the radius `τ ↦ (x, τy)`, `τ ∈ [0, 1]`: `|T3(x, sy)[(0, v), (0, w), (0, y)]| ≤ m‖v‖‖w‖‖y‖`, `τ ↦ H(x, τy)` with derivative `Hr'` at `s` ⇒ `‖Hr'‖ ≤ m‖y‖` | SP L3 ("`‖D_y³ f‖ ≤ M₃`" along rays) | Derivatives are taken within `[0, 1]`, so `‖y‖ = 2r` is allowed. | +| `axis_convexConcave` | `Df` with derivative `D2f(t, 0)` and `D2f(·)(1, 0) u` with derivative `T3(t, 0)(1, 0) u` at `(t, 0)`, `|T3(t, 0)[(1, 0), u, (1, 0)]| ≤ B` on `[a, c]` ⇒ `Df(·, 0) u + (B/2)t²` convex and `Df(·, 0) u − (B/2)t²` concave on `[a, c]` | SP L1 (`|g_0'''| ≤ m`), L5–L6 (`‖w''‖ ≤ m`) | `u = (0, v)`, `B = m‖v‖` gives `hwcv`, `hwcc`. `u = (1, 0)`, `B = m` gives `hG0cv`, `hG0cc` (SP: `|f_xxx| ≤ M₃`). | +| `block_nonneg`, `block_bound_collar` | `K ≥ 0`, `0 ≤ ε ≤ ε₀`; the block bound `m` on `D = [−2r, 2r] × B̄(0, 2r)`; on the collar of width `ε₀`, `T4 p a b c` the derivative of `t ↦ T3(t, p₂) a b c` at `p₁`, with the block bound `K` ⇒ the block bound `m + Kε` on the collar of width `ε` | I3's continuity step (SP bounds `M₃` on `D`; `f ∈ C⁴` near `D`) | Each collar point `(x, y)` is within `ε` of a point `(x₀, y) ∈ D`. The mean value inequality along `x` on the convex interval of width `ε₀` adds at most `Kε` times the block weight. | +| `ridge_capHyp_C5` | `ridge_capHyp_C4`'s hypotheses without `hHxb`, `hHrb`, `hG0cv`, `hG0cc`, `hwcv`, `hwcc`, and with `|T3(x, 0)[(1, 0), (1, 0), (1, 0)]| ≤ m` on the pin segment ⇒ the same conclusion | SP §2, L1–L20 | The six hypotheses are derived: `hHxb`, `hHrb` by the first two rows; `hwcv`, `hwcc` from the block bound by `axis_convexConcave`; `hG0cv`, `hG0cc` from the pin-segment bound. | +| `ridge_capHyp_D` | `0 < ε₀`, `K ≥ 0`; on the collar of width `ε₀`: `Df`, `D2f`, `T3`, `T4` (as above) with the block bound `K`, `DG` (strict), `H`, `Hx`, `Hr`; on `D`: the block bound `m`, `Φ4` with its two blocks `≤ n`; `|f_xxx| ≤ m` on the pin segment; (H1) `8rm² < λ`, (H2) `rn ≤ 1/20`; critical pins; gap `r³/6` ⇒ `∃ ε ∈ (0, ε₀]` with `ridge_capHyp_C4`'s conclusion on `(−2r − ε, 2r + ε)` | SP §2 (H1), (H2), `M₃`, `M₄` on `D`, `f ∈ C⁴` near `D`; L1–L20 | Since (H1) is strict, `ε` is chosen with `8r(m + Kε)² < λ`, `ε ≤ ε₀` and `ε ≤ r/2`, and `ridge_capHyp_C5` is applied with `m + Kε`. `K` is any finite bound, which SP's `C⁴` gives on a compact collar. | | `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. | @@ -124,7 +130,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)`. `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. `h1Toy_C4` (v2.0) meets every hypothesis of `ridge_capHyp_C4`, with `f_xxx = 2` constant, so `Φ4 = 0`, both blocks vanish and (H2) holds with `n = 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. `h1Toy_C4` (v2.0) meets every hypothesis of `ridge_capHyp_C4`, with `f_xxx = 2` constant, so `Φ4 = 0`, both blocks vanish and (H2) holds with `n = 0`. `h1Toy_D` (v2.1) meets every hypothesis of `ridge_capHyp_D` with `ε₀ = 1/2`: `T3` is constant, so `T4 = 0` and `K = 0`, and `|f_xxx| = 2 = m` on the pin segment. The theorem chooses `ε` itself and yields a ridge on `(−2 − ε, 2 + ε)` and the cap. 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 @@ -139,7 +145,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; 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. No analytic step of L1–L20 is assumed: of SP's steps L1–L12, the last input, L4's `f_xxx ≥ 7/4` on `D`, is proved since v2.0 (`ridge_capHyp_C4`, from L2's second statement and (H2)). 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 the block bound `hT` excludes `f_xxx`; the convexity pair for `w`; the L3 bounds `Hx`, `Hr`; (H1); the pins; and `DG`. On `D`: SP's block bound `n` on the derivative of `f_xxx`, with (H2). | SP §2 (H1), L6, L7, L9–L12; CAP §§2–5 | These are checked with exact constants by SP's script. Since v2.0, Lean also proves L2's second statement and L4's `f_xxx ≥ 7/4` from (H2) (`ridge_capHyp_C4`). Since v1.9, Lean proves L6, L9 and L12 with SP's constants and derives `hconv` (`ridge_capHyp_C3`). 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`); since v2.1 these pairs and L3's bounds on `∂_x D_y² f` and `D_y³ f` are derived from the block bound and `|f_xxx| ≤ m` on the pin segment (`ridge_capHyp_C5`); 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`. Since v2.1 Lean proves the continuity step (`block_bound_collar`, `ridge_capHyp_D`). With the block bound `m` on `D`, and some bound `K` on the `x`-derivative of the third derivatives on a collar of width `ε₀`, the bound `m + Kε` holds on the collar of width `ε`, and (H1) stays strict for small `ε`. What stays informal is that `f ∈ C⁴` near `D` supplies the derivative data and some `K`, by compactness of a closed collar. No analytic step of L1–L20 is assumed: of SP's steps L1–L12, the last input, L4's `f_xxx ≥ 7/4` on `D`, is proved since v2.0 (`ridge_capHyp_C4`, from L2's second statement and (H2)). The source data listed in this row stay hypotheses. Since v2.1 (`ridge_capHyp_D`) the quantitative ones are needed on `D` only: the block bound `m`; `|f_xxx| ≤ m` on the pin segment, which the block bound `hT` excludes; SP's block bound `n` on the derivative of `f_xxx`; (H1) and (H2); and, as exact conditions at points of `D`, the critical pins and the gap `r³/6`. On a collar of width `ε₀`, only qualitative data are assumed: `Df`, `D2f`, `T3` and its `x`-derivative with some bound `K`, `DG` (strict), `H`, `Hx` and `Hr`. | SP §2 (H1), L6, L7, L9–L12; CAP §§2–5 | These are checked with exact constants by SP's script. Since v2.1, Lean derives the six derivative bounds from the block bound and `|f_xxx| ≤ m` on the pin segment, and proves the continuity step from `D` to the collar (`ridge_capHyp_C5`, `ridge_capHyp_D`). Since v2.0, Lean also proves L2's second statement and L4's `f_xxx ≥ 7/4` from (H2) (`ridge_capHyp_C4`). Since v1.9, Lean proves L6, L9 and L12 with SP's constants and derives `hconv` (`ridge_capHyp_C3`). 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 @@ -156,5 +162,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. 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. v2.0 adds four §2 rows (`hermite_gap_le_concave` to `ridge_capHyp_C4`), the `h1Toy_C4` sentence of §3 and a further revision of the SP row and I3; its 108 v1.9 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. v2.0 adds four §2 rows (`hermite_gap_le_concave` to `ridge_capHyp_C4`), the `h1Toy_C4` sentence of §3 and a further revision of the SP row and I3; its 108 v1.9 declarations are unchanged. v2.1 adds six §2 rows (`hessian_x_bound` to `ridge_capHyp_D`, seven theorems), the `h1Toy_D` sentence of §3 and a further revision of the SP row and I3; its 113 v2.0 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 349277946..9ffef7878 100644 --- a/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean +++ b/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean @@ -23,7 +23,9 @@ `ridge_capHyp_source` composes them from source data on a collar `[-2r - ε, 2r + ε]` of `D` (the source data themselves are hypotheses). Since v1.9, L6 and L9–L12 are proved too, and `ridge_capHyp_C3` derives `hconv`; since v2.0 `ridge_capHyp_C4` also derives SP's - `f_xxx ≥ 7/4` (L4, from L2's second statement and (H2)). + `f_xxx ≥ 7/4` (L4, from L2's second statement and (H2)). Since v2.1 `ridge_capHyp_C5` derives + the six derivative bounds from the block bound, and `ridge_capHyp_D` assumes SP's quantitative + bounds on `D` only (the continuity step to the collar is proved). 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. @@ -2628,6 +2630,385 @@ theorem ridge_capHyp_C4 [FiniteDimensional ℝ E] {f : ℝ × E → ℝ} exact ridge_capHyp_C3 hr hε hεr hDf hD2 hD3 hT hxxx hGs hH hHx hHxb hHr hHrb hlam hH1 hM hS hG0cv hG0cc hwcv hwcc hnorm + +/-! ### The derivative bounds from the block bound, and SP's bounds on `D` (v2.1) + +Up to v2.0 the capstones took six derivative bounds besides the block bound `hT`: +- `hHxb` and `hHrb`, the inputs of L3; +- `hwcv` and `hwcc`, the envelope inputs of L5–L6; +- `hG0cv` and `hG0cc`, the envelope inputs of L1–L2. + +All six follow from `hT` and from `|f_xxx| ≤ m` on the pin segment, and `ridge_capHyp_C5` derives +them. Up to v2.0 the bounds `m` were also assumed on a collar `[−2r − ε, 2r + ε]` of SP's `D`. +`ridge_capHyp_D` assumes them on `D` only, through the continuity step `block_bound_collar` (I3). -/ + +/-- **L3's `x`-input from the block bound.** Let `y ↦ ∂_y f (t, y)` have derivative `H (t, 0)` at `0` +and `Df` have derivative `D2f (t, 0)` at `(t, 0)` for every `t ∈ J`, where `J` is uniquely +differentiable at `x ∈ J`. If `t ↦ H (t, 0)` has derivative `Hx'` at `x`, then +`Hx' v w = T3 (x, 0) [(0, v), (0, w), (1, 0)]`, so `‖Hx'‖ ≤ m` when that block is at most +`m ‖v‖ ‖w‖`. This derives v1.6's hypothesis `hHxb`. -/ +theorem hessian_x_bound {Df : ℝ × E → ℝ × E →L[ℝ] ℝ} {D2f : ℝ × E → ℝ × E →L[ℝ] ℝ × E →L[ℝ] ℝ} + {T3 : ℝ × E → ℝ × E → ℝ × E → ℝ × E →L[ℝ] ℝ} + {H : ℝ × E → E →L[ℝ] E →L[ℝ] ℝ} {Hx' : E →L[ℝ] E →L[ℝ] ℝ} {J : Set ℝ} {m x : ℝ} + (hJ : UniqueDiffWithinAt ℝ J x) (hxJ : x ∈ J) (hm : 0 ≤ m) + (hH : ∀ t ∈ J, HasFDerivAt (fun y => (Df (t, y)).comp (ContinuousLinearMap.inr ℝ ℝ E)) + (H (t, 0)) 0) + (hD2 : ∀ t ∈ J, HasFDerivAt Df (D2f (t, 0)) (t, 0)) + (hD3 : ∀ a b : ℝ × E, HasFDerivAt (fun q => D2f q a b) (T3 (x, 0) a b) (x, 0)) + (hT : ∀ v w : E, |T3 (x, 0) (0, v) (0, w) (1, 0)| ≤ m * (‖v‖ * ‖w‖)) + (hHx : HasDerivAt (fun t => H (t, 0)) Hx' x) : ‖Hx'‖ ≤ m := by + have hp : HasDerivAt (fun t : ℝ => (t, (0 : E))) ((1 : ℝ), (0 : E)) x := + (hasDerivAt_id x).prodMk (hasDerivAt_const x (0 : E)) + have key : ∀ v w : E, Hx' v w = T3 (x, 0) (0, v) (0, w) (1, 0) := by + intro v w + have h1 : HasDerivAt (fun t => H (t, 0) v w) (Hx' v w) x := by + have := (hHx.clm_apply (hasDerivAt_const x v)).clm_apply (hasDerivAt_const x w) + simpa using this + have h2 : HasDerivAt (fun t => D2f (t, 0) (0, v) (0, w)) (T3 (x, 0) (0, v) (0, w) (1, 0)) x := + HasFDerivAt.comp_hasDerivAt (l := fun q => D2f q (0, v) (0, w)) x (hD3 (0, v) (0, w)) hp + have h3 : HasDerivWithinAt (fun t => D2f (t, 0) (0, v) (0, w)) (Hx' v w) J x := + h1.hasDerivWithinAt.congr_of_mem (fun t ht => (transverse_hessian_eq (hH t ht) (hD2 t ht) v w).symm) hxJ + exact hJ.eq_deriv _ h3 h2.hasDerivWithinAt + refine ContinuousLinearMap.opNorm_le_bound _ hm fun v => ?_ + refine ContinuousLinearMap.opNorm_le_bound _ (mul_nonneg hm (norm_nonneg v)) fun w => ?_ + rw [key, Real.norm_eq_abs, mul_assoc] + exact hT v w + +/-- **L3's radial input from the block bound.** Along the radius `τ ↦ (x, τ y)`, `τ ∈ [0, 1]`, if +`τ ↦ H (x, τ y)` has derivative `Hr'` at `s`, then `Hr' v w = T3 (x, s y) [(0, v), (0, w), (0, y)]`, +so `‖Hr'‖ ≤ m ‖y‖` when that block is at most `m ‖v‖ ‖w‖ ‖y‖`. The identification uses derivatives +within `[0, 1]`, so the endpoint `τ = 1` may lie on the sphere `‖y‖ = 2r`. This derives v1.6's +hypothesis `hHrb`. -/ +theorem hessian_r_bound {Df : ℝ × E → ℝ × E →L[ℝ] ℝ} {D2f : ℝ × E → ℝ × E →L[ℝ] ℝ × E →L[ℝ] ℝ} + {T3 : ℝ × E → ℝ × E → ℝ × E → ℝ × E →L[ℝ] ℝ} + {H : ℝ × E → E →L[ℝ] E →L[ℝ] ℝ} {Hr' : E →L[ℝ] E →L[ℝ] ℝ} {x m s : ℝ} {y : E} + (hm : 0 ≤ m) (hs : s ∈ Icc (0 : ℝ) 1) + (hH : ∀ τ ∈ Icc (0 : ℝ) 1, HasFDerivAt (fun z => (Df (x, z)).comp (ContinuousLinearMap.inr ℝ ℝ E)) + (H (x, τ • y)) (τ • y)) + (hD2 : ∀ τ ∈ Icc (0 : ℝ) 1, HasFDerivAt Df (D2f (x, τ • y)) (x, τ • y)) + (hD3 : ∀ a b : ℝ × E, HasFDerivAt (fun q => D2f q a b) (T3 (x, s • y) a b) (x, s • y)) + (hT : ∀ v w : E, |T3 (x, s • y) (0, v) (0, w) (0, y)| ≤ m * (‖v‖ * ‖w‖ * ‖y‖)) + (hHr : HasDerivAt (fun τ : ℝ => H (x, τ • y)) Hr' s) : ‖Hr'‖ ≤ m * ‖y‖ := by + have hp : HasDerivAt (fun τ : ℝ => (x, τ • y)) ((0 : ℝ), y) s := by + have := (hasDerivAt_const s x).prodMk ((hasDerivAt_id s).smul_const y) + simpa using this + have key : ∀ v w : E, Hr' v w = T3 (x, s • y) (0, v) (0, w) (0, y) := by + intro v w + have h1 : HasDerivAt (fun τ => H (x, τ • y) v w) (Hr' v w) s := by + have := (hHr.clm_apply (hasDerivAt_const s v)).clm_apply (hasDerivAt_const s w) + simpa using this + have h2 : HasDerivAt (fun τ : ℝ => D2f (x, τ • y) (0, v) (0, w)) + (T3 (x, s • y) (0, v) (0, w) (0, y)) s := + HasFDerivAt.comp_hasDerivAt (l := fun q => D2f q (0, v) (0, w)) s (hD3 (0, v) (0, w)) hp + have h3 : HasDerivWithinAt (fun τ : ℝ => D2f (x, τ • y) (0, v) (0, w)) (Hr' v w) (Icc 0 1) s := + h1.hasDerivWithinAt.congr_of_mem + (fun τ hτ => (transverse_hessian_eq (hH τ hτ) (hD2 τ hτ) v w).symm) hs + exact (uniqueDiffOn_Icc zero_lt_one s hs).eq_deriv _ h3 h2.hasDerivWithinAt + have hmy : 0 ≤ m * ‖y‖ := mul_nonneg hm (norm_nonneg y) + refine ContinuousLinearMap.opNorm_le_bound _ hmy fun v => ?_ + refine ContinuousLinearMap.opNorm_le_bound _ (mul_nonneg hmy (norm_nonneg v)) fun w => ?_ + rw [key, Real.norm_eq_abs] + calc |T3 (x, s • y) (0, v) (0, w) (0, y)| ≤ m * (‖v‖ * ‖w‖ * ‖y‖) := hT v w + _ = m * ‖y‖ * ‖v‖ * ‖w‖ := by ring + +/-- **The envelope inputs of L1 and L5–L6 from a second-derivative bound.** If the second derivative +`T3 (t, 0) [(1, 0), u, (1, 0)]` of `t ↦ Df (t, 0) u` has absolute value at most `B` on `[a, c]`, then +`Df (·, 0) u + (B/2) t²` is convex and `Df (·, 0) u − (B/2) t²` is concave there. With `u = (0, v)` +and `B = m‖v‖` (from the block bound) this gives `hwcv` and `hwcc`. With `u = (1, 0)` and `B = m` +(SP: `|f_xxx| ≤ M₃`) it gives `hG0cv` and `hG0cc`. -/ +theorem axis_convexConcave {Df : ℝ × E → ℝ × E →L[ℝ] ℝ} + {D2f : ℝ × E → ℝ × E →L[ℝ] ℝ × E →L[ℝ] ℝ} + {T3 : ℝ × E → ℝ × E → ℝ × E → ℝ × E →L[ℝ] ℝ} {a c B : ℝ} {u : ℝ × E} + (hD2 : ∀ t ∈ Icc a c, HasFDerivAt Df (D2f (t, 0)) (t, 0)) + (hD3 : ∀ t ∈ Icc a c, HasFDerivAt (fun q => D2f q (1, 0) u) (T3 (t, 0) (1, 0) u) (t, 0)) + (hB : ∀ t ∈ Icc a c, |T3 (t, 0) (1, 0) u (1, 0)| ≤ B) : + ConvexOn ℝ (Icc a c) (fun t => Df (t, 0) u + B / 2 * t ^ 2) ∧ + ConcaveOn ℝ (Icc a c) (fun t => Df (t, 0) u - B / 2 * t ^ 2) := by + have hp : ∀ t : ℝ, HasDerivAt (fun s : ℝ => (s, (0 : E))) ((1 : ℝ), (0 : E)) t := fun t => + (hasDerivAt_id t).prodMk (hasDerivAt_const t (0 : E)) + have hg : ∀ t ∈ Icc a c, HasDerivAt (fun s => Df (s, 0) u) (D2f (t, 0) (1, 0) u) t := by + intro t ht + have h1 : HasDerivAt (fun s => Df (s, 0)) (D2f (t, 0) (1, 0)) t := + (hD2 t ht).comp_hasDerivAt t (hp t) + simpa using h1.clm_apply (hasDerivAt_const t u) + have hg' : ∀ t ∈ Icc a c, HasDerivAt (fun s => D2f (s, 0) (1, 0) u) (T3 (t, 0) (1, 0) u (1, 0)) t := + fun t ht => HasFDerivAt.comp_hasDerivAt (l := fun q => D2f q (1, 0) u) t (hD3 t ht) (hp t) + have hcont : ContinuousOn (fun s => Df (s, 0) u) (Icc a c) := + fun t ht => (hg t ht).continuousAt.continuousWithinAt + have hsq : ∀ t : ℝ, HasDerivAt (fun s : ℝ => B / 2 * s ^ 2) (B * t) t := by + intro t + have := (hasDerivAt_pow 2 t).const_mul (B / 2) + convert this using 1 + ring + have hlin : ∀ t : ℝ, HasDerivAt (fun s : ℝ => B * s) B t := by + intro t + simpa using (hasDerivAt_id t).const_mul B + have hIo : ∀ t ∈ interior (Icc a c), t ∈ Icc a c := fun t ht => interior_subset ht + constructor + · refine convexOn_of_hasDerivWithinAt2_nonneg (convex_Icc a c) + (f' := fun t => D2f (t, 0) (1, 0) u + B * t) (f'' := fun t => T3 (t, 0) (1, 0) u (1, 0) + B) + (hcont.add (continuousOn_const.mul (continuousOn_id.pow 2))) ?_ ?_ ?_ + · intro t ht + exact ((hg t (hIo t ht)).add (hsq t)).hasDerivWithinAt + · intro t ht + exact ((hg' t (hIo t ht)).add (hlin t)).hasDerivWithinAt + · intro t ht + have := hB t (hIo t ht) + have := neg_abs_le (T3 (t, 0) (1, 0) u (1, 0)) + show 0 ≤ T3 (t, 0) (1, 0) u (1, 0) + B + linarith + · refine concaveOn_of_hasDerivWithinAt2_nonpos (convex_Icc a c) + (f' := fun t => D2f (t, 0) (1, 0) u - B * t) (f'' := fun t => T3 (t, 0) (1, 0) u (1, 0) - B) + (hcont.sub (continuousOn_const.mul (continuousOn_id.pow 2))) ?_ ?_ ?_ + · intro t ht + exact ((hg t (hIo t ht)).sub (hsq t)).hasDerivWithinAt + · intro t ht + exact ((hg' t (hIo t ht)).sub (hlin t)).hasDerivWithinAt + · intro t ht + have := hB t (hIo t ht) + have := le_abs_self (T3 (t, 0) (1, 0) u (1, 0)) + show T3 (t, 0) (1, 0) u (1, 0) - B ≤ 0 + linarith + +/-- The block weight `∏ (|sᵢ| + ‖yᵢ‖) − ∏ |sᵢ|` is nonnegative. -/ +theorem block_nonneg {F : Type*} [SeminormedAddCommGroup F] (s₁ s₂ s₃ : ℝ) (y₁ y₂ y₃ : F) : + 0 ≤ (|s₁| + ‖y₁‖) * (|s₂| + ‖y₂‖) * (|s₃| + ‖y₃‖) - |s₁| * |s₂| * |s₃| := by + 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 + +/-- **The continuity step of I3: the block bound from `D` to a collar.** Assume the block bound holds +with `m` on SP's `D = [−2r, 2r] × B̄(0, 2r)`. Assume also that on the collar +`[−2r − ε₀, 2r + ε₀] × B̄(0, 2r)` the `x`-derivative `T4` of `T3` exists and satisfies the same block +bound with some `K ≥ 0` (SP: `f ∈ C⁴` near `D`, so `‖D⁴ f‖` is bounded on a compact collar). Then the +block bound holds with `m + Kε` on the collar of width `ε ≤ ε₀`. Each collar point `(x, y)` is +within `ε` of a point `(x₀, y) ∈ D`, and the mean value inequality along `x` gives the rest. -/ +theorem block_bound_collar {T3 : ℝ × E → ℝ × E → ℝ × E → ℝ × E →L[ℝ] ℝ} + {T4 : ℝ × E → ℝ × E → ℝ × E → ℝ × E → ℝ} {r m K ε₀ ε : ℝ} (hr : 0 < r) (hK : 0 ≤ K) + (hε : 0 ≤ ε) (hεε : ε ≤ ε₀) + (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₃|)) + (hD4x : ∀ p ∈ Icc (-2 * r - ε₀) (2 * r + ε₀) ×ˢ Metric.closedBall (0 : E) (2 * r), + ∀ a b c : ℝ × E, HasDerivAt (fun t => T3 (t, p.2) a b c) (T4 p a b c) p.1) + (hT4 : ∀ p ∈ Icc (-2 * r - ε₀) (2 * r + ε₀) ×ˢ Metric.closedBall (0 : E) (2 * r), + ∀ (s₁ s₂ s₃ : ℝ) (y₁ y₂ y₃ : E), + |T4 p (s₁, y₁) (s₂, y₂) (s₃, y₃) - s₁ * s₂ * s₃ * T4 p (1, 0) (1, 0) (1, 0)| ≤ + K * ((|s₁| + ‖y₁‖) * (|s₂| + ‖y₂‖) * (|s₃| + ‖y₃‖) - |s₁| * |s₂| * |s₃|)) : + ∀ 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 + K * ε) * ((|s₁| + ‖y₁‖) * (|s₂| + ‖y₂‖) * (|s₃| + ‖y₃‖) - |s₁| * |s₂| * |s₃|) := by + rintro ⟨x, y⟩ ⟨hx, hy⟩ s₁ s₂ s₃ y₁ y₂ y₃ + have hX := block_nonneg s₁ s₂ s₃ y₁ y₂ y₃ + set X := (|s₁| + ‖y₁‖) * (|s₂| + ‖y₂‖) * (|s₃| + ‖y₃‖) - |s₁| * |s₂| * |s₃| with hXdef + obtain ⟨x₀, hx₀, hxx₀⟩ : ∃ x₀ ∈ Icc (-2 * r) (2 * r), |x - x₀| ≤ ε := by + by_cases h1 : x ≤ -2 * r + · refine ⟨-2 * r, ⟨le_rfl, ?_⟩, ?_⟩ + · linarith [hx.1] + · rw [abs_le]; constructor <;> linarith [hx.1] + · by_cases h2 : 2 * r ≤ x + · refine ⟨2 * r, ⟨?_, le_rfl⟩, ?_⟩ + · linarith + · rw [abs_le]; constructor <;> linarith [hx.2] + · exact ⟨x, ⟨by linarith, by linarith⟩, by simp [hε]⟩ + set g : ℝ → ℝ := fun t => T3 (t, y) (s₁, y₁) (s₂, y₂) (s₃, y₃) - + s₁ * s₂ * s₃ * T3 (t, y) (1, 0) (1, 0) (1, 0) with hg + have hderiv : ∀ t ∈ Icc (-2 * r - ε₀) (2 * r + ε₀), HasDerivWithinAt g + (T4 (t, y) (s₁, y₁) (s₂, y₂) (s₃, y₃) - s₁ * s₂ * s₃ * T4 (t, y) (1, 0) (1, 0) (1, 0)) + (Icc (-2 * r - ε₀) (2 * r + ε₀)) t := by + intro t ht + have hp : (t, y) ∈ Icc (-2 * r - ε₀) (2 * r + ε₀) ×ˢ Metric.closedBall (0 : E) (2 * r) := ⟨ht, hy⟩ + have h1 : HasDerivAt (fun t => T3 (t, y) (s₁, y₁) (s₂, y₂) (s₃, y₃)) + (T4 (t, y) (s₁, y₁) (s₂, y₂) (s₃, y₃)) t := hD4x _ hp _ _ _ + have h2 : HasDerivAt (fun t => T3 (t, y) (1, 0) (1, 0) (1, 0)) (T4 (t, y) (1, 0) (1, 0) (1, 0)) t := + hD4x _ hp _ _ _ + exact (h1.sub (h2.const_mul (s₁ * s₂ * s₃))).hasDerivWithinAt + have hbound : ∀ t ∈ Icc (-2 * r - ε₀) (2 * r + ε₀), + ‖T4 (t, y) (s₁, y₁) (s₂, y₂) (s₃, y₃) - s₁ * s₂ * s₃ * T4 (t, y) (1, 0) (1, 0) (1, 0)‖ ≤ K * X := + fun t ht => by rw [Real.norm_eq_abs]; exact hT4 (t, y) ⟨ht, hy⟩ _ _ _ _ _ _ + have hxS : x ∈ Icc (-2 * r - ε₀) (2 * r + ε₀) := ⟨by linarith [hx.1], by linarith [hx.2]⟩ + have hx₀S : x₀ ∈ Icc (-2 * r - ε₀) (2 * r + ε₀) := + ⟨by linarith [hx₀.1, hε, hεε], by linarith [hx₀.2, hε, hεε]⟩ + have hmvt := (convex_Icc (-2 * r - ε₀) (2 * r + ε₀)).norm_image_sub_le_of_norm_hasDerivWithin_le + hderiv hbound hx₀S hxS + rw [Real.norm_eq_abs, Real.norm_eq_abs] at hmvt + have h0 : |g x₀| ≤ m * X := hT (x₀, y) ⟨hx₀, hy⟩ s₁ s₂ s₃ y₁ y₂ y₃ + have hKX : 0 ≤ K * X := mul_nonneg hK hX + have h3 : K * X * |x - x₀| ≤ K * X * ε := mul_le_mul_of_nonneg_left hxx₀ hKX + have h4 := abs_sub_abs_le_abs_sub (g x) (g x₀) + show |g x| ≤ (m + K * ε) * X + nlinarith + +/-- **The cap from the block bound alone.** `ridge_capHyp_C4` with its six derivative-bound +hypotheses derived. `hHxb`, `hHrb`, `hwcv` and `hwcc` come from the block bound `hT` +(`hessian_x_bound`, `hessian_r_bound`, `axis_convexConcave`). `hG0cv` and `hG0cc` come from +`|f_xxx| ≤ m` on the pin segment (`hTe`, SP: `|f_xxx| ≤ M₃`). The conclusion is unchanged. -/ +theorem ridge_capHyp_C5 [FiniteDimensional ℝ E] {f : ℝ × E → ℝ} + {Df : ℝ × E → ℝ × E →L[ℝ] ℝ} {D2f : ℝ × E → ℝ × E →L[ℝ] ℝ × E →L[ℝ] ℝ} + {T3 : ℝ × E → ℝ × E → ℝ × E → ℝ × E →L[ℝ] ℝ} {Φ4 : ℝ × E → ℝ × E →L[ℝ] ℝ} {n : ℝ} + {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₃|)) + (hTe : ∀ x ∈ Icc (-r / 2) (r / 2), |T3 (x, 0) (1, 0) (1, 0) (1, 0)| ≤ m) + (hD4 : ∀ p ∈ Icc (-2 * r) (2 * r) ×ˢ Metric.closedBall (0 : E) (2 * r), + HasFDerivAt (fun q => T3 q (1, 0) (1, 0) (1, 0)) (Φ4 p) p) + (hn4x : ∀ p ∈ Icc (-2 * r) (2 * r) ×ˢ Metric.closedBall (0 : E) (2 * r), |Φ4 p (1, 0)| ≤ n) + (hn4y : ∀ p ∈ Icc (-2 * r) (2 * r) ×ˢ Metric.closedBall (0 : E) (2 * r), ‖(Φ4 p).comp (ContinuousLinearMap.inr ℝ ℝ E)‖ ≤ n) + (hH2 : r * n ≤ 1 / 20) + (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) + (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) + (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) + (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 + have hm0 : 0 ≤ m := (abs_nonneg _).trans (hTe 0 ⟨by linarith, by linarith⟩) + have h0Y : (0 : E) ∈ Metric.closedBall (0 : E) (2 * r) := Metric.mem_closedBall_self (by positivity) + have hax : ∀ t ∈ Icc (-2 * r - ε) (2 * r + ε), + (t, (0 : E)) ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r) := + fun t ht => ⟨ht, h0Y⟩ + have hpin : ∀ t ∈ Icc (-r / 2) (r / 2), + (t, (0 : E)) ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r) := + fun t ht => hax t ⟨by linarith [ht.1], by linarith [ht.2]⟩ + -- `∂_x D_y² f` + have hHxb : ∀ x ∈ Icc (-2 * r - ε) (2 * r + ε), ‖Hx x‖ ≤ m := by + intro x hx + refine hessian_x_bound (J := Icc (-2 * r - ε) (2 * r + ε)) + (uniqueDiffOn_Icc (by linarith) x hx) hx hm0 (fun t ht => hH _ (hax t ht)) + (fun t ht => hD2 _ (hax t ht)) (hD3 _ (hax x hx)) (fun v w => ?_) (hHx x hx) + have := hT _ (hax x hx) 0 0 1 v w 0 + simpa using this + -- `∂_ρ D_y² f` + have hHrb : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + ∀ s ∈ Icc (0 : ℝ) 1, ‖Hr p s‖ ≤ m * ‖p.2‖ := by + rintro ⟨x, y⟩ hp s hs + have hyb : ‖y‖ ≤ 2 * r := by simpa [Metric.mem_closedBall, dist_zero_right] using hp.2 + have hseg : ∀ τ ∈ Icc (0 : ℝ) 1, + (x, τ • y) ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r) := by + intro τ hτ + refine ⟨hp.1, ?_⟩ + rw [Metric.mem_closedBall, dist_zero_right, norm_smul, Real.norm_eq_abs, abs_of_nonneg hτ.1] + nlinarith [hτ.2, norm_nonneg y] + refine hessian_r_bound hm0 hs (fun τ hτ => hH _ (hseg τ hτ)) (fun τ hτ => hD2 _ (hseg τ hτ)) + (hD3 _ (hseg s hs)) (fun v w => ?_) (hHr _ hp s hs) + have := hT _ (hseg s hs) 0 0 0 v w y + simpa using this + -- `w = ∂_y f (·, 0)` and `G0 = ∂_x f (·, 0)` + have hw : ∀ v : E, ConvexOn ℝ (Icc (-2 * r - ε) (2 * r + ε)) + (fun t => Df (t, 0) (0, v) + m * ‖v‖ / 2 * t ^ 2) ∧ + ConcaveOn ℝ (Icc (-2 * r - ε) (2 * r + ε)) (fun t => Df (t, 0) (0, v) - m * ‖v‖ / 2 * t ^ 2) := + fun v => axis_convexConcave (fun t ht => hD2 _ (hax t ht)) + (fun t ht => hD3 _ (hax t ht) (1, 0) (0, v)) + (fun t ht => by have := hT _ (hax t ht) 1 0 1 0 v 0; simpa using this) + have hG0 := axis_convexConcave (u := ((1 : ℝ), (0 : E))) (fun t ht => hD2 _ (hpin t ht)) + (fun t ht => hD3 _ (hpin t ht) (1, 0) (1, 0)) hTe + exact ridge_capHyp_C4 hr hε hεr hDf hD2 hD3 hT hD4 hn4x hn4y hH2 hGs hH hHx hHxb hHr hHrb hlam + hH1 hM hS hG0.1 hG0.2 (fun v => (hw v).1) (fun v => (hw v).2) hnorm + +/-- **The cap from SP's bounds on `D` (the continuity step of I3).** The quantitative hypotheses are +assumed on SP's `D` only: +- the block bound `m` and `|f_xxx| ≤ m` on the pin segment; +- SP's `M₄` blocks `n`; +- (H1) and (H2). + +On a collar of some width `ε₀ > 0`, only qualitative data are assumed: the derivatives, the strict +derivative of `∂_y f`, and some bound `K ≥ 0` on the `x`-derivative of `T3` in block form (SP: +`f ∈ C⁴` near `D`). Because (H1) is strict, some `ε ∈ (0, ε₀]` keeps `8r(m + Kε)² < λ`. +`ridge_capHyp_C5` then applies with `m + Kε` (`block_bound_collar`). -/ +theorem ridge_capHyp_D [FiniteDimensional ℝ E] {f : ℝ × E → ℝ} + {Df : ℝ × E → ℝ × E →L[ℝ] ℝ} {D2f : ℝ × E → ℝ × E →L[ℝ] ℝ × E →L[ℝ] ℝ} + {T3 : ℝ × E → ℝ × E → ℝ × E → ℝ × E →L[ℝ] ℝ} {T4 : ℝ × E → ℝ × E → ℝ × E → ℝ × E → ℝ} + {Φ4 : ℝ × E → ℝ × E →L[ℝ] ℝ} {n : ℝ} + {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 K lam ε₀ : ℝ} (hr : 0 < r) (hε₀ : 0 < ε₀) + (hK : 0 ≤ K) + (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) + (hD4x : ∀ p ∈ Icc (-2 * r - ε₀) (2 * r + ε₀) ×ˢ Metric.closedBall (0 : E) (2 * r), + ∀ a b c : ℝ × E, HasDerivAt (fun t => T3 (t, p.2) a b c) (T4 p a b c) p.1) + (hT4 : ∀ p ∈ Icc (-2 * r - ε₀) (2 * r + ε₀) ×ˢ Metric.closedBall (0 : E) (2 * r), + ∀ (s₁ s₂ s₃ : ℝ) (y₁ y₂ y₃ : E), + |T4 p (s₁, y₁) (s₂, y₂) (s₃, y₃) - s₁ * s₂ * s₃ * T4 p (1, 0) (1, 0) (1, 0)| ≤ + K * ((|s₁| + ‖y₁‖) * (|s₂| + ‖y₂‖) * (|s₃| + ‖y₃‖) - |s₁| * |s₂| * |s₃|)) + (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₃|)) + (hTe : ∀ x ∈ Icc (-r / 2) (r / 2), |T3 (x, 0) (1, 0) (1, 0) (1, 0)| ≤ m) + (hD4 : ∀ p ∈ Icc (-2 * r) (2 * r) ×ˢ Metric.closedBall (0 : E) (2 * r), + HasFDerivAt (fun q => T3 q (1, 0) (1, 0) (1, 0)) (Φ4 p) p) + (hn4x : ∀ p ∈ Icc (-2 * r) (2 * r) ×ˢ Metric.closedBall (0 : E) (2 * r), |Φ4 p (1, 0)| ≤ n) + (hn4y : ∀ p ∈ Icc (-2 * r) (2 * r) ×ˢ Metric.closedBall (0 : E) (2 * r), ‖(Φ4 p).comp (ContinuousLinearMap.inr ℝ ℝ E)‖ ≤ n) + (hH2 : r * n ≤ 1 / 20) + (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) + (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) + (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) + (hnorm : f (-r / 2, 0) - f (r / 2, 0) = r ^ 3 / 6) : + ∃ ε, 0 < ε ∧ ε ≤ ε₀ ∧ + (∃ 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 + have hev : ∀ᶠ ε in 𝓝[>] (0 : ℝ), 0 < ε ∧ ε ≤ ε₀ ∧ ε ≤ r / 2 ∧ 8 * r * (m + K * ε) ^ 2 < lam := by + have hc : ContinuousAt (fun ε : ℝ => 8 * r * (m + K * ε) ^ 2) 0 := by fun_prop + have h1 : ∀ᶠ ε in 𝓝 (0 : ℝ), 8 * r * (m + K * ε) ^ 2 < lam := + hc.eventually_lt continuousAt_const (by simpa using hH1) + have h2 : ∀ᶠ ε in 𝓝 (0 : ℝ), ε < ε₀ := eventually_lt_nhds hε₀ + have h3 : ∀ᶠ ε in 𝓝 (0 : ℝ), ε < r / 2 := eventually_lt_nhds (by linarith) + filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds h1, nhdsWithin_le_nhds h2, + nhdsWithin_le_nhds h3] with ε hε h1 h2 h3 + exact ⟨hε, h2.le, h3.le, h1⟩ + obtain ⟨ε, hε, hεε, hεr, hH1'⟩ := hev.exists + have hsub : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + p ∈ Icc (-2 * r - ε₀) (2 * r + ε₀) ×ˢ Metric.closedBall (0 : E) (2 * r) := + fun p hp => ⟨⟨by linarith [hp.1.1], by linarith [hp.1.2]⟩, hp.2⟩ + have hsubI : ∀ x ∈ Icc (-2 * r - ε) (2 * r + ε), x ∈ Icc (-2 * r - ε₀) (2 * r + ε₀) := + fun x hx => ⟨by linarith [hx.1], by linarith [hx.2]⟩ + have hmm : m ≤ m + K * ε := le_add_of_nonneg_right (mul_nonneg hK hε.le) + exact ⟨ε, hε, hεε, ridge_capHyp_C5 (m := m + K * ε) hr hε hεr (fun p hp => hDf p (hsub p hp)) + (fun p hp => hD2 p (hsub p hp)) (fun p hp => hD3 p (hsub p hp)) + (block_bound_collar hr hK hε.le hεε hT hD4x hT4) (fun x hx => (hTe x hx).trans hmm) + hD4 hn4x hn4y hH2 (fun p hp => hGs p (hsub p hp)) (fun p hp => hH p (hsub p hp)) + (fun x hx => hHx x (hsubI x hx)) (fun p hp => hHr p (hsub p hp)) hlam hH1' hM hS hnorm⟩ + end Slice /-! ### A concrete instance and the necessity of each hypothesis @@ -3593,4 +3974,126 @@ theorem h1Toy_C4 : simp only [smul_eq_mul] simp +/-- **`ridge_capHyp_D` is not vacuous.** `h1ToyF` meets every hypothesis of `ridge_capHyp_D` with +`ε₀ = 1/2`. `T3` is constant, so `T4 = 0` and `K = 0`, and `|f_xxx| = 2 = m` on the pin segment. +The theorem chooses the collar width itself. It gives the ridge on `(−2 − ε, 2 + ε)` for some +`ε > 0` and the cap with `M = (−1/2, 0)`, from hypotheses on `D` and qualitative collar data only. -/ +theorem h1Toy_D : + (∃ ε > 0, ∃ h : ℝ → ℝ, ∀ x ∈ Ioo (-2 * 1 - ε : ℝ) (2 * 1 + ε), 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_D (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 ℝ ℝ ℝ) + (T4 := fun _ _ _ _ => 0) (Φ4 := fun _ => 0) (n := 0) + (DG := fun _ => ((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ) ∘L ContinuousLinearMap.snd ℝ ℝ ℝ) + (H := fun _ => (-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ) (Hx := fun _ => 0) + (Hr := fun _ _ => 0) (r := 1) (m := 2) (K := 0) (lam := 40) (ε₀ := 1 / 2) one_pos + (by norm_num) le_rfl + (fun p _ => hDf p) (fun p _ => hD2 p) (fun p _ a b => hD3 p a b) + (fun p _ a b c => hasDerivAt_const p.1 _) (fun p _ s₁ s₂ s₃ y₁ y₂ y₃ => by simp) + (fun p _ => hT p) (fun x _ => by simp) (fun p _ => hasFDerivAt_const _ p) (fun p _ => by simp) + (fun p _ => by simp) (by norm_num) + (fun p _ => hGs p) (fun p _ => hH p) + (fun x _ => hasDerivAt_const x ((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ)) + (fun p _ s _ => hasDerivAt_const s ((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ)) + (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 ⟨ε, hε, -, 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 ⟨⟨ε, hε, hex⟩, hC⟩ + end CapFirstExit diff --git a/frontiers/cap_first_exit_lean_20261002/MANIFEST.json b/frontiers/cap_first_exit_lean_20261002/MANIFEST.json index 04efca195..e64d1763e 100644 --- a/frontiers/cap_first_exit_lean_20261002/MANIFEST.json +++ b/frontiers/cap_first_exit_lean_20261002/MANIFEST.json @@ -119,6 +119,13 @@ "CapFirstExit.third_deriv_exists_two", "CapFirstExit.fxxx_lower", "CapFirstExit.ridge_capHyp_C4", + "CapFirstExit.hessian_x_bound", + "CapFirstExit.hessian_r_bound", + "CapFirstExit.axis_convexConcave", + "CapFirstExit.block_nonneg", + "CapFirstExit.block_bound_collar", + "CapFirstExit.ridge_capHyp_C5", + "CapFirstExit.ridge_capHyp_D", "CapFirstExit.toyF", "CapFirstExit.toyRidge", "CapFirstExit.toy_ridge_ge", @@ -145,7 +152,8 @@ "CapFirstExit.h1Toy_ridge_differentiable", "CapFirstExit.h1Toy_source", "CapFirstExit.h1Toy_C3", - "CapFirstExit.h1Toy_C4" + "CapFirstExit.h1Toy_C4", + "CapFirstExit.h1Toy_D" ], "expected_axioms": { "CapFirstExit.path_meets_frontier": [ @@ -578,6 +586,41 @@ "Quot.sound", "propext" ], + "CapFirstExit.hessian_x_bound": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.hessian_r_bound": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.axis_convexConcave": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.block_nonneg": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.block_bound_collar": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.ridge_capHyp_C5": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.ridge_capHyp_D": [ + "Classical.choice", + "Quot.sound", + "propext" + ], "CapFirstExit.toyF": [ "Classical.choice", "Quot.sound", @@ -712,6 +755,11 @@ "Classical.choice", "Quot.sound", "propext" + ], + "CapFirstExit.h1Toy_D": [ + "Classical.choice", + "Quot.sound", + "propext" ] }, "files": [ @@ -722,18 +770,18 @@ }, { "path": "ALIGNMENT.md", - "bytes": 38646, - "sha256": "bc6699d8a20b664a3b53478fd216d38e4861935a397ef5f5d4d75ffea6f16b96" + "bytes": 43249, + "sha256": "b5c6149055a5065cfd68974eb63e5efe22bc1f8ba245529178097399eedce4a9" }, { "path": "CapFirstExit.lean", - "bytes": 208489, - "sha256": "29ff78369cadf9d429f995c54ae33ad0777193165fb7a1609f40f779a35b86d7" + "bytes": 243630, + "sha256": "734fb06e60344306d45bc7a4d58569014f3edd1c12d35e7abb64fb0d9c3dc26f" }, { "path": "README.md", - "bytes": 20933, - "sha256": "4bf3c609e18483feacfb7082e016d44fc6898c18cf496e0d9b69a6a9bb7a2e21" + "bytes": 23706, + "sha256": "c03b290cab94245f1c61aaa057f385eca333934c9b1ef090409d7a7d123860ad" }, { "path": "gate.py", @@ -758,7 +806,7 @@ { "path": "test_gate.py", "bytes": 6275, - "sha256": "e30eb16fb9944e626427db2badabfb4c57c4662b54f34860928e1fbabf69860b" + "sha256": "f08f5dafe37645d68ea582034b32106c1771c467afb48b9ac355ee1512570daf" } ] } diff --git a/frontiers/cap_first_exit_lean_20261002/README.md b/frontiers/cap_first_exit_lean_20261002/README.md index bdb3c9041..38f547b1e 100644 --- a/frontiers/cap_first_exit_lean_20261002/README.md +++ b/frontiers/cap_first_exit_lean_20261002/README.md @@ -49,6 +49,14 @@ Since v2.0, `ridge_capHyp_C4` also derives the one analytic input that `ridge_ca So the hypotheses of `ridge_capHyp_C4` are SP's (H1), (H2), the critical pins, the gap `r³/6` and the derivative data with the bounds `m` (on the collar) and `n` (on `D`). No step of L1–L20 remains a hypothesis. +Since v2.1, the quantitative bounds enter on `D` only: +- `ridge_capHyp_C5` derives six derivative-bound hypotheses of `ridge_capHyp_C4` from the block bound `m`, and from `|f_xxx| ≤ m` on the pin segment: + - L3's inputs `‖∂_x D_y² f‖ ≤ m` and `‖∂_ρ D_y² f‖ ≤ m‖y‖` (`hessian_x_bound`, `hessian_r_bound`); + - the convex and concave envelopes of `∂_y f(·, 0)` and `∂_x f(·, 0)`, which are the inputs of L5–L6 and L1–L2 (`axis_convexConcave`). +- `ridge_capHyp_D` assumes the bounds `m`, `n`, (H1) and (H2) on SP's `D` only. On a collar of some width `ε₀ > 0` it assumes the derivatives, and some bound `K` on the `x`-derivative of the third derivatives (SP: `f ∈ C⁴` near `D`). + - The continuity step `block_bound_collar` gives the block bound `m + Kε` on the collar of width `ε`. + - Because (H1) is strict, some `ε > 0` keeps `8r(m + Kε)² < λ`. + In the topological theorems, `X` is any topological space, and nothing is assumed about `f` outside `C` except along the single ridge path. - The core theorems use only (C1)–(C3): no metric, smoothness, Morse, compactness or probability hypothesis. Their @@ -105,6 +113,12 @@ single ridge path. | `fxxx_lower` | L4's `f_xxx ≥ 7/4` (v2.0). If `|∂_x f_xxx| ≤ n` and `‖D_y f_xxx‖ ≤ n` on `D`, `f_xxx(x₀, 0) ≥ 2` and (H2) `rn ≤ 1/20`, then `f_xxx ≥ 7/4` on `D` (the proof bounds `f_xxx ≥ 2 − 9rn/2`, and the statement exports `7/4`). Move first in `x`, then along the ray to `y`, as in SP's L3 (SP rounds this to `2 − 5rn`) | | `ridge_capHyp_C4` | the cap from SP's hypotheses (v2.0): `ridge_capHyp_C3` with `f_xxx ≥ 7/4` replaced by a derivative `Φ4` of `f_xxx` on `D`, its two blocks bounded by `n`, and (H2) `rn ≤ 1/20` | | `h1Toy_C4` | `h1ToyF` meets every hypothesis of `ridge_capHyp_C4` (`f_xxx = 2` constant, `n = 0`). The theorem gives its ridge and cap with neither `hconv` nor `f_xxx ≥ 7/4` supplied | +| `hessian_x_bound`, `hessian_r_bound` | L3's inputs from the block bound (v2.1). `∂_x D_y² f (x, 0)[v, w] = T3(x, 0)[(0, v), (0, w), (1, 0)]` and `∂_ρ D_y² f (x, sy)[v, w] = T3(x, sy)[(0, v), (0, w), (0, y)]`. The identification uses derivatives within an interval, so collar endpoints and the sphere are allowed. So `‖∂_x D_y² f‖ ≤ m` and `‖∂_ρ D_y² f‖ ≤ m‖y‖` | +| `axis_convexConcave` | the envelope inputs (v2.1). If `|∂_x² (Df(·, 0) u)| ≤ B` on `[a, c]`, then `Df(·, 0) u ± (B/2)t²` is convex, respectively concave. Take `u = (0, v)`, `B = m‖v‖` for `w` (L5–L6), and `u = (1, 0)`, `B = m` for `G0` (L1–L2) | +| `block_nonneg`, `block_bound_collar` | the continuity step of I3 (v2.1). Assume the block bound `m` on `D`, and some bound `K` on the `x`-derivative of `T3` in block form on a collar of width `ε₀`. Then the block bound `m + Kε` holds on the collar of width `ε ≤ ε₀`, by the mean value inequality from the nearest point of `D` | +| `ridge_capHyp_C5` | `ridge_capHyp_C4` with `hHxb`, `hHrb`, `hwcv`, `hwcc`, `hG0cv` and `hG0cc` derived from the block bound and `|f_xxx| ≤ m` on the pin segment (v2.1) | +| `ridge_capHyp_D` | the cap from SP's bounds on `D` (v2.1). The bounds `m`, `n`, (H1) and (H2) are assumed on `D`, with qualitative derivative data and some `K ≥ 0` on a collar of width `ε₀`. It concludes the ridge on `(−2r − ε, 2r + ε)`, `h(∓r/2) = 0`, the cap and (C2⁺), for some `ε ∈ (0, ε₀]` | +| `h1Toy_D` | `h1ToyF` meets every hypothesis of `ridge_capHyp_D` (`T4 = 0`, `K = 0`, `ε₀ = 1/2`). The theorem gives a ridge on `(−2 − ε, 2 + ε)` for some `ε > 0`, and the cap | | `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 | @@ -129,13 +143,15 @@ This packet does not formalize: - the source data themselves. Since v2.0 every analytic step of L1–L20 that `ridge_capHyp_C4` uses is proved: L1–L13 and L16–L20, with L7's existence, uniqueness and regularity of `h`. L14 (the critical-point count in `D`) and L15 - (Morse indices) are not formalized and are not used by the cap theorem. `ridge_capHyp_C4` takes, as hypotheses: - - the derivatives `Df`, `DG`, `H`, `D2f` and the third derivatives, with the bounds `m`, on the collar - `[−2r − ε, 2r + ε] × B̄(0, 2r)`; - - the derivative of `f_xxx`, with its block bound `n`, on `D`. - - 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; + (Morse indices) are not formalized and are not used by the cap theorem. Since v2.1 `ridge_capHyp_D` takes, as + hypotheses: + - the quantitative bounds on SP's `D` only: the third-derivative block bound `m`, `|f_xxx| ≤ m` on the pin segment, + the block bound `n` on the derivative of `f_xxx`, (H1) and (H2); + - qualitative data on some collar `[−2r − ε₀, 2r + ε₀] × B̄(0, 2r)`: the derivatives `Df`, `DG`, `H`, `D2f`, the + third derivatives and their `x`-derivatives, with some bound `K` on the latter. + + The continuity step from `D` to the collar is proved (`block_bound_collar`). What stays informal is that SP's + `f ∈ C⁴` near `D` supplies these data and some `K`, by compactness of a closed collar; - the match between the source's coordinates and the Lean objects: that SP's cap is `[-2r, r/2] × B̄(0, 2r)` in a frame `φ` and that SP analyses the periodic lift. The transport to the torus and the face list are themselves proved (`CapHyp.toTorus`, `frontier_cylinder`); @@ -174,7 +190,7 @@ The source gate checks: bound); - rebuilds the package fresh; - replays the module with `leanchecker`; -- prints the axioms of all 113 declarations, requiring exactly the manifest's report: each uses only `propext`, +- prints the axioms of all 121 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 3484afdac..afdfb1a54 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"]), 113) + self.assertEqual(len(m["targets"]), 121) self.assertEqual(m['scientific_effect'], 'NONE') def copy(self):