X01 統合版1.2「確認依頼」への回答

T = Σ_I (x_i−u)(1−x_i) + Σ_J (v−x_j)x_j の各項は、各側の極値の定義と箱制約だけで非負（u ≥ v 不要）。σ = 1−u+A, ρ = v+B, e = u+v−1+B−A を代入して多項式部分が 2w−w²+(w−1)²−1 = 0（w = u+v）で消え、残りが 2T+2(1−v)A+2uB+(B−A)² になることを再展開した。Lean 側 rank_gap_core の hid はこの恒等式で、finite_rank_gap は I, J の非交差すら要求しない。

等号：g>0 なら u ≥ g（v ≥ 0）、1−v ≥ g（u ≤ 1）、よって R ≥ 2g(A+B)、R=0 ⇒ A=B=0。分割が任意でも等号なら自動的に I は上位集合になる。安定性 (3) と「他を端点に置くと総和が A−B 動く」注記も正しい。

平方根型に u ≥ v が必要な理由（符号付き g_I の平方から正値は出ない）は本文の通り。rank_gap_partition_sqrt の仮定 hab と一致。

端点：η=0 で第1枝は δ=0 のみ、値 1、第2枝は √(1−2δ)（(17) と一致）。η=1/2 で δ₀=1/4 にて両枝 1/2、δ_c=3/8 にて 0。一般に δ₀ で両枝 1−η、δ_c で 0。第1枝の下界は 1−2δ−b² = (1−b)²、第2枝の箱制約 (1−η−h)/2 ≥ 0 ⟺ δ ≥ δ₀。

Lean 候補：band_small_lower の要は ((1+t)/2)² = (1+t)/2 − δ = 1−2δ−b²（t=√(1−4δ), b=(1−t)/2）で、a ≤ b は √(1−4δ) ≤ 1−2a ⟺ a(1−a) ≤ δ から。band_gap_witness の3枝は本文の達成配置と同じ。finite_band_attainment は (1^p, u, v, 0^q) で |S−(p+1)| = |u+v−1| = a、v ≤ u より整列後の g_{p+1} = u−v。有限ベクトル → 分割形の量化は finite_band_gap が rank_gap_partition と abs_integer_offset_defect（k=|I|）を band_gap_lower に渡す形で閉じている。

(9)：座標 1/2 があれば残りの総和 s−1/2+e、|e| ≤ 1/2 で端数の欠損は (1/2+e)(1/2−e)、合わせて D ≥ 1/2−e²。達成配置 (1^{s−1}, 1/2, 1/2−η, 0…) は S=s−η, D=1/2−η²。厳密不等号の必要性：この配置に round01（t>1/2 で 1）を当てると 1 の数は s−1 なので、等号を許すと個数の主張も落ちる。

Rounding.lean の位相非依存証明を追った：|x_i − round(x_i)| = min(x_i,1−x_i) ≤ 2x_i(1−x_i) より σ+ρ ≤ 2D < 1−2η²；個数が s でなければ片側の誤差質量 ≥ 1−η；その側の成分は [0,1/2] なので half_bounded_mass_defect（尺度2倍の integer_offset_defect, k=1：Σd² ≤ m²−m+1/2、よって欠損 ≥ 1/2−(1−m)² ≥ 1/2−η²）と矛盾。同値なしは no_half_below_barrier。L1一意性 round01_l1_unique は各項の不等式が等号になることから従う。

T7 の仮定は「コンパクト凸多面体 P、P で相対開な凸集合 U」。T6 では U_E = {Q < M−E} ∩ H_S（Q 凸の劣位集合、開）、T9 では {D > δ} ∩ P（D 凹の優位集合、開）で満たされる。T7 の証明で確認した点：U∩F ≠ ∅ なら U∩relint F ≠ ∅（相対開性）；半径方向線分が U に再入しない（凸性）；面同士の交わりは境界にあるので (13) を恒等写像と貼り合わせられる；K は全過程で固定；処理順は次元降順で、同次元の面は境界でしか交わらない。

T8 では「Ω_E が X_E へも K_E へも強変形収縮する」と「X_E が K_E へ収縮する」を区別している（K_E ⊄ X_E）。(12) の放射収縮は ‖x−c‖ ≥ R_E を保ち H_S 内に留まる。E=E_max を別扱いにしているのも正しい。

頂点：帯境界が非活性なら箱頂点で総和 s のみ（s±η は (s−1,s+1) の内側）。活性なら n−1 座標が 0/1、残りは s−η−j ∈ (0,1) ⇒ j=s−1、値 a；s+η−j ∈ (0,1) ⇒ j=s、値 η。個数 n·C(n−1,s−1) = s·C(n,s), n·C(n−1,s) = (n−s)·C(n,s)。

辺：箱辺は j=s−1（t ∈ [a,1]）と j=s（t ∈ [0,η]）だけ。両端が帯で切られる箱辺は η>1/2 のとき存在しない（s+η−1 < j < s−η に整数なし）。帯面の辺は下側 j=s−1（和 a）, j=s−2（和 1+a）、上側 j=s（和 η）, j=s−1（和 1+η）。二座標の和 t の中点値 t−t²/2 は順に c, d, d, c。B–B 辺は存在しない（二値頂点は2座標以上異なり、帯境界上にない）。

閾値：c−k=(1−η)²/2, h−k=(η−1/2)², d−c=(2η−1)/2 > 0, d−h=(4η−2η²−1)/4 > 0（根 1±1/√2 の間）。c=h ⟺ η²=1/2。

成分数：各 L/U 頂点は箱辺でただ一つの B につく；下側短辺は 1 の位置集合（大きさ s−1）を共有する L 同士、上側短辺は正の位置集合（大きさ s+1）を共有する U 同士を結ぶ；δ ≥ max(c,h) で「箱辺→下側短辺→箱辺」による一要素交換。端：s=1 で下側長辺、s=n−1 で上側長辺が消えるが数え上げに影響しない。等号の扱い（閾値では変化後の値）は「面全体が許容」の定義と整合。

グラフ補題：T7 で K に強変形収縮し、K の各面は連結で自分の辺を含むので、成分数は許容頂点＋全体許容辺のグラフに等しい。

数値：check_wide_eta.py（辺を活性制約の階数で独立検出）と check_eta_classification.py を再実行、PASS、JSON 同一。独立の格子計算：n=2, s=1, η=0.9 で δ=0.1, 0.2, 0.26 に 4, 4, 1；n=3, s=1 と s=2, η=0.9 で δ=0.05, 0.092, 0.2, 0.3 に 3, 12, 7, 1；n=3, s=1, η=0.6（h<c の側）で δ=0.2, 0.245, 0.28 に 3, 12, 3。すべて T9 と一致。

数学：なし。

注記の提案（2点）：(a) δ=k ちょうどでは L, U 頂点は F_δ の孤立点になる。L で ∇D = (1−2x_i) を許容方向 d（1 の座標は減少のみ、0 の座標は増加のみ、Σd ≥ 0）と内積すると 2Σ_{ones}|d_i| + (2−2η)|d_a| > 0 なので、すべての許容方向で D が一次で増える。図 3 で新しい島が「点として生まれる」ことの説明になる。(b) 格子計算の読み方：閾値の直上では許容領域が細い帯状になり、格子では分断されて過大な成分数が出る（例：n=2, η=0.6, δ=0.245 で格子 3000×3000 が 10 を返すが、真値は 6。余分の 4 は各 L/U 島の先端の孤立格子点）。図や検算スクリプトの注記に「閾値近傍の格子値は信頼しない」と書いておくと安全。

直接証明の各行を確認：min(x,1−x) ≤ 2x(1−x)；整数差が 1 未満なら 0；同値があれば二つの丸めが同じ総和を持ち矛盾；D ≥ 2ρ(1−ρ)；(16)(17)。s=1 の還元 g_1² ≥ 2Q−S²（非負性のみで可、p_{(2)} ≤ 1−p_{(1)}）、s=n−1 の補数、m=0 の √(r²−2E)。「先行性をなお調べる範囲」の絞り込み n ≥ 4, 2 ≤ s ≤ n−2, S ∉ ℤ も整合。

Rosenberg–Jakobsson (2008, Genetics 179:2027) の実在と、ホモ接合度（二乗和）から最大対立遺伝子頻度の上下限を与える論文であることは PMC の抄録で確認した。Theorem 1(ii) の式 (17) そのものは原文未読。Gorban §4.2・Fig.4.5 と Rubensson–Niklasson §5.1 の式は未確認。前回私が「記憶ベース」と断った Rubensson–Rudberg–Sałek 2008 が概要のみの照合に留まっていることも、記述と整合。

手で追った要点。integer_offset_defect：F(S,D,k) = D−(S−k)(1−(S−k)) に対し F(S+t, D+t(1−t), k) = (1−t)F(S,D,k) + tF(S,D,k−1)（展開して両辺 D−y+y²+2ty、y=S−k）、空列で k(k+1) ≥ 0。床関数を使わない帰納で、本文 (4) の全整数版になっている。half_coordinate_defect：残りに k−1 を当てて 1/4−e²。half_bounded_mass_defect：上記の通り。BandSharp：項目2。robust_total_rounding：項目3。round01_l1_unique：項目3。33宣言すべての陳述が本文の T1・T2・T4（および §9 の (16)）と対応し、仮定の過不足はない。algebra_check.py を再実行、13恒等式 PASS。4ファイルの SHA-256 は run-results/verification.json の記載と一致、zip 内の写しとも同一。

コンパイルで引っかかりうる箇所（確認できていない、いずれも数学ではなくタクティクの問題）：

• pairPadded_sum の simp [pairPadded, Fintype.sum_sum_type] <;> ring：Fin p 上の定数和のキャスト形（Finset.card_univ, Fintype.card_fin, nsmul_eq_mul）が simp 後に残ると ring で閉じない可能性。
• round01 をタクティクブロックで定義しているため、rw [round01, if_pos …] が展開できない可能性（unfold round01 か simp only [round01] の方が堅い）。Real の < の決定性は classical で問題ないはず。
• FiniteBand.lean の import Mathlib（全体）は lake exe cache get が前提。他ファイルと揃えて必要モジュールだけにする方が再現性が高い。
• API 名（Real.sqrt_le_left, sq_le_sq₀, Int.cast_natCast, Fintype.sum_sum_type, Finset.sum_erase_add）は 2025 年時点の Mathlib に存在するはず。retry-record の API 照合と同じ範囲で、私も記憶ベース。
• verify.py は Audit.lean を自動生成するので、BandSharp に #print axioms が2件しかないことは合否に影響しない。static_audit の theorem_count: 47 は「宣言数」であり「検証済み数」と読まれないよう、キー名を declared_theorems にすると誤読を防げる。

1/2 ≤ η < 1、|S−s| ≤ η とする。(i) D < η(1−η) = k なら最近0/1丸めの 1 の数は s。(ii) D < 1/4 = h なら座標 1/2 はない。いずれも鋭い：(i) は (1^{s−1}, 1−η, 0^{n−s})（T9 の L 頂点、S=s−η, D=k, 1 の数 s−1）、(ii) は (1^{s−1}, 1/2, 0^{n−s})（S=s−1/2 は帯内、D=1/4）。η ≤ 1/2 の 1/2−η² と η=1/2 で連続に接続する（両方 1/4）。

(i) 個数が s でなければ片側の誤差質量 m ≥ 1−η（Rounding.lean の hmass の議論そのまま）で、その側の成分は [0,1/2]。m ≤ 1/2 なら integer_offset_defect（k=0）で欠損 ≥ m(1−m) ≥ (1−η)η（t(1−t) は [0,1/2] で増加、1−η ≤ m）。m > 1/2 なら half_bounded_mass_defect で欠損 ≥ 1/2−(1−m)² > 1/4 > k。(ii) は座標 1/2 が単独で 1/4 を寄与する。

読み方：η>1/2 では「最近丸めが個数を誤る最初の点」が T9 で島として生まれる L/U 頂点そのものであり、「同値が生じる最初の点」が箱辺の中点。T4 と T9 が同じ閾値 k, h を共有する。