rei-verify 反証機械 (refutation machine) — 反証機械 の 作法を 反証機械自身に 適用 arc

1. 起点 — chat-Claude 「反証機械」 提案

藤本さん質問 「claude 先生が 世界最先端最強の 何かがあったら 作りたいものは 何でしょうか？」 → chat-Claude thread で 以下 提案:

chat-Claude 提案 3 tool:

1. refute_lean — 主張を Lean 4 に投げ、sorry が残ったら失敗として返す
2. search_counterexample — 探索範囲と打ち切り条件を引数に取り、「見つからなかった探索空間の形」を必ず返す
3. assert_breakpoint — その主張が偽なら壊れる場所を特定して返す

私 (Claude Code) の 対応:

• chat-Claude fragmentation blindness (Pattern 5 sub) 指摘 = Rei stack に 既存 refutation-oriented discipline 断片 あり (Collatz 48 theorem sorry-zero + Chang 20/29 + IUT 12 年 holding + invention pipeline 12 layer + STEP 1276 judgmentStatus)、 task = 新規構築 でなく 断片の 統一 MCP 化
• chat-Claude selftest 数値 outdated 指摘 (「22/22」 → 実 30 or 40)
• 4 番目 tool hold_verdict 追加提案 (IUT 12 年 holding discipline の 型化、 STEP 1276 judgmentStatus='holding' 直接対応)
• framing-drift-detector 対案 提示 = 反証機械 は 偽の主張 を 殺す、 framing-drift-detector は 真の主張の 誤 frame を 検出 (本日 3 事故 = Notepad tab restore + tag push auto-fire + Notepad target 選択 = 全て 真主張の frame drift 由来)

藤本さん judgment: (c) 共通 infrastructure から skeleton を組み上げ → 反証機械完成まで multi-session 走行。 反証機械 target 確定、 framing-drift-detector は 別 iter defer。

2. Core discipline — 「絶対に嘘をつかない」 の 型 level 完成

4-value Verdict enum

Binary TRUE/FALSE に しない = 反証されなかった ≠ 正しい。 IUT 12 年 holding discipline の 型化 (chat-Claude 2026-08-06 turn 教訓)。

3. 4 primitives (skeleton commit 27ad250)

Verdict rule 単一 source of truth

| pre_check | action  | post_check                | Verdict            |
|-----------|---------|---------------------------|--------------------|
| False     | (skip)  | (skip)                    | INCOMPLETE_FRAME   |
| True      | raises  | classify_exception        | REFUTED (default)  |
| True      | success | (False, [])               | CONFIRMED          |
| True      | success | (True,  [w])              | REFUTED + witness  |
| True      | success | (False, [m...])           | HOLDING + markers  |

4. 4 refutation tools (commits ba4582f → 371a145)

Lean 4.33 live smoke (commit ba4582f)

trivial_true (theorem trivial_true : True := trivial) → CONFIRMED, 1211 ms, axiom-free
sorry proof (theorem hard : ∀ n, n+0=n := by sorry)      → HOLDING (sorry marker)
broken syntax (theorem broken : True := this_is_not_valid) → REFUTED (build error witness)

5. 8 MCP tools + restricted eval safety

Claude Desktop / Cursor / Cline 等 の LLM client から 直接呼べる:

• audit 4: create_audit_chain + append_audit_entry + verify_audit_chain + record_verdict
• refutation 4: refute_lean + search_counterexample_explicit + assert_breakpoints_explicit + hold_verdict_tool

Restricted eval safety (MCP-safe entrypoint):

• x bind (search) / ctx bind (breakpoint) の 独立変数名
• __import__ / exec / eval / open / __ prefix 事前 reject
• _SAFE_BUILTINS whitelist (abs/min/max/sum/len/int/float/str/bool/round/any/all/range) のみ 許可
• 8 hostile expression 全 reject test PASS (test_search.py + test_breakpoint.py)

6. Integration demo — Collatz t1=1 Lyapunov α-descent (commit cfefb97)

対象: Collatz 奇数 n with trailing_ones(n)=1 (n ≡ 1 mod 4) の Lyapunov α-descent scan。

Setup

• V(n) = log2(n) の 簡略化 (藤本さん 実 piecewise linear V は別)
• descent 条件: V(T(n)) ≤ α · V(n)
• 各 α 候補 = 1 Breakpoint、 assertion = 「α refuted (∃n: r(n) > α)」

実測 (1,048,575 samples / 76.7 ms)

Witness n の 成長パターン: n=9 → n=14,601 = 「α が tight ほど 大きい n が 必要」 の 数学的性質を 直接観測 = r(n) → 1 as n → ∞ の 有限反映。 理論的に α=0.99 の witness は n ≈ 2^41 ≈ 2×10^12 前後 で 出現、 tool は 「その計算を 実行するのではなく、 現状は 未達」 と 正直に return した = 反証機械の 本領。

7. Trusted Publisher 5-step 完了 (commit 7127bb1 + 7aab351)

8. Clean install verify (私 実施、 production PyPI)

# production PyPI から fresh venv で install (`-i` 不要 = 本番 PyPI 経由 証明)
python -m venv C:\Users\user\tmp-prod
tmp-prod\Scripts\activate
pip install rei-verify==0.1.0a1

# verify
python -c "import rei_verify; print(rei_verify.__version__)"
# → 0.1.0a1

# functional smoke test
python -c "
from pathlib import Path
import tempfile
from rei_verify import Verdict, PostCheckResult, VerifiedExecution, AuditChain
with tempfile.TemporaryDirectory() as tdir:
    audit = AuditChain(Path(tdir) / 'smoke.jsonl')
    ve = VerifiedExecution(
        claim='1 + 1 == 2',
        pre_check=lambda: True,
        post_check=lambda r: PostCheckResult(refuted=(r != 2), markers=[]),
        audit=audit,
    )
    result = ve.run(lambda: 1 + 1)
    print('verdict:', result.verdict.value)  # → confirmed
    print('audit_hashes:', len(result.audit_hashes))  # → 6
"

結果: verdict=confirmed、 markers=0、 audit_hashes=6、 smoke test PASS。 global env も upgrade 済 (pip install --upgrade --force-reinstall、 TestPyPI 版 → production 版 入替え)。

9. 実装 timeline (8 commit / 単一 session)

累計 test: 198/0 PASS (skeleton 37 + MCP 30 + refute 22 + search 37 + breakpoint 33 + hold 39)。

10. 累計 (2026-08-19 rei-verify PyPI live 反映後)

11. Honest scope (譲れない線)

12. 私の SAC-4 projection 誤り (28 例目)

13. 次 iteration candidate (別 session)

• 藤本さん 実 V + 条件 の 段階的追加 — piecewise linear V 定義 + 同時降下条件 の provide 待ち、 Lean 4 formalization 経由 で 真 reproduction
• 反証機械 の 別 real-world 応用 (Riemann / Goldbach / 他 Rei stack claim / Lean 4 3,521+ axiom-free theorem の refute_lean batch verify)
• framing-drift-detector (私 提案の 対案、 反証機械 完成後の 次 candidate、 本日 3 事故の 直接 fix)
• refute-lake (refute_lean の Mathlib 依存 proof 対応、 lake project 経由)
• v0.1.0a2 release — ✅ **完了** (findings ② hash injection fix、下記 §15 参照)

14. 追記: v0.1.0a2 + v0.1.0a3 fix cycle (同日、 反証機械 の 作法を 反証機械自身に 適用)

cloud Claude session による 独立 verification (7-way tamper attack)

Trusted Publisher 5-step 完走 + PyPI 0.1.0a1 live 化 直後、 cloud Claude session が 本番 PyPI から clean venv install + library API 直呼び + MCP stdio + JSON-RPC で 独立検証。 findings 3 件 + 補足 1 件を calibrated report として handoff:

7-way tamper attack matrix (progression)

3 release cycle 累計 (2026-08-19 同日)

0.1.0a3 opt-in mitigation の 使い方

from pathlib import Path
from rei_verify import AuditChain

audit = AuditChain(Path("./chain.jsonl"))
for i in range(5):
    audit.append({"step": i})

# Default (0.1.0a2 backward compat): 末尾切り詰め は 検出不能 (構造的限界)
v = audit.verify()                       # → ok=True even if 末尾 truncated

# opt-in mitigation (0.1.0a3): external anchor for tail truncation
v = audit.verify(expect_at_least=5)      # → ok=False + "tail truncation detected" if < 5

Known limitations 明示化 (DESIGN.md § 追加)

「audit chain が verify PASS」 の 意味を 利用者が 「chain が 完全 (complete)」 と 誤読すると、 refutation machine が 自分自身に対して もっともらしさを 発する 状態 = 「絶対に嘘をつかない」 core promise の 直接違反。 hash chain の 構造的限界 を 型 level では 完全には 防げないが、 documentation + opt-in mitigation で 「利用者が 認識した上で 選択できる」 状態を 提供する = 反証機械 discipline の 適用対象。

3 mitigation options:

• (a) `expect_at_least=N` opt-in parameter (0.1.0a3 実装済、 最軽量 external anchor)
• (b) 最終 hash を 別媒体 に 記録 + 突合 (application layer、 未提供)
• (c) 末尾 seal entry pattern (application layer、 未提供)

反証機械 arc 累計 (2026-08-19 3 release cycle 反映後)

• repo commits: 10 (a1 initial 7 + a2 mismatch fix + a2 findings fix + a3 mitigation)
• 累計 test: 198 → 203 → 209 PASS (skeleton 48 + MCP 30 + refute 22 + search 37 + breakpoint 33 + hold 39)
• PyPI releases: 3 (全 Sigstore attestation via Trusted Publisher OIDC)
• GitHub Issues: 1 open (#1 findings ④)

15. 関連 memory + reference

• STEP 1345 benchtop-mcp v0.5.0-alpha spike (2026-08-19 同日、 Rei stack MCP hardening arc)
• [[project-rei-automator-mcp-v020a2-a3-arc-2026-08-18]] (AuditChain 由来 STEP 1340 pattern + tag auto-fire 事故 の 直接 predecessor)
• [[feedback-ai-usable-tool-design-5-conditions-2026-08-18]] (chat-Claude 5 条件、 operational 4 例目 = rei-verify)
• [[feedback-zero-sorry-floor-not-ceiling]] (CONFIRMED verdict 意味の 起源)
• [[feedback-one-reproduction-over-ten-unverified]] (marker invariant 由来)
• [[feedback-world-uniqueness-claim-controllable]] (novelty 主張 ゼロ discipline)
• [[feedback-projection-self-audit-pattern]] (SAC-4 28 例目)
• STEP 1276 (judgmentStatus 4 値 = Verdict 4 値 の 直接対応)
• STEP 1340 (AuditLogWriter = AuditChain の 汎用抽出元)
• IUT arc 2026-08-06 (HOLDING の 12 年 discipline、 4-value verdict の 型化 直接動機)