diff --git a/.github/workflows/cap-first-exit-lean.yml b/.github/workflows/cap-first-exit-lean.yml new file mode 100644 index 000000000..9d96705e3 --- /dev/null +++ b/.github/workflows/cap-first-exit-lean.yml @@ -0,0 +1,58 @@ +name: Cap first exit (Lean kernel evidence, no scientific promotion) + +'on': + pull_request: + paths: + - 'frontiers/cap_first_exit_lean_20261002/**' + - '.github/workflows/cap-first-exit-lean.yml' + - 'reviews/d1_cap_elder_partner_second_pass_claude_20260930/REVIEW.md' + - 'imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md' + workflow_dispatch: + +permissions: + contents: read + +jobs: + kernel-evidence: + runs-on: ubuntu-latest + timeout-minutes: 30 + env: + LEAN_NUM_THREADS: 2 + PYTHONDONTWRITEBYTECODE: '1' + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Source gate and unit tests in both Python modes (no Lean) + run: | + set -euo pipefail + P=frontiers/cap_first_exit_lean_20261002 + python -B -S -m unittest discover -s "$P" -p 'test_*.py' -v + python -B -O -S -m unittest discover -s "$P" -p 'test_*.py' -v + python -B -S "$P/gate.py" + - name: Install pinned Lean and retrieve the Mathlib cache + uses: leanprover/lean-action@50fcf42d2e460296f1a34b402e990d1b24f8b596 + with: + lake-package-directory: frontiers/cap_first_exit_lean_20261002 + auto-config: 'false' + build: 'false' + test: 'false' + lint: 'false' + use-mathlib-cache: 'true' + use-github-cache: 'false' + - name: Fresh build, leanchecker replay, axiom audit, negative controls + run: python -B -S frontiers/cap_first_exit_lean_20261002/gate.py --execute + - name: Tracked tree unchanged + run: git diff --exit-code + - name: Preserve logs and receipt + if: always() + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 + with: + name: cap-first-exit-lean-${{ github.run_id }}-${{ github.run_attempt }} + path: frontiers/cap_first_exit_lean_20261002/.lake/evidence/ + include-hidden-files: true + if-no-files-found: error + retention-days: 14 diff --git a/frontiers/cap_first_exit_lean_20261002/.gitignore b/frontiers/cap_first_exit_lean_20261002/.gitignore new file mode 100644 index 000000000..ae7367994 --- /dev/null +++ b/frontiers/cap_first_exit_lean_20261002/.gitignore @@ -0,0 +1,2 @@ +.lake/ +__pycache__/ diff --git a/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md b/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md new file mode 100644 index 000000000..394f4bf91 --- /dev/null +++ b/frontiers/cap_first_exit_lean_20261002/ALIGNMENT.md @@ -0,0 +1,110 @@ +# Alignment: Lean statements against the source lines + +**Sources, pinned by git blob on main and checked by `gate.py`:** + +| Source | Path | Role | +|---|---|---| +| SP | `reviews/d1_cap_elder_partner_second_pass_claude_20260930/REVIEW.md` | the line-numbered reconstruction of CAP §§2–5. L13, L16, L17 and L19–L22 are proved here. L7, L11, L12 and L18 enter `ridge_capHyp` as hypotheses. | +| CAP | `imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md` | the deterministic theorem that SP reconstructs | + +The source setting (SP §2) is as follows: + +- coordinates `(x, y) ∈ ℝ × ℝ^(d-1)`; +- pins `M = (-r/2, 0)` and `S = (r/2, 0)`; +- `b = f(M)` and `s = f(S) = b - r³/6`; +- the cap `C = [-2r, r/2] × B̄(0, 2r)`; +- the ridge `x ↦ (x, h(x))`. + +## 1. Hypotheses + +| Lean field | Lean statement | Source | Notes for the reviewer | +|---|---|---|---| +| `CapHyp.mem` | `M ∈ C` | SP L16 (`M = (-r/2, 0)`, `-2r ≤ -r/2 ≤ r/2`) | | +| `CapHyp.ceiling` | `∀ x ∈ C, f x ≤ b` | SP L16 | Lean does not require `f M = b`. The source has it, but no conclusion needs it. | +| `CapHyp.frontier_le` | `∀ x ∈ frontier C, f x ≤ s` | SP L17 (left face), L18 (curved side), L19 (right face) | `frontier` is the topological frontier in the ambient space `X`. See interface I1. | +| `CapHyp.older` | `b < f z` | SP L17 (`g(2r) ≥ b + 11r³/96`), L20 | `z = (2r, h(2r))` | +| `CapHyp.ridge` | `∃ γ : Path M z, ∀ t, s ≤ f (γ t)` | SP L20 | The source ridge is the graph of `h` on `[a, 2r]`. Its minimum is exactly `s`, at `S`. Lean needs only `≥ s`. | +| `hS` (in `path_through_saddle`, `saddle_cut`) | `∀ x ∈ frontier C, x ≠ S → f x < s` | SP L19, "only `S` attains it" | Strict on the left face (L17) and on the curved side (L18). Equality on the right face only at `S`. | + +## 2. Conclusions + +| Lean theorem | Statement | Source | Notes | +|---|---|---|---| +| `CapHyp.barrier` | every path from `M` to a point `> b` has a point with `f ≤ s` | SP L21, first two sentences | "Whatever it does afterwards": no constraint on the path outside `C`. | +| `connectionLevels`, `CapHyp.maximin_isGreatest`, `CapHyp.maximin_eq` | `IsGreatest {m ∣ ∃ w γ, b < f w ∧ ∀ t, m ≤ f (γ t)} s`, and `sSup = s` | SP L21, `d_f(M) = s` | The set's supremum is `sup_γ inf_t f(γ t)`. For continuous `f`, `inf_t` is SP's `min_γ f`. SP has `f(γ(1)) > f(M)`; Lean has `> b`, which is the same since `b = f(M)` in SP. | +| `component_joined` | a path inside `U` puts its endpoint in `M`'s component of `U` | standard | | +| `CapHyp.component_separated` | if `U` misses `frontier C`, then `M`'s component of `U` has no point `> b` | SP L21 in component form | Proved by `preconnected_subset_of_frontier_disjoint`. No path-connectedness and no continuity of `f`. | +| `CapHyp.elder_merge_iff_closed` | `(∃ w ∈ connectedComponentIn {x ∣ h ≤ f x} M, b < f w) ↔ h ≤ s` | SP L22 (filtration `{f ≥ t}`) | | +| `CapHyp.elder_merge_iff_open` | the same with `{x ∣ h < f x}` and `h < s` | the open-superlevel convention | Supplied so either convention can be used. | +| `CapHyp.joinedLevels`, `CapHyp.elder_death_level` | `IsGreatest {h ∣ ∃ w ∈ cc{f ≥ h}(M), b < f w} s` | SP L22, "the largest `t` at which it contains a point of value `> b`, i.e. at `t = d_f(M)`" | Both halves of SP's "i.e." are proved: the largest such `t` exists and is `s`, and `s = d_f(M)`. See interface I2. | +| `CapHyp.path_through_saddle` | under `hS`, every path from `M` to a point `> b` inside `{f ≥ s}` passes through `S` | SP L19 + L21 | | +| `CapHyp.saddle_cut`, `toy_saddle_cut` | under `hS` and `M ≠ S`: `M ∈ connectedComponentIn ({f ≥ s} \ {S}) M`, and every point of that component has `f ≤ b` | replaces SP L22's "distinct critical values make it `S`" | A topological identification of the merge point. Together with `elder_merge_iff_closed` at `h = s`, removing `S` at the death level disconnects `M` from every older point. The membership conjunct rules out the vacuous case `M = S`; SP's pins are distinct (`-r/2 ≠ r/2`). No Morse hypothesis. | +| `isClosed_connectedComponentIn` | a connected component of a closed set is closed | standard | Not in Mathlib at the pinned revision; proved from `IsPreconnected.closure`. | +| `CapHyp.older_peak` | `[CompactSpace X] [LocallyConnectedSpace X]`, `Continuous f`, `h ≤ s` ⇒ `∃ p ∈ cc{f ≥ h}(M), b < f p ∧ IsLocalMax f p ∧ ∀ w ∈ cc{f ≥ h}(M), f w ≤ f p` | SP L22, "the older endpoint" | Compactness gives the maximum over the closed component. Local connectedness makes that maximum a local maximum of `f` on `X`: the `{f > h}`-component of `p` is an open neighbourhood inside the component. | +| `CapHyp.elder_alive` | `f M = b`, `s < h` ⇒ `∀ w ∈ cc{f ≥ h}(M), f w ≤ f M` | SP L22, the class is alive above `s` | No compactness needed. | +| `CapHyp.olderPeakLevels`, `CapHyp.elder_death_level_peak` | `IsGreatest {h ∣ ∃ p ∈ cc{f ≥ h}(M), f M < f p ∧ IsLocalMax f p} s` | SP L22, the death level | This is the elder rule's death level, stated with older local maxima instead of older points. | +| `frontier_image_subset` | `Continuous e`, `IsOpenMap e`, `T2Space X`, `IsCompact C` ⇒ `frontier (e '' C) ⊆ e '' frontier C` | I1 | No injectivity: if a preimage of a frontier point were interior to `C`, the open map would make the point interior to `e '' C`. | +| `CapHyp.map`, `CapHyp.map_saddle` | `CapHyp (f ∘ e) C M z b s` ⇒ `CapHyp f (e '' C) (e M) (e z) b s`; and (C2⁺) for the lift ⇒ (C2⁺) for `e S` | I1 | | +| `torusCover`, `torusCover_continuous`, `torusCover_isOpenMap`, `CapHyp.toTorus` | for any frame `φ : Y ≃ₜ ℝ^d`, a cap for `f ∘ torusCover L d ∘ φ` on compact `C` gives a cap for `f` on the torus `(ℝ/Lℤ)^d` | I1; SP §2's coordinates, "every frame" | The torus is `Fin d → AddCircle L`. | +| `frontier_cylinder`, `isCompact_cylinder` | `frontier (Icc a c ×ˢ closedBall 0 R) = {a, c} ×ˢ closedBall 0 R ∪ Icc a c ×ˢ sphere 0 R` for `a ≤ c`, `R ≠ 0`, in `ℝ × E` with `E` a real normed space; compact when `E` is proper | SP L16–L19 (`a = -2r`, `c = r/2`, `R = 2r`) | The three pieces are L17's left face, L19's right face and L18's curved side. | +| `convex_zeros_between`, `convex_zeros_left`, `convex_zeros_right` | a convex function vanishing at `a < c` is `≤ 0` on `[a, c]` and `≥ 0` outside | SP L13, L17 | Uses `ConvexOn.le_on_segment` and `ConvexOn.slope_mono_adjacent`. | +| `ridge_profile` | on `D = [-2r, 2r]`: `g' = F`, `F(-r/2) = F(r/2) = 0`, `ConvexOn D (F - (x + r/2)(x - r/2)/8)` ⇒ `g ≤ g(-r/2)` on `[-2r, r/2]`; `g(r/2) ≤ g` on `[-r/2, 2r]`; `g(-2r) ≤ g(-r/2) - 9r³/32`; `g(r/2) + 9r³/32 ≤ g(2r)` | SP L13 (sign pattern), L16 (ceiling along the ridge), L17 (both exact integrals `9r³/32`), L20 (ridge minimum) | SP states L12 as `F'' − 1/4 > 0`; Lean takes the weaker convexity of `F − q`. L17's integrals come from comparing `g` with `Q = x³/24 − r²x/32`, `Q' = q`. | +| `ridge_capHyp` | `CapHyp f C M z b s`, with `C = Icc (-2r) (r/2) ×ˢ closedBall 0 (2r)`, `M = (-r/2, h(-r/2))`, `z = (2r, h(2r))`, `b = g(-r/2)`, `s = g(r/2)` | SP L16, L17, L19, L20 | Hypotheses, all local as in SP: `hT` = L7's `f(x, y) ≤ g(x)` on `C`; `hg` = L11 on `[-2r, 2r]`; `hh` = continuity of `h` on `[-r/2, 2r]`; `hFa`, `hFc` = critical pins; `hconv` = L12 on `[-2r, 2r]`; `hside` = L18 (non-strict suffices); `hM` (`h(a) = 0` in SP); `hgap` (SP: `r³/6 < 9r³/32`). The ridge path does not need to stay in `C`. | +| `ridge_saddle_strict` | under `hTs` (the unique transverse maximizer, L7) and a strict `hside`, every frontier point other than `S = (r/2, h(r/2))` has `f < s` | SP L19, "only `S` attains it" | The left face is strict through `hgap`; the right face is strict through uniqueness. | +| `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. | + +## 3. Non-vacuity and necessity, proved in Lean + +The toy model is `toyF x = max (-|x|) (x - 2)` on `ℝ`, with: + +- the cap `[-2, 1]`; +- `M = 0`, `b = 0`; +- `S = 1`, `s = -1`; +- `z = 3`; +- the ridge `t ↦ 3t`. + +The proved facts are: + +- `toy_capHyp` and `toy_saddle_strict`: the toy satisfies (C1)–(C3) and (C2⁺). +- `toy_death_level`: the death level is `-1`. +- `toy_needs_C2`, at `s = -3/2`: Lean proves that (C1) and (C3) hold, that (C2) fails (`f(1) = -1 > -3/2`), and that + the maximin level is not `-3/2`. +- `toy_needs_C1`, at `b = -1/2`: Lean proves that (C2) and (C3) hold, that (C1) fails (`f(0) = 0 > -1/2`), and that + the maximin level is not `-1`. The witness is the constant path. +- `toy_needs_C3`, at `s = 5`: Lean proves that (C1), (C2) and `b < f(z)` hold, that no ridge exists (every path starts + at `f(M) = 0 < 5`), and that the maximin level is not `5`. + +Each necessity theorem is one conjunction, so it certifies its own premises, not only its conclusion. + +`ridgeToy_capHyp` and `ridgeToy_saddle_strict` instantiate `ridge_capHyp` and `ridge_saddle_strict` at SP's normalization, with `r = 1`, `E = ℝ`, `f(x, y) = x³/3 − x/4 − y²`, `h = 0` and `F = x² − 1/4`. The gap there is exactly `r³/6`, so all ridge hypotheses are jointly satisfiable. + +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. + +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. + +## 4. Interfaces that stay informal + +| | 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. | +| 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 multi-variable analytic steps L1–L12 and L18, which supply `hT`, `hTs`, `hg`, `hFa`, `hFc`, `hconv`, `hside` and `hgap` of `ridge_capHyp` from `G_r` | SP L1–L12, L18; CAP §§2–5 | Hermite identity, increments, strong concavity, implicit function theorem, ridge identity, `F''` bound and curved-side estimate, with exact constants checked by SP's script, not in Lean. L13, L16, L17, L19 and L20 are proved in Lean from these outputs. | +| I4 | Theorem A, measurability, `Q^W(G_r^c) ≤ C r³` | P §§7–8, C1, G1 | probability | + +## 5. Review contract + +An alignment review should be written by a non-Claude lane (OpenAI/Codex, xAI/Grok, or another provider). Its record +names: + +- the reviewer's provider and agent; +- the exact head commit; +- the `MANIFEST.json` SHA-256. + +For each row of §§1–2, the record gives ALIGNED, MISALIGNED (with the corrected statement), or NOT ASSESSED. For each +row of §4, it says whether the interface is stated correctly. + +A changed Lean source, toolchain or pin makes an earlier review stale. 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 new file mode 100644 index 000000000..a5dd14bae --- /dev/null +++ b/frontiers/cap_first_exit_lean_20261002/CapFirstExit.lean @@ -0,0 +1,880 @@ +/- + CapFirstExit: the topological step from a separating cap to the global elder level. + + `CapHyp f C M z b s` bundles the conclusions that CAP §§2–5 derive from the local good event + `G_r` (reviews/d1_cap_elder_partner_second_pass_claude_20260930/REVIEW.md, L16–L20): + + (C1) `M ∈ C` and `f ≤ b` on the cap `C` (L16); + (C2) `f ≤ s` on the whole frontier of `C` (L17–L19); + (C3) `b < f z`, and a path from `M` to `z` along which `f ≥ s` (L17, L20). + + The saddle form adds (C2⁺): every frontier point other than `S` has `f < s` (L19). + + Nothing is assumed about `f` outside `C` beyond the witness path in (C3). The core theorems use + no metric, smoothness, Morse, compactness or probabilistic hypothesis, and their separation + statements do not even use continuity of `f`. `X` is an arbitrary topological space; the torus + is one instance. Only the older-peak theorems add compactness, local connectedness and + continuity of `f`, all of which hold on the torus. + + What this file does NOT formalize: the multi-variable analytic steps L1–L12 and L18 (they enter + `ridge_capHyp` as hypotheses; L13, L16, L17, L19 and L20 are proved from them); the + identification of the H0 persistence pairing with the elder rule (L22, P §8); the + unstable-branch analysis (L23); and every probabilistic statement. +-/ +import Mathlib + +open Set unitInterval + +namespace CapFirstExit + +variable {X : Type*} [TopologicalSpace X] + +/-! ### First exit -/ + +/-- First exit along a path. A path from a point of `C` to a point outside `C` meets the frontier +of `C`. -/ +theorem path_meets_frontier {C : Set X} {x y : X} (γ : Path x y) (hx : x ∈ C) (hy : y ∉ C) : + ∃ t : I, γ t ∈ frontier C := by + have hS : (γ ⁻¹' C).Nonempty := ⟨0, by simpa using hx⟩ + have hS' : γ ⁻¹' C ≠ univ := by + intro h + have h1 : (1 : I) ∈ γ ⁻¹' C := h ▸ mem_univ _ + exact hy (by simpa using h1) + obtain ⟨t, ht⟩ := nonempty_frontier_iff.mpr ⟨hS, hS'⟩ + exact ⟨t, γ.continuous.frontier_preimage_subset C ht⟩ + +/-- First exit for connected sets. A preconnected set that contains a point of `C` and does not +meet the frontier of `C` lies inside `C`. No path-connectedness is needed. -/ +theorem preconnected_subset_of_frontier_disjoint {C K : Set X} (hK : IsPreconnected K) {M : X} + (hMK : M ∈ K) (hMC : M ∈ C) (hfr : ∀ x ∈ K, x ∉ frontier C) : K ⊆ C := by + intro w hwK + by_contra hwC + have : PreconnectedSpace K := isPreconnected_iff_preconnectedSpace.mp hK + have hS : (((↑) : K → X) ⁻¹' C).Nonempty := ⟨⟨M, hMK⟩, hMC⟩ + have hS' : (((↑) : K → X) ⁻¹' C) ≠ univ := by + intro h + have h1 : (⟨w, hwK⟩ : K) ∈ (((↑) : K → X) ⁻¹' C) := h ▸ mem_univ _ + exact hwC h1 + obtain ⟨⟨x, hxK⟩, hx⟩ := nonempty_frontier_iff.mpr ⟨hS, hS'⟩ + exact hfr x hxK (continuous_subtype_val.frontier_preimage_subset C hx) + +/-! ### The cap hypotheses -/ + +/-- The cap hypotheses (C1)–(C3) for a local maximum `M` of height `b`, a separating level `s`, +and an older point `z`. -/ +structure CapHyp (f : X → ℝ) (C : Set X) (M z : X) (b s : ℝ) : Prop where + /-- (C1) `M` lies in the cap. -/ + mem : M ∈ C + /-- (C1) The ceiling: `f ≤ b` on the cap (L16). -/ + ceiling : ∀ x ∈ C, f x ≤ b + /-- (C2) The frontier bound: `f ≤ s` on the frontier of the cap (L17–L19). -/ + frontier_le : ∀ x ∈ frontier C, f x ≤ s + /-- (C3) The older endpoint: `f z > b` (L17). -/ + older : b < f z + /-- (C3) The ridge: a path from `M` to `z` along which `f ≥ s` (L20). -/ + ridge : ∃ γ : Path M z, ∀ t, s ≤ f (γ t) + +namespace CapHyp + +variable {f : X → ℝ} {C : Set X} {M z : X} {b s : ℝ} + +/-- `M` itself is at height at least `s` (the ridge starts at `M`). -/ +theorem s_le_f_M (H : CapHyp f C M z b s) : s ≤ f M := by + obtain ⟨γ, hγ⟩ := H.ridge + simpa using hγ 0 + +/-! ### The maximin level `d_f(M)` (L21) -/ + +/-- The upper barrier. Every path from `M` to a point strictly above `b` passes through a point +of height at most `s`, whatever the path does outside `C`. -/ +theorem barrier (H : CapHyp f C M z b s) {w : X} (hw : b < f w) (γ : Path M w) : + ∃ t : I, f (γ t) ≤ s := by + have hwC : w ∉ C := fun h => (not_le.mpr hw) (H.ceiling w h) + obtain ⟨t, ht⟩ := path_meets_frontier γ H.mem hwC + exact ⟨t, H.frontier_le _ ht⟩ + +end CapHyp + +/-- The connection levels of `M`: heights `m` such that some path from `M` to a point strictly +above `b` stays at height at least `m`. Its supremum is the maximin level `d_f(M)` of L21. -/ +def connectionLevels (f : X → ℝ) (M : X) (b : ℝ) : Set ℝ := + {m | ∃ (w : X) (γ : Path M w), b < f w ∧ ∀ t, m ≤ f (γ t)} + +namespace CapHyp + +variable {f : X → ℝ} {C : Set X} {M z : X} {b s : ℝ} + +/-- The maximin level is attained and equals `s` (L21). -/ +theorem maximin_isGreatest (H : CapHyp f C M z b s) : + IsGreatest (connectionLevels f M b) s := by + obtain ⟨γ₀, hγ₀⟩ := H.ridge + refine ⟨⟨z, γ₀, H.older, hγ₀⟩, ?_⟩ + rintro m ⟨w, γ, hw, hγ⟩ + obtain ⟨t, ht⟩ := H.barrier hw γ + exact (hγ t).trans ht + +/-- `d_f(M) = s`, as a supremum (L21). -/ +theorem maximin_eq (H : CapHyp f C M z b s) : sSup (connectionLevels f M b) = s := + H.maximin_isGreatest.csSup_eq + +/-! ### Superlevel components: the persistence filtration (L22) -/ + +/-- Component separation. If `U` avoids the frontier of `C`, the connected component of `M` in +`U` lies in `C`, so it contains no point strictly above `b`. -/ +theorem component_separated (H : CapHyp f C M z b s) {U : Set X} + (hU : ∀ x ∈ frontier C, x ∉ U) {w : X} (hw : w ∈ connectedComponentIn U M) : f w ≤ b := by + have hMU : M ∈ U := by + by_contra hMU + rw [connectedComponentIn_eq_empty hMU] at hw + exact notMem_empty w hw + exact H.ceiling w (preconnected_subset_of_frontier_disjoint isPreconnected_connectedComponentIn + (mem_connectedComponentIn hMU) H.mem + (fun x hx hxf => hU x hxf (connectedComponentIn_subset U M hx)) hw) + +end CapHyp + +/-- Component joining. If a path from `M` to `z` stays in `U`, then `z` lies in the connected +component of `M` in `U`. -/ +theorem component_joined {U : Set X} {M z : X} (γ : Path M z) (hγ : ∀ t, γ t ∈ U) : + z ∈ connectedComponentIn U M := by + have hsub : range γ ⊆ U := by + rintro _ ⟨t, rfl⟩ + exact hγ t + exact (isConnected_range γ.continuous).isPreconnected.subset_connectedComponentIn + ⟨0, γ.source⟩ hsub ⟨1, γ.target⟩ + +namespace CapHyp + +variable {f : X → ℝ} {C : Set X} {M z : X} {b s : ℝ} + +/-- **Elder merge, closed superlevel filtration `{f ≥ h}`** (the filtration of L22). The connected +component of `M` in `{f ≥ h}` contains a point strictly above `b` if and only if `h ≤ s`. -/ +theorem elder_merge_iff_closed (H : CapHyp f C M z b s) (h : ℝ) : + (∃ w ∈ connectedComponentIn {x | h ≤ f x} M, b < f w) ↔ h ≤ s := by + constructor + · rintro ⟨w, hw, hbw⟩ + by_contra hhs + rw [not_le] at hhs + have hU : ∀ x ∈ frontier C, x ∉ {x | h ≤ f x} := by + intro x hx hxU + have h1 : h ≤ f x := hxU + have h2 := H.frontier_le x hx + linarith + exact absurd (H.component_separated hU hw) (not_le.mpr hbw) + · intro hhs + obtain ⟨γ₀, hγ₀⟩ := H.ridge + exact ⟨z, component_joined γ₀ (fun t => le_trans hhs (hγ₀ t)), H.older⟩ + +/-- **Elder merge, open superlevel filtration `{f > h}`.** The connected component of `M` in +`{f > h}` contains a point strictly above `b` if and only if `h < s`. -/ +theorem elder_merge_iff_open (H : CapHyp f C M z b s) (h : ℝ) : + (∃ w ∈ connectedComponentIn {x | h < f x} M, b < f w) ↔ h < s := by + constructor + · rintro ⟨w, hw, hbw⟩ + by_contra hhs + rw [not_lt] at hhs + have hU : ∀ x ∈ frontier C, x ∉ {x | h < f x} := by + intro x hx hxU + have h1 : h < f x := hxU + have h2 := H.frontier_le x hx + linarith + exact absurd (H.component_separated hU hw) (not_le.mpr hbw) + · intro hhs + obtain ⟨γ₀, hγ₀⟩ := H.ridge + exact ⟨z, component_joined γ₀ (fun t => lt_of_lt_of_le hhs (hγ₀ t)), H.older⟩ + +/-- The set of levels at which the class born at `M` is joined to an older point. -/ +def joinedLevels (f : X → ℝ) (M : X) (b : ℝ) : Set ℝ := + {h | ∃ w ∈ connectedComponentIn {x | h ≤ f x} M, b < f w} + +/-- **Elder death level.** In the closed superlevel filtration, the largest level at which the +component of `M` contains an older point exists and equals `s`, whatever `f` does outside the cap. +This is the death level of the class born at `M` in L22. -/ +theorem elder_death_level (H : CapHyp f C M z b s) : IsGreatest (joinedLevels f M b) s := + ⟨(H.elder_merge_iff_closed s).mpr le_rfl, fun _ hh => (H.elder_merge_iff_closed _).mp hh⟩ + +/-! ### The merging saddle -/ + +/-- Every path from `M` to a point strictly above `b` that stays in `{f ≥ s}` passes through `S`, +when `S` is the only frontier point at height `s` (C2⁺, L19). The statement says something only when +`M ≠ S`, as in the source, where the pins are distinct. -/ +theorem path_through_saddle (H : CapHyp f C M z b s) {S : X} + (hS : ∀ x ∈ frontier C, x ≠ S → f x < s) {w : X} (hw : b < f w) (γ : Path M w) + (hγ : ∀ t, s ≤ f (γ t)) : ∃ t, γ t = S := by + have hwC : w ∉ C := fun h => (not_le.mpr hw) (H.ceiling w h) + obtain ⟨t, ht⟩ := path_meets_frontier γ H.mem hwC + refine ⟨t, ?_⟩ + by_contra hne + have h1 := hS _ ht hne + have h2 := hγ t + linarith + +/-- **`S` is a cut point at the death level.** Assume (C2⁺) and `M ≠ S`. Then `M` lies in its own +component of `{f ≥ s} \ {S}`, so the statement is not vacuous, and that component contains no +point strictly above `b`. By contrast, `{f ≥ s}` itself joins `M` to an older point +(`elder_merge_iff_closed` at `h = s`). Removing `S` therefore disconnects `M` from every older +point at the death level. -/ +theorem saddle_cut (H : CapHyp f C M z b s) {S : X} + (hS : ∀ x ∈ frontier C, x ≠ S → f x < s) (hMS : M ≠ S) : + M ∈ connectedComponentIn ({x | s ≤ f x} \ {S}) M ∧ + ∀ w ∈ connectedComponentIn ({x | s ≤ f x} \ {S}) M, f w ≤ b := by + refine ⟨mem_connectedComponentIn ⟨H.s_le_f_M, hMS⟩, fun w hw => ?_⟩ + refine H.component_separated (fun x hx hxU => ?_) hw + obtain ⟨h1, h2⟩ := hxU + have h3 := hS x hx h2 + have h4 : s ≤ f x := h1 + linarith + +/-! ### Exterior invariance -/ + +/-- **Exterior invariance.** Any `g` that agrees with `f` on the closure of the cap and along one +ridge path satisfies the same cap hypotheses. Every conclusion above (maximin level, elder merge +levels, death level, saddle cut) therefore holds for `g` with the same `s`, however `g` behaves +elsewhere: remote saddles, high corridors and re-entries change nothing. -/ +theorem congr {g : X → ℝ} (H : CapHyp f C M z b s) (γ₀ : Path M z) (hγ₀ : ∀ t, s ≤ f (γ₀ t)) + (hgC : ∀ x ∈ closure C, g x = f x) (hgγ : ∀ t, g (γ₀ t) = f (γ₀ t)) : + CapHyp g C M z b s where + mem := H.mem + ceiling x hx := (hgC x (subset_closure hx)).symm ▸ H.ceiling x hx + frontier_le x hx := (hgC x (frontier_subset_closure hx)).symm ▸ H.frontier_le x hx + older := by + have h1 := hgγ 1 + rw [γ₀.target] at h1 + rw [h1] + exact H.older + ridge := ⟨γ₀, fun t => (hgγ t).symm ▸ hγ₀ t⟩ + +end CapHyp + +/-! ### The elder-rule interface on a compact, locally connected space + +The elder rule pairs the class born at `M` with the level at which its superlevel component first +contains a strictly higher local maximum (an older class). On a compact, locally connected space +with continuous `f` (a closed manifold, in particular the torus), the following theorems identify +that level as `s`. -/ + +/-- A connected component of a closed set is closed. -/ +theorem isClosed_connectedComponentIn {F : Set X} (hF : IsClosed F) (x : X) : + IsClosed (connectedComponentIn F x) := by + by_cases hx : x ∈ F + · refine isClosed_of_closure_subset ?_ + exact isPreconnected_connectedComponentIn.closure.subset_connectedComponentIn + (subset_closure (mem_connectedComponentIn hx)) + (closure_minimal (connectedComponentIn_subset F x) hF) + · rw [connectedComponentIn_eq_empty hx] + exact isClosed_empty + +namespace CapHyp + +variable {f : X → ℝ} {C : Set X} {M z : X} {b s : ℝ} + +/-- **An older peak below the death level.** For every level `h ≤ s`, the component of `M` in +`{f ≥ h}` contains a point `p` with `f p > b` that maximizes `f` over the component and is a local +maximum of `f` on `X`: the older class that absorbs the class born at `M`. -/ +theorem older_peak [CompactSpace X] [LocallyConnectedSpace X] (H : CapHyp f C M z b s) + (hf : Continuous f) {h : ℝ} (hh : h ≤ s) : + ∃ p ∈ connectedComponentIn {x | h ≤ f x} M, b < f p ∧ IsLocalMax f p ∧ + ∀ w ∈ connectedComponentIn {x | h ≤ f x} M, f w ≤ f p := by + have hF : IsClosed {x | h ≤ f x} := isClosed_le continuous_const hf + obtain ⟨w, hwK, hbw⟩ := (H.elder_merge_iff_closed h).mpr hh + obtain ⟨p, hpK, hpmax⟩ := (isClosed_connectedComponentIn hF M).isCompact.exists_isMaxOn + ⟨w, hwK⟩ hf.continuousOn + have hmax : ∀ x ∈ connectedComponentIn {x | h ≤ f x} M, f x ≤ f p := isMaxOn_iff.mp hpmax + have hbp : b < f p := lt_of_lt_of_le hbw (hmax w hwK) + have hsb : s ≤ b := le_trans H.s_le_f_M (H.ceiling M H.mem) + have hpU : p ∈ {x | h < f x} := by + show h < f p + linarith + have hU : IsOpen {x | h < f x} := isOpen_lt continuous_const hf + have hVK : connectedComponentIn {x | h < f x} p ⊆ connectedComponentIn {x | h ≤ f x} M := by + rw [connectedComponentIn_eq hpK] + exact connectedComponentIn_mono p (fun x (hx : h < f x) => (le_of_lt hx : h ≤ f x)) + refine ⟨p, hpK, hbp, ?_, hmax⟩ + exact Filter.eventually_of_mem (hU.connectedComponentIn.mem_nhds (mem_connectedComponentIn hpU)) + (fun x hx => hmax x (hVK hx)) + +/-- **No older point above the death level.** For every level `h > s`, `M` is a highest point of +its component in `{f ≥ h}`, when `b = f M`: the class born at `M` is the elder of its component. -/ +theorem elder_alive (H : CapHyp f C M z b s) (hMb : f M = b) {h : ℝ} (hh : s < h) : + ∀ w ∈ connectedComponentIn {x | h ≤ f x} M, f w ≤ f M := by + intro w hw + rw [hMb] + by_contra hlt + rw [not_le] at hlt + exact absurd ((H.elder_merge_iff_closed h).mp ⟨w, hw, hlt⟩) (not_le.mpr hh) + +/-- The levels at which the component of `M` in `{f ≥ h}` contains a strictly higher local +maximum of `f`. -/ +def olderPeakLevels (f : X → ℝ) (M : X) : Set ℝ := + {h | ∃ p ∈ connectedComponentIn {x | h ≤ f x} M, f M < f p ∧ IsLocalMax f p} + +/-- **Elder death level, peak form.** On a compact, locally connected space with continuous `f` +and `b = f M`, the largest level at which the component of `M` contains a strictly higher local +maximum exists and equals `s`. This is the death level of the elder rule. -/ +theorem elder_death_level_peak [CompactSpace X] [LocallyConnectedSpace X] + (H : CapHyp f C M z b s) (hf : Continuous f) (hMb : f M = b) : + IsGreatest (olderPeakLevels f M) s := by + refine ⟨?_, fun h hh => ?_⟩ + · obtain ⟨p, hpK, hbp, hloc, -⟩ := H.older_peak hf le_rfl + exact ⟨p, hpK, hMb ▸ hbp, hloc⟩ + · obtain ⟨p, hpK, hMp, -⟩ := hh + exact (H.elder_merge_iff_closed h).mp ⟨p, hpK, hMb ▸ hMp⟩ + +end CapHyp + +/-! ### Charts: the cap on the torus and its faces + +The analysis of CAP §§2–5 runs in Euclidean coordinates on the periodic lift `f ∘ e` of a field +`f` on the torus, where `e : ℝ^d → T^d` is the covering map. The two lemmas below transport the cap +hypotheses to the torus and list the faces of the cylinder cap. The transport needs only that `e` +is continuous and open, that the target is Hausdorff and that the cap is compact; injectivity is +not used. -/ + +/-- Frontier of a compact image. If `e` is continuous and open, `X` is Hausdorff and `C` is +compact, every frontier point of `e '' C` is the image of a frontier point of `C`. -/ +theorem frontier_image_subset {Y : Type*} [TopologicalSpace Y] [T2Space X] {e : Y → X} + (hec : Continuous e) (heo : IsOpenMap e) {C : Set Y} (hC : IsCompact C) : + frontier (e '' C) ⊆ e '' frontier C := by + intro x hx + have hcl : IsClosed (e '' C) := (hC.image hec).isClosed + have hx1 : x ∈ e '' C := by + have h := hx.1 + rwa [hcl.closure_eq] at h + obtain ⟨y, hyC, rfl⟩ := hx1 + refine ⟨y, ⟨subset_closure hyC, fun hyi => hx.2 ?_⟩, rfl⟩ + exact interior_maximal (image_mono interior_subset) (heo _ isOpen_interior) ⟨y, hyi, rfl⟩ + +namespace CapHyp + +/-- **Transport along a chart.** The cap hypotheses for the lift `f ∘ e` on a compact cap `C` +give the cap hypotheses for `f` on `e '' C`, with the same `b` and `s`. -/ +theorem map {Y : Type*} [TopologicalSpace Y] [T2Space X] {e : Y → X} (hec : Continuous e) + (heo : IsOpenMap e) {f : X → ℝ} {C : Set Y} (hC : IsCompact C) {M z : Y} {b s : ℝ} + (H : CapHyp (f ∘ e) C M z b s) : CapHyp f (e '' C) (e M) (e z) b s where + mem := ⟨M, H.mem, rfl⟩ + ceiling := by + rintro _ ⟨y, hy, rfl⟩ + exact H.ceiling y hy + frontier_le := by + intro x hx + obtain ⟨y, hy, rfl⟩ := frontier_image_subset hec heo hC hx + exact H.frontier_le y hy + older := H.older + ridge := by + obtain ⟨γ, hγ⟩ := H.ridge + exact ⟨γ.map hec, fun t => hγ t⟩ + +/-- Transport of (C2⁺): if only `S` attains `s` on the frontier of `C` for the lift, only `e S` +attains it on the frontier of `e '' C`. -/ +theorem map_saddle {Y : Type*} [TopologicalSpace Y] [T2Space X] {e : Y → X} (hec : Continuous e) + (heo : IsOpenMap e) {f : X → ℝ} {C : Set Y} (hC : IsCompact C) {S : Y} {s : ℝ} + (hS : ∀ y ∈ frontier C, y ≠ S → (f ∘ e) y < s) : + ∀ x ∈ frontier (e '' C), x ≠ e S → f x < s := by + intro x hx hne + obtain ⟨y, hy, rfl⟩ := frontier_image_subset hec heo hC hx + exact hS y hy (fun h => hne (h ▸ rfl)) + +end CapHyp + +/-- **The faces of the cylinder cap** `[a, c] × B̄(0, R)`: the two end faces `{a, c} × B̄(0, R)` +and the curved side `[a, c] × S(0, R)`. These are the faces estimated in L17–L19. -/ +theorem frontier_cylinder {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {a c R : ℝ} + (hac : a ≤ c) (hR : R ≠ 0) : + frontier (Icc a c ×ˢ Metric.closedBall (0 : E) R) = + ({a, c} : Set ℝ) ×ˢ Metric.closedBall (0 : E) R ∪ Icc a c ×ˢ Metric.sphere (0 : E) R := by + rw [frontier_prod_eq, closure_Icc, frontier_closedBall (0 : E) hR, frontier_Icc hac, + Metric.isClosed_closedBall.closure_eq] + exact union_comm _ _ + +/-- The cylinder cap is compact in finite dimension. -/ +theorem isCompact_cylinder {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [ProperSpace E] + (a c R : ℝ) : IsCompact (Icc a c ×ˢ Metric.closedBall (0 : E) R) := + isCompact_Icc.prod (isCompact_closedBall 0 R) + +/-- The covering map of the flat torus `(ℝ / Lℤ)^d`. -/ +def torusCover (L : ℝ) (d : ℕ) : (Fin d → ℝ) → (Fin d → AddCircle L) := + Pi.map fun _ => ((↑) : ℝ → AddCircle L) + +theorem torusCover_continuous (L : ℝ) (d : ℕ) : Continuous (torusCover L d) := + Continuous.piMap fun _ => continuous_quotient_mk' + +theorem torusCover_isOpenMap (L : ℝ) (d : ℕ) : IsOpenMap (torusCover L d) := + IsOpenMap.piMap (fun _ => QuotientAddGroup.isOpenMap_coe) + (Filter.Eventually.of_forall fun _ => QuotientAddGroup.mk_surjective) + +/-- **The cap on the torus.** Let `φ` be any coordinate frame (a homeomorphism onto `ℝ^d`), and +suppose the periodic lift `f ∘ torusCover L d ∘ φ` satisfies the cap hypotheses on a compact cap +`C`. Then `f` satisfies them on the image of `C` in the torus `(ℝ / Lℤ)^d`, with the same `b` and +`s`. No embedding radius is used. -/ +theorem CapHyp.toTorus {Y : Type*} [TopologicalSpace Y] {L : ℝ} {d : ℕ} + (φ : Y ≃ₜ (Fin d → ℝ)) {f : (Fin d → AddCircle L) → ℝ} {C : Set Y} (hC : IsCompact C) + {M z : Y} {b s : ℝ} (H : CapHyp (f ∘ (torusCover L d ∘ φ)) C M z b s) : + CapHyp f ((torusCover L d ∘ φ) '' C) (torusCover L d (φ M)) (torusCover L d (φ z)) b s := + H.map ((torusCover_continuous L d).comp φ.continuous) + ((torusCover_isOpenMap L d).comp φ.isOpenMap) hC + +/-! ### From the ridge to the cap hypotheses (L13, L16, L17, L19, L20) + +SP §2 normalizes the pins to `x = a = -r/2` and `x = c = r/2`, on the cap +`C = [-2r, r/2] × B̄(0, 2r)` in coordinates `(x, y) ∈ ℝ × E`. The multi-variable analytic steps +enter as hypotheses, each the output of a named step of SP: +- `hT` (L7): on the cap, `f (x, y) ≤ f (x, h x)`, with `h` the transverse maximizer; +- `hg` (L11): the ridge function `g x = f (x, h x)` has derivative `F x`; +- `hFa`, `hFc` (L13): `F a = F c = 0`, because the pins are critical; +- `hconv` (L12): `F - q` is convex, where `q x = (x - a)(x - c)/8`; this is SP's `F'' ≥ 1/4`; +- `hside` (L18): on the curved side, `f ≤ g c`; +- `hgap`: `g a - g c < 9r³/32`. SP's normalization `g a - g c = r³/6` satisfies it. + +From these inputs Lean derives the rest: +- L13: the sign pattern of `F`; +- L16: the ceiling `g ≤ g a` on `[-2r, c]`; +- L17: both exact face integrals `9r³/32`, by comparing `g` with the cubic + `Q x = x³/24 - r²x/32`; +- L19: the face assembly; +- L20: the ridge path. -/ + +section Ridge + +/-- A convex function that vanishes at `a ≤ c` is `≤ 0` between them. -/ +theorem convex_zeros_between {φ : ℝ → ℝ} {D : Set ℝ} (hφ : ConvexOn ℝ D φ) {a c : ℝ} + (haD : a ∈ D) (hcD : c ∈ D) (hac : a ≤ c) (ha : φ a = 0) (hc : φ c = 0) {x : ℝ} + (hx : x ∈ Icc a c) : φ x ≤ 0 := by + have h := hφ.le_on_segment haD hcD (by rw [segment_eq_Icc hac]; exact hx) + rwa [ha, hc, max_self] at h + +/-- A convex function that vanishes at `a < c` is `≥ 0` to the right of `c`. -/ +theorem convex_zeros_right {φ : ℝ → ℝ} {D : Set ℝ} (hφ : ConvexOn ℝ D φ) {a c : ℝ} + (haD : a ∈ D) (hac : a < c) (ha : φ a = 0) (hc : φ c = 0) {x : ℝ} (hxD : x ∈ D) + (hx : c ≤ x) : 0 ≤ φ x := by + rcases eq_or_lt_of_le hx with rfl | hlt + · rw [hc] + · have h := hφ.slope_mono_adjacent haD hxD hac hlt + rw [ha, hc, sub_self, zero_div, sub_zero] at h + rw [le_div_iff₀ (sub_pos.mpr hlt), zero_mul] at h + exact h + +/-- A convex function that vanishes at `a < c` is `≥ 0` to the left of `a`. -/ +theorem convex_zeros_left {φ : ℝ → ℝ} {D : Set ℝ} (hφ : ConvexOn ℝ D φ) {a c : ℝ} + (hcD : c ∈ D) (hac : a < c) (ha : φ a = 0) (hc : φ c = 0) {x : ℝ} (hxD : x ∈ D) + (hx : x ≤ a) : 0 ≤ φ x := by + rcases eq_or_lt_of_le hx with rfl | hlt + · rw [ha] + · have h := hφ.slope_mono_adjacent hxD hcD hlt hac + rw [ha, hc, sub_self, zero_div, zero_sub] at h + rw [div_le_iff₀ (sub_pos.mpr hlt), zero_mul] at h + linarith + +/-- **The ridge profile (L13, L16, L17, L20).** On `D = [-2r, 2r]`, let `g' = F`, with `F` +vanishing at the pins `∓r/2` and `F - (x + r/2)(x - r/2)/8` convex. Then: +- `g ≤ g(-r/2)` on `[-2r, r/2]`; +- `g ≥ g(r/2)` on `[-r/2, 2r]`; +- `g(-2r) ≤ g(-r/2) - 9r³/32`; +- `g(2r) ≥ g(r/2) + 9r³/32`. -/ +theorem ridge_profile {g F : ℝ → ℝ} {r : ℝ} (hr : 0 < r) + (hg : ∀ x ∈ Icc (-2 * r) (2 * r), HasDerivAt g (F x) x) + (hFa : F (-r / 2) = 0) (hFc : F (r / 2) = 0) + (hconv : ConvexOn ℝ (Icc (-2 * r) (2 * r)) (fun x => F x - (x + r / 2) * (x - r / 2) / 8)) : + (∀ x ∈ Icc (-2 * r) (r / 2), g x ≤ g (-r / 2)) ∧ + (∀ x ∈ Icc (-r / 2) (2 * r), g (r / 2) ≤ g x) ∧ + g (-2 * r) ≤ g (-r / 2) - 9 * r ^ 3 / 32 ∧ g (r / 2) + 9 * r ^ 3 / 32 ≤ g (2 * r) := by + have hac : -r / 2 < r / 2 := by linarith + have haD : -r / 2 ∈ Icc (-2 * r) (2 * r) := ⟨by linarith, by linarith⟩ + have hcD : r / 2 ∈ Icc (-2 * r) (2 * r) := ⟨by linarith, by linarith⟩ + have hLD : Icc (-2 * r) (-r / 2) ⊆ Icc (-2 * r) (2 * r) := Icc_subset_Icc le_rfl (by linarith) + have hMD : Icc (-r / 2) (r / 2) ⊆ Icc (-2 * r) (2 * r) := + Icc_subset_Icc (by linarith) (by linarith) + have hRD : Icc (r / 2) (2 * r) ⊆ Icc (-2 * r) (2 * r) := Icc_subset_Icc (by linarith) le_rfl + set φ : ℝ → ℝ := fun x => F x - (x + r / 2) * (x - r / 2) / 8 with hφdef + have hφa : φ (-r / 2) = 0 := by simp only [hφdef, hFa]; ring + have hφc : φ (r / 2) = 0 := by simp only [hφdef, hFc]; ring + have hgc : ContinuousOn g (Icc (-2 * r) (2 * r)) := + fun x hx => (hg x hx).continuousAt.continuousWithinAt + -- L13: the sign pattern of `F` + have hFl : ∀ x ∈ Icc (-2 * r) (-r / 2), 0 ≤ F x := by + intro x hx + have h1 := convex_zeros_left hconv hcD hac hφa hφc (hLD hx) hx.2 + have h2 : 0 ≤ (x + r / 2) * (x - r / 2) / 8 := by + have : 0 ≤ (x + r / 2) * (x - r / 2) := + mul_nonneg_of_nonpos_of_nonpos (by linarith [hx.2]) (by linarith [hx.2]) + positivity + simp only [hφdef] at h1 + linarith + have hFm : ∀ x ∈ Icc (-r / 2) (r / 2), F x ≤ 0 := by + intro x hx + have h1 := convex_zeros_between hconv haD hcD hac.le hφa hφc hx + have h2 : (x + r / 2) * (x - r / 2) ≤ 0 := + mul_nonpos_of_nonneg_of_nonpos (by linarith [hx.1]) (by linarith [hx.2]) + simp only [hφdef] at h1 + linarith + have hFr : ∀ x ∈ Icc (r / 2) (2 * r), 0 ≤ F x := by + intro x hx + have h1 := convex_zeros_right hconv haD hac hφa hφc (hRD hx) hx.1 + have h2 : 0 ≤ (x + r / 2) * (x - r / 2) := mul_nonneg (by linarith [hx.1]) (by linarith [hx.1]) + simp only [hφdef] at h1 + linarith + -- monotonicity of `g` on the three pieces + have hmonoL : MonotoneOn g (Icc (-2 * r) (-r / 2)) := + monotoneOn_of_hasDerivWithinAt_nonneg (convex_Icc _ _) (hgc.mono hLD) + (fun x hx => (hg x (hLD (interior_subset hx))).hasDerivWithinAt) + (fun x hx => hFl x (interior_subset hx)) + have hantiM : AntitoneOn g (Icc (-r / 2) (r / 2)) := + antitoneOn_of_hasDerivWithinAt_nonpos (convex_Icc _ _) (hgc.mono hMD) + (fun x hx => (hg x (hMD (interior_subset hx))).hasDerivWithinAt) + (fun x hx => hFm x (interior_subset hx)) + have hmonoR : MonotoneOn g (Icc (r / 2) (2 * r)) := + monotoneOn_of_hasDerivWithinAt_nonneg (convex_Icc _ _) (hgc.mono hRD) + (fun x hx => (hg x (hRD (interior_subset hx))).hasDerivWithinAt) + (fun x hx => hFr x (interior_subset hx)) + -- L17: compare `g` with the cubic `Q`, whose derivative is `(x + r/2)(x - r/2)/8` + set Q : ℝ → ℝ := fun x => x ^ 3 / 24 - r ^ 2 * x / 32 with hQdef + have hQ : ∀ x, HasDerivAt Q ((x + r / 2) * (x - r / 2) / 8) x := by + intro x + have h1 := ((hasDerivAt_pow 3 x).div_const 24).sub ((hasDerivAt_id x).const_mul (r ^ 2 / 32)) + convert h1 using 1 + · funext y + simp only [hQdef, id, Pi.sub_apply] + ring + · push_cast + ring + have hG : ∀ x ∈ Icc (-2 * r) (2 * r), HasDerivAt (fun x => g x - Q x) (φ x) x := + fun x hx => (hg x hx).sub (hQ x) + have hGc : ContinuousOn (fun x => g x - Q x) (Icc (-2 * r) (2 * r)) := + fun x hx => (hG x hx).continuousAt.continuousWithinAt + have hGL : MonotoneOn (fun x => g x - Q x) (Icc (-2 * r) (-r / 2)) := + monotoneOn_of_hasDerivWithinAt_nonneg (convex_Icc _ _) (hGc.mono hLD) + (fun x hx => (hG x (hLD (interior_subset hx))).hasDerivWithinAt) + (fun x hx => convex_zeros_left hconv hcD hac hφa hφc (hLD (interior_subset hx)) + (interior_subset hx).2) + have hGR : MonotoneOn (fun x => g x - Q x) (Icc (r / 2) (2 * r)) := + monotoneOn_of_hasDerivWithinAt_nonneg (convex_Icc _ _) (hGc.mono hRD) + (fun x hx => (hG x (hRD (interior_subset hx))).hasDerivWithinAt) + (fun x hx => convex_zeros_right hconv haD hac hφa hφc (hRD (interior_subset hx)) + (interior_subset hx).1) + have hLa : (-r / 2 : ℝ) ∈ Icc (-2 * r) (-r / 2) := ⟨by linarith, le_rfl⟩ + have hL2 : (-2 * r : ℝ) ∈ Icc (-2 * r) (-r / 2) := ⟨le_rfl, by linarith⟩ + have hRc : (r / 2 : ℝ) ∈ Icc (r / 2) (2 * r) := ⟨le_rfl, by linarith⟩ + have hR2 : (2 * r : ℝ) ∈ Icc (r / 2) (2 * r) := ⟨by linarith, le_rfl⟩ + refine ⟨?_, ?_, ?_, ?_⟩ + · intro x hx + rcases le_or_gt x (-r / 2) with h | h + · exact hmonoL ⟨hx.1, h⟩ hLa h + · exact hantiM ⟨le_rfl, hac.le⟩ ⟨h.le, hx.2⟩ h.le + · intro x hx + rcases le_or_gt x (r / 2) with h | h + · exact hantiM ⟨hx.1, h⟩ ⟨hac.le, le_rfl⟩ h + · exact hmonoR hRc ⟨h.le, hx.2⟩ h.le + · have h := hGL hL2 hLa (by linarith) + simp only [hQdef] at h + nlinarith [h] + · have h := hGR hRc hR2 (by linarith) + simp only [hQdef] at h + nlinarith [h] + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + +/-- **The cap hypotheses from the ridge (L16, L17, L19, L20).** Under the analytic inputs listed +above, `f` satisfies (C1)–(C3) on `C = [-2r, r/2] × B̄(0, 2r)`, with `M = (-r/2, h(-r/2))`, +`z = (2r, h(2r))`, `b = g(-r/2)` and `s = g(r/2)`. Every input is local: `g' = F` and the convexity +hold on `[-2r, 2r]`, and `h` is continuous on `[-r/2, 2r]`. -/ +theorem ridge_capHyp {f : ℝ × E → ℝ} {h : ℝ → E} {F : ℝ → ℝ} {r : ℝ} (hr : 0 < r) + (hh : ContinuousOn h (Icc (-r / 2) (2 * r))) + (hg : ∀ x ∈ Icc (-2 * r) (2 * r), HasDerivAt (fun x => f (x, h x)) (F x) x) + (hFa : F (-r / 2) = 0) (hFc : F (r / 2) = 0) + (hconv : ConvexOn ℝ (Icc (-2 * r) (2 * r)) (fun x => F x - (x + r / 2) * (x - r / 2) / 8)) + (hT : ∀ p ∈ Icc (-2 * r) (r / 2) ×ˢ Metric.closedBall (0 : E) (2 * r), f p ≤ f (p.1, h p.1)) + (hside : ∀ p ∈ Icc (-2 * r) (r / 2) ×ˢ Metric.sphere (0 : E) (2 * r), + f p ≤ f (r / 2, h (r / 2))) + (hM : ‖h (-r / 2)‖ ≤ 2 * r) + (hgap : f (-r / 2, h (-r / 2)) - f (r / 2, h (r / 2)) < 9 * r ^ 3 / 32) : + CapHyp f (Icc (-2 * r) (r / 2) ×ˢ Metric.closedBall (0 : E) (2 * r)) (-r / 2, h (-r / 2)) + (2 * r, h (2 * r)) (f (-r / 2, h (-r / 2))) (f (r / 2, h (r / 2))) := by + obtain ⟨hceil, hfloor, hleft, hright⟩ := ridge_profile hr hg hFa hFc hconv + have hcyl : frontier (Icc (-2 * r) (r / 2) ×ˢ Metric.closedBall (0 : E) (2 * r)) = + ({-2 * r, r / 2} : Set ℝ) ×ˢ Metric.closedBall (0 : E) (2 * r) ∪ + Icc (-2 * r) (r / 2) ×ˢ Metric.sphere (0 : E) (2 * r) := + frontier_cylinder (by linarith) (by positivity) + set xt : I → ℝ := fun t => -r / 2 + (t : ℝ) * (2 * r - -r / 2) with hxt + have hxc : Continuous xt := continuous_const.add (continuous_subtype_val.mul continuous_const) + have hx0 : xt 0 = -r / 2 := by simp [hxt] + have hx1 : xt 1 = 2 * r := by simp [hxt] + have hxmem : ∀ t, xt t ∈ Icc (-r / 2) (2 * r) := by + intro t + have h0 := t.2.1 + have h1 := t.2.2 + simp only [hxt] + constructor <;> nlinarith + let γ : Path ((-r / 2 : ℝ), h (-r / 2)) (2 * r, h (2 * r)) := + { toFun := fun t => (xt t, h (xt t)) + continuous_toFun := hxc.prodMk (hh.comp_continuous hxc hxmem) + source' := by simp only [hx0] + target' := by simp only [hx1] } + refine ⟨⟨⟨by linarith, by linarith⟩, mem_closedBall_zero_iff.mpr hM⟩, ?_, ?_, ?_, ⟨γ, ?_⟩⟩ + · intro p hp + exact (hT p hp).trans (hceil p.1 hp.1) + · intro p hp + rw [hcyl] at hp + rcases hp with ⟨hp1, hp2⟩ | hp + · have hpC : p ∈ Icc (-2 * r) (r / 2) ×ˢ Metric.closedBall (0 : E) (2 * r) := by + refine ⟨?_, hp2⟩ + rcases hp1 with h1 | h1 + · rw [h1]; exact ⟨le_refl _, by linarith⟩ + · rw [h1]; exact ⟨by linarith, le_refl _⟩ + have h0 := hT p hpC + rcases hp1 with h1 | h1 + · rw [h1] at h0 + linarith + · rw [h1] at h0 + exact h0 + · exact hside p hp + · linarith + · intro t + exact hfloor (xt t) (hxmem t) + +/-- **(C2⁺) from the ridge.** If, in addition, `h x` is the unique transverse maximizer on the +cap and the curved side is strictly below `g c` (L7, L18), then `S = (r/2, h(r/2))` is the only +frontier point at height `s`. -/ +theorem ridge_saddle_strict {f : ℝ × E → ℝ} {h : ℝ → E} {F : ℝ → ℝ} {r : ℝ} (hr : 0 < r) + (hg : ∀ x ∈ Icc (-2 * r) (2 * r), HasDerivAt (fun x => f (x, h x)) (F x) x) + (hFa : F (-r / 2) = 0) (hFc : F (r / 2) = 0) + (hconv : ConvexOn ℝ (Icc (-2 * r) (2 * r)) (fun x => F x - (x + r / 2) * (x - r / 2) / 8)) + (hT : ∀ p ∈ Icc (-2 * r) (r / 2) ×ˢ Metric.closedBall (0 : E) (2 * r), f p ≤ f (p.1, h p.1)) + (hTs : ∀ p ∈ Icc (-2 * r) (r / 2) ×ˢ Metric.closedBall (0 : E) (2 * r), p.2 ≠ h p.1 → + f p < f (p.1, h p.1)) + (hside : ∀ p ∈ Icc (-2 * r) (r / 2) ×ˢ Metric.sphere (0 : E) (2 * r), + f p < f (r / 2, h (r / 2))) + (hgap : f (-r / 2, h (-r / 2)) - f (r / 2, h (r / 2)) < 9 * r ^ 3 / 32) : + ∀ x ∈ frontier (Icc (-2 * r) (r / 2) ×ˢ Metric.closedBall (0 : E) (2 * r)), + x ≠ (r / 2, h (r / 2)) → f x < f (r / 2, h (r / 2)) := by + obtain ⟨-, -, hleft, -⟩ := ridge_profile hr hg hFa hFc hconv + intro p hp hne + rw [frontier_cylinder (by linarith) (by positivity)] at hp + rcases hp with ⟨hp1, hp2⟩ | hp + · rcases hp1 with h1 | h1 + · have hpC : p ∈ Icc (-2 * r) (r / 2) ×ˢ Metric.closedBall (0 : E) (2 * r) := + ⟨by rw [h1]; exact ⟨le_refl _, by linarith⟩, hp2⟩ + have h0 := hT p hpC + rw [h1] at h0 + linarith + · have hpC : p ∈ Icc (-2 * r) (r / 2) ×ˢ Metric.closedBall (0 : E) (2 * r) := + ⟨by rw [h1]; exact ⟨by linarith, le_refl _⟩, hp2⟩ + have hy : p.2 ≠ h p.1 := by + intro hy + apply hne + rw [h1] at hy + exact Prod.ext h1 hy + have h0 := hTs p hpC hy + rw [h1] at h0 + exact h0 + · exact hside p hp + +end Ridge + +/-! ### A concrete instance and the necessity of each hypothesis + +On `ℝ`, `toyF x = max (-|x|) (x - 2)` has a local maximum `M = 0` at height `b = 0`, a +separating local minimum `S = 1` at height `s = -1`, and an older point `z = 3` at height `1`. +The cap is `[-2, 1]`. The instance shows that `CapHyp` is satisfiable (the theorems are not +vacuous), and the three counterexamples show that dropping (C1), (C2) or (C3) breaks the +maximin conclusion. -/ + +/-- The toy height function. -/ +noncomputable def toyF (x : ℝ) : ℝ := max (-|x|) (x - 2) + +/-- The toy ridge, `t ↦ 3t` from `0` to `3`. -/ +def toyRidge : Path (0 : ℝ) 3 where + toFun t := 3 * (t : ℝ) + continuous_toFun := continuous_const.mul continuous_subtype_val + source' := by simp + target' := by simp + +theorem toy_ridge_ge (t : I) : (-1 : ℝ) ≤ toyF (toyRidge t) := by + have ht0 : (0 : ℝ) ≤ t := t.2.1 + show -1 ≤ max (-|3 * (t : ℝ)|) (3 * (t : ℝ) - 2) + rcases le_or_gt (3 * (t : ℝ)) 1 with h | h + · refine le_max_of_le_left ?_ + rw [abs_of_nonneg (by linarith)] + linarith + · exact le_max_of_le_right (by linarith) + +theorem toy_frontier : frontier (Icc (-2 : ℝ) 1) = {-2, 1} := frontier_Icc (by norm_num) + +/-- The toy satisfies (C1)–(C3) with `C = [-2, 1]`, `M = 0`, `z = 3`, `b = 0`, `s = -1`. -/ +theorem toy_capHyp : CapHyp toyF (Icc (-2 : ℝ) 1) 0 3 0 (-1) where + mem := ⟨by norm_num, by norm_num⟩ + ceiling x hx := by + obtain ⟨_, hx2⟩ := hx + show max (-|x|) (x - 2) ≤ 0 + exact max_le (by linarith [abs_nonneg x]) (by linarith) + frontier_le x hx := by + rw [toy_frontier] at hx + rcases hx with rfl | rfl + · show max (-|(-2 : ℝ)|) ((-2 : ℝ) - 2) ≤ -1 + norm_num [abs_of_neg] + · show max (-|(1 : ℝ)|) ((1 : ℝ) - 2) ≤ -1 + norm_num + older := by + show (0 : ℝ) < max (-|(3 : ℝ)|) ((3 : ℝ) - 2) + norm_num + ridge := ⟨toyRidge, toy_ridge_ge⟩ + +/-- In the toy, `S = 1` is the only frontier point at height `-1` (C2⁺). -/ +theorem toy_saddle_strict : ∀ x ∈ frontier (Icc (-2 : ℝ) 1), x ≠ 1 → toyF x < -1 := by + intro x hx hne + rw [toy_frontier] at hx + rcases hx with rfl | h + · show max (-|(-2 : ℝ)|) ((-2 : ℝ) - 2) < -1 + norm_num [abs_of_neg] + · exact absurd h hne + +/-- In the toy, removing `S = 1` from `{f ≥ -1}` disconnects `M = 0` from every older point. The +cut is not vacuous: `M` lies in its own component. -/ +theorem toy_saddle_cut : + (0 : ℝ) ∈ connectedComponentIn ({x | (-1 : ℝ) ≤ toyF x} \ {1}) 0 ∧ + ∀ w ∈ connectedComponentIn ({x | (-1 : ℝ) ≤ toyF x} \ {1}) 0, toyF w ≤ 0 := + toy_capHyp.saddle_cut toy_saddle_strict (by norm_num) + +/-- The toy's elder death level is `-1`. -/ +theorem toy_death_level : IsGreatest (CapHyp.joinedLevels toyF 0 0) (-1) := + toy_capHyp.elder_death_level + +theorem toy_f_M : toyF 0 = 0 := by + show max (-|(0 : ℝ)|) ((0 : ℝ) - 2) = 0 + norm_num + +theorem toy_f_S : toyF 1 = -1 := by + show max (-|(1 : ℝ)|) ((1 : ℝ) - 2) = -1 + norm_num + +/-- Necessity of (C2). At the level `s = -3/2`, (C1) and (C3) hold, (C2) fails (the frontier point +`1` has height `-1 > -3/2`), and the maximin level is not `-3/2`. -/ +theorem toy_needs_C2 : + (∀ x ∈ Icc (-2 : ℝ) 1, toyF x ≤ 0) ∧ (0 : ℝ) < toyF 3 ∧ + (∃ γ : Path (0 : ℝ) 3, ∀ t, (-3 / 2 : ℝ) ≤ toyF (γ t)) ∧ + ¬ (∀ x ∈ frontier (Icc (-2 : ℝ) 1), toyF x ≤ -3 / 2) ∧ + ¬ IsGreatest (connectionLevels toyF 0 0) (-3 / 2) := by + refine ⟨toy_capHyp.ceiling, toy_capHyp.older, + ⟨toyRidge, fun t => le_trans (by norm_num) (toy_ridge_ge t)⟩, fun h => ?_, ?_⟩ + · have h1 := h 1 (by rw [toy_frontier]; simp) + rw [toy_f_S] at h1 + norm_num at h1 + · rintro ⟨-, hub⟩ + have hmem : (-1 : ℝ) ∈ connectionLevels toyF 0 0 := + ⟨3, toyRidge, toy_capHyp.older, toy_ridge_ge⟩ + have := hub hmem + norm_num at this + +/-- Necessity of (C1). At the ceiling `b = -1/2`, (C2) and (C3) hold, (C1) fails (`f M = 0 > -1/2`), +and the constant path at `M` shows that the maximin level is not `-1`. -/ +theorem toy_needs_C1 : + ¬ (∀ x ∈ Icc (-2 : ℝ) 1, toyF x ≤ -1 / 2) ∧ + (∀ x ∈ frontier (Icc (-2 : ℝ) 1), toyF x ≤ -1) ∧ (-1 / 2 : ℝ) < toyF 3 ∧ + (∃ γ : Path (0 : ℝ) 3, ∀ t, (-1 : ℝ) ≤ toyF (γ t)) ∧ + ¬ IsGreatest (connectionLevels toyF 0 (-1 / 2)) (-1) := by + refine ⟨fun h => ?_, toy_capHyp.frontier_le, lt_trans (by norm_num) toy_capHyp.older, + toy_capHyp.ridge, ?_⟩ + · have h1 := h 0 ⟨by norm_num, by norm_num⟩ + rw [toy_f_M] at h1 + norm_num at h1 + · rintro ⟨-, hub⟩ + have hmem : (0 : ℝ) ∈ connectionLevels toyF 0 (-1 / 2) := + ⟨0, Path.refl 0, by rw [toy_f_M]; norm_num, fun t => by simp [toy_f_M]⟩ + have := hub hmem + norm_num at this + +/-- Necessity of (C3). At the level `s = 5`, (C1) and (C2) hold and `z` is older, but no ridge stays +at height `≥ 5` (it starts at `f M = 0`), and the maximin level is not `5`: the barrier at the true +level `-1` excludes it. -/ +theorem toy_needs_C3 : + (∀ x ∈ Icc (-2 : ℝ) 1, toyF x ≤ 0) ∧ + (∀ x ∈ frontier (Icc (-2 : ℝ) 1), toyF x ≤ 5) ∧ (0 : ℝ) < toyF 3 ∧ + ¬ (∃ γ : Path (0 : ℝ) 3, ∀ t, (5 : ℝ) ≤ toyF (γ t)) ∧ + ¬ IsGreatest (connectionLevels toyF 0 0) 5 := by + refine ⟨toy_capHyp.ceiling, fun x hx => le_trans (toy_capHyp.frontier_le x hx) (by norm_num), + toy_capHyp.older, ?_, ?_⟩ + · rintro ⟨γ, hγ⟩ + have h0 := hγ 0 + rw [Path.source, toy_f_M] at h0 + norm_num at h0 + · rintro ⟨hmem, -⟩ + have h1 := toy_capHyp.maximin_isGreatest.2 hmem + norm_num at h1 + +/-- The ridge toy: SP's normalization at `r = 1` with one transverse coordinate, +`f (x, y) = x³/3 - x/4 - y²`, ridge `h = 0`, ridge derivative `F x = x² - 1/4`. -/ +noncomputable def ridgeToyF (p : ℝ × ℝ) : ℝ := p.1 ^ 3 / 3 - p.1 / 4 - p.2 ^ 2 + +/-- The ridge hypotheses of `ridge_capHyp` are jointly satisfiable. Here the gap is +`g(-1/2) - g(1/2) = 1/6`, which is SP's normalization `r³/6`. -/ +theorem ridgeToy_capHyp : + CapHyp ridgeToyF (Icc (-2 * 1) (1 / 2) ×ˢ Metric.closedBall (0 : ℝ) (2 * 1)) (-1 / 2, 0) + (2 * 1, 0) (ridgeToyF (-1 / 2, 0)) (ridgeToyF (1 / 2, 0)) := by + refine ridge_capHyp (E := ℝ) (f := ridgeToyF) (h := fun _ => (0 : ℝ)) + (F := fun x => x ^ 2 - 1 / 4) (r := 1) one_pos continuousOn_const ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ + · intro x _ + have h1 := ((hasDerivAt_pow 3 x).div_const 3).sub ((hasDerivAt_id x).div_const 4) + convert h1 using 1 + · funext y + simp only [ridgeToyF, id, Pi.sub_apply] + ring + · push_cast + ring + · norm_num + · norm_num + · have hc : ConvexOn ℝ univ (fun x : ℝ => (7 / 8 : ℝ) • x ^ 2 + (-7 / 32 : ℝ)) := + ((even_two.convexOn_pow).smul (by norm_num)).add (convexOn_const _ convex_univ) + refine (hc.subset (subset_univ _) (convex_Icc _ _)).congr ?_ + intro x _ + simp only [smul_eq_mul] + ring + · rintro ⟨x, y⟩ - + simp only [ridgeToyF] + nlinarith [sq_nonneg y] + · rintro ⟨x, y⟩ ⟨⟨hx1, hx2⟩, hy⟩ + rw [mem_sphere_zero_iff_norm, Real.norm_eq_abs] at hy + have hy2 : y ^ 2 = 4 := by rw [← sq_abs, hy]; norm_num + simp only [ridgeToyF, hy2] + nlinarith [mul_nonneg (sub_nonneg.mpr hx2) (sq_nonneg x), + mul_nonneg (by linarith : (0 : ℝ) ≤ x + 2) (by linarith : (0 : ℝ) ≤ 2 - x)] + · simp + · simp only [ridgeToyF] + norm_num + +/-- In the ridge toy, `S = (1/2, 0)` is the only frontier point at height `s` (C2⁺). -/ +theorem ridgeToy_saddle_strict : + ∀ x ∈ frontier (Icc (-2 * 1) (1 / 2) ×ˢ Metric.closedBall (0 : ℝ) (2 * 1)), + x ≠ (1 / 2, 0) → ridgeToyF x < ridgeToyF (1 / 2, 0) := by + refine ridge_saddle_strict (E := ℝ) (f := ridgeToyF) (h := fun _ => (0 : ℝ)) + (F := fun x => x ^ 2 - 1 / 4) (r := 1) one_pos ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_ + · intro x _ + have h1 := ((hasDerivAt_pow 3 x).div_const 3).sub ((hasDerivAt_id x).div_const 4) + convert h1 using 1 + · funext y + simp only [ridgeToyF, id, Pi.sub_apply] + ring + · push_cast + ring + · norm_num + · norm_num + · have hc : ConvexOn ℝ univ (fun x : ℝ => (7 / 8 : ℝ) • x ^ 2 + (-7 / 32 : ℝ)) := + ((even_two.convexOn_pow).smul (by norm_num)).add (convexOn_const _ convex_univ) + refine (hc.subset (subset_univ _) (convex_Icc _ _)).congr ?_ + intro x _ + simp only [smul_eq_mul] + ring + · rintro ⟨x, y⟩ - + simp only [ridgeToyF] + nlinarith [sq_nonneg y] + · rintro ⟨x, y⟩ - hy + have hy' : y ≠ 0 := hy + simp only [ridgeToyF] + nlinarith [sq_pos_of_ne_zero hy'] + · rintro ⟨x, y⟩ ⟨⟨hx1, hx2⟩, hy⟩ + rw [mem_sphere_zero_iff_norm, Real.norm_eq_abs] at hy + have hy2 : y ^ 2 = 4 := by rw [← sq_abs, hy]; norm_num + simp only [ridgeToyF, hy2] + nlinarith [mul_nonneg (sub_nonneg.mpr hx2) (sq_nonneg x), + mul_nonneg (by linarith : (0 : ℝ) ≤ x + 2) (by linarith : (0 : ℝ) ≤ 2 - x)] + · simp only [ridgeToyF] + norm_num + +end CapFirstExit diff --git a/frontiers/cap_first_exit_lean_20261002/MANIFEST.json b/frontiers/cap_first_exit_lean_20261002/MANIFEST.json new file mode 100644 index 000000000..f978bfee1 --- /dev/null +++ b/frontiers/cap_first_exit_lean_20261002/MANIFEST.json @@ -0,0 +1,404 @@ +{ + "object": "CAP-FIRST-EXIT-LEAN-20261002-v1", + "scientific_effect": "NONE", + "mathematical_acceptance": false, + "alignment_review": "NOT_CLAIMED", + "module": "CapFirstExit", + "toolchain": "leanprover/lean4:v4.34.1", + "mathlib_rev": "d13f23b723b8a846827a245b89c10fc7d3f11612", + "dependency_revisions": { + "plausible": "118aa17ee84656b8bd727fef7c458ee8c833385c", + "LeanSearchClient": "ddf04cf3949fa556442341e87d47f9f6e6074707", + "importGraph": "e928b72544873815af278d38681b31c0293588e3", + "proofwidgets": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5", + "aesop": "355695d523e41d0554926416cba2a2b3544fbbc9", + "Qq": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259", + "batteries": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2", + "Cli": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204", + "mathlib": "d13f23b723b8a846827a245b89c10fc7d3f11612" + }, + "pins_on_main": [ + { + "path": "reviews/d1_cap_elder_partner_second_pass_claude_20260930/REVIEW.md", + "git_blob": "a653dbc7bd8bd692433587f050ab8678713c297e" + }, + { + "path": "imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md", + "git_blob": "0633aca3c2a2882b0de4399da0a75d64c2e6b2e1" + } + ], + "allowed_axioms": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "targets": [ + "CapFirstExit.path_meets_frontier", + "CapFirstExit.preconnected_subset_of_frontier_disjoint", + "CapFirstExit.CapHyp", + "CapFirstExit.CapHyp.s_le_f_M", + "CapFirstExit.CapHyp.barrier", + "CapFirstExit.connectionLevels", + "CapFirstExit.CapHyp.maximin_isGreatest", + "CapFirstExit.CapHyp.maximin_eq", + "CapFirstExit.CapHyp.component_separated", + "CapFirstExit.component_joined", + "CapFirstExit.CapHyp.elder_merge_iff_closed", + "CapFirstExit.CapHyp.elder_merge_iff_open", + "CapFirstExit.CapHyp.joinedLevels", + "CapFirstExit.CapHyp.elder_death_level", + "CapFirstExit.CapHyp.path_through_saddle", + "CapFirstExit.CapHyp.saddle_cut", + "CapFirstExit.CapHyp.congr", + "CapFirstExit.isClosed_connectedComponentIn", + "CapFirstExit.CapHyp.older_peak", + "CapFirstExit.CapHyp.elder_alive", + "CapFirstExit.CapHyp.olderPeakLevels", + "CapFirstExit.CapHyp.elder_death_level_peak", + "CapFirstExit.frontier_image_subset", + "CapFirstExit.CapHyp.map", + "CapFirstExit.CapHyp.map_saddle", + "CapFirstExit.frontier_cylinder", + "CapFirstExit.isCompact_cylinder", + "CapFirstExit.torusCover", + "CapFirstExit.torusCover_continuous", + "CapFirstExit.torusCover_isOpenMap", + "CapFirstExit.CapHyp.toTorus", + "CapFirstExit.convex_zeros_between", + "CapFirstExit.convex_zeros_right", + "CapFirstExit.convex_zeros_left", + "CapFirstExit.ridge_profile", + "CapFirstExit.ridge_capHyp", + "CapFirstExit.ridge_saddle_strict", + "CapFirstExit.toyF", + "CapFirstExit.toyRidge", + "CapFirstExit.toy_ridge_ge", + "CapFirstExit.toy_frontier", + "CapFirstExit.toy_capHyp", + "CapFirstExit.toy_saddle_strict", + "CapFirstExit.toy_saddle_cut", + "CapFirstExit.toy_death_level", + "CapFirstExit.toy_f_M", + "CapFirstExit.toy_f_S", + "CapFirstExit.toy_needs_C2", + "CapFirstExit.toy_needs_C1", + "CapFirstExit.toy_needs_C3", + "CapFirstExit.ridgeToyF", + "CapFirstExit.ridgeToy_capHyp", + "CapFirstExit.ridgeToy_saddle_strict" + ], + "expected_axioms": { + "CapFirstExit.path_meets_frontier": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.preconnected_subset_of_frontier_disjoint": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.CapHyp": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.CapHyp.s_le_f_M": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.CapHyp.barrier": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.connectionLevels": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.CapHyp.maximin_isGreatest": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.CapHyp.maximin_eq": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.CapHyp.component_separated": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.component_joined": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.CapHyp.elder_merge_iff_closed": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.CapHyp.elder_merge_iff_open": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.CapHyp.joinedLevels": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.CapHyp.elder_death_level": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.CapHyp.path_through_saddle": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.CapHyp.saddle_cut": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.CapHyp.congr": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.isClosed_connectedComponentIn": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.CapHyp.older_peak": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.CapHyp.elder_alive": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.CapHyp.olderPeakLevels": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.CapHyp.elder_death_level_peak": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.frontier_image_subset": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.CapHyp.map": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.CapHyp.map_saddle": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.frontier_cylinder": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.isCompact_cylinder": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.torusCover": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.torusCover_continuous": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.torusCover_isOpenMap": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.CapHyp.toTorus": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.convex_zeros_between": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.convex_zeros_right": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.convex_zeros_left": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.ridge_profile": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.ridge_capHyp": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.ridge_saddle_strict": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.toyF": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.toyRidge": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.toy_ridge_ge": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.toy_frontier": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.toy_capHyp": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.toy_saddle_strict": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.toy_saddle_cut": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.toy_death_level": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.toy_f_M": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.toy_f_S": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.toy_needs_C2": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.toy_needs_C1": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.toy_needs_C3": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.ridgeToyF": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.ridgeToy_capHyp": [ + "Classical.choice", + "Quot.sound", + "propext" + ], + "CapFirstExit.ridgeToy_saddle_strict": [ + "Classical.choice", + "Quot.sound", + "propext" + ] + }, + "files": [ + { + "path": ".gitignore", + "bytes": 20, + "sha256": "b34af236d1df9e39ed4f98fca51702530ce76bdee4e1a69512f6caed933c3374" + }, + { + "path": "ALIGNMENT.md", + "bytes": 11887, + "sha256": "c55a89e0c5134f78d0051bda0f221a0f50f2802a72def8b2d37dc41d362821a8" + }, + { + "path": "CapFirstExit.lean", + "bytes": 42711, + "sha256": "2fe8943b74c6aa66a46b7b1db6fe5332f82dff2ee01ff27731188404ddad4ebd" + }, + { + "path": "README.md", + "bytes": 9402, + "sha256": "5256f80e0e500f61098bac8cdd9e0a349573bf212ca5bcbf41af6566bf10c7f7" + }, + { + "path": "gate.py", + "bytes": 12390, + "sha256": "eaceb18e3ad096a0b1fab332dc095b78221867d79f9ba0e120b2c2e4812c7395" + }, + { + "path": "lake-manifest.json", + "bytes": 3547, + "sha256": "04549ed79e36b417686b94d91994aad4dad7bb78d896bd2e74099ff95265935b" + }, + { + "path": "lakefile.toml", + "bytes": 252, + "sha256": "3fa8afe35db80e433b9ff59fab399df0b44ade73aeda1452b884a24ed1b01a52" + }, + { + "path": "lean-toolchain", + "bytes": 25, + "sha256": "d5edba4e4b8faad9c1baeadb265716d20d03be4d1a2647dc5e35b0c0325bea7b" + }, + { + "path": "test_gate.py", + "bytes": 6274, + "sha256": "f7df7152065d3fb69aed839138575b0cca3f821d958f5849f617e69e390bc6b3" + } + ] +} diff --git a/frontiers/cap_first_exit_lean_20261002/README.md b/frontiers/cap_first_exit_lean_20261002/README.md new file mode 100644 index 000000000..204cdc148 --- /dev/null +++ b/frontiers/cap_first_exit_lean_20261002/README.md @@ -0,0 +1,122 @@ +# Cap first exit in Lean: the topological global step of D1 component III + +**Object:** `CAP-FIRST-EXIT-LEAN-20261002-v1`. **Author:** Anthropic / Claude, Claude Code session `017Mi3hx…`. +**Kind:** a Lean 4 / Mathlib formalization, with its own source and execution gate. **Scientific effect:** NONE. No +register, catalog, STATUS, PROOF_INDEX, GRAPH or `formal/` scope change. **Same GitHub account as every lane: zero +organizational-independence credit.** The author will not merge. + +## What is proved + +The audit of D1 named one step as load-bearing: the deterministic implication from the local good event to "`S` is +the *global* elder partner of `M`". It asked for that step to have a completely independent derivation. + +That implication has two parts: + +- **Analytic part (CAP §§2–5, second pass L1–L20).** From `G_r`, construct a cap `C` and a ridge with three + properties: + - (C1) `f ≤ b` on `C`; + - (C2) `f ≤ s` on the frontier of `C`, with only `S` attaining `s` (C2⁺); + - (C3) a path from `M` to an older point `z`, `f(z) > b`, along which `f ≥ s`. +- **Topological part (L21–L22).** From (C1)–(C3), deduce `M`'s global maximin level and its superlevel death level. + +This packet kernel-checks two things: +- the whole topological part; +- the one-variable and assembly steps of the analytic part (L13, L16, L17, L19, L20, in `ridge_capHyp`). + +The multi-variable estimates L1–L12 and L18 remain hypotheses. + +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. + +| Lean declaration | Statement | +|---|---| +| `CapHyp f C M z b s` | (C1)–(C3) as one `Prop` structure | +| `CapHyp.maximin_isGreatest`, `maximin_eq` | `d_f(M) = sup_γ inf_t f(γ t) = s`, attained (L21) | +| `CapHyp.elder_merge_iff_closed` | for every `h`: the component of `M` in `{f ≥ h}` contains a point `> b` **iff** `h ≤ s` | +| `CapHyp.elder_merge_iff_open` | for every `h`: the component of `M` in `{f > h}` contains a point `> b` **iff** `h < s` | +| `CapHyp.elder_death_level` | the largest such `h` exists and equals `s` (L22's death level) | +| `CapHyp.path_through_saddle` | under (C2⁺): every path from `M` to a point `> b` inside `{f ≥ s}` passes through `S` | +| `CapHyp.saddle_cut`, `toy_saddle_cut` | under (C2⁺) and `M ≠ S`: `M` lies in its own component of `{f ≥ s} \ {S}`, so the statement is not vacuous, and that component has no point `> b`. `S` is a cut point at the death level. The toy shows this on concrete data | +| `CapHyp.older_peak` | on a compact, locally connected space with continuous `f`: for every `h ≤ s`, `M`'s component in `{f ≥ h}` contains a local maximum `p` of `f` with `f p > b` that is highest in the component (the older class) | +| `CapHyp.elder_alive` | with `b = f M`: for every `h > s`, `M` is a highest point of its component in `{f ≥ h}` | +| `CapHyp.elder_death_level_peak` | compact, locally connected, continuous, `b = f M`: the largest level at which `M`'s component contains a strictly higher local maximum exists and is `s` | +| `CapHyp.congr` | exterior invariance: agreement on `closure C` and along one ridge preserves every hypothesis, hence every conclusion | +| `CapHyp.map`, `CapHyp.map_saddle` | transport: if the lift `f ∘ e` satisfies (C1)–(C3) (and (C2⁺)) on a compact cap `C`, then `f` satisfies them on `e '' C`. Needs only `e` continuous and open and the target Hausdorff; no injectivity | +| `torusCover`, `CapHyp.toTorus` | the covering map `ℝ^d → (ℝ/Lℤ)^d` is continuous and open, so a cap verified for the periodic lift in any coordinate frame transfers to the torus with the same `b`, `s`. No embedding radius is needed for this step | +| `frontier_cylinder`, `isCompact_cylinder` | `frontier ([a, c] × B̄(0, R)) = {a, c} × B̄(0, R) ∪ [a, c] × S(0, R)`: exactly the end faces and curved side estimated in L17–L19; the cylinder is compact | +| `ridge_profile` | L13, L16, L17 and L20 in one variable. Assume, on `[−2r, 2r]`, that `g' = F`, `F(∓r/2) = 0` and `F − (x + r/2)(x − r/2)/8` is convex. Then `g ≤ g(−r/2)` on `[−2r, r/2]` and `g ≥ g(r/2)` on `[−r/2, 2r]`. Also `g(−2r) ≤ g(−r/2) − 9r³/32` and `g(2r) ≥ g(r/2) + 9r³/32`: the exact face integrals | +| `ridge_capHyp`, `ridge_saddle_strict` | (C1)–(C3), and (C2⁺), on the cylinder `[−2r, r/2] × B̄(0, 2r)`, derived from the multi-variable outputs, each assumed only where SP supplies it: L7 (transverse maximum, unique for (C2⁺)), L11 (`g' = F` on `[−2r, 2r]`), L12 (`F'' ≥ 1/4` as convexity on `[−2r, 2r]`), L18 (curved side), and the gap `b − s < 9r³/32` | +| `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 | +| `toy_capHyp`, `toy_death_level` | a concrete instance on `ℝ`, showing the hypotheses are satisfiable and the theorems are not vacuous | +| `toy_needs_C1`, `toy_needs_C2`, `toy_needs_C3` | proved counterexamples: for each of (C1), (C2), (C3), Lean proves that the other two hold, that this one fails, and that the maximin conclusion fails | + +The two engines of the proof are: + +- `path_meets_frontier`: a path that leaves `C` meets `frontier C`. +- `preconnected_subset_of_frontier_disjoint`: a preconnected set that meets `C` and avoids `frontier C` lies inside + `C`. + +The second is what lets the component statements avoid path-connectedness and continuity of `f`. + +`saddle_cut` gives a topological reason why the death happens at `S`. The source instead identifies `S` through a +Morse-theoretic step: distinct critical values make the merging critical point unique. `saddle_cut` does not need +that step. + +## What is not proved here + +This packet does not formalize: + +- the multi-variable analytic steps L1–L12 and L18: the Hermite identity, increments, strong concavity and the + transverse maximizer, the implicit function theorem, the ridge identity, the `F''` bound, and the curved side. These + enter `ridge_capHyp` as hypotheses, and L13, L16, L17, L19 and L20 are proved from them; +- 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`); +- 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 + informal; +- L23, P §8, and every probabilistic statement (Theorem A, `Q^W(G_r^c) ≤ C r^3`). + +So issue Math-#193's "D1 Lean / kernel formalization" remains **partially** unsupplied. [ALIGNMENT.md](ALIGNMENT.md) +maps every Lean statement to its source line and lists these interfaces. + +## Running it + +The package pins the same toolchain and Mathlib revision as `formal/`: Lean `v4.34.1`, Mathlib `d13f23b7`. It has its +own `lakefile.toml` and `lake-manifest.json`, and it neither imports nor alters `formal/`. + + python3 frontiers/cap_first_exit_lean_20261002/gate.py # source gate (no Lean needed) + python3 -m unittest discover -s frontiers/cap_first_exit_lean_20261002 -p 'test_*.py' -v + cd frontiers/cap_first_exit_lean_20261002 && lake exe cache get && cd - + python3 frontiers/cap_first_exit_lean_20261002/gate.py --execute # build, replay, axioms, controls + +The source gate checks: + +- every file against `MANIFEST.json` (bytes and SHA-256), and the exact tree; +- the two pinned sources on main, by git blob; +- toolchain and dependency pins; +- that the only import is `Mathlib`; +- that no forbidden token (`sorry`, `axiom`, `native_decide`, `set_option`, …) appears outside comments; +- that the declared targets equal the manifest list. + +`--execute` additionally: + +- fails unless the running Lean is exactly the pinned release, and unless every dependency worktree is at its pinned + revision with no staged, unstaged or untracked changes (checked before the build and again when the receipt is + bound); +- rebuilds the package fresh; +- replays the module with `leanchecker`; +- prints the axioms of all 52 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. + +The workflow `.github/workflows/cap-first-exit-lean.yml` runs all of this on pull requests that touch the packet. + +A green run is kernel evidence for the displayed Lean statements, relative to Lean's kernel and the pinned toolchain. +It does not show that the statements say what the source says. That is the job of the alignment review requested +in [ALIGNMENT.md](ALIGNMENT.md), which must come from a non-Claude lane. diff --git a/frontiers/cap_first_exit_lean_20261002/gate.py b/frontiers/cap_first_exit_lean_20261002/gate.py new file mode 100644 index 000000000..9f6706bea --- /dev/null +++ b/frontiers/cap_first_exit_lean_20261002/gate.py @@ -0,0 +1,268 @@ +#!/usr/bin/env python3 +"""Source and execution gate for the CapFirstExit Lean packet. Standard library only. + + python3 gate.py source identity, main pins, toolchain pins, forbidden tokens, + declared targets + python3 gate.py --execute the same, then a fresh `lake build`, a `leanchecker` replay, the + per-declaration axiom audit against MANIFEST.json, and three + negative controls (injected sorry, custom axiom, native_decide) + that the audit must reject + +Scientific effect: NONE. A green gate is kernel evidence for the displayed Lean statements only. +It is not an alignment review and not an acceptance of any parent theorem. +""" +import argparse +import hashlib +import json +import pathlib +import re +import shutil +import subprocess +import sys + +ROOT = pathlib.Path(__file__).resolve().parent +REPO = ROOT.parents[1] +MODULE = 'CapFirstExit' +NAME = r"[A-Za-z_][A-Za-z0-9_'.₀-₉]*" +AXIOM_LINE = re.compile(r"'(" + NAME + r")' (?:depends on axioms: \[([^\]]*)\]|does not depend on any axioms)") +DECL = re.compile(r'^(?:noncomputable )?(theorem|def|structure) (' + NAME + r')') +FORBIDDEN = ('sorry', 'admit', 'axiom', 'native_decide', 'implemented_by', 'extern', 'unsafe', + 'opaque', 'set_option', 'macro', 'elab', 'syntax', 'run_cmd', 'run_tac', 'decreasing_by', + 'partial', 'debug', 'ofReduceBool', 'trustCompiler') +SKIP_DIRS = {'.lake', '__pycache__'} + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def git_blob(data): + return hashlib.sha1(b'blob %d\0' % len(data) + data).hexdigest() + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def load_json(text): + def unique(pairs): + keys = [k for k, _ in pairs] + require(len(keys) == len(set(keys)), 'duplicate JSON key') + return dict(pairs) + return json.loads(text, object_pairs_hook=unique) + + +def strip_comments(text): + """Remove Lean block comments (nested) and line comments; strings are not used in the source.""" + out, depth, i = [], 0, 0 + while i < len(text): + if text.startswith('/-', i): + depth += 1 + i += 2 + elif depth and text.startswith('-/', i): + depth -= 1 + i += 2 + elif depth: + i += 1 + elif text.startswith('--', i): + j = text.find('\n', i) + i = len(text) if j < 0 else j + else: + out.append(text[i]) + i += 1 + require(depth == 0, 'unterminated block comment') + return ''.join(out) + + +def forbidden_tokens(text): + code = strip_comments(text) + words = set(re.findall(r'[A-Za-z_][A-Za-z0-9_]*', code)) + return sorted(set(FORBIDDEN) & words) + + +def declarations(text): + """Fully qualified names of top-level theorem/def/structure declarations. + + Namespaces prefix names; named sections only scope variables and must close like namespaces.""" + stack, names = [], [] + for line in strip_comments(text).splitlines(): + m = re.match(r'^(namespace|section) (' + NAME + r')\s*$', line) + if m: + stack.append((m.group(1), m.group(2))) + continue + m = re.match(r'^end (' + NAME + r')\s*$', line) + if m: + require(stack and stack[-1][1] == m.group(1), 'unbalanced namespace or section: ' + m.group(1)) + stack.pop() + continue + require(re.match(r'^(section|end)\s*$', line) is None, 'anonymous section or end is not supported') + m = DECL.match(line) + if m: + names.append('.'.join([n for k, n in stack if k == 'namespace'] + [m.group(2)])) + require(not stack, 'unclosed namespace or section') + return names + + +def audit_axioms(text, targets, allowed): + records = {} + for name, raw in AXIOM_LINE.findall(text): + require(name in targets and name not in records, 'unexpected or duplicate axiom report: ' + name) + axioms = [] if not raw.strip() else [a.strip() for a in raw.split(',')] + require(all(re.fullmatch(NAME, a) for a in axioms), 'malformed axiom name') + require(set(axioms) <= set(allowed), 'forbidden transitive axiom: ' + repr(sorted(set(axioms) - set(allowed)))) + records[name] = sorted(set(axioms)) + require(set(records) == set(targets), 'missing axiom report: ' + repr(sorted(set(targets) - set(records)))) + return records + + +def source_check(root=ROOT, repo=REPO): + m = load_json((root / 'MANIFEST.json').read_text()) + present = sorted(p.relative_to(root).as_posix() for p in root.rglob('*') + if p.is_file() and not SKIP_DIRS & set(p.relative_to(root).parts)) + expected = sorted([e['path'] for e in m['files']] + ['MANIFEST.json']) + require(present == expected, 'packet tree differs from manifest: ' + repr(present)) + for e in m['files']: + p = root / e['path'] + require(not p.is_symlink() and '/' not in e['path'], 'flat regular file required: ' + e['path']) + data = p.read_bytes() + require(len(data) == e['bytes'] and sha(data) == e['sha256'], 'source identity mismatch: ' + e['path']) + for pin in m['pins_on_main']: + p = repo / pin['path'] + require(p.is_file() and not p.is_symlink(), 'pinned source missing: ' + pin['path']) + require(git_blob(p.read_bytes()) == pin['git_blob'], 'pinned source drifted: ' + pin['path']) + require((root / 'lean-toolchain').read_text().strip() == m['toolchain'], 'toolchain pin mismatch') + lakefile = (root / 'lakefile.toml').read_text() + require(re.search(r'^rev = "' + m['mathlib_rev'] + r'"$', lakefile, re.M) is not None, 'lakefile Mathlib rev mismatch') + lock = load_json((root / 'lake-manifest.json').read_text()) + revs = {pkg['name']: pkg['rev'] for pkg in lock['packages']} + require(revs.get('mathlib') == m['mathlib_rev'], 'lake-manifest Mathlib rev mismatch') + require(revs == m['dependency_revisions'], 'dependency revisions differ from MANIFEST.json') + lean_files = sorted(p.relative_to(root).as_posix() for p in root.rglob('*.lean') + if not SKIP_DIRS & set(p.relative_to(root).parts)) + require(lean_files == [MODULE + '.lean'], 'unexpected Lean files: ' + repr(lean_files)) + text = (root / (MODULE + '.lean')).read_text() + code = strip_comments(text) + imports = re.findall(r'^import\s+(\S+)', code, re.M) + require(imports == ['Mathlib'], 'imports must be exactly Mathlib: ' + repr(imports)) + bad = forbidden_tokens(text) + require(not bad, 'forbidden tokens in Lean source: ' + repr(bad)) + decls = declarations(text) + require(len(decls) == len(set(decls)), 'duplicate declaration names') + require(decls == m['targets'], 'declared targets differ from MANIFEST.json') + require(sorted(m['expected_axioms']) == sorted(m['targets']), 'expected_axioms must cover exactly the targets') + require(set(m['allowed_axioms']) == {'propext', 'Classical.choice', 'Quot.sound'}, 'allowed axiom set changed') + return m + + +def pinned_lean_version(toolchain): + m = re.fullmatch(r'leanprover/lean4:v(\d+\.\d+\.\d+)', toolchain) + require(m is not None, 'unrecognized toolchain pin: ' + toolchain) + return m.group(1) + + +def check_lean_version(text, toolchain): + """The running Lean must be exactly the pinned release, not merely a compatible one.""" + version = pinned_lean_version(toolchain) + require(re.match(r'Lean \(version ' + re.escape(version) + r',', text.strip()) is not None, + 'running Lean differs from the pinned ' + version + ': ' + text.strip()[:120]) + return text.strip() + + +def check_worktree_clean(name, status): + """`git status --porcelain` output of a dependency: staged, unstaged or untracked changes fail.""" + require(status.strip() == '', 'dependency worktree is not clean: ' + name + ': ' + status.strip()[:200]) + + +def dependency_state(m): + """Exact pinned revision and a clean worktree for every dependency, read from the checkouts.""" + actual = {} + for name in m['dependency_revisions']: + repo = str(ROOT / '.lake' / 'packages' / name) + actual[name] = subprocess.check_output(['git', '-C', repo, 'rev-parse', 'HEAD'], text=True).strip() + check_worktree_clean(name, subprocess.check_output( + ['git', '-C', repo, 'status', '--porcelain', '--untracked-files=normal'], text=True)) + require(actual == m['dependency_revisions'], 'checked-out dependency revisions differ from MANIFEST.json') + return actual + + +def run(command, label, out, expect_success=True): + proc = subprocess.run(command, cwd=ROOT, text=True, capture_output=True, timeout=1800) + log = proc.stdout + proc.stderr + (out / (label + '.log')).write_text(log) + if expect_success: + require(proc.returncode == 0, label + ' failed:\n' + log[-4000:]) + return log + + +def execute(m): + out = ROOT / '.lake' / 'evidence' + if out.exists(): + shutil.rmtree(out) + out.mkdir(parents=True) + version = check_lean_version(run(['lake', 'env', 'lean', '--version'], 'version', out), m['toolchain']) + dependency_state(m) + build = ROOT / '.lake' / 'build' + require(not build.is_symlink(), 'symlink build directory') + if build.exists(): + shutil.rmtree(build) # fresh build of this package; the Mathlib cache is untouched + log = run(['lake', 'build'], 'build', out) + require('error' not in log.lower(), 'build log reports an error') + require('declaration uses' not in log, 'build log reports sorry or a similar escape') + run(['lake', 'env', 'leanchecker', MODULE], 'leanchecker', out) + audit = out / 'Axioms.lean' + audit.write_text('import ' + MODULE + '\n' + ''.join('#print axioms ' + n + '\n' for n in m['targets'])) + axioms = audit_axioms(run(['lake', 'env', 'lean', str(audit)], 'axioms', out), m['targets'], m['allowed_axioms']) + require(axioms == {k: sorted(v) for k, v in m['expected_axioms'].items()}, 'axiom report differs from MANIFEST.json') + controls = { + 'sorry': 'theorem injected : False := by sorry\n', + 'custom_axiom': 'axiom hiddenPremise : False\ntheorem injected : False := hiddenPremise\n', + 'native_decide': 'theorem injected : (2 : Nat) + 2 = 4 := by native_decide\n'} + outcomes = {} + for label, body in controls.items(): + path = out / ('Control_' + label + '.lean') + path.write_text('import ' + MODULE + '\n' + body + '#print axioms injected\n') + clog = run(['lake', 'env', 'lean', str(path)], 'control_' + label, out, expect_success=False) + try: + audit_axioms(clog, ['injected'], m['allowed_axioms']) + except ValueError as exc: + require('forbidden transitive axiom' in str(exc), 'control ' + label + ' failed for the wrong reason: ' + str(exc)) + outcomes[label] = 'REJECTED' + continue + raise ValueError('negative control escaped the audit: ' + label) + actual = dependency_state(m) + receipt = { + 'scientific_effect': 'NONE', + 'module': MODULE, + 'lean_version': version, + 'toolchain': m['toolchain'], + 'dependency_revisions': actual, + 'source_sha256': {e['path']: e['sha256'] for e in m['files']}, + 'build': 'PASS', 'leanchecker': 'PASS', 'dependency_worktrees': 'CLEAN', + 'axioms': axioms, + 'negative_controls': outcomes, + 'alignment_review': 'NOT_CLAIMED'} + text = json.dumps(receipt, indent=2, sort_keys=True) + '\n' + (out / 'receipt.json').write_text(text) + return receipt + + +def main(): + p = argparse.ArgumentParser(description=__doc__.splitlines()[0]) + p.add_argument('--execute', action='store_true', help='build, replay, audit axioms and run negative controls') + args = p.parse_args() + m = source_check() + if args.execute: + receipt = execute(m) + print(json.dumps({'passed': True, 'axioms_allowed_only': True, + 'negative_controls': receipt['negative_controls'], 'targets': len(m['targets'])}, sort_keys=True)) + else: + print(json.dumps({'passed': True, 'source_check': 'PASS', 'targets': len(m['targets'])}, sort_keys=True)) + + +if __name__ == '__main__': + try: + main() + except (ValueError, KeyError, subprocess.CalledProcessError) as exc: + print('GATE FAILURE: ' + str(exc), file=sys.stderr) + sys.exit(1) diff --git a/frontiers/cap_first_exit_lean_20261002/lake-manifest.json b/frontiers/cap_first_exit_lean_20261002/lake-manifest.json new file mode 100644 index 000000000..292d7c116 --- /dev/null +++ b/frontiers/cap_first_exit_lean_20261002/lake-manifest.json @@ -0,0 +1,117 @@ +{ + "version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [ + { + "name": "plausible", + "url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "118aa17ee84656b8bd727fef7c458ee8c833385c", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "name": "LeanSearchClient", + "url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "ddf04cf3949fa556442341e87d47f9f6e6074707", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "name": "importGraph", + "url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "e928b72544873815af278d38681b31c0293588e3", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "name": "proofwidgets", + "url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "name": "aesop", + "url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "355695d523e41d0554926416cba2a2b3544fbbc9", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "name": "Qq", + "url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "name": "batteries", + "url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "name": "Cli", + "url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.34.0", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "name": "mathlib", + "url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "d13f23b723b8a846827a245b89c10fc7d3f11612", + "manifestFile": "lake-manifest.json", + "inputRev": "d13f23b723b8a846827a245b89c10fc7d3f11612", + "inherited": false, + "configFile": "lakefile.lean" + } + ], + "name": "cap_first_exit", + "lakeDir": ".lake", + "fixedToolchain": true +} diff --git a/frontiers/cap_first_exit_lean_20261002/lakefile.toml b/frontiers/cap_first_exit_lean_20261002/lakefile.toml new file mode 100644 index 000000000..8b02204e2 --- /dev/null +++ b/frontiers/cap_first_exit_lean_20261002/lakefile.toml @@ -0,0 +1,11 @@ +name = "cap_first_exit" +version = "0.1.0" +defaultTargets = ["CapFirstExit"] + +[[require]] +name = "mathlib" +git = "https://github.com/leanprover-community/mathlib4.git" +rev = "d13f23b723b8a846827a245b89c10fc7d3f11612" + +[[lean_lib]] +name = "CapFirstExit" diff --git a/frontiers/cap_first_exit_lean_20261002/lean-toolchain b/frontiers/cap_first_exit_lean_20261002/lean-toolchain new file mode 100644 index 000000000..ba8ebf2db --- /dev/null +++ b/frontiers/cap_first_exit_lean_20261002/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.34.1 diff --git a/frontiers/cap_first_exit_lean_20261002/test_gate.py b/frontiers/cap_first_exit_lean_20261002/test_gate.py new file mode 100644 index 000000000..61ca37bc1 --- /dev/null +++ b/frontiers/cap_first_exit_lean_20261002/test_gate.py @@ -0,0 +1,147 @@ +"""Unit tests for gate.py (standard library only; no Lean needed).""" +import json +import pathlib +import shutil +import sys +import tempfile +import unittest + +HERE = pathlib.Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import gate # noqa: E402 + +ALLOWED = ['propext', 'Classical.choice', 'Quot.sound'] + + +class SourceGate(unittest.TestCase): + def test_tree_passes(self): + m = gate.source_check() + self.assertEqual(len(m["targets"]), 53) + self.assertEqual(m['scientific_effect'], 'NONE') + + def copy(self): + tmp = pathlib.Path(tempfile.mkdtemp()) + self.addCleanup(shutil.rmtree, tmp) + repo = tmp / 'repo' + packet = repo / 'frontiers' / HERE.name + packet.mkdir(parents=True) + for p in HERE.iterdir(): + if p.is_file(): + shutil.copy2(p, packet / p.name) + m = json.loads((HERE / 'MANIFEST.json').read_text()) + for pin in m['pins_on_main']: + dst = repo / pin['path'] + dst.parent.mkdir(parents=True, exist_ok=True) + shutil.copy2(gate.REPO / pin['path'], dst) + return repo, packet + + def assertGateFails(self, repo, packet, fragment): + with self.assertRaises(ValueError) as ctx: + gate.source_check(packet, repo) + self.assertIn(fragment, str(ctx.exception)) + + def test_copy_passes(self): + repo, packet = self.copy() + gate.source_check(packet, repo) + + def test_modified_lean_rejected(self): + repo, packet = self.copy() + p = packet / 'CapFirstExit.lean' + p.write_text(p.read_text().replace('h ≤ s := by', 'h < s := by', 1)) + self.assertGateFails(repo, packet, 'source identity mismatch') + + def test_extra_file_rejected(self): + repo, packet = self.copy() + (packet / 'Extra.lean').write_text('import Mathlib\n') + self.assertGateFails(repo, packet, 'packet tree differs') + + def test_pin_drift_rejected(self): + repo, packet = self.copy() + m = json.loads((HERE / 'MANIFEST.json').read_text()) + p = repo / m['pins_on_main'][0]['path'] + p.write_bytes(p.read_bytes() + b'\n') + self.assertGateFails(repo, packet, 'pinned source drifted') + + +class Tokens(unittest.TestCase): + def test_comments_ignored(self): + self.assertEqual(gate.forbidden_tokens('/- sorry -/\n-- axiom\ntheorem t : True := trivial\n'), []) + + def test_nested_comment(self): + self.assertEqual(gate.forbidden_tokens('/- a /- sorry -/ b -/\ntheorem t : True := trivial\n'), []) + + def test_code_detected(self): + self.assertEqual(gate.forbidden_tokens('theorem t : False := by sorry\n'), ['sorry']) + self.assertEqual(gate.forbidden_tokens('set_option maxHeartbeats 0\n'), ['set_option']) + self.assertEqual(gate.forbidden_tokens('axiom p : False\n'), ['axiom']) + self.assertEqual(gate.forbidden_tokens('/- x -/ example : 1 = 1 := by native_decide\n'), ['native_decide']) + + def test_unterminated_comment(self): + with self.assertRaises(ValueError): + gate.forbidden_tokens('/- open\n') + + +class Declarations(unittest.TestCase): + def test_namespaces(self): + text = ('namespace A\ntheorem x : True := trivial\nnamespace B\nnoncomputable def y : Nat := 0\n' + 'end B\nstructure Z : Prop where\n p : True\nend A\n') + self.assertEqual(gate.declarations(text), ['A.x', 'A.B.y', 'A.Z']) + + def test_sections_do_not_prefix(self): + text = ('namespace A\nsection S\ntheorem x : True := trivial\nend S\n' + 'theorem y : True := trivial\nend A\n') + self.assertEqual(gate.declarations(text), ['A.x', 'A.y']) + + def test_anonymous_section_rejected(self): + with self.assertRaises(ValueError): + gate.declarations('section\ntheorem x : True := trivial\nend\n') + + def test_unbalanced(self): + with self.assertRaises(ValueError): + gate.declarations('namespace A\nend B\n') + with self.assertRaises(ValueError): + gate.declarations('namespace A\ntheorem x : True := trivial\n') + + +class Pins(unittest.TestCase): + def test_version_exact(self): + ok = 'Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit abc, Release)\n' + self.assertTrue(gate.check_lean_version(ok, 'leanprover/lean4:v4.34.1').startswith('Lean (version 4.34.1,')) + for bad in ('Lean (version 4.34.2, x86_64, Release)', 'Lean (version 4.34.10, x86_64, Release)', + 'Lean (version 4.34.1-rc1, x86_64, Release)', ''): + with self.assertRaises(ValueError): + gate.check_lean_version(bad, 'leanprover/lean4:v4.34.1') + with self.assertRaises(ValueError): + gate.pinned_lean_version('leanprover/lean4:nightly') + + def test_worktree_clean(self): + gate.check_worktree_clean('mathlib', '') + for status in (' M Mathlib/Order/Basic.lean\n', 'M Mathlib/Order/Basic.lean\n', '?? extra.lean\n'): + with self.assertRaises(ValueError): + gate.check_worktree_clean('mathlib', status) + + +class Axioms(unittest.TestCase): + def test_allowed(self): + text = ("'A.x' depends on axioms: [propext, Classical.choice, Quot.sound]\n" + "'A.y' does not depend on any axioms\n") + self.assertEqual(gate.audit_axioms(text, ['A.x', 'A.y'], ALLOWED), + {'A.x': ['Classical.choice', 'Quot.sound', 'propext'], 'A.y': []}) + + def test_forbidden(self): + for bad in ('sorryAx', 'Lean.ofReduceBool', 'hiddenPremise'): + with self.assertRaises(ValueError) as ctx: + gate.audit_axioms("'A.x' depends on axioms: [propext, " + bad + "]\n", ['A.x'], ALLOWED) + self.assertIn('forbidden transitive axiom', str(ctx.exception)) + + def test_missing_and_duplicate(self): + with self.assertRaises(ValueError): + gate.audit_axioms("'A.x' does not depend on any axioms\n", ['A.x', 'A.y'], ALLOWED) + with self.assertRaises(ValueError): + gate.audit_axioms("'A.x' does not depend on any axioms\n" * 2, ['A.x'], ALLOWED) + with self.assertRaises(ValueError): + gate.audit_axioms("'A.z' does not depend on any axioms\n", ['A.x'], ALLOWED) + + +if __name__ == '__main__': + unittest.main()