#!/usr/bin/env python3 """Exact Proposition 5.1 certificate for On Structured State-Space Duality. This is not a reduced analogue. It constructs a literal two-state, non-diagonal linear SSM whose causal kernel is M = I_T + e_T e_1^T. For a width-N 1-semiseparable masked-attention dual, the nonzero (T, 1) entry forces every causal-mask transition on the path 1 -> T to be nonzero. The leading (T-1)-by-(T-1) score block has every entry strictly below its diagonal equal to zero and every diagonal entry nonzero. It is therefore upper triangular with rank T-1. Taking N=2 and T>=4 contradicts rank(Q K^T) <= N. All recurrence calculations use exact Python integers. No tolerance, random seed, fitted model, or source implementation is involved. """ from __future__ import annotations import argparse import csv import hashlib import json from pathlib import Path Matrix = list[list[int]] Vector = list[int] def matmul(left: Matrix, right: Matrix) -> Matrix: return [ [sum(left[i][k] * right[k][j] for k in range(len(right))) for j in range(len(right[0]))] for i in range(len(left)) ] def matvec(matrix: Matrix, vector: Vector) -> Vector: return [sum(row[j] * vector[j] for j in range(len(vector))) for row in matrix] def dot(left: Vector, right: Vector) -> int: return sum(x * y for x, y in zip(left, right, strict=True)) def build_parameters(length: int) -> tuple[list[Matrix], list[Vector], list[Vector]]: """Return an explicit non-diagonal rank-one SSM of state width two. We start from D=diag(1,0), then conjugate by S=[[1,1],[0,1]]. Thus every used transition is A=S D S^-1=[[1,-1],[0,0]], which is non-diagonal and rank one. Input/output vectors are transformed by b'=S b and c'=S^-T c. """ if length < 4: raise ValueError("length must be at least 4 for T-1 > state width 2") transition = [[1, -1], [0, 0]] transitions = [[[1, 0], [0, 1]]] + [transition for _ in range(length - 1)] inputs = [[1, 0]] + [[1, 1] for _ in range(length - 1)] outputs = [[1, -1]] outputs += [[0, 1] for _ in range(length - 2)] outputs += [[1, 0]] return transitions, inputs, outputs def recurrence_kernel( transitions: list[Matrix], inputs: list[Vector], outputs: list[Vector] ) -> Matrix: """Materialize M[t,s]=c_t^T A_t ... A_{s+1} b_s exactly.""" length = len(inputs) kernel = [[0 for _ in range(length)] for _ in range(length)] for source in range(length): state = inputs[source] kernel[source][source] = dot(outputs[source], state) for target in range(source + 1, length): state = matvec(transitions[target], state) kernel[target][source] = dot(outputs[target], state) return kernel def expected_kernel(length: int) -> Matrix: matrix = [[int(i == j) for j in range(length)] for i in range(length)] matrix[-1][0] = 1 return matrix def exact_rank(matrix: Matrix) -> int: """Fraction-free Gaussian elimination over the integers.""" work = [row[:] for row in matrix] rows, columns = len(work), len(work[0]) rank = 0 for column in range(columns): pivot = next((r for r in range(rank, rows) if work[r][column] != 0), None) if pivot is None: continue work[rank], work[pivot] = work[pivot], work[rank] pivot_value = work[rank][column] for row in range(rank + 1, rows): if work[row][column] == 0: continue factor = work[row][column] work[row] = [ pivot_value * work[row][j] - factor * work[rank][j] for j in range(columns) ] rank += 1 if rank == rows: break return rank def sha256(path: Path) -> str: digest = hashlib.sha256() with path.open("rb") as handle: for chunk in iter(lambda: handle.read(1 << 20), b""): digest.update(chunk) return digest.hexdigest() def run_case(length: int) -> dict: transitions, inputs, outputs = build_parameters(length) observed = recurrence_kernel(transitions, inputs, outputs) expected = expected_kernel(length) exact_match = observed == expected transition = transitions[1] transition_rank = exact_rank(transition) transition_is_non_diagonal = transition[0][1] != 0 or transition[1][0] != 0 off_target_nonzero = sum( int(observed[i][j] != 0 and not (i == j or (i == length - 1 and j == 0))) for i in range(length) for j in range(length) ) state_width = 2 required_score_rank = length - 1 contradiction_margin = required_score_rank - state_width impossible = exact_match and required_score_rank > state_width # Destructive control: remove the wraparound entry. I_T then has an # explicit width-one dual: L=I (zero transition factors), Q=K=1. control_kernel = [[int(i == j) for j in range(length)] for i in range(length)] control_mask = [[int(i == j) for j in range(length)] for i in range(length)] control_scores = [[1 for _ in range(length)] for _ in range(length)] control_product = [ [control_mask[i][j] * control_scores[i][j] for j in range(length)] for i in range(length) ] return { "T": length, "state_width_N": state_width, "transition_matrix": transition, "transition_exact_rank": transition_rank, "transition_is_non_diagonal": transition_is_non_diagonal, "kernel_exactly_I_plus_eT_e1T": exact_match, "off_target_nonzero_entries": off_target_nonzero, "required_attention_score_rank_lower_bound": required_score_rank, "attention_score_rank_upper_bound": state_width, "rank_contradiction_margin": contradiction_margin, "width_N_1SS_attention_dual_impossible": impossible, "destructive_control_I_has_width_1_dual": control_product == control_kernel, } def main() -> None: parser = argparse.ArgumentParser() parser.add_argument("--output-dir", type=Path, required=True) args = parser.parse_args() args.output_dir.mkdir(parents=True, exist_ok=True) lengths = [4, 8, 16, 32, 64] cases = [run_case(length) for length in lengths] result = { "schema_version": 1, "paper_id": "DKathyl3XN", "paper_arxiv": "2510.04944v1", "registered_claim_index": 5, "source_location": "Section 5, Proposition 5.1, pages 15-16", "object": "literal two-state non-diagonal SSM and width-matched 1-SS masked-attention dual", "arithmetic": "exact Python integers", "proof_certificate": { "kernel": "M = I_T + e_T e_1^T", "path_argument": "M[T,1] != 0 forces every 1-SS mask factor a_2,...,a_T to be nonzero", "minor_argument": "the leading (T-1)x(T-1) score minor is upper triangular with nonzero diagonal", "rank_lower_bound": "rank(QK^T) >= T-1", "rank_upper_bound": "rank(QK^T) <= N", "contradiction": "T-1 > N for N=2 and every tested T>=4", }, "cases": cases, "all_literal_kernels_exact": all(c["kernel_exactly_I_plus_eT_e1T"] for c in cases), "all_transitions_non_diagonal_rank_one": all( c["transition_is_non_diagonal"] and c["transition_exact_rank"] == 1 for c in cases ), "all_width_matched_duals_ruled_out": all( c["width_N_1SS_attention_dual_impossible"] for c in cases ), "all_destructive_controls_pass": all( c["destructive_control_I_has_width_1_dual"] for c in cases ), } json_path = args.output_dir / "claim5_non_diagonal_witness_results.json" json_path.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") csv_path = args.output_dir / "claim5_non_diagonal_witness_cases.csv" with csv_path.open("w", newline="") as handle: fields = [ "T", "state_width_N", "transition_exact_rank", "transition_is_non_diagonal", "kernel_exactly_I_plus_eT_e1T", "off_target_nonzero_entries", "required_attention_score_rank_lower_bound", "attention_score_rank_upper_bound", "rank_contradiction_margin", "width_N_1SS_attention_dual_impossible", "destructive_control_I_has_width_1_dual", ] writer = csv.DictWriter(handle, fieldnames=fields) writer.writeheader() for case in cases: writer.writerow({key: case[key] for key in fields}) manifest_path = args.output_dir / "OUTPUT_SHA256SUMS.txt" manifest_path.write_text( "".join(f"{sha256(path)} {path.name}\n" for path in (csv_path, json_path)) ) print(json.dumps({ "all_literal_kernels_exact": result["all_literal_kernels_exact"], "all_transitions_non_diagonal_rank_one": result["all_transitions_non_diagonal_rank_one"], "all_width_matched_duals_ruled_out": result["all_width_matched_duals_ruled_out"], "all_destructive_controls_pass": result["all_destructive_controls_pass"], "output_manifest_sha256": sha256(manifest_path), }, sort_keys=True)) if __name__ == "__main__": main()