STEP 1375 — 4 repo public publish arc + protocol utilities landed

2026-08-23 (帰宅後 arc 続編 Arc 3-5 合流) · SAC-4 認諾 2 件 · commit hash 追記予定

1. 経緯

STEP 1370 の 帰宅後 4 arc 連鎖の うち、 Arc 2 (STEP 1370 site 反映) までは 前 turn 記録済。 本 STEP は 残 Arc 3-5 の 合流記録:

STEP 1373 (別 session の REPRODUCING.md pilot) が Arc 3 の v0.2.0a1 を 土台として 参照 しているが、 Arc 3 自体は entry-level 未記録、 Arc 4/5 は 完全未記録。 本 STEP で 揃える。

2. Arc 3 — rei-checker-mcp v0.2.0a1 protocol utility 5 module

V02_PROTOCOL.md (STEP 1366 起草、 chat-Claude Gemini critique 13 findings A-E → 6 protocol distill) の うち 4 protocol を isolated + testable utility として wire-ready 化。 real LeanBackend 未 landing、 v0.2.0a1 は 「protocol utilities in place, not yet wired to running Lean」 位置付け明示。

ProtocolStatusLocationTest
§1 A1 Sandboxdoc onlydocs/V02_PROTOCOL.md §1n/a (env-level)
§2 A2 spawn error handlinglandedrei_checker/subprocess_util.py::_run_lean_safely4 case
§3 A3 process tree killlandedrei_checker/subprocess_util.py::_kill_process_tree1 case cross-platform (Windows taskkill / POSIX killpg)
§4 B4 axiom JSON parselandedrei_checker/axiom_parser.py::parse_axioms_from_lean_json_output10 case (fixture-based)
§5 C7 REPL serverStage 1lean_backend/ (STEP 1367 spike, v4.29.0 pin)13 smoke pass
§6 D11 UNCLASSIFIEDlandedschema.py::ReasonCode.UNCLASSIFIED3 case + 1 update

副次 discipline: AxiomScanResult.saw_axiom_diagnostic 独立 flag = 「axiom list 空 → 真空 True」 trap 予防 (V02_PROTOCOL.md §4 threat 直接 counter)。 _run_lean_safely NEVER raises invariant = 全 failure mode を 明示 tuple で 表現 (subprocess wrapper が 例外を hide しない)。

verify: 73/73 test PASS (55 pre-existing + 18 new)、 version 0.1.0a1 → 0.2.0a1。 commit: ba45b3a push 済。

3. Arc 4 — discovery-worker v0.3 merge_gate runtime enforcement

v0.2 は requires_pipeline_pass: true を advisory flag として emit (downstream consumer が ignore 可能)、 v0.3 で 促進境界 (pipeline output → output/approved/) で runtime enforcement。 生成 noise が operator ceremony 経由で approved/ に 入る経路を 構造的に閉じる。

促進 decision matrix (asymmetric)

OriginVerdictDefaultWith --allow-partial
Generatorfull passPROMOTE同
Generatorpartial passREJECTREJECT (asymmetric — override 効かない)
Humanfull passPROMOTE同
Humanpartial passHOLDPROMOTE (human_override)
Anydropped / NEITHERREJECT常に REJECT

非対称性の意義: --allow-partial は 人間の 判断責任で partial pass promote する escape hatch。 generator の partial pass は override 不能。

verify: 23/23 test PASS + Smoke test (v0.2 pipeline output に dry-run): 3 Wolstenholme conjectures 全 dropped_at_stage (v0.2 で hunter_beta が arXiv prior art 検出) → merge_gate 3 REJECT = 生成 noise が approved/ に 到達せず (v0.3 core value 実証)。 commit: bb019e8 local (repo remote 未設定 = 隔離 by boundary 設計継承)。

4. Arc 5 — 4 repo public 公開 (fc0web 下)

publish-4repos.sh 経由で 4 repo を 一括 public 公開達成。 4 previously local-only repo → GitHub public visible の 大きな 可視性 milestone。

repoURLcommitlicense特記
codetrailgithub.com/fc0web/codetrail6d6a709MIT ✅package.json + README を fc0web に revert (Marketplace publisher は CHANGE-ME-publisher-id 復元 = defer 明示)
rei-solvergithub.com/fc0web/rei-solver52e53c0MIT ✅Z3/SymPy/PySAT 統合層 (21 tracked files)
rei-fpgagithub.com/fc0web/rei-fpga78e4f9eMIT ✅yosys/GOWIN + rei-solver で 回路等価証明 (21 tracked files)
analog-forgegithub.com/fc0web/analog-forge3263073MIT ✅analog circuit dataset generator (53 tracked files、 out/*/trials.jsonl 3 個 80 MB warning)

5. SAC-4 認諾 record (2 件)

#1 — nobukifujimoto owner 404 → fc0web pivot: cloud Claude session の 「GitHub owner = nobukifujimoto」 assertion が 未存在 account (404 Not Found) だった。 実行直前 gh api users/nobukifujimoto で 404 検出、 stop → 藤本さん判断 (option 2 = fc0web) GO で pivot。 cloud Claude assertion は user intent (「これから 作る予定」) を 前提とした先読みだったが、 私 (Rei機 session) の 現状 verify で 「未存在」 判明、 feedback-verify-claim-must-cover-all-source-derived-numbers operational 実例 (「所有者」 数値 = account 存在の verify 主張の 部分性)。 pivot 影響: codetrail の 5 箇所 revert commit 6d6a709 + publish-4repos.sh の OWNER="${OWNER:-fc0web}" 化 + SKIP_MARKETPLACE_GATE=1 flag 追加 (gate は marketplace publish 用、 git push とは 論理層別)。

#2 — rei-fpga phantom CRLF diff cross-session 分業 fill: cloud Claude が 「.gitattributes で 消えている」 と claim、 実測で 4 files (examples/*.json) 未消去 = Windows filesystem 側で git add --renormalize 未実行だった partial gap。 私 (Rei機 session) で renormalize 実行 → 0 dirty clean 復元 = cross-session 分業の 別 例 (「chat/cloud で 認知 + local で 実行」 pattern)。

6. 副次 finding (analog-forge 80 MB files 3 個)

analog-forge push 時 GitHub warning: out/final/trials.jsonl + out/demo3/trials.jsonl + out/demo4/trials.jsonl 各 80.25 MB (GitHub 推奨 50 MB 超過、 hard limit 100 MB 未達)。 藤本さん 「tracked のまま出す」 判断で 意図的公開 = 動作は 意図通り。 「生成物込み repo」 として 公開状態、 rei-open-problems 型 「作品」 pattern と 整合的。 clone / download 経験優先の 場合 Git LFS 移行が defer candidate、 今 action 不要。

7. ⚠ 藤本さん実行必要 (私 API 不能、 STEP 1370 継続)

GitHub 側 PAT revoke:

  1. https://github.com/settings/tokens 開く
  2. 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 を 検索
  3. 「Delete」 or 「Revoke」 実行

★ 私が redact したのは local file の PAT 文字列除去のみ、 GitHub server 側 token は 依然 有効。 revoke で 初めて 万一 leak 経由の 使用不能化が 安全確定。

8. Honest scope 8 条

  1. rei-checker-mcp v0.2.0a1 は utility landed のみ、 real LeanBackend 未 wire = 「protocol prep 完了、 実 Lean judgment は Stage 2 defer」 明示、 「v0.2 完成」 主張ではない。
  2. discovery-worker v0.3 merge_gate は promotion 境界のみ enforce、 Lean 4 stage (TOTAL_FILTER_COUNT の 3rd) は 未 wire = full pass unreachable 状態 (意図的、 generator noise が approved/ に 現状 到達不能 discipline)。
  3. fc0web 下 4 repo 公開は 「初回 push」 のみ = README / issue template / CI / release 等 downstream ceremony は 未整備。
  4. analog-forge 80 MB × 3 files は 意図的公開、 「作品」 pattern の 継承 だが GitHub 推奨 50 MB 超で clone 体験 悪化余地あり。
  5. codetrail Marketplace publisher は defer、 現状 CHANGE-ME-publisher-id = vsce publish は gate で 停止する状態、 GitHub 公開のみ 完了。
  6. 「4 repo 公開で 世界初」 主張ゼロ (feedback-world-uniqueness-claim-controllable 適用) = 各 repo は 個別 tool、 4 repo 揃った公開行為 自体は publish action の 実行のみ、 novelty ゼロ。
  7. cross-session collaboration (cloud Claude + Rei機 session) の SAC-4 認諾 2 + fact verify 数件 は 本 arc の 質保証 evidence だが、 「cross-session 分業で 世界初」 主張は しない (10 例目 pattern)。
  8. PAT revoke は 私 API 不能、 藤本さん実行必要、 未実行状態継続。

9. 関連 memory