hamming_distance_gate tool v0.1

STEP: 1507 / 公開日: 2026-08-28 / Test: 35/35 PASS / Lean 4: 13 theorem zero sorry / Type: STEP 1493 情報科学 arc candidate #2 実装

短答 (3 行)

1. 決定表 (first-match priority)

2. 使用例 (TS)

import { hammingDistanceGate } from './src/mcp/hamming-distance-gate';

// A: identical → TRUE
const rA = hammingDistanceGate({ a: [1,0,1,0], b: [1,0,1,0] });
// { verdict: 'TRUE', reason: 'identical', distance: 0, length: 4, ... }

// B: 1-bit flip, threshold=1 → TRUE (correctable)
const rB = hammingDistanceGate({ a: [1,0,1,0], b: [1,1,1,0] });
// { verdict: 'TRUE', reason: 'correctable', distance: 1, ... }

// C: 2-bit flip, threshold=1 → NEITHER (detection only)
const rC = hammingDistanceGate({ a: [1,0,1,0], b: [1,1,0,0] });
// { verdict: 'NEITHER', reason: 'detection_only', distance: 2, ... }

// D: 3-bit flip, threshold=1 → FALSE (uncorrectable)
const rD = hammingDistanceGate({ a: [1,0,1,0], b: [0,1,0,0] });
// { verdict: 'FALSE', reason: 'uncorrectable', distance: 3, ... }

// E: custom threshold=2 (double-bit correction)
const rE = hammingDistanceGate({
  a: [1,0,1,0], b: [1,1,0,0], correctionThreshold: 2
});
// { verdict: 'TRUE', reason: 'correctable', distance: 2, ... }

3. Lean 4 formalization (13 theorem zero sorry)

-- Hamming 距離 定義 (STEP 1493 継承、 disjoint patterns)
hd_self_zero            : ∀ xs, hamming_dist xs xs = 0
hd_single_diff          : hamming_dist [1] [0] = 1

-- verdict 決定表 (★核 4 theorem)
verdict_identical_gives_true      : d=0 → TRUE
verdict_correctable_gives_true    : d≤threshold, d>0 → TRUE
verdict_detection_gives_neither   : d=threshold+1 → NEITHER
verdict_uncorrectable_gives_false : d>threshold+1 → FALSE

-- threshold=1 specialization (single-bit correction)
verdict_d0_t1_true / d1_t1_true / d2_t1_neither / d3_t1_false

-- threshold=0 specialization (strict identical only)
verdict_d0_t0_true / d1_t0_neither / d2_t0_false

4. Test coverage (35/35 PASS)

実行: npx tsx test/step1507-hamming-distance-gate-test.ts

5. STEP 1479 par2 recovery evidence との 対応

STEP 1479 (2026-08-27) で 「par2cmdline-turbo 1.1.1 で 1116 blocks 中 1 byte 破損 injection → repair で md5 完全一致復元」 を 実測。 本 tool は その 抽象化 identity:

• par2 redundancy 10% = correctionThreshold ~10% length 対応
• 1 byte 破損 = Hamming distance 1-8 bit (境界)
• 復元成功 = TRUE (correctable) verdict と 対応

本 tool は 実測 evidence の 静的 identity 層、 実 recovery は par2 layer に 委譲。

6. Rei stack 姉妹 tool 群 (更新)

6 tool 揃った ことで 「1 値 / 2 値比較 / 多試行 / 分布 / ゲーム / 誤り訂正」 の 6 側面 D-FUMT₈ verdict 化 core 拡張。

7. Honest scope