diff --git a/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md b/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md index 1228d4461..51bc6961d 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`). 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. diff --git a/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean b/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean index df7f5d2b6..63d3ac226 100644 --- a/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean +++ b/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean @@ -16,10 +16,13 @@ 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 step L6, the existence and implicit-function - regularity of the transverse maximizer `h`, and L9–L12 (they enter `ridge_capHyp_H1`, - `ridge_capHyp_of_slices` and `ridge_inputs_of_joint` as hypotheses; L1–L5, L7's maximum and - uniqueness, L8, L11's chain rule, L13 and L16–L20 are proved from them); the identification of the H0 persistence pairing with the elder rule (L22, P §8); the + 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, + uniqueness and implicit-function regularity of the ridge `h`: `ridge_exists`, + `ridge_differentiable`), L8, L11's chain rule, L13 and L16–L20 are proved. The L7 lemmas take the + slice data on an open `U ⊇ [-2r, 2r]`; its extension from the cap's `x`-range `[-2r, r/2]` and + their composition with `ridge_capHyp_H1` are not formalized. 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. -/ import Mathlib @@ -1265,6 +1268,165 @@ theorem ridge_capHyp_H1 {f : ℝ × E → ℝ} {h : ℝ → E} {F G0 : ℝ → exact ridge_capHyp_normalized hr hg0 hG0cv hG0cc hG0a hG0c hδ hh hg hFa hFc hconv hconc hball hcrit hha hhc hw hwcv hwcc hnorm +/-- **L7 (uniqueness of the transverse critical point).** A `δ`-strongly concave slice, `δ > 0`, +has at most one critical point in `K`. -/ +theorem slice_critical_unique {K : Set E} {φ : E → ℝ} {δ : ℝ} (hφ : StrongConcaveOn K δ φ) + (hδ : 0 < δ) {p q : E} (hp : p ∈ K) (hq : q ∈ K) (hdp : HasFDerivAt φ (0 : E →L[ℝ] ℝ) p) + (hdq : HasFDerivAt φ (0 : E →L[ℝ] ℝ) q) : p = q := by + have h1 := slice_le hφ hp hdp hq + have h2 := slice_le hφ hq hdq hp + rw [norm_sub_rev] at h2 + have h3 : δ * ‖q - p‖ ^ 2 ≤ 0 := by linarith + have h4 : ‖q - p‖ ^ 2 ≤ 0 := by + have : δ * ‖q - p‖ ^ 2 ≤ δ * 0 := by rw [mul_zero]; exact h3 + exact le_of_mul_le_mul_left this hδ + have h5 : ‖q - p‖ = 0 := by nlinarith [norm_nonneg (q - p)] + exact (sub_eq_zero.mp (norm_eq_zero.mp h5)).symm + +/-- **L7 (existence of the transverse critical point).** If the slice is `δ`-strongly concave and +differentiable on `B̄(0, R)` and its derivative at `0` has norm `< δR` (SP: `‖w‖ < δ · 2r`), the +maximum over the compact ball is attained in the open ball, so it is a critical point. On the +sphere the radial derivative is `≤ w(p) - δR² < 0` (SP's L7 computation, here from the strong +concavity engine), which contradicts maximality. -/ +theorem slice_critical_exists [ProperSpace E] {φ : E → ℝ} {Dφ : E → E →L[ℝ] ℝ} {δ R : ℝ} + (hR : 0 < R) (hφ : StrongConcaveOn (Metric.closedBall (0 : E) R) δ φ) + (hD : ∀ y ∈ Metric.closedBall (0 : E) R, HasFDerivAt φ (Dφ y) y) (hw : ‖Dφ 0‖ < δ * R) : + ∃ p ∈ Metric.ball (0 : E) R, HasFDerivAt φ (0 : E →L[ℝ] ℝ) p := by + have h0 : (0 : E) ∈ Metric.closedBall (0 : E) R := Metric.mem_closedBall_self hR.le + have hcont : ContinuousOn φ (Metric.closedBall (0 : E) R) := + fun y hy => (hD y hy).continuousAt.continuousWithinAt + obtain ⟨p, hp, hmax⟩ := (isCompact_closedBall (0 : E) R).exists_isMaxOn ⟨0, h0⟩ hcont + have hpR : ‖p‖ ≤ R := by simpa using hp + have hlt : ‖p‖ < R := by + by_contra hc + have hpn : ‖p‖ = R := le_antisymm hpR (not_lt.mp hc) + have hseg : segment ℝ p (p + -p) ⊆ Metric.closedBall (0 : E) R := by + rw [add_neg_cancel] + exact (convex_closedBall (0 : E) R).segment_subset hp h0 + have hcone := mem_posTangentConeAt_of_segment_subset hseg + have hnp := hmax.isLocalMaxOn.hasFDerivWithinAt_nonpos (hD p hp).hasFDerivWithinAt hcone + have e1 := strongConcave_le_of_hasFDerivAt hφ hp (hD p hp) h0 + have e2 := strongConcave_le_of_hasFDerivAt hφ h0 (hD 0 h0) hp + simp only [zero_sub, sub_zero, norm_neg, map_neg] at e1 e2 hnp + have hb : Dφ 0 p ≤ ‖Dφ 0‖ * ‖p‖ := + (le_abs_self _).trans (by simpa [Real.norm_eq_abs] using (Dφ 0).le_opNorm p) + rw [hpn] at e1 e2 hb + have : ‖Dφ 0‖ * R < δ * R * R := by nlinarith + nlinarith + have hpb : p ∈ Metric.ball (0 : E) R := by simpa using hlt + have hloc : IsLocalMax φ p := + hmax.isLocalMax (Metric.closedBall_mem_nhds_of_mem hpb) + refine ⟨p, hpb, ?_⟩ + have hz := hloc.hasFDerivAt_eq_zero (hD p hp) + rw [← hz] + exact hD p hp + +/-- In finite dimension, a bilinear form `A : E →L E →L ℝ` with `A v v ≤ -δ‖v‖²`, `δ > 0`, is +invertible as a map `E → E*` (SP L7: "`D_y² f` invertible"). -/ +theorem isInvertible_of_negDef [FiniteDimensional ℝ E] {A : E →L[ℝ] E →L[ℝ] ℝ} {δ : ℝ} + (hδ : 0 < δ) (hA : ∀ v : E, A v v ≤ -δ * ‖v‖ ^ 2) : A.IsInvertible := by + have hinj : Function.Injective A := by + intro v w hvw + have h1 : A (v - w) = 0 := by rw [map_sub, hvw, sub_self] + have h2 := hA (v - w) + rw [h1, zero_apply] at h2 + have h3 : ‖v - w‖ ^ 2 ≤ 0 := by nlinarith [sq_nonneg ‖v - w‖] + have h4 : ‖v - w‖ = 0 := by nlinarith [norm_nonneg (v - w)] + exact sub_eq_zero.mp (norm_eq_zero.mp h4) + have hrank : Module.finrank ℝ E = Module.finrank ℝ (E →L[ℝ] ℝ) := by + rw [← (LinearMap.toContinuousLinearMap : (E →ₗ[ℝ] ℝ) ≃ₗ[ℝ] E →L[ℝ] ℝ).finrank_eq] + exact (Subspace.dual_finrank_eq).symm + have hsurj : Function.Surjective A := + (LinearMap.injective_iff_surjective_of_finrank_eq_finrank hrank (f := (A : E →ₗ[ℝ] E →L[ℝ] ℝ))).mp hinj + refine ⟨(LinearEquiv.ofBijective (A : E →ₗ[ℝ] E →L[ℝ] ℝ) ⟨hinj, hsurj⟩).toContinuousLinearEquiv, ?_⟩ + ext v w + rfl + +/-- **L7 (regularity of the ridge, pointwise).** If the transverse gradient `G` is strictly +differentiable at `(x0, h x0)` with invertible transverse part, `h x0` is a critical point, and +near `x0` the critical point of each slice in a neighbourhood `K` of `h x0` is unique and equal to +`h x`, then `h` agrees near `x0` with the implicit function of `G = 0` (Mathlib's +`implicitFunctionOfProdDomain`), so `h` is strictly differentiable at `x0` with +`h' = -(∂_y G)⁻¹ ∂_x G` (SP L9's formula). -/ +theorem ridge_hasStrictFDerivAt [CompleteSpace E] {f : ℝ × E → ℝ} {G : ℝ × E → E →L[ℝ] ℝ} + {DG : ℝ × E →L[ℝ] E →L[ℝ] ℝ} {h : ℝ → E} {K : Set E} {x0 : ℝ} + (hGs : HasStrictFDerivAt G DG (x0, h x0)) + (hinv : (DG ∘L ContinuousLinearMap.inr ℝ ℝ E).IsInvertible) + (hG : ∀ᶠ v in 𝓝 (x0, h x0), HasFDerivAt (fun y => f (v.1, y)) (G v) v.2) + (hcrit0 : HasFDerivAt (fun y => f (x0, y)) (0 : E →L[ℝ] ℝ) (h x0)) (hK : K ∈ 𝓝 (h x0)) + (huniq : ∀ᶠ x in 𝓝 x0, ∀ y ∈ K, HasFDerivAt (fun y => f (x, y)) (0 : E →L[ℝ] ℝ) y → y = h x) : + HasStrictFDerivAt h (-(DG ∘L ContinuousLinearMap.inr ℝ ℝ E).inverse ∘L + (DG ∘L ContinuousLinearMap.inl ℝ ℝ E)) x0 := by + have hGu : G (x0, h x0) = 0 := (hG.self_of_nhds).unique hcrit0 + have hψ := hGs.hasStrictFDerivAt_implicitFunctionOfProdDomain hinv + have hev := hGs.eventually_apply_implicitFunctionOfProdDomain hinv + have htend := hGs.tendsto_implicitFunctionOfProdDomain hinv + set ψ := hGs.implicitFunctionOfProdDomain hinv with hψdef + have hpair : Tendsto (fun x => (x, ψ x)) (𝓝 x0) (𝓝 (x0, h x0)) := + (tendsto_id.prodMk_nhds htend) + have hGψ := hpair.eventually hG + have hKψ := htend.eventually hK + have heq : ψ =ᶠ[𝓝 x0] h := by + filter_upwards [hev, hGψ, hKψ, huniq] with x h1 h2 h3 h4 + rw [h1, hGu] at h2 + exact h4 (ψ x) h3 h2 + exact hψ.congr_of_eventuallyEq heq + + +/-- **L7 (regularity of the ridge on `[-2r, 2r]`).** With the slices `δ`-strongly concave and `h x` a +critical point in `B̄(0, 2r)` for `x` in an open set `U ⊇ [-2r, 2r]` (SP: `f ∈ C⁴` near `D`), `h x` +in the open ball on `[-2r, 2r]`, and the transverse gradient strictly differentiable along the +ridge with negative definite transverse part, `h` is strictly differentiable at every +`x ∈ [-2r, 2r]`. This supplies `hh'` of `ridge_inputs_of_joint`. -/ +theorem ridge_differentiable [FiniteDimensional ℝ E] {f : ℝ × E → ℝ} {G : ℝ × E → E →L[ℝ] ℝ} + {DG : ℝ → ℝ × E →L[ℝ] E →L[ℝ] ℝ} {h : ℝ → E} {U : Set ℝ} {r δ : ℝ} (hδ : 0 < δ) + (hU : IsOpen U) (hIU : Icc (-2 * r) (2 * r) ⊆ U) + (hconc : ∀ x ∈ U, + StrongConcaveOn (Metric.closedBall (0 : E) (2 * r)) δ (fun y => f (x, y))) + (hball : ∀ x ∈ U, h x ∈ Metric.closedBall (0 : E) (2 * r)) + (hcrit : ∀ x ∈ U, HasFDerivAt (fun y => f (x, y)) (0 : E →L[ℝ] ℝ) (h x)) + (hint : ∀ x ∈ Icc (-2 * r) (2 * r), h x ∈ Metric.ball (0 : E) (2 * r)) + (hG : ∀ x ∈ Icc (-2 * r) (2 * r), + ∀ᶠ v in 𝓝 (x, h x), HasFDerivAt (fun y => f (v.1, y)) (G v) v.2) + (hGs : ∀ x ∈ Icc (-2 * r) (2 * r), HasStrictFDerivAt G (DG x) (x, h x)) + (hneg : ∀ x ∈ Icc (-2 * r) (2 * r), ∀ v : E, + (DG x ∘L ContinuousLinearMap.inr ℝ ℝ E) v v ≤ -δ * ‖v‖ ^ 2) : + ∀ x ∈ Icc (-2 * r) (2 * r), HasStrictFDerivAt h + (-(DG x ∘L ContinuousLinearMap.inr ℝ ℝ E).inverse ∘L (DG x ∘L ContinuousLinearMap.inl ℝ ℝ E)) x := by + intro x hx + have hK : Metric.closedBall (0 : E) (2 * r) ∈ 𝓝 (h x) := + Metric.closedBall_mem_nhds_of_mem (hint x hx) + have huniq : ∀ᶠ x' in 𝓝 x, ∀ y ∈ Metric.closedBall (0 : E) (2 * r), + HasFDerivAt (fun y => f (x', y)) (0 : E →L[ℝ] ℝ) y → y = h x' := by + filter_upwards [hU.mem_nhds (hIU hx)] with x' hx' y hy hdy + exact slice_critical_unique (hconc x' hx') hδ hy (hball x' hx') hdy (hcrit x' hx') + exact ridge_hasStrictFDerivAt (hGs x hx) (isInvertible_of_negDef hδ (hneg x hx)) (hG x hx) + (hcrit x (hIU hx)) hK huniq + + +/-- **L7 (existence of the ridge).** If on an open set `U` of `x`-values the slices are +`δ`-strongly concave and differentiable on `B̄(0, 2r)` with `‖∂_y f(x, 0)‖ < δ · 2r`, a map `h` +with `h x` a critical point in the open ball exists on `U` (by choice; unique by +`slice_critical_unique`). -/ +theorem ridge_exists [ProperSpace E] {f : ℝ × E → ℝ} {Dφ : ℝ → E → E →L[ℝ] ℝ} {U : Set ℝ} + {r δ : ℝ} (hr : 0 < r) + (hconc : ∀ x ∈ U, + StrongConcaveOn (Metric.closedBall (0 : E) (2 * r)) δ (fun y => f (x, y))) + (hD : ∀ x ∈ U, ∀ y ∈ Metric.closedBall (0 : E) (2 * r), + HasFDerivAt (fun y => f (x, y)) (Dφ x y) y) + (hw : ∀ x ∈ U, ‖Dφ x 0‖ < δ * (2 * r)) : + ∃ h : ℝ → E, ∀ x ∈ U, h x ∈ Metric.ball (0 : E) (2 * r) ∧ + HasFDerivAt (fun y => f (x, y)) (0 : E →L[ℝ] ℝ) (h x) := by + have hex : ∀ x : ℝ, ∃ p : E, x ∈ U → p ∈ Metric.ball (0 : E) (2 * r) ∧ + HasFDerivAt (fun y => f (x, y)) (0 : E →L[ℝ] ℝ) p := by + intro x + by_cases hx : x ∈ U + · obtain ⟨p, hp, hdp⟩ := slice_critical_exists (by positivity) (hconc x hx) (hD x hx) (hw x hx) + exact ⟨p, fun _ => ⟨hp, hdp⟩⟩ + · exact ⟨0, fun h => absurd h hx⟩ + choose h hh using hex + exact ⟨h, fun x hx => hh x hx⟩ + end Slice /-! ### A concrete instance and the necessity of each hypothesis @@ -1764,4 +1926,79 @@ theorem h1Toy_capHyp : · simp only [h1ToyF] norm_num + +/-- **`ridge_differentiable` is not vacuous.** For `h1ToyF`, with `h = 0`, transverse gradient +`G (x, y) = -40 y`, its constant derivative `DG = -40 · snd`, `δ = 40` and `U = (-3, 3)`, the +statement lists every hypothesis of `ridge_differentiable` at this instance, and its last +conjunct is that theorem's conclusion, obtained by applying it. -/ +theorem h1Toy_ridge_differentiable : + IsOpen (Ioo (-3 : ℝ) 3) ∧ Icc (-2 * (1 : ℝ)) (2 * 1) ⊆ Ioo (-3) 3 ∧ + (∀ x ∈ Ioo (-3 : ℝ) 3, + StrongConcaveOn (Metric.closedBall (0 : ℝ) (2 * 1)) 40 (fun y => h1ToyF (x, y))) ∧ + (∀ x ∈ Ioo (-3 : ℝ) 3, (0 : ℝ) ∈ Metric.closedBall (0 : ℝ) (2 * 1)) ∧ + (∀ x ∈ Ioo (-3 : ℝ) 3, HasFDerivAt (fun y => h1ToyF (x, y)) (0 : ℝ →L[ℝ] ℝ) 0) ∧ + (∀ x ∈ Icc (-2 * (1 : ℝ)) (2 * 1), (0 : ℝ) ∈ Metric.ball (0 : ℝ) (2 * 1)) ∧ + (∀ x ∈ Icc (-2 * (1 : ℝ)) (2 * 1), ∀ᶠ v in nhds (x, (0 : ℝ)), + HasFDerivAt (fun y => h1ToyF (v.1, y)) (ContinuousLinearMap.mul ℝ ℝ (-40 * v.2)) v.2) ∧ + (∀ x ∈ Icc (-2 * (1 : ℝ)) (2 * 1), + HasStrictFDerivAt (fun p : ℝ × ℝ => ContinuousLinearMap.mul ℝ ℝ (-40 * p.2)) + (((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ) ∘L ContinuousLinearMap.snd ℝ ℝ ℝ) (x, 0)) ∧ + (∀ v : ℝ, ((((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ) ∘L ContinuousLinearMap.snd ℝ ℝ ℝ) ∘L + ContinuousLinearMap.inr ℝ ℝ ℝ) v v ≤ -40 * ‖v‖ ^ 2) ∧ + ∀ x ∈ Icc (-2 * (1 : ℝ)) (2 * 1), HasStrictFDerivAt (fun _ : ℝ => (0 : ℝ)) + (-((((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ) ∘L ContinuousLinearMap.snd ℝ ℝ ℝ) ∘L + ContinuousLinearMap.inr ℝ ℝ ℝ).inverse ∘L + ((((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ) ∘L ContinuousLinearMap.snd ℝ ℝ ℝ) ∘L + ContinuousLinearMap.inl ℝ ℝ ℝ)) x := by + have hslope : ∀ x y : ℝ, HasFDerivAt (fun y : ℝ => h1ToyF (x, y)) + (ContinuousLinearMap.mul ℝ ℝ (-40 * y)) y := by + intro x y + rw [hasFDerivAt_iff_hasDerivAt] + have h1 := ((hasDerivAt_pow 2 y).const_mul 20).const_sub (x ^ 3 / 3 - x / 4) + convert h1 using 1 + · funext t + simp only [h1ToyF] + · simp + ring + have hGs : ∀ p : ℝ × ℝ, HasStrictFDerivAt (fun p : ℝ × ℝ => ContinuousLinearMap.mul ℝ ℝ (-40 * p.2)) + (((-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 hIU : Icc (-2 * (1 : ℝ)) (2 * 1) ⊆ Ioo (-3) 3 := + fun t ht => ⟨by linarith [ht.1], by linarith [ht.2]⟩ + have hconc : ∀ x ∈ Ioo (-3 : ℝ) 3, + StrongConcaveOn (Metric.closedBall (0 : ℝ) (2 * 1)) 40 (fun y => h1ToyF (x, y)) := by + intro t _ + rw [strongConcaveOn_iff_convex] + refine (concaveOn_const (t ^ 3 / 3 - t / 4) (convex_closedBall (0 : ℝ) (2 * 1))).congr ?_ + intro y _ + simp only [h1ToyF, Real.norm_eq_abs, sq_abs] + ring + have hball : ∀ x ∈ Ioo (-3 : ℝ) 3, (0 : ℝ) ∈ Metric.closedBall (0 : ℝ) (2 * 1) := + fun t _ => by simp + have hcrit : ∀ x ∈ Ioo (-3 : ℝ) 3, HasFDerivAt (fun y => h1ToyF (x, y)) (0 : ℝ →L[ℝ] ℝ) 0 := + fun t _ => by simpa using hslope t 0 + have hint : ∀ x ∈ Icc (-2 * (1 : ℝ)) (2 * 1), (0 : ℝ) ∈ Metric.ball (0 : ℝ) (2 * 1) := + fun t _ => by simp + have hG : ∀ x ∈ Icc (-2 * (1 : ℝ)) (2 * 1), ∀ᶠ v in nhds (x, (0 : ℝ)), + HasFDerivAt (fun y => h1ToyF (v.1, y)) (ContinuousLinearMap.mul ℝ ℝ (-40 * v.2)) v.2 := + fun t _ => Filter.Eventually.of_forall (fun v => hslope v.1 v.2) + have hneg : ∀ v : ℝ, ((((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ) ∘L + ContinuousLinearMap.snd ℝ ℝ ℝ) ∘L ContinuousLinearMap.inr ℝ ℝ ℝ) v v ≤ -40 * ‖v‖ ^ 2 := by + intro v + simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.inr_apply, + ContinuousLinearMap.coe_snd', smul_apply, ContinuousLinearMap.mul_apply', smul_eq_mul, + Real.norm_eq_abs, sq_abs] + nlinarith [sq_nonneg v] + refine ⟨isOpen_Ioo, hIU, hconc, hball, hcrit, hint, hG, fun x _ => hGs (x, 0), hneg, ?_⟩ + exact ridge_differentiable (E := ℝ) (f := h1ToyF) + (G := fun p => ContinuousLinearMap.mul ℝ ℝ (-40 * p.2)) + (DG := fun _ => ((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ) ∘L ContinuousLinearMap.snd ℝ ℝ ℝ) + (h := fun _ => (0 : ℝ)) (U := Ioo (-3) 3) (r := 1) (δ := 40) (by norm_num) isOpen_Ioo hIU + hconc hball hcrit hint hG (fun x _ => hGs (x, 0)) (fun _ _ => hneg) + end CapFirstExit diff --git a/frontiers/cap_first_exit_lean_20261002/MANIFEST.json b/frontiers/cap_first_exit_lean_20261002/MANIFEST.json index 17e016736..eae9c2a8e 100644 --- a/frontiers/cap_first_exit_lean_20261002/MANIFEST.json +++ b/frontiers/cap_first_exit_lean_20261002/MANIFEST.json @@ -91,6 +91,12 @@ "CapFirstExit.hessian_increment", "CapFirstExit.slices_strongConcave", "CapFirstExit.ridge_capHyp_H1", + "CapFirstExit.slice_critical_unique", + "CapFirstExit.slice_critical_exists", + "CapFirstExit.isInvertible_of_negDef", + "CapFirstExit.ridge_hasStrictFDerivAt", + "CapFirstExit.ridge_differentiable", + "CapFirstExit.ridge_exists", "CapFirstExit.toyF", "CapFirstExit.toyRidge", "CapFirstExit.toy_ridge_ge", @@ -113,7 +119,8 @@ "CapFirstExit.spToy_capHyp", "CapFirstExit.spToy_normalized", "CapFirstExit.h1ToyF", - "CapFirstExit.h1Toy_capHyp" + "CapFirstExit.h1Toy_capHyp", + "CapFirstExit.h1Toy_ridge_differentiable" ], "expected_axioms": { "CapFirstExit.path_meets_frontier": [ @@ -406,6 +413,36 @@ "Quot.sound", "propext" ], + "CapFirstExit.slice_critical_unique": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.slice_critical_exists": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.isInvertible_of_negDef": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.ridge_hasStrictFDerivAt": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.ridge_differentiable": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.ridge_exists": [ + "Classical.choice", + "Quot.sound", + "propext" + ], "CapFirstExit.toyF": [ "Classical.choice", "Quot.sound", @@ -520,6 +557,11 @@ "Classical.choice", "Quot.sound", "propext" + ], + "CapFirstExit.h1Toy_ridge_differentiable": [ + "Classical.choice", + "Quot.sound", + "propext" ] }, "files": [ @@ -530,18 +572,18 @@ }, { "path": "ALIGNMENT.md", - "bytes": 22998, - "sha256": "73fc8bff14c9eb42650228f905fb229bec6a67725bec166fe1e9738fab84596d" + "bytes": 27594, + "sha256": "d4e601491a5946626e8246772fcb22c4357404809072a85211def4bb522fa486" }, { "path": "CapFirstExit.lean", - "bytes": 93791, - "sha256": "6d4dc00f7d20e2268b39f9b37fbd3fa4326d843678cab6727e73c714b7a25955" + "bytes": 108623, + "sha256": "e15e738d864c06ad71f776940f107c8f2854589c7e246853c5fb8eb7ccfc8223" }, { "path": "README.md", - "bytes": 13713, - "sha256": "0ef7a243688759c71e4b4f2bc6848bbd932440c7fce65c67f0f8453338cd3d71" + "bytes": 15682, + "sha256": "05cb1e63f2d8eb53331c32f3647f6a01f4b3f8a9e569c7958514e9250f5437ec" }, { "path": "gate.py", @@ -566,7 +608,7 @@ { "path": "test_gate.py", "bytes": 6274, - "sha256": "04249947dc69b95b37b7ca5ec8e496e195947983ead8b5e3380dcf0d4265dc46" + "sha256": "45638c157104334c177218754a149cc23336e638a41adfca2648eedc17ac1df1" } ] } diff --git a/frontiers/cap_first_exit_lean_20261002/README.md b/frontiers/cap_first_exit_lean_20261002/README.md index e62ccfd4c..febd58e2b 100644 --- a/frontiers/cap_first_exit_lean_20261002/README.md +++ b/frontiers/cap_first_exit_lean_20261002/README.md @@ -26,14 +26,14 @@ This packet kernel-checks three things: - L1–L2, the Hermite bound `g(a) − g(c) ≤ m(c − a)³/12`, which under the normalization `b − s = r³/6` forces `m ≥ 2`; - since v1.6, L3–L4: the transverse Hessian's increments from its third-derivative bounds `m` (mean value inequality), then the slice strong concavity `δ = λ − 5rm` from SP's Hessian bound at `M`; - L5, the transverse-gradient bound, from the third-derivative bound `m`; - - L7, the transverse maximum and its uniqueness; + - L7, the transverse maximum and its uniqueness; since v1.7 also the existence of the ridge `h` (compactness) and its strict differentiability (Mathlib's implicit function theorem plus uniqueness of the critical point); - L8, the ridge bound; - L11's chain rule; - L18, the curved side. These are derived from L4's output, the strong concavity of each transverse slice. `ridge_capHyp_sp` takes SP's hypotheses with `m ≥ 2` assumed. `ridge_capHyp_normalized` derives `m ≥ 2` from SP's normalization (gap exactly `r³/6`, pins critical, third derivatives bounded by `m`). `ridge_capHyp_H1` (v1.6) also derives `hconc` and `δ > rm(8m − 5)` from SP's hypothesis (H1) `λ > 8rm²`. -The estimate L6, L7's existence and regularity of `h`, and L9–L12 remain hypotheses. +The estimates L6 and L9–L12 (which give `hconv`) remain hypotheses. So do the full-domain ridge premises: the L7 lemmas need the slice data on an open `U ⊇ [−2r, 2r]`, beyond the cap's `x`-range `[−2r, r/2]`, and no declaration composes them with the source route (see [What is not proved here](#what-is-not-proved-here)). In the topological theorems, `X` is any topological space, and nothing is assumed about `f` outside `C` except along the single ridge path. @@ -74,6 +74,9 @@ single ridge path. | `hessian_increment` | L3: derivative bounds `m` on `∂_x H` (along `y = 0`) and on `D_y H` (along rays) give `‖H(p) − H(M)‖ ≤ m(|Δx| + ‖Δy‖)` | | `transverse_hessian_le`, `slices_strongConcave` | L4: `H(M) ≤ −λ` and those increments give `H ≤ −(λ − 5rm)` on the cap, so each slice is `(λ − 5rm)`-strongly concave | | `ridge_capHyp_H1`, `h1ToyF`, `h1Toy_capHyp` | the cap from SP's (H1) `λ > 8rm²` with Hessian data in place of `hconc`; `x³/3 − x/4 − 20y²` (`λ = 40 > 32`) meets every hypothesis | +| `slice_critical_unique`, `slice_critical_exists`, `ridge_exists` | L7 existence: a `δ`-strongly concave slice with `‖∂_y f(x, 0)‖ < δ · 2r` has exactly one critical point, and it lies in the open ball; a ridge map `h` exists | +| `isInvertible_of_negDef`, `ridge_hasStrictFDerivAt`, `ridge_differentiable` | L7 regularity: a negative definite transverse Hessian is invertible, and the implicit function of `∂_y f = 0` agrees with `h`, so `h` is strictly differentiable on `[−2r, 2r]` with `h' = −(∂_y G)⁻¹ ∂_x G` | +| `h1Toy_ridge_differentiable` | every hypothesis of `ridge_differentiable` at `h1ToyF` (`h = 0`, `G = −40y`, `δ = 40`, `U = (−3, 3)`), listed in the proposition itself, and its conclusion | | `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 | @@ -96,10 +99,18 @@ that step. This packet does not formalize: -- the analytic step L6 (the `w'` bound), the existence and implicit-function regularity of the transverse maximizer - `h`, and L9–L12 (the `‖h'‖` and `F''` bounds). These enter `ridge_capHyp_H1`, `ridge_capHyp_of_slices` and +- 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 full-domain ridge premises, and the composition of the L7 lemmas with the source route. `slices_strongConcave` + and `ridge_capHyp_H1` derive or consume the slice data only for `x ∈ [−2r, r/2]`. `ridge_differentiable` needs strong + concavity and critical points on an open `U ⊇ [−2r, 2r]`, and `ridge_exists` needs its derivatives and gradient bound + on the whole of `U`. `ridge_differentiable` also takes `hG`, `hGs` and `hneg` along the ridge on `[−2r, 2r]` as + inputs. SP states L4 on all of `D` (increment `9r/2 < 5r`), but no declaration proves this extension + beyond `r/2` or feeds `ridge_exists` and `ridge_differentiable` into `ridge_inputs_of_joint` and `ridge_capHyp_H1`. + These premises remain inputs; - 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`); @@ -138,7 +149,7 @@ The source gate checks: bound); - rebuilds the package fresh; - replays the module with `leanchecker`; -- prints the axioms of all 81 declarations, requiring exactly the manifest's report: each uses only `propext`, +- prints the axioms of all 88 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 c44063a23..15c1a9a65 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"]), 81) + self.assertEqual(len(m["targets"]), 88) self.assertEqual(m['scientific_effect'], 'NONE') def copy(self):