Cap first exit in Lean v1.7 (stacked on #255): L7 kernel-checked, existence, uniqueness and implicit-function regularity of the ridge

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`). Inputs that remain: L6, L7's existence and regularity of `h`, and L9–L12. |
+| 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`). Inputs that remain: L6 and L9–L12, and the full-domain ridge premises (the slice data on an open `U ⊇ [−2r, 2r]`, and the composition of the L7 lemmas with the source route; see 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:
@@ -67,8 +67,14 @@ The source setting (SP §2) is as follows:
 | `strongConcaveOn_of_hessian` | `HasFDerivAt φ (Dφ y) y`, `HasFDerivAt Dφ (H y) y` and `H y v v ≤ −δ‖v‖²` on convex `K` ⇒ `StrongConcaveOn K δ φ` | SP L7's first sentence ("`δ`-strongly concave … (L4)") | The quadratic-form bound `D_y² f ≤ −δI` is SP's form. The proof restricts to segments and uses Mathlib's `concaveOn_of_hasDerivWithinAt2_nonpos`. |
 | `hessian_increment` | `x ↦ H(x, 0)` with derivative of norm `≤ m` on `[−2r, r/2]`, and `s ↦ H(x, s • y)` with derivative of norm `≤ m‖y‖` on `[0, 1]` for each cap point ⇒ `‖H(p) − H(M)‖ ≤ m(|p.1 + r/2| + ‖p.2‖)` on the cap | SP L3 ("moving first in `x` then in `y` … `sup‖∂_x u‖ |Δx| + sup‖D_y u‖ ‖Δy‖`", for `u = D_y² f`) | Mean value inequality twice: along `y = 0`, then along the ray from `(x, 0)` to `(x, y)`. The `y`-bound is stated along rays, i.e. `‖D_y³ f[y]‖ ≤ m‖y‖`, which is what L3 uses and is implied by `‖D_y³ f‖ ≤ m`. (Lean at the pinned Mathlib does not synthesize the norm on the triple-nested operator space, so the bound is not stated as `‖D_y H‖ ≤ m`.) |
 | `transverse_hessian_le` | `H(M) v v ≤ −λ‖v‖²`, `‖H(p) − H(M)‖ ≤ m(|p.1 + r/2| + ‖p.2‖)` on the cap ⇒ `H(p) v v ≤ −(λ − 5rm)‖v‖²` there | SP L4 (`D_y² f(p) ≤ D_y² f(M) + 5rm · I`), with L3's increment `|Δx| + ‖Δy‖ < 5r` | The increment hypothesis is `hessian_increment`'s conclusion. |
-| `slices_strongConcave` | under the same data on the cap, each slice `y ↦ f(x, y)`, `x ∈ [−2r, r/2]`, is `(λ − 5rm)`-strongly concave on `B̄(0, 2r)` | SP L4 (`δ = λ − 5rm`) | SP proves it on `D`; the cap's range of `x` suffices. |
+| `slices_strongConcave` | under the same data on the cap, each slice `y ↦ f(x, y)`, `x ∈ [−2r, r/2]`, is `(λ − 5rm)`-strongly concave on `B̄(0, 2r)` | SP L4 (`δ = λ − 5rm`) | SP proves it on `D`. The cap's range of `x` suffices for the cap theorems, but the L7 lemmas need it on an open `U ⊇ [−2r, 2r]`; that extension is not formalized (I3). |
 | `ridge_capHyp_H1` | the conclusions of `ridge_capHyp_normalized`, with `hconc` and `hδ` replaced by the slice derivatives `Dφ` and Hessians `H` on the cap, the third-derivative bounds of `hessian_increment` (`∂_x H` along `y = 0` and `D_y H` along rays, both at `m`), `H(M) ≤ −λ` and (H1) `8rm² < λ` | SP §2 (H1), L1–L5, L7, L8, L11, L12, L16–L20 | `δ := λ − 5rm`, and `rm(8m − 5) < λ − 5rm` is (H1). SP's (H2) `rn ≤ 1/20` feeds only L4's `f_xxx ≥ 7/4` and L12, so it is not needed here. |
+| `slice_critical_unique` | `δ > 0`, `δ`-strongly concave slice, two critical points in `K` ⇒ they are equal | SP L7 ("unique by strict concavity … the unique critical point") | From `slice_le` applied both ways. |
+| `slice_critical_exists` | `[ProperSpace E]`, `R > 0`, `δ`-strongly concave and differentiable on `B̄(0, R)`, `‖Dφ(0)‖ < δR` ⇒ a critical point exists in the open ball | SP L7 ("the radial derivative is negative on the boundary … attained in the interior"; `‖w‖ · 2r < δ · 4r²`) | The maximum over the compact ball exists. On the sphere, `Dφ(p)(p) ≤ w(p) − δR² < 0` (engine applied at `p` and at `0`) contradicts `Dφ(p)(−p) ≤ 0` at a maximum (Mathlib's tangent-cone condition). SP's strict `‖w‖ < 2mr² < 2rδ/k` gives the hypothesis. |
+| `isInvertible_of_negDef` | `[FiniteDimensional ℝ E]`, `A v v ≤ −δ‖v‖²`, `δ > 0` ⇒ `A : E →L E →L ℝ` is invertible | SP L7 ("`D_y² f` invertible") | Injective, hence bijective by equal finite dimension of `E` and `E*`. |
+| `ridge_hasStrictFDerivAt` | `HasStrictFDerivAt G DG (x0, h x0)` with invertible `DG ∘ inr`, `G` the slice gradient near `(x0, h x0)`, `h x0` critical, local uniqueness of critical points in a neighbourhood of `h x0` ⇒ `HasStrictFDerivAt h (−(DG∘inr)⁻¹ ∘ (DG∘inl)) x0` | SP L7 (implicit function theorem) and L9 (`h' = −(D_y² f)⁻¹ ∂_x ∇_y f`) | Uses Mathlib's `implicitFunctionOfProdDomain`. The implicit solution is a critical point near `h x0`, so it equals `h` by uniqueness, and no continuity of `h` is assumed. |
+| `ridge_differentiable` | on an open `U ⊇ [−2r, 2r]`: slices `δ`-strongly concave and `h x` critical in `B̄(0, 2r)`; on `[−2r, 2r]`: `h x` in the open ball, `G` the slice gradient near the ridge, strictly differentiable with negative definite transverse part ⇒ `h` strictly differentiable on `[−2r, 2r]` | SP L7 (`h ∈ C³` by the implicit function theorem; first order here) | `U` reflects SP's `f ∈ C⁴` near `D`: derivatives at `x = ±2r` need a two-sided neighbourhood. The interior condition follows from L8 (`δ‖h‖ ≤ ‖w‖ < 2rδ`). Composed with `ridge_inputs_of_joint` (via `HasStrictFDerivAt.hasFDerivAt` and `HasFDerivAt.hasDerivAt`), it would supply `hh'`; no declaration performs this composition, and its premises on `U`, and `hG`, `hGs`, `hneg` on `[−2r, 2r]`, are not derived from the cap data (I3). |
+| `ridge_exists` | `[ProperSpace E]`, on `U`: slices strongly concave and differentiable on `B̄(0, 2r)` with `‖Dφ_x(0)‖ < δ · 2r` ⇒ `∃ h`, with `h x` a critical point in the open ball for every `x ∈ U` | SP L7 ("call it `h(x)`") | By choice. Unique by `slice_critical_unique`, so it is SP's `h`. |
 | `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. |
 
@@ -101,7 +107,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.
+`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.
 
 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
@@ -116,7 +122,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); L7's existence of the transverse maximizer `h(x)` in the ball and the implicit-function regularity of `h`; 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.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); 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`; with existence and regularity of `h` themselves proved since v1.7; the slice data that `ridge_exists` and `ridge_differentiable` take on an open `U ⊇ [−2r, 2r]` (strong concavity, critical points, slice derivatives and `‖∂_y f(x, 0)‖ < 2rδ`), whereas `slices_strongConcave` and `ridge_capHyp_H1` provide or consume them only for `x ∈ [−2r, r/2]` (SP proves L4 on all of `D`, increment `9r/2 < 5r`); the composition of those L7 lemmas with `ridge_inputs_of_joint` and `ridge_capHyp_H1`, which no declaration performs; 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.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
@@ -133,5 +139,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. 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. A same-provider read, including any Claude
 read, gives zero independence credit. A build or merge is not an alignment review.