#!/usr/bin/env python3
"""Pinned verifier for Axler's compact pi(x) coefficient 44.053."""

from __future__ import annotations

import hashlib
import importlib.util
from importlib.metadata import version
import json
from fractions import Fraction
from math import factorial
from pathlib import Path
import platform
import re
import sys
from types import ModuleType

import flint
from flint import arb, ctx, fmpq


if not __debug__:
    raise SystemExit("verify.py requires assertions")


PRECISION = 256
ctx.prec = PRECISION

PUBLISHED_COEFFICIENT_Q = Fraction(70_935, 1_000)
NEW_COEFFICIENT_Q = Fraction(44_053, 1_000)

ACTUAL_LEFT_ENDPOINT_Q = Fraction(2_953, 100)
LOW_LOG_LEFT_Q = Fraction(3_385, 1_000)
LOW_LOG_RIGHT = 10
LOW_LOG_CELLS = 16_384
LOW_LI_MAJORANT_C_Q = Fraction(55)

HIGH_LI_MAJORANT_ORDER = 15
HIGH_LI_MAJORANT_START = 40
TABLE_START = 44
TABLE_END = 3_000

FKS_ASYMPTOTIC_AMPLITUDE_Q = Fraction(9_221_056, 1_000_000)
FKS_ASYMPTOTIC_DECAY_Q = Fraction(84_768_363, 100_000_000)
PI_LOWER_Q = Fraction(314_159, 100_000)

EXPECTED_ACTIVE_REQUIREMENT_Q = Fraction(
    2_709_976_113_860_085_547_103_395_243_942_841_453_423_728_245_400,
    61_517_068_085_059_134_496_927_148_872_832_330_483_236_342_381,
)
EXPECTED_REQUIREMENT_MARGIN_Q = Fraction(
    35_286_491_024_504_889_736_445_352_041_201_354_282_345_510_193,
    61_517_068_085_059_134_496_927_148_872_832_330_483_236_342_381_000,
)

C0050_VERIFIER_SHA256 = (
    "852ed0428364c5f9cf4f332e33a4478f5c71fabd24e2fa0878172a24092f7451"
)
C0050_RESULTS_SHA256 = (
    "b3b522330c75c28584fb4101b7f394b8105be171bb0cd693a28087f2055b5cd8"
)

HERE = Path(__file__).resolve().parent
SOURCE = HERE / "source"
OUTPUT = HERE / "results.json"

EXPECTED_RUNTIME = {
    "python": "3.14.6",
    "python-flint": "0.9.0",
    "flint": "3.6.0",
}

EXPECTED_SOURCE_HASHES = {
    "dependency/c0050/claim.md": "16a959ec7eb1a21904bf27fb9e475cb03b0c5f7de3122d53f79b8f852ca4a5c6",
    "dependency/c0050/results.json": "b3b522330c75c28584fb4101b7f394b8105be171bb0cd693a28087f2055b5cd8",
    "dependency/c0050/verify.py": "852ed0428364c5f9cf4f332e33a4478f5c71fabd24e2fa0878172a24092f7451",
    "dependency/c0051/PIN.md": "eab6844dc104e589b0d6d6388025f9bafaf3be154706a0846f65d41ce412c3b9",
    "dependency/c0051/claim.md": "4652e00adb520157e7d36b01985901bdb3b21d65b0516aa0ba859dc0f81ef8df",
    "dependency/c0051/verify.py": "a9ca2416786e3349aaf3bc2a32894572bf4a6c3cb1e52c53690621c2e5521874",
    "primary/axler-2203.05917.tex": "0436439c8c2b8a2c13cc7ef1935cb8d62136ff1784f035da9673f98f4853bfa9",
    "primary/axler-integers-24-A34.pdf": "c093bd507a7e130d1c28ebe8a8707d811a39f8c60ba6cc598afc4bc6e2e522f9",
    "primary/axler-integers-24-A34.txt": "5597897b3fed188cbaee881fb8a0048ecfdcf265edbf2dc1fb69a8787781d50e",
    "primary/buthe-1511.02032.pdf": "350f96313810ded3e8eaf2af6006b227c8834235e177f49eabb3d43d4931c4d1",
    "primary/buthe-1511.02032.txt": "584e158d4e4d3dd3aee1242f94ceaed34f8af77527d4974f1d86519a3178c3c2",
    "primary/fiori-kadiri-swidinsky-2206.12557v2.pdf": "405e5dcbca6067fa436141b8a08c79b81bc12deca03bfe12d667428c36b50fbb",
    "primary/fiori-kadiri-swidinsky-2206.12557v2.txt": "9c926ea1ed333e8008c245f8f5bdd87c72fff0eb1647f87d7e02fbf198169edf",
    "repository/experiment-runner.py": "3f5b0fe5ae53428a657c5d3e0c0c06c38c8b2230796e31ee3285893e5a3d03fe",
    "repository/independent-check.py": "09d654a60ffcacedc093875f35d009501fb925979794ccf2c55dd2cf25dadec7",
    "repository/independent-review.md": "f87fd42d0e46a083e9ffaa9b13072c0b72f08e9b3c9ea301e9df63d1ad495e16",
    "repository/literature-search.md": "378e39d7ce88116ff8d63fcf8e8652d56be3245ddb16596ca2e4d889d9d2901e",
    "repository/original-proof-note.md": "7ca4c75d67ce5a44dd0418a15454bb92e6f968bbaa2032634c4e183b6b130516",
    "repository/original-result.md": "a66f00892453109b91c65e8d6f5c20a240ecb312f67211acc628b8bed6ee91e5",
    "repository/previous-pin.md": "d956b30ce454e468b3456a851d86392fcfc21bb83f80c8b93df1a31c51d12f38",
    "repository/previous-verify.py": "26fdc8a71084ba41e0580a4fe9a6315efbc437f4d3a6707361d2cc3ff6b35db2",
}


def repository_root() -> Path:
    for parent in Path(__file__).resolve().parents:
        if (parent / "canon").is_dir() and (parent / "pyproject.toml").is_file():
            return parent
    raise RuntimeError("repository root not found")


def sha256(path: Path) -> str:
    return hashlib.sha256(path.read_bytes()).hexdigest()


def pin_sources() -> dict[str, str]:
    actual = {
        relative: sha256(SOURCE / relative)
        for relative in sorted(EXPECTED_SOURCE_HASHES)
    }
    assert actual == EXPECTED_SOURCE_HASHES
    return actual


def pin_runtime() -> dict[str, str]:
    actual = {
        "python": platform.python_version(),
        "python-flint": version("python-flint"),
        "flint": flint.__FLINT_VERSION__,
    }
    assert actual == EXPECTED_RUNTIME
    return actual


def normalized(path: Path) -> str:
    return re.sub(r"\s+", " ", path.read_text())


def audit_source_anchors() -> dict[str, list[str]]:
    texts = {
        "axler": normalized(SOURCE / "primary/axler-integers-24-A34.txt"),
        "buthe": normalized(SOURCE / "primary/buthe-1511.02032.txt"),
        "fks": normalized(
            SOURCE / "primary/fiori-kadiri-swidinsky-2206.12557v2.txt"
        ),
    }
    anchors = {
        "axler": [
            "Proposition 4. For every x ≥ 29.53",
            "70.935",
        ],
        "buthe": ["li(x) − π(x) > 0 for 2 ≤ x ≤ 1019"],
        "fks": [
            "li(x) − Li(x) = li(2)",
            "Corollary 22. For all x ≥ 2 we have",
            "Table 4. Values for επ,num",
            "Table 7. Other forms of bounds Eπ ≤ B(x)",
        ],
    }
    for name, tokens in anchors.items():
        for token in tokens:
            assert token in texts[name]
    return anchors


def load_pinned_module(name: str, path: Path) -> ModuleType:
    spec = importlib.util.spec_from_file_location(name, path)
    assert spec is not None and spec.loader is not None
    module = importlib.util.module_from_spec(spec)
    sys.modules[name] = module
    spec.loader.exec_module(module)
    return module


def load_c0050_verifier() -> ModuleType:
    path = repository_root() / "canon" / "witnesses" / "C-0050" / "verify.py"
    digest = hashlib.sha256(path.read_bytes()).hexdigest()
    assert digest == C0050_VERIFIER_SHA256

    spec = importlib.util.spec_from_file_location("_c0050_verifier", path)
    assert spec is not None and spec.loader is not None
    module = importlib.util.module_from_spec(spec)
    spec.loader.exec_module(module)
    return module


C0050 = load_c0050_verifier()
FKS_TABLE_ROWS = C0050.FKS_TABLE_ROWS
HIGH_LI_REMAINDER_Q = C0050.LI_REMAINDER_Q


def audit_dependencies() -> dict[str, object]:
    c0050_results_path = SOURCE / "dependency/c0050/results.json"
    assert sha256(c0050_results_path) == C0050_RESULTS_SHA256
    c0050 = json.loads(c0050_results_path.read_text())
    assert c0050["verdict"] == "ACCEPT"
    assert c0050["fks_table_transcript"]["parsed_rows"] == 164
    assert c0050["fks_table_transcript"]["source_matches_ast_literal"]

    c0051_module = load_pinned_module(
        "c0051_dependency", SOURCE / "dependency/c0051/verify.py"
    )
    c0051 = c0051_module.certify()
    assert c0051.amplitude_margin > arb("1.18e-7")
    assert c0051.decay_margin > arb("3.66e-9")
    return {
        "C-0050": {
            "verdict": c0050["verdict"],
            "table_rows": c0050["fks_table_transcript"]["parsed_rows"],
            "source_matches_ast_literal": True,
        },
        "C-0051": {
            "amplitude_margin": str(c0051.amplitude_margin),
            "decay_margin": str(c0051.decay_margin),
        },
    }


def q(value: Fraction | int) -> arb:
    value = Fraction(value)
    return arb(fmpq(value.numerator, value.denominator))


def make_interval(left: Fraction, right: Fraction) -> arb:
    midpoint = (left + right) / 2
    radius = (right - left) / 2
    return arb(
        fmpq(midpoint.numerator, midpoint.denominator),
        fmpq(radius.numerator, radius.denominator),
    )


def convolve(
    left: list[Fraction], right: list[Fraction]
) -> list[Fraction]:
    result = [Fraction(0)] * (len(left) + len(right) - 1)
    for left_index, left_value in enumerate(left):
        for right_index, right_value in enumerate(right):
            result[left_index + right_index] += left_value * right_value
    return result


def subtract_polynomials(
    left: list[Fraction], right: list[Fraction]
) -> list[Fraction]:
    result = [Fraction(0)] * max(len(left), len(right))
    for index, value in enumerate(left):
        result[index] += value
    for index, value in enumerate(right):
        result[index] -= value
    return result


def evaluate_polynomial(coefficients: list[Fraction], value: arb) -> arb:
    result = arb(0)
    for coefficient in reversed(coefficients):
        result *= value
        result += q(coefficient)
    return result


def denominator(log_x: arb, coefficient: Fraction) -> arb:
    return (
        log_x
        - 1
        - 1 / log_x
        - 3 / log_x**2
        - q(coefficient) / log_x**3
    )


def denominator_scale(log_x: arb) -> arb:
    reciprocal_log = 1 / log_x
    return (
        1
        - reciprocal_log
        - reciprocal_log**2
        - 3 * reciprocal_log**3
        - q(NEW_COEFFICIENT_Q) * reciprocal_log**4
    )


def exact_normalized_li_gap(log_x: arb) -> arb:
    return (
        1 / denominator_scale(log_x)
        - log_x * (-log_x).exp() * log_x.ei()
    )


def high_li_normalized_majorant(log_x: arb | int) -> arb:
    log_x = log_x if isinstance(log_x, arb) else arb(log_x)
    result = arb(0)
    for index in range(HIGH_LI_MAJORANT_ORDER + 1):
        result += factorial(index) / log_x**index
    result += q(HIGH_LI_REMAINDER_Q) / log_x ** (
        HIGH_LI_MAJORANT_ORDER + 1
    )
    return result


def high_li_normalized_majorant_q(log_x: int) -> Fraction:
    result = Fraction(0)
    for index in range(HIGH_LI_MAJORANT_ORDER + 1):
        result += Fraction(factorial(index), log_x**index)
    result += HIGH_LI_REMAINDER_Q / log_x ** (
        HIGH_LI_MAJORANT_ORDER + 1
    )
    return result


def high_normalized_gap(log_x: arb | int) -> arb:
    log_x = log_x if isinstance(log_x, arb) else arb(log_x)
    return (
        1 / denominator_scale(log_x)
        - high_li_normalized_majorant(log_x)
    )


def high_normalized_gap_q(log_x: int) -> Fraction:
    reciprocal_log = Fraction(1, log_x)
    scale = (
        1
        - reciprocal_log
        - reciprocal_log**2
        - 3 * reciprocal_log**3
        - NEW_COEFFICIENT_Q * reciprocal_log**4
    )
    return Fraction(1, 1) / scale - high_li_normalized_majorant_q(log_x)


def verify_denominators() -> dict[str, str]:
    actual_log = q(ACTUAL_LEFT_ENDPOINT_Q).log()
    assert actual_log > q(LOW_LOG_LEFT_Q)

    new_at_lower_log_q = (
        LOW_LOG_LEFT_Q
        - 1
        - 1 / LOW_LOG_LEFT_Q
        - 3 / LOW_LOG_LEFT_Q**2
        - NEW_COEFFICIENT_Q / LOW_LOG_LEFT_Q**3
    )
    assert new_at_lower_log_q > 0

    new_at_endpoint = denominator(actual_log, NEW_COEFFICIENT_Q)
    published_at_endpoint = denominator(
        actual_log, PUBLISHED_COEFFICIENT_Q
    )
    assert new_at_endpoint > q(Fraction(69, 100))
    assert published_at_endpoint > q(Fraction(4, 100_000))

    # D_A'(L)=1+L^-2+6L^-3+3A L^-4 is positive for every L>0.
    assert NEW_COEFFICIENT_Q > 0
    assert PUBLISHED_COEFFICIENT_Q > NEW_COEFFICIENT_Q

    return {
        "log_29_53_minus_3_385": str(actual_log - q(LOW_LOG_LEFT_Q)),
        "new_denominator_at_log_3_385_exact": str(new_at_lower_log_q),
        "new_denominator_at_x_29_53": str(new_at_endpoint),
        "published_denominator_at_x_29_53": str(
            published_at_endpoint
        ),
        "coefficient_decrease_exact": str(
            PUBLISHED_COEFFICIENT_Q - NEW_COEFFICIENT_Q
        ),
    }


def verify_low_direct_li_cover() -> dict[str, object]:
    minimum_gap = None
    minimum_cell = None
    for index in range(LOW_LOG_CELLS):
        left = LOW_LOG_LEFT_Q + (
            Fraction(LOW_LOG_RIGHT) - LOW_LOG_LEFT_Q
        ) * index / LOW_LOG_CELLS
        right = LOW_LOG_LEFT_Q + (
            Fraction(LOW_LOG_RIGHT) - LOW_LOG_LEFT_Q
        ) * (index + 1) / LOW_LOG_CELLS
        log_interval = make_interval(left, right)
        assert denominator_scale(log_interval) > 0
        gap = exact_normalized_li_gap(log_interval)
        assert gap > 0
        if minimum_gap is None or gap.lower() < minimum_gap.lower():
            minimum_gap = gap
            minimum_cell = (left, right)

    assert minimum_gap is not None and minimum_cell is not None
    return {
        "cells": LOW_LOG_CELLS,
        "minimum_gap": str(minimum_gap),
        "minimum_gap_lower": str(minimum_gap.lower()),
        "minimum_cell": [str(minimum_cell[0]), str(minimum_cell[1])],
    }


def verify_low_rational_li_majorant() -> dict[str, str]:
    log_10 = arb(LOW_LOG_RIGHT)
    normalized_li = log_10 * (-log_10).exp() * log_10.ei()
    majorant = (
        1
        + 1 / log_10
        + 2 / log_10**2
        + 6 / log_10**3
        + q(LOW_LI_MAJORANT_C_Q) / log_10**4
    )
    initial_gap = majorant - normalized_li
    assert initial_gap > q(Fraction(2, 1_000_000))

    # For the corresponding R(L)=exp(-L)Ei(L) majorant,
    # (U-R)'+(U-R) has numerator 55(1-5/L)-24.
    forcing_at_10_q = (
        LOW_LI_MAJORANT_C_Q
        * (1 - Fraction(5, LOW_LOG_RIGHT))
        - factorial(4)
    )
    assert forcing_at_10_q == Fraction(7, 2)

    # Multiplication by the positive denominator scale gives
    # t^4 times this polynomial, whose coefficients are all positive.
    residual_factor_q = (
        NEW_COEFFICIENT_Q - 44,
        NEW_COEFFICIENT_Q + 67,
        2 * NEW_COEFFICIENT_Q + 73,
        6 * NEW_COEFFICIENT_Q + 165,
        55 * NEW_COEFFICIENT_Q,
    )
    assert all(coefficient > 0 for coefficient in residual_factor_q)

    # Buethe's pi(x)<=li(x) computation through 10^19 overlaps e^40.
    buethe_overlap = 19 * arb(10).log() - 40
    assert buethe_overlap > 3

    return {
        "majorant_gap_at_log_10": str(initial_gap),
        "forcing_numerator_at_log_10_exact": str(forcing_at_10_q),
        "denominator_residual_factor": str(residual_factor_q),
        "log_10_pow_19_minus_40": str(buethe_overlap),
    }


def monotonicity_factor() -> list[Fraction]:
    coefficient = NEW_COEFFICIENT_Q
    scale = [
        Fraction(1),
        -Fraction(1),
        -Fraction(1),
        -Fraction(3),
        -coefficient,
    ]
    majorant = [
        Fraction(factorial(index))
        for index in range(HIGH_LI_MAJORANT_ORDER + 1)
    ] + [HIGH_LI_REMAINDER_Q]
    majorant_derivative = [
        index * majorant[index] for index in range(1, len(majorant))
    ]
    reciprocal_derivative_numerator = [
        Fraction(1),
        Fraction(2),
        Fraction(9),
        4 * coefficient,
    ]
    numerator = subtract_polynomials(
        reciprocal_derivative_numerator,
        convolve(convolve(scale, scale), majorant_derivative),
    )
    assert all(value == 0 for value in numerator[:3])
    return numerator[3:]


def verify_high_li_majorant_and_monotonicity() -> dict[str, str]:
    start = arb(HIGH_LI_MAJORANT_START)
    normalized_exact_li = start * (-start).exp() * start.ei()
    majorant_gap = high_li_normalized_majorant(start) - normalized_exact_li
    assert majorant_gap > 0

    forcing_q = (
        HIGH_LI_REMAINDER_Q
        * (
            1
            - Fraction(
                HIGH_LI_MAJORANT_ORDER + 2, HIGH_LI_MAJORANT_START
            )
        )
        - factorial(HIGH_LI_MAJORANT_ORDER + 1)
    )
    assert forcing_q == factorial(HIGH_LI_MAJORANT_ORDER + 1)

    factor = monotonicity_factor()
    minimum = None
    subdivisions = 256
    for index in range(subdivisions):
        reciprocal_log = make_interval(
            Fraction(index, subdivisions * HIGH_LI_MAJORANT_START),
            Fraction(index + 1, subdivisions * HIGH_LI_MAJORANT_START),
        )
        value = evaluate_polynomial(factor, reciprocal_log)
        assert value > 0
        if minimum is None or value.lower() < minimum.lower():
            minimum = value
    assert minimum is not None

    return {
        "majorant_gap_at_log_40": str(majorant_gap),
        "forcing_numerator_at_log_40_exact": str(forcing_q),
        "monotonicity_factor_minimum": str(minimum),
        "monotonicity_factor_minimum_lower": str(minimum.lower()),
    }


def table_requirement(log_x: int, epsilon: Fraction) -> Fraction:
    reciprocal_log = Fraction(1, log_x)
    return log_x**4 * (
        1
        - reciprocal_log
        - reciprocal_log**2
        - 3 * reciprocal_log**3
        - Fraction(
            1, high_li_normalized_majorant_q(log_x) + epsilon
        )
    )


def verify_fks_numerical_ranges() -> dict[str, object]:
    assert q(PI_LOWER_Q) < arb.pi()
    assert arb(2).li() > 1

    # Table 7: E_pi <= L^2 exp(-L/2)/(8*pi) on 8<=L<=60.8.
    # The error decreases on [40,44], while the normalized gap decreases
    # because the monotonicity factor above is positive.
    assert Fraction(2, HIGH_LI_MAJORANT_START) < Fraction(1, 2)
    table7_error_at_40 = (
        arb(HIGH_LI_MAJORANT_START) ** 2
        * (-arb(HIGH_LI_MAJORANT_START) / 2).exp()
        / (8 * q(PI_LOWER_Q))
    )
    table7_margin = high_normalized_gap(TABLE_START) - table7_error_at_40
    assert table7_margin > q(Fraction(8, 1_000_000))

    assert len(FKS_TABLE_ROWS) == 164
    assert FKS_TABLE_ROWS[0][0] == TABLE_START
    assert FKS_TABLE_ROWS[-1][0] == TABLE_END
    assert all(
        FKS_TABLE_ROWS[index][0] < FKS_TABLE_ROWS[index + 1][0]
        for index in range(len(FKS_TABLE_ROWS) - 1)
    )
    assert all(
        FKS_TABLE_ROWS[index][1] > FKS_TABLE_ROWS[index + 1][1]
        for index in range(len(FKS_TABLE_ROWS) - 1)
    )

    requirements = []
    margins = []
    for (left, epsilon), (right, _) in zip(
        FKS_TABLE_ROWS, FKS_TABLE_ROWS[1:]
    ):
        requirement = table_requirement(right, epsilon)
        assert NEW_COEFFICIENT_Q > requirement
        requirements.append((requirement, left, right))

        margin_q = high_normalized_gap_q(right) - epsilon
        assert margin_q > 0
        margins.append((margin_q, left, right))

    active_requirement, active_left, active_right = max(requirements)
    assert (active_left, active_right) == (2_100, 2_200)
    assert active_requirement == EXPECTED_ACTIVE_REQUIREMENT_Q

    requirement_margin_q = NEW_COEFFICIENT_Q - active_requirement
    assert requirement_margin_q == EXPECTED_REQUIREMENT_MARGIN_Q

    minimum_margin_q, minimum_left, minimum_right = min(margins)
    assert (minimum_left, minimum_right) == (2_100, 2_200)

    return {
        "table7_margin": str(table7_margin),
        "table4_rows": len(FKS_TABLE_ROWS),
        "active_interval": [active_left, active_right],
        "active_requirement_exact": str(active_requirement),
        "active_requirement_decimal": float(active_requirement),
        "coefficient_minus_requirement_exact": str(requirement_margin_q),
        "coefficient_minus_requirement_decimal": float(
            requirement_margin_q
        ),
        "minimum_exact_interval_margin": str(minimum_margin_q),
        "minimum_exact_interval_margin_decimal": float(minimum_margin_q),
    }


def asymptotic_factor() -> list[Fraction]:
    scale = [
        Fraction(1),
        -Fraction(1),
        -Fraction(1),
        -Fraction(3),
        -NEW_COEFFICIENT_Q,
    ]
    majorant = [
        Fraction(factorial(index))
        for index in range(HIGH_LI_MAJORANT_ORDER + 1)
    ] + [HIGH_LI_REMAINDER_Q]
    reserve_q = (NEW_COEFFICIENT_Q - 13) / 2
    majorant[4] += reserve_q
    numerator = subtract_polynomials(
        [Fraction(1)], convolve(scale, majorant)
    )
    assert all(value == 0 for value in numerator[:4])
    return numerator[4:]


def verify_asymptotic_tail() -> dict[str, str]:
    reserve_q = (NEW_COEFFICIENT_Q - 13) / 2
    assert reserve_q == Fraction(31_053, 2_000)

    factor = asymptotic_factor()
    reciprocal_log = make_interval(Fraction(0), Fraction(1, TABLE_END))
    factor_value = evaluate_polynomial(factor, reciprocal_log)
    assert factor_value > 15

    log_3000 = arb(TABLE_END)
    simple_gap = q(reserve_q) / log_3000**4
    sqrt_log = log_3000.sqrt()
    asymptotic_error = (
        q(FKS_ASYMPTOTIC_AMPLITUDE_Q)
        * log_3000
        * sqrt_log
        * (-q(FKS_ASYMPTOTIC_DECAY_Q) * sqrt_log).exp()
    )
    margin = simple_gap - asymptotic_error
    assert q(FKS_ASYMPTOTIC_DECAY_Q) * sqrt_log > 11
    assert margin > q(Fraction(18, 100_000_000_000_000))

    return {
        "reserve_exact": str(reserve_q),
        "tail_polynomial_factor": str(factor_value),
        "simple_gap_at_log_3000": str(simple_gap),
        "c0051_error_at_log_3000": str(asymptotic_error),
        "margin_at_log_3000": str(margin),
    }


def main() -> None:
    result = {
        "verdict": "ACCEPT",
        "claim": "C-0055",
        "material_defect_repaired": (
            "the previous verifier pinned the superseded C-0050 verifier hash "
            "and failed before executing its certificate"
        ),
        "source_hashes": pin_sources(),
        "source_anchors": audit_source_anchors(),
        "runtime": pin_runtime(),
        "dependencies": audit_dependencies(),
        "published_coefficient": str(PUBLISHED_COEFFICIENT_Q),
        "new_coefficient": str(NEW_COEFFICIENT_Q),
        "denominators": verify_denominators(),
        "low_direct_li_cover": verify_low_direct_li_cover(),
        "low_rational_li_majorant": verify_low_rational_li_majorant(),
        "high_li_majorant": verify_high_li_majorant_and_monotonicity(),
        "fks_numerical_ranges": verify_fks_numerical_ranges(),
        "asymptotic_tail": verify_asymptotic_tail(),
        "normalization": (
            "FKS uses Li(x)=li(x)-li(2); the absolute C-0051 error "
            "therefore supplies the required one-sided upper comparison"
        ),
        "scope": "explicit prime-counting inequality only; all-height RH excluded",
    }
    payload = json.dumps(result, indent=2, sort_keys=True) + "\n"
    OUTPUT.write_text(payload)
    print(payload, end="")


if __name__ == "__main__":
    main()
