#!/usr/bin/env python3
"""Independent analytic certificate for Lemmas 2.1 and 2.2.

The finite property test in the original reproduction could only establish a
toy version of Claim 5.  This script records the exact measure-zero argument,
checks its finite combinatorial reduction with rational arithmetic, and runs
destructive controls for the assumptions that make the lemmas true.
"""

from __future__ import annotations

import hashlib
import itertools
import json
import platform
import time
from fractions import Fraction
from pathlib import Path


ROOT = Path(__file__).resolve().parent
OUT = ROOT / "claim5_analytic_evidence"
PAPER_TEX = ROOT / "source_arxiv_2508.09628" / "main.tex"
PAPER_TAR = ROOT / "source_arxiv_2508.09628.tar"


def sha256(path: Path) -> str:
    h = hashlib.sha256()
    with path.open("rb") as handle:
        for block in iter(lambda: handle.read(1 << 20), b""):
            h.update(block)
    return h.hexdigest()


def update_matrix(leaders: tuple[int, ...], gamma: Fraction):
    """Return L with y_i=(1-gamma)x_i+gamma*x_{leaders[i]}."""
    n = len(leaders)
    matrix = [[Fraction(0) for _ in range(n)] for _ in range(n)]
    for i, leader in enumerate(leaders):
        matrix[i][i] += 1 - gamma
        matrix[i][leader] += gamma
    return matrix


def outer_zero_symmetric(a, b) -> bool:
    """Whether a b^T+b a^T is exactly zero."""
    n = len(a)
    return all(a[p] * b[q] + b[p] * a[q] == 0 for p in range(n) for q in range(n))


def outer_zero_skew(a, b) -> bool:
    """Whether a b^T-b a^T is exactly zero."""
    n = len(a)
    return all(a[p] * b[q] - b[p] * a[q] == 0 for p in range(n) for q in range(n))


def exact_combinatorial_audit() -> dict:
    gammas = [Fraction(1, 3), Fraction(1, 2), Fraction(2, 3)]
    maps = 0
    row_checks = 0
    candidate_pair_checks = 0
    symmetric_identity_only_when_same = True
    skew_identity_only_when_same = True
    for n in range(2, 6):
        for leaders in itertools.product(range(n), repeat=n):
            for gamma in gammas:
                maps += 1
                matrix = update_matrix(leaders, gamma)
                for row in matrix:
                    row_checks += 1
                    assert all(value >= 0 for value in row)
                    assert sum(row) == 1
                for query in range(n):
                    a = matrix[query]
                    for j in range(n):
                        for k in range(j + 1, n):
                            b = [matrix[j][q] - matrix[k][q] for q in range(n)]
                            assert sum(a) == 1
                            assert sum(b) == 0
                            candidate_pair_checks += 1
                            same_candidate_map = all(value == 0 for value in b)
                            if outer_zero_symmetric(a, b) and not same_candidate_map:
                                symmetric_identity_only_when_same = False
                            if outer_zero_skew(a, b) and not same_candidate_map:
                                skew_identity_only_when_same = False
    assert symmetric_identity_only_when_same
    assert skew_identity_only_when_same
    return {
        "n_values": [2, 3, 4, 5],
        "gamma_values": ["1/3", "1/2", "2/3"],
        "functional_leader_maps_times_gamma": maps,
        "row_stochasticity_checks": row_checks,
        "exact_query_candidate_pair_checks": candidate_pair_checks,
        "symmetric_part_identity_implies_same_candidate_map":
            symmetric_identity_only_when_same,
        "skew_part_identity_implies_same_candidate_map":
            skew_identity_only_when_same,
        "arithmetic": "fractions.Fraction; no floating-point comparisons",
    }


def destructive_controls() -> dict:
    # Invertibility is necessary for a generic singleton statement.
    points = [-1, 2]
    zero_b_scores = [[0 * x * y for y in points] for x in points]
    zero_b_top_multiplicity = [
        sum(score == max(row) for score in row) for row in zero_b_scores
    ]

    # Scalar gamma outside [0,1] is no longer a convex combination.
    gamma = Fraction(6, 5)
    scalar_outside = (1 - gamma) * Fraction(0) + gamma * Fraction(1)

    # Paper Remark 2.3: coordinate-wise convexity does not imply membership in
    # a non-axis-aligned convex hull.  Unit triangle is x>=0,y>=0,x+y<=1.
    x = (Fraction(1), Fraction(0))
    leader = (Fraction(0), Fraction(1))
    coordinate_gamma = (Fraction(3, 5), Fraction(7, 10))
    matrix_step = (
        x[0] + coordinate_gamma[0] * (leader[0] - x[0]),
        x[1] + coordinate_gamma[1] * (leader[1] - x[1]),
    )
    return {
        "singular_B_control": {
            "B": 0,
            "points": points,
            "top_multiplicity": zero_b_top_multiplicity,
            "distinct_argmax_not_singleton": all(v == 2 for v in zero_b_top_multiplicity),
        },
        "gamma_outside_convex_range_control": {
            "gamma": "6/5",
            "old_hull": "[0,1]",
            "updated_point": str(scalar_outside),
            "outside_old_hull": scalar_outside > 1,
        },
        "matrix_valued_step_control": {
            "old_hull": "conv{(0,0),(1,0),(0,1)}",
            "coordinate_step": ["3/5", "7/10"],
            "updated_point": [str(value) for value in matrix_step],
            "coordinate_sum": str(sum(matrix_step)),
            "outside_old_hull": sum(matrix_step) > 1,
        },
    }


def proof_certificate() -> dict:
    return {
        "lemma_2_1": {
            "statement": (
                "For invertible B^t, for Lebesgue-almost-every initial "
                "configuration the hardmax set is a singleton for every "
                "particle and every finite integer time."
            ),
            "independent_steps": [
                (
                    "Fix a finite leader history through time t. Each current "
                    "token is A_i X^0, where A_i is a nonnegative coefficient "
                    "row summing to one, because every update is a scalar "
                    "convex combination."
                ),
                (
                    "A tie for query i between distinct candidate maps j,k is "
                    "Q(X^0)=<B^t A_i X^0,(A_j-A_k)X^0>=0. Let a=A_i and "
                    "b=A_j-A_k; then sum(a)=1 and sum(b)=0."
                ),
                (
                    "If the symmetric part of B^t is nonzero and Q were the "
                    "zero polynomial, diagonal coefficients force a_p b_p=0; "
                    "cross coefficients then force b=0. If B^t is "
                    "skew-symmetric, zero polynomial coefficients force "
                    "a_p b_q=a_q b_p, so b=c a; the row sums give c=0. Thus "
                    "Q is nonzero whenever the candidate maps are distinct."
                ),
                (
                    "The zero set of a nonzero real polynomial has Lebesgue "
                    "measure zero. There are finitely many leader histories, "
                    "queries and candidate pairs at fixed t, and countably "
                    "many integer times. Finite and countable unions preserve "
                    "measure zero. If b=0, the candidate positions coincide "
                    "identically and represent one element of the set, not a "
                    "distinct tie."
                ),
            ],
            "logical_dependencies": [
                "finite token count",
                "invertible (hence nonzero) B^t",
                "scalar gamma^t in (0,1)",
                "discrete times t in nonnegative integers",
            ],
            "decision": "verified_by_independent_measure_zero_proof",
        },
        "lemma_2_2": {
            "statement": "K^{t+1} is a subset of K^t for gamma^t in (0,1).",
            "independent_steps": [
                (
                    "The selected leader y_i^t belongs to K^t. Therefore "
                    "x_i^{t+1}=(1-gamma^t)x_i^t+gamma^t y_i^t belongs to K^t "
                    "by convexity."
                ),
                (
                    "K^{t+1} is the convex hull of points x_i^{t+1}, all of "
                    "which lie in K^t. Since K^t is convex, their entire convex "
                    "hull is contained in K^t."
                ),
            ],
            "decision": "verified_by_direct_convexity_proof",
        },
    }


def markdown_report(payload: dict) -> str:
    audit = payload["exact_combinatorial_audit"]
    controls = payload["destructive_controls"]
    return f"""# Claim 5 analytic certificate

Decision: **verified** by an independent measure-zero proof and a direct
convexity proof.

The all-time singleton statement is reduced, on each finite leader history, to
the zero set of a nonzero quadratic polynomial.  The coefficient argument uses
only `sum(a)=1`, `sum(b)=0`, and invertibility of the key-query matrix.  A
finite union covers each time and a countable union covers all integer times.

Lemma 2.2 follows immediately because every new token is a scalar convex
combination of two points in the old hull.

The rational-arithmetic audit checked {audit['functional_leader_maps_times_gamma']:,}
leader-map/step-size combinations, {audit['row_stochasticity_checks']:,}
row invariants, and {audit['exact_query_candidate_pair_checks']:,} exact
query/candidate coefficient systems.  It found no case where the tie
polynomial vanished identically for distinct candidate maps.

Destructive controls passed:

- Singular `B=0` produced multiplicity
  {controls['singular_B_control']['top_multiplicity']}.
- `gamma=6/5` moved 0 toward 1 to
  {controls['gamma_outside_convex_range_control']['updated_point']}, outside
  `[0,1]`.
- The coordinate-wise matrix step produced
  {controls['matrix_valued_step_control']['updated_point']} with coordinate
  sum {controls['matrix_valued_step_control']['coordinate_sum']}, outside the
  unit triangle.
"""


def main() -> None:
    started = time.perf_counter()
    OUT.mkdir(exist_ok=True)
    payload = {
        "paper": {
            "submission_number": 8097,
            "openreview_id": "zrn7rRuvhW",
            "arxiv": "2508.09628",
            "source_tar_sha256": sha256(PAPER_TAR),
            "main_tex_sha256": sha256(PAPER_TEX),
            "source_lines": {
                "lemma_2_1": "main.tex:285-306",
                "lemma_2_2": "main.tex:346-355",
            },
        },
        "proof_certificate": proof_certificate(),
        "exact_combinatorial_audit": exact_combinatorial_audit(),
        "destructive_controls": destructive_controls(),
        "environment": {
            "python": platform.python_version(),
            "platform": platform.platform(),
        },
    }
    payload["runtime_seconds"] = time.perf_counter() - started
    certificate = OUT / "certificate.json"
    report = OUT / "PROOF.md"
    certificate.write_text(json.dumps(payload, indent=2, sort_keys=True) + "\n")
    report.write_text(markdown_report(payload))
    files = [certificate, report, ROOT / "claim5_analytic_certificate.py"]
    (OUT / "SHA256SUMS").write_text(
        "".join(f"{sha256(path)}  {path.relative_to(ROOT)}\n" for path in files)
    )
    print(json.dumps(payload, indent=2, sort_keys=True))


if __name__ == "__main__":
    main()