code/claim5_non_diagonal_witness.py

#!/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()