"""Exact finite gates for the reserve-five rank-twelve endpoint.

This certificate verifies the complete finite integer enumeration and
resulting inequalities in the core section.  It does not replace the
geometric proofs of the exclusions and additional codimension bounds.
Python standard library only; no floating-point calculations.
"""


def rows(length, old_rank=12, reserve=5):
    for gamma in (0, 1):
        for pure_last in range(gamma + 1):
            e = length * (gamma - pure_last)
            for delta in range((length - 1) * (3 - gamma) + 1):
                for j in range(length * (2 - pure_last) + 1):
                    L = delta + e - j
                    h = length * (3 - gamma) - delta
                    u = length * (2 - pure_last) - j
                    w = max(0, (3 * j - 2 * e + 1) // 2)
                    if L < 1 or j > 2 * L or w > delta:
                        continue
                    rank = min(2 * L - j, u, h)
                    chi = 0 if rank < 2 else rank * u - rank * (rank + 1) // 2
                    bound = (L * old_rank + reserve * length - 12
                             - length * gamma * (3 - gamma) + 2 * pure_last
                             - (delta - w) * h - j * u - chi)
                    yield (gamma, pure_last, delta, j), (L, h, u, chi), bound


def main():
    for length, expected_count in ((2, 17), (3, 47)):
        count = 0
        excluded = 0
        minimum = None
        for key, values, raw in rows(length):
            gamma, pure_last, delta, j = key
            L, h, u, chi = values
            assert L >= 1
            count += 1
            if gamma == 1 and pure_last == 0 and delta == 0 and j > 0:
                excluded += 1
                print(length, key, "excluded: direct-sum coefficient injectivity")
                continue
            if key == (1, 0, 1, 2):
                excluded += 1
                print(length, key, "excluded: constant-row exceptional locus")
                continue
            revised = raw
            reason = "raw estimate"
            if length == 2 and key == (0, 0, 1, 0):
                # Transverse Z: Q has dimension 7; two outputs collinear, cost 6.
                # Nontransverse: new Z position costs 2 and relation line 4.
                revised += min(12 - 6, 2 + 4)
                reason = "off-diagonal pair rank / separate Z and relation positions"
            if length == 3 and key == (0, 0, 1, 0):
                # Off cubic: chi=0. On cubic: Z has a last line; Z cost 2
                # and relation line inside a fixed three-plane costs 6.
                revised += min(chi, 2 + 6)
                reason = "zero cokernel or conic last-line relation"
            if length == 3 and key == (0, 0, 2, 0):
                good_expanded = raw + chi - 10 + (12 - 9)
                bad_expanded = raw + chi - 11 + 6
                nontransverse = raw + 2 + 5
                assert (good_expanded, bad_expanded, nontransverse) == (6, 8, 6)
                revised = min(good_expanded, bad_expanded, nontransverse)
                reason = "three exhaustive expanded-evaluation/position branches"
            if key == (1, 1, 1, 0):
                revised += chi
                if length == 2:
                    revised += 2
                reason = "zero skew cokernel; pair kernel/relationship saving"
            assert revised > 5, (length, key, values, raw, revised)
            minimum = revised if minimum is None else min(minimum, revised)
            if raw <= 5:
                print(length, key, "raw", raw, "revised", revised, reason)
        assert count == expected_count
        assert minimum == 6
        print("length", length, "rows", count, "excluded", excluded,
              "retained", count - excluded, "positive-overlap minimum", minimum)

    pair = [(g, (10 - g) * (12 - g) + g - 3) for g in range(5, 10)]
    triple = [(g, (15 - g) * (12 - g) + g + 1) for g in range(5, 13)]
    assert min(value for _, value in pair) == 9
    assert min(value for _, value in triple) == 13
    print("zero-overlap pair bounds:", pair)
    print("zero-overlap triple bounds:", triple)
    for g in (13, 14):
        assert g + 1 > 5  # at any newly allowed old rank r>=g
    print("Newly allowed triple graph ranks 13,14 have bound at least g+1>5.")
    print("All 64 finite rank rows are covered; all surviving bounds are strict.")
    print("Unbounded-rank persistence is proved by slopes and the written endpoint argument.")


if __name__ == "__main__":
    main()