src/4-representation — representation.py

1"""2representation.py — the validation package of "Universal Latent Representation in Finite Ring Continuum" (Akhtman,3Entropy 2026, 28, 40; doi 10.3390/e28010040), the paper 4-representation of the FRC corpus4(finite-ring-space/src/4-representation), added with the paper's predicate ledger (Appendix A, 17 September 2026; one5script since 24 September 2026, the three block scripts merged).6========================================================================================================================78One script, three blocks, thirteen checks (eleven exact, two chart), standard library only. Each check names the9predicate(s) of the paper's ledger it witnesses (LEDGER below; predicates cited as 4:XN) under a `# 4:XN (<key>)` marker,10the key the predicate's accession key, and the ledger's source column links the marker of the check that decides each11predicate (PREDICATES below; finitering.space/src/4-representation/#<key>). Where a predicate is12proved in Lean (lean/FrcCore/Representation.lean, no axioms; lean/FrcLedger/Representation.lean on Mathlib), the check13here is the instance the reader can run.1415    python3 representation.py     every block, results.json written; exit 1 if a check fails (≈ 10 s)16    python3 representation.py C   one block (A, B or C); no results.json17    from frc_4_representation import predicate; predicate("4:C1")    one predicate: its block runs once per session1819Blocks:  A  adequacy and the Universal Subspace Theorem on every finite model   EXACT          (4:B4, B5, C1–C4)20         B  the shell as host, the frames as charts, the worked instance         EXACT          (4:B6, C5)21         C  the finite ring geometry of embeddings                               CHART / EXACT  (4:E1–E3)2223Everything the blocks share:24  * finite models: the latent domain Z, the observations X_m, the representation spaces W_m as small sets, and the25    enumeration of every map between them (the theorem's clauses are decided on every configuration);26  * the shell datum: p = 4κ+1 prime, its primitive generators and its affine frames x ↦ a + b x;27  * the PASS/FAIL registry every block reports into (results.json).2829Kinds: EXACT checks are exhaustive or integer-pinned computations (a pass is a proof on the tested instances);30CHART checks decide a [chart] predicate in floating point with the closed forms checked.31"""32import os, json, sys, itertools, math, random3334SCRIPT = os.path.splitext(os.path.basename(__file__))[0]        # "representation": the one script, the name results.json and the site pages carry3536# The shells (p, κ): p = 4κ+1 prime.37SHELLS = [(5, 1), (13, 3), (17, 4), (29, 7), (37, 9), (41, 10)]3839# ----------------------------------------------------------------------------- registry40RESULTS = []4142# The paper's predicate ledger (Appendix A, predicates cited as 4:XN): the predicate(s) each check witnesses.43LEDGER = {44    "A1": "4:B4", "A2": "4:B5", "A3": "4:B5", "A4": "4:C1, 4:C2", "A5": "4:C3, 4:C4",45    "B1": "4:B6", "B2": "4:C5", "B3": "4:C1, 4:C3",46    "C1": "4:E1", "C2": "4:E1", "C3": "4:E2", "C4": "4:E3", "C5": "4:E3",47}4849BLOCK = {"A": "adequacy and the Universal Subspace Theorem on every finite model",   # check-id prefix -> the block (the function block_<letter> below)50         "B": "the shell as host, the frames as charts, the worked instance",51         "C": "the finite ring geometry of embeddings"}5253# the deciding check of each witnessed predicate: the one whose verdict decides the predicate's statement (the other checks that54# touch it are corroboration, listed by predicate() from the records)55PREDICATES = {56    "4:B4": "A1", "4:B5": "A2", "4:B6": "B1",57    "4:C1": "A4", "4:C2": "A4", "4:C3": "A5", "4:C4": "A5", "4:C5": "B2",58    "4:E1": "C1", "4:E2": "C3", "4:E3": "C4",59}60_RAN = set()                                            # blocks already run in this session (predicate() runs each once)6162def check(pid, label, ok, detail="", kind="EXACT"):63    """Record one predicate check. pid = package check id; LEDGER[pid] = the paper statement(s) decided."""64    ok = bool(ok)65    rows = LEDGER.get(pid, "")66    RESULTS.append({"id": pid, "rows": rows, "block": pid[0], "script": SCRIPT, "label": label, "ok": ok, "detail": detail, "kind": kind})67    print(f"  [{'PASS' if ok else 'FAIL'}] {pid:4s} {kind:6s} [{rows}] {label}" + (f"  --  {detail}" if detail else ""))68    return ok6970def summary(write=True):71    n_ok = sum(r["ok"] for r in RESULTS)72    print(f"\nSUMMARY: {n_ok}/{len(RESULTS)} checks passed" + ("" if n_ok == len(RESULTS) else "  <-- FAILURES"))73    if write:74        with open("results.json", "w") as f:75            json.dump(RESULTS, f, indent=1)76    return n_ok == len(RESULTS)7778def markers():79    """predicate label -> (script file, line) of its marker `# <paper>:<label> (<key>)`: the line of the check that decides it."""80    import re81    out = {}82    for i, line in enumerate(open(os.path.abspath(__file__), encoding="utf-8"), 1):83        m = re.match(r"\s*# ((?:\d+:[A-Z]+\d+[a-z]?(?: \(p\d{5}\))?)(?:, \d+:[A-Z]+\d+[a-z]?(?: \(p\d{5}\))?)*)\s*$", line)84        if m:85            for lab in re.findall(r"\d+:[A-Z]+\d+[a-z]?", m.group(1)): out.setdefault(lab, (SCRIPT + ".py", i))86    return out8788def _run_block(letter):89    if letter not in _RAN:90        globals()[f"block_{letter}"](); _RAN.add(letter)9192def predicate(label, lines=14):93    """Verify one ledger predicate: run the block of the check that decides it (once per session), print that check's source94    (from its marker) and every record that cites the predicate, and return True iff all pass."""95    pid = PREDICATES.get(label)96    if pid is None:97        print(f"{label}: no python witness (see the predicate's Lean witness or its source)"); return None98    citing = {i[0] for i, rows in LEDGER.items() if label in [t.strip() for t in rows.split(",")]}99    for b in sorted({pid[0]} | citing): _run_block(b)          # the deciding block and every block whose checks cite the predicate100    mk = markers().get(label)101    if mk:102        src = open(os.path.abspath(__file__), encoding="utf-8").read().split("\n")103        print(f"— {mk[0]}:{mk[1]} (the check that decides {label}: {pid})")104        for j in range(mk[1] - 1, min(mk[1] - 1 + lines, len(src))): print(f"{j + 1:5d}  {src[j]}")105    recs = [r for r in RESULTS if label in [t.strip() for t in r["rows"].split(",")]]106    ok = all(r["ok"] for r in recs)107    for r in recs:108        role = "(deciding)" if r["id"] == pid else "(corroborating)"109        print(f"  [{'PASS' if r['ok'] else 'FAIL'}] {r['id']:4s} {role:16s} {r['detail'][:150]}")110    print(f"{label}: {'VERIFIED' if ok and recs else 'FAILED'} — {len(recs)} record(s)")111    return ok112113def verify_all():114    """Run every block (those already run in this session are not re-run) and print the summary; True iff every check passed."""115    for b in sorted(BLOCK): _run_block(b)116    return summary(write=False)117118# ----------------------------------------------------------------------------- finite models119def maps(dom, cod):120    """Every map dom -> cod, as a dict."""121    for vals in itertools.product(cod, repeat=len(dom)):122        yield dict(zip(dom, vals))123124def injective(f, dom):125    return len({f[x] for x in dom}) == len(dom)126127def compose(f, g, dom):128    """x ↦ f(g(x)) on dom."""129    return {x: f[g[x]] for x in dom}130131def adequate(g, E, Z, W):132    """Definition 2: E ∘ g is a bijection Z -> W (W the codomain of E)."""133    phi = {z: E[g[z]] for z in Z}134    return len({phi[z] for z in Z}) == len(Z) == len(W)135136def inverse(phi, Z):137    """The inverse of a bijection given by its dict on Z."""138    return {phi[z]: z for z in Z}139140# ----------------------------------------------------------------------------- the shell datum141def is_prime(n):142    return n > 1 and all(n % q for q in range(2, int(n ** .5) + 1))143144def order(x, p):145    k, y = 1, x % p146    while y != 1:147        y = y * x % p; k += 1148    return k149150def generators(p):151    """The primitive generators of F_p^x, in increasing order."""152    return [g for g in range(2, p) if order(g, p) == p - 1]153154def frames(p):155    """The affine frames x ↦ a + b x of F_p (1:C2): p(p−1) of them."""156    return [(a, b) for a in range(p) for b in range(1, p)]157158def frame_map(frame, p):159    a, b = frame160    return {x: (a + b * x) % p for x in range(p)}161162for _p, _k in SHELLS:163    assert is_prime(_p) and _p == 4 * _k + 1, (_p, _k)164165# ------------------------------------------------------------------------------------------------------------166# block A: adequacy and the Universal Subspace Theorem on every finite model (4:B4, B5, C1–C4)167# Sections 3–4 of the paper, decided by exhaustion: the latent domain Z, the observations X and the representation168# spaces W are small sets, and every map g : Z → X, E : X → W is enumerated.  A1: adequacy (E ∘ g a bijection169# Z → W, Definition 2) forces g injective, and the adequate E are counted (|Z|! · |W|^{|X|−|Z|} for injective g, none170# otherwise).  A2: for every pair of adequate representations of one g, the transition ψ = φ₂ ∘ φ₁⁻¹ is the unique171# bijection W₁ → W₂ with E₂ ∘ g = ψ ∘ E₁ ∘ g; E₂ = ψ ∘ E₁ on all of X exactly when the two agree off g(Z), which172# fails in some configurations with X ⊋ g(Z) (counted).  A3: Lemma 1's set-level form, ψ(E₁(X)) = E₂(X), on every173# pair.  A4: Theorem 1 (i)–(iii) over every injective ι_m : W_m → U = F_5 — the charts ψ_m are injective, the174# transitions Ψ_{m→n} are bijections of the images composing as ψ_k ∘ ψ_m⁻¹, and the canonical ι_m = φ_m⁻¹ makes every175# chart the inclusion.  A5: Corollaries 1–2 — the lifts L_m = φ_m⁻¹ ∘ E_m invert g_m, are the unique preimage, and176# agree across modalities on every latent state.177def models(nZ, nX, nW):178    Z = list(range(nZ)); X = [f"x{i}" for i in range(nX)]; W = [f"w{i}" for i in range(nW)]179    return Z, X, W180181def block_A():182    """Block A — adequacy and the Universal Subspace Theorem on every finite model (EXACT): A1–A5."""183    # A1 adequacy forces g injective; the count of adequate E for a given g184    ok = True; det = []; total = 0185    for nZ, nX in [(1, 1), (1, 2), (2, 2), (2, 3), (3, 3), (3, 4), (2, 4)]:186        Z, X, W = models(nZ, nX, nZ)187        for g in maps(Z, X):188            n_ad = sum(adequate(g, E, Z, W) for E in maps(X, W)); total += 1189            if injective(g, Z):190                ok &= n_ad == math.factorial(nZ) * nZ ** (nX - nZ)191            else:192                ok &= n_ad == 0193        det.append(f"|Z|={nZ},|X|={nX}: {nX**nZ} maps g")194    # 4:B4 (p04008)195    check("A1", "adequacy (E o g bijective Z -> W) forces g injective; adequate E number |Z|! |W|^(|X|-|Z|) for injective g, 0 otherwise", ok,196             f"{total} observation maps over 7 model sizes; " + "; ".join(det[:3]))197198    # A2 the transition psi = phi_2 o phi_1^{-1}: unique bijection with E2 o g = psi o E1 o g; E2 = psi o E1 off g(Z) not forced199    ok = True; det = []; n_pairs = 0; n_off = 0; n_total_off = 0200    for nZ, nX in [(2, 2), (2, 3), (3, 3), (3, 4)]:201        Z, X, W1 = models(nZ, nX, nZ); W2 = [f"v{i}" for i in range(nZ)]202        for g in maps(Z, X):203            if not injective(g, Z): continue204            ads1 = [E for E in maps(X, W1) if adequate(g, E, Z, W1)]205            ads2 = [E for E in maps(X, W2) if adequate(g, E, Z, W2)]206            for E1 in ads1:207                phi1 = {z: E1[g[z]] for z in Z}; inv1 = inverse(phi1, Z)208                for E2 in ads2:209                    n_pairs += 1210                    phi2 = {z: E2[g[z]] for z in Z}211                    psi = {w: phi2[inv1[w]] for w in W1}212                    ok &= len(set(psi.values())) == nZ                                   # a bijection W1 -> W2213                    ok &= all(E2[g[z]] == psi[E1[g[z]]] for z in Z)                      # E2 o g = psi o E1 o g214                    others = [q for q in maps(W1, W2) if all(E2[g[z]] == q[E1[g[z]]] for z in Z)]215                    ok &= others == [psi]                                                # unique216                    if nX > nZ:217                        n_total_off += 1218                        if any(E2[x] != psi[E1[x]] for x in X): n_off += 1               # off g(Z) the equation can fail219        det.append(f"|Z|={nZ},|X|={nX}")220    ok &= n_off > 0221    # 4:B5 (p04009)222    check("A2", "psi = phi_2 o phi_1^-1 is the unique bijection W1 -> W2 with E2 o g = psi o E1 o g; E2 = psi o E1 on all of X only when X = g(Z)", ok,223             f"{n_pairs} pairs of adequate representations; off g(Z) the equation fails in {n_off} of {n_total_off} pairs with X != g(Z)")224225    # A3 Lemma 1 at the level of images: psi(E1(X)) = E2(X) = W2226    ok = True; n = 0227    for nZ, nX in [(2, 3), (3, 4)]:228        Z, X, W1 = models(nZ, nX, nZ); W2 = [f"v{i}" for i in range(nZ)]229        for g in maps(Z, X):230            if not injective(g, Z): continue231            ads1 = [E for E in maps(X, W1) if adequate(g, E, Z, W1)]232            ads2 = [E for E in maps(X, W2) if adequate(g, E, Z, W2)]233            for E1 in ads1:234                inv1 = inverse({z: E1[g[z]] for z in Z}, Z)235                for E2 in ads2:236                    psi = {w: E2[g[inv1[w]]] for w in W1}; n += 1237                    ok &= {psi[E1[x]] for x in X} == {E2[x] for x in X} == set(W2)238    check("A3", "Lemma 1 as images: psi(E1(X)) = E2(X) = W2 for every pair of adequate representations", ok, f"{n} pairs")239240    # A4 Theorem 1 (i)-(iii): every injective iota_m : W_m -> U = F_5; the canonical iota241    p = 5; U = list(range(p)); Z = [0, 2, 3]; X1 = ["a", "b", "c", "d"]; X2 = ["s", "t", "u"]242    g1 = {0: "b", 2: "d", 3: "a"}; g2 = {0: "t", 2: "s", 3: "u"}243    W1 = ["w0", "w1", "w2"]; W2 = ["v0", "v1", "v2"]244    E1 = {"a": "w2", "b": "w0", "c": "w0", "d": "w1"}; E2 = {"s": "v1", "t": "v2", "u": "v0"}245    assert adequate(g1, E1, Z, W1) and adequate(g2, E2, Z, W2)246    phi1 = {z: E1[g1[z]] for z in Z}; phi2 = {z: E2[g2[z]] for z in Z}247    ok = True; n = 0248    iotas = lambda W: [dict(zip(W, perm)) for perm in itertools.permutations(U, len(W))]249    for i1 in iotas(W1):250        psi1 = {z: i1[phi1[z]] for z in Z}251        ok &= injective(psi1, Z)                                                          # (i)252        for i2 in iotas(W2):253            psi2 = {z: i2[phi2[z]] for z in Z}; n += 1254            img1 = {psi1[z] for z in Z}; Psi = {psi1[z]: psi2[z] for z in Z}                  # (ii) Psi_{1->2} = psi2 o psi1^-1255            ok &= len(Psi) == len(Z) and set(Psi) == img1 and set(Psi.values()) == {psi2[z] for z in Z}256            back = {psi2[z]: psi1[z] for z in Z}257            ok &= all(back[Psi[u]] == u for u in img1)                                       # Psi_{2->1} o Psi_{1->2} = id258    inv1, inv2 = inverse(phi1, Z), inverse(phi2, Z)259    can1 = {w: inv1[w] for w in W1}; can2 = {w: inv2[w] for w in W2}                          # iota_m = phi_m^{-1}, into U260    ok &= all(can1[phi1[z]] == z and can2[phi2[z]] == z for z in Z)                         # (iii) psi_m = inclusion261    ok &= {can1[w] for w in W1} == {can2[w] for w in W2} == set(Z)262    # 4:C1 (p04011), 4:C2 (p04012)263    check("A4", "Theorem 1: psi_m = iota_m o phi_m injective for every injective iota_m; Psi_{m->n} a bijection of the images with inverse Psi_{n->m}; iota_m = phi_m^-1 makes every chart the inclusion of Z", ok,264             f"Z of size 3 in F_5, two modalities, {n} pairs of embeddings (60 x 60)")265266    # A5 Corollaries 1-2: the lifts267    L1 = {x: inv1[E1[x]] for x in X1}; L2 = {x: inv2[E2[x]] for x in X2}268    ok = all(L1[g1[z]] == z and L2[g2[z]] == z for z in Z)                                    # L_m o g_m = id269    ok &= all((E1[x] == phi1[z]) == (L1[x] == z) for x in X1 for z in Z)                     # L_m x the unique z with E_m x = phi_m z270    ok &= all(L1[g1[z]] == L2[g2[z]] for z in Z)                                             # cross-modal consistency271    ok &= L1["c"] == 0 and E1["c"] == E1["b"]                                                 # an unresolved observation lifts to the state it encodes272    # 4:C3 (p04013), 4:C4 (p04014)273    check("A5", "Corollary 1: L_m = phi_m^-1 o E_m inverts g_m and L_m x is the unique z with E_m x = phi_m z; Corollary 2: L_m(g_m z) = L_n(g_n z), psi o L_m o g_m = psi", ok,274             "the F_5 instance; the observation c (not in g_1(Z)) lifts to the state its code names")275276# ------------------------------------------------------------------------------------------------------------277# block B: the shell as host, the frames as charts, the worked instance (4:B6, C1, C3, C5)278# B1: a representation space of the size of the latent domain embeds in the shell (|W_m| = |Z| ≤ p), the least279# shell hosting a domain of N states is the least prime p = 4κ+1 ≥ N (tabulated for N ≤ 60), and the canonical280# ι_m = φ_m⁻¹ is exhibited for Z ⊂ F_13 with three modalities whose representation spaces are quantised integer281# vectors in Z^{d_m}.  B2: the charts of the shell that respect its arithmetic are its affine frames x ↦ a + b x282# (1:C2): p(p−1) of them, any two related by one affine map (simply transitive), so the transition Ψ_{m→n} between two283# frames is affine — on F_5, F_13, F_17.  B3: the F_13 instance end to end: Ψ_{m→n} between the three modalities,284# its composition law, and the lifts recovering every latent state from every observation.285def least_shell(N):286    p = max(N, 5)287    while not (is_prime(p) and p % 4 == 1): p += 1288    return p289290def block_B():291    """Block B — the shell as host, the frames as charts, the worked instance (EXACT): B1–B3."""292    # B1 the host: |W| = |Z| <= p; the least hosting shell; the canonical iota on F_13293    table = {N: least_shell(N) for N in range(2, 61)}294    ok = all(table[N] >= N and is_prime(table[N]) and table[N] % 4 == 1 for N in table)295    ok &= table[13] == 13 and table[14] == 17 and table[30] == 37 and table[42] == 53 and table[54] == 61296    p = 13; Z = [1, 2, 4, 7, 8, 11, 12]297    random.seed(4)298    mods = []299    for m, d in enumerate((2, 3, 5)):300        X = [f"x{m}_{i}" for i in range(9)]301        gz = random.sample(X, len(Z)); g = dict(zip(Z, gz))                                 # injective observation map302        codes = set()303        while len(codes) < len(Z): codes.add(tuple(random.randint(-8, 8) for _ in range(d)))  # W_m: distinct quantised vectors304        W = sorted(codes); phi = dict(zip(Z, W)); E = {x: random.choice(W) for x in X}305        for z in Z: E[g[z]] = phi[z]                                                        # adequate: E o g = phi bijective306        assert adequate(g, E, Z, W)307        inv = inverse(phi, Z); iota = {w: inv[w] for w in W}                              # iota_m = phi_m^-1 into F_13308        ok &= injective(iota, W) and all(iota[phi[z]] == z for z in Z) and {iota[w] for w in W} == set(Z)309        mods.append((X, g, W, phi, E, iota))310    ok &= all(len(W) == len(Z) <= p for _, _, W, _, _, _ in mods)311    # 4:B6 (p04010)312    check("B1", "|W_m| = |Z| <= p: the representation space embeds in the shell; the least hosting shell of N states is the least prime p = 4k+1 >= N; the canonical iota_m = phi_m^-1 exhibited on F_13", ok,313             "N=13->13, 14->17, 30->37, 42->53, 54->61; Z of size 7 in F_13, three modalities with codes in Z^2, Z^3, Z^5")314315    # B2 the frames as charts: simply transitive, the transition affine316    ok = True; det = []317    for p in (5, 13, 17):318        F = frames(p); ok &= len(F) == p * (p - 1)319        maps = {f: frame_map(f, p) for f in F}320        ok &= all(injective(maps[f], range(p)) for f in F)                               # every frame is a chart321        for f1 in F[:26]:322            m1 = maps[f1]; inv1 = {m1[x]: x for x in range(p)}323            for f2 in F:324                Psi = {m1[x]: maps[f2][x] for x in range(p)}                                 # Psi = psi_2 o psi_1^-1325                a, b = Psi[0], (Psi[1] - Psi[0]) % p326                ok &= b != 0 and all(Psi[u] == (a + b * u) % p for u in range(p))            # affine, invertible327        # simply transitive: for the frame (0,1) and any (c,d) exactly one affine map carries it328        for c in range(p):329            for d in range(1, p):330                sols = [(a, b) for a in range(p) for b in range(1, p) if a == c and b == d]331                ok &= len(sols) == 1332        det.append(f"p={p}: {len(F)} frames")333    # 4:C5 (p04015)334    check("B2", "the arithmetic charts of the shell are its p(p-1) affine frames; Psi_{m->n} between two frames is one invertible affine map (simply transitive)", ok, "; ".join(det))335336    # B3 the F_13 instance end to end337    ok = True338    (X1, g1, W1, phi1, E1, i1), (X2, g2, W2, phi2, E2, i2), (X3, g3, W3, phi3, E3, i3) = mods339    psi = [{z: io[ph[z]] for z in Z} for ph, io in ((phi1, i1), (phi2, i2), (phi3, i3))]340    ok &= all(ps[z] == z for ps in psi for z in Z)                                            # canonical: every chart the inclusion341    # general iota: random injective embeddings into F_13, the transitions and their composition law342    for _ in range(50):343        ios = [dict(zip(W, random.sample(range(p), len(W)))) for W in (W1, W2, W3)]344        ps = [{z: io[ph[z]] for z in Z} for ph, io in zip((phi1, phi2, phi3), ios)]345        ok &= all(injective(q, Z) for q in ps)346        T = lambda m, n: {ps[m][z]: ps[n][z] for z in Z}347        ok &= all(T(1, 2)[T(0, 1)[u]] == T(0, 2)[u] for u in T(0, 1))                        # Psi_{2->3} o Psi_{1->2} = Psi_{1->3}348        ok &= all(T(0, 0)[u] == u for u in T(0, 0))349    # the lifts350    L = [{x: inverse(ph, Z)[E[x]] for x in X} for X, E, ph in ((X1, E1, phi1), (X2, E2, phi2), (X3, E3, phi3))]351    ok &= all(L[0][g1[z]] == z and L[1][g2[z]] == z and L[2][g3[z]] == z for z in Z)352    ok &= all(L[m][x] in Z for m, X in enumerate((X1, X2, X3)) for x in X)353    check("B3", "the F_13 instance: canonical charts are the inclusion; for random embeddings the transitions compose, Psi_{n->k} o Psi_{m->n} = Psi_{m->k}; the three lifts recover every latent state", ok,354             "50 random triples of embeddings W_m -> F_13; 27 observations lifted")355356# ------------------------------------------------------------------------------------------------------------357# block C: the finite ring geometry of embeddings (4:E1, E2, E3)358# Section 6 of the paper.  C1 (CHART): the character chart of the shell, z ↦ (cos 2πkz/p, sin 2πkz/p)_{k<p−1}, is359# equivariant — a translation z ↦ z + a rotates plane k by 2πka/p — and has ‖Emb(z)‖² = p − 1 for every z: the whole360# chart lies on one sphere; a chart that is not equivariant (random) does not.  C2 (EXACT): the same in the shell's361# own arithmetic — the conjugate norm Σ_k g^{kz} g^{k(n−z)} equals n = p − 1 for every z and every generator g, and362# translation multiplies coordinate k by g^{ka}.  C3 (CHART): the quantisation count — the grid points Δ·Z^d within363# Δ/2 of a sphere of radius R grow like (R/Δ)^{d−1} (fitted exponents at d = 2, 3).  C4, C5 (EXACT): the Gödel364# code G(x) = ∏ p_i^{x_i} is injective on the box {0..4}³ over the primes 2, 3, 5 (125 distinct codes, maximum365# 810 000); reduced modulo the least prime above the maximum, q = 810 013, it stays injective, while smaller moduli366# collide; the two-prime code 2^a 3^b is injective on a, b ≤ 20 (the core instance), and signed coordinates are367# coded after a shift.368def emb(p, z):369    return [f(2 * math.pi * k * z / p) for k in range(1, p) for f in (math.cos, math.sin)]370371def block_C():372    """Block C — the finite ring geometry of embeddings (C1–C2 CHART; C3–C5 EXACT): C1–C5."""373    # C1 the character chart on the sphere (chart)374    ok = True; det = []375    for p, k in SHELLS[:4]:376        norms = [sum(c * c for c in emb(p, z)) for z in range(p)]377        ok &= all(abs(n - (p - 1)) < 1e-9 for n in norms)378        # equivariance: Emb(z + a) = R(a) Emb(z), R(a) the block rotation by 2 pi k a / p in plane k379        for a in range(1, p):380            for z in range(p):381                e, ez = emb(p, z + a), emb(p, z)382                for kk in range(1, p):383                    c, s = math.cos(2 * math.pi * kk * a / p), math.sin(2 * math.pi * kk * a / p)384                    x, y = ez[2 * (kk - 1)], ez[2 * (kk - 1) + 1]385                    ok &= abs(c * x - s * y - e[2 * (kk - 1)]) < 1e-9 and abs(s * x + c * y - e[2 * (kk - 1) + 1]) < 1e-9386        det.append(f"p={p}: |Emb|^2 = {p-1}")387    random.seed(1)388    rnd = [[random.gauss(0, 1) for _ in range(8)] for _ in range(13)]389    spread = max(sum(c * c for c in v) for v in rnd) - min(sum(c * c for c in v) for v in rnd)390    ok &= spread > 1                                                                       # a non-equivariant chart is not on a sphere391    # 4:E1 (p04018)392    check("C1", "the character chart z -> (cos 2 pi k z/p, sin 2 pi k z/p)_k has |Emb(z)|^2 = p-1 for every z and is translation-equivariant (block rotations); a random chart is not on a sphere", ok,393             "; ".join(det) + f"; random control: norm spread {spread:.1f}", kind="CHART")394395    # C2 the conjugate norm in the shell's arithmetic, exact396    ok = True; det = []397    for p, k in SHELLS:398        n = p - 1399        for g in generators(p):400            for z in range(n + 1):401                ok &= sum(pow(g, kk * z, p) * pow(g, kk * (n - z), p) for kk in range(n)) % p == n % p402            for z in range(n):403                for a in range(1, 4):404                    ok &= all(pow(g, kk * (z + a), p) == pow(g, kk * a, p) * pow(g, kk * z, p) % p for kk in range(n))405        det.append(f"p={p}: {len(generators(p))} generators")406    check("C2", "sum_k g^(kz) g^(k(n-z)) = n = p-1 in F_p for every z <= n and every generator; translation multiplies coordinate k by g^(ka)", ok, "; ".join(det[:4]))407408    # C3 the quantisation count on the sphere (chart): exponent d-1409    def count(d, r):410        """grid points of Z^d within 1/2 of the sphere of radius r (Delta = 1)."""411        rng = range(-int(r) - 1, int(r) + 2)412        if d == 2:413            return sum(1 for x in rng for y in rng if abs(math.hypot(x, y) - r) <= 0.5)414        return sum(1 for x in rng for y in rng for z in rng if abs(math.sqrt(x * x + y * y + z * z) - r) <= 0.5)415    ok = True; det = []416    for d in (2, 3):417        radii = list(range(10, 101, 10)) if d == 2 else list(range(5, 41, 5))418        cs = [count(d, r) for r in radii]419        xs = [math.log(r) for r in radii]; ys = [math.log(c) for c in cs]420        mx, my = sum(xs) / len(xs), sum(ys) / len(ys)421        slope = sum((x - mx) * (y - my) for x, y in zip(xs, ys)) / sum((x - mx) ** 2 for x in xs)   # least squares422        ok &= abs(slope - (d - 1)) < 0.15423        det.append(f"d={d}: R = {radii[0]}..{radii[-1]}, counts {cs[0]}..{cs[-1]}, slope {slope:.2f}")424    # 4:E2 (p04019)425    check("C3", "grid points within Delta/2 of the sphere of radius R number ~ (R/Delta)^(d-1): least-squares exponents within 0.15 of d-1 at d = 2, 3", ok, "; ".join(det), kind="CHART")426427    # C4 the Goedel code on the box {0..4}^3 over 2, 3, 5; reduction mod q428    box = [(a, b, c) for a in range(5) for b in range(5) for c in range(5)]429    G = {x: 2 ** x[0] * 3 ** x[1] * 5 ** x[2] for x in box}430    ok = len(set(G.values())) == len(box) == 125431    mx = max(G.values()); ok &= mx == 810000432    q = mx + 1433    while not is_prime(q): q += 1434    ok &= q == 810013 and len({v % q for v in G.values()}) == 125435    coll = {m: 125 - len({v % m for v in G.values()}) for m in (101, 1009, 10007, 100003)}436    ok &= coll[101] > 0                                                                    # below the maximum the guarantee lapses437    # 4:E3 (p04020)438    check("C4", "G(x) = 2^a 3^b 5^c is injective on {0..4}^3 (125 codes, max 810000); mod q = 810013 (the least prime above the maximum) injective by the bound; below it the bound gives nothing: mod 101 there are collisions", ok,439             f"collisions below the maximum: {coll} (none at 1009, 10007, 100003 is the accident of these residues, not the bound)")440441    # C5 the two-prime core instance and signed coordinates442    codes = {(a, b): 2 ** a * 3 ** b for a in range(21) for b in range(21)}443    ok = len(set(codes.values())) == 441444    signed = [(a, b, c) for a in range(-2, 3) for b in range(-2, 3) for c in range(-2, 3)]445    Gs = {x: 2 ** (x[0] + 2) * 3 ** (x[1] + 2) * 5 ** (x[2] + 2) for x in signed}446    ok &= len(set(Gs.values())) == 125 and max(Gs.values()) == 810000447    check("C5", "2^a 3^b injective on a, b <= 20 (441 codes); signed coordinates in {-2..2}^3 coded after the shift +2: 125 distinct codes, the same maximum", ok, "")448449if __name__ == "__main__":450    import time451    want = [a.upper() for a in sys.argv[1:]] or sorted(BLOCK)452    bad = [b for b in want if b not in BLOCK]453    if bad: sys.exit(f"no block {', '.join(bad)}: the blocks are {', '.join(sorted(BLOCK))}")454    t0 = time.time()455    for b in want:456        t = time.time(); _run_block(b); print(f"    [block {b}: {time.time() - t:.1f} s]")457    ok = summary(write=(want == sorted(BLOCK)))458    kinds = {}459    for r in RESULTS: kinds[r["kind"]] = kinds.get(r["kind"], 0) + 1460    print("by kind: " + ", ".join(f"{k} {v}" for k, v in sorted(kinds.items())) + f"; {len(RESULTS)} checks in {time.time() - t0:.1f} s" + ("; results.json written" if want == sorted(BLOCK) else ""))461    sys.exit(0 if ok else 1)462