Skip to content

Add redacted evidence excerpts for the four incident cases #130

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
uda-lab-agent merged 1 commit into from
Sep 23, 2026
Merged

Add redacted evidence excerpts for the four incident cases #130

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
71 changes: 71 additions & 0 deletions evidence/redacted-excerpts/INC-001-case-A.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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`）で初めて構成された．
90 changes: 90 additions & 0 deletions evidence/redacted-excerpts/INC-002-case-B.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 欄参照）．
Loading
Loading