d6g8k5htny-coder · Oct 5, 2026 · Oct 5, 2026 · Oct 5, 2026
@@ -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.