diff --git a/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md b/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md index fba93b3c4..8f0a5e682 100644 --- a/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md +++ b/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md @@ -101,6 +101,11 @@ The source setting (SP §2) is as follows: | `block_of_norm` | `B` a trilinear form on `ℝ × E` (a `ContinuousMultilinearMap` on `Fin 3`) with `‖B‖ ≤ K` ⇒ `|B[a, b, c] − s₁s₂s₃ B[e, e, e]| ≤ K((|s₁| + ‖y₁‖)(|s₂| + ‖y₂‖)(|s₃| + ‖y₃‖) − |s₁||s₂||s₃|)` for `a = (s₁, y₁)`, `b = (s₂, y₂)`, `c = (s₃, y₃)`, `e = (1, 0)` | I3's "some `K`": a norm bound gives the block form | Three-term telescoping (`a → s₁e`, then `b → s₂e`, then `c → s₃e`). Each term has one transverse argument `(0, yᵢ)` and is bounded with `‖(s, y)‖ ≤ |s| + ‖y‖`. The three bounds sum to the right side exactly. | | `collar_subset_open` | `E` proper, `0 < r`, `U` open, `D ⊆ U` ⇒ `∃ ε₀ > 0` with `[−2r − ε₀, 2r + ε₀] × B̄(0, 2r) ⊆ U` | SP's "near `D`" | `D` is compact, so some closed thickening of `D` lies in `U`. In the max metric each collar point is within `ε₀` of a point of `D`. | | `ridge_capHyp_E` | `U` open with `D ⊆ U`, and `f` `C⁴` on `U`. On `D`: the block bound `m` on `D³f`; `|D⁴f[e, e, e, e]| ≤ n` and `|D⁴f[(0, v), e, e, e]| ≤ n‖v‖`. On the pin segment, `|D³f(x, 0)[e, e, e]| ≤ m`. Also `D²f(M)[(0, v), (0, v)] ≤ −λ‖v‖²`, (H1) `8rm² < λ`, (H2) `rn ≤ 1/20`, `Df(M) = Df(S) = 0` and the gap `r³/6` ⇒ `∃ ε > 0` with `ridge_capHyp_C4`'s conclusion on `(−2r − ε, 2r + ε)` | SP §2 (`f ∈ C⁴` near `D`; (H1), (H2), `M₃`, `M₄` on `D`); L1–L20 | `D^k f = iteratedFDeriv ℝ k f` and `e = (1, 0)`. `ridge_capHyp_D` is applied with `Df = fderiv f`, `D2f = fderiv (fderiv f)`, `T3 p a b c = D³f(p)[c, a, b]`, `T4 p a b c = D⁴f(p)[e, c, a, b]` and `Φ4 p w = D⁴f(p)[w, e, e, e]`; `DG`, `H`, `Hx` and `Hr` are built from `D2f` and its derivative. `ε₀` comes from `collar_subset_open`, and `K = max C 0`, where `‖D⁴f‖ ≤ C` on the compact collar. The block bound is invariant under a common permutation of the three slots, so the slot order in `T3` and `T4` does not matter. Nothing is assumed off `D` except `C⁴` on `U`. | +| `CapHyp.of_const_mul` | `0 < c` and `CapHyp (fun x => c * f x) C M z (c * b) (c * s)` ⇒ `CapHyp f C M z b s` | P §7 uses the cap for every gap `k` | Every field of (C1)–(C3) is an inequality between values of `f` (or membership), so dividing by `c > 0` preserves it. The ridge is the same path. | +| `hasFDerivAt_zero_const_mul_iff` | `c ≠ 0` ⇒ (`y ↦ c φ(y)` has derivative `0` at `y` ⇔ `φ` has derivative `0` at `y`) | the ridge `h` of `f` and of `c f` | Multiply by `c⁻¹` for the forward direction. So the ridge hypotheses and conclusions of `ridge_capHyp_E` for `f/(6k)` are those for `f`. | +| `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`. | | `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. | @@ -146,7 +151,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 | Only the identification of SP's objects with these Lean objects remains. | +| 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`). | | 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 | @@ -165,5 +170,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. 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. 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 d3d8a6fbe..a19c5deb4 100644 --- a/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean +++ b/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean @@ -30,6 +30,10 @@ 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. + Since v2.4 `ridge_capHyp_K` states the cap on P §7's event `G_r` for every pin gap + `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`. 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. @@ -4624,4 +4628,217 @@ theorem quarticToy_E : obtain ⟨-, -, hC, -⟩ := hcap (fun _ => 0) (fun x _ => ⟨by simp, hcrit0 x⟩) exact ⟨⟨ε, hε, hex⟩, hC⟩ +/-! ### v2.4: the cap on P §7's event `G_r`, for every pin gap `k > 0` + +P §7 (`imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md`) uses the deterministic +cap on `G_r = {λ_min(−A_M) > [4/(3k)] r M3², r M4 ≤ 3k/10}` with the pin gap `f(M) − f(S) = k r³`. +`ridge_capHyp_E` is the case `k = 1/6`. A positive factor `f ↦ c f` multiplies every derivative +bound and the transverse curvature by `c`, and changes neither the critical points nor the cap. -/ + +namespace CapHyp + +variable {f : X → ℝ} {C : Set X} {M z : X} {b s : ℝ} + +/-- A positive factor. A cap for `c f` at the levels `c b`, `c s` is a cap for `f` at `b`, `s`. -/ +theorem of_const_mul {c : ℝ} (hc : 0 < c) + (H : CapHyp (fun x => c * f x) C M z (c * b) (c * s)) : CapHyp f C M z b s where + mem := H.mem + ceiling x hx := le_of_mul_le_mul_left (H.ceiling x hx) hc + frontier_le x hx := le_of_mul_le_mul_left (H.frontier_le x hx) hc + older := lt_of_mul_lt_mul_left H.older hc.le + ridge := by + obtain ⟨γ, hγ⟩ := H.ridge + exact ⟨γ, fun t => le_of_mul_le_mul_left (hγ t) hc⟩ + +end CapHyp + +section GapK + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + +/-- A nonzero factor does not move the points where the derivative vanishes. -/ +theorem hasFDerivAt_zero_const_mul_iff {φ : E → ℝ} {c : ℝ} (hc : c ≠ 0) {y : E} : + HasFDerivAt (fun y => c * φ y) (0 : E →L[ℝ] ℝ) y ↔ HasFDerivAt φ (0 : E →L[ℝ] ℝ) y := by + constructor + · intro h + have h' := h.const_mul c⁻¹ + rw [smul_zero] at h' + exact h'.congr_of_eventuallyEq + (Filter.Eventually.of_forall fun y => (inv_mul_cancel_left₀ hc (φ y)).symm) + · intro h + have h' := h.const_mul c + rwa [smul_zero] at h' + +/-- On an open set where `f ∈ C⁴`, the derivatives of order `≤ 4` of `c f` are `c` times those of +`f`. -/ +theorem iteratedFDeriv_const_mul_of_isOpen {f : ℝ × E → ℝ} {U : Set (ℝ × E)} (hU : IsOpen U) + (hf : ContDiffOn ℝ 4 f U) (c : ℝ) {i : ℕ} (hi : i ≤ 4) {p : ℝ × E} (hp : p ∈ U) : + iteratedFDeriv ℝ i (fun q => c * f q) p = c • iteratedFDeriv ℝ i f p := by + have hfa : ContDiffAt ℝ i f p := + (hf.contDiffAt (hU.mem_nhds hp)).of_le (by exact_mod_cast hi) + exact iteratedFDeriv_const_smul_apply' (a := c) hfa + +/-- **The cap for every gap `k > 0`** (P §7's event `G_r`). With the pin gap +`f(M) − f(S) = k r³`, the hypotheses `(4/(3k)) r m² < λ` and `r n ≤ 3k/10` give the conclusion of +`ridge_capHyp_E`. That theorem is the case `k = 1/6`; the proof applies it to `f / (6k)`. -/ +theorem ridge_capHyp_K [FiniteDimensional ℝ E] {f : ℝ × E → ℝ} {U : Set (ℝ × E)} + {r k m n 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) + (hT : ∀ p ∈ Icc (-2 * r) (2 * r) ×ˢ Metric.closedBall (0 : E) (2 * r), + ∀ (s₁ s₂ s₃ : ℝ) (y₁ y₂ y₃ : E), + |iteratedFDeriv ℝ 3 f p ![(s₁, y₁), (s₂, y₂), (s₃, y₃)] - + s₁ * s₂ * s₃ * iteratedFDeriv ℝ 3 f p ![(1, 0), (1, 0), (1, 0)]| ≤ + m * ((|s₁| + ‖y₁‖) * (|s₂| + ‖y₂‖) * (|s₃| + ‖y₃‖) - |s₁| * |s₂| * |s₃|)) + (hTe : ∀ x ∈ Icc (-r / 2) (r / 2), |iteratedFDeriv ℝ 3 f (x, 0) ![(1, 0), (1, 0), (1, 0)]| ≤ m) + (hn4x : ∀ p ∈ Icc (-2 * r) (2 * r) ×ˢ Metric.closedBall (0 : E) (2 * r), + |iteratedFDeriv ℝ 4 f p ![(1, 0), (1, 0), (1, 0), (1, 0)]| ≤ n) + (hn4y : ∀ 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)]| ≤ n * ‖v‖) + (hH2 : r * n ≤ 3 * k / 10) + (hlam : ∀ v : E, iteratedFDeriv ℝ 2 f (-r / 2, 0) ![(0, v), (0, v)] ≤ -lam * ‖v‖ ^ 2) + (hH1 : 4 / (3 * k) * r * m ^ 2 < lam) + (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 + obtain ⟨c, hc_def⟩ : ∃ c : ℝ, c = 1 / (6 * k) := ⟨_, rfl⟩ + have hk0 : k ≠ 0 := hk.ne' + have hc : 0 < c := by rw [hc_def]; positivity + have hD : ∀ p ∈ Icc (-2 * r) (2 * r) ×ˢ Metric.closedBall (0 : E) (2 * r), p ∈ U := + fun p hp => hDU hp + have hseg : ∀ x ∈ Icc (-r / 2) (r / 2), ((x, 0) : ℝ × E) ∈ U := by + intro x hx + apply hDU + refine ⟨⟨by linarith [hx.1], by linarith [hx.2]⟩, ?_⟩ + simp only [Metric.mem_closedBall, dist_self] + linarith + have hsc : ∀ {i : ℕ}, i ≤ 4 → ∀ p ∈ U, + iteratedFDeriv ℝ i (fun q => c * f q) p = c • iteratedFDeriv ℝ i f p := + fun hi p hp => iteratedFDeriv_const_mul_of_isOpen hU hf c hi hp + have hdiff : ∀ p ∈ U, DifferentiableAt ℝ f p := fun p hp => + (hf.contDiffAt (hU.mem_nhds hp)).differentiableAt (by norm_num) + have hMU : ((-r / 2, 0) : ℝ × E) ∈ U := hseg _ ⟨le_refl _, by linarith⟩ + have hSU : ((r / 2, 0) : ℝ × E) ∈ U := hseg _ ⟨by linarith, le_refl _⟩ + have key := ridge_capHyp_E (E := E) (f := fun q => c * f q) (U := U) (m := c * m) + (n := c * n) (lam := c * lam) hr hU hDU (contDiffOn_const.mul hf) + (fun p hp s₁ s₂ s₃ y₁ y₂ y₃ => by + rw [hsc (by norm_num) p (hD p hp)] + simp only [smul_apply, smul_eq_mul] + have h := hT p hp s₁ s₂ s₃ y₁ y₂ y₃ + generalize iteratedFDeriv ℝ 3 f p ![(s₁, y₁), (s₂, y₂), (s₃, y₃)] = A at h ⊢ + generalize iteratedFDeriv ℝ 3 f p ![(1, 0), (1, 0), (1, 0)] = B at h ⊢ + rw [show c * A - s₁ * s₂ * s₃ * (c * B) = c * (A - s₁ * s₂ * s₃ * B) by ring, abs_mul, + abs_of_pos hc, mul_assoc c m] + exact mul_le_mul_of_nonneg_left h hc.le) + (fun x hx => by + rw [hsc (by norm_num) _ (hseg x hx)] + simp only [smul_apply, smul_eq_mul] + rw [abs_mul, abs_of_pos hc] + exact mul_le_mul_of_nonneg_left (hTe x hx) hc.le) + (fun p hp => by + rw [hsc (by norm_num) p (hD p hp)] + simp only [smul_apply, smul_eq_mul] + rw [abs_mul, abs_of_pos hc] + exact mul_le_mul_of_nonneg_left (hn4x p hp) hc.le) + (fun p hp v => by + rw [hsc (by norm_num) p (hD p hp)] + simp only [smul_apply, smul_eq_mul] + rw [abs_mul, abs_of_pos hc, mul_assoc] + exact mul_le_mul_of_nonneg_left (hn4y p hp v) hc.le) + (by + rw [hc_def, show r * (1 / (6 * k) * n) = r * n / (6 * k) by ring, + div_le_iff₀ (by positivity)] + linarith) + (fun v => by + rw [hsc (by norm_num) _ hMU] + simp only [smul_apply, smul_eq_mul] + calc c * iteratedFDeriv ℝ 2 f (-r / 2, 0) ![(0, v), (0, v)] + ≤ c * (-lam * ‖v‖ ^ 2) := mul_le_mul_of_nonneg_left (hlam v) hc.le + _ = -(c * lam) * ‖v‖ ^ 2 := by ring) + (by + have h8 : 8 * r * (c * m) ^ 2 = c * (4 / (3 * k) * r * m ^ 2) := by + rw [hc_def]; field_simp; ring + rw [h8] + exact mul_lt_mul_of_pos_left hH1 hc) + (by rw [fderiv_const_mul (hdiff _ hMU) c, hM, smul_zero]) + (by rw [fderiv_const_mul (hdiff _ hSU) c, hS, smul_zero]) + (by + show c * f (-r / 2, 0) - c * f (r / 2, 0) = r ^ 3 / 6 + rw [← mul_sub, hnorm, hc_def] + field_simp) + obtain ⟨ε, hε, hex, hcap⟩ := key + refine ⟨ε, hε, ?_, ?_⟩ + · obtain ⟨h, hh⟩ := hex + exact ⟨h, fun x hx => ⟨(hh x hx).1, (hasFDerivAt_zero_const_mul_iff hc.ne').1 (hh x hx).2⟩⟩ + · intro h hh + obtain ⟨h1, h2, hC, hfr⟩ := hcap h fun x hx => + ⟨(hh x hx).1, (hasFDerivAt_zero_const_mul_iff hc.ne').2 (hh x hx).2⟩ + exact ⟨h1, h2, hC.of_const_mul hc, fun x hx hne => lt_of_mul_lt_mul_left (hfr x hx hne) hc.le⟩ + +/-- **P §7's `G_r` with operator norms.** If `‖D³f‖ ≤ M3` and `‖D⁴f‖ ≤ M4` on +`D = [−2r, 2r] × B̄(0, 2r)`, then `(4/(3k)) r M3² < λ` and `r M4 ≤ 3k/10` give the cap. Each +partial-block bound used by `ridge_capHyp_K` is at most the operator norm (`block_of_norm`). -/ +theorem ridge_capHyp_norm_K [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) + (h3 : ∀ p ∈ Icc (-2 * r) (2 * r) ×ˢ Metric.closedBall (0 : E) (2 * r), + ‖iteratedFDeriv ℝ 3 f p‖ ≤ M3) + (h4 : ∀ p ∈ Icc (-2 * r) (2 * r) ×ˢ Metric.closedBall (0 : E) (2 * r), + ‖iteratedFDeriv ℝ 4 f p‖ ≤ M4) + (hH2 : r * M4 ≤ 3 * k / 10) + (hlam : ∀ v : E, iteratedFDeriv ℝ 2 f (-r / 2, 0) ![(0, v), (0, v)] ≤ -lam * ‖v‖ ^ 2) + (hH1 : 4 / (3 * k) * r * M3 ^ 2 < lam) + (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 + have he : ‖((1 : ℝ), (0 : E))‖ = 1 := by simp [Prod.norm_def] + have hv : ∀ v : E, ‖((0 : ℝ), v)‖ = ‖v‖ := fun v => by simp [Prod.norm_def] + refine ridge_capHyp_K hr hk hU hDU hf + (fun p hp s₁ s₂ s₃ y₁ y₂ y₃ => block_of_norm (h3 p hp) s₁ s₂ s₃ y₁ y₂ y₃) + (fun x hx => ?_) (fun p hp => ?_) (fun p hp v => ?_) hH2 hlam hH1 hM hS hnorm + · have hp : ((x, 0) : ℝ × E) ∈ Icc (-2 * r) (2 * r) ×ˢ Metric.closedBall (0 : E) (2 * r) := by + refine ⟨⟨by linarith [hx.1], by linarith [hx.2]⟩, ?_⟩ + simp only [Metric.mem_closedBall, dist_self] + linarith + have h := (iteratedFDeriv ℝ 3 f (x, 0)).le_opNorm ![(1, 0), (1, 0), (1, 0)] + simp only [Fin.prod_univ_three, Matrix.cons_val_zero, Matrix.cons_val_one, + Matrix.cons_val_two, Matrix.tail_cons, Matrix.head_cons, he, mul_one] at h + rw [← Real.norm_eq_abs] + exact h.trans (h3 _ hp) + · have h := (iteratedFDeriv ℝ 4 f p).le_opNorm ![(1, 0), (1, 0), (1, 0), (1, 0)] + simp only [Fin.prod_univ_four, Matrix.cons_val_zero, Matrix.cons_val_one, + Matrix.cons_val_two, Matrix.cons_val_three, Matrix.tail_cons, Matrix.head_cons, he, + mul_one] at h + rw [← Real.norm_eq_abs] + exact h.trans (h4 p hp) + · have h := (iteratedFDeriv ℝ 4 f p).le_opNorm ![(0, v), (1, 0), (1, 0), (1, 0)] + simp only [Fin.prod_univ_four, Matrix.cons_val_zero, Matrix.cons_val_one, + Matrix.cons_val_two, Matrix.cons_val_three, Matrix.tail_cons, Matrix.head_cons, he, hv, + mul_one] at h + rw [← Real.norm_eq_abs] + exact h.trans (mul_le_mul_of_nonneg_right (h4 p hp) (norm_nonneg v)) + +end GapK + end CapFirstExit diff --git a/frontiers/cap_first_exit_lean_20261002/MANIFEST.json b/frontiers/cap_first_exit_lean_20261002/MANIFEST.json index 97f92e75d..6a496bda1 100644 --- a/frontiers/cap_first_exit_lean_20261002/MANIFEST.json +++ b/frontiers/cap_first_exit_lean_20261002/MANIFEST.json @@ -159,7 +159,12 @@ "CapFirstExit.h1Toy_D", "CapFirstExit.h1Toy_E", "CapFirstExit.quarticToyF", - "CapFirstExit.quarticToy_E" + "CapFirstExit.quarticToy_E", + "CapFirstExit.CapHyp.of_const_mul", + "CapFirstExit.hasFDerivAt_zero_const_mul_iff", + "CapFirstExit.iteratedFDeriv_const_mul_of_isOpen", + "CapFirstExit.ridge_capHyp_K", + "CapFirstExit.ridge_capHyp_norm_K" ], "expected_axioms": { "CapFirstExit.path_meets_frontier": [ @@ -796,6 +801,31 @@ "Classical.choice", "Quot.sound", "propext" + ], + "CapFirstExit.CapHyp.of_const_mul": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.hasFDerivAt_zero_const_mul_iff": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.iteratedFDeriv_const_mul_of_isOpen": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.ridge_capHyp_K": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.ridge_capHyp_norm_K": [ + "Classical.choice", + "Quot.sound", + "propext" ] }, "files": [ @@ -806,18 +836,18 @@ }, { "path": "ALIGNMENT.md", - "bytes": 47642, - "sha256": "60433b419fd5b11569c83afad0cb226c79e6e5c90666849d2aa288d4fee16469" + "bytes": 50298, + "sha256": "0ff1cac44071631810e347466ba485e413c70fa065b426e7dc48ce6ae928e441" }, { "path": "CapFirstExit.lean", - "bytes": 274905, - "sha256": "fde8c26af78c5d2475c2af1332d98b54a550fe469cb0fcc097ea2f7754db5f51" + "bytes": 287184, + "sha256": "15715eb444368202f88203f8c22414a94b042de9f18058c1edc6241f187c0839" }, { "path": "README.md", - "bytes": 25901, - "sha256": "624368518e401c32c92c5e93a01f88b9326b450f60eea5ffc2f60259fe5fde27" + "bytes": 27180, + "sha256": "89ab09a53701c4f3f49c1adb21650a7ff79737878e60cc8efccddbf81e083667" }, { "path": "gate.py", @@ -842,7 +872,7 @@ { "path": "test_gate.py", "bytes": 6275, - "sha256": "04d262b9d5c202c777ce2d71dc7bfe4478ee7d3471957d1725d08b19dedf22e5" + "sha256": "7bb42e28c76271f27006bfa8d4f543c24aba410998dddc8865b330d7d9d73c0d" } ] } diff --git a/frontiers/cap_first_exit_lean_20261002/README.md b/frontiers/cap_first_exit_lean_20261002/README.md index 37e9958dd..af747d71d 100644 --- a/frontiers/cap_first_exit_lean_20261002/README.md +++ b/frontiers/cap_first_exit_lean_20261002/README.md @@ -64,6 +64,8 @@ Since v2.2, `ridge_capHyp_E` assumes only that `f` is `C⁴` on an open `U ⊇ D 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. +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. + 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 @@ -131,6 +133,10 @@ single ridge path. | `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 | +| `CapHyp.of_const_mul` | a cap for `c f` at the levels `c b`, `c s` with `c > 0` is a cap for `f` at `b`, `s` (v2.4) | +| `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) | | `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 | @@ -203,7 +209,7 @@ The source gate checks: bound); - rebuilds the package fresh; - replays the module with `leanchecker`; -- prints the axioms of all 127 declarations, requiring exactly the manifest's report: each uses only `propext`, +- prints the axioms of all 132 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 57bdae9c9..8b2517c5b 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"]), 127) + self.assertEqual(len(m["targets"]), 132) self.assertEqual(m['scientific_effect'], 'NONE') def copy(self):