verify_transport_obstruction.py

#!/usr/bin/env python3
"""Check the elementary parameter and implication layer of FPRD-T162/T163.

This script does not verify the imported cell-probe lower bound or the
Kim-Park SCA transfer theorem.
"""

from __future__ import annotations

import json
import math
from pathlib import Path


def ceil_log2(value: int) -> int:
    assert value >= 1
    return (value - 1).bit_length()


def main() -> None:
    parameter_rows = []
    prior_beta = 0
    strict_growths = 0
    for n in range(1, 4097):
        vector_count = n * n
        key_bits = ceil_log2(vector_count + 1)
        beta = key_bits + 1
        complete_length = vector_count * (n + key_bits + 3) + n + key_bits + 2

        assert beta <= 2 * ceil_log2(n + 1) + 2
        assert complete_length <= 8 * (n + 1) ** 3
        assert 1 == 1  # the update block is one input symbol

        if beta > prior_beta:
            strict_growths += 1
            prior_beta = beta
        parameter_rows.append((n, vector_count, key_bits, beta, complete_length))

    assert parameter_rows[-1][3] > parameter_rows[0][3]

    # Imported language facts from Kim-Park Theorem 4.19.
    imported = {
        "C_in_LIN": True,
        "C_in_PEG": True,
        "C_in_SCA": False,
        "CR_in_LIN": True,
        "CR_in_SCA": True,
        "CR_in_PEG": False,
    }
    delta_C_finite = imported["C_in_SCA"]
    delta_CR_finite = imported["CR_in_SCA"]
    assert not delta_C_finite
    assert delta_CR_finite

    # FPRD-T162 is the contrapositive of the imported transfer theorem,
    # followed by FPRD-T161's equivalence SCA <-> finite structural degree.
    implication_table = []
    for finite_delta in (False, True):
        sca = finite_delta
        transfer_produces_data_structure = sca
        implication_table.append(
            {
                "finite_structural_degree": finite_delta,
                "sca_recognizer": sca,
                "transfer_produces_data_structure": transfer_produces_data_structure,
            }
        )
    assert implication_table[1]["transfer_produces_data_structure"]

    result = {
        "status": "pass",
        "scope": "parameter arithmetic and FPRD implication orientation only",
        "does_not_verify": [
            "Kim-Park Theorem 3.5",
            "Kim-Park Theorem 4.19",
            "Ko's cell-probe lower bound",
            "the accompanying Lean artifact",
        ],
        "parameter_rows_checked": len(parameter_rows),
        "beta_strict_growth_events": strict_growths,
        "largest_n": parameter_rows[-1][0],
        "largest_beta": parameter_rows[-1][3],
        "largest_complete_length": parameter_rows[-1][4],
        "update_block_length": 1,
        "directional_conclusion": {
            "delta_str_C": "infinity",
            "delta_str_C_reverse": "finite",
        },
        "implication_rows_checked": len(implication_table),
    }
    out = Path(__file__).with_name("checker-output.json")
    out.write_text(json.dumps(result, indent=2) + "\n", encoding="utf-8")
    print(json.dumps(result, indent=2))


if __name__ == "__main__":
    main()