diff --git a/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md b/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md index 51bc6961d..a77286fb8 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, 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). | +| SP | `reviews/d1_cap_elder_partner_second_pass_claude_20260930/REVIEW.md` | the line-numbered reconstruction of CAP §§2–5. L13, L16, L17 and L19–L22 are proved here. Since v1.5, L1, L2, L5, L7 (maximum and uniqueness), L8, L11's chain rule and L18 are also proved, from SP's normalization and L4's output (`ridge_capHyp_normalized`, `ridge_capHyp_sp`, `ridge_capHyp_of_slices`). Since v1.6, L3–L4 are proved from SP's (H1) and the third-derivative bounds on the transverse Hessian (`ridge_capHyp_H1`). Since v1.7, L7's existence and implicit-function regularity of `h` are proved (`ridge_exists`, `ridge_differentiable`). Since v1.8, L3–L4 are proved on a collar of `D` and the route up to L12 (`hconv`) is composed from SP's source data there (`ridge_capHyp_source`). Inputs that remain: L6 and L9–L12, and the source data themselves (I3). | | 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,14 +67,18 @@ 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 for the cap theorems, but the L7 lemmas need it on an open `U ⊇ [−2r, 2r]`; that extension is not formalized (I3). | +| `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. The L7 lemmas need it on an open `U ⊇ [−2r, 2r]`, which `slices_strongConcave_D` (v1.8) supplies. | | `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_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_capHyp_source` (v1.8) performs this composition, deriving the premises on `U = (−2r − ε, 2r + ε)` and `hG`, `hneg` on `[−2r, 2r]`; `hGs` stays a source-data hypothesis on the collar (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`. | +| `hessian_increment_D` | as `hessian_increment`, on the collar `x ∈ [−2r − ε, 2r + ε]`, `ε > 0` | SP L3 on `D` | The same two mean-value steps; only the `x`-range changes. | +| `transverse_hessian_le_D` | as `transverse_hessian_le`, on the collar, with `0 < ε ≤ r/2` ⇒ `H(p) ≤ −(λ − 5rm)` | SP L4 ("on `D`, `|Δx| + ‖Δy‖ ≤ 9r/2 < 5r`") | On the collar `|x + r/2| ≤ 3r`, so the increment is at most `5r`; `ε ≤ r/2` is exactly what keeps SP's `5r`. | +| `slices_strongConcave_D` | every slice over the collar is `(λ − 5rm)`-strongly concave on `B̄(0, 2r)` | SP L4 (`δ = λ − 5rm` on `D`) | Covers the open `U = (−2r − ε, 2r + ε) ⊇ [−2r, 2r]` that L7 needs. | +| `ridge_capHyp_source` | `[FiniteDimensional ℝ E]`, on the collar `× B̄(0, 2r)`: joint derivative `Df`, strict derivative `DG` of `∂_y f = Df ∘ inr`, transverse Hessian `H` with L3's bounds `m`, (H1) `8rm² < λ` with `H(M) ≤ −λ`, pins `Df(∓r/2, 0) = 0`, the convexity pairs for `∂_x f(·, 0)` on `[−r/2, r/2]` and for `∂_y f(·, 0)` on the collar, gap `f(M) − f(S) = r³/6` ⇒ (i) a ridge exists on `U`; (ii) for every ridge on `U` (critical point in `B̄(0, 2r)`) with `hconv` for `F x = ∂_x f(x, h x)`: `h(∓r/2) = 0`, and (C1)–(C3), (C2⁺) on the cap with `M = (−r/2, 0)`, `z = (2r, h(2r))`, `b = f(M)`, `s = f(S)` | SP §2 normalization, (H1), L1–L5, L7, L8, L11, L16–L20; with L12 as `hconv` | The composition (I3). L5 on the collar gives `‖∂_y f(x, 0)‖ ≤ 3mr² < 2rδ` (`δ > 11rm`). That supplies `ridge_exists`, and through L8 the open-ball condition of `ridge_differentiable`. Uniqueness at the critical pins gives `h(∓r/2) = 0`. `DG ∘ inr = H` holds by uniqueness of derivatives, so it is negative definite. The strict hypothesis `DG` is SP's `f ∈ C²` near the ridge. `hconv` is stated for the ridge it quantifies over, which is unique. | | `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 +111,7 @@ Each necessity theorem is one conjunction, so it certifies its own premises, not The ridge toy has `δ = 2`, below SP's `δ > rm(8m − 5) = 22`. So `spToyF (x, y) = x³/3 − x/4 − 12y²` is added: there `m = 2` (`f_xxx = 2`), `δ = 24`, `w = 0` and the gap is exactly `r³/6`. `spToy_capHyp` shows that every hypothesis of `ridge_capHyp_sp` holds there, so SP's normalized hypotheses are jointly satisfiable. `spToy_normalized` does the same for `ridge_capHyp_normalized`, with `G0 = x² − 1/4`, `|G0''| = 2 = m` and gap exactly `1/6`. -`spToyF` has `λ = 24 < 8rm² = 32`, so it does not meet (H1). `h1ToyF (x, y) = x³/3 − x/4 − 20y²` (v1.6) has a constant transverse Hessian `−40`, so `λ = 40 > 32`, its Hessian increments vanish and the gap is exactly `1/6`. `h1Toy_capHyp` shows that every hypothesis of `ridge_capHyp_H1` holds there. `h1Toy_ridge_differentiable` (v1.7) states every hypothesis of `ridge_differentiable` at `h1ToyF`, with `h = 0`, transverse gradient `−40y`, its derivative `−40 · snd`, `δ = 40` and `U = (−3, 3)`, as conjuncts of its proposition, and derives that theorem's conclusion from them. +`spToyF` has `λ = 24 < 8rm² = 32`, so it does not meet (H1). `h1ToyF (x, y) = x³/3 − x/4 − 20y²` (v1.6) has a constant transverse Hessian `−40`, so `λ = 40 > 32`, its Hessian increments vanish and the gap is exactly `1/6`. `h1Toy_capHyp` shows that every hypothesis of `ridge_capHyp_H1` holds there. `h1Toy_ridge_differentiable` (v1.7) states every hypothesis of `ridge_differentiable` at `h1ToyF`, with `h = 0`, transverse gradient `−40y`, its derivative `−40 · snd`, `δ = 40` and `U = (−3, 3)`, as conjuncts of its proposition, and derives that theorem's conclusion from them. `h1Toy_source` (v1.8) meets every hypothesis of `ridge_capHyp_source` on the collar `ε = 1/2`, with joint derivative `(x² − 1/4, −40y)`, transverse derivative `−40 · snd` and `H = −40`, and the theorem then yields its ridge and, for `h = 0` (`F = x² − 1/4` meets L12), its cap at `M = (−1/2, 0)`. 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 +126,7 @@ illustrates the hypotheses; it is not a model of the planar cap. |---|---|---|---| | I1 | Coordinates: SP's cap is `[-2r, r/2] × B̄(0, 2r)` in a frame `φ` of the periodic lift, and SP's "boundary" is the topological frontier. The transport to the torus (`CapHyp.toTorus`) and the face list (`frontier_cylinder`) are proved; the transport needs no embedding radius | SP §2 | Only the identification of SP's objects with these Lean objects remains. | | I2 | Persistence bookkeeping: in H0 superlevel persistence with distinct critical values, the class born at a local maximum `M` dies at the largest level at which its component contains a strictly higher local maximum (the elder rule) | SP L22, P §8 | This is the definition of the elder pairing. On a compact, locally connected space, Lean proves that this level is `s` (`elder_death_level_peak`). Only the identification of the persistence module's pairing with that definition is informal. | -| I3 | The analytic steps that produce the inputs of `ridge_capHyp_H1` from `G_r`: (H1) `λ > 8rm²`; the slice derivatives and Hessians on the cap, with the third-derivative blocks `∂_x D_y² f` (along `y = 0`) and `D_y³ f` (along rays) bounded by `m`. These bounds are L3's input; L3's increment step itself is proved (`hessian_increment`); `m` as a bound on the third derivatives, which gives the convexity pairs for `G0 = ∂_x f(·, 0)` (L1's input `|g_0'''| ≤ m`) and for `w` (L5's input `‖w''‖ ≤ m`); the critical pins `G0(∓r/2) = 0` and `h(∓r/2) = 0`; L6 (the `w'` bound); for L7, the strict differentiability of the transverse gradient along the ridge (from `f ∈ C²` near `D`), the identification of `G` with the slice gradient on a neighbourhood of each ridge point `(x, h x)`, `x ∈ [−2r, 2r]` (`hG`); the negative definiteness `(DG x ∘ inr) v v ≤ −δ‖v‖²` along the ridge for `x ∈ [−2r, 2r]` (`hneg`), whereas `transverse_hessian_le` gives `H ≤ −(λ − 5rm)` only on the cap (`x ∈ [−2r, r/2]`) and only for the slice Hessians `H`, which no declaration identifies with `DG x ∘ inr`; 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` (since v1.8, `ridge_capHyp_source` derives `hG` from the joint derivative on an open neighbourhood, and `hneg` from `transverse_hessian_le_D` on the collar with `DG ∘ inr = H` along the ridge; `hGs` stays a source-data hypothesis on the collar); with existence and regularity of `h` themselves proved since v1.7; the source data of `ridge_capHyp_source` on the collar `[−2r − ε, 2r + ε] × B̄(0, 2r)`: the derivatives `Df`, `DG`, `H` and the bounds `m` there. SP has `f ∈ C⁴` near `D` and bounds the third derivatives on `D`; on a thin enough collar a bound `m + η` holds by continuity and (H1) stays strict for small `η`. Lean does not prove this step; and L9–L12 (`‖h'‖` and the `F''` bound giving `hconv`) | SP §2 (H1), L6, L7, L9–L12; CAP §§2–5 | These are checked with exact constants by SP's script, not in Lean. Since v1.8 the extension of L4 to the collar and the composition of the L7 lemmas with the cap are proved. Since v1.8, Lean composes L1–L5, L7, L8 and L11 with the cap from the source data on a collar (`ridge_capHyp_source`). Since v1.7, Lean proves L7's existence and regularity of `h`. Since v1.6, Lean proves L3–L4 (from (H1) and the increment bound). Since v1.5, Lean proves L1, L2, L5, L7's maximum and uniqueness, L8, L11's chain rule and L18 from those outputs, and checks SP's constants in the curvature step. L13, L16, L17, L19 and L20 were already proved in v1.4. | | I4 | Theorem A, measurability, `Q^W(G_r^c) ≤ C r³` | P §§7–8, C1, G1 | probability | ## 5. Review contract @@ -139,5 +143,5 @@ row of §4, it says whether the interface is stated correctly. A changed Lean source, toolchain or pin makes an earlier review stale. -v1.5 is additive: it inserts the sections `Slice` and the slice-route toy, and updates the file's header comment. The 53 v1.4 declarations and their statements are unchanged, as the diff against v1.4 shows. The v1.4 alignment review ([5396110365](https://github.com/d6g8k5htny-coder/Math-/pull/246#pullrequestreview-5396110365), `ALIGNED_SCOPED`) therefore still covers the v1.4 rows once a reviewer confirms by diff that they are unchanged. A delta review assesses the new rows: the fourteen slice rows of §2, the v1.5 toy paragraphs of §3 and the revised I3. v1.6 adds five further §2 rows (`strongConcaveOn_of_hessian` to `ridge_capHyp_H1`), the `h1ToyF` paragraph of §3 and a further revision of I3; its 74 v1.5 declarations are unchanged. v1.7 adds six §2 rows (`slice_critical_unique` to `ridge_exists`), the `h1Toy_ridge_differentiable` sentence of §3 and a further revision of I3; its 81 v1.6 declarations are unchanged. A same-provider read, including any Claude +v1.5 is additive: it inserts the sections `Slice` and the slice-route toy, and updates the file's header comment. The 53 v1.4 declarations and their statements are unchanged, as the diff against v1.4 shows. The v1.4 alignment review ([5396110365](https://github.com/d6g8k5htny-coder/Math-/pull/246#pullrequestreview-5396110365), `ALIGNED_SCOPED`) therefore still covers the v1.4 rows once a reviewer confirms by diff that they are unchanged. A delta review assesses the new rows: the fourteen slice rows of §2, the v1.5 toy paragraphs of §3 and the revised I3. v1.6 adds five further §2 rows (`strongConcaveOn_of_hessian` to `ridge_capHyp_H1`), the `h1ToyF` paragraph of §3 and a further revision of I3; its 74 v1.5 declarations are unchanged. v1.7 adds six §2 rows (`slice_critical_unique` to `ridge_exists`), the `h1Toy_ridge_differentiable` sentence of §3 and a further revision of I3; its 81 v1.6 declarations are unchanged. v1.8 adds four §2 rows (`hessian_increment_D` to `ridge_capHyp_source`), the `h1Toy_source` sentence of §3 and a further revision of I3; its 88 v1.7 declarations are unchanged. 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 63d3ac226..35f1e1255 100644 --- a/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean +++ b/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean @@ -19,9 +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. 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 + `ridge_differentiable`), L8, L11's chain rule, L13 and L16–L20 are proved, and since v1.8 + `ridge_capHyp_source` composes them from source data on a collar `[-2r - ε, 2r + ε]` of `D` + (the source data themselves are hypotheses). Also not formalized: the identification of the H0 persistence pairing with the elder rule (L22, P §8); the unstable-branch analysis (L23); and every probabilistic statement. -/ @@ -1427,6 +1427,293 @@ theorem ridge_exists [ProperSpace E] {f : ℝ × E → ℝ} {Dφ : ℝ → E → choose h hh using hex exact ⟨h, fun x hx => hh x hx⟩ +/-! ### The full domain (v1.8) + +SP proves L4 on all of `D`, where the increment from `M` is at most `9r/2 < 5r`, and assumes +`f ∈ C⁴` near `D`. The lemmas below take the source data on a collar `x ∈ [-2r - ε, 2r + ε]`, +`0 < ε ≤ r/2`, where `|x + r/2| ≤ 3r` keeps the increment at most `5r`. So every slice over the open +set `(-2r - ε, 2r + ε) ⊇ [-2r, 2r]` is `(λ - 5rm)`-strongly concave, which is what the L7 lemmas +need, and `ridge_capHyp_source` composes L7 with the cap. -/ + +/-- **L3 on the full domain.** As `hessian_increment`, with the `x`-range `[-2r - ε, 2r + ε]`. -/ +theorem hessian_increment_D {H : ℝ × E → E →L[ℝ] E →L[ℝ] ℝ} {Hx : ℝ → E →L[ℝ] E →L[ℝ] ℝ} + {Hr : ℝ × E → ℝ → E →L[ℝ] E →L[ℝ] ℝ} {r m ε : ℝ} (hr : 0 < r) (hε : 0 < ε) + (hHx : ∀ x ∈ Icc (-2 * r - ε) (2 * r + ε), HasDerivAt (fun t => H (t, 0)) (Hx x) x) + (hHxb : ∀ x ∈ Icc (-2 * r - ε) (2 * r + ε), ‖Hx x‖ ≤ m) + (hHr : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + ∀ s ∈ Icc (0 : ℝ) 1, HasDerivAt (fun s : ℝ => H (p.1, s • p.2)) (Hr p s) s) + (hHrb : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + ∀ s ∈ Icc (0 : ℝ) 1, ‖Hr p s‖ ≤ m * ‖p.2‖) : + ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + ‖H p - H (-r / 2, 0)‖ ≤ m * (|p.1 - -r / 2| + ‖p.2‖) := by + rintro ⟨x, y⟩ hp + have hx := hp.1 + have h1 : ‖H (x, (1 : ℝ) • y) - H (x, (0 : ℝ) • y)‖ ≤ m * ‖y‖ * ‖(1 : ℝ) - 0‖ := + (convex_Icc (0 : ℝ) 1).norm_image_sub_le_of_norm_hasDerivWithin_le + (f := fun s : ℝ => H (x, s • y)) (fun s hs => (hHr (x, y) hp s hs).hasDerivWithinAt) + (fun s hs => hHrb (x, y) hp s hs) (left_mem_Icc.mpr zero_le_one) + (right_mem_Icc.mpr zero_le_one) + have ha : -r / 2 ∈ Icc (-2 * r - ε) (2 * r + ε) := ⟨by linarith, by linarith⟩ + have h2 : ‖H (x, 0) - H (-r / 2, 0)‖ ≤ m * ‖x - -r / 2‖ := + (convex_Icc (-2 * r - ε) (2 * r + ε)).norm_image_sub_le_of_norm_hasDerivWithin_le + (f := fun t => H (t, 0)) (fun t ht => (hHx t ht).hasDerivWithinAt) hHxb ha hx + simp only [one_smul, zero_smul, sub_zero, norm_one, mul_one] at h1 + rw [Real.norm_eq_abs] at h2 + calc ‖H (x, y) - H (-r / 2, 0)‖ ≤ ‖H (x, y) - H (x, 0)‖ + ‖H (x, 0) - H (-r / 2, 0)‖ := + norm_sub_le_norm_sub_add_norm_sub (H (x, y)) (H (x, 0)) (H (-r / 2, 0)) + _ ≤ m * ‖y‖ + m * |x - -r / 2| := add_le_add h1 h2 + _ = m * (|(x, y).1 - -r / 2| + ‖(x, y).2‖) := by simp only; ring + +/-- **L4's Hessian bound on the full domain.** As `transverse_hessian_le`, for +`x ∈ [-2r - ε, 2r + ε]` with `0 < ε ≤ r/2`: there `|x + r/2| ≤ 3r`, so the increment is still at +most `5r`. -/ +theorem transverse_hessian_le_D {H : ℝ × E → E →L[ℝ] E →L[ℝ] ℝ} {r m lam ε : ℝ} + (hm : 0 ≤ m) (hε : 0 < ε) (hεr : ε ≤ r / 2) + (hlip : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + ‖H p - H (-r / 2, 0)‖ ≤ m * (|p.1 - -r / 2| + ‖p.2‖)) + (hlam : ∀ v : E, H (-r / 2, 0) v v ≤ -lam * ‖v‖ ^ 2) : + ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), ∀ v : E, + H p v v ≤ -(lam - 5 * r * m) * ‖v‖ ^ 2 := by + rintro ⟨x, y⟩ ⟨hx, hy⟩ v + have hy' : ‖y‖ ≤ 2 * r := by simpa using hy + have hdx : |x - -r / 2| ≤ 3 * r := by + rw [abs_le]; constructor <;> linarith [hx.1, hx.2] + have hinc : ‖H (x, y) - H (-r / 2, 0)‖ ≤ 5 * r * m := by + have := hlip (x, y) ⟨hx, hy⟩ + calc ‖H (x, y) - H (-r / 2, 0)‖ ≤ m * (|x - -r / 2| + ‖y‖) := this + _ ≤ m * (3 * r + 2 * r) := by gcongr + _ = 5 * r * m := by ring + have hsplit : H (x, y) v v = H (-r / 2, 0) v v + (H (x, y) - H (-r / 2, 0)) v v := by + simp + have hb := (H (x, y) - H (-r / 2, 0)).le_opNorm₂ v v + have hb' : (H (x, y) - H (-r / 2, 0)) v v ≤ 5 * r * m * ‖v‖ ^ 2 := by + have h1 := (le_abs_self _).trans (by simpa [Real.norm_eq_abs] using hb) + calc (H (x, y) - H (-r / 2, 0)) v v ≤ ‖H (x, y) - H (-r / 2, 0)‖ * ‖v‖ * ‖v‖ := h1 + _ ≤ 5 * r * m * ‖v‖ * ‖v‖ := by gcongr + _ = 5 * r * m * ‖v‖ ^ 2 := by ring + rw [hsplit] + have := hlam v + nlinarith + +/-- **L4 on the full domain.** Every slice `y ↦ f (x, y)`, `x ∈ [-2r - ε, 2r + ε]`, is +`(λ - 5rm)`-strongly concave on `B̄(0, 2r)`. -/ +theorem slices_strongConcave_D {f : ℝ × E → ℝ} {Dφ : ℝ × E → E →L[ℝ] ℝ} + {H : ℝ × E → E →L[ℝ] E →L[ℝ] ℝ} {r m lam ε : ℝ} (hm : 0 ≤ m) (hε : 0 < ε) + (hεr : ε ≤ r / 2) + (hD : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + HasFDerivAt (fun y => f (p.1, y)) (Dφ p) p.2) + (hH : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + HasFDerivAt (fun y => Dφ (p.1, y)) (H p) p.2) + (hlip : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + ‖H p - H (-r / 2, 0)‖ ≤ m * (|p.1 - -r / 2| + ‖p.2‖)) + (hlam : ∀ v : E, H (-r / 2, 0) v v ≤ -lam * ‖v‖ ^ 2) : + ∀ x ∈ Icc (-2 * r - ε) (2 * r + ε), + StrongConcaveOn (Metric.closedBall (0 : E) (2 * r)) (lam - 5 * r * m) (fun y => f (x, y)) := by + intro x hx + have hbd := transverse_hessian_le_D hm hε hεr hlip hlam + exact strongConcaveOn_of_hessian (Dφ := fun y => Dφ (x, y)) (H := fun y => H (x, y)) + (convex_closedBall _ _) (fun y hy => hD (x, y) ⟨hx, hy⟩) (fun y hy => hH (x, y) ⟨hx, hy⟩) + (fun y hy v => hbd (x, y) ⟨hx, hy⟩ v) + +/-- **The cap from SP's source data (L1–L5, L7, L8, L11, L18 composed).** Fix a collar +`0 < ε ≤ r/2` and assume, for `x ∈ [-2r - ε, 2r + ε]` and `y ∈ B̄(0, 2r)`: a joint derivative `Df` of `f`, strictly differentiable in +its transverse part `∂_y f = Df ∘ inr` with derivative `DG`; the transverse Hessian `H` with the +third-derivative bounds `m` of L3; (H1) `8rm² < λ` with `H(M) ≤ -λ`; the critical pins +`Df(∓r/2, 0) = 0`; the weak bounds `|∂_x³ f(·, 0)| ≤ m` on `[-r/2, r/2]` (L1) and +`|∂_x² ∂_y f(·, 0)| ≤ m` on the collar (L5); and the gap `f(M) - f(S) = r³/6`. Then: +- a ridge `h` exists: on `(-2r - ε, 2r + ε)`, `h x` is a critical point of its slice in the open + ball; +- for any such ridge (unique by `slice_critical_unique`) with L12's `hconv` for + `F x = ∂_x f(x, h x)`, `h(∓r/2) = 0`, and (C1)–(C3) and (C2⁺) hold on the cap with `M = (-r/2, 0)`, + `S = (r/2, 0)`, `b = f(M)` and `s = f(S)`. + +L8 puts `h` in the open ball on `[-2r, 2r]` (`‖w‖ ≤ 3mr² < 2rδ`); the implicit function theorem +(`ridge_differentiable`) makes `h` differentiable there, with negative definite `DG ∘ inr = H`; +`ridge_inputs_of_joint` gives L11; `ridge_capHyp_H1` gives the cap. Only L12 (`hconv`) remains an +input, with L6 and L9–L11's quantitative bounds that SP uses to prove it. -/ +theorem ridge_capHyp_source [FiniteDimensional ℝ E] {f : ℝ × E → ℝ} + {Df : ℝ × E → ℝ × E →L[ℝ] ℝ} {DG : ℝ × E → ℝ × E →L[ℝ] E →L[ℝ] ℝ} + {H : ℝ × E → E →L[ℝ] E →L[ℝ] ℝ} {Hx : ℝ → E →L[ℝ] E →L[ℝ] ℝ} + {Hr : ℝ × E → ℝ → E →L[ℝ] E →L[ℝ] ℝ} {r m lam ε : ℝ} (hr : 0 < r) (hε : 0 < ε) + (hεr : ε ≤ r / 2) + (hDf : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + HasFDerivAt f (Df p) p) + (hGs : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + HasStrictFDerivAt (fun q => (Df q).comp (ContinuousLinearMap.inr ℝ ℝ E)) (DG p) p) + (hH : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + HasFDerivAt (fun y => (Df (p.1, y)).comp (ContinuousLinearMap.inr ℝ ℝ E)) (H p) p.2) + (hHx : ∀ x ∈ Icc (-2 * r - ε) (2 * r + ε), HasDerivAt (fun t => H (t, 0)) (Hx x) x) + (hHxb : ∀ x ∈ Icc (-2 * r - ε) (2 * r + ε), ‖Hx x‖ ≤ m) + (hHr : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + ∀ s ∈ Icc (0 : ℝ) 1, HasDerivAt (fun s : ℝ => H (p.1, s • p.2)) (Hr p s) s) + (hHrb : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + ∀ s ∈ Icc (0 : ℝ) 1, ‖Hr p s‖ ≤ m * ‖p.2‖) + (hlam : ∀ v : E, H (-r / 2, 0) v v ≤ -lam * ‖v‖ ^ 2) (hH1 : 8 * r * m ^ 2 < lam) + (hM : Df (-r / 2, 0) = 0) (hS : Df (r / 2, 0) = 0) + (hG0cv : ConvexOn ℝ (Icc (-r / 2) (r / 2)) (fun t => Df (t, 0) (1, 0) + m / 2 * t ^ 2)) + (hG0cc : ConcaveOn ℝ (Icc (-r / 2) (r / 2)) (fun t => Df (t, 0) (1, 0) - m / 2 * t ^ 2)) + (hwcv : ∀ v : E, ConvexOn ℝ (Icc (-2 * r - ε) (2 * r + ε)) + (fun t => Df (t, 0) (0, v) + m * ‖v‖ / 2 * t ^ 2)) + (hwcc : ∀ v : E, ConcaveOn ℝ (Icc (-2 * r - ε) (2 * r + ε)) + (fun t => Df (t, 0) (0, v) - m * ‖v‖ / 2 * t ^ 2)) + (hnorm : f (-r / 2, 0) - f (r / 2, 0) = r ^ 3 / 6) : + (∃ h : ℝ → E, ∀ x ∈ Ioo (-2 * r - ε) (2 * r + ε), h x ∈ Metric.ball (0 : E) (2 * r) ∧ + HasFDerivAt (fun y => f (x, y)) (0 : E →L[ℝ] ℝ) (h x)) ∧ + ∀ h : ℝ → E, (∀ x ∈ Ioo (-2 * r - ε) (2 * r + ε), + h x ∈ Metric.closedBall (0 : E) (2 * r) ∧ + HasFDerivAt (fun y => f (x, y)) (0 : E →L[ℝ] ℝ) (h x)) → + ConvexOn ℝ (Icc (-2 * r) (2 * r)) + (fun x => Df (x, h x) (1, 0) - (x + r / 2) * (x - r / 2) / 8) → + h (-r / 2) = 0 ∧ h (r / 2) = 0 ∧ + CapHyp f (Icc (-2 * r) (r / 2) ×ˢ Metric.closedBall (0 : E) (2 * r)) (-r / 2, 0) + (2 * r, h (2 * r)) (f (-r / 2, 0)) (f (r / 2, 0)) ∧ + ∀ x ∈ frontier (Icc (-2 * r) (r / 2) ×ˢ Metric.closedBall (0 : E) (2 * r)), + x ≠ (r / 2, 0) → f x < f (r / 2, 0) := by + have hUX : Ioo (-2 * r - ε) (2 * r + ε) ⊆ Icc (-2 * r - ε) (2 * r + ε) := Ioo_subset_Icc_self + have hcapX : Icc (-2 * r) (r / 2) ⊆ Icc (-2 * r - ε) (2 * r + ε) := + Icc_subset_Icc (by linarith) (by linarith) + have hIU : Icc (-2 * r) (2 * r) ⊆ Ioo (-2 * r - ε) (2 * r + ε) := + fun t ht => ⟨by linarith [ht.1], by linarith [ht.2]⟩ + have h0Y : (0 : E) ∈ Metric.closedBall (0 : E) (2 * r) := Metric.mem_closedBall_self (by positivity) + -- the slice derivatives are the transverse parts of `Df` + have hD : ∀ p ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r), + HasFDerivAt (fun y => f (p.1, y)) ((Df p).comp (ContinuousLinearMap.inr ℝ ℝ E)) p.2 := by + rintro ⟨x, y⟩ hp + exact slice_hasFDerivAt (hDf (x, y) hp) + -- L1–L2: `m ≥ 2` + have hg0 : ∀ x ∈ Icc (-r / 2) (r / 2), + HasDerivAt (fun x => f (x, 0)) (Df (x, 0) (1, 0)) x := by + intro x hx + have hx' : (x, (0 : E)) ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r) := + ⟨⟨by linarith [hx.1], by linarith [hx.2]⟩, h0Y⟩ + have hp : HasDerivAt (fun t : ℝ => (t, (0 : E))) ((1 : ℝ), (0 : E)) x := + (hasDerivAt_id x).prodMk (hasDerivAt_const x (0 : E)) + exact (hDf _ hx').comp_hasDerivAt x hp + have hG0a : Df (-r / 2, 0) (1, 0) = 0 := by simp [hM] + have hG0c : Df (r / 2, 0) (1, 0) = 0 := by simp [hS] + have hm : 2 ≤ m := hermite_m_ge_two (g := fun x => f (x, 0)) hr hg0 hG0cv hG0cc hG0a hG0c hnorm + have hm0 : 0 ≤ m := by linarith + -- L3–L4 on the full domain + have hlip := hessian_increment_D hr hε hHx hHxb hHr hHrb + have hneg := transverse_hessian_le_D hm0 hε hεr hlip hlam + have hconcX := slices_strongConcave_D hm0 hε hεr hD hH hlip hlam + have h11 : 11 * (r * m) < lam - 5 * r * m := by + nlinarith [mul_nonneg (mul_nonneg hr.le hm0) (sub_nonneg.2 hm)] + have hrm : 0 < r * m := mul_pos hr (by linarith) + have hδ0 : 0 < lam - 5 * r * m := by linarith + -- L5 on the full domain: `‖w x‖ ≤ 3mr² < 2rδ` + have hwv : ∀ (t : ℝ) (v : E), + ((Df (t, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)) v = Df (t, 0) (0, v) := fun t v => by simp + have hwcv' : ∀ v : E, ConvexOn ℝ (Icc (-2 * r - ε) (2 * r + ε)) + (fun t => ((Df (t, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)) v + m * ‖v‖ / 2 * t ^ 2) := + fun v => (hwcv v).congr fun t _ => by simp only [hwv] + have hwcc' : ∀ v : E, ConcaveOn ℝ (Icc (-2 * r - ε) (2 * r + ε)) + (fun t => ((Df (t, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)) v - m * ‖v‖ / 2 * t ^ 2) := + fun v => (hwcc v).congr fun t _ => by simp only [hwv] + have hwa : (Df (-r / 2, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E) = 0 := by simp [hM] + have hwc : (Df (r / 2, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E) = 0 := by simp [hS] + have hwlt : ∀ x ∈ Icc (-2 * r - ε) (2 * r + ε), + ‖(Df (x, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)‖ < (lam - 5 * r * m) * (2 * r) := by + intro x hx + have h1 := slice_gradient_bound (w := fun t => (Df (t, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)) + hm0 hwcv' hwcc' (show -r / 2 ∈ Icc (-2 * r - ε) (2 * r + ε) from ⟨by linarith, by linarith⟩) + (show r / 2 ∈ Icc (-2 * r - ε) (2 * r + ε) from ⟨by linarith, by linarith⟩) (by linarith) + hwa hwc hx + have h2 : |(x - -r / 2) * (x - r / 2)| ≤ 6 * r ^ 2 := by + have hxx : 0 ≤ (x - (-2 * r - ε)) * (2 * r + ε - x) := + mul_nonneg (by linarith [hx.1]) (by linarith [hx.2]) + have hee : 0 ≤ (r / 2 - ε) * (9 * r / 2 + ε) := + mul_nonneg (by linarith) (by linarith) + rw [abs_le]; constructor <;> nlinarith [sq_nonneg x, sq_nonneg r] + have h3 : ‖(Df (x, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)‖ ≤ 3 * m * r ^ 2 := + calc ‖(Df (x, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)‖ + ≤ m / 2 * |(x - -r / 2) * (x - r / 2)| := h1 + _ ≤ m / 2 * (6 * r ^ 2) := by gcongr + _ = 3 * m * r ^ 2 := by ring + have h4 : 22 * r * (r * m) < (lam - 5 * r * m) * (2 * r) := by nlinarith + nlinarith + have hslice0 : ∀ x ∈ Icc (-2 * r - ε) (2 * r + ε), + HasFDerivAt (fun y => f (x, y)) ((Df (x, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)) 0 := + fun x hx => hD (x, 0) ⟨hx, h0Y⟩ + refine ⟨ridge_exists (Dφ := fun x y => (Df (x, y)).comp (ContinuousLinearMap.inr ℝ ℝ E)) hr + (fun x hx => hconcX x (hUX hx)) (fun x hx y hy => hD (x, y) ⟨hUX hx, hy⟩) + (fun x hx => hwlt x (hUX hx)), ?_⟩ + intro h hhU hconv + have hball : ∀ x ∈ Ioo (-2 * r - ε) (2 * r + ε), h x ∈ Metric.closedBall (0 : E) (2 * r) := + fun x hx => (hhU x hx).1 + have hcrit : ∀ x ∈ Ioo (-2 * r - ε) (2 * r + ε), + HasFDerivAt (fun y => f (x, y)) (0 : E →L[ℝ] ℝ) (h x) := fun x hx => (hhU x hx).2 + -- L7 uniqueness: the pins are on the ridge + have hMU : -r / 2 ∈ Ioo (-2 * r - ε) (2 * r + ε) := ⟨by linarith, by linarith⟩ + have hSU : r / 2 ∈ Ioo (-2 * r - ε) (2 * r + ε) := ⟨by linarith, by linarith⟩ + have hha : h (-r / 2) = 0 := + slice_critical_unique (hconcX _ (hUX hMU)) hδ0 (hball _ hMU) h0Y (hcrit _ hMU) + (by simpa [hwa] using hslice0 _ (hUX hMU)) + have hhc : h (r / 2) = 0 := + slice_critical_unique (hconcX _ (hUX hSU)) hδ0 (hball _ hSU) h0Y (hcrit _ hSU) + (by simpa [hwc] using hslice0 _ (hUX hSU)) + -- L8: the ridge is in the open ball on `[-2r, 2r]` + have hint : ∀ x ∈ Icc (-2 * r) (2 * r), h x ∈ Metric.ball (0 : E) (2 * r) := by + intro x hx + have hxU := hIU hx + have h8 := slice_ridge_bound (hconcX x (hUX hxU)) h0Y (hball x hxU) (hcrit x hxU) + (hslice0 x (hUX hxU)) + have h9 := hwlt x (hUX hxU) + rw [Metric.mem_ball, dist_zero_right] + have : (lam - 5 * r * m) * ‖h x‖ < (lam - 5 * r * m) * (2 * r) := by linarith + exact lt_of_mul_lt_mul_left this hδ0.le + have hridgeX : ∀ x ∈ Icc (-2 * r) (2 * r), + (x, h x) ∈ Icc (-2 * r - ε) (2 * r + ε) ×ˢ Metric.closedBall (0 : E) (2 * r) := + fun x hx => ⟨hUX (hIU hx), hball x (hIU hx)⟩ + -- L7 regularity: the transverse part of `DG` is `H`, negative definite + have hDGH : ∀ x ∈ Icc (-2 * r) (2 * r), + DG (x, h x) ∘L ContinuousLinearMap.inr ℝ ℝ E = H (x, h x) := by + intro x hx + have h1 : HasFDerivAt (fun y => (Df (x, y)).comp (ContinuousLinearMap.inr ℝ ℝ E)) + ((DG (x, h x)).comp (ContinuousLinearMap.inr ℝ ℝ E)) (h x) := + (hGs _ (hridgeX x hx)).hasFDerivAt.comp (h x) (hasFDerivAt_prodMk_right x (h x)) + exact h1.unique (hH _ (hridgeX x hx)) + have hnegR : ∀ x ∈ Icc (-2 * r) (2 * r), ∀ v : E, + (DG (x, h x) ∘L ContinuousLinearMap.inr ℝ ℝ E) v v ≤ -(lam - 5 * r * m) * ‖v‖ ^ 2 := by + intro x hx v + rw [hDGH x hx] + exact hneg _ (hridgeX x hx) v + have hG : ∀ x ∈ Icc (-2 * r) (2 * r), ∀ᶠ v in 𝓝 (x, h x), + HasFDerivAt (fun y => f (v.1, y)) ((Df v).comp (ContinuousLinearMap.inr ℝ ℝ E)) v.2 := by + intro x hx + have hopen : IsOpen (Ioo (-2 * r - ε) (2 * r + ε) ×ˢ Metric.ball (0 : E) (2 * r)) := + isOpen_Ioo.prod Metric.isOpen_ball + filter_upwards [hopen.mem_nhds ⟨hIU hx, hint x hx⟩] with v hv + exact hD v ⟨hUX hv.1, Metric.ball_subset_closedBall hv.2⟩ + have hstrict := ridge_differentiable (f := f) + (G := fun q => (Df q).comp (ContinuousLinearMap.inr ℝ ℝ E)) (DG := fun x => DG (x, h x)) + (h := h) (U := Ioo (-2 * r - ε) (2 * r + ε)) hδ0 isOpen_Ioo hIU + (fun x hx => hconcX x (hUX hx)) hball hcrit hint hG + (fun x hx => hGs _ (hridgeX x hx)) hnegR + -- L11 + have hDr : ∀ x ∈ Icc (-2 * r) (2 * r), HasFDerivAt f (Df (x, h x)) (x, h x) := + fun x hx => hDf _ (hridgeX x hx) + have hridge : ∀ x ∈ Icc (-2 * r) (2 * r), + (Df (x, h x)).comp (ContinuousLinearMap.inr ℝ ℝ E) = 0 := + fun x hx => (slice_hasFDerivAt (hDr x hx)).unique (hcrit x (hIU hx)) + obtain ⟨hh, hg, -⟩ := ridge_inputs_of_joint hr hDr + (fun x hx => (hstrict x hx).hasFDerivAt.hasDerivAt) hridge + have hFa : Df (-r / 2, h (-r / 2)) (1, 0) = 0 := by simp [hha, hM] + have hFc : Df (r / 2, h (r / 2)) (1, 0) = 0 := by simp [hhc, hS] + have hcap : ∀ x ∈ Icc (-2 * r) (r / 2), x ∈ Ioo (-2 * r - ε) (2 * r + ε) := + fun x hx => ⟨by linarith [hx.1], by linarith [hx.2]⟩ + have key := ridge_capHyp_H1 (w := fun t => (Df (t, 0)).comp (ContinuousLinearMap.inr ℝ ℝ E)) + hr hg0 hG0cv hG0cc hG0a hG0c + (fun p hp => hD p ⟨hcapX hp.1, hp.2⟩) (fun p hp => hH p ⟨hcapX hp.1, hp.2⟩) + (fun x hx => hHx x (hcapX hx)) (fun x hx => hHxb x (hcapX hx)) + (fun p hp => hHr p ⟨hcapX hp.1, hp.2⟩) (fun p hp => hHrb p ⟨hcapX hp.1, hp.2⟩) hlam hH1 + hh hg hFa hFc hconv (fun x hx => hball x (hcap x hx)) (fun x hx => hcrit x (hcap x hx)) + hha hhc (fun x hx => hslice0 x (hcapX hx)) + (fun v => (hwcv' v).subset hcapX (convex_Icc _ _)) + (fun v => (hwcc' v).subset hcapX (convex_Icc _ _)) (by rw [hha, hhc]; exact hnorm) + rw [hha, hhc] at key + exact ⟨hha, hhc, key⟩ + end Slice /-! ### A concrete instance and the necessity of each hypothesis @@ -2001,4 +2288,104 @@ theorem h1Toy_ridge_differentiable : (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) +/-- **`ridge_capHyp_source` is not vacuous.** `h1ToyF` meets every source hypothesis on the full +collar `[-5/2, 5/2] × B̄(0, 2)` (`ε = 1/2`): joint derivative `(x² - 1/4, -40y)`, transverse gradient `-40y` +with derivative `-40 · snd`, constant transverse Hessian `-40`, `m = 2`, `λ = 40 > 32`, pins +`(∓1/2, 0)` and gap `1/6`. The theorem then gives the ridge, and for `h = 0`, which meets L12 +(`F = x² - 1/4`), the cap with `M = (-1/2, 0)`. -/ +theorem h1Toy_source : + (∃ h : ℝ → ℝ, ∀ x ∈ Ioo (-2 * 1 - 1 / 2 : ℝ) (2 * 1 + 1 / 2), h x ∈ Metric.ball (0 : ℝ) (2 * 1) ∧ + HasFDerivAt (fun y => h1ToyF (x, y)) (0 : ℝ →L[ℝ] ℝ) (h x)) ∧ + CapHyp h1ToyF (Icc (-2 * 1) (1 / 2) ×ˢ Metric.closedBall (0 : ℝ) (2 * 1)) (-1 / 2, 0) + (2 * 1, 0) (h1ToyF (-1 / 2, 0)) (h1ToyF (1 / 2, 0)) := by + have hDf : ∀ p : ℝ × ℝ, HasFDerivAt h1ToyF ((p.1 ^ 2 - 1 / 4) • ContinuousLinearMap.fst ℝ ℝ ℝ + + (-40 * p.2) • ContinuousLinearMap.snd ℝ ℝ ℝ) p := by + intro p + have hf : HasFDerivAt (fun q : ℝ × ℝ => q.1) (ContinuousLinearMap.fst ℝ ℝ ℝ) p := + hasFDerivAt_fst + have hs : HasFDerivAt (fun q : ℝ × ℝ => q.2) (ContinuousLinearMap.snd ℝ ℝ ℝ) p := + hasFDerivAt_snd + have h1 := HasFDerivAt.sub (HasFDerivAt.sub + (HasFDerivAt.const_mul (HasFDerivAt.pow hf 3) (1 / 3)) (HasFDerivAt.const_mul hf (1 / 4))) + (HasFDerivAt.const_mul (HasFDerivAt.pow hs 2) 20) + convert h1 using 1 + · funext q + simp only [h1ToyF, Pi.sub_apply] + ring + · ext <;> simp; ring + have hGs : ∀ p : ℝ × ℝ, HasStrictFDerivAt (fun q : ℝ × ℝ => ((q.1 ^ 2 - 1 / 4) • + ContinuousLinearMap.fst ℝ ℝ ℝ + (-40 * q.2) • ContinuousLinearMap.snd ℝ ℝ ℝ).comp + (ContinuousLinearMap.inr ℝ ℝ ℝ)) + (((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ) ∘L ContinuousLinearMap.snd ℝ ℝ ℝ) p := by + intro p + convert (((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ) ∘L + ContinuousLinearMap.snd ℝ ℝ ℝ).hasStrictFDerivAt (x := p) using 1 + funext q + ext + simp + have hH : ∀ p : ℝ × ℝ, HasFDerivAt (fun y => ((p.1 ^ 2 - 1 / 4) • ContinuousLinearMap.fst ℝ ℝ ℝ + + (-40 * y) • ContinuousLinearMap.snd ℝ ℝ ℝ).comp (ContinuousLinearMap.inr ℝ ℝ ℝ)) + ((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ) p.2 := by + intro p + convert ((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ).hasFDerivAt (x := p.2) using 1 + funext y + ext + simp + have hsrc := ridge_capHyp_source (E := ℝ) (f := h1ToyF) + (Df := fun p => (p.1 ^ 2 - 1 / 4) • ContinuousLinearMap.fst ℝ ℝ ℝ + + (-40 * p.2) • ContinuousLinearMap.snd ℝ ℝ ℝ) + (DG := fun _ => ((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ) ∘L ContinuousLinearMap.snd ℝ ℝ ℝ) + (H := fun _ => (-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ) (Hx := fun _ => 0) + (Hr := fun _ _ => 0) (r := 1) (m := 2) (lam := 40) (ε := 1 / 2) one_pos (by norm_num) + (by norm_num) + (fun p _ => hDf p) (fun p _ => hGs p) (fun p _ => hH p) + (fun x _ => hasDerivAt_const x ((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ)) + (fun x _ => by simp only [ContinuousLinearMap.opNorm_zero]; norm_num) + (fun p _ s _ => hasDerivAt_const s ((-40 : ℝ) • ContinuousLinearMap.mul ℝ ℝ)) + (fun p _ s _ => by simp only [ContinuousLinearMap.opNorm_zero]; positivity) + (fun v => by + simp only [smul_apply, ContinuousLinearMap.mul_apply', smul_eq_mul, Real.norm_eq_abs, sq_abs] + nlinarith [sq_nonneg v]) + (by norm_num) (by ext <;> norm_num) (by ext <;> norm_num) ?_ ?_ ?_ ?_ (by simp only [h1ToyF]; norm_num) + · obtain ⟨hex, hcap⟩ := hsrc + have hcrit0 : ∀ x : ℝ, HasFDerivAt (fun y => h1ToyF (x, y)) (0 : ℝ →L[ℝ] ℝ) 0 := by + intro x + have := slice_hasFDerivAt (hDf (x, 0)) + convert this using 1 + ext + simp + have hq : ConvexOn ℝ univ (fun x : ℝ => (7 / 8 : ℝ) • x ^ 2 + (-7 / 32 : ℝ)) := + ((even_two.convexOn_pow).smul (by norm_num)).add (convexOn_const _ convex_univ) + obtain ⟨-, -, hC, -⟩ := hcap (fun _ => 0) (fun x _ => ⟨by simp, hcrit0 x⟩) + ((hq.subset (subset_univ _) (convex_Icc _ _)).congr fun x _ => by + simp only [smul_eq_mul] + simp + ring) + exact ⟨hex, hC⟩ + · have hc : ConvexOn ℝ univ (fun x : ℝ => (2 : ℝ) • x ^ 2 + (-1 / 4 : ℝ)) := + ((even_two.convexOn_pow).smul (by norm_num)).add (convexOn_const _ convex_univ) + refine (hc.subset (subset_univ _) (convex_Icc _ _)).congr ?_ + intro x _ + simp only [smul_eq_mul] + simp + ring + · refine (concaveOn_const (-1 / 4 : ℝ) (convex_Icc _ _)).congr ?_ + intro x _ + simp + ring + · intro v + have hc : ConvexOn ℝ univ (fun t : ℝ => ‖v‖ • t ^ 2) := + (even_two.convexOn_pow).smul (norm_nonneg v) + refine (hc.subset (subset_univ _) (convex_Icc _ _)).congr ?_ + intro t _ + simp only [smul_eq_mul] + simp + · intro v + have hc : ConcaveOn ℝ univ (fun t : ℝ => -(‖v‖ • t ^ 2)) := + ((even_two.convexOn_pow).smul (norm_nonneg v)).neg + refine (hc.subset (subset_univ _) (convex_Icc _ _)).congr ?_ + intro t _ + simp only [smul_eq_mul] + simp + end CapFirstExit diff --git a/frontiers/cap_first_exit_lean_20261002/MANIFEST.json b/frontiers/cap_first_exit_lean_20261002/MANIFEST.json index eae9c2a8e..22694a48a 100644 --- a/frontiers/cap_first_exit_lean_20261002/MANIFEST.json +++ b/frontiers/cap_first_exit_lean_20261002/MANIFEST.json @@ -97,6 +97,10 @@ "CapFirstExit.ridge_hasStrictFDerivAt", "CapFirstExit.ridge_differentiable", "CapFirstExit.ridge_exists", + "CapFirstExit.hessian_increment_D", + "CapFirstExit.transverse_hessian_le_D", + "CapFirstExit.slices_strongConcave_D", + "CapFirstExit.ridge_capHyp_source", "CapFirstExit.toyF", "CapFirstExit.toyRidge", "CapFirstExit.toy_ridge_ge", @@ -120,7 +124,8 @@ "CapFirstExit.spToy_normalized", "CapFirstExit.h1ToyF", "CapFirstExit.h1Toy_capHyp", - "CapFirstExit.h1Toy_ridge_differentiable" + "CapFirstExit.h1Toy_ridge_differentiable", + "CapFirstExit.h1Toy_source" ], "expected_axioms": { "CapFirstExit.path_meets_frontier": [ @@ -443,6 +448,26 @@ "Quot.sound", "propext" ], + "CapFirstExit.hessian_increment_D": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.transverse_hessian_le_D": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.slices_strongConcave_D": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.ridge_capHyp_source": [ + "Classical.choice", + "Quot.sound", + "propext" + ], "CapFirstExit.toyF": [ "Classical.choice", "Quot.sound", @@ -562,6 +587,11 @@ "Classical.choice", "Quot.sound", "propext" + ], + "CapFirstExit.h1Toy_source": [ + "Classical.choice", + "Quot.sound", + "propext" ] }, "files": [ @@ -572,18 +602,18 @@ }, { "path": "ALIGNMENT.md", - "bytes": 27594, - "sha256": "d4e601491a5946626e8246772fcb22c4357404809072a85211def4bb522fa486" + "bytes": 30447, + "sha256": "56e26e4df8a971f079df05228fb252b0dcacf2fab605bcc5991312ce60ef2196" }, { "path": "CapFirstExit.lean", - "bytes": 108623, - "sha256": "e15e738d864c06ad71f776940f107c8f2854589c7e246853c5fb8eb7ccfc8223" + "bytes": 132854, + "sha256": "c68114a718bff7736dadad0f0d96eeba468cea0819f7dfb81729fbf0d4ca80ff" }, { "path": "README.md", - "bytes": 15682, - "sha256": "05cb1e63f2d8eb53331c32f3647f6a01f4b3f8a9e569c7958514e9250f5437ec" + "bytes": 16494, + "sha256": "5b52fd6160139a30944faf6e0da1eb44772f2b623888331ebc618111320b6f15" }, { "path": "gate.py", @@ -608,7 +638,7 @@ { "path": "test_gate.py", "bytes": 6274, - "sha256": "45638c157104334c177218754a149cc23336e638a41adfca2648eedc17ac1df1" + "sha256": "000fe2c5c1daf29a2de30bf0522e737426b5b6eb623e5ad619b82fce93714d3c" } ] } diff --git a/frontiers/cap_first_exit_lean_20261002/README.md b/frontiers/cap_first_exit_lean_20261002/README.md index febd58e2b..3691b0423 100644 --- a/frontiers/cap_first_exit_lean_20261002/README.md +++ b/frontiers/cap_first_exit_lean_20261002/README.md @@ -33,7 +33,12 @@ 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. 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)). +Since v1.8, `ridge_capHyp_source` composes these steps from SP's source data on a collar `[−2r − ε, 2r + ε] × B̄(0, 2r)` of `D` (`0 < ε ≤ r/2`). The data are the derivatives of `f` with the third-derivative bounds `m`, (H1), the critical pins and the gap `r³/6`. From them it proves: +- that a ridge `h` exists, and `h(∓r/2) = 0`; +- L8's interior bound, and the implicit-function regularity of `h` on `[−2r, 2r]`; +- L11, and then (C1)–(C3) and (C2⁺) on the cap. + +The estimates L6 and L9–L12 (which give `hconv`) remain hypotheses. In the topological theorems, `X` is any topological space, and nothing is assumed about `f` outside `C` except along the single ridge path. @@ -77,6 +82,9 @@ single ridge path. | `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 | +| `hessian_increment_D`, `transverse_hessian_le_D`, `slices_strongConcave_D` | L3–L4 on a collar of SP's `D`: on the collar `x ∈ [−2r − ε, 2r + ε]`, `0 < ε ≤ r/2`, the increment is at most `3r + 2r = 5r` (SP: `9r/2 < 5r` on `D`), so every slice is `(λ − 5rm)`-strongly concave | +| `ridge_capHyp_source` | the composed source route (v1.8). From the source data on the collar it proves that a ridge exists on `(−2r − ε, 2r + ε)`. For any such ridge with L12's `hconv`, it proves `h(∓r/2) = 0` and the cap with `M = (−r/2, 0)` and `S = (r/2, 0)`. Inside: L5 gives `‖w‖ ≤ 3mr² < 2rδ`, L8 gives the open ball, `DG ∘ inr = H` is negative definite, the IFT gives `h'`, and then L11 and `ridge_capHyp_H1` follow | +| `h1Toy_source` | `h1ToyF` meets every hypothesis of `ridge_capHyp_source` (`ε = 1/2`, joint derivative `(x² − 1/4, −40y)`); the theorem gives its ridge and its cap | | `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,13 +112,10 @@ 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`. `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 source data themselves. `ridge_capHyp_source` takes, as hypotheses, the derivatives `Df`, `DG` and `H` and the + third-derivative bounds `m` on the collar `[−2r − ε, 2r + ε] × B̄(0, 2r)`. SP has `f ∈ C⁴` near `D` and bounds the + third derivatives on `D`. On a thin enough collar the bound `m + η` holds by continuity, and (H1) stays strict for + small `η`; Lean does not prove this step; - the match between the source's coordinates and the Lean objects: that SP's cap is `[-2r, r/2] × B̄(0, 2r)` in a frame `φ` and that SP analyses the periodic lift. The transport to the torus and the face list are themselves proved (`CapHyp.toTorus`, `frontier_cylinder`); @@ -149,7 +154,7 @@ The source gate checks: bound); - rebuilds the package fresh; - replays the module with `leanchecker`; -- prints the axioms of all 88 declarations, requiring exactly the manifest's report: each uses only `propext`, +- prints the axioms of all 93 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 15c1a9a65..53706a426 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"]), 88) + self.assertEqual(len(m["targets"]), 93) self.assertEqual(m['scientific_effect'], 'NONE') def copy(self):