From 4f2d0484e75115aa22800fa820d7ba1c1b97984c Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 5 Oct 2026 17:56:38 +0000 Subject: [PATCH] Cap first exit in Lean v2.5: the cap under CAP (1) with its partial-block norms MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit CAP §1 (imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md) states the deterministic theorem with the partial-block norms M_j = max_{a+c=j} sup_D ||d_x^a D_y^c f||_op and lambda = lambda_min(-D_y^2 f(M)), under (1): lambda > (4/(3 kappa)) r M_3^2, r M_4 <= 3 kappa/10. ridge_capHyp_K (v2.4) takes the third derivative as one block inequality. Six additive declarations in a new section PartialBlock and a toy: - iteratedFDeriv_three_swap12, iteratedFDeriv_three_swap23: the third derivative of a C^3 function is symmetric (Mathlib has the symmetry of higher derivatives only for analytic functions); - block_of_partial: for a symmetric trilinear form, the partial-block bounds with c = 1, 2, 3 give the block inequality; - ridge_capHyp_blocks: the cap under CAP (1) as written; - mixedToyF, mixedToy_blocks: h1ToyF + x y^2 meets every hypothesis with M3 = 2, M4 = 0, lambda = 41; its mixed block d_x D_y^2 f = 2 is nonzero. The 132 v2.4 statements and lines are unchanged. ALIGNMENT gains three section 2 rows, a section 3 sentence and an I1 revision; README, test_gate (138 targets) and MANIFEST are updated. 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 | 9 +- .../CapFirstExit.lean | 338 ++++++++++++++++++ .../MANIFEST.json | 52 ++- .../cap_first_exit_lean_20261002/README.md | 13 +- .../cap_first_exit_lean_20261002/test_gate.py | 2 +- 5 files changed, 399 insertions(+), 15 deletions(-) diff --git a/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md b/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md index 8f0a5e682..31cbb4973 100644 --- a/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md +++ b/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md @@ -106,6 +106,9 @@ The source setting (SP §2) is as follows: | `iteratedFDeriv_const_mul_of_isOpen` | `U` open, `f` `C⁴` on `U`, `i ≤ 4`, `p ∈ U` ⇒ `D^i(c f)(p) = c · D^i f(p)` | — | Mathlib's `iteratedFDeriv_const_smul_apply'` at a point where `f` is `C^i`; an open `U` supplies that. | | `ridge_capHyp_K` | as `ridge_capHyp_E`, with `0 < k`, the gap `f(M) − f(S) = k r³`, (H1) `(4/(3k)) r m² < λ` and (H2) `r n ≤ 3k/10` in place of `r³/6`, `8rm² < λ` and `rn ≤ 1/20` ⇒ the same conclusion | P §7: `G_r = {λ_min(−A_M) > [4/(3k)] r M3², r M4 ≤ 3k/10}`, with `M3`, `M4` the cap theorem's partial-block norms on the local cylinder and `λ = λ_min(−A_M)` | Applies `ridge_capHyp_E` to `f/(6k)`. Every derivative bound and `λ` are divided by `6k`, and the gap becomes `r³/6`. Then `8r(m/(6k))² < λ/(6k)` ⇔ `(4/(3k)) r m² < λ`, and `r n/(6k) ≤ 1/20` ⇔ `r n ≤ 3k/10`. The case `k = 1/6` is `ridge_capHyp_E`. `λ` enters through `D²f(M)[(0, v), (0, v)] ≤ −λ‖v‖²`, which is `λ_min(−A_M) ≥ λ`; any `λ` strictly between the threshold and `λ_min(−A_M)` works. | | `ridge_capHyp_norm_K` | as `ridge_capHyp_K`, with `‖D³f(p)‖ ≤ M3` and `‖D⁴f(p)‖ ≤ M4` for `p ∈ D` in place of the block hypotheses, and `M3`, `M4` in (H1), (H2) | P §7 (`M3`, `M4` on the local cylinder); P §4 bounds them by `K₀(J_r + ‖A_r‖_F)` | `block_of_norm` gives the block bound. `|D³f[e, e, e]| ≤ ‖D³f‖`, `|D⁴f[e, e, e, e]| ≤ ‖D⁴f‖` and `|D⁴f[(0, v), e, e, e]| ≤ ‖D⁴f‖‖v‖` with `‖e‖ = 1` and `‖(0, v)‖ = ‖v‖` in the max norm on `ℝ × E`. An operator-norm bound implies the block bound, so this event lies inside P's `G_r`. | +| `iteratedFDeriv_three_swap₁₂`, `iteratedFDeriv_three_swap₂₃` | `f` `C³` at `p` ⇒ `D³f(p)[a, b, c] = D³f(p)[b, a, c]` and `D³f(p)[a, b, c] = D³f(p)[a, c, b]` | CAP §1: `∂_x^a D_y^c f` names a block without fixing the order of differentiation | Mathlib proves the symmetry of all iterated derivatives only for analytic functions; for `C²` it has the symmetry of the second derivative (`ContDiffAt.isSymmSndFDerivAt`). The first swap applies that to `Df`, which is `C²` at `p`, through `D³f[a, b, c] = D²(Df)[a, b] c`. The second uses `D³f[a, b, c] = (D(D²f)[a])[b, c]`: `D²f` is symmetric at every point near `p`, so `q ↦ D²f(q)[b, c] − D²f(q)[c, b]` vanishes near `p`, and its derivative at `p` is zero. | +| `block_of_partial` | `B` trilinear on `ℝ × E` and invariant under both swaps, with `|B[(0, y), e, e]| ≤ m‖y‖`, `|B[(0, y₁), (0, y₂), e]| ≤ m‖y₁‖‖y₂‖` and `|B[(0, y₁), (0, y₂), (0, y₃)]| ≤ m‖y₁‖‖y₂‖‖y₃‖` ⇒ the block inequality of `block_of_norm`'s conclusion, with constant `m` | CAP §1: `M₃ = max_{a+c=3} sup_D ‖∂_x^a D_y^c f‖_op`, its blocks with `c = 1, 2, 3` | Multilinear expansion of `B[(s₁, y₁), (s₂, y₂), (s₃, y₃)]` with `(s, y) = s e + (0, y)`. The all-`e` term is the one subtracted. Each of the other seven terms is a partial block in some slot order; the swaps bring it to the canonical order (transverse slots first), where it is bounded by `m` times the product of its `|sᵢ|` and `‖yᵢ‖`. The seven bounds add up to `m(Π(|sᵢ| + ‖yᵢ‖) − Π|sᵢ|)`. No sign of `m` is assumed. | +| `ridge_capHyp_blocks` | as `ridge_capHyp_K`, with the block inequality `hT` replaced by CAP's partial-block bounds on `D` with `M3` for `c = 1, 2, 3`, and `M3`, `M4` in place of `m`, `n` | CAP §1 (1): `λ > (4/(3κ)) r M₃²` and `r M₄ ≤ 3κ/10`, with `M_j` the partial-block norms and `λ = λ_min(−D_y² f(M))`; P §7's `G_r` | `block_of_partial` at each `p ∈ D`, with the swaps at `p`: `f` is `C⁴`, hence `C³`, near `p` because `U` is open. As in `ridge_capHyp_K`, the `c = 0` block of `M₃` is assumed on the pin segment only, and of the fourth derivative only the blocks `c = 0` and `c = 1` (slot order `(0, v), e, e, e`) are assumed. CAP's `M₃` and `M₄` bound all of these, so CAP's (1) implies the hypotheses. CAP's transverse norm is Euclidean; here `E` is any finite-dimensional normed space. | | `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. | @@ -138,7 +141,7 @@ Each necessity theorem is one conjunction, so it certifies its own premises, not The ridge toy has `δ = 2`, below SP's `δ > rm(8m − 5) = 22`. So `spToyF (x, y) = x³/3 − x/4 − 12y²` is added: there `m = 2` (`f_xxx = 2`), `δ = 24`, `w = 0` and the gap is exactly `r³/6`. `spToy_capHyp` shows that every hypothesis of `ridge_capHyp_sp` holds there, so SP's normalized hypotheses are jointly satisfiable. `spToy_normalized` does the same for `ridge_capHyp_normalized`, with `G0 = x² − 1/4`, `|G0''| = 2 = m` and gap exactly `1/6`. -`spToyF` has `λ = 24 < 8rm² = 32`, so it does not meet (H1). `h1ToyF (x, y) = x³/3 − x/4 − 20y²` (v1.6) has a constant transverse Hessian `−40`, so `λ = 40 > 32`, its Hessian increments vanish and the gap is exactly `1/6`. `h1Toy_capHyp` shows that every hypothesis of `ridge_capHyp_H1` holds there. `h1Toy_ridge_differentiable` (v1.7) states every hypothesis of `ridge_differentiable` at `h1ToyF`, with `h = 0`, transverse gradient `−40y`, its derivative `−40 · snd`, `δ = 40` and `U = (−3, 3)`, as conjuncts of its proposition, and derives that theorem's conclusion from them. `h1Toy_source` (v1.8) meets every hypothesis of `ridge_capHyp_source` on the collar `ε = 1/2`, with joint derivative `(x² − 1/4, −40y)`, transverse derivative `−40 · snd` and `H = −40`, and the theorem then yields its ridge and, for `h = 0` (`F = x² − 1/4` meets L12), its cap at `M = (−1/2, 0)`. `h1Toy_C3` (v1.9) meets every hypothesis of `ridge_capHyp_C3`, with `D²f = diag(2x, −40)` and third derivatives `T a b = 2a₁b₁ · fst` (only `f_xxx = 2 ≥ 7/4` is nonzero), and the theorem yields its ridge and cap with no `hconv` supplied. `h1Toy_C4` (v2.0) meets every hypothesis of `ridge_capHyp_C4`, with `f_xxx = 2` constant, so `Φ4 = 0`, both blocks vanish and (H2) holds with `n = 0`. `h1Toy_D` (v2.1) meets every hypothesis of `ridge_capHyp_D` with `ε₀ = 1/2`: `T3` is constant, so `T4 = 0` and `K = 0`, and `|f_xxx| = 2 = m` on the pin segment. The theorem chooses `ε` itself and yields a ridge on `(−2 − ε, 2 + ε)` and the cap. `h1Toy_E` (v2.2) meets every hypothesis of `ridge_capHyp_E` with `U = ℝ²`. `h1ToyF` is a polynomial, `D³f[a, b, c] = 2a₁b₁c₁`, `D⁴f = 0` and `D²f[(0, v), (0, v)] = −40v²`, so `m = 2`, `n = 0` and `λ = 40`; Lean computes these iterated derivatives from the Fréchet derivatives. The theorem yields a ridge on `(−2 − ε, 2 + ε)` for some `ε > 0`, and the cap. `quarticToy_E` (v2.3) does the same away from the degenerate face. `quarticToyF = h1ToyF + (x² − 1/4)²/480` keeps both pins critical and the gap at `1/6`; Lean computes `D³f[a, b, c] = (2 + x/20)a₁b₁c₁` and `D⁴f[a, b, c, d] = a₁b₁c₁d₁/20`. With `r = 1`, `m = 81/40` (the maximum of `|f_xxx|` on the pin segment), `n = 1/20` and `λ = 40`, (H2) holds with equality and (H1) reads `8m² = 32.805 < 40`. So `fxxx_lower` is used with `n > 0` and the collar bound `K` is positive, which answers the optional non-vacuity remarks of K4 (finding 8) and K6 (a). +`spToyF` has `λ = 24 < 8rm² = 32`, so it does not meet (H1). `h1ToyF (x, y) = x³/3 − x/4 − 20y²` (v1.6) has a constant transverse Hessian `−40`, so `λ = 40 > 32`, its Hessian increments vanish and the gap is exactly `1/6`. `h1Toy_capHyp` shows that every hypothesis of `ridge_capHyp_H1` holds there. `h1Toy_ridge_differentiable` (v1.7) states every hypothesis of `ridge_differentiable` at `h1ToyF`, with `h = 0`, transverse gradient `−40y`, its derivative `−40 · snd`, `δ = 40` and `U = (−3, 3)`, as conjuncts of its proposition, and derives that theorem's conclusion from them. `h1Toy_source` (v1.8) meets every hypothesis of `ridge_capHyp_source` on the collar `ε = 1/2`, with joint derivative `(x² − 1/4, −40y)`, transverse derivative `−40 · snd` and `H = −40`, and the theorem then yields its ridge and, for `h = 0` (`F = x² − 1/4` meets L12), its cap at `M = (−1/2, 0)`. `h1Toy_C3` (v1.9) meets every hypothesis of `ridge_capHyp_C3`, with `D²f = diag(2x, −40)` and third derivatives `T a b = 2a₁b₁ · fst` (only `f_xxx = 2 ≥ 7/4` is nonzero), and the theorem yields its ridge and cap with no `hconv` supplied. `h1Toy_C4` (v2.0) meets every hypothesis of `ridge_capHyp_C4`, with `f_xxx = 2` constant, so `Φ4 = 0`, both blocks vanish and (H2) holds with `n = 0`. `h1Toy_D` (v2.1) meets every hypothesis of `ridge_capHyp_D` with `ε₀ = 1/2`: `T3` is constant, so `T4 = 0` and `K = 0`, and `|f_xxx| = 2 = m` on the pin segment. The theorem chooses `ε` itself and yields a ridge on `(−2 − ε, 2 + ε)` and the cap. `h1Toy_E` (v2.2) meets every hypothesis of `ridge_capHyp_E` with `U = ℝ²`. `h1ToyF` is a polynomial, `D³f[a, b, c] = 2a₁b₁c₁`, `D⁴f = 0` and `D²f[(0, v), (0, v)] = −40v²`, so `m = 2`, `n = 0` and `λ = 40`; Lean computes these iterated derivatives from the Fréchet derivatives. The theorem yields a ridge on `(−2 − ε, 2 + ε)` for some `ε > 0`, and the cap. `quarticToy_E` (v2.3) does the same away from the degenerate face. `quarticToyF = h1ToyF + (x² − 1/4)²/480` keeps both pins critical and the gap at `1/6`; Lean computes `D³f[a, b, c] = (2 + x/20)a₁b₁c₁` and `D⁴f[a, b, c, d] = a₁b₁c₁d₁/20`. With `r = 1`, `m = 81/40` (the maximum of `|f_xxx|` on the pin segment), `n = 1/20` and `λ = 40`, (H2) holds with equality and (H1) reads `8m² = 32.805 < 40`. So `fxxx_lower` is used with `n > 0` and the collar bound `K` is positive, which answers the optional non-vacuity remarks of K4 (finding 8) and K6 (a). `mixedToy_blocks` (v2.5) instantiates `ridge_capHyp_blocks` with a nonzero mixed block. `mixedToyF = h1ToyF + xy²` keeps both pins critical and the gap at `1/6`. Lean computes `D³f[a, b, c] = 2a₁b₁c₁ + 2(a₁b₂c₂ + a₂b₁c₂ + a₂b₂c₁)` and `D⁴f = 0`. So the partial blocks of `D³f` are `2, 0, 2, 0` for `c = 0, 1, 2, 3`, `M3 = 2`, `M4 = 0`, and `λ = 41`, since `D_y² f(M) = −40 + 2x = −41` at `x = −1/2`. With `k = 1/6` and `r = 1`, (1) reads `8 M3² = 32 < 41` and `r M4 = 0 ≤ 1/20`. Unlike the earlier toys, the block inequality is not trivial there, since the mixed terms of `D³f` do not vanish. 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 @@ -151,7 +154,7 @@ illustrates the hypotheses; it is not a model of the planar cap. | | Interface | Where it is argued | Why it is outside this packet | |---|---|---|---| -| 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, P §7 | Only the identification of SP's objects with these Lean objects remains. Since v2.4 the gap normalization is proved: P §7 states `G_r` for a pin gap `k r³`, and `ridge_capHyp_K` takes exactly those hypotheses (SP's normalization is `k = 1/6`). | +| 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, P §7 | Only the identification of SP's objects with these Lean objects remains. Since v2.4 the gap normalization is proved: P §7 states `G_r` for a pin gap `k r³`, and `ridge_capHyp_K` takes exactly those hypotheses (SP's normalization is `k = 1/6`). Since v2.5 the norms are CAP's own: `ridge_capHyp_blocks` takes CAP (1) with CAP's partial-block norms `M_j`, and derives the block inequality from them by the symmetry of `D³f`. | | 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`); since v2.1 these pairs and L3's bounds on `∂_x D_y² f` and `D_y³ f` are derived from the block bound and `|f_xxx| ≤ m` on the pin segment (`ridge_capHyp_C5`); the critical pins `G0(∓r/2) = 0` and `h(∓r/2) = 0`; L6 (the `w'` bound; proved since v1.9); for L7, the strict differentiability of the transverse gradient along the ridge (from `f ∈ C²` near `D`), the identification of `G` with the slice gradient on a neighbourhood of each ridge point `(x, h x)`, `x ∈ [−2r, 2r]` (`hG`); the negative definiteness `(DG x ∘ inr) v v ≤ −δ‖v‖²` along the ridge for `x ∈ [−2r, 2r]` (`hneg`), whereas `transverse_hessian_le` gives `H ≤ −(λ − 5rm)` only on the cap (`x ∈ [−2r, r/2]`) and only for the slice Hessians `H`, which no declaration identifies with `DG x ∘ inr` (since v1.8, `ridge_capHyp_source` derives `hG` from the joint derivative on an open neighbourhood, and `hneg` from `transverse_hessian_le_D` on the collar with `DG ∘ inr = H` along the ridge; `hGs` stays a source-data hypothesis on the collar); with existence and regularity of `h` themselves proved since v1.7; the source data of `ridge_capHyp_source` on the collar `[−2r − ε, 2r + ε] × B̄(0, 2r)`: the derivatives `Df`, `DG`, `H` and the bounds `m` there. SP has `f ∈ C⁴` near `D` and bounds the third derivatives on `D`. Since v2.1 Lean proves the continuity step (`block_bound_collar`, `ridge_capHyp_D`). With the block bound `m` on `D`, and some bound `K` on the `x`-derivative of the third derivatives on a collar of width `ε₀`, the bound `m + Kε` holds on the collar of width `ε`, and (H1) stays strict for small `ε`. Since v2.2 the remaining qualitative step is proved too (`ridge_capHyp_E`). `f ∈ C⁴` on an open `U ⊇ D` supplies every derivative datum, a collar inside `U` (`collar_subset_open`) and the bound `K` on `‖D⁴f‖` over the compact collar (by compactness; `block_of_norm` turns it into the block bound). No analytic step of L1–L20 is assumed: of SP's steps L1–L12, the last input, L4's `f_xxx ≥ 7/4` on `D`, is proved since v2.0 (`ridge_capHyp_C4`, from L2's second statement and (H2)). The source data listed in this row stay hypotheses. Since v2.1 (`ridge_capHyp_D`) the quantitative ones are needed on `D` only: the block bound `m`; `|f_xxx| ≤ m` on the pin segment, which the block bound `hT` excludes; SP's block bound `n` on the derivative of `f_xxx`; (H1) and (H2); and, as exact conditions at points of `D`, the critical pins and the gap `r³/6`. On a collar of width `ε₀`, `ridge_capHyp_D` assumes only qualitative data: `Df`, `D2f`, `T3` and its `x`-derivative with some bound `K`, `DG` (strict), `H`, `Hx` and `Hr`. Since v2.2 (`ridge_capHyp_E`) these are derived, and the only assumption off `D` is `f ∈ C⁴` on an open neighbourhood of `D`. | SP §2 (H1), L6, L7, L9–L12; CAP §§2–5 | These are checked with exact constants by SP's script. Since v2.2, Lean derives the collar data, the collar and `K` from `f ∈ C⁴` near `D` (`ridge_capHyp_E`). Since v2.1, Lean derives the six derivative bounds from the block bound and `|f_xxx| ≤ m` on the pin segment, and proves the continuity step from `D` to the collar (`ridge_capHyp_C5`, `ridge_capHyp_D`). Since v2.0, Lean also proves L2's second statement and L4's `f_xxx ≥ 7/4` from (H2) (`ridge_capHyp_C4`). Since v1.9, Lean proves L6, L9 and L12 with SP's constants and derives `hconv` (`ridge_capHyp_C3`). Since v1.8 the extension of L4 to the collar and the composition of the L7 lemmas with the cap are proved. Since v1.8, Lean composes L1–L5, L7, L8 and L11 with the cap from the source data on a collar (`ridge_capHyp_source`). Since v1.7, Lean proves L7's existence and regularity of `h`. Since v1.6, Lean proves L3–L4 (from (H1) and the increment bound). Since v1.5, Lean proves L1, L2, L5, L7's maximum and uniqueness, L8, L11's chain rule and L18 from those outputs, and checks SP's constants in the curvature step. L13, L16, L17, L19 and L20 were already proved in v1.4. | | I4 | Theorem A, measurability, `Q^W(G_r^c) ≤ C r³` | P §§7–8, C1, G1 | probability | @@ -170,5 +173,5 @@ row of §4, it says whether the interface is stated correctly. A changed Lean source, toolchain or pin makes an earlier review stale. -v1.5 is additive: it inserts the sections `Slice` and the slice-route toy, and updates the file's header comment. The 53 v1.4 declarations and their statements are unchanged, as the diff against v1.4 shows. The v1.4 alignment review ([5396110365](https://github.com/d6g8k5htny-coder/Math-/pull/246#pullrequestreview-5396110365), `ALIGNED_SCOPED`) therefore still covers the v1.4 rows once a reviewer confirms by diff that they are unchanged. A delta review assesses the new rows: the fourteen slice rows of §2, the v1.5 toy paragraphs of §3 and the revised I3. v1.6 adds five further §2 rows (`strongConcaveOn_of_hessian` to `ridge_capHyp_H1`), the `h1ToyF` paragraph of §3 and a further revision of I3; its 74 v1.5 declarations are unchanged. v1.7 adds six §2 rows (`slice_critical_unique` to `ridge_exists`), the `h1Toy_ridge_differentiable` sentence of §3 and a further revision of I3; its 81 v1.6 declarations are unchanged. v1.8 adds four §2 rows (`hessian_increment_D` to `ridge_capHyp_source`), the `h1Toy_source` sentence of §3 and a further revision of I3; its 88 v1.7 declarations are unchanged. v1.9 adds nine §2 rows (`convex_deriv_sign` to `ridge_capHyp_C3`, fourteen theorems), the `h1Toy_C3` sentence of §3 and a further revision of the SP row and I3; its 93 v1.8 declarations are unchanged. v2.0 adds four §2 rows (`hermite_gap_le_concave` to `ridge_capHyp_C4`), the `h1Toy_C4` sentence of §3 and a further revision of the SP row and I3; its 108 v1.9 declarations are unchanged. v2.1 adds six §2 rows (`hessian_x_bound` to `ridge_capHyp_D`, seven theorems), the `h1Toy_D` sentence of §3 and a further revision of the SP row and I3; its 113 v2.0 declarations are unchanged. v2.2 adds three §2 rows (`block_of_norm` to `ridge_capHyp_E`), the `h1Toy_E` sentence of §3 and a further revision of the SP row and I3. The statements of its 121 v2.1 declarations are unchanged. The only edits to v2.1 lines are in the header comment and in the docstrings of `ridge_differentiable` and `fxxx_lower`, which take up the wording residuals of the K1, K4 and K5 reads. v2.3 adds the `quarticToy_E` sentence of §3 (two declarations, `quarticToyF` and `quarticToy_E`). Its 125 v2.2 statements are unchanged. Its only edits to v2.2 lines are the two optional wording points deferred from the K6 reads: I3's credit for `K` and the `ridge_differentiable` docstring, which now names `ridge_capHyp_source` as the declaration that performs the composition. It also adds one header line. v2.4 adds five §2 rows (`CapHyp.of_const_mul` to `ridge_capHyp_norm_K`, five declarations) and a revision of I1. Its 127 v2.3 statements and lines are unchanged; it also adds one header paragraph. A same-provider read, including any Claude +v1.5 is additive: it inserts the sections `Slice` and the slice-route toy, and updates the file's header comment. The 53 v1.4 declarations and their statements are unchanged, as the diff against v1.4 shows. The v1.4 alignment review ([5396110365](https://github.com/d6g8k5htny-coder/Math-/pull/246#pullrequestreview-5396110365), `ALIGNED_SCOPED`) therefore still covers the v1.4 rows once a reviewer confirms by diff that they are unchanged. A delta review assesses the new rows: the fourteen slice rows of §2, the v1.5 toy paragraphs of §3 and the revised I3. v1.6 adds five further §2 rows (`strongConcaveOn_of_hessian` to `ridge_capHyp_H1`), the `h1ToyF` paragraph of §3 and a further revision of I3; its 74 v1.5 declarations are unchanged. v1.7 adds six §2 rows (`slice_critical_unique` to `ridge_exists`), the `h1Toy_ridge_differentiable` sentence of §3 and a further revision of I3; its 81 v1.6 declarations are unchanged. v1.8 adds four §2 rows (`hessian_increment_D` to `ridge_capHyp_source`), the `h1Toy_source` sentence of §3 and a further revision of I3; its 88 v1.7 declarations are unchanged. v1.9 adds nine §2 rows (`convex_deriv_sign` to `ridge_capHyp_C3`, fourteen theorems), the `h1Toy_C3` sentence of §3 and a further revision of the SP row and I3; its 93 v1.8 declarations are unchanged. v2.0 adds four §2 rows (`hermite_gap_le_concave` to `ridge_capHyp_C4`), the `h1Toy_C4` sentence of §3 and a further revision of the SP row and I3; its 108 v1.9 declarations are unchanged. v2.1 adds six §2 rows (`hessian_x_bound` to `ridge_capHyp_D`, seven theorems), the `h1Toy_D` sentence of §3 and a further revision of the SP row and I3; its 113 v2.0 declarations are unchanged. v2.2 adds three §2 rows (`block_of_norm` to `ridge_capHyp_E`), the `h1Toy_E` sentence of §3 and a further revision of the SP row and I3. The statements of its 121 v2.1 declarations are unchanged. The only edits to v2.1 lines are in the header comment and in the docstrings of `ridge_differentiable` and `fxxx_lower`, which take up the wording residuals of the K1, K4 and K5 reads. v2.3 adds the `quarticToy_E` sentence of §3 (two declarations, `quarticToyF` and `quarticToy_E`). Its 125 v2.2 statements are unchanged. Its only edits to v2.2 lines are the two optional wording points deferred from the K6 reads: I3's credit for `K` and the `ridge_differentiable` docstring, which now names `ridge_capHyp_source` as the declaration that performs the composition. It also adds one header line. v2.4 adds five §2 rows (`CapHyp.of_const_mul` to `ridge_capHyp_norm_K`, five declarations) and a revision of I1. Its 127 v2.3 statements and lines are unchanged; it also adds one header paragraph. v2.5 adds three §2 rows (`iteratedFDeriv_three_swap₁₂` to `ridge_capHyp_blocks`, four declarations in a new section `PartialBlock`), the `mixedToy_blocks` sentence of §3 (two declarations, `mixedToyF` and `mixedToy_blocks`) and a revision of I1. Its 132 v2.4 statements and lines are unchanged; it also adds one header paragraph. 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 a19c5deb4..123d1a780 100644 --- a/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean +++ b/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean @@ -34,6 +34,10 @@ `f(M) − f(S) = k r³` with `k > 0`, namely `(4/(3k)) r m² < λ` and `r n ≤ 3k/10`, by rescaling `f ↦ f/(6k)` (`ridge_capHyp_E` is the case `k = 1/6`). `ridge_capHyp_norm_K` takes the bounds as operator norms `‖D³f‖ ≤ M3`, `‖D⁴f‖ ≤ M4` on `D`. + Since v2.5 `ridge_capHyp_blocks` takes CAP (1) as written, with CAP's partial-block norms: the + block inequality for `D³f` is derived from the partial blocks (`block_of_partial`), using the + symmetry of `D³f` for `f ∈ C³` (`iteratedFDeriv_three_swap₁₂`, `iteratedFDeriv_three_swap₂₃`). + `mixedToy_blocks` exercises it with a nonzero mixed block `∂_x D_y² f = 2`. 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. @@ -4841,4 +4845,338 @@ theorem ridge_capHyp_norm_K [FiniteDimensional ℝ E] {f : ℝ × E → ℝ} {U end GapK +/-! ### v2.5: CAP (1) in its own partial-block norms + +CAP §1 (`imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md`) states the deterministic +theorem with `M_j = max_{a+c=j} sup_D ‖∂_x^a D_y^c f‖_op` (`c` transverse Euclidean unit vectors, +chosen independently) and `λ = λ_min(−D_y² f(M))`, under (1): `λ > (4/(3κ)) r M_3²`, +`r M_4 ≤ 3κ/10`. `ridge_capHyp_K` takes the third derivative as one block inequality `hT`. +`block_of_partial` derives `hT` from CAP's partial blocks with `c = 1, 2, 3`, using the symmetry of +`D³f`, which holds for `f ∈ C³` (`iteratedFDeriv_three_swap₁₂`, `iteratedFDeriv_three_swap₂₃`). +`ridge_capHyp_blocks` then states the cap under CAP's hypotheses as written. -/ + +section PartialBlock + +open Filter Topology + +variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] + +/-- The third derivative of a `C³` function is symmetric in its first two slots: here +`D³f[a, b, c] = D²(Df)[a, b] c`, and `Df` has a symmetric second derivative. -/ +theorem iteratedFDeriv_three_swap₁₂ {f : F → ℝ} {p : F} (hf : ContDiffAt ℝ 3 f p) (a b c : F) : + iteratedFDeriv ℝ 3 f p ![a, b, c] = iteratedFDeriv ℝ 3 f p ![b, a, c] := by + have h2 : ContDiffAt ℝ 2 (fderiv ℝ f) p := hf.fderiv_right (by norm_num) + have hs : IsSymmSndFDerivAt ℝ (fderiv ℝ f) p := h2.isSymmSndFDerivAt (by simp) + have hr : ∀ x y : F, iteratedFDeriv ℝ 3 f p ![x, y, c] = + iteratedFDeriv ℝ 2 (fderiv ℝ f) p ![x, y] c := by + intro x y + rw [iteratedFDeriv_succ_apply_right] + have e : Fin.init ![x, y, c] = ![x, y] := by ext i; fin_cases i <;> rfl + rw [e] + rfl + rw [hr, hr, IsSymmSndFDerivAt.iteratedFDeriv_cons (hf := hs)] + +/-- The third derivative of a `C³` function is symmetric in its last two slots: here +`D³f[a, b, c] = (D(D²f)[a])[b, c]`, and `D²f` is symmetric on a neighbourhood of `p`, so its +derivative at `p` is symmetric too. -/ +theorem iteratedFDeriv_three_swap₂₃ {f : F → ℝ} {p : F} (hf : ContDiffAt ℝ 3 f p) (a b c : F) : + iteratedFDeriv ℝ 3 f p ![a, b, c] = iteratedFDeriv ℝ 3 f p ![a, c, b] := by + have hev : (fun q => iteratedFDeriv ℝ 2 f q ![b, c]) =ᶠ[𝓝 p] + (fun q => iteratedFDeriv ℝ 2 f q ![c, b]) := by + filter_upwards [hf.eventually (by simp)] with q hq + have hq2 : ContDiffAt ℝ 2 f q := hq.of_le (by norm_num) + exact IsSymmSndFDerivAt.iteratedFDeriv_cons (hf := hq2.isSymmSndFDerivAt (by simp)) + have hd : DifferentiableAt ℝ (iteratedFDeriv ℝ 2 f) p := + (hf.iteratedFDeriv_right (i := 2) (m := 1) (by norm_num)).differentiableAt (by norm_num) + have key : ∀ v : Fin 2 → F, fderiv ℝ (fun q => iteratedFDeriv ℝ 2 f q v) p a = + fderiv ℝ (iteratedFDeriv ℝ 2 f) p a v := by + intro v + have := ((ContinuousMultilinearMap.apply ℝ (fun _ : Fin 2 => F) ℝ v).hasFDerivAt.comp p + hd.hasFDerivAt).fderiv + rw [show (fun q => iteratedFDeriv ℝ 2 f q v) = + (ContinuousMultilinearMap.apply ℝ (fun _ : Fin 2 => F) ℝ v) ∘ iteratedFDeriv ℝ 2 f from rfl, + this] + rfl + rw [iteratedFDeriv_succ_apply_left, iteratedFDeriv_succ_apply_left] + have t1 : Fin.tail ![a, b, c] = ![b, c] := by ext i; fin_cases i <;> rfl + have t2 : Fin.tail ![a, c, b] = ![c, b] := by ext i; fin_cases i <;> rfl + simp only [Matrix.cons_val_zero, t1, t2] + rw [← key, ← key, hev.fderiv_eq] + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + +/-- **CAP's partial blocks give the block inequality.** For a symmetric trilinear form `B` on +`ℝ × E`, bounds by `m` on the three partial blocks with `c = 1, 2, 3` transverse slots, namely +`|B[(0, y), e, e]| ≤ m‖y‖`, `|B[(0, y₁), (0, y₂), e]| ≤ m‖y₁‖‖y₂‖` and +`|B[(0, y₁), (0, y₂), (0, y₃)]| ≤ m‖y₁‖‖y₂‖‖y₃‖` with `e = (1, 0)`, give the block inequality `hT` of +`ridge_capHyp_E` and `ridge_capHyp_K`. The proof expands `B[(s₁, y₁), (s₂, y₂), (s₃, y₃)]` +multilinearly: the seven mixed terms are partial blocks in some slot order, symmetry brings each to +the canonical order, and their bounds add up to `m(Π(|sᵢ| + ‖yᵢ‖) − Π|sᵢ|)`. No sign of `m` is +assumed. -/ +theorem block_of_partial {B : ContinuousMultilinearMap ℝ (fun _ : Fin 3 => ℝ × E) ℝ} {m : ℝ} + (hs₁₂ : ∀ a b c : ℝ × E, B ![a, b, c] = B ![b, a, c]) + (hs₂₃ : ∀ a b c : ℝ × E, B ![a, b, c] = B ![a, c, b]) + (k₁ : ∀ y : E, |B ![((0 : ℝ), y), (1, 0), (1, 0)]| ≤ m * ‖y‖) + (k₂ : ∀ y₁ y₂ : E, |B ![((0 : ℝ), y₁), (0, y₂), (1, 0)]| ≤ m * ‖y₁‖ * ‖y₂‖) + (k₃ : ∀ y₁ y₂ y₃ : E, |B ![((0 : ℝ), y₁), (0, y₂), (0, y₃)]| ≤ m * ‖y₁‖ * ‖y₂‖ * ‖y₃‖) + (s₁ s₂ s₃ : ℝ) (y₁ y₂ y₃ : E) : + |B ![(s₁, y₁), (s₂, y₂), (s₃, y₃)] - s₁ * s₂ * s₃ * B ![(1, 0), (1, 0), (1, 0)]| ≤ + m * ((|s₁| + ‖y₁‖) * (|s₂| + ‖y₂‖) * (|s₃| + ‖y₃‖) - |s₁| * |s₂| * |s₃|) := by + have hu0 : ∀ x b c z : ℝ × E, Function.update ![x, b, c] 0 z = ![z, b, c] := fun _ _ _ _ => by + funext i; fin_cases i <;> simp + have hu1 : ∀ a x c z : ℝ × E, Function.update ![a, x, c] 1 z = ![a, z, c] := fun _ _ _ _ => by + funext i; fin_cases i <;> simp + have hu2 : ∀ a b x z : ℝ × E, Function.update ![a, b, x] 2 z = ![a, b, z] := fun _ _ _ _ => by + funext i; fin_cases i <;> simp + have a₁ : ∀ x x' b c : ℝ × E, B ![x + x', b, c] = B ![x, b, c] + B ![x', b, c] := by + intro x x' b c + have := B.map_update_add ![x, b, c] 0 x x' + rwa [hu0, hu0, hu0] at this + have a₂ : ∀ a x x' c : ℝ × E, B ![a, x + x', c] = B ![a, x, c] + B ![a, x', c] := by + intro a x x' c + have := B.map_update_add ![a, x, c] 1 x x' + rwa [hu1, hu1, hu1] at this + have a₃ : ∀ a b x x' : ℝ × E, B ![a, b, x + x'] = B ![a, b, x] + B ![a, b, x'] := by + intro a b x x' + have := B.map_update_add ![a, b, x] 2 x x' + rwa [hu2, hu2, hu2] at this + have m₁ : ∀ (t : ℝ) (x b c : ℝ × E), B ![t • x, b, c] = t * B ![x, b, c] := by + intro t x b c + have := B.map_update_smul ![x, b, c] 0 t x + rwa [hu0, hu0, smul_eq_mul] at this + have m₂ : ∀ (t : ℝ) (a x c : ℝ × E), B ![a, t • x, c] = t * B ![a, x, c] := by + intro t a x c + have := B.map_update_smul ![a, x, c] 1 t x + rwa [hu1, hu1, smul_eq_mul] at this + have m₃ : ∀ (t : ℝ) (a b x : ℝ × E), B ![a, b, t • x] = t * B ![a, b, x] := by + intro t a b x + have := B.map_update_smul ![a, b, x] 2 t x + rwa [hu2, hu2, smul_eq_mul] at this + set e : ℝ × E := ((1 : ℝ), (0 : E)) with he_def + have hsp : ∀ (s : ℝ) (y : E), ((s, y) : ℝ × E) = s • e + ((0 : ℝ), y) := by + intro s y; ext <;> simp [he_def] + set P₁ := |s₁| + ‖y₁‖ + set P₂ := |s₂| + ‖y₂‖ + set P₃ := |s₃| + ‖y₃‖ + -- the multilinear expansion + have expand : B ![(s₁, y₁), (s₂, y₂), (s₃, y₃)] - s₁ * s₂ * s₃ * B ![e, e, e] = + (s₂ * s₃ * B ![((0 : ℝ), y₁), e, e] + s₂ * B ![((0 : ℝ), y₁), e, (0, y₃)] + + s₃ * B ![((0 : ℝ), y₁), (0, y₂), e] + B ![((0 : ℝ), y₁), (0, y₂), (0, y₃)]) + + (s₁ * s₃ * B ![e, ((0 : ℝ), y₂), e] + s₁ * B ![e, ((0 : ℝ), y₂), (0, y₃)]) + + s₁ * s₂ * B ![e, e, ((0 : ℝ), y₃)] := by + rw [hsp s₁ y₁, hsp s₂ y₂, hsp s₃ y₃] + simp only [a₁, a₂, a₃, m₁, m₂, m₃] + ring + rw [he_def] at expand ⊢ + rw [expand] + -- the seven partial blocks, brought to the canonical order by symmetry + have b₁ := k₁ y₁ + have b₂ : |B ![((0 : ℝ), y₁), (1, 0), (0, y₃)]| ≤ m * ‖y₁‖ * ‖y₃‖ := by + rw [hs₂₃]; exact k₂ y₁ y₃ + have b₃ := k₂ y₁ y₂ + have b₄ := k₃ y₁ y₂ y₃ + have b₅ : |B ![(1, 0), ((0 : ℝ), y₂), (1, 0)]| ≤ m * ‖y₂‖ := by + rw [hs₁₂]; exact k₁ y₂ + have b₆ : |B ![(1, 0), ((0 : ℝ), y₂), (0, y₃)]| ≤ m * ‖y₂‖ * ‖y₃‖ := by + rw [hs₁₂, hs₂₃]; exact k₂ y₂ y₃ + have b₇ : |B ![(1, 0), (1, 0), ((0 : ℝ), y₃)]| ≤ m * ‖y₃‖ := by + rw [hs₂₃, hs₁₂]; exact k₁ y₃ + have hP : m * (P₁ * P₂ * P₃ - |s₁| * |s₂| * |s₃|) = + (|s₂| * |s₃| * (m * ‖y₁‖) + |s₂| * (m * ‖y₁‖ * ‖y₃‖) + |s₃| * (m * ‖y₁‖ * ‖y₂‖) + + m * ‖y₁‖ * ‖y₂‖ * ‖y₃‖) + + (|s₁| * |s₃| * (m * ‖y₂‖) + |s₁| * (m * ‖y₂‖ * ‖y₃‖)) + |s₁| * |s₂| * (m * ‖y₃‖) := by + simp only [P₁, P₂, P₃]; ring + rw [hP] + refine (abs_add_le _ _).trans (add_le_add ((abs_add_le _ _).trans (add_le_add + ((abs_add_le _ _).trans (add_le_add ((abs_add_le _ _).trans (add_le_add + ((abs_add_le _ _).trans (add_le_add ?_ ?_)) ?_)) ?_)) ((abs_add_le _ _).trans + (add_le_add ?_ ?_)))) ?_) + · rw [abs_mul, abs_mul]; exact mul_le_mul_of_nonneg_left b₁ (by positivity) + · rw [abs_mul]; exact mul_le_mul_of_nonneg_left b₂ (abs_nonneg _) + · rw [abs_mul]; exact mul_le_mul_of_nonneg_left b₃ (abs_nonneg _) + · exact b₄ + · rw [abs_mul, abs_mul]; exact mul_le_mul_of_nonneg_left b₅ (by positivity) + · rw [abs_mul]; exact mul_le_mul_of_nonneg_left b₆ (abs_nonneg _) + · rw [abs_mul, abs_mul]; exact mul_le_mul_of_nonneg_left b₇ (by positivity) + +/-- **The cap under CAP (1) as written.** `f ∈ C⁴` on an open `U ⊇ D`; CAP's partial-block bounds +on `D` with `M3` for `c = 1, 2, 3` transverse slots, and for `c = 0` on the pin segment only (CAP +bounds it on all of `D`); the two partial blocks of the fourth derivative that the proof uses, +`c = 0` and `c = 1`, with `M4`; the transverse curvature `λ` at `M`; and (1), +`(4/(3k)) r M3² < λ` and `r M4 ≤ 3k/10`, for the pin gap `k r³`. The conclusion is that of +`ridge_capHyp_K`. -/ +theorem ridge_capHyp_blocks [FiniteDimensional ℝ E] {f : ℝ × E → ℝ} {U : Set (ℝ × E)} + {r k M3 M4 lam : ℝ} (hr : 0 < r) (hk : 0 < k) (hU : IsOpen U) + (hDU : Icc (-2 * r) (2 * r) ×ˢ Metric.closedBall (0 : E) (2 * r) ⊆ U) + (hf : ContDiffOn ℝ 4 f U) + (h30 : ∀ x ∈ Icc (-r / 2) (r / 2), |iteratedFDeriv ℝ 3 f (x, 0) ![(1, 0), (1, 0), (1, 0)]| ≤ M3) + (h31 : ∀ p ∈ Icc (-2 * r) (2 * r) ×ˢ Metric.closedBall (0 : E) (2 * r), ∀ y : E, + |iteratedFDeriv ℝ 3 f p ![(0, y), (1, 0), (1, 0)]| ≤ M3 * ‖y‖) + (h32 : ∀ p ∈ Icc (-2 * r) (2 * r) ×ˢ Metric.closedBall (0 : E) (2 * r), ∀ y₁ y₂ : E, + |iteratedFDeriv ℝ 3 f p ![(0, y₁), (0, y₂), (1, 0)]| ≤ M3 * ‖y₁‖ * ‖y₂‖) + (h33 : ∀ p ∈ Icc (-2 * r) (2 * r) ×ˢ Metric.closedBall (0 : E) (2 * r), ∀ y₁ y₂ y₃ : E, + |iteratedFDeriv ℝ 3 f p ![(0, y₁), (0, y₂), (0, y₃)]| ≤ M3 * ‖y₁‖ * ‖y₂‖ * ‖y₃‖) + (h40 : ∀ p ∈ Icc (-2 * r) (2 * r) ×ˢ Metric.closedBall (0 : E) (2 * r), + |iteratedFDeriv ℝ 4 f p ![(1, 0), (1, 0), (1, 0), (1, 0)]| ≤ M4) + (h41 : ∀ p ∈ Icc (-2 * r) (2 * r) ×ˢ Metric.closedBall (0 : E) (2 * r), ∀ v : E, + |iteratedFDeriv ℝ 4 f p ![(0, v), (1, 0), (1, 0), (1, 0)]| ≤ M4 * ‖v‖) + (hlam : ∀ v : E, iteratedFDeriv ℝ 2 f (-r / 2, 0) ![(0, v), (0, v)] ≤ -lam * ‖v‖ ^ 2) + (hH1 : 4 / (3 * k) * r * M3 ^ 2 < lam) (hH2 : r * M4 ≤ 3 * k / 10) + (hM : fderiv ℝ f (-r / 2, 0) = 0) (hS : fderiv ℝ f (r / 2, 0) = 0) + (hnorm : f (-r / 2, 0) - f (r / 2, 0) = k * r ^ 3) : + ∃ ε, 0 < ε ∧ + (∃ h : ℝ → E, ∀ x ∈ Ioo (-2 * r - ε) (2 * r + ε), h x ∈ Metric.ball (0 : E) (2 * r) ∧ + HasFDerivAt (fun y => f (x, y)) (0 : E →L[ℝ] ℝ) (h x)) ∧ + ∀ h : ℝ → E, (∀ x ∈ Ioo (-2 * r - ε) (2 * r + ε), + h x ∈ Metric.closedBall (0 : E) (2 * r) ∧ + HasFDerivAt (fun y => f (x, y)) (0 : E →L[ℝ] ℝ) (h x)) → + h (-r / 2) = 0 ∧ h (r / 2) = 0 ∧ + CapHyp f (Icc (-2 * r) (r / 2) ×ˢ Metric.closedBall (0 : E) (2 * r)) (-r / 2, 0) + (2 * r, h (2 * r)) (f (-r / 2, 0)) (f (r / 2, 0)) ∧ + ∀ x ∈ frontier (Icc (-2 * r) (r / 2) ×ˢ Metric.closedBall (0 : E) (2 * r)), + x ≠ (r / 2, 0) → f x < f (r / 2, 0) := by + refine ridge_capHyp_K hr hk hU hDU hf (fun p hp s₁ s₂ s₃ y₁ y₂ y₃ => ?_) h30 h40 h41 hH2 hlam + hH1 hM hS hnorm + have hp3 : ContDiffAt ℝ 3 f p := (hf.contDiffAt (hU.mem_nhds (hDU hp))).of_le (by norm_num) + exact block_of_partial (iteratedFDeriv_three_swap₁₂ hp3) (iteratedFDeriv_three_swap₂₃ hp3) + (h31 p hp) (h32 p hp) (h33 p hp) s₁ s₂ s₃ y₁ y₂ y₃ + +end PartialBlock + +/-- A toy with a nonzero mixed block. `x³/3 − x/4 − 20y²` plus `xy²`: the pins and the gap `1/6` are +unchanged, and `∂_x D_y² f = 2`. -/ +noncomputable def mixedToyF (p : ℝ × ℝ) : ℝ := + p.1 ^ 3 / 3 - p.1 / 4 - 20 * p.2 ^ 2 + p.1 * p.2 ^ 2 + +/-- **`ridge_capHyp_blocks` with a nonzero mixed block.** On `mixedToyF` the partial blocks of +`D³f` are `2` (`c = 0`), `0` (`c = 1`), `2` (`c = 2`, the mixed block `∂_x D_y² f`) and `0` +(`c = 3`), so `M3 = 2`; `D⁴f = 0`, so `M4 = 0`; and `λ = 41`. CAP (1) holds with `k = 1/6`, `r = 1`: +`8 M3² = 32 < 41` and `r M4 = 0 ≤ 1/20`. Unlike `h1Toy_E` and `quarticToy_E`, the block inequality +`hT` is not trivial here, since the mixed terms of `D³f` do not vanish. -/ +theorem mixedToy_blocks : + (∃ ε > 0, ∃ h : ℝ → ℝ, ∀ x ∈ Ioo (-2 * 1 - ε : ℝ) (2 * 1 + ε), h x ∈ Metric.ball (0 : ℝ) (2 * 1) ∧ + HasFDerivAt (fun y => mixedToyF (x, y)) (0 : ℝ →L[ℝ] ℝ) (h x)) ∧ + CapHyp mixedToyF (Icc (-2 * 1) (1 / 2) ×ˢ Metric.closedBall (0 : ℝ) (2 * 1)) (-1 / 2, 0) + (2 * 1, 0) (mixedToyF (-1 / 2, 0)) (mixedToyF (1 / 2, 0)) := by + have hf : ∀ p : ℝ × ℝ, HasFDerivAt (fun q : ℝ × ℝ => q.1) (ContinuousLinearMap.fst ℝ ℝ ℝ) p := + fun p => hasFDerivAt_fst + have hs : ∀ p : ℝ × ℝ, HasFDerivAt (fun q : ℝ × ℝ => q.2) (ContinuousLinearMap.snd ℝ ℝ ℝ) p := + fun p => hasFDerivAt_snd + have hDf : ∀ p : ℝ × ℝ, HasFDerivAt mixedToyF + ((p.1 ^ 2 - 1 / 4 + p.2 ^ 2) • ContinuousLinearMap.fst ℝ ℝ ℝ + + (-40 * p.2 + 2 * p.1 * p.2) • ContinuousLinearMap.snd ℝ ℝ ℝ) p := by + intro p + have h1 := HasFDerivAt.add (HasFDerivAt.sub (HasFDerivAt.sub + (HasFDerivAt.const_mul (HasFDerivAt.pow (hf p) 3) (1 / 3)) + (HasFDerivAt.const_mul (hf p) (1 / 4))) + (HasFDerivAt.const_mul (HasFDerivAt.pow (hs p) 2) 20)) + (HasFDerivAt.mul (hf p) (HasFDerivAt.pow (hs p) 2)) + convert h1 using 1 + · funext q + simp only [mixedToyF, Pi.sub_apply, Pi.add_apply, Pi.mul_apply] + ring + · ext <;> simp + ring + have hD2 : ∀ p : ℝ × ℝ, HasFDerivAt (fun q : ℝ × ℝ => (q.1 ^ 2 - 1 / 4 + q.2 ^ 2) • + ContinuousLinearMap.fst ℝ ℝ ℝ + (-40 * q.2 + 2 * q.1 * q.2) • ContinuousLinearMap.snd ℝ ℝ ℝ) + (((2 * p.1) • ContinuousLinearMap.fst ℝ ℝ ℝ + (2 * p.2) • ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight + (ContinuousLinearMap.fst ℝ ℝ ℝ) + + ((2 * p.2) • ContinuousLinearMap.fst ℝ ℝ ℝ + + (-40 + 2 * p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight + (ContinuousLinearMap.snd ℝ ℝ ℝ)) p := by + intro p + have h1 : HasFDerivAt (fun q : ℝ × ℝ => q.1 ^ 2 - 1 / 4 + q.2 ^ 2) + ((2 * p.1) • ContinuousLinearMap.fst ℝ ℝ ℝ + (2 * p.2) • ContinuousLinearMap.snd ℝ ℝ ℝ) p := by + have := ((HasFDerivAt.pow (hf p) 2).sub_const (1 / 4)).add (HasFDerivAt.pow (hs p) 2) + convert this using 1 + ext <;> simp + have h2 : HasFDerivAt (fun q : ℝ × ℝ => -40 * q.2 + 2 * q.1 * q.2) + ((2 * p.2) • ContinuousLinearMap.fst ℝ ℝ ℝ + (-40 + 2 * p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ) + p := by + have := (HasFDerivAt.const_mul (hs p) (-40)).add + ((HasFDerivAt.const_mul (hf p) 2).mul (hs p)) + convert this using 1 + ext <;> simp + ring + exact (h1.smul_const (ContinuousLinearMap.fst ℝ ℝ ℝ)).add + (h2.smul_const (ContinuousLinearMap.snd ℝ ℝ ℝ)) + have hcd : ContDiff ℝ 4 mixedToyF := by unfold mixedToyF; fun_prop + have hfd : fderiv ℝ mixedToyF = fun p => (p.1 ^ 2 - 1 / 4 + p.2 ^ 2) • + ContinuousLinearMap.fst ℝ ℝ ℝ + (-40 * p.2 + 2 * p.1 * p.2) • ContinuousLinearMap.snd ℝ ℝ ℝ := + funext fun p => (hDf p).fderiv + have h2 : ∀ (y : ℝ × ℝ) (m : Fin 2 → ℝ × ℝ), iteratedFDeriv ℝ 2 mixedToyF y m = + 2 * y.1 * (m 0).1 * (m 1).1 + 2 * y.2 * ((m 0).1 * (m 1).2 + (m 0).2 * (m 1).1) + + (-40 + 2 * y.1) * (m 0).2 * (m 1).2 := by + intro y m + rw [iteratedFDeriv_two_apply, hfd, (hD2 y).fderiv] + simp + ring + have h3 : ∀ (x : ℝ × ℝ) (m : Fin 3 → ℝ × ℝ), iteratedFDeriv ℝ 3 mixedToyF x m = + 2 * (m 0).1 * (m 1).1 * (m 2).1 + 2 * (m 0).2 * ((m 1).1 * (m 2).2 + (m 1).2 * (m 2).1) + + 2 * (m 0).1 * (m 1).2 * (m 2).2 := by + intro x m + rw [DifferentiableAt.iteratedFDeriv_succ_apply_left' + (hcd.contDiffAt.differentiableAt_iteratedFDeriv (by norm_num))] + have hg : HasFDerivAt (fun y => iteratedFDeriv ℝ 2 mixedToyF y (Fin.tail m)) + ((2 * (m 1).1 * (m 2).1 + 2 * (m 1).2 * (m 2).2) • ContinuousLinearMap.fst ℝ ℝ ℝ + + (2 * ((m 1).1 * (m 2).2 + (m 1).2 * (m 2).1)) • ContinuousLinearMap.snd ℝ ℝ ℝ) x := by + have := (((2 * (m 1).1 * (m 2).1 + 2 * (m 1).2 * (m 2).2) • ContinuousLinearMap.fst ℝ ℝ ℝ + + (2 * ((m 1).1 * (m 2).2 + (m 1).2 * (m 2).1)) • + ContinuousLinearMap.snd ℝ ℝ ℝ).hasFDerivAt (x := x)).add_const (-40 * (m 1).2 * (m 2).2) + convert this using 1 + funext y; rw [h2]; simp [Fin.tail]; ring + rw [hg.fderiv] + simp + ring + have h4 : ∀ (x : ℝ × ℝ) (m : Fin 4 → ℝ × ℝ), iteratedFDeriv ℝ 4 mixedToyF x m = 0 := by + intro x m + rw [DifferentiableAt.iteratedFDeriv_succ_apply_left' + (hcd.contDiffAt.differentiableAt_iteratedFDeriv (by norm_num))] + have hc : (fun y => iteratedFDeriv ℝ 3 mixedToyF y (Fin.tail m)) = + fun _ => iteratedFDeriv ℝ 3 mixedToyF x (Fin.tail m) := by + funext y; rw [h3, h3] + have hg : HasFDerivAt (fun y => iteratedFDeriv ℝ 3 mixedToyF y (Fin.tail m)) + (0 : ℝ × ℝ →L[ℝ] ℝ) x := by + rw [hc]; exact hasFDerivAt_const _ _ + rw [hg.fderiv] + simp + have hsrc := ridge_capHyp_blocks (E := ℝ) (f := mixedToyF) (U := univ) (r := 1) (k := 1 / 6) + (M3 := 2) (M4 := 0) (lam := 41) one_pos (by norm_num) isOpen_univ (subset_univ _) + hcd.contDiffOn + (fun x _ => by rw [h3]; simp) + (fun p _ y => by rw [h3]; simp) + (fun p _ y₁ y₂ => by + rw [h3] + simp only [Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two, Matrix.tail_cons, + Matrix.head_cons, Real.norm_eq_abs] + rw [show (2 * (0 : ℝ) * 0 * 1 + 2 * y₁ * (0 * 0 + y₂ * 1) + 2 * 0 * y₂ * 0) = 2 * (y₁ * y₂) by + ring, abs_mul, abs_mul] + norm_num [mul_assoc]) + (fun p _ y₁ y₂ y₃ => by + rw [h3] + simp only [Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two, Matrix.tail_cons, + Matrix.head_cons, Real.norm_eq_abs] + rw [show (2 * (0 : ℝ) * 0 * 0 + 2 * y₁ * (0 * y₃ + y₂ * 0) + 2 * 0 * y₂ * y₃) = 0 by ring, + abs_zero] + positivity) + (fun p _ => by rw [h4]; simp) + (fun p _ v => by rw [h4]; simp) + (fun v => by + rw [h2] + simp only [Matrix.cons_val_zero, Matrix.cons_val_one, Real.norm_eq_abs, sq_abs] + nlinarith [sq_nonneg v]) + (by norm_num) (by norm_num) + (by rw [(hDf _).fderiv]; ext <;> norm_num) + (by rw [(hDf _).fderiv]; ext <;> norm_num) + (by simp only [mixedToyF]; norm_num) + obtain ⟨ε, hε, hex, hcap⟩ := hsrc + have hcrit0 : ∀ x : ℝ, HasFDerivAt (fun y => mixedToyF (x, y)) (0 : ℝ →L[ℝ] ℝ) 0 := by + intro x + have := slice_hasFDerivAt (hDf (x, 0)) + convert this using 1 + ext + simp + obtain ⟨-, -, hC, -⟩ := hcap (fun _ => 0) (fun x _ => ⟨by simp, hcrit0 x⟩) + exact ⟨⟨ε, hε, hex⟩, hC⟩ + end CapFirstExit diff --git a/frontiers/cap_first_exit_lean_20261002/MANIFEST.json b/frontiers/cap_first_exit_lean_20261002/MANIFEST.json index 6a496bda1..3e3154602 100644 --- a/frontiers/cap_first_exit_lean_20261002/MANIFEST.json +++ b/frontiers/cap_first_exit_lean_20261002/MANIFEST.json @@ -164,7 +164,13 @@ "CapFirstExit.hasFDerivAt_zero_const_mul_iff", "CapFirstExit.iteratedFDeriv_const_mul_of_isOpen", "CapFirstExit.ridge_capHyp_K", - "CapFirstExit.ridge_capHyp_norm_K" + "CapFirstExit.ridge_capHyp_norm_K", + "CapFirstExit.iteratedFDeriv_three_swap\u2081\u2082", + "CapFirstExit.iteratedFDeriv_three_swap\u2082\u2083", + "CapFirstExit.block_of_partial", + "CapFirstExit.ridge_capHyp_blocks", + "CapFirstExit.mixedToyF", + "CapFirstExit.mixedToy_blocks" ], "expected_axioms": { "CapFirstExit.path_meets_frontier": [ @@ -826,6 +832,36 @@ "Classical.choice", "Quot.sound", "propext" + ], + "CapFirstExit.iteratedFDeriv_three_swap\u2081\u2082": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.iteratedFDeriv_three_swap\u2082\u2083": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.block_of_partial": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.ridge_capHyp_blocks": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.mixedToyF": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.mixedToy_blocks": [ + "Classical.choice", + "Quot.sound", + "propext" ] }, "files": [ @@ -836,18 +872,18 @@ }, { "path": "ALIGNMENT.md", - "bytes": 50298, - "sha256": "0ff1cac44071631810e347466ba485e413c70fa065b426e7dc48ce6ae928e441" + "bytes": 53896, + "sha256": "bd516fef651e7b233d1309e7d7f9f774a1eeee5f3584030a838a6a80e1d94fb8" }, { "path": "CapFirstExit.lean", - "bytes": 287184, - "sha256": "15715eb444368202f88203f8c22414a94b042de9f18058c1edc6241f187c0839" + "bytes": 307724, + "sha256": "f3993aab9348f24a090f2ecbb5fc9e12acc03fc2576045e3ca689d3443425688" }, { "path": "README.md", - "bytes": 27180, - "sha256": "89ab09a53701c4f3f49c1adb21650a7ff79737878e60cc8efccddbf81e083667" + "bytes": 28556, + "sha256": "cc4090d652f0ed03dbd19499b17c5f8d246a21aa1fd8124b4ff443724ea5a7c7" }, { "path": "gate.py", @@ -872,7 +908,7 @@ { "path": "test_gate.py", "bytes": 6275, - "sha256": "7bb42e28c76271f27006bfa8d4f543c24aba410998dddc8865b330d7d9d73c0d" + "sha256": "a3600f82b6d86b37c30ba3752b6982f12435057bb5b0274d59ce74f2b9082c94" } ] } diff --git a/frontiers/cap_first_exit_lean_20261002/README.md b/frontiers/cap_first_exit_lean_20261002/README.md index af747d71d..c0dce98e6 100644 --- a/frontiers/cap_first_exit_lean_20261002/README.md +++ b/frontiers/cap_first_exit_lean_20261002/README.md @@ -66,6 +66,8 @@ Since v2.3, `quarticToy_E` also instantiates `ridge_capHyp_E` away from the dege Since v2.4, `ridge_capHyp_K` states the cap for every pin gap `k > 0`, on exactly P §7's event `G_r = {λ_min(−A_M) > [4/(3k)] r M3², r M4 ≤ 3k/10}` with `f(M) − f(S) = k r³`. It applies `ridge_capHyp_E` to `f/(6k)`. That divides every derivative bound and the transverse curvature by `6k`, and leaves the critical points, the ridge and the cap unchanged (`CapHyp.of_const_mul`, `hasFDerivAt_zero_const_mul_iff`, `iteratedFDeriv_const_mul_of_isOpen`). `ridge_capHyp_norm_K` takes `M3` and `M4` as bounds on the operator norms of `D³f` and `D⁴f` over `D`, the jet suprema whose tails the probability side bounds. +Since v2.5, `ridge_capHyp_blocks` takes CAP (1) as written. CAP states its hypotheses with the partial-block norms `M_j = max_{a+c=j} sup_D ‖∂_x^a D_y^c f‖_op`, whereas `ridge_capHyp_K` takes the third derivative as one block inequality. `block_of_partial` derives that inequality from the partial blocks with `c = 1, 2, 3`: it expands `D³f` multilinearly and uses its symmetry. Lean proves that symmetry for `f ∈ C³` (`iteratedFDeriv_three_swap₁₂`, `iteratedFDeriv_three_swap₂₃`); Mathlib has the symmetry of higher derivatives only for analytic functions. `mixedToy_blocks` instantiates the theorem with the nonzero mixed block `∂_x D_y² f = 2`. + In the topological theorems, `X` is any topological space, and nothing is assumed about `f` outside `C` except along the single ridge path. - The core theorems use only (C1)–(C3): no metric, smoothness, Morse, compactness or probability hypothesis. Their @@ -137,6 +139,10 @@ single ridge path. | `hasFDerivAt_zero_const_mul_iff`, `iteratedFDeriv_const_mul_of_isOpen` | a nonzero factor leaves the zeros of the derivative in place; on an open set where `f ∈ C⁴`, `D^i(c f) = c · D^i f` for `i ≤ 4` (v2.4) | | `ridge_capHyp_K` | the cap on P §7's `G_r` for every gap `k > 0`: `f(M) − f(S) = k r³`, `(4/(3k)) r m² < λ` and `r n ≤ 3k/10` (v2.4). The case `k = 1/6` is `ridge_capHyp_E` | | `ridge_capHyp_norm_K` | `ridge_capHyp_K` with operator-norm bounds `‖D³f‖ ≤ M3` and `‖D⁴f‖ ≤ M4` on `D` (v2.4) | +| `iteratedFDeriv_three_swap₁₂`, `iteratedFDeriv_three_swap₂₃` | the third derivative of a `C³` function is symmetric (v2.5) | +| `block_of_partial` | for a symmetric trilinear form, CAP's partial-block bounds with `c = 1, 2, 3` give the block inequality (v2.5) | +| `ridge_capHyp_blocks` | the cap under CAP (1) as written, with CAP's partial-block norms `M3`, `M4` (v2.5) | +| `mixedToyF`, `mixedToy_blocks` | `h1ToyF + xy²` meets every hypothesis of `ridge_capHyp_blocks` with `M3 = 2`, `M4 = 0` and `λ = 41`; its mixed block `∂_x D_y² f = 2` is nonzero (v2.5) | | `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 | @@ -169,8 +175,9 @@ This packet does not formalize: - the critical pins and the gap `r³/6`. The derivative data, a collar inside `U` and the bound `K` on it are derived (`collar_subset_open`, - `block_of_norm`, `block_bound_collar`). That the local field on `G_r` satisfies SP's §2 setting is SP's input and - is not formalized; + `block_of_norm`, `block_bound_collar`). Since v2.5 the block bound `m` is derived too, from CAP's + partial-block norm `M3` (`block_of_partial`, `ridge_capHyp_blocks`). That the local field on `G_r` satisfies + SP's §2 setting is SP's input and is not formalized; - 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`); @@ -209,7 +216,7 @@ The source gate checks: bound); - rebuilds the package fresh; - replays the module with `leanchecker`; -- prints the axioms of all 132 declarations, requiring exactly the manifest's report: each uses only `propext`, +- prints the axioms of all 138 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 8b2517c5b..06fb433af 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"]), 132) + self.assertEqual(len(m["targets"]), 138) self.assertEqual(m['scientific_effect'], 'NONE') def copy(self):