#!/usr/bin/env python3
# SPDX-License-Identifier: MIT
# Copyright (c) 2026 Pablo Nogueira Grossi / G6 LLC
"""
book28/ch06-verify.py -- every number and quotation on book28/ch06-the-circle-comes-back.html. Run first (R24).
    python3 book28/ch06-verify.py [--downloads DIR]
  [1] Zois Lecture 4, Atiyah 1967 §2.2 and §2.4, Dugger §12 and §35: the sentences quoted, by PDF page
  [2] clutching: line bundles on S^2 glued by z^k; degree = winding number, and degrees add under tensor product
  [3] Atiyah's trick: the quarter-turn [[0,-I],[I,0]] joined to the identity through invertibles
  [4] Clifford algebras, exactly: the centre of the complex ones has period 2, of the real ones period 4
  [5] Dugger's KO(RP^n) = Z/2^f(n): f counts s <= n with s = 0,1,2,4 mod 8, so f(n+8) = f(n) + 4
  [6] the Lean: book28/CliffordSmall.lean
  [HONESTY]
"""
import os, re, subprocess, sys
from itertools import combinations
from pathlib import Path
import numpy as np
ROOT = Path(__file__).resolve().parent.parent
FAIL = []
def check(label, ok, detail=""):
    print(("PASS " if ok else "FAIL ") + label + (f"  -- {detail}" if detail else ""))
    if not ok: FAIL.append(label)
def dl():
    if "--downloads" in sys.argv: return Path(sys.argv[sys.argv.index("--downloads") + 1])
    for c in ("~/mnt/Downloads", "~/Downloads"):
        p = Path(os.path.expanduser(c))
        if p.is_dir(): return p
sq = lambda s: re.sub(r"\s+", "", s.replace("-\n", "")).lower()
def pages(name):
    return subprocess.run(["pdftotext", "-layout", str(dl() / name), "-"], stdout=subprocess.PIPE,
                          stderr=subprocess.DEVNULL, text=True).stdout.split("\f")

print("[1] the texts")
ZO = pages("18 LECTURES ON K-THEORY.pdf")
AT = pages("K-THEORY LECTURES BY NOTES BY M. F. A.TIYAH* D. W. ANDERSON.pdf")
DU = pages("A GEOMETRIC INTRODUCTION TO K-THEORY DANIEL DUGGER.pdf")
QS = [(ZO, "Zois", 72, "12 Lecture 4 (Bott Periodicity)"),
      (ZO, "Zois", 73, "Let b ∈ K −1 R be the generator corresponding to the function z 7→ 1/z"),
      (ZO, "Zois", 73, "where β(1) is the tautological line bundle"),
      (ZO, "Zois", 73, "and thus we obtain the Hopf line bundle"),
      (ZO, "Zois", 74, "which acts on R2 ⊕ R2 is homotopic to the identity"),
      (ZO, "Zois", 74, "The above is known as Atiyah’s trick."),
      (ZO, "Zois", 8, "there are no finite dimensional division algebras over R in dimensions other than 1, 2, 4 and 8"),
      (AT, "Atiyah", 48, "The fundamental theorem for K-theory is the periodicity theorem"),
      (AT, "Atiyah", 81, "abelian group Z generated by [H] - [1]"),
      (DU, "Dugger", 85, "found an 8-fold periodicity (with respect to k) in the case of real vector bundles, and a 2-fold periodicity in the case of complex bundles"),
      (DU, "Dugger", 85, "Bott’s periodicity theorems are of paramount importance in modern algebraic topology"),
      (DU, "Dugger", 289, "s ≡ 0, 1, 2, or 4 mod 8")]
for T, who, pg, q in QS:
    check(f'{who} PDF p.{pg}: "{q[:60]}"', sq(q) in sq(T[pg - 1]))

print("[2] clutching: the bundle on S^2 glued along the equator by z -> z^k")
def wn(f, M=4096):
    z = np.exp(2j * np.pi * np.arange(M) / M); w = f(z)
    return round(float(np.angle(np.roll(w, -1) / w).sum() / (2 * np.pi)))
deg = {k: wn(lambda z, k=k: z ** k) for k in range(-3, 4)}
check("the clutching function z^k has winding number k, k = -3..3 (the degree, i.e. first Chern number, of the bundle)",
      all(deg[k] == k for k in deg), str(deg))
check("Zois' generator b is z -> 1/z: winding number -1", wn(lambda z: 1 / z) == -1)
pairs = [(a, b) for a in range(-2, 3) for b in range(-2, 3)]
check("tensor product multiplies clutching functions, and the degrees add: wn(z^a z^b) = a + b for all 25 pairs",
      all(wn(lambda z, a=a, b=b: z ** a * z ** b) == a + b for a, b in pairs))
f = lambda z: (z - 0.3) * (z + 0.2j) / (z - 3)
th = np.linspace(0, 2 * np.pi, 800, endpoint=False); zz = np.exp(1j * th)
g = lambda z: -(z ** 2) / 3                      # z^2, scaled to match f's size near the circle
mins = [np.abs((1 - s) * f(zz) + s * g(zz)).min() for s in np.linspace(0, 1, 201)]
check("same winding, same bundle: (z-.3)(z+.2i)/(z-3) has winding 2, and the straight-line homotopy to -z^2/3 never vanishes on the circle",
      wn(f) == 2 and wn(g) == 2 and min(mins) > 0.01, f"min |f_s| = {min(mins):.3f}")

print("[3] Atiyah's trick: [[0,-I],[I,0]] on R^2 + R^2 is homotopic to the identity")
I2 = np.eye(2); Z2 = np.zeros((2, 2))
R = lambda t: np.block([[np.cos(t) * I2, -np.sin(t) * I2], [np.sin(t) * I2, np.cos(t) * I2]])
ts = np.linspace(0, np.pi / 2, 401)
check("R(0) = identity, R(pi/2) = [[0,-I],[I,0]]", np.allclose(R(0), np.eye(4)) and np.allclose(R(np.pi / 2), np.block([[Z2, -I2], [I2, Z2]])))
check("det R(t) = 1 at all 401 points: the path never leaves the invertibles", all(abs(np.linalg.det(R(t)) - 1) < 1e-12 for t in ts))

print("[4] Clifford algebras, exactly: monomials e_S, S a subset of {1..n}")
def mul(S, T, sqr):
    """e_S e_T = sign * e_{S xor T}; generators anticommute and square to sqr (+1 or -1)."""
    sign = 1; S = list(S)
    for t in sorted(T):
        after = sum(1 for s in S if s > t)          # move e_t left past larger indices already there
        sign *= (-1) ** after
        if t in S: sign *= sqr; S.remove(t)
        else: S.append(t); S.sort()
    return sign, tuple(S)
def centre(n, sqr):
    subsets = [tuple(c) for k in range(n + 1) for c in combinations(range(1, n + 1), k)]
    gens = [(i,) for i in range(1, n + 1)]
    return [S for S in subsets if all(mul(S, g, sqr) == mul(g, S, sqr) for g in gens)]
rows = []
for n in range(0, 17):
    Zc = centre(n, +1)                                # complex: the sign convention does not matter over C
    Zr = centre(n, -1)                                # real Cl_{0,n}: e_i^2 = -1
    top = tuple(range(1, n + 1))
    w2 = mul(top, top, -1)[0] if n else 1             # omega^2 in Cl_{0,n}
    kind = "R" if len(Zr) == 1 else ("C" if w2 == -1 else "R+R")
    rows.append((n, len(Zc), kind, w2))
print("      n  dim centre (complex)  centre (real Cl_0,n)  omega^2")
for r in rows: print("     %2d  %d  %-4s  %+d" % r)
check("complex Clifford algebras: centre of dimension 1 for n even, 2 for n odd, n = 0..16 (period 2)",
      all(r[1] == (1 if r[0] % 2 == 0 else 2) for r in rows))
check("real Cl_0,n: centre R for n even; for n odd, C when n = 1 mod 4 and R+R when n = 3 mod 4 (period 4)",
      all(r[2] == ("R" if r[0] % 2 == 0 else ("C" if r[0] % 4 == 1 else "R+R")) for r in rows))
check("the pattern of centres repeats every 4 for n = 0..16", all(rows[n][2] == rows[n + 4][2] for n in range(13)))

print("[5] Dugger 35.14: KO(RP^n) = Z/2^f, f(n) = #{0 < s <= n : s = 0, 1, 2, 4 mod 8}")
fcount = lambda n: sum(1 for s in range(1, n + 1) if s % 8 in (0, 1, 2, 4))
F = [fcount(n) for n in range(1, 33)]
print("     f(1..32) =", F)
check("f(n + 8) = f(n) + 4 for n = 1..24: four new factors of 2 every eight dimensions", all(fcount(n + 8) == fcount(n) + 4 for n in range(1, 25)))
check("|KO(RP^n)| for n = 1..8: 2, 4, 4, 8, 8, 8, 8, 16", [2 ** fcount(n) for n in range(1, 9)] == [2, 4, 4, 8, 8, 8, 8, 16])

print("[6] the Lean")
lean = (ROOT / "book28/CliffordSmall.lean").read_text(encoding="utf-8")
names = re.findall(r"^theorem (\w+)", lean, re.M)
check("CliffordSmall.lean: qi_sq, qj_sq, qi_qj_anticomm, J_sq, J_det", names == ["qi_sq", "qj_sq", "qi_qj_anticomm", "J_sq", "J_det"])
check("no sorry in code", "sorry" not in re.sub(r"/-.*?-/|--[^\n]*", "", lean, flags=re.S))
ax = (ROOT / "book28/cliffordsmall.axioms.txt").read_text()
check("axiom report: all 5 on [propext, Classical.choice, Quot.sound]", ax.count("[propext, Classical.choice, Quot.sound]") == 5)
check("lakefile builds it in lean_lib Book28", "`CliffordSmall" in (ROOT / "lakefile.lean").read_text())

print("[HONESTY]")
print("  Bott periodicity itself is quoted, not proved. [2] computes winding numbers numerically and")
print("  takes from the sources that the winding number of the clutching function is the bundle's degree.")
print("  [4] is exact sign arithmetic on monomials; it finds the period-4 pattern of the centres, not the")
print("  full period 8, which needs the division algebra (R, C or H) of each simple factor and is quoted.")
print("  [5] evaluates Dugger's formula; it does not compute KO.")
print(f"\n{len(FAIL)} FAIL" + (": " + ", ".join(FAIL) if FAIL else ""))
sys.exit(1 if FAIL else 0)