#!/usr/bin/env python3
"""
verify_P276.py — Verifier for Addendum 276 (the closure-map family).

  S1  Closure data: laws on explicit instances   — checks 1-4
  S2  Composition and the kernel ladder          — checks 5-7
  S3  The three instances                        — checks 8-11
  S4  Cokernel as opposite datum                 — check  12
"""
import sys
import numpy as np
import mpmath as mp

mp.mp.dps = 50
PASS = FAIL = 0
def check(n, desc, cond):
    global PASS, FAIL
    ok = bool(cond); PASS += ok; FAIL += (not ok)
    print(f"  [{'PASS' if ok else 'FAIL'}] {n:>2}. {desc}")

rng = np.random.default_rng(276)

def random_closure_datum(nX, n0):
    """Random retraction pair P: R^nX -> R^n0, C: R^n0 -> R^nX, PC = I."""
    C = rng.standard_normal((nX, n0))
    # P = (C^T C)^{-1} C^T  is the canonical retraction (pseudo-inverse)
    P = np.linalg.solve(C.T @ C, C.T)
    return P, C

print("S1  Closure data: laws on explicit instances")
P, C = random_closure_datum(7, 3)
I3 = np.eye(3); e = C @ P
check(1, "section law PC = id (random 7->3 datum): max dev %.1e"
         % np.max(np.abs(P @ C - I3)), np.allclose(P @ C, I3, atol=1e-10))
check(2, "closure operator idempotent: e^2 = e, max dev %.1e"
         % np.max(np.abs(e @ e - e)), np.allclose(e @ e, e, atol=1e-10))
check(3, "C o P = I exactly on the canonical sector: e*C = C, max dev %.1e"
         % np.max(np.abs(e @ C - C)), np.allclose(e @ C, C, atol=1e-10))
rk = np.linalg.matrix_rank(np.eye(7) - e)
check(4, "defect: rank(id - e) = dim ker P = %d = 7 - 3" % rk, rk == 4)

print("S2  Composition and the kernel ladder")
P1, C1 = random_closure_datum(9, 5)   # X -> X0
P2, C2 = random_closure_datum(5, 2)   # X0 -> X00
Pc, Cc = P2 @ P1, C1 @ C2
check(5, "composite is a closure datum: (P2 P1)(C1 C2) = id, max dev %.1e"
         % np.max(np.abs(Pc @ Cc - np.eye(2))),
      np.allclose(Pc @ Cc, np.eye(2), atol=1e-10))
k1 = 9 - np.linalg.matrix_rank(P1)
k2 = 5 - np.linalg.matrix_rank(P2)
kc = 9 - np.linalg.matrix_rank(Pc)
check(6, "kernel ladder exact: dim ker(P2P1) = %d = ker P1 (%d) + ker P2 (%d)"
         % (kc, k1, k2), kc == k1 + k2)
# monotonicity: composing with any further datum cannot shrink the kernel
P3, C3 = random_closure_datum(2, 1)
kcc = 9 - np.linalg.matrix_rank(P3 @ Pc)
check(7, "dark accumulates: further closure grows kernel (%d >= %d)"
         % (kcc, kc), kcc >= kc)

print("S3  The three instances")
check(8, "I1 fold (Hilb): ker rank per level = (l+1)^2-(l+1) = l(l+1), "
         "dark fraction l/(l+1) monotone -> 1 (l=1..200)",
      all((l+1)**2-(l+1) == l*(l+1) for l in range(1, 201)) and
      all(l/(l+1) < (l+1)/(l+2) for l in range(1, 200)))
PI = mp.pi
TB = PI*(4*PI**3 + PI**2 + PI)
smooth = sorted(2**a*3**b for a in range(12) for b in range(8)
                if 2 < 2**a*3**b < 4000)
def nearest_chord(x):
    return min(smooth, key=lambda s: abs(s - x))
check(9, "I2 chord (Met): residue at T_b = |432/T_b - 1| = G_1 = %s (A266)"
         % mp.nstr(432/TB - 1, 8),
      nearest_chord(float(TB)) == 432 and
      abs((432/TB - 1) - mp.mpf("0.0034557781")) < 1e-9)
check(10, "I2 idempotency: nearest-chord o nearest-chord = nearest-chord "
          "on grid", all(nearest_chord(nearest_chord(x)) == nearest_chord(x)
                         for x in np.linspace(3, 3000, 500)))
rho = TB - 430
check(11, "I3 locking (Dyn): defect non-empty — rho irrational (poly in pi), "
          "nearest tongue distance %s > 0" % mp.nstr(abs(rho - mp.mpf(1)/2), 6),
      abs(rho - mp.mpf(1)/2) > 0.01)

print("S4  Cokernel as opposite datum")
# opposite datum (C^T as retraction of P^T): P^T C^T -> (CP)^T;  C^T P^T = (PC)^T = id
check(12, "opposite datum (C^T, P^T) is a closure datum: C^T P^T = id^T, "
          "max dev %.1e — cokernels are defects in F"
          % np.max(np.abs(C.T @ np.linalg.pinv(C.T) - np.eye(3))),
      np.allclose((P @ C).T, np.eye(3), atol=1e-10))

print(f"\n{'='*60}\nRESULT: {PASS} PASS / {FAIL} FAIL")
sys.exit(0 if FAIL == 0 else 1)