diff --git a/evidence/redacted-excerpts/INC-001-case-A.md b/evidence/redacted-excerpts/INC-001-case-A.md new file mode 100644 index 0000000..f39a2d7 --- /dev/null +++ b/evidence/redacted-excerpts/INC-001-case-A.md @@ -0,0 +1,71 @@ +# INC-001 / Case A — `w1pTime_continuous_in_H` の consumer verdict（2026-06-28） + +- **Incident card:** `evidence/incidents/INC-001.md` +- **論文の対応箇所:** §IV Case A（`paper/sections/04-incidents.tex`），claim CLM-005・CLM-008 +- **Session:** `90fa24bb-c5e4-43ff-8d27-1799177561a0`（host vps，`evidence/session-index/90fa24bb-c5e4-43ff-8d27-1799177561a0.md`） +- **Evidence ID:** EV-0925（メイン transcript，`claude-projects/-workspaces-lean-pde/90fa24bb-c5e4-43ff-8d27-1799177561a0.jsonl`） +- **抜粋範囲:** 同 JSONL の L7650〜L7740（2026-06-28T07:33〜07:59Z） +- **本抜粋が支える記述:** 論文 Case A の「a later proof attempt checked only that no capstone theorem depended on it」，および card の「consumer verdict は未使用であることの利用箇所調査であり，宣言の型の soundness には踏み込んでいない」 + +表記: orchestrator = メインセッションの assistant．`s1-core-opus`／`wkernel-opus` = 派遣された prover agent．引用は原文（英語）のまま．`[…]` は省略．Git trailer と session URL は省いた． + +## 1. 07:35:13Z — orchestrator: 攻撃対象を `w1pTime_continuous_in_H` に定める（L7652） + +> Important strategic finding from the prover: **the whole foundation converges on one core, and the mollification route to it is circular.** B2 (cutoff) and the WALL A commutation *identity* are proved sorry-free, but B1 (the no-Dirac reflection) needs the trace `u(0)` — i.e. the **Bochner-valued 1D-Sobolev FTC / continuous representative**, which *is* `w1pTime_continuous_in_H`. So building the continuous rep *via* mollification is circular (B1 needs the very thing it builds). The real core is one theorem — the **direct Bochner FTC** — and it must be attacked directly, not through mollification. + +## 2. 07:36:20Z — orchestrator → `wkernel-opus` 派遣 prompt 冒頭（L7666） + +宣言は「Lions–Magenes の定理」として汎用の指数 `p` で言い換えられ，型の検査は課題に含まれていない． + +> Attack the single months-class core that the entire final-4-axiom campaign routes through: `w1pTime_continuous_in_H` (the open sorry at `LerayHopf/Bochner/TimeSobolev.lean` ~line 544, Lions–Magenes `W^{1,p}(0,T;V,V') ↪ C([0,T];H)`). A prior prover found the mollification-via-reflection route is CIRCULAR […] +> +> YOUR JOB, in two parts: +> +> PART 1 — RESOLVE THE SOUND, NON-CIRCULAR ROUTE […] Pick the route with NO circular trace dependency and state it precisely […] +> +> PART 2 — START BUILDING the chosen route toward sorry-free `w1pTime_continuous_in_H` […] + +## 3. 07:55:55Z — `wkernel-opus` 第 1 報（L7699） + +> Done with the core investigation. Sound non-circular route FOUND and documented; two R1 building-block kernels PROVED sorry-free. The target stays at its single original ALLOW_SORRY (statement byte-identical, no new axiom). Honest scope: full discharge is genuinely multi-day; I closed the trace-free kernels and characterized the residual precisely. +> +> […] +> +> FILES: route doc + scratch kernel above. TimeSobolev.lean UNTOUCHED (git diff empty; 1 ALLOW_SORRY unchanged). No new axiom/opaque. + +## 4. 07:58:20Z — `wkernel-opus` の consumer verdict（L7731） + +> DECISIVE QUESTION RESOLVED. […] +> +> ANSWER: The sound route to removing the C axioms is (b) the STRONG-APPROXIMANT structure, NOT (a) weak-limit Lions–Magenes FTC. `w1pTime_continuous_in_H` is BYPASSED — it is off the critical path. This makes the limit-passage foundation DAYS-CLASS, not months-class. +> +> EVIDENCE (traced end-to-end): +> 1. `w1pTime_continuous_in_H` is APPLIED NOWHERE — referenced only in docstrings. It is a standalone scaffold. The real C axiom is `galerkin_limit_passage_R3` (R3/AxiomaticClosure.lean:558), applied to the WEAK LIMIT `alPkg.u` (AubinLionsAssembly.lean:84). +> 2. `alPkg.u` carries ONLY `u_aestronglyMeasurable` — no strong derivative, not even a V'-valued weak derivative. […] +> 3. The axiom's five conclusions are each obtainable WITHOUT any continuous-in-H representative of the limit: […] +> +> […] +> +> RECOMMENDATION: Redirect the campaign from "build months-class Lions–Magenes weak-FTC" to "wire the (b) strong-approximant limit passage (Temam III.3) to discharge `galerkin_limit_passage_R3`." That is the path that actually reaches the axiom removal. `w1pTime_continuous_in_H` can stay an off-critical-path scaffold (its own proof, the V'-FTC + interior-mollification route, is documented below the verdict for whoever wants to finish it, but it does NOT gate the C axioms). + +## 5. 07:59:09Z — orchestrator: 計画の破棄と redirect（L7733） + +> Major course-correction — and a hugely favorable one. The prover traced the actual consumer and found `w1pTime_continuous_in_H` is **applied nowhere** (docstrings only) — it's off the critical path. […] **The entire months-class Lions–Magenes / Bochner-weak-FTC machinery is bypassed** — C becomes days-class Temam-III.3 wiring of proved pieces. +> +> This is decisive enough that it must be codex-validated before the pivot […]. Let me hold the now-off-path R1 build, commit the verdict, and codex it. + +## 6. 07:59:32Z — verdict の commit（L7736〜L7737） + +commit message の件名（Bash tool 入力）: + +> docs(bochner): consumer verdict — w1pTime_continuous_in_H is OFF critical path; C is days-class (b)-route + +push 結果（07:59:37Z）: + +```text + a438304..7bb9b27 lane-bochner-f3 -> lane-bochner-f3 +``` + +## 抜粋範囲に存在しないもの + +この窓（07:33〜08:05Z）の全メッセージを通じて，宣言の仮定 `1 ≤ p ∧ 1 ≤ q` を検討する記述はない．verdict の根拠は「参照されていない」という利用箇所調査であり，型の真偽は問われていない．session index は，この transcript 全体で `theorem w1pTime_continuous_in_H` の宣言文字列が一度も現れないことを別途記録している．`p = q = 1` の反例は 2026-07-16 の issue #158（`evidence/repository-snapshots/leray-hopf/issues.json`）で初めて構成された． diff --git a/evidence/redacted-excerpts/INC-002-case-B.md b/evidence/redacted-excerpts/INC-002-case-B.md new file mode 100644 index 0000000..aee802d --- /dev/null +++ b/evidence/redacted-excerpts/INC-002-case-B.md @@ -0,0 +1,90 @@ +# INC-002 / Case B — PR #27 `galerkinConvection_antisymm` のマージ前 adjudication（2026-06-21） + +- **Incident card:** `evidence/incidents/INC-002.md` +- **論文の対応箇所:** §IV Case B（`paper/sections/04-incidents.tex`），claim CLM-005・CLM-008 +- **Session:** `90fa24bb-c5e4-43ff-8d27-1799177561a0`（host vps，`evidence/session-index/90fa24bb-c5e4-43ff-8d27-1799177561a0.md`） +- **Evidence ID:** EV-0925（メイン transcript，`claude-projects/-workspaces-lean-pde/90fa24bb-c5e4-43ff-8d27-1799177561a0.jsonl`） +- **抜粋範囲:** 同 JSONL の L991〜L1039（2026-06-21T02:57〜03:18Z） +- **GitHub 側:** leray-hopf#27（`evidence/repository-snapshots/leray-hopf/issues.json`） +- **本抜粋が支える記述:** 論文 Case B の「Two proof revisions had attempted the unrestricted statement before an independent reviewer identified this missing closure condition」「A numerical diagnostic showed a discrepancy of approximately 80.7 without the projection hypotheses and about 10^-13 with them」「removed the placeholder before merge」 + +表記: orchestrator = メインセッションの assistant．prover／adjudicator／reviewer = `Agent` tool で派遣された subagent（報告は task-notification または tool result として transcript に現れる）．引用は原文（英語）のまま．`[…]` は省略． + +## 1. 02:57:08Z — prover（3rd pass）の報告: statement が偽である旨の blocker note（L991） + +> **antisymm status: honest blocker (not proved).** I determined `galerkinConvection_antisymm` is **false as currently stated** (arbitrary `v w : L2VF`). The proposed `(k,l) ↦ (k,-(k+l))` self-bijection of `fourierBox n` does not exist: `box × box` is not invariant under it (`neg_mem_fourierBox` covers only `k ↦ -k`; concrete witness `k=(1,0,0), l=(1,1,0) ⇒ -(k+l)=(-2,-1,0) ∉ box` for `n=1`). The box truncation breaks the `l ↔ m` IBP reindex, and finite support of `u` does not rescue it. The statement needs `v, w ∈ Vₙ` (a signature change owned by lean-coder). I left a precise `ALLOW_SORRY` documenting exactly this (1 remaining sorry, line 234) […] + +## 2. 02:58:12Z — orchestrator: マージ保留と adjudication の決定（L993） + +> **But** it surfaced a statement-gate issue and left **one `ALLOW_SORRY` on a statement it believes is FALSE**: `galerkinConvection_antisymm` for arbitrary `v,w` (the `fourierBox` reindex genuinely fails; it claims the statement needs `v,w ∈ Vₙ`). That's a problem — discipline forbids a sorry on a false statement; if it's false-as-stated, the *statement* must be fixed (add `v,w ∈ Vₙ`) before merge, not papered with a sorry. The agent itself requested independent confirmation. +> +> So I won't merge it yet. Adjudicating the crux (is `galerkinConvection_antisymm` genuinely false-as-stated, and is `galerkinConvection_bound` sound?), then routing the statement fix. + +## 3. 02:58:35Z — adjudicator の派遣 prompt 冒頭（L994） + +> You are an INDEPENDENT statement-gate adjudicator for PR #27 (3rd revision) in repo uda-lab/lean-pde (branch lane-t/torus3-nsforms, Issue #22, T³ convection form). […] The two prior revisions were unsound; be adversarial. + +## 4. 03:00:41Z — adjudication の結果（L1002） + +> **ADJUDICATION: ANTISYMM-FALSE-NEEDS-Vₙ** +> +> `galerkinConvection_antisymm` (TorusConvectionForm.lean:232–234) is **genuinely FALSE as stated** for arbitrary `v w : L2VF`. Independently confirmed two ways: +> +> 1. **Structural:** `fourierBox n = Icc(−n,n)³` (GalerkinProjection.lean:41). The summand reads `ŵ_i(−(k+l))` with `k,l ∈ box` but `−(k+l)` ranges over `[−2n,2n]³ ⊋ box`. The `l↔m` IBP reindex that drives antisymmetry needs `box×box` invariant under `(k,l)↦(k,−(k+l))`, which it is not […]. Author's witness is arithmetically correct: n=1, k=(1,0,0), l=(1,1,0) ⇒ −(k+l)=(−2,−1,0)∉box. +> 2. **Numerical (my independent reproduction):** with a genuinely div-free `u`, arbitrary v,w give `galConv u v w = 56.69 ≠ −24.03 = −galConv u w v` (diff 80.7). Restricting v,w to Vₙ (box support): both = −50.9597 (diff 1.2e-13). So it is false-as-stated and **true under `velocityProjection_n n v = v`, `velocityProjection_n n w = w`** […] +> +> The `ALLOW_SORRY` documentation is an accurate blocker note, not a false-blocker — it correctly says "false as stated, needs Vₙ." **However, per discipline, a `sorry` parked on a statement the author has proven false is itself a defect** (sorry ⊢ False; a landmine even though quarantined). The correct action is exactly what the note prescribes: **fix the signature first** (add the two `Vₙ` hypotheses), then the sorry becomes legitimate. Adding `v,w∈Vₙ` is a **faithful fix, not a weakening**: the `Torus3NSForms.b_antisymm` field […] needs unrestricted antisymmetry, but it is witnessed by the genuine `∫(u·∇)v·w` form […]; the truncated `galerkinConvection` only ever needs to agree with `b` on `Vₙ` via `b_galerkin` […]. The new lemma has **zero downstream consumers** today, so the signature change breaks nothing. +> +> […] +> +> ``` +> theorem galerkinConvection_antisymm (n : ℕ) (u : L2Sigma) (v w : L2VF) +> (hv : velocityProjection_n n v = v) (hw : velocityProjection_n n w = w) : +> galerkinConvection n (u : L2VF) v w = -galerkinConvection n (u : L2VF) w v +> ``` + +## 5. 03:01:39Z — orchestrator → prover: signature 修正と証明の派遣（L1006） + +> Finish PR #27 (issue #22, T³ convection) by discharging the last `sorry`: `galerkinConvection_antisymm` […]. An independent adjudication CONFIRMED (structurally + numerically) that the lemma is FALSE for arbitrary `v,w` and TRUE under `v,w ∈ Vₙ`, and AUTHORIZED the faithful signature fix below. […] REMOVE the `-- ALLOW_SORRY` (the statement is now TRUE). + +## 6. 03:13:32Z — prover の完了報告（L1020） + +> **Task complete.** PR #27's last `sorry` (`galerkinConvection_antisymm`) is discharged; `LerayHopf/TorusConvectionForm.lean` is now sorry-free. +> +> […] +> +> ### Signature fix (adjudication-authorized) +> `galerkinConvection_antisymm` gained two finite-support hypotheses: +> `(hv : velocityProjection_n n v = v) (hw : velocityProjection_n n w = w)`. The `u` slot is unchanged (`u : L2Sigma`, carrying `DivFreeL2 u`). No external callers exist (grep-verified), so nothing downstream breaks. The `-- ALLOW_SORRY` was removed (statement is now TRUE). +> +> ### Proof (sorry-free) +> Per fixed `k`: restrict both inner `l`-sums from `fourierBox n` to the `σ_k`-invariant set `C_k = box.filter (-(k+l) ∈ box)` (coefficients vanish outside the box via `coeff_zero_outside_box`); reindex the swapped sum by the involution `l ↦ -(k+l)` (`Finset.sum_nbij'`); combine `lₐ + (-(k+l))ₐ = -kₐ`; kill via `∑_a kₐ ûₐ(k) = 0` (`DivFreeL2 u`). […] +> +> ### Remaining sorry +> **None** in `TorusConvectionForm.lean` […] +> +> ### Checks (verified locally — exit codes) +> - `check-no-sorry.sh` → 0 +> - `check-no-axiom.sh` → 0 +> - `check-theorem-names.sh` → 0 +> - `flock /tmp/lean-build.lock lake build LerayHopf.TorusConvectionForm` → BUILD_EXIT=0 (green) +> - downstream `lake build LerayHopf.AxiomaticClosure` → BUILD_EXIT=0 (green) +> +> Committed (`0219ae6` […]) and pushed to `lane-t/torus3-nsforms`; PR #27 body updated to reflect sorry-free status. + +## 7. 03:17:14Z〜03:17:44Z — 最終レビューとマージ（L1035〜L1037） + +orchestrator: + +> #27 antisymm review: **APPROVE** — sound. The blessed `Vₙ` signature, genuine full-strength antisymmetry, `hv`/`hw` load-bearing in the box→`C_k` restriction, the `l↦-(k+l)` involution correctly discharged through `sum_nbij'`, and the `∑ₐ kₐûₐ(k)=0` div-free kill applied verbatim. File sorry-free, axiom-clean, both CI checks green, MERGEABLE. + +`gh pr merge 27 […] --squash` の結果（03:17:44Z）: + +```text +M27=0 + f0c55ce..56b9cfc main -> origin/main +``` + +## 注記 + +差 80.7／1.2e-13 は adjudicator が自前で行った数値再現であり，certified counterexample ではない（card および論文本文と同じ扱い）．先行 2 revision の差分自体は本抜粋に含まれない（card の Confidence 欄参照）． diff --git a/evidence/redacted-excerpts/INC-004-case-C.md b/evidence/redacted-excerpts/INC-004-case-C.md new file mode 100644 index 0000000..57841b4 --- /dev/null +++ b/evidence/redacted-excerpts/INC-004-case-C.md @@ -0,0 +1,102 @@ +# INC-004 / Case C — PR #120 の公開定理 `edge_inf_eq_schwartz_tensor` 消失のマージ前検出（2026-07-10） + +- **Incident card:** `evidence/incidents/INC-004.md` +- **論文の対応箇所:** §IV「Public declarations during refactoring」（`paper/sections/04-incidents.tex`），claim CLM-008 +- **Session:** `7e6156bf-4a4b-40e2-aa46-95822f4d9aa7`（host local-main，`evidence/session-index/7e6156bf-4a4b-40e2-aa46-95822f4d9aa7.md`） +- **Evidence ID:** EV-1669（メイン transcript，`claude-projects/research-lean/7e6156bf-4a4b-40e2-aa46-95822f4d9aa7.jsonl`） +- **抜粋範囲:** 同 JSONL の L436〜L513（2026-07-10T00:12〜00:39Z） +- **GitHub 側:** leray-hopf#120（`evidence/repository-snapshots/leray-hopf/issues.json`） +- **本抜粋が支える記述:** 論文の「one public theorem on the R^3 side, with no downstream users, was omitted from the theorems to reconnect and disappeared. Neither the build nor an earlier review of module structure noticed」「A separate reviewer compared the public declaration inventory before and after the refactor, statement by statement. The theorem was restored with its original statement」 + +表記: orchestrator = メインセッションの assistant（この session では日本語で応答），`prrev-111-1` = 宣言単位レビュー担当の reviewer agent，`glue-111` = 実装担当の coder agent．引用は原文のまま．`[…]` は省略． + +## 1. 00:12:31Z — orchestrator → `prrev-111-1`: verdict の要求（L437） + +> You went idle without reporting. Send your pr-review verdict now: PASS or findings (file:line, severity blocking/non-blocking, evidence), covering statement integrity of the public declarations, no new sorry/axiom/maxHeartbeats, hypothesis minimality of the generic module, deletion completeness, and docstring accuracy. + +## 2. 00:12:57Z — `prrev-111-1` の verdict（L441） + +> VERDICT: FINDINGS (1 blocking, 1 non-blocking). Not a clean PASS. +> +> Method: diffed every public declaration's exact statement between `main` and this branch for both lane files (not just the diff hunks — I re-extracted signatures via regex and did full-file tail diffs). Everything in both lane files from `convFormL2_extends` (R3) / `convFormL2_cont_fixedTest` (Torus) onward — including `r3ConvectionGapOp_holds`, `r3ConvectionGapOp_exists`, `r3_NSForms_exists`, `torusConvectionGap_holds`, and the tail decls — is byte-identical to main. No new `sorry`/`axiom`/`opaque`/`unsafe`/`ALLOW_*` anywhere. `set_option` count and values unchanged in both lane files vs main. +> +> BLOCKING — silent deletion of a public declaration, LerayHopf/R3/ConvectionExtension.lean: +> `edge_inf_eq_schwartz_tensor` was a public theorem on main (main:LerayHopf/R3/ConvectionExtension.lean:980-983, NOT `private`): +> ``` +> theorem edge_inf_eq_schwartz_tensor : +> edgeSlot2 ⊓ edgeSlot3 = LinearMap.range (TensorProduct.mapIncl schwartzSpan schwartzSpan) := +> LerayHopf.R3.TensorIntersection.range_map_subtype_inf_range_map_subtype schwartzSpan +> ``` +> It is completely absent from the new R3 file (grep confirms zero occurrences) — deleted along with its sole use site inside what's now the generic module's private `psi_agree`, with no replacement wrapper added. Evidence this is a real gap, not intentional symmetry: +> 1. Torus kept its counterpart: `edge_inf_eq_galerkin_tensor` is preserved verbatim as a thin wrapper at LerayHopf/Torus/ConvectionExtension.lean:97-105. +> 2. The new shared module's own docstring (LerayHopf/Analysis/TensorEdgeGluing.lean:55-57) explicitly claims: "the tensor-intersection identity's local name (`edge_inf_eq_schwartz_tensor`/`edge_inf_eq_galerkin_tensor` — same content, inlined here from `TensorIntersection` and re-exposed per lane under the lane's own name)" — true for Torus, false for R3. +> Nothing else in-repo currently calls it (checked via `git grep` across all of main), so this doesn't break the build, but it's an advertised public name silently dropped, contradicting both the sibling lane and the new module's own docs. Fix: add the one-line wrapper to R3 mirroring Torus's `edge_inf_eq_galerkin_tensor`. +> +> NON-BLOCKING — stale docstring, LerayHopf/Torus/ConvectionExtension.lean:39: […] + +## 3. 00:13:07Z〜00:13:21Z — orchestrator: 差し戻し（L443・L444） + +> pr-review が blocking 1 件（R3 側の公開定理 `edge_inf_eq_schwartz_tensor` の無断削除 — Torus 側は wrapper 保持で非対称）+ non-blocking 1 件（Torus ヘッダの `gInv` 記述が虚偽化）を検出。glue-111 に修正を差し戻します。 + +`glue-111` への指示（抜粋）: + +> 1. BLOCKING: `edge_inf_eq_schwartz_tensor` was public on main (R3/ConvectionExtension.lean:980-983) and is now silently gone […]. Restore it in the R3 file as a one-line wrapper mirroring the Torus one, with its exact main-branch statement […] + +## 4. 00:17:23Z — `glue-111` の修正報告（L458） + +> Both fixed, one commit `05f3967` on `issue-111-pr1-tensor-glue`: +> +> 1. Restored `edge_inf_eq_schwartz_tensor` in R3/ConvectionExtension.lean as a one-line wrapper right after the `detDomain` wrapper, mirroring Torus's `edge_inf_eq_galerkin_tensor` exactly, same statement it had on main: +> `edgeSlot2 ⊓ edgeSlot3 = LinearMap.range (TensorProduct.mapIncl schwartzSpan schwartzSpan)`, proved via `LerayHopf.R3.TensorIntersection.range_map_subtype_inf_range_map_subtype schwartzSpan`. +> 2. Torus/ConvectionExtension.lean header: dropped the stale `gInv — left-inverse of detDomain.subtype` bullet […] +> +> Both files build clean individually, full `lake build` (3179 jobs) green, no new warnings in either edited region. +> +> ``` +> $ ./scripts/agent-preflight.sh > /tmp/preflight-111-1b.log 2>&1; echo exit=$?; tail -3 /tmp/preflight-111-1b.log +> exit=0 +> OK: LerayHopf.localCompactness_R3_of_ballCompact — Core-clean (no project axioms, no sorryAx). +> AXIOM LIVE PIN OK — all 4 declarations match their pinned axiom sets (R3: 0 project axioms — KERNEL-ONLY, 𝕋³: 0 project axioms — KERNEL-ONLY). +> PREFLIGHT OK +> ``` + +## 5. 00:17:37Z〜00:17:43Z — orchestrator による確認と push（L461・L462） + +```text +$ grep -n "edge_inf_eq_schwartz_tensor" LerayHopf/R3/ConvectionExtension.lean | head -3; git log --oneline main..HEAD +1025:theorem edge_inf_eq_schwartz_tensor : +05f3967 refactor(dedup): restore edge_inf_eq_schwartz_tensor wrapper; fix stale header list +5528204 refactor(dedup): rewire Torus ConvectionExtension onto shared TensorEdgeGluing (issue #111 PR-1, 3/3) +e39838e refactor(dedup): rewire R3 ConvectionExtension onto shared TensorEdgeGluing (issue #111 PR-1, 2/3) +5a89347 refactor(dedup): extract shared tensor/edge-gluing module (issue #111 PR-1, 1/3) +``` + +## 6. 00:18:08Z〜00:18:15Z — PR #120 の作成（L464・L466） + +PR 本文（`gh pr create` 入力）の該当箇所: + +> ## Reviews (in-house, pre-PR) +> - modularity-reviewer: PASS (import surface clean, no cycles, thin instantiations verified, no generality leaks). […] +> - pr-reviewer: 1 blocking finding — `edge_inf_eq_schwartz_tensor` silently dropped on the R3 side — fixed in 05f3967 (restored with its exact main-branch statement); 1 stale-docstring fix. + +結果: + +```text +https://github.com/uda-lab/lean-pde/pull/120 +route: codex (dispatched) +``` + +## 7. 00:38:54Z — マージ（L513） + +`gh pr merge 120 --merge` の本文（Bash tool 入力）: + +> Gates: local preflight PREFLIGHT OK + AXIOM LIVE PIN OK (orchestrator-verified); guards pass; review evidence = @codex review comment on HEAD 05f3967 ('Didn't find any major issues' […]); in-house pr-reviewer blocking finding fixed pre-merge; modularity-reviewer PASS. + +## 抜粋範囲の境界 + +修正 commit `05f3967` 以後，マージまでの間に `prrev-111-1` からの独立したメッセージは +メイン transcript にも同 agent の transcript（EV-1639〜EV-1668 の範囲）にも現れない． +本 transcript が示す修正後の確認は，orchestrator 自身の grep（上記 5）と PR #120 本文・ +merge 本文の記載である．`prrev-111-1` の初回 verdict（上記 2）が述べる +「`convFormL2_extends`／`convFormL2_cont_fixedTest` 以降は byte-identical」は修正前の +照合結果である． diff --git a/evidence/redacted-excerpts/INC-005-case-D.md b/evidence/redacted-excerpts/INC-005-case-D.md new file mode 100644 index 0000000..d3ab34c --- /dev/null +++ b/evidence/redacted-excerpts/INC-005-case-D.md @@ -0,0 +1,178 @@ +# INC-005 / Case D — コンテナ低メモリ cascade の検出と回復（2026-07-18） + +- **Incident card:** `evidence/incidents/INC-005.md`（2026-07-31 の訂正節を含む） +- **論文の対応箇所:** §IV「Resource availability and orchestration」（`paper/sections/04-incidents.tex`），claim CLM-008 +- **Session:** `de129390-559a-4ecd-950e-3667cf1c1c3c`（host vps，`evidence/session-index/de129390-559a-4ecd-950e-3667cf1c1c3c.md`） +- **Evidence ID:** EV-0247（メイン transcript，`claude-projects/-tmp-hermes-worktrees-lean-pde-notes-issue-51/de129390-559a-4ecd-950e-3667cf1c1c3c.jsonl`） +- **抜粋範囲:** 同 JSONL の L7281〜L7329（2026-07-18T06:28〜06:31Z）および L7331〜L7573（07:32〜07:52Z） +- **本抜粋が支える記述:** 論文の「Monitoring had covered the visible Lean process rather than memory available to the whole container」「Roughly seventy minutes after a status check had reported the container healthy on that basis, the author's next status request arrived after an eight-minute delay, followed at once by an instruction to kill stale processes」「a memory check report 606 MiB available」「the fourteen stale chains」「A cumulative kill counter […] was read as confirmation that the out of memory (OOM) killer had terminated the builds」「raised available memory to 2.2 GiB」「The worktree returned to the original agent, the duplicate stopped, and the build completed under a global lock」 + +表記: owner = 著者（user メッセージ），orchestrator = メインセッションの assistant，`issue155`／`issue155b` = 派遣された implementation agent．引用は原文（日本語・コマンド出力）のまま．`[…]` は省略．`` は session 固有の長い作業ディレクトリ path の置換，`~` は home directory の置換．Swap 行は host 側の値（card 参照）． + +## 1. 06:28:39Z — owner の状況確認（L7283） + +> 短時間と言ってもやはりコンテナのリソースでは時間がかかっているのかねぇ？　あぁ，無理に止めなくていいよ，状況を知りたいだけ + +## 2. 06:28:52Z — orchestrator の `ps aux | grep -E 'lake|lean'` 出力（L7289，冒頭 3 行） + +前日 07-17 起動の codex broker がこの時点で出力に現れているが，以下 3 の報告では言及されない． + +```text +vscode 414083 0.0 0.5 1023020 20196 ? Ssl Jul17 0:00 /usr/bin/node ~/.claude/plugins/cache/openai-codex/codex/1.0.6/scripts/app-server-broker.mjs serve --endpoint unix:/tmp/cxc-nzwzHH/broker.sock --cwd /tmp/hermes-worktrees/lean-pde-notes-issue-51 […] +vscode 419445 0.0 0.2 1014596 10740 ? Ssl Jul17 0:00 /usr/bin/node ~/.claude/plugins/cache/openai-codex/codex/1.0.6/scripts/app-server-broker.mjs serve […] --cwd /workspaces/lean-pde-notes/.claude/worktrees/agent-a1ca7a1691a00fca3 […] +vscode 426718 0.0 0.2 1014324 10584 ? Ssl Jul17 0:00 /usr/bin/node ~/.claude/plugins/cache/openai-codex/codex/1.0.6/scripts/app-server-broker.mjs serve […] --cwd /wt-153 […] +[…] +``` + +## 3. 06:29:27Z — orchestrator の報告（誤診断，L7304） + +> **issue155b の detached ビルド（wt-155、Torus.ConvectionExtension）** +> - 15:00 に再起動されたビルドが現在 **1896/1929** まで到達（15:28 時点、更新継続中）。[…] +> - 遅さの原因は 2 つ重なっています: (1) wt-155 は `lake exe cache get` を通していない worktree なので mathlib をソースからコンパイルしている、(2) コンテナの CPU/メモリ制約で並列度が 3〜4 プロセスに留まり、1 ファイル 20〜70 秒かかっている。[…] +> - メモリは lean プロセス合計で ~850MB 程度と cgroup 上限（3.42GiB)に対し余裕があり、OOM の危険はいまのところありません。 + +## 4. 06:30:55Z — owner（L7309） + +> cache は worktree で共有する方針じゃなかったかね？ それだと実質フルビルドですね．まぁ良いですよ．時間はあるので． + +## 5. 07:32〜07:40Z — 8 分の配送遅延と kill 指示（queue-operation 記録，L7331・L7332・L7342） + +transcript の queue 操作記録（`type: queue-operation`）を時刻順に転記する． + +| timestamp (UTC) | operation | content | +|---|---|---| +| 07:32:21.086Z | enqueue | `status` | +| 07:40:09.776Z | dequeue | — | +| 07:40:12.282Z | enqueue | 不要なサブエージェント・stale プロセス・codex ゾンビ・その他，無駄にメモリーを食っているものを片っ端から一度殺してください．メモリーを少しでもあけると Lean の作業も早くなるでしょう． | + +## 6. 07:40:39Z — 枯渇の検出（L7352） + +```text +$ free -h; cat /sys/fs/cgroup/memory.max /sys/fs/cgroup/memory.current + total used free shared buff/cache available +Mem: 3.8Gi 3.2Gi 196Mi 3.9Mi 699Mi 606Mi +Swap: 2.0Gi 110Mi 1.9Gi +--- +3670016000 +3567398912 +``` + +## 7. 07:41:25Z — 残留チェーンの特定（L7367） + +`readlink /proc//cwd` の結果（15 系統中，末尾の 1 系統のみ稼働中）: + +```text +414097 -> /tmp/hermes-worktrees/lean-pde-notes-issue-51 +419459 -> /workspaces/lean-pde-notes/.claude/worktrees/agent-a1ca7a1691a00fca3 (deleted) +426732 -> /wt-153 +439647 -> /wt-147 +512171 -> /wt-166 +556278 -> /nwt-65 +561064 -> /nwt-66 +563827 -> /workspaces/lean-pde-notes/.claude/worktrees/agent-a81a93a6b0dd4253d (deleted) +579598 -> /workspaces/lean-pde-notes/.claude/worktrees/agent-aec021c65c5c8cdbf (deleted) +585295 -> /nwt-68 +597450 -> /workspaces/lean-pde-notes/.claude/worktrees/agent-a616e07de824a2008 (deleted) +602315 -> /nwt-72 +605160 -> /workspaces/lean-pde-notes/.claude/worktrees/agent-ac6e3fa980298248b (deleted) +665705 -> /nwt-70 +875628 -> /tmp/hermes-worktrees/notes-issue-30 +``` + +## 8. 07:42:18Z〜07:42:49Z — 一括 kill と回復（L7377・L7384） + +Bash tool 入力の description: "Kill 14 stale codex broker/app-server chains, keep active notes-issue-30 chain"．直後の計測: + +```text + total used free shared buff/cache available +Mem: 3.8Gi 1.6Gi 276Mi 3.9Mi 2.3Gi 2.2Gi +Swap: 2.0Gi 156Mi 1.8Gi +--- +3430502400 +--- +945303 1863MB […]/bin/lean /wt-155/LerayHopf/Torus/ConvectionExtension.lean -o +386323 643MB claude --resume +945221 112MB […]/bin/lake build LerayHopf.Torus.ConvectionExtension +``` + +## 9. 07:44:12Z〜07:44:44Z — 累積カウンタの読み取りと当時の帰属（L7410・L7415） + +```text +$ cat /sys/fs/cgroup/memory.events +low 0 +high 0 +max 31553152 +oom 0 +oom_kill 7 +oom_group_kill 0 +``` + +orchestrator → `issue155b`（07:44:44Z）: + +> (1) 判明した事実: あなたのビルドが繰り返し死んでいた原因は OOM です（cgroup memory.events で oom_kill=7 を確認。ログの exit 137 = SIGKILL はすべてこれ）。直近 16:42 頃には mathlib 依存は全て built 済みで、ターゲットの LerayHopf/Torus/ConvectionExtension.lean 本体のコンパイル（RSS 1.8GB 超）まで到達した後に殺されています。[…] +> (2) owner 指示でコンテナのメモリ大掃除を実施しました: 旧 worktree に紐づく codex app-server/broker ゾンビ 14 系統（約 1〜1.5GB）を kill 済み。used 3.2Gi → 1.6Gi、available は 2.2Gi に回復しています。[…] +> (3) 指示: いますぐ `flock /tmp/lean-build.lock lake build LerayHopf.Torus.ConvectionExtension` を再実行してください […] もし再度 137 で死ぬ場合は、(a) `LEAN_NUM_THREADS=1` を付けて逐次コンパイルでピークメモリを下げる、(b) それでも駄目なら owner へのエスカレーション対象として私に報告してください […] + +この帰属（7 件の kill が当日の build 死である）は 2026-07-31 の host 側 kernel log 照合（KSE2026 issue #100）で否定された．7 件はすべて 07-16 の host global OOM に帰属し，当日の kill 機構は未特定である（card の訂正節）． + +## 10. 07:45:03Z — 死亡と判定されていた `issue155` の報告（L7459） + +> (b) 詰まっていた点（解消済み）: 新規 worktree（wt-155）の `.lake` が空で、targeted build が mathlib ~1900 ファイルの実質フルビルドに突入し数時間かかっていた […]。1回 build を kill し、既存 clone（lean-pde、mathlib フルビルド済み 8.5G）から `cp -al` でハードリンク共有し復旧。現在は対象ファイルのみを正しくコンパイル中（`lake` 経過時間 数分、mathlib 再ビルドなし — プロセスツリーで確認済み）。 + +## 11. 07:45:29Z〜07:46:15Z — 二重稼働の解消（L7463・L7471・L7481） + +orchestrator: + +> issue155（先代・死亡と判定していた agent）が生きていて、しかもキャッシュ共有を自力で復旧し正しい targeted build 中とのこと。後継 issue155b と二重体制になっているので、即座に交通整理します。 + +`TaskStop` の結果（07:46:03Z）: + +```text +{"message":"Successfully stopped task: trbmczr7p […]","task_id":"trbmczr7p","task_type":"in_process_teammate"} +``` + +残った build（07:46:15Z）: + +```text +946048 flock /tmp/lean-build.lock lake +946049 […]/bin/lake build LerayHopf.Torus.ConvectionExtension +946109 […]/bin/lean /wt-155/LerayHopf/Torus/ConvectionExtension.lean -o +``` + +## 12. 07:47:34Z — 常設指示への注入（L7491） + +`~/.claude/CLAUDE.md` に追記された節（Bash tool 入力の heredoc）: + +> ## 本コンテナ限定 — メモリ・プロセス衛生（恒常規約、2026-07-18 owner 指示で明文化） +> +> このコンテナは cgroup 上限 ~3.4GiB。Lean/mathlib ビルドはピーク 2〜3.4GiB に達し、**メモリが最稀少資源**。`exit 137` は原則 OOM（`cat /sys/fs/cgroup/memory.events` の `oom_kill` で確認）。以下は「思い出したら守る」メモリー任せにせず、毎回機械的に実施する: +> +> 1. **codex プラグインの broker/app-server チェーンは自動回収されない**（cwd ごとに `app-server-broker.mjs` + `codex app-server` ×2、計 60〜330MB）。codex 事前レビュー完了・worktree 撤収のたびに該当チェーンを即 kill する。放置実績: 2026-07-18 に 14 系統 ~1.5GB を溜め込み Lean ビルドが OOM 連発。 +> 2. **定期 sweep**: Lean ビルド開始前・agent dispatch 前に `ps aux | grep app-server-broker` を確認し、cwd が削除済み/merge 済み worktree を指す chain を全て kill（`readlink /proc//cwd` で判定）。 +> 3. **ビルド前ヘッドルーム確認**: `free -h` で available ≥ 2GiB。不足なら先に掃除（削るのはゾンビであって稼働中ビルドではない）。 +> 4. **新規 worktree に自前 `.lake` を作らせない** — mathlib フルビルド済みクローンの `.lake` を `cp -al`（ハードリンク）で共有。cold build は mathlib ~1900 ファイルの実質フルビルド（数時間 + OOM リスク）になる。 +> 5. **dispatch prompt に毎回明記**: (a) `.lake` 共有方法、(b) `flock /tmp/lean-build.lock`（コンテナ全体で lean build 同時 1 個）、(c) 作業完了時に自分の codex chain を掃除すること。 +> 6. OOM 再発時の縮退: `LEAN_NUM_THREADS=1` で逐次コンパイル → それでも不可なら owner へエスカレーション（モジュール分割の判断材料として報告）。 + +## 13. 07:48:04Z — orchestrator の経緯説明（L7501，第 1 段落） + +> **いつから溜め込んでいたか**: プロセスの起動時刻から、14 系統のうち 13 系統は **昨日 7/17 の夜間波**のものでした。codex 事前レビューを worktree ごとに実行するたびに broker+app-server が 1 系統ずつ生まれ（1 worktree = 1 系統、自動回収なし）、PR が merge され worktree が用済みになっても私が一度も回収せず、**丸一日半放置**していました。[…]「コンテナ資源が最重要制約」という指示をメモリーに持ちながら、lean ビルドの並列度にしか適用せず、自分が起こしたプラグインプロセスの後始末には適用していなかった […] + +## 14. 07:49:42Z — owner（L7512） + +> はい．global memory にも project memory にもしっかりと刻んでください．なお，codex server が放置されていて OOM 連発を起こしたのも既に数回目です．メモリーにも入っているはずです． + +## 15. 07:51:55Z — 4 層への記録完了（L7571，冒頭） + +> 刻み終わりました。記録先は 4 層です： +> +> **Global memory** […] — 新規 `feedback_reap_agent_side_processes.md`：汎用規則「オーケストレーションが生む常駐サイドプロセスは完了イベントごとに reap + 重処理前に sweep」。再犯 2 回（2026-05-09 の tmux pane 版 […]、2026-07-18 の codex chain 版）を明記 […] +> **本 project memory** […] — 新規 `feedback-container-memory-hygiene.md` […] +> **lean-pde 側 project memory** — ビルド制約の正典 `project_build_env_memory_ceiling.md` に追記 […] +> **注入層** — `~/.claude/CLAUDE.md` の「本コンテナ限定 — メモリ・プロセス衛生」節 […] + +global memory の実物は EV-0005（`claude-projects/-home-vscode/memory/feedback_reap_agent_side_processes.md`）として escrow に収録されている． + +## 抜粋範囲外の関連事象 + +同日 12:42Z／13:06Z の別形態での再発（正当な単一ビルドのピーク RSS による `available` 低下）と 13:10Z の規約定着確認は，session index と card に記録されているが本抜粋には含めない． diff --git a/evidence/redacted-excerpts/README.md b/evidence/redacted-excerpts/README.md new file mode 100644 index 0000000..8a3ecf6 --- /dev/null +++ b/evidence/redacted-excerpts/README.md @@ -0,0 +1,29 @@ +# evidence/redacted-excerpts/ + +論文 §IV の 4 事例（Case A–D）を支える一次セッション記録の抜粋．各ファイルは +`private/raw-sessions/`（gitignored escrow）の JSONL transcript から手で選別し， +`scripts/redact_check.py` を通したもの．引用は原文のまま，省略は `[…]`， +redaction による置換は `<…>` または `~` で示す． + +| ファイル | Incident | 論文 | session | Evidence ID | 窓（UTC） | +|---|---|---|---|---|---| +| `INC-001-case-A.md` | INC-001 | §IV Case A | `90fa24bb` (vps) | EV-0925 | 2026-06-28 07:33–07:59 | +| `INC-002-case-B.md` | INC-002 | §IV Case B | `90fa24bb` (vps) | EV-0925 | 2026-06-21 02:57–03:18 | +| `INC-004-case-C.md` | INC-004 | §IV Public declarations during refactoring | `7e6156bf` (local-main) | EV-1669 | 2026-07-10 00:12–00:39 | +| `INC-005-case-D.md` | INC-005 | §IV Resource availability and orchestration | `de129390` (vps) | EV-0247 | 2026-07-18 06:28–06:31, 07:32–07:52 | + +各ファイルの冒頭に，出典（EV-ID・JSONL の行範囲）と，対応する incident card・claim・ +論文の文を記す．INC-003（ログローテーションによる記録喪失）は「記録が存在しない」ことが +内容であり，抜粋の対象にならない． + +## 選別と redaction の方針 + +- 論文本文と incident card が引用する事実（時刻・数値・判断）を一次記録で確認できる + 最小限の範囲に限る．抜粋範囲外の関連事象は各ファイル末尾で card への参照に留める． +- 抜粋中の path は，username を含む home directory を `~` に，session 固有の長い + 作業ディレクトリを `` に置換した．Git trailer・session URL・agent の + 内部 ID の類は省いた． +- 人物は「owner（著者）」「orchestrator」「agent 名」で表記する．GitHub login は + 公開 repository（`uda-lab/leray-hopf`，旧名 `lean-pde`）に関するもののみ残る． +- 追加・変更時は `python3 scripts/redact_check.py --dir evidence/redacted-excerpts` + で検出ゼロを確認する（denylist は `private/redact-names.txt`）． diff --git a/scripts/check_frozen_paths.sh b/scripts/check_frozen_paths.sh index 81dc255..043e3ac 100755 --- a/scripts/check_frozen_paths.sh +++ b/scripts/check_frozen_paths.sh @@ -52,6 +52,11 @@ base="${1:-origin/main}" # # issue #109 (2026-08-01): the owner authorized synchronizing the CMT abstract # draft with the post-#106 manuscript abstract (decision record in issue #73). +# +# issue #127 (2026-09-23): the manuscript states that the repository provides +# redacted evidence excerpts, and the owner decided to bring the repository in +# line with that sentence rather than change it. The excerpts for Cases A-D +# are added under evidence/redacted-excerpts/ as owner-authorized additions. FREEZE_EXEMPT_PINNED=( "notes/submission-metadata.md:78cf2f79ede6b296e06b06071f2ed123a4491850" "evidence/incidents/INC-005.md:468838e6516409137c0acb880f962d41a3e87425" @@ -59,6 +64,11 @@ FREEZE_EXEMPT_PINNED=( "claims/paper-claims.md:74b0041a54c029d375cceadf92c9795abb760e32" "analysis/incident-ranking.md:f669c68ea3a2ffa3381fdf8b997752909261f69c" "analysis/incident-candidates.md:1ad4ab9df88fa2173f127f54354f7c333360ae80" + "evidence/redacted-excerpts/README.md:8a3ecf68c20956b7224542b70a43fc0516973256" + "evidence/redacted-excerpts/INC-001-case-A.md:f39a2d71abe97c7d39482d2c4bd9f6fa6ef8eba7" + "evidence/redacted-excerpts/INC-002-case-B.md:aee802d27f2c4a219888cc1646c787fb364099ea" + "evidence/redacted-excerpts/INC-004-case-C.md:57841b42c7b24d9134d595541578905cc4d1956a" + "evidence/redacted-excerpts/INC-005-case-D.md:d3ab34cfde2b883faeacca5430982cde5b2901dc" ) FREEZE_EXEMPT_UNPINNED=( "scripts/check_frozen_paths.sh"