From f0920c502a49d46c885095ff952b236a77f503a1 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 21:11:32 +0000 Subject: [PATCH 1/3] Cap first exit in Lean v1.7: existence, uniqueness and regularity of the ridge (L7) Stacked on v1.6 (Math-#255). Adds seven declarations (standard axioms only): - slice_critical_unique: a delta-strongly concave slice (delta > 0) has at most one critical point; - slice_critical_exists: with |Df(0)| < delta R the maximum over the compact ball is interior, hence critical (radial derivative < 0 on the sphere from the strong-concavity engine; tangent-cone condition); - isInvertible_of_negDef: a negative definite A : E ->L E ->L R is invertible in finite dimension; - ridge_hasStrictFDerivAt: the implicit function of the transverse gradient (Mathlib implicitFunctionOfProdDomain) is a critical point near h x0, so it equals h, giving h' = -(d_y G)^-1 d_x G; - ridge_differentiable: h strictly differentiable on [-2r, 2r] given the slice data on an open U containing it (f C^4 near D); - ridge_exists: a ridge map h exists on U by choice; - h1Toy_ridge_differentiable: the hypotheses hold for h1ToyF. The 81 v1.6 declarations are unchanged. Interface I3 shrinks to L6 and L9-L12 (hconv) plus the derivative data. Source gate, unit tests (both modes) and --execute (88 declarations, three negative controls) pass locally. Scientific effect NONE. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3 --- .../cap_first_exit_lean_20261002/ALIGNMENT.md | 14 +- .../CapFirstExit.lean | 212 +++++++++++++++++- .../MANIFEST.json | 58 ++++- .../cap_first_exit_lean_20261002/README.md | 14 +- .../cap_first_exit_lean_20261002/test_gate.py | 2 +- 5 files changed, 278 insertions(+), 22 deletions(-) diff --git a/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md b/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md index 1228d4461..fc109f32b 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. | | CAP | `imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md` | the deterministic theorem that SP reconstructs | The source setting (SP §2) is as follows: @@ -69,6 +69,12 @@ The source setting (SP §2) is as follows: | `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. | | `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 supplies `hh'`. | +| `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) shows the same for `ridge_differentiable`, with transverse gradient `−40y`, `δ = 40` and `U = (−3, 3)`. 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`), with existence and regularity of `h` themselves proved since v1.7; 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..0e630efe2 100644 --- a/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean +++ b/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean @@ -16,10 +16,11 @@ 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. 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 +1266,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 +1924,48 @@ theorem h1Toy_capHyp : · simp only [h1ToyF] norm_num + +/-- **`ridge_differentiable` is not vacuous.** For `h1ToyF` (`h = 0`, transverse gradient +`-40 y`, `δ = 40`, `U = (-3, 3)`) every hypothesis holds. -/ +theorem h1Toy_ridge_differentiable : + ∀ x ∈ Icc (-2 * (1 : ℝ)) (2 * 1), + ∃ L : ℝ →L[ℝ] ℝ, HasStrictFDerivAt (fun _ : ℝ => (0 : ℝ)) L 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 + intro x hx + 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 + (fun t ht => ⟨by linarith [ht.1], by linarith [ht.2]⟩) + (fun t _ => by + 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) + (fun t _ => by simp) (fun t _ => by simpa using hslope t 0) (fun t _ => by simp) + (fun t _ => Filter.Eventually.of_forall (fun v => hslope v.1 v.2)) (fun t _ => hGs _) + (fun t _ v => by + 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]) x hx⟩ + end CapFirstExit diff --git a/frontiers/cap_first_exit_lean_20261002/MANIFEST.json b/frontiers/cap_first_exit_lean_20261002/MANIFEST.json index 17e016736..ce84b3838 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": 26128, + "sha256": "03c4c1720fedf0e0ca14a53c5789c4ea03044d16d7a0b6550a727d23721335a5" }, { "path": "CapFirstExit.lean", - "bytes": 93791, - "sha256": "6d4dc00f7d20e2268b39f9b37fbd3fa4326d843678cab6727e73c714b7a25955" + "bytes": 105835, + "sha256": "3a6b335804ac07954f36f1d163b3f9598b7980d47b0d873a9dc6a0a914a8c424" }, { "path": "README.md", - "bytes": 13713, - "sha256": "0ef7a243688759c71e4b4f2bc6848bbd932440c7fce65c67f0f8453338cd3d71" + "bytes": 14585, + "sha256": "32c1401763c41b7b44ff86a8d0b1dc8a56f0a69f13d2873fc8175e9a024c49b4" }, { "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..5cd27be86 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. 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` | the hypotheses of `ridge_differentiable` hold for `h1ToyF` | | `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,8 +99,9 @@ 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 match between the source's coordinates and the Lean objects: that SP's cap is `[-2r, r/2] × B̄(0, 2r)` in a @@ -138,7 +142,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): From 192be0d27be734cc69907ae22a1590b9cbf01b91 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 21:24:37 +0000 Subject: [PATCH 2/3] Cap first exit Lean v1.7: state the toy's hypotheses; list the full-domain ridge premises Answers the two Codex P2 findings on Math-#257. - h1Toy_ridge_differentiable now states, as conjuncts of its proposition, every hypothesis of ridge_differentiable at h1ToyF (h = 0, G = -40y, DG = -40 snd, delta = 40, U = (-3, 3)), and derives that theorem's conclusion from them. Its checked target is no longer the trivial strict differentiability of a constant. - README, ALIGNMENT (SP row, slices_strongConcave and ridge_differentiable rows, toy paragraph, I3) and the file header now list the full-domain ridge premises as unformalized: the L7 lemmas take the slice data on an open U containing [-2r, 2r], while slices_strongConcave and ridge_capHyp_H1 cover only x in [-2r, r/2], and no declaration composes ridge_exists/ridge_differentiable with the source route. 88 declarations, unchanged list; the 81 v1.6 declarations are untouched. Source gate, 18 tests and gate.py --execute (axioms, negative controls) pass. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3 --- .../cap_first_exit_lean_20261002/ALIGNMENT.md | 10 +-- .../CapFirstExit.lean | 77 +++++++++++++------ .../MANIFEST.json | 12 +-- .../cap_first_exit_lean_20261002/README.md | 10 ++- 4 files changed, 74 insertions(+), 35 deletions(-) diff --git a/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md b/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md index fc109f32b..0f1198f7b 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`). Inputs that remain: L6 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,13 +67,13 @@ 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 supplies `hh'`. | +| `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` 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. | @@ -107,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. `h1Toy_ridge_differentiable` (v1.7) shows the same for `ridge_differentiable`, with transverse gradient `−40y`, `δ = 40` and `U = (−3, 3)`. +`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 @@ -122,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); for L7, the strict differentiability of the transverse gradient along the ridge (from `f ∈ C²` near `D`), with existence and regularity of `h` themselves proved since v1.7; 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. | +| 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`), 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 diff --git a/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean b/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean index 0e630efe2..63d3ac226 100644 --- a/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean +++ b/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean @@ -19,7 +19,9 @@ 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. Also not formalized: the + `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. -/ @@ -1925,11 +1927,29 @@ theorem h1Toy_capHyp : norm_num -/-- **`ridge_differentiable` is not vacuous.** For `h1ToyF` (`h = 0`, transverse gradient -`-40 y`, `δ = 40`, `U = (-3, 3)`) every hypothesis holds. -/ +/-- **`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 : - ∀ x ∈ Icc (-2 * (1 : ℝ)) (2 * 1), - ∃ L : ℝ →L[ℝ] ℝ, HasStrictFDerivAt (fun _ : ℝ => (0 : ℝ)) L x := by + 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 @@ -1948,24 +1968,37 @@ theorem h1Toy_ridge_differentiable : funext q ext simp - intro x hx - exact ⟨_, ridge_differentiable (E := ℝ) (f := h1ToyF) + 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 - (fun t ht => ⟨by linarith [ht.1], by linarith [ht.2]⟩) - (fun t _ => by - 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) - (fun t _ => by simp) (fun t _ => by simpa using hslope t 0) (fun t _ => by simp) - (fun t _ => Filter.Eventually.of_forall (fun v => hslope v.1 v.2)) (fun t _ => hGs _) - (fun t _ v => by - 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]) x hx⟩ + (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 ce84b3838..a704b4c93 100644 --- a/frontiers/cap_first_exit_lean_20261002/MANIFEST.json +++ b/frontiers/cap_first_exit_lean_20261002/MANIFEST.json @@ -572,18 +572,18 @@ }, { "path": "ALIGNMENT.md", - "bytes": 26128, - "sha256": "03c4c1720fedf0e0ca14a53c5789c4ea03044d16d7a0b6550a727d23721335a5" + "bytes": 27115, + "sha256": "2225f0cd302587ca45afed146dfcbb7a1ae17152907f8ba47ce1429fa72aed6a" }, { "path": "CapFirstExit.lean", - "bytes": 105835, - "sha256": "3a6b335804ac07954f36f1d163b3f9598b7980d47b0d873a9dc6a0a914a8c424" + "bytes": 108623, + "sha256": "e15e738d864c06ad71f776940f107c8f2854589c7e246853c5fb8eb7ccfc8223" }, { "path": "README.md", - "bytes": 14585, - "sha256": "32c1401763c41b7b44ff86a8d0b1dc8a56f0a69f13d2873fc8175e9a024c49b4" + "bytes": 15579, + "sha256": "f578f8619be63f2aa4a9f852fd40a73fbbc119066f452f814e11ec56b7a03ff8" }, { "path": "gate.py", diff --git a/frontiers/cap_first_exit_lean_20261002/README.md b/frontiers/cap_first_exit_lean_20261002/README.md index 5cd27be86..0dc2d8dc0 100644 --- a/frontiers/cap_first_exit_lean_20261002/README.md +++ b/frontiers/cap_first_exit_lean_20261002/README.md @@ -33,7 +33,7 @@ This packet kernel-checks three things: 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 estimates L6 and L9–L12 (which give `hconv`) 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. @@ -76,7 +76,7 @@ single ridge path. | `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` | the hypotheses of `ridge_differentiable` hold for `h1ToyF` | +| `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 | @@ -104,6 +104,12 @@ This packet does not formalize: 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`. 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`); From 3d1d7fda76eb44090e630d8bc90822020f591253 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 3 Oct 2026 23:28:10 +0000 Subject: [PATCH 3/3] Cap first exit Lean v1.7: K1 AMEND, list hG and hneg among the I3 inputs Applies Grok Bot agent 6's K1 read (Math-#257 comment 5974574796) verbatim: - ALIGNMENT I3 names the identification of G with the slice gradient along the ridge (hG) and the negative definiteness of DG x . inr on [-2r, 2r] (hneg); - the ridge_differentiable row says hG, hGs, hneg on [-2r, 2r] are not derived; - README lists the same inputs. MANIFEST hashes refreshed. CapFirstExit.lean unchanged. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3 --- frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md | 4 ++-- frontiers/cap_first_exit_lean_20261002/MANIFEST.json | 8 ++++---- frontiers/cap_first_exit_lean_20261002/README.md | 3 ++- 3 files changed, 8 insertions(+), 7 deletions(-) diff --git a/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md b/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md index 0f1198f7b..51bc6961d 100644 --- a/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md +++ b/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md @@ -73,7 +73,7 @@ The source setting (SP §2) is as follows: | `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` are not derived from the cap data (I3). | +| `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. | @@ -122,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); for L7, the strict differentiability of the transverse gradient along the ridge (from `f ∈ C²` near `D`), 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. | +| 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 diff --git a/frontiers/cap_first_exit_lean_20261002/MANIFEST.json b/frontiers/cap_first_exit_lean_20261002/MANIFEST.json index a704b4c93..eae9c2a8e 100644 --- a/frontiers/cap_first_exit_lean_20261002/MANIFEST.json +++ b/frontiers/cap_first_exit_lean_20261002/MANIFEST.json @@ -572,8 +572,8 @@ }, { "path": "ALIGNMENT.md", - "bytes": 27115, - "sha256": "2225f0cd302587ca45afed146dfcbb7a1ae17152907f8ba47ce1429fa72aed6a" + "bytes": 27594, + "sha256": "d4e601491a5946626e8246772fcb22c4357404809072a85211def4bb522fa486" }, { "path": "CapFirstExit.lean", @@ -582,8 +582,8 @@ }, { "path": "README.md", - "bytes": 15579, - "sha256": "f578f8619be63f2aa4a9f852fd40a73fbbc119066f452f814e11ec56b7a03ff8" + "bytes": 15682, + "sha256": "05cb1e63f2d8eb53331c32f3647f6a01f4b3f8a9e569c7958514e9250f5437ec" }, { "path": "gate.py", diff --git a/frontiers/cap_first_exit_lean_20261002/README.md b/frontiers/cap_first_exit_lean_20261002/README.md index 0dc2d8dc0..febd58e2b 100644 --- a/frontiers/cap_first_exit_lean_20261002/README.md +++ b/frontiers/cap_first_exit_lean_20261002/README.md @@ -107,7 +107,8 @@ This packet does not formalize: - 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`. SP states L4 on all of `D` (increment `9r/2 < 5r`), but no declaration proves this extension + 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