"""Exact short-length exterior gates for the accompanying manuscript.

The single-evaluation lemma handles the excluded symbolic family; the
written long-tuple estimates handle lengths at least sixteen. These
computations verify arithmetic only, after the incidence reductions.
All operations use the Python standard library and exact integers.
"""

from functools import lru_cache


@lru_cache(None)
def exact_cokernel_cap(rank_cap, old_span, coefficient_dimension):
    answer = 0
    for rank in range(2, min(rank_cap, old_span, coefficient_dimension) + 1):
        kernel = rank * (rank - 1) // 2
        upper_right_factor = max(rank, coefficient_dimension - rank)
        lower_left_factor = max(rank, old_span - rank)
        two_sided = max(
            min(b * upper_right_factor + kernel,
                (rank - b) * lower_left_factor + 4 * kernel)
            for b in range(rank + 1)
        )
        answer = max(answer, min(
            rank * coefficient_dimension - rank * (rank + 1) // 2,
            rank * (coefficient_dimension - 2) + 1,
            two_sided,
        ))
    return answer


def main():
    checked = 0
    symbolic = 0
    for length in range(4, 16):
        old_rank = 6 * length - 5
        minimum = None
        minimizer = None
        row_count = 0
        symbolic_count = 0
        for last_corank in range(2):
            for pure_last_rank in range(last_corank + 1):
                e = (last_corank - pure_last_rank) * length
                total_coefficient_rank = (2 - pure_last_rank) * length
                for overlap in range((3 - last_corank) * length):
                    h = (3 - last_corank) * length - overlap
                    tau = overlap + e
                    assert h <= old_rank
                    for j in range(total_coefficient_rank + 1):
                        L = tau - j
                        u = total_coefficient_rank - j
                        w = max(0, (3 * j - 2 * e + 1) // 2)
                        if L < 1 or 3 * j > 2 * tau or w > overlap:
                            continue
                        assert L - 1 >= 0
                        if last_corank == pure_last_rank == j == 0:
                            # The whole omitted family, not merely its failing
                            # rows, has a separate proof valid at every length.
                            symbolic_count += 1
                            continue
                        rank_cap = min(2 * tau - 3 * j, h, u)
                        cokernel = exact_cokernel_cap(rank_cap, h, u)
                        normal_loss = ((3 - last_corank) * last_corank
                                       - pure_last_rank * (5 - last_corank
                                                           + pure_last_rank))
                        codimension = (L * old_rank + 6 * length
                                       - length * normal_loss
                                       - (overlap - w) * h - j * u - cokernel)
                        excess = codimension - old_rank - 5
                        record = (last_corank, pure_last_rank, overlap, j,
                                  L, h, u, w, rank_cap, cokernel)
                        assert excess > 0, (length, record, excess)
                        if minimum is None or excess < minimum:
                            minimum, minimizer = excess, record
                        row_count += 1
        checked += row_count
        symbolic += symbolic_count
        print(f"length={length:2d} M={old_rank:2d} checked={row_count:4d} "
              f"symbolic={symbolic_count:2d} minimum={minimum:3d} "
              f"minimizer={minimizer}")
    assert (checked, symbolic) == (8427, 330)
    print(f"Exact endpoint rows checked: {checked}")
    print(f"Rows covered by the uniform single-evaluation lemma: {symbolic}")
    print(f"Total short-length rows: {checked + symbolic}")
    print("All finite gates are strict; all old-rank slopes are nonnegative.")
    print("The unbounded length ranges are covered by written symbolic proofs.")


if __name__ == "__main__":
    main()