evidence/code/verify_claim5.py

"""Primary machine-checkable contract for Claim 5."""

from __future__ import annotations

import json
import math
import sys
from pathlib import Path


EXPECTED_JAW_SHA256 = (
    "5c58e2c84797bf06ff18291b692e4a62"
    "fc3e39f67212a93429a6dfa15e2b5d5e"
)


def evaluate(record: dict) -> dict:
    failures: list[str] = []
    source = record["jaw_source"]
    mesh = record["mesh"]
    voxels = record["voxelization"]
    diffusion = record["diffusion"]
    modalities = record["cross_modalities"]

    if source["sha256"] != EXPECTED_JAW_SHA256:
        failures.append("jaw source SHA-256")
    if source["commit"] != "e1f8cef196adb29149a2193ffb0cb05dab631420":
        failures.append("jaw source commit")
    if source["dataset_paper_doi"] != "10.1016/j.dental.2021.01.009":
        failures.append("jaw source peer-reviewed provenance")
    if mesh["format"] != "ASCII STL" or mesh["triangle_count"] < 40_000:
        failures.append("full anatomical jaw mesh")
    if voxels["representation"] != "sparse regular-grid surface voxels":
        failures.append("sparse voxel representation")
    if voxels["nonempty_voxels"] < 1_000:
        failures.append("jaw voxel scale")
    if not (0.0 < voxels["occupancy_fraction"] < 0.25):
        failures.append("jaw grid sparsity")
    if min(voxels["index_extent"]) < 10:
        failures.append("jaw three-dimensional extent")
    if voxels["largest_6_connected_component_fraction"] < 0.75:
        failures.append("jaw voxel connectivity")

    point = modalities["point_cloud"]
    gmm = modalities["covariance_aware_gmm"]
    armadillo_voxels = modalities["sparse_armadillo_voxels"]
    if point["count"] != 5_000:
        failures.append("paper-scale point cloud")
    if gmm["count"] != 500:
        failures.append("paper-scale GMM")
    if gmm.get("kernel") != "Eq.6 covariance-aware Gaussian overlap":
        failures.append("Eq.6 covariance-aware GMM kernel")
    if (
        gmm.get("covariance_matrices") != 500
        or gmm.get("covariance_dimension") != 3
        or gmm.get("minimum_covariance_eigenvalue", 0.0) <= 0.0
    ):
        failures.append("positive full GMM covariances")
    if (
        armadillo_voxels.get("edge") != 0.05
        or armadillo_voxels.get("nonempty_voxels", 0) < 100
    ):
        failures.append("paper-scale sparse Armadillo voxels")

    for name, modality in (
        ("point", point),
        ("gmm", gmm),
        ("voxel", armadillo_voxels),
    ):
        eigenvalues = modality["diffusion_eigenvalues"]
        if not math.isclose(eigenvalues[0], 1.0, abs_tol=2e-8):
            failures.append(f"{name} leading diffusion eigenvalue")
        if min(eigenvalues) < -2e-8 or max(eigenvalues) > 1.0 + 2e-8:
            failures.append(f"{name} diffusion damping")

    if diffusion["normalization"] != "symmetric Sinkhorn":
        failures.append("jaw Sinkhorn normalization")
    if diffusion.get("sinkhorn_residual_max", math.inf) > 2e-10:
        failures.append("jaw Sinkhorn residual")
    if diffusion["row_residual_max"] > 2e-10:
        failures.append("jaw constant preservation")
    largest = diffusion["largest_symmetric_eigenvalues"]
    smallest = diffusion["smallest_symmetric_eigenvalues"]
    if abs(largest[0] - 1.0) > 2e-8:
        failures.append("jaw leading diffusion eigenvalue")
    if max(largest) > 1.0 + 2e-8 or min(smallest) < -2e-8:
        failures.append("jaw spectral damping")

    snapshots = diffusion["snapshots"]
    masses = [item["mass"] for item in snapshots]
    minima = [item["minimum"] for item in snapshots]
    l2_values = [item["weighted_l2_from_constant"] for item in snapshots]
    roughness = [item["q_roughness"] for item in snapshots]
    moments = [item["spatial_second_moment"] for item in snapshots]
    if max(abs(value - 1.0) for value in masses) > 2e-10:
        failures.append("jaw mass conservation")
    if min(minima) < -2e-10:
        failures.append("jaw positivity")
    if any(
        later > earlier * (1.0 + 2e-9) + 1e-10
        for earlier, later in zip(l2_values, l2_values[1:])
    ):
        failures.append("jaw monotone L2 smoothing")
    if min(roughness) < -2e-8:
        failures.append("jaw nonnegative diffusion roughness")
    if any(
        later > earlier * (1.0 + 2e-8) + 1e-10
        for earlier, later in zip(roughness, roughness[1:])
    ):
        failures.append("jaw monotone diffusion roughness")
    if moments[1] <= moments[0] + 1e-8:
        failures.append("jaw Dirac spatial spreading")

    return {
        "claim_5_contract_pass": not failures,
        "verifier": "primary_record_contract",
        "failures": failures,
        "summary": {
            "jaw_triangles": mesh["triangle_count"],
            "jaw_nonempty_voxels": voxels["nonempty_voxels"],
            "jaw_occupancy_fraction": voxels["occupancy_fraction"],
            "jaw_component_fraction": (
                voxels["largest_6_connected_component_fraction"]
            ),
            "maximum_mass_error": max(
                abs(value - 1.0) for value in masses
            ),
            "minimum_signal_value": min(minima),
            "l2_reduction_ratio": l2_values[-1] / l2_values[0],
            "roughness_reduction_ratio": (
                roughness[-1] / max(roughness[0], 1e-300)
            ),
        },
    }


def main() -> None:
    if len(sys.argv) != 3:
        raise SystemExit("usage: verify_claim5.py RAW_JSON OUTPUT_JSON")
    record = json.loads(Path(sys.argv[1]).read_text(encoding="utf-8"))
    result = evaluate(record)
    Path(sys.argv[2]).write_text(
        json.dumps(result, indent=2) + "\n", encoding="utf-8"
    )
    print("CLAIM5_PRIMARY=" + json.dumps(result, sort_keys=True))
    if not result["claim_5_contract_pass"]:
        raise SystemExit(1)


if __name__ == "__main__":
    main()