"""v108 -- The Pascal Ladder Theorem: carrier selection g = 5 is EXACTLY
equivalent to the degree-2 bound K = 2; the red-team Target-B residual
becomes one named hypothesis with zero slack.  [I]/[L] + [P].

v106 NAMED the hypothesis (Quadratic Boundary Locality); this script
supplies the missing arithmetic theorem that makes the hypothesis carry the
whole carrier choice:

  [I] 1. PASCAL LADDER THEOREM.  The closure condition
             2^{g-1} = sum_{k<=K} C(g,k)
         has, for every K, EXACTLY ONE solution: g = 2K+1
         (verified K = 1..6 over g = 1..60).  Structural reason, checked:
         for odd g the midpoint identity sum_{k<=(g-1)/2} C(g,k) = 2^{g-1}
         holds by binomial symmetry (so g = 2K+1 always solves), and for
         even g the strict straddle
             sum_{k<g/2} = (2^g - C(g,g/2))/2  <  2^{g-1}  <  sum_{k<=g/2}
         excludes every even g; monotonicity in K gives uniqueness.
  [I] 2. EXACT EQUIVALENCE (the sharpening of red-team Target B): the
         carrier selection "g = 5" is EQUIVALENT to the truncation degree
         "K = 2" -- zero slack in either direction.  The Pascal SELECTION
         residual (CAR.PASCAL.01 / REDTEAM.B.01, typed [A]/[P]) is
         therefore exactly ONE hypothesis: Quadratic Boundary Locality
         (the seam certifies code degrees <= 2).  QBL => K=2 <=> g=5 =>
         dim S+ = 16 = 1+10+5 => D5 => (with the family geometry) E8.
  [I] 3. NEIGHBOUR-WORLD CONTROLS (the ladder is a real axis of worlds):
         K = 1 -> g = 3:  code 2^2 = 4 = 1+3,    N_fam = (4-1)/3   = 1
                          (a ONE-family world);
         K = 2 -> g = 5:  code 2^4 = 16 = 1+10+5, N_fam = (16-1)/5 = 3;
         K = 3 -> g = 7:  code 2^6 = 64 = 1+21+35+7, N_fam = 63/7  = 9
                          (a NINE-family world);
         K = 4 -> g = 9:  N_fam = 255/9 NOT an integer (9 is not prime;
                          Fermat fails) -- the world is inconsistent.
  [I] 4. OVERDETERMINATION CROSS-CHECK (ties v14 to the ladder): among
         the ladder worlds g = 2K+1, the established rank condition
         g + N_fam = 8 = rank E8 (v14) selects g = 5 ALONE
         (3+1 = 4, 5+3 = 8, 7+9 = 16, ...).  Two INDEPENDENT selections
         -- the degree bound (QBL, [P]) and the rank-8 closure ([I], v14)
         -- agree on the same world.
  [P] 5. THE ONE HYPOTHESIS, precisely stated (recorded, not claimed):
         QBL = "the seam Calderon datum is a single two-point kernel, and
         the carrier code is generated by the degrees that kernel
         certifies, i.e. K <= 2".  If proven (from reflection positivity
         / the bilinear nature of the OS pairing), the carrier choice
         upgrades [A]/[P] -> [L] along the v106 chain.  Nothing here
         closes it; this script removes all slack around it.
"""
import sympy as sp

from tfpt_constants import check, summary, reset, N_fam, dim_Splus, rankE8


def closure_solutions(K, gmax=60):
    return [g for g in range(1, gmax + 1)
            if 2**(g - 1) == sum(sp.binomial(g, k) for k in range(K + 1))]


def run():
    reset()
    print("v108 Pascal ladder (carrier selection g=5 <=> degree bound K=2)")

    # 1. the ladder theorem
    check("PASCAL LADDER: for K = 1..6 the closure 2^{g-1} = "
          "sum_{k<=K} C(g,k) has exactly one solution g = 2K+1 "
          "(scan g = 1..60)",
          all(closure_solutions(K) == [2 * K + 1] for K in range(1, 7)))
    check("structural reason (odd g): midpoint identity "
          "sum_{k<=(g-1)/2} C(g,k) = 2^{g-1} for g = 3,5,...,15",
          all(sum(sp.binomial(g, k) for k in range((g - 1) // 2 + 1))
              == 2**(g - 1) for g in range(3, 16, 2)))
    check("structural reason (even g): strict straddle "
          "sum_{k<g/2} < 2^{g-1} < sum_{k<=g/2} for g = 2,4,...,16 "
          "(no even solutions)",
          all(sum(sp.binomial(g, k) for k in range(g // 2))
              < 2**(g - 1)
              < sum(sp.binomial(g, k) for k in range(g // 2 + 1))
              for g in range(2, 17, 2)))

    # 2. the exact equivalence
    check("EXACT EQUIVALENCE: g = 5 <=> K = 2 (zero slack): the Pascal "
          "selection residual (CAR.PASCAL.01/REDTEAM.B.01) IS the single "
          "hypothesis Quadratic Boundary Locality",
          closure_solutions(2) == [5] and 2 * 2 + 1 == 5)
    check("the chain after K = 2: g = 5 => dim S+ = 2^4 = 16 = 1+10+5 "
          "=> N_fam = (16-1)/5 = 3, rank E8 = g + N_fam = 8 "
          "(tfpt_constants re-verified)",
          dim_Splus == 16 == 1 + 10 + 5
          and N_fam == 3 == (2**4 - 1) // 5 and rankE8 == 8)

    # 3. neighbour-world controls
    worlds = {}
    for K in (1, 2, 3, 4):
        g = 2 * K + 1
        code = 2**(g - 1)
        worlds[K] = (g, code, sp.Rational(code - 1, g))
    check("NEIGHBOUR WORLDS: K=1 -> (g=3, code 4, N_fam=1); K=2 -> "
          "(5, 16, 3); K=3 -> (7, 64, 9); K=4 -> (9, 256, 255/9 NOT "
          "integer: inconsistent world)",
          worlds[1] == (3, 4, 1) and worlds[2] == (5, 16, 3)
          and worlds[3] == (7, 64, 9)
          and not worlds[4][2].is_integer)

    # 4. overdetermination cross-check
    rank_sel = [K for K in (1, 2, 3)
                if worlds[K][0] + worlds[K][2] == 8]
    check("OVERDETERMINATION: among ladder worlds, g + N_fam = 8 = "
          "rank E8 (v14) selects K = 2 ALONE (3+1=4, 5+3=8, 7+9=16) -- "
          "two independent selections agree",
          rank_sel == [2])

    # 5. the one hypothesis
    check("THE ONE HYPOTHESIS [P] (recorded, not claimed): QBL = 'the "
          "seam Calderon datum is a single two-point kernel; the carrier "
          "code is generated by the degrees it certifies (K <= 2)'. If "
          "proven from reflection positivity, the carrier choice upgrades "
          "[A]/[P] -> [L] along QBL => K=2 <=> g=5 => 16 => D5 => E8",
          True)

    return summary("v108 Pascal ladder")


if __name__ == "__main__":
    raise SystemExit(1 if run() else 0)