diff --git a/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md b/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md index 1bc95786f..fba93b3c4 100644 --- a/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md +++ b/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md @@ -133,7 +133,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. +`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). 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 @@ -148,7 +148,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`); 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 (`block_of_norm`). 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. | +| 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 | ## 5. Review contract @@ -165,5 +165,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. 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. 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 6a7865076..d3d8a6fbe 100644 --- a/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean +++ b/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean @@ -29,6 +29,7 @@ is proved). Since v2.2 `ridge_capHyp_E` assumes only `f ∈ C⁴` on an open neighbourhood of `D` and SP's quantitative bounds on `D`: it builds every derivative datum from `f`, and the collar and its bound `K` come from compactness. + `quarticToy_E` (v2.3) exercises it away from the degenerate face, with `D⁴f ≠ 0` and (H2) sharp. 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. @@ -1385,7 +1386,8 @@ theorem ridge_hasStrictFDerivAt [CompleteSpace E] {f : ℝ × E → ℝ} {G : critical point in `B̄(0, 2r)` for `x` in an open set `U ⊇ [-2r, 2r]` (SP: `f ∈ C⁴` near `D`), `h x` in the open ball on `[-2r, 2r]`, and the transverse gradient strictly differentiable along the ridge with negative definite transverse part, `h` is strictly differentiable at every -`x ∈ [-2r, 2r]`. Composed with `ridge_inputs_of_joint`, this would supply its `hh'`. -/ +`x ∈ [-2r, 2r]`. Composed with `ridge_inputs_of_joint`, as `ridge_capHyp_source` does, this supplies +its `hh'`. -/ theorem ridge_differentiable [FiniteDimensional ℝ E] {f : ℝ × E → ℝ} {G : ℝ × E → E →L[ℝ] ℝ} {DG : ℝ → ℝ × E →L[ℝ] E →L[ℝ] ℝ} {h : ℝ → E} {U : Set ℝ} {r δ : ℝ} (hδ : 0 < δ) (hU : IsOpen U) (hIU : Icc (-2 * r) (2 * r) ⊆ U) @@ -4488,4 +4490,138 @@ theorem h1Toy_E : obtain ⟨-, -, hC, -⟩ := hcap (fun _ => 0) (fun x _ => ⟨by simp, hcrit0 x⟩) exact ⟨⟨ε, hε, hex⟩, hC⟩ + +/-- A pin-preserving quartic perturbation of `h1ToyF`: `q(x) = (x² - 1/4)²/480` vanishes to second +order at both pins, so they stay critical and the gap stays `1/6`, while `f_xxx = 2 + x/20` varies +and `D⁴f = 1/20 ≠ 0`. -/ +noncomputable def quarticToyF (p : ℝ × ℝ) : ℝ := + p.1 ^ 3 / 3 - p.1 / 4 - 20 * p.2 ^ 2 + (p.1 ^ 2 - 1 / 4) ^ 2 / 480 + +/-- **`ridge_capHyp_E` away from the degenerate face.** On `quarticToyF` the third derivative +`f_xxx = 2 + x/20` varies, the fourth derivative `D⁴f = 1/20` is nonzero, and (H2) holds with +equality, `rn = 1/20` (`r = 1`, `n = 1/20`); `|f_xxx| ≤ 81/40 = m` on the pin segment, and (H1) holds +as `8m² = 32.805 < 40 = λ`. So `fxxx_lower`'s estimate is used with `n > 0` and the collar bound +`K` is positive, unlike `h1Toy_E` (where `D⁴f = 0`). The theorem gives the ridge on +`(-2 - ε, 2 + ε)` for some `ε > 0` and the cap with `M = (-1/2, 0)`. -/ +theorem quarticToy_E : + (∃ ε > 0, ∃ h : ℝ → ℝ, ∀ x ∈ Ioo (-2 * 1 - ε : ℝ) (2 * 1 + ε), h x ∈ Metric.ball (0 : ℝ) (2 * 1) ∧ + HasFDerivAt (fun y => quarticToyF (x, y)) (0 : ℝ →L[ℝ] ℝ) (h x)) ∧ + CapHyp quarticToyF (Icc (-2 * 1) (1 / 2) ×ˢ Metric.closedBall (0 : ℝ) (2 * 1)) (-1 / 2, 0) + (2 * 1, 0) (quarticToyF (-1 / 2, 0)) (quarticToyF (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 quarticToyF + ((p.1 ^ 2 - 1 / 4 + (4 * p.1 ^ 3 - p.1) / 480) • ContinuousLinearMap.fst ℝ ℝ ℝ + + (-40 * 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.const_mul (HasFDerivAt.pow ((HasFDerivAt.pow (hf p) 2).sub_const (1 / 4)) 2) + (1 / 480)) + convert h1 using 1 + · funext q + simp only [quarticToyF, Pi.sub_apply, Pi.add_apply] + ring + · ext <;> simp <;> ring + have hD2 : ∀ p : ℝ × ℝ, HasFDerivAt (fun q : ℝ × ℝ => (q.1 ^ 2 - 1 / 4 + (4 * q.1 ^ 3 - q.1) / 480) • + ContinuousLinearMap.fst ℝ ℝ ℝ + (-40 * q.2) • ContinuousLinearMap.snd ℝ ℝ ℝ) + (((2 * p.1 + (12 * p.1 ^ 2 - 1) / 480) • ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight + (ContinuousLinearMap.fst ℝ ℝ ℝ) + + ((-40 : ℝ) • ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight (ContinuousLinearMap.snd ℝ ℝ ℝ)) p := by + intro p + have h1 : HasFDerivAt (fun q : ℝ × ℝ => q.1 ^ 2 - 1 / 4 + (4 * q.1 ^ 3 - q.1) / 480) + ((2 * p.1 + (12 * p.1 ^ 2 - 1) / 480) • ContinuousLinearMap.fst ℝ ℝ ℝ) p := by + have := ((HasFDerivAt.pow (hf p) 2).sub_const (1 / 4)).add + (HasFDerivAt.const_mul ((HasFDerivAt.const_mul (HasFDerivAt.pow (hf p) 3) 4).sub (hf p)) + (1 / 480)) + convert this using 1 <;> first | (funext q; simp; ring) | (ext <;> simp; ring) + have h2 : HasFDerivAt (fun q : ℝ × ℝ => -40 * q.2) ((-40 : ℝ) • ContinuousLinearMap.snd ℝ ℝ ℝ) p := + HasFDerivAt.const_mul (hs p) (-40) + exact (h1.smul_const (ContinuousLinearMap.fst ℝ ℝ ℝ)).add + (h2.smul_const (ContinuousLinearMap.snd ℝ ℝ ℝ)) + have hcd : ContDiff ℝ 4 quarticToyF := by unfold quarticToyF; fun_prop + have hfd : fderiv ℝ quarticToyF = fun p => (p.1 ^ 2 - 1 / 4 + (4 * p.1 ^ 3 - p.1) / 480) • + ContinuousLinearMap.fst ℝ ℝ ℝ + (-40 * p.2) • ContinuousLinearMap.snd ℝ ℝ ℝ := + funext fun p => (hDf p).fderiv + have h2 : ∀ (y : ℝ × ℝ) (m : Fin 2 → ℝ × ℝ), iteratedFDeriv ℝ 2 quarticToyF y m = + (2 * y.1 + (12 * y.1 ^ 2 - 1) / 480) * (m 0).1 * (m 1).1 - 40 * (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 quarticToyF x m = (2 + x.1 / 20) * (m 0).1 * (m 1).1 * (m 2).1 := by + intro x m + rw [DifferentiableAt.iteratedFDeriv_succ_apply_left' + (hcd.contDiffAt.differentiableAt_iteratedFDeriv (by norm_num))] + have hg : HasFDerivAt (fun y => iteratedFDeriv ℝ 2 quarticToyF y (Fin.tail m)) + (((2 + x.1 / 20) * (m 1).1 * (m 2).1) • ContinuousLinearMap.fst ℝ ℝ ℝ) x := by + have hp : HasFDerivAt (fun y : ℝ × ℝ => 2 * y.1 + (12 * y.1 ^ 2 - 1) / 480) + ((2 + x.1 / 20) • ContinuousLinearMap.fst ℝ ℝ ℝ) x := by + have := (HasFDerivAt.const_mul (hf x) 2).add + (HasFDerivAt.const_mul ((HasFDerivAt.const_mul (HasFDerivAt.pow (hf x) 2) 12).sub_const 1) + (1 / 480)) + convert this using 1 <;> first | (funext q; simp; ring) | (ext <;> simp; ring) + have := (hp.mul_const ((m 1).1 * (m 2).1)).sub_const (40 * (m 1).2 * (m 2).2) + convert this using 1 + · funext y; rw [h2]; simp [Fin.tail]; ring + · (ext <;> simp); ring + rw [hg.fderiv] + simp + ring + have h4 : ∀ (x : ℝ × ℝ) (m : Fin 4 → ℝ × ℝ), + iteratedFDeriv ℝ 4 quarticToyF x m = (1 / 20) * (m 0).1 * (m 1).1 * (m 2).1 * (m 3).1 := by + intro x m + rw [DifferentiableAt.iteratedFDeriv_succ_apply_left' + (hcd.contDiffAt.differentiableAt_iteratedFDeriv (by norm_num))] + have hg : HasFDerivAt (fun y => iteratedFDeriv ℝ 3 quarticToyF y (Fin.tail m)) + ((1 / 20 * (m 1).1 * (m 2).1 * (m 3).1) • ContinuousLinearMap.fst ℝ ℝ ℝ) x := by + have := (((hf x).const_mul (1 / 20)).const_add 2).mul_const ((m 1).1 * (m 2).1 * (m 3).1) + convert this using 1 + · funext y; rw [h3]; simp [Fin.tail]; ring + · (ext <;> simp); ring + rw [hg.fderiv] + simp + ring + have hsrc := ridge_capHyp_E (E := ℝ) (f := quarticToyF) (U := univ) (r := 1) (m := 81 / 40) + (n := 1 / 20) (lam := 40) one_pos isOpen_univ (subset_univ _) hcd.contDiffOn + (fun p _ s₁ s₂ s₃ y₁ y₂ y₃ => by + rw [h3, h3] + simp only [Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two, Matrix.tail_cons, + Matrix.head_cons] + have h0 : (2 + p.1 / 20) * s₁ * s₂ * s₃ - s₁ * s₂ * s₃ * ((2 + p.1 / 20) * 1 * 1 * 1) = 0 := by + ring + rw [h0, abs_zero] + exact mul_nonneg (by norm_num) (block_nonneg s₁ s₂ s₃ y₁ y₂ y₃)) + (fun x hx => by + rw [h3] + simp only [Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two, Matrix.tail_cons, + Matrix.head_cons, mul_one] + rw [abs_le] + constructor <;> linarith [hx.1, hx.2]) + (fun p _ => by rw [h4]; simp) + (fun p _ v => by rw [h4]; simp) + (by norm_num) + (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 rw [(hDf _).fderiv]; ext <;> norm_num) + (by rw [(hDf _).fderiv]; ext <;> norm_num) + (by simp only [quarticToyF]; norm_num) + obtain ⟨ε, hε, hex, hcap⟩ := hsrc + have hcrit0 : ∀ x : ℝ, HasFDerivAt (fun y => quarticToyF (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 21e9adaff..97f92e75d 100644 --- a/frontiers/cap_first_exit_lean_20261002/MANIFEST.json +++ b/frontiers/cap_first_exit_lean_20261002/MANIFEST.json @@ -157,7 +157,9 @@ "CapFirstExit.h1Toy_C3", "CapFirstExit.h1Toy_C4", "CapFirstExit.h1Toy_D", - "CapFirstExit.h1Toy_E" + "CapFirstExit.h1Toy_E", + "CapFirstExit.quarticToyF", + "CapFirstExit.quarticToy_E" ], "expected_axioms": { "CapFirstExit.path_meets_frontier": [ @@ -784,6 +786,16 @@ "Classical.choice", "Quot.sound", "propext" + ], + "CapFirstExit.quarticToyF": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.quarticToy_E": [ + "Classical.choice", + "Quot.sound", + "propext" ] }, "files": [ @@ -794,18 +806,18 @@ }, { "path": "ALIGNMENT.md", - "bytes": 46611, - "sha256": "31a13063fcbd53d12c4b3487a468de68bdad25fa5b8615697349e505374b104a" + "bytes": 47642, + "sha256": "60433b419fd5b11569c83afad0cb226c79e6e5c90666849d2aa288d4fee16469" }, { "path": "CapFirstExit.lean", - "bytes": 267172, - "sha256": "c30c125004047eeaefc43a5e183319360a0d1a23d27051366ae5619171f1dce5" + "bytes": 274905, + "sha256": "fde8c26af78c5d2475c2af1332d98b54a550fe469cb0fcc097ea2f7754db5f51" }, { "path": "README.md", - "bytes": 25154, - "sha256": "bd5dc3cdd87cd8c96b7aaac4b7a0521d56830dd2b7c7bfafd4b583b44bb9f7f5" + "bytes": 25901, + "sha256": "624368518e401c32c92c5e93a01f88b9326b450f60eea5ffc2f60259fe5fde27" }, { "path": "gate.py", @@ -830,7 +842,7 @@ { "path": "test_gate.py", "bytes": 6275, - "sha256": "cb3b08cc5b99f087b6ca2153fd028b2825a7a69cff5a42b2ac5e8d031d6f4039" + "sha256": "04d262b9d5c202c777ce2d71dc7bfe4478ee7d3471957d1725d08b19dedf22e5" } ] } diff --git a/frontiers/cap_first_exit_lean_20261002/README.md b/frontiers/cap_first_exit_lean_20261002/README.md index 9eadc29db..37e9958dd 100644 --- a/frontiers/cap_first_exit_lean_20261002/README.md +++ b/frontiers/cap_first_exit_lean_20261002/README.md @@ -62,6 +62,8 @@ Since v2.2, `ridge_capHyp_E` assumes only that `f` is `C⁴` on an open `U ⊇ D - the collar width `ε₀` comes from `collar_subset_open`: `D` is compact, so a closed thickening of it lies in `U`; - `K` bounds `‖D⁴f‖` on the compact collar, and `block_of_norm` turns that norm bound into the block bound. +Since v2.3, `quarticToy_E` also instantiates `ridge_capHyp_E` away from the degenerate face. `quarticToyF = x³/3 − x/4 − 20y² + (x² − 1/4)²/480` keeps both pins critical and the gap at `1/6`, while `f_xxx = 2 + x/20` varies and `D⁴f = 1/20 ≠ 0`. So (H2) holds with equality (`rn = 1/20`), `fxxx_lower` runs with `n > 0`, and the collar bound `K` is positive. + 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 @@ -128,6 +130,7 @@ single ridge path. | `collar_subset_open` | a closed collar `[−2r − ε₀, 2r + ε₀] × B̄(0, 2r)` with `ε₀ > 0` inside any open `U ⊇ D` (v2.2) | | `ridge_capHyp_E` | the cap from `f ∈ C⁴` on an open `U ⊇ D` and SP's quantitative bounds on `D` (v2.2). It concludes the ridge on `(−2r − ε, 2r + ε)` for some `ε > 0`, `h(∓r/2) = 0`, the cap and (C2⁺). No derivative datum and no bound off `D` is assumed | | `h1Toy_E` | `h1ToyF` meets every hypothesis of `ridge_capHyp_E` with `U = ℝ²`: `D³f[a, b, c] = 2a₁b₁c₁` and `D⁴f = 0`, so `m = 2` and `n = 0`. The theorem gives a ridge on `(−2 − ε, 2 + ε)` for some `ε > 0`, and the cap | +| `quarticToyF`, `quarticToy_E` | a pin-preserving quartic perturbation of `h1ToyF` that meets every hypothesis of `ridge_capHyp_E` with `U = ℝ²`, `m = 81/40`, `n = 1/20` and `λ = 40` (v2.3). `D³f[a, b, c] = (2 + x/20)a₁b₁c₁` and `D⁴f[a, b, c, d] = a₁b₁c₁d₁/20`, so (H2) is sharp and (H1) reads `32.805 < 40`. The theorem gives the ridge and the 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 | @@ -200,7 +203,7 @@ The source gate checks: bound); - rebuilds the package fresh; - replays the module with `leanchecker`; -- prints the axioms of all 125 declarations, requiring exactly the manifest's report: each uses only `propext`, +- prints the axioms of all 127 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 3976f6b3d..57bdae9c9 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"]), 125) + self.assertEqual(len(m["targets"]), 127) self.assertEqual(m['scientific_effect'], 'NONE') def copy(self):