diff --git a/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md b/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md
index 31cbb4973..ef05eb264 100644
--- a/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md
+++ b/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md
@@ -109,6 +109,9 @@ The source setting (SP §2) is as follows:
 | `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. |
+| `addCircle_locallyConnectedSpace`, `torus_locallyConnectedSpace` | `ℝ/Lℤ` and `(ℝ/Lℤ)^d` are locally connected | the older-peak theorems' hypothesis, on the torus | The covering map `ℝ → ℝ/Lℤ` is a quotient map, so the circle's topology is coinduced from `ℝ`, and local connectedness passes to coinduced topologies (`IsCoinducing.locallyConnectedSpace`). A finite product of locally connected spaces is locally connected. Compactness for `L > 0` is Mathlib's instance. |
+| `torus_capHyp_blocks` | `φ : ℝ × E ≃ₜ ℝ^d`; `g p = f (torusCover L d (φ p))` for every `p`; the hypotheses of `ridge_capHyp_blocks` for `g` ⇒ `∃ z` with `CapHyp f (T '' C) (T M) z (f (T M)) (f (T S))` and (C2⁺) on the frontier of `T '' C`, where `T = torusCover L d ∘ φ`, `M = (−r/2, 0)` and `S = (r/2, 0)` | P §7: the cap theorem applied to the periodic lift in a contact frame; SP §2's frame `φ` | `ridge_capHyp_blocks` for `g`, then `CapHyp.toTorus` and `CapHyp.map_saddle`. The cap `C` is compact because `E` is finite-dimensional. `φ` is any homeomorphism; P's contact frame, an affine isometry, is one. |
+| `torus_elder_death_level_blocks` | as `torus_capHyp_blocks`, with `L > 0` and `f` continuous ⇒ `IsGreatest (olderPeakLevels f (T M)) (f (T S))` | SP L22, P §8: the death level of the class born at `M` | `elder_death_level_peak` on the torus, which is compact and locally connected. Identifying this level with the pairing of the persistence module is I2. |
 | `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. |
 
@@ -145,7 +148,10 @@ The ridge toy has `δ = 2`, below SP's `δ > rm(8m − 5) = 22`. So `spToyF (x,
 
 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
-torus.
+torus. Since v2.6 `torusToy_elder` exhibits one on `(ℝ/16ℤ)²`. `torusToyF` reads `mixedToyF` through the chart
+`circleChart L θ = ‖θ + L/4‖ − L/4`, which inverts the covering map on `[−L/4, L/4]`, so its lift equals `mixedToyF` on
+`(−4, 4)²`. `torus_elder_death_level_blocks` applies with `r = 1`, `k = 1/6`, `M3 = 2`, `M4 = 0` and `λ = 41`: the death
+level of the class born at the image of `M` is the value at the image of `S`.
 
 The toy is one-dimensional, so its "saddle" `S = 1` is a local minimum, the index-`d−1` point for `d = 1`. The toy
 illustrates the hypotheses; it is not a model of the planar cap.
@@ -154,9 +160,9 @@ 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`). 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`. |
+| 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`. Since v2.6 the composition is proved: `torus_capHyp_blocks` takes CAP (1) for the lift `f ∘ torusCover L d ∘ φ` in any frame `φ : ℝ × E ≃ₜ ℝ^d` and concludes on the torus, and `torus_elder_death_level_blocks` gives the elder death level there. What stays informal is only the reading of P's contact frame (an affine isometry, hence such a `φ`) and of P's field as these objects. |
 | 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. |
+| 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. Since v2.5 and v2.6 no analytic step remains: `ridge_capHyp_blocks` and `torus_capHyp_blocks` take P §7's `G_r` exactly (CAP (1) with CAP's partial-block norms and `λ`) for the periodic lift in the frame, together with `f ∈ C⁴` near `D`. That the lift of the Gaussian field is `C⁴` almost surely is P §2's input, on the probability side (I4). |
 | I4 | Theorem A, measurability, `Q^W(G_r^c) ≤ C r³` | P §§7–8, C1, G1 | probability |
 
 ## 5. Review contract
@@ -173,5 +179,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. 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
+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. v2.6 adds three §2 rows (`addCircle_locallyConnectedSpace` to `torus_elder_death_level_blocks`, four declarations, two of them in a new section `Torus`), the `torusToy_elder` sentence of §3 (ten declarations: `circleChart`, `circleChart_continuous`, `circleChart_coe`, the five `mixedToy_*` derivative lemmas, `torusToyF` and `torusToy_elder`) and revisions of I1 and I3. Its 138 v2.5 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 123d1a780..01744e2cf 100644
--- a/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean
+++ b/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean
@@ -38,6 +38,9 @@
   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`.
+  Since v2.6 `torus_capHyp_blocks` and `torus_elder_death_level_blocks` state the cap and the elder
+  death level on the torus `(ℝ/Lℤ)^d` for a field whose periodic lift meets CAP (1) in any frame;
+  `torusToy_elder` is a concrete instance on `(ℝ/16ℤ)²`.
   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.
@@ -5179,4 +5182,292 @@ theorem mixedToy_blocks :
   obtain ⟨-, -, hC, -⟩ := hcap (fun _ => 0) (fun x _ => ⟨by simp, hcrit0 x⟩)
   exact ⟨⟨ε, hε, hex⟩, hC⟩
 
+/-! ### v2.6: the cap and the elder death level on the torus, under CAP (1)
+
+P §7 applies the cap theorem to the periodic lift of the field on `(ℝ/Lℤ)^d`, in a contact frame
+whose first axis joins the pins. `torus_capHyp_blocks` composes `ridge_capHyp_blocks` (v2.5) with
+`CapHyp.toTorus` and `CapHyp.map_saddle` for any frame `φ : ℝ × E ≃ₜ ℝ^d`. Then
+`torus_elder_death_level_blocks` adds `elder_death_level_peak` on the torus, which is compact
+(`L > 0`) and locally connected (`torus_locallyConnectedSpace`). `torusToy_elder` instantiates it
+on `(ℝ/16ℤ)²`. -/
+
+/-- The circle `ℝ/Lℤ` is locally connected: its topology is coinduced by the covering map from
+`ℝ`, and local connectedness passes to coinduced topologies. -/
+theorem addCircle_locallyConnectedSpace (L : ℝ) : LocallyConnectedSpace (AddCircle L) :=
+  (QuotientAddGroup.isQuotientMap_mk (AddSubgroup.zmultiples L)).isCoinducing.locallyConnectedSpace
+
+/-- The torus `(ℝ/Lℤ)^d` is locally connected: a finite product of locally connected spaces. -/
+theorem torus_locallyConnectedSpace (L : ℝ) (d : ℕ) :
+    LocallyConnectedSpace (Fin d → AddCircle L) :=
+  haveI := addCircle_locallyConnectedSpace L
+  Pi.locallyConnectedSpace_of_finite_not_preconnectedSpace (Set.toFinite _)
+
+section Torus
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+
+/-- **The cap on the torus under CAP (1).** Let `φ : ℝ × E ≃ₜ ℝ^d` be any frame and let
+`g = f ∘ torusCover L d ∘ φ` be the lift of a function `f` on the torus `(ℝ/Lℤ)^d`. If `g` meets
+the hypotheses of `ridge_capHyp_blocks` (CAP §1's (1) with its partial-block norms, in the frame
+`φ`), then `f` satisfies (C1)–(C3) on the image of the cap in the torus, with `M` and `S` the images
+of the pins, and (C2⁺): every other frontier point of the image is strictly below `f(S)`. -/
+theorem torus_capHyp_blocks [FiniteDimensional ℝ E] {L : ℝ} {d : ℕ}
+    (φ : ℝ × E ≃ₜ (Fin d → ℝ)) {f : (Fin d → AddCircle L) → ℝ} {g : ℝ × E → ℝ}
+    (hg : ∀ p, g p = f (torusCover L d (φ p))) {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 g U)
+    (h30 : ∀ x ∈ Icc (-r / 2) (r / 2), |iteratedFDeriv ℝ 3 g (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 g 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 g 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 g 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 g 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 g p ![(0, v), (1, 0), (1, 0), (1, 0)]| ≤ M4 * ‖v‖)
+    (hlam : ∀ v : E, iteratedFDeriv ℝ 2 g (-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 ℝ g (-r / 2, 0) = 0) (hS : fderiv ℝ g (r / 2, 0) = 0)
+    (hnorm : g (-r / 2, 0) - g (r / 2, 0) = k * r ^ 3) :
+    ∃ z, CapHyp f ((torusCover L d ∘ φ) '' (Icc (-2 * r) (r / 2) ×ˢ Metric.closedBall (0 : E) (2 * r)))
+        (torusCover L d (φ (-r / 2, 0))) z (f (torusCover L d (φ (-r / 2, 0))))
+        (f (torusCover L d (φ (r / 2, 0)))) ∧
+      ∀ x ∈ frontier ((torusCover L d ∘ φ) ''
+          (Icc (-2 * r) (r / 2) ×ˢ Metric.closedBall (0 : E) (2 * r))),
+        x ≠ torusCover L d (φ (r / 2, 0)) → f x < f (torusCover L d (φ (r / 2, 0))) := by
+  obtain ⟨ε, -, ⟨h0, hh0⟩, hall⟩ := ridge_capHyp_blocks hr hk hU hDU hf h30 h31 h32 h33 h40 h41
+    hlam hH1 hH2 hM hS hnorm
+  obtain ⟨-, -, hC, hSf⟩ := hall h0 fun x hx => ⟨Metric.ball_subset_closedBall (hh0 x hx).1,
+    (hh0 x hx).2⟩
+  have hgf : g = f ∘ (torusCover L d ∘ φ) := funext hg
+  subst hgf
+  have hK : IsCompact (Icc (-2 * r) (r / 2) ×ˢ Metric.closedBall (0 : E) (2 * r)) :=
+    isCompact_Icc.prod (isCompact_closedBall 0 (2 * r))
+  exact ⟨_, hC.toTorus φ hK, CapHyp.map_saddle ((torusCover_continuous L d).comp φ.continuous)
+    ((torusCover_isOpenMap L d).comp φ.isOpenMap) hK hSf⟩
+
+/-- **The elder death level on the torus under CAP (1).** For `L > 0` and a continuous `f` on
+`(ℝ/Lℤ)^d` whose lift in the frame `φ` meets CAP §1's (1), the largest level at which the
+component of the image of `M` contains a strictly higher local maximum is `f` at the image of `S`.
+This is `elder_death_level_peak` on the torus, which is compact and locally connected. -/
+theorem torus_elder_death_level_blocks [FiniteDimensional ℝ E] {L : ℝ} [Fact (0 < L)] {d : ℕ}
+    (φ : ℝ × E ≃ₜ (Fin d → ℝ)) {f : (Fin d → AddCircle L) → ℝ} (hfc : Continuous f)
+    {g : ℝ × E → ℝ} (hg : ∀ p, g p = f (torusCover L d (φ p))) {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 g U)
+    (h30 : ∀ x ∈ Icc (-r / 2) (r / 2), |iteratedFDeriv ℝ 3 g (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 g 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 g 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 g 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 g 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 g p ![(0, v), (1, 0), (1, 0), (1, 0)]| ≤ M4 * ‖v‖)
+    (hlam : ∀ v : E, iteratedFDeriv ℝ 2 g (-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 ℝ g (-r / 2, 0) = 0) (hS : fderiv ℝ g (r / 2, 0) = 0)
+    (hnorm : g (-r / 2, 0) - g (r / 2, 0) = k * r ^ 3) :
+    IsGreatest (CapHyp.olderPeakLevels f (torusCover L d (φ (-r / 2, 0))))
+      (f (torusCover L d (φ (r / 2, 0)))) := by
+  obtain ⟨z, H, -⟩ := torus_capHyp_blocks φ hg hr hk hU hDU hf h30 h31 h32 h33 h40 h41 hlam hH1
+    hH2 hM hS hnorm
+  have := torus_locallyConnectedSpace L d
+  exact H.elder_death_level_peak hfc rfl
+
+end Torus
+
+/-- A continuous chart of the circle near `0`: `circleChart L θ = ‖θ + L/4‖ − L/4`, which equals
+`x` at the image of every `x` with `|x| ≤ L/4` (`circleChart_coe`). -/
+noncomputable def circleChart (L : ℝ) (θ : AddCircle L) : ℝ :=
+  ‖θ + ((L / 4 : ℝ) : AddCircle L)‖ - L / 4
+
+/-- `circleChart` is continuous. -/
+theorem circleChart_continuous (L : ℝ) : Continuous (circleChart L) :=
+  (continuous_norm.comp (continuous_id.add continuous_const)).sub continuous_const
+
+/-- `circleChart L` inverts the covering map on `[−L/4, L/4]`. -/
+theorem circleChart_coe {L : ℝ} (hL : 0 < L) {x : ℝ} (hx : |x| ≤ L / 4) :
+    circleChart L (x : AddCircle L) = x := by
+  have h1 := (abs_le.mp hx).1
+  have h2 := (abs_le.mp hx).2
+  have hn : ‖((x + L / 4 : ℝ) : AddCircle L)‖ = |x + L / 4| :=
+    (AddCircle.norm_coe_eq_abs_iff L hL.ne').mpr (by
+      rw [abs_of_nonneg (by linarith), abs_of_pos hL]; linarith)
+  unfold circleChart
+  rw [← AddCircle.coe_add, hn, abs_of_nonneg (by linarith)]
+  ring
+
+/-- The derivative of `mixedToyF` (v2.5's toy), stated as a lemma for reuse. -/
+theorem mixedToy_hasFDerivAt (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
+  have hf : HasFDerivAt (fun q : ℝ × ℝ => q.1) (ContinuousLinearMap.fst ℝ ℝ ℝ) p := hasFDerivAt_fst
+  have hs : HasFDerivAt (fun q : ℝ × ℝ => q.2) (ContinuousLinearMap.snd ℝ ℝ ℝ) p := hasFDerivAt_snd
+  have h1 := HasFDerivAt.add (HasFDerivAt.sub (HasFDerivAt.sub
+    (HasFDerivAt.const_mul (HasFDerivAt.pow hf 3) (1 / 3))
+    (HasFDerivAt.const_mul hf (1 / 4)))
+    (HasFDerivAt.const_mul (HasFDerivAt.pow hs 2) 20))
+    (HasFDerivAt.mul hf (HasFDerivAt.pow hs 2))
+  convert h1 using 1
+  · funext q
+    simp only [mixedToyF, Pi.sub_apply, Pi.add_apply, Pi.mul_apply]
+    ring
+  · ext <;> simp
+    ring
+
+/-- `mixedToyF` is `C⁴`. -/
+theorem mixedToy_contDiff : ContDiff ℝ 4 mixedToyF := by unfold mixedToyF; fun_prop
+
+/-- The second derivative of `mixedToyF`. -/
+theorem mixedToy_iteratedFDeriv_two (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
+  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 hD2 : HasFDerivAt (fun q : ℝ × ℝ => (q.1 ^ 2 - 1 / 4 + q.2 ^ 2) •
+      ContinuousLinearMap.fst ℝ ℝ ℝ + (-40 * q.2 + 2 * q.1 * q.2) • ContinuousLinearMap.snd ℝ ℝ ℝ)
+      (((2 * y.1) • ContinuousLinearMap.fst ℝ ℝ ℝ + (2 * y.2) • ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight
+          (ContinuousLinearMap.fst ℝ ℝ ℝ) +
+        ((2 * y.2) • ContinuousLinearMap.fst ℝ ℝ ℝ +
+          (-40 + 2 * y.1) • ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight
+          (ContinuousLinearMap.snd ℝ ℝ ℝ)) y := by
+    have h1 : HasFDerivAt (fun q : ℝ × ℝ => q.1 ^ 2 - 1 / 4 + q.2 ^ 2)
+        ((2 * y.1) • ContinuousLinearMap.fst ℝ ℝ ℝ + (2 * y.2) • ContinuousLinearMap.snd ℝ ℝ ℝ) y := by
+      have := ((HasFDerivAt.pow (hf y) 2).sub_const (1 / 4)).add (HasFDerivAt.pow (hs y) 2)
+      convert this using 1
+      ext <;> simp
+    have h2 : HasFDerivAt (fun q : ℝ × ℝ => -40 * q.2 + 2 * q.1 * q.2)
+        ((2 * y.2) • ContinuousLinearMap.fst ℝ ℝ ℝ + (-40 + 2 * y.1) • ContinuousLinearMap.snd ℝ ℝ ℝ)
+        y := by
+      have := (HasFDerivAt.const_mul (hs y) (-40)).add
+        ((HasFDerivAt.const_mul (hf y) 2).mul (hs y))
+      convert this using 1
+      ext <;> simp
+      ring
+    exact (h1.smul_const (ContinuousLinearMap.fst ℝ ℝ ℝ)).add
+      (h2.smul_const (ContinuousLinearMap.snd ℝ ℝ ℝ))
+  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 => (mixedToy_hasFDerivAt p).fderiv
+  rw [iteratedFDeriv_two_apply, hfd, hD2.fderiv]
+  simp
+  ring
+
+/-- The third derivative of `mixedToyF`: `2a₁b₁c₁ + 2a₂(b₁c₂ + b₂c₁) + 2a₁b₂c₂`. -/
+theorem mixedToy_iteratedFDeriv_three (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
+  rw [DifferentiableAt.iteratedFDeriv_succ_apply_left'
+    (mixedToy_contDiff.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 [mixedToy_iteratedFDeriv_two]; simp [Fin.tail]; ring
+  rw [hg.fderiv]
+  simp
+  ring
+
+/-- The fourth derivative of `mixedToyF` vanishes. -/
+theorem mixedToy_iteratedFDeriv_four (x : ℝ × ℝ) (m : Fin 4 → ℝ × ℝ) :
+    iteratedFDeriv ℝ 4 mixedToyF x m = 0 := by
+  rw [DifferentiableAt.iteratedFDeriv_succ_apply_left'
+    (mixedToy_contDiff.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 [mixedToy_iteratedFDeriv_three, mixedToy_iteratedFDeriv_three]
+  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
+
+/-- A function on the torus `(ℝ/16ℤ)²` whose lift equals `mixedToyF` on `(−4, 4)²`:
+`mixedToyF` read through `circleChart` in each coordinate. It is continuous. -/
+noncomputable def torusToyF (θ : Fin 2 → AddCircle (16 : ℝ)) : ℝ :=
+  mixedToyF (circleChart 16 (θ 0), circleChart 16 (θ 1))
+
+/-- **A concrete instance of the elder death level on the torus.** On `(ℝ/16ℤ)²`, with the standard
+frame `ℝ × ℝ ≃ₜ ℝ²`, the lift of `torusToyF` agrees with `mixedToyF` near the cap, so it meets
+CAP (1) with `r = 1`, `k = 1/6`, `M3 = 2`, `M4 = 0` and `λ = 41`. `torus_elder_death_level_blocks`
+then gives the death level of the class born at the image of `M = (−1/2, 0)`: it is the value at
+the image of `S = (1/2, 0)`. This is the first concrete instance of the older-peak theorems
+(`older_peak`, `elder_death_level_peak`), whose compactness hypothesis fails on the earlier toys'
+domain `ℝ`. -/
+theorem torusToy_elder :
+    IsGreatest (CapHyp.olderPeakLevels torusToyF
+        (torusCover 16 2 ((Homeomorph.finTwoArrow (X := ℝ)).symm (-1 / 2, 0))))
+      (torusToyF (torusCover 16 2 ((Homeomorph.finTwoArrow (X := ℝ)).symm (1 / 2, 0)))) := by
+  have : Fact ((0 : ℝ) < 16) := ⟨by norm_num⟩
+  set φ : ℝ × ℝ ≃ₜ (Fin 2 → ℝ) := (Homeomorph.finTwoArrow (X := ℝ)).symm with hφ
+  set U : Set (ℝ × ℝ) := Ioo (-4) 4 ×ˢ Ioo (-4) 4 with hU_def
+  have hU : IsOpen U := isOpen_Ioo.prod isOpen_Ioo
+  have hGU : ∀ p ∈ U, torusToyF (torusCover 16 2 (φ p)) = mixedToyF p := by
+    rintro ⟨a, b⟩ ⟨ha, hb⟩
+    have ha' : |a| ≤ 16 / 4 := by rw [abs_le]; constructor <;> linarith [ha.1, ha.2]
+    have hb' : |b| ≤ 16 / 4 := by rw [abs_le]; constructor <;> linarith [hb.1, hb.2]
+    simp only [torusToyF, torusCover, hφ, Homeomorph.finTwoArrow_symm_apply, Pi.map_apply]
+    simp [circleChart_coe (by norm_num : (0 : ℝ) < 16) ha',
+      circleChart_coe (by norm_num : (0 : ℝ) < 16) hb']
+  have hev : ∀ p ∈ U, (fun q => torusToyF (torusCover 16 2 (φ q))) =ᶠ[nhds p] mixedToyF :=
+    fun p hp => Filter.eventuallyEq_of_mem (hU.mem_nhds hp) hGU
+  have hD : ∀ n p, p ∈ U → iteratedFDeriv ℝ n (fun q => torusToyF (torusCover 16 2 (φ q))) p =
+      iteratedFDeriv ℝ n mixedToyF p :=
+    fun n p hp => ((hev p hp).iteratedFDeriv ℝ n).eq_of_nhds
+  have hDU : Icc (-2 * 1) (2 * 1) ×ˢ Metric.closedBall (0 : ℝ) (2 * 1) ⊆ U := by
+    rintro ⟨a, b⟩ ⟨ha, hb⟩
+    rw [Metric.mem_closedBall, Real.dist_eq, sub_zero, abs_le] at hb
+    exact ⟨⟨by linarith [ha.1], by linarith [ha.2]⟩, ⟨by linarith [hb.1], by linarith [hb.2]⟩⟩
+  have hseg : ∀ x ∈ Icc (-1 / 2 : ℝ) (1 / 2), ((x, 0) : ℝ × ℝ) ∈ U := fun x hx =>
+    ⟨⟨by linarith [hx.1], by linarith [hx.2]⟩, ⟨by norm_num, by norm_num⟩⟩
+  have hM : ((-1 / 2, 0) : ℝ × ℝ) ∈ U := hseg _ ⟨by norm_num, by norm_num⟩
+  have hS : ((1 / 2, 0) : ℝ × ℝ) ∈ U := hseg _ ⟨by norm_num, by norm_num⟩
+  refine torus_elder_death_level_blocks (E := ℝ) (L := 16) (d := 2) φ
+    (mixedToy_contDiff.continuous.comp ((circleChart_continuous 16).comp (continuous_apply 0) |>.prodMk
+      ((circleChart_continuous 16).comp (continuous_apply 1))))
+    (g := fun q => torusToyF (torusCover 16 2 (φ q))) (fun p => rfl) (U := U)
+    (r := 1) (k := 1 / 6) (M3 := 2) (M4 := 0) (lam := 41) one_pos (by norm_num) hU hDU
+    (mixedToy_contDiff.contDiffOn.congr fun p hp => hGU p hp)
+    (fun x hx => ?_) (fun p hp y => ?_) (fun p hp y₁ y₂ => ?_) (fun p hp y₁ y₂ y₃ => ?_)
+    (fun p hp => ?_) (fun p hp v => ?_) (fun v => ?_) (by norm_num) (by norm_num) ?_ ?_ ?_
+  · rw [hD 3 _ (hseg _ (by simpa using hx)), mixedToy_iteratedFDeriv_three]; simp
+  · rw [hD 3 _ (hDU hp), mixedToy_iteratedFDeriv_three]; simp
+  · rw [hD 3 _ (hDU hp), mixedToy_iteratedFDeriv_three]
+    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]
+  · rw [hD 3 _ (hDU hp), mixedToy_iteratedFDeriv_three]
+    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
+  · rw [hD 4 _ (hDU hp), mixedToy_iteratedFDeriv_four]; simp
+  · rw [hD 4 _ (hDU hp), mixedToy_iteratedFDeriv_four]; simp
+  · rw [hD 2 _ (by simpa using hM), mixedToy_iteratedFDeriv_two]
+    simp only [Matrix.cons_val_zero, Matrix.cons_val_one, Real.norm_eq_abs, sq_abs]
+    nlinarith [sq_nonneg v]
+  · rw [(hev _ (by simpa using hM)).fderiv_eq, (mixedToy_hasFDerivAt _).fderiv]
+    ext <;> norm_num
+  · rw [(hev _ (by simpa using hS)).fderiv_eq, (mixedToy_hasFDerivAt _).fderiv]
+    ext <;> norm_num
+  · rw [hGU _ (by simpa using hM), hGU _ (by simpa using hS)]
+    simp only [mixedToyF]; norm_num
+
 end CapFirstExit
diff --git a/frontiers/cap_first_exit_lean_20261002/MANIFEST.json b/frontiers/cap_first_exit_lean_20261002/MANIFEST.json
index 3e3154602..d909b4778 100644
--- a/frontiers/cap_first_exit_lean_20261002/MANIFEST.json
+++ b/frontiers/cap_first_exit_lean_20261002/MANIFEST.json
@@ -170,7 +170,21 @@
   "CapFirstExit.block_of_partial",
   "CapFirstExit.ridge_capHyp_blocks",
   "CapFirstExit.mixedToyF",
-  "CapFirstExit.mixedToy_blocks"
+  "CapFirstExit.mixedToy_blocks",
+  "CapFirstExit.addCircle_locallyConnectedSpace",
+  "CapFirstExit.torus_locallyConnectedSpace",
+  "CapFirstExit.torus_capHyp_blocks",
+  "CapFirstExit.torus_elder_death_level_blocks",
+  "CapFirstExit.circleChart",
+  "CapFirstExit.circleChart_continuous",
+  "CapFirstExit.circleChart_coe",
+  "CapFirstExit.mixedToy_hasFDerivAt",
+  "CapFirstExit.mixedToy_contDiff",
+  "CapFirstExit.mixedToy_iteratedFDeriv_two",
+  "CapFirstExit.mixedToy_iteratedFDeriv_three",
+  "CapFirstExit.mixedToy_iteratedFDeriv_four",
+  "CapFirstExit.torusToyF",
+  "CapFirstExit.torusToy_elder"
  ],
  "expected_axioms": {
   "CapFirstExit.path_meets_frontier": [
@@ -862,6 +876,76 @@
    "Classical.choice",
    "Quot.sound",
    "propext"
+  ],
+  "CapFirstExit.addCircle_locallyConnectedSpace": [
+   "Classical.choice",
+   "Quot.sound",
+   "propext"
+  ],
+  "CapFirstExit.torus_locallyConnectedSpace": [
+   "Classical.choice",
+   "Quot.sound",
+   "propext"
+  ],
+  "CapFirstExit.torus_capHyp_blocks": [
+   "Classical.choice",
+   "Quot.sound",
+   "propext"
+  ],
+  "CapFirstExit.torus_elder_death_level_blocks": [
+   "Classical.choice",
+   "Quot.sound",
+   "propext"
+  ],
+  "CapFirstExit.circleChart": [
+   "Classical.choice",
+   "Quot.sound",
+   "propext"
+  ],
+  "CapFirstExit.circleChart_continuous": [
+   "Classical.choice",
+   "Quot.sound",
+   "propext"
+  ],
+  "CapFirstExit.circleChart_coe": [
+   "Classical.choice",
+   "Quot.sound",
+   "propext"
+  ],
+  "CapFirstExit.mixedToy_hasFDerivAt": [
+   "Classical.choice",
+   "Quot.sound",
+   "propext"
+  ],
+  "CapFirstExit.mixedToy_contDiff": [
+   "Classical.choice",
+   "Quot.sound",
+   "propext"
+  ],
+  "CapFirstExit.mixedToy_iteratedFDeriv_two": [
+   "Classical.choice",
+   "Quot.sound",
+   "propext"
+  ],
+  "CapFirstExit.mixedToy_iteratedFDeriv_three": [
+   "Classical.choice",
+   "Quot.sound",
+   "propext"
+  ],
+  "CapFirstExit.mixedToy_iteratedFDeriv_four": [
+   "Classical.choice",
+   "Quot.sound",
+   "propext"
+  ],
+  "CapFirstExit.torusToyF": [
+   "Classical.choice",
+   "Quot.sound",
+   "propext"
+  ],
+  "CapFirstExit.torusToy_elder": [
+   "Classical.choice",
+   "Quot.sound",
+   "propext"
   ]
  },
  "files": [
@@ -872,18 +956,18 @@
   },
   {
    "path": "ALIGNMENT.md",
-   "bytes": 53896,
-   "sha256": "bd516fef651e7b233d1309e7d7f9f774a1eeee5f3584030a838a6a80e1d94fb8"
+   "bytes": 57035,
+   "sha256": "91b086c04d083d2220821c8b6900e2bd070ad11f4be03bf2255bdbd83d677f21"
   },
   {
    "path": "CapFirstExit.lean",
-   "bytes": 307724,
-   "sha256": "f3993aab9348f24a090f2ecbb5fc9e12acc03fc2576045e3ca689d3443425688"
+   "bytes": 326607,
+   "sha256": "040aa91fcbdf25ccdaced1c828dd779318217a7c41ac928f87e8d17a8d3c3ef0"
   },
   {
    "path": "README.md",
-   "bytes": 28556,
-   "sha256": "cc4090d652f0ed03dbd19499b17c5f8d246a21aa1fd8124b4ff443724ea5a7c7"
+   "bytes": 30364,
+   "sha256": "826c0d67f25119f242575f65c29e70c2621266980b96527a428bbba6aa04a2ab"
   },
   {
    "path": "gate.py",
@@ -908,7 +992,7 @@
   {
    "path": "test_gate.py",
    "bytes": 6275,
-   "sha256": "a3600f82b6d86b37c30ba3752b6982f12435057bb5b0274d59ce74f2b9082c94"
+   "sha256": "4d6f32d2fd4c669a81bb5d23e600231305209af503806dabfb08c93a97720bba"
   }
  ]
 }
diff --git a/frontiers/cap_first_exit_lean_20261002/README.md b/frontiers/cap_first_exit_lean_20261002/README.md
index c0dce98e6..4f5e1bf09 100644
--- a/frontiers/cap_first_exit_lean_20261002/README.md
+++ b/frontiers/cap_first_exit_lean_20261002/README.md
@@ -68,12 +68,14 @@ Since v2.4, `ridge_capHyp_K` states the cap for every pin gap `k > 0`, on exactl
 
 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`.
 
+Since v2.6, the cap and the elder death level are stated on the torus. `torus_capHyp_blocks` takes CAP (1) for the periodic lift `f ∘ torusCover L d ∘ φ` of a field `f` on `(ℝ/Lℤ)^d`, in any frame `φ : ℝ × E ≃ₜ ℝ^d`, and concludes (C1)–(C3) and (C2⁺) on the torus. `torus_elder_death_level_blocks` adds the elder death level there, via `elder_death_level_peak`: the torus is compact for `L > 0` and locally connected (`torus_locallyConnectedSpace`). `torusToy_elder` is a concrete instance on `(ℝ/16ℤ)²`, the first for the older-peak theorems.
+
 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
   separation steps do not even use continuity of `f`.
 - The two older-peak theorems, `older_peak` and `elder_death_level_peak`, add compactness, local connectedness and
-  continuity of `f`. All three hold on the torus.
+  continuity of `f`. All three hold on the torus. Since v2.6 `torusToy_elder` is a concrete instance on `(ℝ/16ℤ)²`.
 
 | Lean declaration | Statement |
 |---|---|
@@ -143,6 +145,12 @@ single ridge path.
 | `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) |
+| `addCircle_locallyConnectedSpace`, `torus_locallyConnectedSpace` | `ℝ/Lℤ` and the torus `(ℝ/Lℤ)^d` are locally connected (v2.6) |
+| `torus_capHyp_blocks` | the cap and (C2⁺) on the torus for a field whose periodic lift meets CAP (1) in any frame `φ` (v2.6) |
+| `torus_elder_death_level_blocks` | with `L > 0` and `f` continuous, the elder death level of the class born at `M` on the torus is `f(S)` (v2.6) |
+| `circleChart`, `circleChart_continuous`, `circleChart_coe` | a continuous chart `‖θ + L/4‖ − L/4` of `ℝ/Lℤ` that inverts the covering map on `[−L/4, L/4]` (v2.6) |
+| `mixedToy_hasFDerivAt`, `mixedToy_contDiff`, `mixedToy_iteratedFDeriv_two`, `_three`, `_four` | the derivatives of `mixedToyF` as lemmas (v2.6) |
+| `torusToyF`, `torusToy_elder` | `mixedToyF` read through `circleChart` on `(ℝ/16ℤ)²`; its lift meets CAP (1) near the cap, and the elder death level of the image of `M` is the value at the image of `S` (v2.6) |
 | `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 |
@@ -180,7 +188,9 @@ This packet does not formalize:
   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`);
+  proved (`CapHyp.toTorus`, `frontier_cylinder`). Since v2.6 the composition with CAP (1) is proved too
+  (`torus_capHyp_blocks`, `torus_elder_death_level_blocks`), so only the reading of P's contact frame and field as
+  these objects is informal;
 - the definition of the H0 superlevel persistence pairing itself: that the class born at a local maximum `M` dies at
   the largest level at which its component contains a strictly higher local maximum. On a compact, locally connected
   space Lean proves that this level is `s` (`elder_death_level_peak`); only the persistence-module bookkeeping is
@@ -216,7 +226,7 @@ The source gate checks:
   bound);
 - rebuilds the package fresh;
 - replays the module with `leanchecker`;
-- prints the axioms of all 138 declarations, requiring exactly the manifest's report: each uses only `propext`,
+- prints the axioms of all 152 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 06fb433af..77a808695 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"]), 138)
+        self.assertEqual(len(m["targets"]), 152)
         self.assertEqual(m['scientific_effect'], 'NONE')
 
     def copy(self):