The validation package of Incompleteness Without Infinity: one script, godel.py, 7 blocks, standard library only, one check per predicate of the paper's predicate ledger — 24 of 24 checks passing. The script is rendered below with an anchor per line; its markers (# 25:C1 (p25010): the predicate and its key) are the checks the ledger predicates cite, and the block index opens each block at its definition. The notebook frc-25-godel.ipynb runs one cell per predicate on Google Colab (its generator make_notebook.py). Installed from this site as a named requirement: pip install frc-25-godel --find-links https://finitering.space/pkg/ (the sdist frc-25-godel-20261012.tar.gz).
Blocks: A (3) · B (3) · C (6) · D (5) · E (2) · F (2) · G (3) — the predicates each decides in parentheses.
1"""2godel.py — the validation package of "Incompleteness Without Infinity" (Akhtman, preprint 2026; Preprints3doi 10.20944/preprints202607.0850.v1), the paper 25-godel of the FRC corpus (finite-ring-space/src/25-godel), added with4the paper's predicate ledger (Appendix A, 3 October 2026).5========================================================================================================================67One script, seven blocks, twenty-four checks, standard library only. Each check names the predicate(s) of the paper's ledger8it witnesses (LEDGER below; predicates cited as 25:XN) under a `# 25:XN (<key>)` marker, the key the predicate's accession9key, and the ledger's source column links the marker of the check that decides each predicate (PREDICATES below;10finitering.space/src/25-godel/#<key>). Where a predicate is proved in Lean (lean/FrcCore/Godel.lean, no axioms;11lean/FrcLedger/Godel.lean on Mathlib), the check here is the instance the reader can run.1213 python3 godel.py every block, results.json written; exit 1 if a check fails (≈ 2 min)14 python3 godel.py D one block (A–G); no results.json15 from frc_25_godel import predicate; predicate("25:F1") one predicate: its block runs once per session1617Blocks: A Gödel's hypotheses over a finite structure (Section 3) EXACT (25:C1, C2, C5)18 B the part and the whole: collisions, aliasing, the wrap (Section 4) EXACT (25:D1, D3, D4; corroborates J2)19 C the reach bound and the horizon's counting facts (Sections 5.1, 5.3, 5.4) EXACT (25:E1, E2, E4, G1, G2, G7)20 D the diagonal under finitude: mention cost, the template, density (5.2) EXACT (25:F1–F4, F6)21 E fragment truth: the pairing prefix and the guessed labels (Section 5.3) EXACT (25:G4, G5)22 F second-order decidability and the trichotomy's middle cell (Section 6) EXACT (25:H2, H5)23 G the window below the threshold: decoders, the dense-coded instance (5.2) EXACT (25:F7, F8, G8)2425Everything the blocks share:26 * the running example M_p = ({0,…,p−1}; 0, 1, +, ×), arithmetic modulo a prime, with its tables read on demand;27 * a prenex evaluator that builds the whole evaluation object (no short-circuit) and counts its matrix evaluations;28 * the certificate format of the wrap lemma: a record of term steps, each checked by one table lookup, and its verifier;29 * every formula over M_2 up to a given length, written out, with its truth table and free variables (the complete enumerations30 of block D), and an independent reader of the written formula, against which the tables are checked;31 * the PASS/FAIL registry every block reports into (results.json).32Block G has its own formulas, printer and model checker (the function _dense).3334Kinds: every check is EXACT — an exhaustive or integer-pinned computation, no floating point; a pass is a proof on the35tested instances. The counts a label states are asserted by the check. Where a check works on a sample, its label says so and36the sample is fixed: the sentences of A2, C5 and F2 (a list of eight), the completions of two certificates in B3 (seeded), the37maps at N = 3 in D2 (every 37th), the matrix family over M_5 in E1. D3 and D5 decide ranges of structures and the base38cases of t(M) < m; the comment of block D carries the proofs for every structure. G1 and G2 model-check written formulas39on small prime fields, G2 and G3 build the instance as strings and sample the positions of lambda (seeded); the comment of40block G carries the proofs for the fields of the instance, where no model check is possible.41"""42import os, json, sys, itertools, math, random43from fractions import Fraction4445SCRIPT = os.path.splitext(os.path.basename(__file__))[0] # "godel": the one script, the name results.json and the site pages carry4647# ----------------------------------------------------------------------------- registry48RESULTS = []4950# The paper's predicate ledger (Appendix A, predicates cited as 25:XN): the predicate(s) each check witnesses.51LEDGER = {52 "A1": "25:C1", "A2": "25:C2", "A3": "25:C5",53 "B1": "25:D1", "B2": "25:D3", "B3": "25:D4, 25:J2",54 "C1": "25:E1", "C2": "25:E2", "C3": "25:E4", "C4": "25:G1", "C5": "25:G2", "C6": "25:G7",55 "D1": "25:F1", "D2": "25:F2", "D3": "25:F4", "D4": "25:F3", "D5": "25:F6",56 "E1": "25:G4", "E2": "25:G5",57 "F1": "25:H2", "F2": "25:H5",58 "G1": "25:F7", "G2": "25:F8", "G3": "25:G8",59}6061BLOCK = {"A": "Gödel's hypotheses over a finite structure", # check-id prefix -> the block (the function block_<letter> below)62 "B": "the part and the whole: collisions, aliasing, the wrap",63 "C": "the reach bound and the horizon's counting facts",64 "D": "the diagonal under finitude: mention cost, the template, density",65 "E": "fragment truth: the pairing prefix and the guessed labels",66 "F": "second-order decidability and the trichotomy's middle cell",67 "G": "the window below the threshold: decoders, the dense-coded instance"}6869# the deciding check of each witnessed predicate: the one whose verdict decides the predicate's statement (the other checks that70# touch it are corroboration, listed by predicate() from the records)71PREDICATES = {72 "25:C1": "A1", "25:C2": "A2", "25:C5": "A3",73 "25:D1": "B1", "25:D3": "B2", "25:D4": "B3",74 "25:E1": "C1", "25:E2": "C2", "25:E4": "C3", "25:G1": "C4", "25:G2": "C5", "25:G7": "C6",75 "25:F1": "D1", "25:F2": "D2", "25:F4": "D3", "25:F3": "D4", "25:F6": "D5",76 "25:G4": "E1", "25:G5": "E2",77 "25:H2": "F1", "25:H5": "F2",78 "25:F7": "G1", "25:F8": "G2", "25:G8": "G3",79}80_RAN = set() # blocks already run in this session (predicate() runs each once)81T_EXACT = {} # (a, m) -> (d, fit_table), computed in D3 and read in D5 (block D)8283def check(pid, label, ok, detail="", kind="EXACT"):84 """Record one predicate check. pid = package check id; LEDGER[pid] = the paper statement(s) decided."""85 ok = bool(ok)86 rows = LEDGER.get(pid, "")87 RESULTS.append({"id": pid, "rows": rows, "block": pid[0], "script": SCRIPT, "label": label, "ok": ok, "detail": detail, "kind": kind})88 print(f" [{'PASS' if ok else 'FAIL'}] {pid:4s} {kind:6s} [{rows}] {label}" + (f" -- {detail}" if detail else ""))89 return ok9091def summary(write=True, expect=None):92 """Print the verdict and (write=True) store results.json. `expect` lists the check ids that must have run: a check that93 never reported fails the summary, as a check that reported FAIL does."""94 n_ok = sum(r["ok"] for r in RESULTS)95 ran = sorted(r["id"] for r in RESULTS)96 census = expect is None or ran == sorted(expect)97 print(f"\nSUMMARY: {n_ok}/{len(RESULTS)} checks passed" + ("" if n_ok == len(RESULTS) else " <-- FAILURES"))98 if not census: print(f" <-- CENSUS: expected {sorted(expect)}, ran {ran}")99 if write:100 with open("results.json", "w") as f:101 json.dump(RESULTS, f, indent=1)102 return n_ok == len(RESULTS) and census103104def markers():105 """predicate label -> (script file, line) of its marker `# <paper>:<label> (<key>)`: the line of the check that decides it."""106 import re107 out = {}108 for i, line in enumerate(open(os.path.abspath(__file__), encoding="utf-8"), 1):109 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)110 if m:111 for lab in re.findall(r"\d+:[A-Z]+\d+[a-z]?", m.group(1)): out.setdefault(lab, (SCRIPT + ".py", i))112 return out113114def _run_block(letter):115 if letter not in _RAN:116 globals()[f"block_{letter}"](); _RAN.add(letter)117118def predicate(label, lines=14):119 """Verify one ledger predicate: run the block of the check that decides it (once per session), print that check's source120 (from its marker) and every record that cites the predicate, and return True iff all pass."""121 pid = PREDICATES.get(label)122 if pid is None:123 print(f"{label}: no python witness (see the predicate's Lean witness or its source)"); return None124 citing = {i[0] for i, rows in LEDGER.items() if label in [t.strip() for t in rows.split(",")]}125 for b in sorted({pid[0]} | citing): _run_block(b) # the deciding block and every block whose checks cite the predicate126 mk = markers().get(label)127 if mk:128 src = open(os.path.abspath(__file__), encoding="utf-8").read().split("\n")129 print(f"— {mk[0]}:{mk[1]} (the check that decides {label}: {pid})")130 for j in range(mk[1] - 1, min(mk[1] - 1 + lines, len(src))):131 if not src[j].strip(): break # the check ends at the first blank line132 print(f"{j + 1:5d} {src[j]}")133 recs = [r for r in RESULTS if label in [t.strip() for t in r["rows"].split(",")]]134 ok = all(r["ok"] for r in recs) and any(r["id"] == pid for r in recs) # every citing record passes, and the deciding check reported135 for r in recs:136 role = "(deciding)" if r["id"] == pid else "(corroborating)"137 print(f" [{'PASS' if r['ok'] else 'FAIL'}] {r['id']:4s} {role:16s} {r['detail'][:150]}")138 print(f"{label}: {'VERIFIED' if ok else 'FAILED'} — {len(recs)} record(s)")139 return ok140141def verify_all():142 """Run every block (those already run in this session are not re-run) and print the summary; True iff every check passed."""143 for b in sorted(BLOCK): _run_block(b)144 return summary(write=False, expect=list(LEDGER))145146# ----------------------------------------------------------------------------- shared primitives147def is_prime(n):148 """Deterministic Miller–Rabin on the first twelve prime bases (exact below 3.3e24)."""149 if n < 2: return False150 small = (2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37)151 for q in small:152 if n % q == 0: return n == q153 d, s = n - 1, 0154 while d % 2 == 0: d //= 2; s += 1155 for a in small:156 x = pow(a, d, n)157 if x in (1, n - 1): continue158 for _ in range(s - 1):159 x = x * x % n160 if x == n - 1: break161 else: return False162 return True163164def next_prime_1mod4(n):165 """The least prime p >= n with p = 1 (mod 4)."""166 n += (1 - n) % 4167 while not is_prime(n): n += 4168 return n169170P_SMALL, P_MID, P_BIG = 13, next_prime_1mod4(10 ** 6), next_prime_1mod4(10 ** 18) # 13, 1000033, 1000000000000000009171assert (P_MID, P_BIG) == (1000033, 10 ** 18 + 9)172173def iroot(n, k):174 """floor(n^(1/k)) by integer bisection."""175 lo, hi = 0, 1176 while hi ** k <= n: hi *= 2177 while lo < hi:178 mid = (lo + hi + 1) // 2179 if mid ** k <= n: lo = mid180 else: hi = mid - 1181 return lo182183def catalan(k):184 """The Catalan number C_k by the exact integer recurrence C_{i+1} = C_i · 2(2i+1)/(i+2)."""185 c = 1186 for i in range(k): c = c * 2 * (2 * i + 1) // (i + 2)187 return c188189def trees(leaves, memo={}):190 """Every full binary tree with the given number of leaves: a leaf is 1, an inner node a pair (left, right)."""191 if leaves not in memo:192 memo[leaves] = [1] if leaves == 1 else [(l, r) for k in range(1, leaves) for l in trees(k) for r in trees(leaves - k)]193 return memo[leaves]194195def tree_value(t, p):196 """The value in M_p of the closed term the tree stands for (1 at the leaves, + at the inner nodes)."""197 return 1 % p if t == 1 else (tree_value(t[0], p) + tree_value(t[1], p)) % p198199def tree_text(t):200 """The term written out: 1 at a leaf, (s+t) at an inner node."""201 return "1" if t == 1 else "(" + tree_text(t[0]) + "+" + tree_text(t[1]) + ")"202203def decide(m, pattern, matrix, counter=None):204 """The exhaustive evaluation of the prenex sentence Q1 x1 … Qq xq matrix(x) over a domain of m elements: the whole tree of205 quantifier instantiations is built (no short-circuit), and counter[0] counts the matrix evaluations — m^q of them."""206 def rec(i, vals):207 if i == len(pattern):208 if counter is not None: counter[0] += 1209 return bool(matrix(vals))210 res = [rec(i + 1, vals + (t,)) for t in range(m)]211 return all(res) if pattern[i] == "A" else any(res)212 return rec(0, ())213214def sentences(p):215 """A sample of prenex sentences over M_p, p prime: (text, pattern, matrix, the value number theory gives it). The expected216 values are stated here, not computed: the checks compare the evaluator against them."""217 return [218 ("AxEy x+y=0", "AE", lambda v: (v[0] + v[1]) % p == 0, True),219 ("AxAy x+y=y+x", "AA", lambda v: (v[0] + v[1]) % p == (v[1] + v[0]) % p, True),220 ("AxEy (x=0 or x*y=1)", "AE", lambda v: v[0] == 0 or (v[0] * v[1]) % p == 1, True),221 ("Ex x*x+1=0", "E", lambda v: (v[0] * v[0] + 1) % p == 0, p == 2 or p % 4 == 1), # -1 is a square exactly for p = 2 and p = 1 (mod 4)222 ("ExAy x*y=y", "EA", lambda v: (v[0] * v[1]) % p == v[1], True),223 ("AxEy y*y=x", "AE", lambda v: (v[1] * v[1]) % p == v[0], p == 2), # every element a square only in characteristic 2224 ("ExEyEz (x*x+y*y+z*z=0 and not x=y=z=0)", "EEE", lambda v: (v[0] * v[0] + v[1] * v[1] + v[2] * v[2]) % p == 0 and v != (0, 0, 0), True),225 ("AxAyAz (x+y)+z=x+(y+z)", "AAA", lambda v: ((v[0] + v[1]) + v[2]) % p == (v[0] + (v[1] + v[2])) % p, True),226 ]227228VARS = "abcdef" # the variable names v_0 .. v_5 of the written formulas229230def formulas_M2(V, maxlen):231 """EVERY formula of length <= maxlen over M_2 = ({0, 1}; 0, 1, +, x) in the variables v_0 .. v_{V-1}, written out. Terms: a232 variable, 0, 1 (one symbol), (s+t), (s*t) (three symbols more than their parts); formulas: s=t (one more), ~phi (one more),233 (phi&psi) (three more), Ev phi (two more). Returns ({length: [(truth table, free variables, text)]}, swap): the table is a234 bit mask over the 2^V assignments (bit a: the truth value under the assignment whose coordinate i is bit i of a), the free235 variables a bit mask, the text the formula as a string, and swap(table, i) is the table with coordinate i reassigned (0 <-> 1)."""236 n_as = 1 << V; full = (1 << n_as) - 1237 lo = [sum(1 << a for a in range(n_as) if not (a >> i) & 1) for i in range(V)] # the assignments whose coordinate i is 0238 def swap(tab, i): return ((tab & lo[i]) << (1 << i)) | ((tab >> (1 << i)) & lo[i])239 terms = {1: [(full ^ lo[i], 1 << i, VARS[i]) for i in range(V)] + [(0, 0, "0"), (full, 0, "1")]} # value tables: v_i, the constants240 for L in range(2, maxlen + 1):241 out = []242 for a in range(1, L - 3):243 b = L - 3 - a244 for s_tab, s_fv, s_tx in terms.get(a, []):245 for t_tab, t_fv, t_tx in terms.get(b, []):246 out.append((s_tab ^ t_tab, s_fv | t_fv, "(" + s_tx + "+" + t_tx + ")")) # (s+t) modulo 2247 out.append((s_tab & t_tab, s_fv | t_fv, "(" + s_tx + "*" + t_tx + ")")) # (s*t) modulo 2248 if out: terms[L] = out249 forms = {}250 for L in range(3, maxlen + 1):251 out = []252 for a in range(1, L - 1): # s=t253 for s_tab, s_fv, s_tx in terms.get(a, []):254 for t_tab, t_fv, t_tx in terms.get(L - 1 - a, []): out.append((full ^ s_tab ^ t_tab, s_fv | t_fv, s_tx + "=" + t_tx))255 out += [(full ^ tab, fv, "~" + tx) for tab, fv, tx in forms.get(L - 1, [])] # ~phi256 out += [(tab | swap(tab, i), fv & ~(1 << i), "E" + VARS[i] + tx) for tab, fv, tx in forms.get(L - 2, []) for i in range(V)] # Ev_i phi257 for a in range(3, L - 5): # (phi&psi)258 for t1, f1, x1 in forms.get(a, []):259 for t2, f2, x2 in forms.get(L - 3 - a, []): out.append((t1 & t2, f1 | f2, "(" + x1 + "&" + x2 + ")"))260 if out: forms[L] = out261 return forms, swap262263def read_term(s, i, env):264 """The written term at s[i:], read by recursive descent: (value in M_2 under env, next position, variables occurring), or None."""265 if i >= len(s): return None266 c = s[i]267 if c in "01": return int(c), i + 1, frozenset()268 if c in VARS: return env.get(c, 0), i + 1, frozenset(c)269 if c == "(":270 l = read_term(s, i + 1, env)271 if l is None or l[1] >= len(s) or s[l[1]] not in "+*": return None272 r = read_term(s, l[1] + 1, env)273 if r is None or r[1] >= len(s) or s[r[1]] != ")": return None274 return ((l[0] + r[0]) % 2 if s[l[1]] == "+" else l[0] * r[0]), r[1] + 1, l[2] | r[2]275 return None276277def read_formula(s, i, env):278 """The written formula at s[i:], read by recursive descent and evaluated in M_2 under env (variables absent from env read 0):279 (truth value, next position, free variables), or None if no formula stands there. It shares no code with formulas_M2: the280 truth tables and the free-variable masks of the enumeration are checked against it."""281 if i >= len(s): return None282 c = s[i]283 if c == "~":284 r = read_formula(s, i + 1, env); return None if r is None else (not r[0], r[1], r[2])285 if c == "E" and i + 1 < len(s) and s[i + 1] in VARS:286 x = s[i + 1]; rs = [read_formula(s, i + 2, {**env, x: b}) for b in (0, 1)]287 return None if rs[0] is None else (rs[0][0] or rs[1][0], rs[0][1], rs[0][2] - {x})288 if c == "(": # a conjunction, or an equation whose left term opens a bracket289 l = read_formula(s, i + 1, env)290 if l is not None and l[1] < len(s) and s[l[1]] == "&":291 r = read_formula(s, l[1] + 1, env)292 if r is not None and r[1] < len(s) and s[r[1]] == ")": return l[0] and r[0], r[1] + 1, l[2] | r[2]293 l = read_term(s, i, env)294 if l is None or l[1] >= len(s) or s[l[1]] != "=": return None295 r = read_term(s, l[1] + 1, env)296 return None if r is None else (l[0] == r[0], r[1], l[2] | r[2])297298def name_cost(k, a):299 """The total length of the k shortest distinct names over an alphabet of a letters: a names of one letter, a^2 of two, …"""300 cost, L = 0, 1301 while k > 0:302 take = min(k, a ** L); cost += take * L; k -= take; L += 1303 return cost304305def delta_names(k, k1, a):306 """The least total length of the variable names in the diagonal formula delta(u) = Ev (Diag(u, v) & theta(v)) with k307 coordinates in v and k1 in u: k + k1 distinct variables, each coordinate of v named three times (the block, Diag, theta)308 and each of u once (Diag). Of k + k1 distinct names the k + k1 shortest cost least, and the weight 3 goes to the k309 shortest of them."""310 return 2 * name_cost(k, a) + name_cost(k + k1, a)311312def lambda_names(k, k1, a):313 """The least number of symbols the coordinates cost in lambda = delta(code of delta): each coordinate of v named three314 times, and a closed term of at least one symbol in each of the k1 places of u."""315 return 3 * name_cost(k, a) + k1316317def admits(k, k1, d, a):318 """The name count leaves an instance open, in digit form: lambda's symbols fit a code of k coordinates and delta's a319 code of k1, a code of j coordinates over a structure of d digits holding fewer than d*j letters."""320 return lambda_names(k, k1, a) < d * k and delta_names(k, k1, a) < d * k1321322def fit_table(m, a, d, upto):323 """[n_0, n_1, …, n_upto], n_j the largest n with a^n <= m^j: the longest strings an injective coding by j-tuples can324 reach. For a^(d-1) <= m < a^d each step adds d - 1 or d."""325 out, P, Q, n = [0], 1, 1, 0326 for _ in range(upto):327 P *= m; Q *= a ** (d - 1); n += d - 1328 if Q * a <= P: Q *= a; n += 1329 assert Q <= P < Q * a330 out.append(n)331 return out332333def last_k(w, a, strict=False):334 """The largest k with delta_names(k, k, a) <= w*k (< w*k if strict), 0 if none: the template at one scale.335 delta_names(k, k)/k does not decrease with k (proved in the comment of block D; D5 checks it for a = 2..5, k <= 20000),336 so the k that pass form an initial segment and bisection finds its end. The doubling stops because the quotient is337 unbounded (bound (i) there)."""338 good = (lambda k: delta_names(k, k, a) < w * k) if strict else (lambda k: delta_names(k, k, a) <= w * k)339 if not good(1): return 0340 lo, hi = 1, 2341 while good(hi): hi *= 2342 while lo < hi - 1:343 mid = (lo + hi) // 2344 if good(mid): lo = mid345 else: hi = mid346 return lo347348# ----------------------------------------------------------------------------- the certificate format of the wrap lemma349# A structure is a dict {"U": universe (list), "c": {0: element, 1: element}, "+": table, "*": table}; a table is a function350# (x, y) -> element (M_p: arithmetic on demand) or a dict (a small structure M'). A record is a list of steps:351# ("c", k) the constant k (0 or 1): a term step, checked by reading the constant (one element)352# ("o", op, i, j, v) the term op(step i, step j) has the value v: checked by ONE table lookup, touching at most r+1 = 3 elements353# ("=", i, j) the end sentence: term i = term j, checked by comparing the two recorded values354# ("ax", name) an axiom asserted on syntactic recognition alone: its check consults nothing355def Mp(p, ops="+*"):356 S = {"U": None, "p": p, "c": {0: 0, 1: 1 % p}}357 if "+" in ops: S["+"] = lambda x, y: (x + y) % p358 if "*" in ops: S["*"] = lambda x, y: (x * y) % p359 return S360361def lookup(S, op, x, y):362 t = S[op]363 return t(x, y) if callable(t) else t[(x, y)]364365def verify(record, S, axioms=()):366 """Step-check a record against the tables of S, in the system whose axiom rules assert the sentences listed in `axioms` on367 syntactic recognition. Returns (accepted, values, cited entries {(op, x, y): v}, cited elements, number of lookups). Only the368 entries the steps name are consulted."""369 vals, cited, elems, n_look = [], {}, set(), 0370 for st in record:371 if st[0] == "c":372 v = S["c"][st[1]]; vals.append(v); elems.add(v); n_look += 1373 elif st[0] == "o":374 _, op, i, j, v = st375 if not (i < len(vals) and j < len(vals)) or vals[i] is None or vals[j] is None: return False, vals, cited, elems, n_look376 got = lookup(S, op, vals[i], vals[j]); n_look += 1377 cited[(op, vals[i], vals[j])] = got; elems.update((vals[i], vals[j], got))378 if got != v: return False, vals, cited, elems, n_look379 vals.append(v)380 elif st[0] == "=":381 _, i, j = st382 if vals[i] != vals[j]: return False, vals, cited, elems, n_look383 vals.append(None)384 elif st[0] == "ax":385 if st[1] not in axioms: return False, vals, cited, elems, n_look # not an axiom of the system386 vals.append(None) # recognised by its shape; no table entry is consulted387 else: return False, vals, cited, elems, n_look388 return True, vals, cited, elems, n_look389390def term_of(record, i):391 """The term a term step stands for, as a nested tuple."""392 st = record[i]393 return ("c", st[1]) if st[0] == "c" else (st[1], term_of(record, st[2]), term_of(record, st[3]))394395def eval_term(S, t):396 """The value of a term in S, computed from the tables directly (not from a record)."""397 return S["c"][t[1]] if t[0] == "c" else lookup(S, t[0], eval_term(S, t[1]), eval_term(S, t[2]))398399def eval_step(S, record, i, memo=None):400 """The value in S of the term that step i stands for, computed from the tables of S alone — the values the record states are401 not read; shared subterms are evaluated once (a record is a term graph, not a tree)."""402 memo = {} if memo is None else memo403 if i not in memo:404 st = record[i]405 memo[i] = S["c"][st[1]] if st[0] == "c" else lookup(S, st[1], eval_step(S, record, st[2], memo), eval_step(S, record, st[3], memo))406 return memo[i]407408def small_world(cited, elems, ops, fill):409 """The structure M' of the wrap lemma: universe = the cited elements, the tables agreeing with M on every cited entry and410 completed inside the universe by `fill(op, x, y)` elsewhere."""411 U = sorted(elems) or [0]412 S = {"U": U, "c": {k: (k if k in elems else U[0]) for k in (0, 1)}}413 for op in ops:414 S[op] = {(x, y): cited.get((op, x, y), None) for x in U for y in U}415 for (x, y), v in list(S[op].items()):416 if v is None: S[op][(x, y)] = fill(op, x, y, U)417 return S418419def commutative(S, op="+"):420 return all(lookup(S, op, x, y) == lookup(S, op, y, x) for x in S["U"] for y in S["U"])421422# ------------------------------------------------------------------------------------------------------------423# block A: Gödel's hypotheses over a finite structure (25:C1, C2, C5) — Section 3 of the paper.424# A1: no finite structure carries a successor that is injective and omits an element (exhaustive over all N^N maps,425# N ≤ 7), so no finite structure is a model of Q, and none interprets it. A2: the theory of M_p is decided by exhaustive426# evaluation — every sentence of a sample takes the value number theory gives it, the evaluation object has m^q leaves at427# quantifier depth q, exactly one of a sentence and its negation is true; and the characterising sentence σ_M, evaluated428# as a sentence in every structure on 3 elements, holds exactly in the structures isomorphic to M, and in none of 1 or 2429# elements or among the one-element extensions of M, each clause of σ_M with its control. A3: the sentences outnumber the elements — m+1 sentences of length430# at most m+1 admit no injective numbering into M — while truth is given externally by a finite table.431def block_A():432 """Block A — Gödel's hypotheses over a finite structure (EXACT): A1–A3."""433 # A1 no finite model of Q: injective maps on a finite set are onto; the chain 0, S0, SS0, … repeats434 ok = True; det = []; n_maps = n_chain = 0435 for N in range(1, 8):436 n_inj = n_miss = 0437 for S in itertools.product(range(N), repeat=N):438 n_maps += 1439 if len(set(S)) == N:440 n_inj += 1441 ok &= set(S) == set(range(N)) # injective => surjective442 if 0 not in S: n_miss += 1 # a successor of Q: injective with 0 outside its range443 ok &= n_inj == math.factorial(N) and n_miss == 0444 det.append(f"N={N}: {N**N} maps, {n_inj} injective, all onto")445 for N in range(1, 7): # the numerals 0, S0, …, S^N 0 are not pairwise distinct, whatever S446 for S in itertools.product(range(N), repeat=N):447 n_chain += 1448 x, seen = 0, [0]449 for _ in range(N): x = S[x]; seen.append(x)450 ok &= len(set(seen)) < len(seen)451 ok &= n_maps == 873612 and n_chain == 50069 # 1 + 4 + 27 + … + 7^7 maps; 1 + 4 + … + 6^6 chains452 # 25:C1 (p25010)453 check("A1", "no finite model of Q: on N elements every injective map is onto, so no successor is injective and misses 0 (all 873612 maps, N <= 7); the N+1 numerals 0, S0, ..., S^N 0 repeat under every S (all 50069 maps, N <= 6)", ok,454 "; ".join(det[3:]))455456 # A2 completeness and decidability of Th(M_p); the evaluation object has m^q leaves; sigma_M is categorical457 ok = True; det = []; n_sent = 0458 for p in (5, 7, 13):459 for text, pat, mat, want in sentences(p):460 cnt = [0]; v = decide(p, pat, mat, cnt); n_sent += 1461 ok &= v == want and cnt[0] == p ** len(pat) # decided, with the evaluation object of size m^q462 dual = "".join("E" if c == "A" else "A" for c in pat)463 ok &= decide(p, dual, lambda vals, mat=mat: not mat(vals)) == (not v) # exactly one of the sentence and its negation is true464 det.append(f"p={p}: 8 sentences decided, depth-3 objects of {p**3} leaves")465 ok &= n_sent == 24466 # the characterising sentence sigma_M, evaluated as a sentence in a structure (c0, c1, o) on n elements: there are pairwise distinct467 # x_0, x_1, x_2 with c0 = x_0, c1 = x_1, x_a o x_b = x_{a o b} for every table entry of M, and every element is one of them.468 # `distinct` and `closure` switch its first and last clause off, for the controls.469 def sigma(M_tab, n, c0, c1, tab, distinct=True, closure=True):470 for xs in (itertools.permutations(range(n), 3) if distinct else itertools.product(range(n), repeat=3)):471 if xs[0] == c0 and xs[1] == c1 and all(tab[n * xs[a] + xs[b]] == xs[M_tab[a][b]] for a in range(3) for b in range(3)) \472 and (not closure or all(y in xs for y in range(n))): return True473 return False474 def iso_forced(M_tab, c0, c1, tab):475 """Isomorphism to M tested a second way: M is generated by its constants (2 = 1 o 1), so an isomorphism is forced to be476 0 -> c0, 1 -> c1, 2 -> c1 o c1; it is one iff that map is a bijection carrying every table entry."""477 f = (c0, c1, tab[3 * c1 + c1])478 return len(set(f)) == 3 and all(tab[3 * f[a] + f[b]] == f[M_tab[a][b]] for a in range(3) for b in range(3))479 Z3 = [[(a + b) % 3 for b in range(3)] for a in range(3)]480 NC = [[0, 1, 2], [2, 2, 0], [1, 0, 0]] # a second structure: a non-commutative table with 1 o 1 = 2481 ok &= NC[0][1] != NC[1][0] and all(Z3[a][b] == Z3[b][a] for a in range(3) for b in range(3))482 models = {}483 for name, M_tab in (("Z_3", Z3), ("NC", NC)):484 n_mod = total = 0485 for c0 in range(3):486 for c1 in range(3):487 for tab in itertools.product(range(3), repeat=9): # every structure (c0, c1, o) on 3 elements488 total += 1; sg = sigma(M_tab, 3, c0, c1, tab)489 ok &= sg == iso_forced(M_tab, c0, c1, tab) # the models of sigma_M are exactly the structures isomorphic to M490 n_mod += sg491 ok &= total == 3 * 3 * 3 ** 9 == 177147 and n_mod == math.factorial(3)492 ok &= sigma(M_tab, 3, 0, 1, tuple(M_tab[a][b] for a in range(3) for b in range(3))) # M itself is a model493 # smaller structures: the distinctness clause excludes them. Without it sigma_M holds in the one-element structure494 # (every table equation collapses to the point); with it, in no structure of one or two elements.495 n1 = sigma(M_tab, 1, 0, 0, (0,)); n1_open = sigma(M_tab, 1, 0, 0, (0,), distinct=False)496 n2 = n2_scanned = 0497 for c0 in range(2):498 for c1 in range(2):499 for tab in itertools.product(range(2), repeat=4): n2_scanned += 1; n2 += sigma(M_tab, 2, c0, c1, tab)500 ok &= (n1, n1_open, n2, n2_scanned) == (False, True, 0, 64)501 # larger structures: the closure clause excludes them. Every one-element extension of M (4^7 completions of the new row502 # and column) satisfies sigma_M without its closure clause, and none satisfies sigma_M.503 ext = ext_open = ext_scanned = 0504 for new in itertools.product(range(4), repeat=7):505 tab = [0] * 16506 for a in range(3):507 for b in range(3): tab[4 * a + b] = M_tab[a][b]508 for k, (a, b) in enumerate([(0, 3), (1, 3), (2, 3), (3, 0), (3, 1), (3, 2), (3, 3)]): tab[4 * a + b] = new[k]509 ext_scanned += 1; ext += sigma(M_tab, 4, 0, 1, tab); ext_open += sigma(M_tab, 4, 0, 1, tab, closure=False)510 ok &= (ext, ext_open, ext_scanned) == (0, 16384, 16384)511 models[name] = n_mod512 # 25:C2 (p25011)513 check("A2", "Th(M_p) is decided by exhaustive evaluation: a sample of 8 sentences over p = 5, 7, 13 take the values number theory gives them, the evaluation object has m^q leaves, and exactly one of a sentence and its negation is true; sigma_M, evaluated as a sentence in all 177147 structures (c0, c1, o) on 3 elements, holds exactly in the 3! structures isomorphic to M (for M = (Z_3; 0, 1, +) and for a non-commutative M); its distinctness clause excludes the structures of 1 and 2 elements (without it the one-element structure is a model), its closure clause the 16384 one-element extensions of M (without it all are models)", ok,514 "; ".join(det) + f"; models of sigma among 177147 structures: {models}; 64 structures of 2 elements and 16384 extensions to 4 elements: none")515516 # A3 the sentences outnumber the elements; truth is an external table517 ok = True; n_maps = 0518 def value(sent):519 """The truth value of ~…~F, by recursion on the written sentence (F is the false constant)."""520 return False if sent == "F" else not value(sent[1:])521 for m in range(2, 6):522 sents = ["~" * k + "F" for k in range(m + 1)] # F, ~F, ~~F, …: m+1 sentences of length <= m+1523 ok &= len(set(sents)) == m + 1 and max(map(len, sents)) == m + 1524 for f in itertools.product(range(m), repeat=m + 1): # every numbering of them into M525 n_maps += 1526 ok &= len(set(f)) < m + 1 # is not injective527 table = {sent: value(sent) for sent in sents} # the external truth table: m+1 entries, computed from the sentences528 ok &= len(table) == m + 1 and [table[sent] for sent in sents] == [k % 2 == 1 for k in range(m + 1)] # F false, ~F true, alternating529 ok &= n_maps == 2 ** 3 + 3 ** 4 + 4 ** 5 + 5 ** 6 == 16738530 # 25:C5 (p25014)531 check("A3", "Tarski scoped: the m+1 sentences F, ~F, ..., ~^m F of length at most m+1 admit no injective numbering into a structure of m elements (all 16738 maps, m = 2..5), and their truth is a finite external table, computed from the written sentences", ok,532 f"{n_maps} numberings scanned, none injective")533534# ------------------------------------------------------------------------------------------------------------535# block B: the part and the whole (25:D1, D3, D4; corroborates J2) — Section 4.536# B1: an agent with a^K storage states in a structure of m > a^K elements has no injective encoding (every map on six537# instances; at a^K = m the injective readings are the bijections). B2: every total reading has a fibre of at least538# ⌈m/a^K⌉ ≥ 2 elements, some reading attains the bound, and every element outside a maximal faithfully represented range539# is an alias of one inside it. B3: the wrap — for a certificate checked by table lookups, the540# structure M' on the cited elements (the tables agreeing with M on the cited entries, completed arbitrarily) accepts the541# same record by the same steps and makes its end sentence true: under EVERY completion for a certificate over Z_5, under542# a fixed sample of completions for two larger ones; an axiom asserted on syntactic recognition is accepted there too,543# and its truth does not transport.544def block_B():545 """Block B — the part and the whole: collisions, aliasing, the wrap (EXACT): B1–B3."""546 # B1 the relational diagonal: a^K < m leaves no injective encoding547 ok = True; det = []; n_all = 0548 for a, K, m in ((2, 1, 3), (2, 2, 5), (3, 1, 4), (2, 2, 6), (5, 1, 6), (2, 2, 7)):549 states = a ** K; n = 0550 assert states < m551 for rho in itertools.product(range(states), repeat=m): # every assignment of storage states to the m elements552 n += 1553 ok &= any(rho[x] == rho[y] for x in range(m) for y in range(x)) # identifies two of them554 det.append(f"a^K={states}<m={m}: {n} readings"); n_all += n555 ok &= n_all == 2 ** 3 + 4 ** 5 + 3 ** 4 + 4 ** 6 + 5 ** 6 + 4 ** 7 == 37218556 n_inj = sum(1 for rho in itertools.product(range(4), repeat=4) if len(set(rho)) == 4)557 ok &= n_inj == 24 # the control: with as many states as elements, 4! readings are injective558 # 25:D1 (p25015)559 check("B1", "the part cannot hold the whole: with a^K < m every assignment of storage states to the m elements identifies two of them (all 37218 maps on six instances); with a^K = m = 4 the injective readings are the 24 bijections", ok,560 "; ".join(det[:4]))561562 # B2 aliasing with multiplicity563 ok = True; det = []; n_all = 0564 for m, R in ((4, 2), (5, 2), (5, 3), (6, 3), (7, 2), (7, 3), (6, 4), (5, 4)):565 need = -(-m // R); least = m # ceil(m / R)566 for rho in itertools.product(range(R), repeat=m):567 n_all += 1568 big = max(sum(1 for x in range(m) if rho[x] == y) for y in range(R))569 ok &= big >= need; least = min(least, big) # some reading stands for at least ceil(m/R) elements570 ok &= least == need >= 2 # the bound is attained, and it is at least 2571 det.append(f"m={m}, R={R}: largest fibre >= {need}, attained")572 ok &= n_all == 2 ** 4 + 2 ** 5 + 3 ** 5 + 3 ** 6 + 2 ** 7 + 3 ** 7 + 4 ** 6 + 4 ** 5 == 8455573 # a maximal faithfully represented range: a set S of elements on which the reading is injective and which no larger set with574 # that property contains. Every element outside it is read as an element inside it (an alias).575 n_max = 0576 for m, R in ((4, 2), (5, 2), (5, 3), (6, 3), (5, 4), (6, 4)):577 for rho in itertools.product(range(R), repeat=m):578 faithful = [mask for mask in range(1, 2 ** m) if len({rho[x] for x in range(m) if (mask >> x) & 1}) == bin(mask).count("1")]579 for mask in faithful:580 if any(t != mask and t & mask == mask for t in faithful): continue # a larger faithful set contains S: not maximal581 S = [x for x in range(m) if (mask >> x) & 1]; out = [x for x in range(m) if not (mask >> x) & 1]582 n_max += 1583 ok &= len(out) >= 1 and all(any(rho[s0] == rho[x] for s0 in S) for x in out) # some element lies outside, and each is an alias584 ok &= n_max == 31203585 # 25:D3 (p25017)586 check("B2", "aliasing: every total reading of m elements by R < m storage states has a fibre of at least ceil(m/R) >= 2 elements, and some reading attains the bound (all 8455 maps on eight instances, m = 5, R = 4 among them, where m/R < 2); every element outside a maximal faithfully represented range is read as one inside it (all 31203 maximal ranges of all readings on six instances)", ok,587 "; ".join(det))588589 # B3 the wrap: the same certificate, with its warrant, in a small world590 ok = True; det = []591 r = 2 # the largest operation arity592 # (i) a certificate over M_13: ((1+1)+1)*(1+1) = (1+1)*((1+1)+1)593 rec = [("c", 1), ("o", "+", 0, 0, 2), ("o", "+", 1, 0, 3), ("o", "*", 2, 1, 6), ("o", "*", 1, 2, 6), ("=", 3, 4)]594 M = Mp(13); acc, vals, cited, elems, n_look = verify(rec, M)595 ok &= acc and len(elems) <= n_look <= len(rec) # an operand is an earlier step, so each lookup cites at most one new596 # element: within the lemma's bound of r+1 elements per lookup597 rng = random.Random(25); n_fill = 0598 fills = [lambda op, x, y, U: U[0], lambda op, x, y, U: U[(U.index(x) + 2 * U.index(y) + 1) % len(U)]] + [None] * 40599 for f in fills:600 fill = f or (lambda op, x, y, U: rng.choice(U))601 W = small_world(cited, elems, "+*", fill); n_fill += 1602 acc2, vals2, cited2, elems2, n2 = verify(rec, W)603 ok &= acc2 and vals2 == vals and cited2 == cited # accepted by the same steps, the same lookups, the same results604 ok &= eval_term(W, term_of(rec, 3)) == eval_term(W, term_of(rec, 4)) # the end sentence is true in M'605 ok &= n_fill == 42606 bad_val = rec[:3] + [("o", "*", 2, 1, 7)] # the controls: a record cut at a wrong product, and a false end sentence (3 = 6),607 bad_end = rec[:-1] + [("=", 2, 3)] # are rejected in M and in the last small world608 ok &= not verify(bad_val, M)[0] and not verify(bad_end, M)[0] and not verify(bad_val, W)[0] and not verify(bad_end, W)[0]609 det.append(f"M_13: {len(rec)} steps, {n_look} lookups, |M'| = {len(elems)} <= {n_look} <= {(r + 1) * n_look}, {n_fill} completions (2 fixed, 40 seeded)")610 # (ii) a certificate over the carrier 10^18+9 whose term values are reduced modulo p: t = 2^(2^7), a term of 256 leaves, and t*(t+1) = (t+1)*t611 p = P_BIG; M = Mp(p); rec = [("c", 1), ("o", "+", 0, 0, 2)]; v = 2; size = [1, 5] # size[i]: the written length of the term of step i612 for _ in range(7):613 rec.append(("o", "*", len(rec) - 1, len(rec) - 1, v * v % p)); v = v * v % p; size.append(2 * size[-1] + 3)614 i_t = len(rec) - 1615 rec.append(("o", "+", i_t, 0, (v + 1) % p)); i_s = len(rec) - 1; size.append(size[i_t] + 1 + 3)616 rec.append(("o", "*", i_t, i_s, v * (v + 1) % p)); rec.append(("o", "*", i_s, i_t, v * (v + 1) % p)); rec.append(("=", len(rec) - 2, len(rec) - 1))617 end_len = 2 * (size[i_t] + size[i_s] + 3) + 1 # the end sentence written out: a few thousand symbols618 acc, vals, cited, elems, n_look = verify(rec, M)619 ok &= acc and len(elems) <= n_look and len(elems) < 2 ** 8 < p and end_len == 4099 # M' has fewer than 256 elements, M has p620 ok &= pow(2, 2 ** 7, p) == v != 2 ** (2 ** 7) and 2 ** (2 ** 7) > p # the term's integer value 2^128 exceeds p: its value in M_p is the residue621 n_fill2 = 0622 for f in fills[:12]:623 fill = f or (lambda op, x, y, U: rng.choice(U))624 W = small_world(cited, elems, "+*", fill); n_fill2 += 1625 acc2, vals2, cited2, _, _ = verify(rec, W)626 ok &= acc2 and vals2 == vals and cited2 == cited627 ok &= eval_step(W, rec, len(rec) - 3) == eval_step(W, rec, len(rec) - 2) # the end sentence is true in M', evaluated from its own tables628 ok &= n_fill2 == 12629 det.append(f"M_p, p = 10^18+9: {len(rec)} steps, end sentence of {end_len} symbols, values reduced mod p, |M'| = {len(elems)}, {n_fill2} completions")630 # (iii) every completion, exhaustively: 1+(1+1) = (1+1)+1 over (Z_5; 0, 1, +)631 rec = [("c", 1), ("o", "+", 0, 0, 2), ("o", "+", 0, 1, 3), ("o", "+", 1, 0, 3), ("=", 2, 3)]632 M = Mp(5, "+"); acc, vals, cited, elems, n_look = verify(rec, M); U = sorted(elems)633 free = [(x, y) for x in U for y in U if ("+", x, y) not in cited]634 n_all = n_true = 0635 for choice in itertools.product(U, repeat=len(free)):636 tab = dict(zip(free, choice))637 W = small_world(cited, elems, "+", lambda op, x, y, U: tab[(x, y)])638 acc2, vals2, _, _, _ = verify(rec, W); n_all += 1639 n_true += acc2 and eval_term(W, term_of(rec, 2)) == eval_term(W, term_of(rec, 3))640 ok &= acc and n_all == len(U) ** len(free) == 729 and n_true == n_all # a locally sound certificate keeps its truth under every completion641 # (iv) an axiom asserted on syntactic recognition: the system D with the one axiom rule "AxAy x+y=y+x" (true in M: D is sound)642 COMM = "AxAy x+y=y+x"; D_AX = (COMM,)643 rec_ax = [("c", 1), ("o", "+", 0, 0, 2), ("o", "+", 1, 0, 3), ("ax", COMM)]644 acc, vals, cited, elems, _ = verify(rec_ax, M, D_AX); U = sorted(elems)645 free = [(x, y) for x in U for y in U if ("+", x, y) not in cited]646 n_acc = n_comm = n_w = 0647 for choice in itertools.product(U, repeat=len(free)):648 tab = dict(zip(free, choice))649 W = small_world(cited, elems, "+", lambda op, x, y, U: tab[(x, y)]); n_w += 1650 n_acc += verify(rec_ax, W, D_AX)[0]; n_comm += commutative(W)651 ok &= acc and commutative({"U": list(range(5)), "+": M["+"]}) and n_acc == n_w == 2187 and n_comm == 81 # accepted everywhere; its end sentence true in 81 of the 2187 small worlds652 ok &= not verify([("ax", "0=1")], M, D_AX)[0] and not verify(rec_ax, M)[0] # a sentence the system does not list is not accepted653 # (v) the display case of the neutrality theorem: a description T whose axiom rules assert the successor axioms of Q. Its record is654 # accepted by the same syntactic check over M_13, where the axioms are false (0 = S(12))655 T_Q = ("S injective", "0 not in the range of S")656 succ = lambda x: (x + 1) % 13657 q_inj = len({succ(x) for x in range(13)}) == 13; q_zero = all(succ(x) != 0 for x in range(13))658 ok &= verify([("ax", T_Q[0]), ("ax", T_Q[1])], Mp(13), T_Q)[0] and q_inj and not q_zero659 # 25:D4 (p25018)660 check("B3", "the wrap: a certificate checked by table lookups is accepted, by the same steps and with a true end sentence, in the structure M' on its cited elements (|M'| <= lookups, within the lemma's (r+1) x lookups) — under every completion of the uncited entries for a certificate over Z_5 (729 worlds), under a fixed sample of 42 and of 12 completions for certificates over M_13 and over M_p, p = 10^18+9, whose term values are reduced modulo p; a record with a wrong product or a false end sentence is rejected in both worlds; an axiom asserted on syntactic recognition is accepted in all 2187 small worlds of its record and true in 81 of them", ok,661 "; ".join(det) + f"; Z_5: all {n_all} completions keep the end sentence true; the commutativity axiom accepted in {n_acc} of {n_w} worlds, true in {n_comm}; Q's successor axioms accepted as a record over M_13, where 0 = S(12)")662663# ------------------------------------------------------------------------------------------------------------664# block C: the reach bound and the horizon's counting facts (25:E1, E2, E4, G1, G2, G7) — Sections 5.1, 5.3, 5.4.665# C1: the closed terms over {1, +} with l leaves are the C_{l-1} full binary trees, all of value l mod p, giving666# C(C_{l-1}, 2) >= 2^l true equations of length 8l-5 for l >= 6. C2: the records of length <= B over a letters number667# (a^{B+1}-1)/(a-1) < a^{B+1}, and the certified fraction of the cohort falls below every 1/N. C3: in the bare evaluation668# calculus the universal rule applies to the full set of its m premises alone, so a global clause has a derivation of669# length m+1 > H for every budget H < m. C4: truths longer than a budget B, built and written out — no record of length670# <= B contains one. C5: the one-rule system D_tt accepts exactly the true sentences, each in one line, and step-checks671# by m^q evaluations. C6: the two counting cells of the decomposition table that are not predicates of their own — bounded672# consistency by exhaustive search, with the candidate count of its brute certificate, and reach against the budget.673def block_C():674 """Block C — the reach bound and the horizon's counting facts (EXACT): C1–C6."""675 # C1 abundance of truths676 ok = True; det = []; n_trees = 0677 for l in range(1, 11):678 ts = trees(l); n_trees += len(ts)679 ok &= len(ts) == len(set(ts)) == catalan(l - 1) # the terms with l leaves are the full binary trees: Catalan C_{l-1}680 for p in (2, 3, 5, 13):681 ok &= {tree_value(t, p) for t in ts} == {l % p} # all of one value, l mod p682 ok &= all(len(tree_text(t)) == 4 * l - 3 for t in ts) # written out: 4l-3 symbols, an equation t = t' 8l-5683 ok &= n_trees == 6918684 det.append(f"l <= 10: {n_trees} trees enumerated, each of value l mod p for p = 2, 3, 5, 13")685 ok &= all(catalan(l - 1) >= 2 ** (l - 2) for l in range(2, 501)) # C_{l-1} >= 2^{l-2}686 pair = lambda l: catalan(l - 1) * (catalan(l - 1) - 1) // 2687 ok &= all(pair(l) >= 2 ** l for l in range(6, 501)) and [l for l in range(2, 6) if pair(l) < 2 ** l] == [2, 3, 4] # the cohort C(C_{l-1}, 2) >= 2^l from l = 6 (and at l = 5; it fails at l = 2, 3, 4)688 for L in range(43, 4001): # the truths of length <= L: the cohort at l = floor((L+5)/8) leaves689 l = (L + 5) // 8690 ok &= 6 <= l <= 500 and 8 * l - 5 <= L and 9 * l >= L # its equations fit in L symbols and number at least 2^l >= 2^{L/9}691 # 25:E1 (p25019)692 check("C1", "abundance: the closed terms over {1, +} with l leaves are the Catalan(l-1) full binary trees, all of value l mod p (6918 trees enumerated, l <= 10, p = 2, 3, 5, 13); C_{l-1} >= 2^{l-2} and the cohort of true equations C(C_{l-1}, 2) >= 2^l for 6 <= l <= 500, each of 8l-5 symbols, so the truths of length <= L number at least 2^{L/9} (43 <= L <= 4000)", ok,693 "; ".join(det) + f"; cohort at l = 6: {pair(6)} >= 64, at l = 4: {pair(4)} < 16")694695 # C2 vanishing reach696 ok = True; det = []697 for a, Bmax in ((2, 12), (3, 7), (5, 5)):698 for B in range(Bmax + 1):699 n = sum(1 for k in range(B + 1) for _ in itertools.product(range(a), repeat=k)) # the strings of length <= B, enumerated700 ok &= n == (a ** (B + 1) - 1) // (a - 1) < a ** (B + 1)701 a, B = 2, 20; certs = a ** (B + 1)702 f12, f24, f48 = (Fraction(certs, pair(l)) for l in (12, 24, 48))703 ok &= f12 < 1 and f24 < Fraction(1, 10 ** 6) and f48 < f24 < f12704 for N in (10 ** 3, 10 ** 6, 10 ** 12, 10 ** 100):705 l0 = next(l for l in range(6, 2000) if certs * N < pair(l))706 ok &= all(certs * N < pair(l) for l in range(l0, l0 + 60)) # below 1/N from l0 on707 det.append(f"< 1/{'10^' + str(len(str(N)) - 1)} from l = {l0}")708 # 25:E2 (p25020)709 check("C2", "vanishing reach: the records of length <= B over a letters number (a^{B+1}-1)/(a-1) < a^{B+1} (enumerated for a = 2, 3, 5), and at a = 2, B = 20 the certified fraction a^{B+1}/C(C_{l-1}, 2) of the equation cohort is below 1 at l = 12, below 10^-6 at l = 24, and below each tested 1/N (N = 10^3, 10^6, 10^12, 10^100) at the 60 values of l from a first one on", ok,710 f"fraction at l = 12: {f12.numerator}/{f12.denominator}; " + "; ".join(det))711712 # C3 a global clause in the bare evaluation calculus713 ok = True; det = []714 def bare_accepts(deriv, p, phi=lambda x, p: (x + 0) % p == x):715 """The bare evaluation calculus on the clause Ax x+0=x: a premise ("inst", c) is checked by one lookup; the universal rule716 ("all",) is accepted only when a premise for every element of the structure stands before it."""717 have = set()718 for st in deriv:719 if st[0] == "inst":720 if not phi(st[1], p): return False721 have.add(st[1])722 elif st[0] == "all":723 if have != set(range(p)): return False724 else: return False725 return bool(deriv) and deriv[-1] == ("all",)726 for p in (5, 13, 101, 1009):727 deriv = [("inst", c) for c in range(p)] + [("all",)] # the m premises phi(c), one per element, then the universal rule728 ok &= bare_accepts(deriv, p) and len(deriv) == p + 1 and all(len(deriv) > H for H in range(p))729 ok &= not any(bare_accepts(deriv[:c] + deriv[c + 1:], p) for c in range(p)) # with any one premise missing the rule does not apply730 det.append(f"m={p}: length {len(deriv)}")731 n_sub = 0732 for p in (5, 13): # every subset of the premises: the rule applies to the full set alone733 for mask in range(2 ** p):734 n_sub += 1735 ok &= bare_accepts([("inst", c) for c in range(p) if (mask >> c) & 1] + [("all",)], p) == (mask == 2 ** p - 1)736 ok &= n_sub == 2 ** 5 + 2 ** 13 == 8224737 ok &= not bare_accepts([("inst", c) for c in range(5)] + [("all",)], 5, lambda x, p: (x * x) % p == x) # the controls: a false premise (2*2 = 2) is rejected,738 ok &= not bare_accepts([("inst", c) for c in range(5)], 5) # and premises without the universal step derive no global clause739 def rich_accepts(deriv, p):740 """A richer system: the bare calculus with one more rule, which asserts the clause as an axiom on syntactic recognition."""741 return deriv == [("ax", "Ax x+0=x")] or bare_accepts(deriv, p)742 ok &= all(rich_accepts([("ax", "Ax x+0=x")], p) and not bare_accepts([("ax", "Ax x+0=x")], p) for p in (5, 13, 101, 1009)) # there the clause has a one-line derivation743 # 25:E4 (p25022)744 check("C3", "a global clause in the bare evaluation calculus: the universal rule for Ax x+0=x applies to the full set of its m premises alone (all 8224 premise sets for m = 5, 13; every single omission for m = 101, 1009), so the derivation has length m+1, beyond every budget H < m; a false premise is rejected, premises without the universal step derive nothing, and a richer system with an axiom rule for the clause derives it in one line", ok,745 "; ".join(det) + f"; {n_sub} premise sets")746747 # C4 the length horizon: truths longer than the budget, built and measured748 ok = True; det = []749 def comb(l, left):750 """The left comb ((1+1)+1)+… or the right comb 1+(1+(…)) with l leaves, as a tree."""751 t = 1752 for _ in range(l - 1): t = (t, 1) if left else (1, t)753 return t754 for B in (20, 100, 1000):755 l = (B + 5) // 8 + 1756 L, R = comb(l, True), comb(l, False)757 eq = tree_text(L) + "=" + tree_text(R) # the equation, written out758 ok &= L != R and len(eq) > B # longer than every record of length <= B, which would have to contain it759 ok &= all(tree_value(L, p) == tree_value(R, p) for p in (P_SMALL, P_MID)) # and true in M_p760 ok &= len(eq) - 8 <= B # the comb pair one leaf shorter fits: the horizon sits at this length761 det.append(f"B={B}: a true equation of {len(eq)} symbols")762 # 25:G1 (p25028)763 check("C4", "the length horizon on instances: for B = 20, 100, 1000 the equation between the left comb and the right comb of floor((B+5)/8)+1 leaves, built and written out, is true in M_13 and M_1000033 and longer than B, so no record of length <= B contains it", ok,764 "; ".join(det))765766 # C5 the evaluation ceiling: the one-rule system D_tt767 ok = True; det = []768 for p in (5, 7):769 pool = {}; expect = {} # the sample and its negations: text -> (pattern, matrix); the value number theory gives each770 for text, pat, mat, want in sentences(p):771 pool[text] = (pat, mat); expect[text] = want772 pool["not " + text] = ("".join("E" if c == "A" else "A" for c in pat), lambda v, mat=mat: not mat(v)); expect["not " + text] = not want773 cost = [0]774 def dtt_accepts(deriv):775 """D_tt: every line is a sentence asserted outright, its side condition truth under exhaustive evaluation."""776 return all(decide(p, *pool[line], cost) for line in deriv)777 ok &= all(dtt_accepts([t]) == expect[t] for t in pool) # D_tt derives exactly the true sentences: sound, and complete on the sample778 truths = [t for t in pool if expect[t]]779 ok &= len(pool) == 16 and len(truths) == 8780 for t in truths:781 cost[0] = 0; ok &= dtt_accepts([t]) and cost[0] == p ** len(pool[t][0]) # the one-line derivation [t]; its step-check: m^q evaluations at depth q782 ok &= not any(dtt_accepts([t, f]) or dtt_accepts([f, t]) for t in truths[:2] for f in pool if not expect[f]) # a false line anywhere spoils a derivation783 det.append(f"p={p}: 8 truths each derived in one line, 8 falsehoods rejected, step-check {p}^q evaluations (q = 3: {p**3})")784 # 25:G2 (p25029)785 check("C5", "the evaluation ceiling: the one-rule system D_tt accepts exactly the sentences number theory makes true (a sample of 8 sentences and their negations over M_5, M_7), each true one derived in one line, the line being the sentence itself, while the step-check of the one rule performs m^q evaluations at depth q", ok, "; ".join(det))786787 # C6 the decomposition's counting cells: bounded consistency by exhaustive search; its brute certificate; reach against the budget788 ok = True789 M = Mp(5); n_rec = n_acc = n_false = n_absurd = n_absurd_acc = n_cut = 0790 def ext(rec, depth):791 """Every record of at most `depth` further term steps followed by an end step."""792 nonlocal n_rec, n_acc, n_false, n_absurd, n_absurd_acc, n_cut, ok793 k = len(rec)794 for i in range(k):795 for j in range(k):796 full = rec + [("=", i, j)]; n_rec += 1797 acc, vals, _, _, _ = verify(full, M)798 absurd = term_of(full, i) == ("c", 0) and term_of(full, j) == ("c", 1) # the record ends in the absurdity 0 = 1799 n_absurd += absurd800 if acc:801 n_acc += 1; n_absurd_acc += absurd802 n_false += eval_term(M, term_of(full, i)) != eval_term(M, term_of(full, j)) # the end sentence, evaluated from the tables803 if depth == 0: return804 for st in [("c", 0), ("c", 1)] + [("o", op, i, j, v) for op in "+*" for i in range(k) for j in range(k) for v in range(5)]:805 if st[0] == "o" and lookup(M, st[1], verify(rec, M)[1][st[2]], verify(rec, M)[1][st[3]]) != st[4]:806 n_rec += 1; n_cut += 1; ok &= not verify(rec + [st], M)[0] # a step with a wrong value is rejected807 continue808 ext(rec + [st], depth - 1)809 ext([], 3)810 ok &= (n_rec, n_cut, n_acc) == (1026, 272, 562) and n_false == 0 # 754 records with an end step, 272 cut at a wrong value; soundness on every accepted record811 ok &= n_absurd == 34 and n_absurd_acc == 0 # Con: 34 candidates end in 0 = 1, and none is accepted812 n_strings = 0813 for a in (2, 3): # the brute certificate of Con_H lists every candidate record of length <= H:814 for H in range(1, 11): # their number, counted by enumeration, exceeds the budget H815 n = sum(1 for k in range(H + 1) for _ in itertools.product(range(a), repeat=k)); n_strings += n816 ok &= n == (a ** (H + 1) - 1) // (a - 1) > H817 ok &= n_strings == 136935818 eqs = sorted(len(tree_text(t)) * 2 + 1 for l in range(1, 11) for t in trees(l)) # the reflexivity instances t = t, written out: their lengths819 reach = lambda B: sum(1 for L in eqs if L <= B) # those that fit in a budget of B symbols820 ok &= eqs[0] == 3 and all(reach(B) < reach(B + 8) for B in range(3, 68)) # the reach grows over every 8 symbols of budget …821 ok &= all(reach(B) == reach(B + 1) for B in range(3, 10)) # … and not with every symbol: 3 <= B <= 10 holds the one instance 1 = 1822 # 25:G7 (p25034)823 check("C6", "the decomposition's counting cells: bounded consistency decided by exhaustive search — of the 1026 candidate records of at most three term steps over M_5 (754 with an end step, 272 cut at a step with a wrong value), every accepted one has a true end sentence, and the 34 ending in 0 = 1 are all rejected; the brute certificate of Con_H lists (a^(H+1)-1)/(a-1) > H candidate records (enumerated, a = 2, 3, H <= 10); the reflexivity instances t = t that fit a budget B grow in number over every 8 symbols (enumerated, 3 <= B < 68), not with every symbol", ok,824 f"{n_rec} records scanned, {n_acc} accepted, {n_false} with a false end sentence, {n_absurd} ending in 0 = 1 ({n_absurd_acc} accepted); {n_strings} candidate strings enumerated; reach at B = 3, 11, 19, 27: {reach(3)}, {reach(11)}, {reach(19)}, {reach(27)}")825826# ------------------------------------------------------------------------------------------------------------827# block D: the diagonal under finitude (25:F1, F2, F3, F4, F6) — Section 5.2.828# D1: mention cost — a coordinate on which the truth of a formula depends is a variable that occurs free in it: on a family of829# formulas over M_3 and on EVERY formula of length <= 9 over M_2 in four variables, each written out and read back by the830# independent reader. D2: the no-compression theorem on built instances — the graph of every injective map on M_2^N depends831# on all 2N coordinates; every formula that defines such a graph mentions all 2N variables; the diagonal formula written out832# from each of them computes theta at the diagonal image, names each coordinate of v at least three times and each of u at833# least once, and is longer than N, so its code is no N-tuple; with the scales split it is longer than the scale of v.834# D3: density — an injective coding of the a^n strings into k-tuples needs m^k >= a^n (below it every coding collides), so835# n < dk, d the digit count of m in base a; the diagonal formula with k coordinates in v and k1 in u costs at least836# 2c(k) + c(k+k1) symbols, and its instance lambda at least 3c(k) + k1. D4: quotation exceeds mention — over EVERY formula837# of length <= 9 in six variables, the truth depends on fewer coordinates than the formula has symbols. D5: the threshold838# lies inside the count — the two costs fit their codes for no k beyond k*(M), no instance codes lambda at a length839# n >= t(M) = d k*(M), and t(M) < m in every structure.840#841# The statements of D3 and D5 hold for every alphabet a >= 2 and every structure; the checks decide ranges and the base842# cases. Notation: d is the digit count of m, a^(d-1) <= m < a^d; c(j) is the total length of the j shortest names; k >= 1843# and k1 >= 1 are the coordinates of v and of u in delta(u) = Ev (Diag(u, v) & theta(v)), and lambda = delta(code of delta).844# The codes. The code of delta is the k1-tuple that fills u; it codes a string of some length n1 >= |delta|. The code of845# lambda is a k-tuple, the argument of theta; it codes a string of length n >= |lambda|. An injective coding of the strings846# of length n by k-tuples has a^n <= m^k < a^(dk), so n < dk; likewise n1 < d k1. At one scale k1 = k and n1 = n.847# The count. In delta the block binds the k coordinates of v, Diag has k1 + k argument places and theta has k: each848# coordinate of v is named three times and each of u once, by k + k1 distinct names. Of k + k1 distinct names the k + k1849# shortest cost least, and the weight 3 goes to the k shortest: |delta| >= 2c(k) + c(k+k1). In lambda the places of u hold850# k1 closed terms of at least one symbol: |lambda| >= 3c(k) + k1. So an instance needs851# 2c(k) + c(k+k1) < d k1 and 3c(k) + k1 < dk,852# and k*(M) is the largest k for which some k1 satisfies both (0 if none). At one scale the first reads N(k) < dk,853# N(k) = 2c(k) + c(2k), and implies the second.854# (i) Bounds. c(k) is the sum over j >= 0 of the number of the k shortest names longer than j. The names of at most j855# letters number A_j <= 2a^j - 2, so c(k) > kJ - 2a^J for every J >= 1. With J = floor(d/3) + 1, 3J >= d + 1, and856# 3c(k) < dk gives k <= k(3J - d) < 6a^J: k*(M) < 6a^(floor(d/3)+1). At one scale the same sum with the weights gives857# N(k) > 4kJ - 6a^J; with J = floor(d/4) + 1, 4J >= d + 1, and N(k) < dk gives k < 6a^(floor(d/4)+1). N(k)/k =858# 2 c(k)/k + 2 c(2k)/(2k), and each term is twice the mean length of an initial run of the names in order of length, so859# N(k)/k does not decrease: at one scale the k that pass form an initial segment.860# (ii) No instance at n >= t(M) = d k*(M). An instance has k <= k*(M) by definition and n < dk, whatever the two861# injective codings.862# (iii) t(M) < m. For d <= 4 there is no instance: c(j) >= j, so the second inequality gives 3k + k1 < 4k, k1 < k, and863# the first gives 3k + k1 < 4 k1, k1 > k. For d >= 5, d k*(M) < 6d a^J, J = floor(d/3) + 1. For d >= 13,864# 6d a^J <= a^(d-1): it holds at d = 13, 14, 15 for a = 2 (2496 <= 4096, 2688 <= 8192, 5760 <= 16384), hence for every a865# (J < d - 1), and the step d -> d+3 multiplies the left side by a(d+3)/d < a^3. For d = 5, …, 12 it fails at fifteen866# pairs (a, d), all with a <= 5, which D5 decides directly, and holds at every larger a (J < d - 1 again). So867# t(M) < a^(d-1) <= m.868# Below, at one scale. For k <= floor(a^floor((d-1)/4) / 2) the 2k names have at most floor((d-1)/4) letters, so869# N(k) <= (d-1)k, which is at most the largest n with a^n <= m^k: the count leaves these k open.870# The cut 2^400 of the ranges is a test parameter.871def block_D():872 """Block D — the diagonal under finitude: mention cost, the template, density (EXACT): D1–D5."""873 # D1 mention cost: a family over M_3, then every short formula over M_2874 m, V = 3, 3875 assigns = list(itertools.product(range(m), repeat=V)); idx = {a: i for i, a in enumerate(assigns)}876 leaf = [(("v", i), tuple(a[i] for a in assigns), 1, frozenset([i])) for i in range(V)] + [(("k", c), tuple(c for _ in assigns), 1, frozenset()) for c in (0, 1)]877 terms = list(leaf)878 for op, f in (("+", lambda x, y: (x + y) % m), ("*", lambda x, y: (x * y) % m)):879 for s in leaf:880 for t in leaf:881 terms.append(((op, s[0], t[0]), tuple(f(x, y) for x, y in zip(s[1], t[1])), s[2] + t[2] + 3, s[3] | t[3]))882 # a formula is (truth table over the 27 assignments, length in symbols, free variables)883 atoms = [(tuple(x == y for x, y in zip(s[1], t[1])), s[2] + t[2] + 1, s[3] | t[3]) for s in terms for t in terms]884 def neg(f): return (tuple(not b for b in f[0]), f[1] + 1, f[2])885 def ex(i, f): # Ev_i phi: 2 more symbols; v_i is bound886 tab = tuple(any(f[0][idx[a[:i] + (c,) + a[i + 1:]]] for c in range(m)) for a in assigns)887 return (tab, f[1] + 2, f[2] - {i})888 def conj(f, g): return (tuple(x and y for x, y in zip(f[0], g[0])), f[1] + g[1] + 3, f[2] | g[2])889 leaf_atoms = [(tuple(x == y for x, y in zip(s[1], t[1])), s[2] + t[2] + 1, s[3] | t[3]) for s in leaf for t in leaf]890 family = list(atoms) + [neg(f) for f in atoms] + [ex(i, f) for i in range(V) for f in atoms]891 family += [ex(i, ex(j, f)) for i in range(V) for j in range(V) for f in atoms] + [neg(ex(i, f)) for i in range(V) for f in atoms]892 family += [conj(f, g) for f in leaf_atoms for g in leaf_atoms] + [ex(i, conj(f, g)) for i in range(V) for f in leaf_atoms for g in leaf_atoms]893 def depends(tab, i):894 return any(tab[idx[a]] != tab[idx[a[:i] + (c,) + a[i + 1:]]] for a in assigns for c in range(m))895 ok = True; n_dep = [0] * (V + 1); n_idle = 0896 for tab, length, free in family:897 dep = {i for i in range(V) if depends(tab, i)}898 ok &= dep <= free # truth depends on coordinate i => v_i occurs (free)899 n_dep[len(dep)] += 1; n_idle += dep != free # the converse fails: a variable can occur idly (v0 = v0)900 ok &= len(family) == 53925 and n_dep == [31839, 13872, 7566, 648] and n_idle == 21903901 # every formula of length <= 9 over M_2 in four variables, written out. The enumeration's truth table and free variables are902 # first checked against the independent reader of the written formula, under every assignment; then the lemma.903 forms, swap = formulas_M2(4, 9); n2 = n2_dep = 0; by_free = [0] * 5904 for L, fs in forms.items():905 for tab, fv, tx in fs:906 n2 += 1907 reads = [read_formula(tx, 0, {VARS[i]: (a >> i) & 1 for i in range(4)}) for a in range(16)]908 ok &= len(tx) == L and all(r is not None and r[1] == L and r[0] == bool((tab >> a) & 1) for a, r in enumerate(reads))909 free = reads[0][2]910 ok &= free == frozenset(VARS[i] for i in range(4) if (fv >> i) & 1) # the free variables, read off the written formula911 dep = [i for i in range(4) if swap(tab, i) != tab]912 ok &= all(VARS[i] in free for i in dep) # a coordinate read is a variable occurring free913 n2_dep += bool(dep); by_free[len(free)] += 1914 ok &= n2 == 17820 and n2_dep == 8820 and by_free == [4604, 8344, 4128, 720, 24]915 # 25:F1 (p25023)916 check("D1", "mention cost: a coordinate on which the truth of a formula depends is a variable occurring free in it — on a family of 53925 formulas over M_3 (equations between terms with at most one operation, negations, conjunctions, one or two quantifiers) and on all 17820 formulas of length <= 9 over M_2 in four variables, each written out and read back by an independent reader; the converse fails (a variable can occur idly)", ok,917 f"{len(family)} formulas over M_3, depending on 0/1/2/3 coordinates: {n_dep[0]}/{n_dep[1]}/{n_dep[2]}/{n_dep[3]}, {n_idle} with an idle variable; {n2} formulas over M_2, {n2_dep} with a dependence, by number of free variables 0..4: {by_free}")918919 # D2 the no-compression theorem on built instances920 ok = True; n_maps = 0921 def graph_depends(d, N):922 """The coordinates (of u, then of v) on which the relation v = d(u) on M_2^N x M_2^N depends, by reassigning each one."""923 rel = lambda u, v: v == d[u]924 dep_u = [any(rel(u, v) != rel(u ^ (1 << i), v) for u in range(1 << N) for v in range(1 << N)) for i in range(N)]925 dep_v = [any(rel(u, v) != rel(u, v ^ (1 << i)) for u in range(1 << N) for v in range(1 << N)) for i in range(N)]926 return dep_u + dep_v927 for N in (1, 2, 3):928 for k, d in enumerate(itertools.permutations(range(1 << N))): # the injective maps on M_2^N (N = 3: every 37th of the 40320)929 if N == 3 and k % 37: continue930 n_maps += 1; ok &= all(graph_depends(d, N)) # the diagonal relation depends on every one of its 2N coordinates931 ok &= graph_depends((0,) * (1 << N), N) == [False] * N + [True] * N # the control: the graph of a constant map reads no coordinate of u932 ok &= n_maps == 2 + 24 + 1090933 # the template itself, on written formulas. u = v_0..v_{N-1} carries a code of scale N, v = v_N..v_{N+N2-1} a code of scale N2934 # (N2 = N: the theorem's template; N2 > N: the scales split). Diag ranges over EVERY formula of length <= 9 whose relation is the935 # graph of an injective map u -> v, theta over EVERY formula of length <= 5 in v alone that reads each coordinate of v.936 built = []; n_delta = 0; census = {}; least_occ = (99, 99)937 for N, N2 in ((1, 1), (2, 2), (1, 2)):938 V = N + N2; forms, swap = formulas_M2(V, 9); u_side, v_side = 1 << N, 1 << N2939 u_names, v_names = VARS[:N], VARS[N:V]940 def as_map(tab):941 """The injective map d: M_2^N -> M_2^N2 whose graph the table is, or None."""942 d = []943 for u in range(u_side):944 vs = [v for v in range(v_side) if (tab >> (u + u_side * v)) & 1]945 if len(vs) != 1: return None946 d.append(vs[0])947 return tuple(d) if len(set(d)) == u_side else None948 diags = [(L, tx, as_map(tab)) for L, fs in forms.items() for tab, fv, tx in fs if as_map(tab) is not None]949 thetas = [(L, tx) for L, fs in forms.items() if L <= 5 for tab, fv, tx in fs950 if fv >> N << N == fv and all(swap(tab, i) != tab for i in range(N, V))] # theta(v): reads every coordinate of v, no other variable951 ok &= len(diags) > 0 and len(thetas) > 0952 for Ld, dtx, d in diags:953 ok &= {c for c in dtx if c in VARS} == set(VARS[:V]) and Ld >= V # the written Diag mentions every one of its N + N2 variables954 for Lt, ttx in thetas:955 ok &= set(v_names) <= {c for c in ttx if c in VARS} and Lt >= N2 # the written theta mentions every coordinate of v956 for Ld, dtx, d in diags:957 for Lt, ttx in thetas:958 delta = "".join("E" + x for x in v_names) + "(" + dtx + "&" + ttx + ")" # delta(u) = Ev (Diag(u, v) & theta(v)), written out959 n_delta += 1960 for u in range(u_side):961 got = read_formula(delta, 0, {u_names[i]: (u >> i) & 1 for i in range(N)})962 want = read_formula(ttx, 0, {v_names[i]: (d[u] >> i) & 1 for i in range(N2)})963 ok &= got is not None and got[1] == len(delta) and got[2] <= set(u_names) and got[0] == want[0] # delta(u) is theta at the diagonal image of u964 occ_v = min(delta.count(x) for x in v_names); occ_u = min(delta.count(x) for x in u_names)965 ok &= occ_v >= 3 and occ_u >= 1 # each coordinate of v is named three times (block, Diag, theta), each of u once966 least_occ = (min(least_occ[0], occ_v), min(least_occ[1], occ_u))967 ok &= len(delta) == 2 * N2 + 3 + Ld + Lt # the written length: the block, the conjunction, Diag, theta968 ok &= len(delta) >= 3 * N + Lt > N and len(delta) > Lt >= N2 # longer than N and than N2: its code is no N-tuple, and no N2-tuple969 census[(N, N2)] = (len(diags), min(L for L, _, _ in diags), len(thetas))970 built.append(f"(N, N2) = ({N}, {N2}): {len(diags)} formulas define a diagonal relation (shortest {census[(N, N2)][1]} symbols), {len(thetas)} formulas theta")971 ok &= census == {(1, 1): (142, 3, 16), (2, 2): (16, 9, 10), (1, 2): (56, 9, 8)} and n_delta == 142 * 16 + 16 * 10 + 56 * 8 == 2880972 ok &= least_occ == (3, 1) # the counts 3 and 1 are attained973 # 25:F2 (p25024)974 check("D2", "no compression on built instances: the graph of every injective map on M_2^N depends on all 2N coordinates (N = 1, 2; a fixed sample of 1090 maps at N = 3; a constant map as control); every formula of length <= 9 that defines such a graph (N = 1, 2) mentions all 2N variables; each of the 2432 diagonal formulas Ev (Diag & theta), written out from them with each non-degenerate theta of length <= 5 and read back by the independent reader, computes theta at the diagonal image, names each coordinate of v at least three times and each of u at least once (both counts attained), and has at least 3N + |theta| > N symbols, so its code is no N-tuple; with the scales split (u of scale 1, v of scale 2; 448 formulas) it is longer than theta, which is at least as long as the scale of v", ok,975 f"{n_maps} injective maps; " + "; ".join(built) + f"; {n_delta} diagonal formulas written out")976977 # D3 density and the name count of the template978 ok = True979 n_cases = n_codings = 0980 for a, m, n, k in ((2, 3, 2, 1), (3, 2, 1, 1), (2, 2, 3, 2), (3, 4, 2, 1), (2, 5, 3, 1)): # below m^k >= a^n every coding collides: every map, five cases981 src = list(itertools.product(range(a), repeat=n)); n_states = m ** k982 assert n_states < len(src) and n_states ** len(src) <= 400000983 n_cases += 1984 for f in itertools.product(range(n_states), repeat=len(src)):985 n_codings += 1; ok &= len(set(f)) < len(src)986 ok &= n_cases == 5 and n_codings == 3 ** 4 + 2 ** 3 + 4 ** 8 + 4 ** 9 + 5 ** 8 == 718394987 n_inj = sum(1 for f in itertools.product(range(4), repeat=4) if len(set(f)) == 4)988 ok &= n_inj == 24 # the control: at m^k = a^n = 4 injective codings exist989 # the digit bound. d is the digit count of m in base a: a^(d-1) <= m < a^d. The longest strings an injective coding990 # by k-tuples reaches have the largest n with a^n <= m^k letters, and (d-1)k <= n < dk.991 T_EXACT.clear(); n_pairs = 0992 for a, top in ((2, 500), (3, 400), (4, 400), (5, 700)): # every structure in a range, in exact integers993 for m in range(a, top + 1):994 d = 1995 while a ** d <= m: d += 1996 upto = 2 * 6 * a ** (d // 3 + 1) # every k up to twice the bound (i) of D5997 fit = fit_table(m, a, d, upto)998 for k in range(1, upto + 1):999 n_pairs += 1; n = fit[k]1000 ok &= a ** n <= m ** k < a ** (n + 1) and (d - 1) * k <= n < d * k1001 T_EXACT[(a, m)] = (d, fit)1002 ok &= len(T_EXACT) == 499 + 398 + 397 + 696 == 1990 and n_pairs == 4251121003 # the name count of the template, in integers. With k coordinates in v and k1 in u the diagonal formula names k + k11004 # distinct variables, each coordinate of v three times and each of u once (D2). Every ordering of k + k1 names chosen1005 # among the k + k1 + 2 shortest, the first k of an ordering given to v: the least cost in delta is delta_names, the1006 # least in lambda (a one-symbol term in each place of u) is lambda_names, and one ordering attains both.1007 n_ord = 0; least = []; pairs = ((1, 1), (2, 2), (3, 3), (1, 2), (2, 1), (1, 3), (3, 1), (2, 3), (3, 2))1008 for a in (2, 3):1009 for k, k1 in pairs:1010 pool = [L for L in range(1, 6) for _ in range(a ** L)][:k + k1 + 2]1011 costs = set()1012 for c in itertools.combinations(range(len(pool)), k + k1):1013 for p in itertools.permutations([pool[x] for x in c]):1014 n_ord += 1; costs.add((3 * sum(p[:k]) + sum(p[k:]), 3 * sum(p[:k]) + k1))1015 ok &= min(x for x, y in costs) == delta_names(k, k1, a) and min(y for x, y in costs) == lambda_names(k, k1, a)1016 ok &= (delta_names(k, k1, a), lambda_names(k, k1, a)) in costs1017 least.append((min(x for x, y in costs), min(y for x, y in costs)))1018 ok &= n_ord == 528241019 ok &= least == [(4, 4), (10, 8), (18, 15), (6, 5), (8, 7), (8, 6), (14, 13), (12, 9), (16, 14), (4, 4), (9, 8), (15, 12), (5, 5), (7, 7), (7, 6), (11, 10), (11, 9), (13, 11)]1020 # 25:F4 (p25048)1021 check("D3", "density: an injective coding of the a^n strings into k-tuples needs m^k >= a^n — below it every coding collides (all 718394 maps, five cases), at equality injective codings exist — so n < dk, d the digit count of m in base a: the largest n with a^n <= m^k lies between (d-1)k and dk - 1 (425112 pairs (m, k): every k up to 12a^(floor(d/3)+1) in the 1990 structures a <= m <= 500 (a = 2), 400 (a = 3, 4), 700 (a = 5)); the diagonal formula with k coordinates in v and k1 in u names each coordinate of v three times and each of u once: over all 52824 orderings of k + k1 names chosen among the k + k1 + 2 shortest, the first k of an ordering given to v (a = 2, 3; nine pairs (k, k1) with k, k1 <= 3), the least cost in delta is 2c(k) + c(k+k1), the least in lambda, with a one-symbol term in each place of u, is 3c(k) + k1, and one ordering attains both, c the cost of the shortest names", ok,1022 f"{n_codings} codings below the bound, all colliding; {n_pairs} pairs (m, k); (delta, lambda) costs at a = 2, (k, k1) = (1, 1), (2, 2), (3, 3), (2, 3): " + ", ".join(str((delta_names(k, k1, 2), lambda_names(k, k1, 2))) for k, k1 in ((1, 1), (2, 2), (3, 3), (2, 3))))10231024 # D4 quotation exceeds mention: every formula of length <= 9 in six variables1025 ok = True1026 forms, swap = formulas_M2(6, 9); n6 = 0; least = {}; most = {}; hist = [0] * 71027 for L, fs in forms.items():1028 for tab, fv, tx in fs:1029 n6 += 11030 r = read_formula(tx, 0, {})1031 ok &= len(tx) == L and r is not None and r[1] == L and r[2] == frozenset(VARS[i] for i in range(6) if (fv >> i) & 1) and r[0] == bool(tab & 1)1032 fl = [i for i in range(6) if (fv >> i) & 1]1033 for bits in range(1, 1 << len(fl)): # every assignment to the free variables (the others 0)1034 a = sum(1 << i for j, i in enumerate(fl) if (bits >> j) & 1)1035 ok &= read_formula(tx, 0, {VARS[i]: 1 for i in fl if (a >> i) & 1})[0] == bool((tab >> a) & 1)1036 ok &= all(swap(tab, i) == tab for i in range(6) if i not in fl) # and the table does not move along a variable that is not free1037 k = sum(1 for i in range(6) if swap(tab, i) != tab) # the number of coordinates the truth depends on1038 hist[k] += 11039 ok &= k < L # fewer than the formula has symbols1040 least[k] = min(least.get(k, L), L); most[L] = max(most.get(L, 0), k)1041 ok &= n6 == 65600 and least == {0: 3, 1: 3, 2: 3, 3: 7, 4: 9} # the shortest formula reading k coordinates1042 ok &= hist == [28430, 16320, 16170, 4320, 360, 0, 0] # the formulas by the number of coordinates read1043 ok &= most == {3: 2, 4: 2, 5: 2, 6: 2, 7: 3, 8: 3, 9: 4} # six variables are on offer; no formula of 9 symbols reads more than four1044 # 25:F3 (p25025)1045 check("D4", "quotation exceeds mention: over all 65600 formulas of length <= 9 over M_2 in six variables, written out, the truth depends on fewer coordinates than the formula has symbols — the shortest formula reading 2, 3, 4 coordinates has 3, 7, 9 symbols, and none of at most 9 symbols reads five of the six", ok,1046 f"{n6} formulas; least length by coordinates read: {least}; most coordinates read by length: {most}")10471048 # D5 the threshold lies inside the count. An instance with k coordinates in v and k1 in u needs lambda_names < dk and1049 # delta_names < d k1 (admits). k*(M) is the largest k for which some k1 admits; it depends on a and d alone.1050 ok = True1051 n_mono = 0; ends = []1052 for a in (2, 3, 4, 5): # one scale: N(k)/k does not decrease, N(k) = delta_names(k, k)1053 for k in range(1, 20001):1054 n_mono += 1; ok &= delta_names(k + 1, k + 1, a) * k >= delta_names(k, k, a) * (k + 1)1055 ends.append(delta_names(20001, 20001, a))1056 ok &= n_mono == 80000 and ends == [1029078, 686271, 556370, 486813]1057 kstar = {}; n_direct = n_bound = n_scan = n_scan_k = n_scan_k1 = 0; left = []; inside = []1058 for a in range(2, 41): # by digit count: every alphabet a <= 40, every d >= 1 with a^d <= 2^4001059 d = 11060 while a ** d <= 2 ** 400:1061 n_direct += 11062 b3, b4 = 6 * a ** (d // 3 + 1), 6 * a ** (d // 4 + 1) # the bounds (i)1063 k_one = last_k(d, a, strict=True) # one scale: the largest k with N(k) < dk1064 ok &= k_one < b41065 ok &= 3 * name_cost(b3, a) >= d * b3 and delta_names(b4, b4, a) >= d * b4 # at the bounds the counts fail; the quotients do not decrease, so they fail from there on1066 by_bound = d * b3 <= a ** (d - 1)1067 scanned = d <= 12 and b3 <= 100001068 if scanned: # k*(M) by a scan of every k below twice the bound1069 scan = range(1, 2 * b3); n_scan += 1; n_scan_k += len(scan); good = []; one = 01070 for k in scan:1071 reach = d * k - 1 - 3 * name_cost(k, a) # lambda's inequality allows the k1 <= reach1072 ok &= not admits(k, max(reach, 0) + 1, d, a) # and no further k11073 for k1 in range(1, reach + 1): # every such k11074 n_scan_k1 += 11075 if admits(k, k1, d, a):1076 if not good or good[-1] != k: good.append(k)1077 if k1 == k: one = k1078 K = max(good, default=0); kstar[(a, d)] = K1079 ok &= good == list(range(1, K + 1)) and K < b3 # an initial segment, ending below the bound1080 ok &= d * K < a ** (d - 1) # directly: t(M) = d k*(M) < a^(d-1) <= m1081 inside.append((Fraction(d * K, a ** (d - 1)), a, d))1082 ok &= (K == 0) == (d <= 4) and one == k_one <= K # the one-scale threshold found both ways, at most k*(M)1083 if d >= 13: n_bound += 1; ok &= by_bound1084 elif d >= 5 and not by_bound: left.append((a, d))1085 ok &= scanned or (d >= 5 and by_bound) # every case is decided by the scan or by the bound1086 d += 11087 ok &= (n_direct, n_bound, n_scan, n_scan_k, n_scan_k1) == (4347, 3879, 243, 1070649, 1209527) and max(inside) == (Fraction(21, 32), 2, 7)1088 ok &= left == [(2, 5), (2, 6), (2, 7), (2, 8), (2, 9), (2, 10), (2, 11), (2, 12), (3, 5), (3, 6), (3, 7), (4, 5), (4, 6), (5, 5), (5, 6)]1089 ok &= all(x in kstar for x in left) and [d * kstar[(a, d)] for a, d in left] == [10, 18, 42, 72, 126, 180, 275, 396, 15, 36, 84, 20, 54, 30, 66]1090 ok &= [last_k(d, 2, strict=True) for d in (5, 9, 17, 33, 65)] == [1, 7, 43, 806, 209693] and [kstar[(2, d)] for d in (5, 9, 12)] == [2, 14, 33]1091 # the structures of D3, in exact integers: every instance the names leave open, a^n <= m^k and a^n1 <= m^k1 exactly1092 n_inst = n_one = n_try = n_k = n_below = 0; share = []; slack = None1093 for (a, m), (d, fit) in T_EXACT.items():1094 K = kstar[(a, d)]; t = d * K1095 ok &= t < m and (K == 0) == (m < a ** 4)1096 one = 01097 for k in range(1, len(fit)): # every k up to twice the bound1098 n_k += 11099 reach = fit[k] - 3 * name_cost(k, a) # every k1 with lambda's symbols within the reach of k-tuples: k1 <= reach1100 ok &= reach <= len(fit) - 1 # the table covers them all1101 for k1 in range(1, reach + 1):1102 n_try += 11103 if delta_names(k, k1, a) <= fit[k1]: # an instance left open: delta's symbols within the reach of k1-tuples1104 n_inst += 1; one += k1 == k1105 ok &= admits(k, k1, d, a) and k <= K and fit[k] < t # it is admitted in digit form, and lambda's length is below t(M)1106 slack = t - fit[k] if slack is None else min(slack, t - fit[k])1107 n_one += one1108 for k in range(1, a ** ((d - 1) // 4) // 2 + 1): # below, at one scale: each of these k is left open1109 n_below += 1; ok &= lambda_names(k, k, a) <= delta_names(k, k, a) <= fit[k]1110 share.append((Fraction(t, m), a, m))1111 ok &= (n_k, n_try, n_inst, n_one, slack, n_below) == (425112, 102969, 39624, 3615, 1, 1492) and max(share) == (Fraction(21, 32), 2, 64)1112 # 25:F6 (p25047)1113 check("D5", "the threshold lies inside the count: an instance with k coordinates in v and k1 in u needs 2c(k) + c(k+k1) < d k1 and 3c(k) + k1 < dk, d the digit count of m in base a; k*(M) is the largest k for which some k1 satisfies both, and t(M) = d k*(M) — by digit count, k*(M) depending on a and d alone, at every alphabet a <= 40 and every d >= 1 with a^d <= 2^400 (4347 cases): where d <= 12 and 6a^(floor(d/3)+1) <= 10000 (243 cases) a scan of every k below twice that bound (1070649 values) and every k1 the second inequality allows (1209527 pairs) finds the k that pass to be the k <= k*(M), with k*(M) < 6a^(floor(d/3)+1), d k*(M) < a^(d-1) <= m (at most 21/32 of a^(d-1), at a = 2, d = 7), k*(M) = 0 exactly for d <= 4, and the one-scale threshold, the largest k with 2c(k) + c(2k) < dk, found by the scan and by bisection, at most k*(M); from d = 13 on k*(M) < 6a^(floor(d/3)+1) alone gives d k*(M) < a^(d-1) (3879 cases), for d = 5..12 it leaves fifteen pairs (a, d), all scanned, and every case is decided by the scan or the bound; at one scale k < 6a^(floor(d/4)+1) in every case, and (2c(k) + c(2k))/k does not decrease (80000 steps: k <= 20000, a = 2..5); in the 1990 structures of D3, in exact integers, each of the 39624 instances the names leave open (a^n <= m^k, a^n1 <= m^k1; every k up to 12a^(floor(d/3)+1), the 425112 pairs (m, k) of D3, and every k1 within lambda's reach, 102969 pairs (k, k1)) passes in digit form and has n < t(M) (some instance reaches n = t(M) - 1), so no instance codes lambda at a length n >= t(M) under any injective codings; there t(M) < m, k*(M) = 0 exactly when m < a^4, t(M)/m is at most 21/32 (at a = 2, m = 64), and at one scale every k <= floor(a^floor((d-1)/4) / 2) is left open (1492 pairs (m, k))", ok,1114 f"{n_direct} pairs (a, d); k* at a = 2, d = 5, 9, 12: {[kstar[(2, d)] for d in (5, 9, 12)]}; one scale at d = 5, 9, 17, 33, 65: {[last_k(d, 2, strict=True) for d in (5, 9, 17, 33, 65)]}; the fifteen pairs: " + "; ".join(f"({a}, {d}): {d * kstar[(a, d)]} < {a ** (d - 1)}" for a, d in left) + f"; {n_inst} exact instances, {n_one} at one scale")11151116# ------------------------------------------------------------------------------------------------------------1117# block E: fragment truth (25:G4, G5) — Section 5.3.1118# E1: the prefix simulation — the sentence with the uniform prefix Ay1 Ex1 … Ayd Exd and the clause x_i = y_i at the1119# universal positions, evaluated as written, decides what the coded prefix Q1 … Qd decides: every pattern against EVERY1120# matrix over M_2 (depth <= 3) and M_3 (depth <= 2), and against a matrix family over M_5. E2: the guessed labels — a1121# labelling consistent with the position-local clauses and rooted true exists exactly for the well-formed true codes, and1122# it is unique; and the composition of the label layers with the pairing prefix agrees with direct truth on every string1123# of length <= 6 of a small language, conjunctions included.1124def block_E():1125 """Block E — fragment truth: the pairing prefix and the guessed labels (EXACT): E1–E2."""1126 def paired(m, pattern, matrix):1127 """The sentence of the lemma's right-hand side, evaluated by the shared evaluator: the uniform prefix Ay1 Ex1 … Ayd Exd over1128 the matrix [ AND_{i: Q_i = A} x_i = y_i & psi(x) ], the copy clauses standing in the matrix."""1129 d = len(pattern)1130 def mat(v): # v = (y1, x1, …, yd, xd)1131 ys, xs = v[0::2], v[1::2]1132 return all(xs[i] == ys[i] for i in range(d) if pattern[i] == "A") and matrix(tuple(xs))1133 return decide(m, "AE" * d, mat)1134 ok = True; n = 0; det = []1135 for m, dmax in ((2, 3), (3, 2)):1136 for d in range(1, dmax + 1):1137 pts = list(itertools.product(range(m), repeat=d))1138 for bits in range(2 ** len(pts)): # every matrix: every subset of M^d1139 S = {pt for k, pt in enumerate(pts) if (bits >> k) & 1}1140 for pat in itertools.product("AE", repeat=d):1141 n += 11142 ok &= decide(m, "".join(pat), lambda v: v in S) == paired(m, pat, lambda v: v in S)1143 det.append(f"M_{m}: every matrix to depth {dmax}")1144 n5 = 01145 for pat in itertools.product("AE", repeat=2): # over M_5, depth 2: the matrices c1 x1 + c2 x2 in S, six coefficient pairs, every S1146 for cs in ((1, 2), (3, 1), (1, 1), (2, 3), (4, 1), (0, 1)):1147 for smask in range(32):1148 S = {t for t in range(5) if (smask >> t) & 1}1149 mat = lambda v, cs=cs, S=S: sum(c * x for c, x in zip(cs, v)) % 5 in S1150 n5 += 1; ok &= decide(5, "".join(pat), mat) == paired(5, pat, mat)1151 ok &= n == 4184 and n5 == 7681152 wrong = sum(decide(2, "".join(pat), lambda v: v in S) != decide(2, "AE" * 2, lambda v: (v[1], v[3]) in S) # the control: without the copy clauses1153 for S in ({(0, 0)}, {(0, 1), (1, 0)}) for pat in itertools.product("AE", repeat=2)) # the uniform prefix decides something else1154 ok &= wrong > 01155 # 25:G4 (p25031)1156 check("E1", "the prefix simulation: the sentence Ay1 Ex1 ... Ayd Exd [x_i = y_i at the coded universal positions & psi(x)], evaluated as written by the shared evaluator, agrees with Q1 z1 ... Qd zd psi(z) on every pattern and every matrix over M_2 (depth <= 3) and M_3 (depth <= 2), 4184 instances, and on a family of 768 pattern-matrix instances over M_5 at depth 2; without the copy clauses the two differ", ok,1157 f"{n} exhaustive instances ({'; '.join(det)}) + {n5} over M_5")11581159 # E2 the guessed labels: propositional layer, then the composition with the prefix and the environments1160 def parse(s, i=0):1161 """Polish notation over T, F, N (negation), C (conjunction): (value, next position) or None."""1162 if i >= len(s): return None1163 c = s[i]1164 if c in "TF": return (c == "T", i + 1)1165 if c == "N":1166 r = parse(s, i + 1); return None if r is None else (not r[0], r[1])1167 if c == "C":1168 r1 = parse(s, i + 1)1169 if r1 is None: return None1170 r2 = parse(s, r1[1]); return None if r2 is None else (r1[0] and r2[0], r2[1])1171 return None1172 def direct(s):1173 r = parse(s); return None if r is None or r[1] != len(s) else r[0]1174 def consistent(s, ends, vals):1175 """The position-local clauses: ends[i] = the end of the subformula opening at i, vals[i] = its value."""1176 n = len(s)1177 for i, c in enumerate(s):1178 if c in "TF":1179 if not (ends[i] == i + 1 and vals[i] == (c == "T")): return False1180 elif c == "N":1181 if i + 1 >= n or not (ends[i] == ends[i + 1] and vals[i] == (not vals[i + 1])): return False1182 elif c == "C":1183 if i + 1 >= n: return False1184 j = ends[i + 1]1185 if j >= n or not (ends[i] == ends[j] and vals[i] == (vals[i + 1] and vals[j])): return False1186 return True1187 def labellings(s, root=None):1188 n = len(s); out = 01189 for ends in itertools.product(range(1, n + 1), repeat=n):1190 if ends[0] != n: continue1191 for vals in itertools.product((False, True), repeat=n):1192 if root is not None and vals[0] != root: continue1193 out += consistent(s, ends, vals)1194 return out1195 ok = True; n_codes = n_wf = 01196 for L in range(1, 5):1197 for tup in itertools.product("TFNC", repeat=L):1198 s = "".join(tup); n_codes += 1; d = direct(s)1199 if d is None: ok &= labellings(s) == 0 # an ill-formed code admits no labelling1200 else:1201 n_wf += 11202 ok &= labellings(s) == 1 and labellings(s, True) == (1 if d else 0) # exactly the labelling of its parse tree; rooted true iff true1203 ok &= (n_codes, n_wf) == (340, 24)1204 def backward(s):1205 """The one candidate labelling, computed right to left from the clauses; None if a clause cannot be met."""1206 n = len(s); ends = [0] * n; vals = [False] * n1207 for i in range(n - 1, -1, -1):1208 c = s[i]1209 if c in "TF": ends[i], vals[i] = i + 1, c == "T"1210 elif c == "N":1211 if i + 1 >= n: return None1212 ends[i], vals[i] = ends[i + 1], not vals[i + 1]1213 else:1214 if i + 1 >= n or ends[i + 1] >= n: return None1215 j = ends[i + 1]; ends[i], vals[i] = ends[j], vals[i + 1] and vals[j]1216 return (vals[0] if ends[0] == n else None)1217 n_long = 01218 for L in range(1, 9):1219 for tup in itertools.product("TFNC", repeat=L):1220 s = "".join(tup); n_long += 11221 b = backward(s); d = direct(s)1222 ok &= (b is None) == (d is None) and b == d # the pass labels exactly the well-formed codes, with their values1223 ok &= n_long == 873801224 # the composition over M_3, with the variable indices as data. A code is a string over A E N C z t e 0 1: a prefix of d1225 # quantifiers (d = 1, 2), then a matrix in Polish notation whose atoms are `z i` (x_i = 0), `t i` (x_i + x_i = 1) and `e i j`1226 # (x_i = x_j), the indices written as the tokens 0, 1. Truth is computed twice, by two separate routines.1227 ARITY = {"z": 1, "t": 1, "e": 2}1228 def d_matrix(code, i, env, d):1229 """Direct: parse the matrix from position i and evaluate it; (value, next position), or None if ill-formed."""1230 if i >= len(code): return None1231 c = code[i]1232 if c in ARITY:1233 ix = code[i + 1:i + 1 + ARITY[c]]1234 if len(ix) < ARITY[c] or any(ch not in "01" or int(ch) >= d for ch in ix): return None1235 x = [env[int(ch)] for ch in ix]1236 return ((x[0] == 0) if c == "z" else ((2 * x[0]) % 3 == 1) if c == "t" else (x[0] == x[1]), i + 1 + ARITY[c])1237 if c == "N":1238 r = d_matrix(code, i + 1, env, d); return None if r is None else (not r[0], r[1])1239 if c == "C":1240 r1 = d_matrix(code, i + 1, env, d)1241 if r1 is None: return None1242 r2 = d_matrix(code, r1[1], env, d); return None if r2 is None else (r1[0] and r2[0], r2[1])1243 return None1244 def d_truth(code):1245 d = 01246 while d < len(code) and code[d] in "AE": d += 11247 if d not in (1, 2): return None1248 wf = d_matrix(code, d, (0, 0), d)1249 if wf is None or wf[1] != len(code): return None1250 return decide(3, code[:d], lambda v: d_matrix(code, d, tuple(v) + (0,) * (2 - d), d)[0])1251 def clause(code, d, q, ends):1252 """The position-local clause on the parse label of matrix position d + q (ends[q]: the end of the subformula opening there).1253 It refers to labels at positions to its right only."""1254 n = len(code); i = d + q; c = code[i]; e = ends[q]1255 if q == 0 and e != n: return False # the root: the matrix ends where the code ends1256 if c in "zt": return i + 1 < n and code[i + 1] in "01" and e == i + 21257 if c == "e": return i + 2 < n and code[i + 1] in "01" and code[i + 2] in "01" and e == i + 31258 if c == "N": return i + 1 < n and code[i + 1] in "NCzte" and e == ends[q + 1]1259 if c == "C":1260 if not (i + 1 < n and code[i + 1] in "NCzte"): return False1261 j = ends[q + 1]1262 return j < n and code[j] in "NCzte" and e == ends[j - d]1263 if c in "01": # an index token: owned by the atom before it, its own labels inert1264 own = (i - 1 >= d and code[i - 1] in "zte") or (i - 2 >= d and code[i - 2] == "e" and code[i - 1] in "01")1265 return own and e == i + 11266 return False # a quantifier token inside the matrix1267 def structural(code, d, ends):1268 """The clauses on the ends (the parse labels), at every matrix position."""1269 return ends[0] == len(code) and all(clause(code, d, q, ends) for q in range(len(code) - d))1270 def valued(code, d, ends, vals, x):1271 """The clauses on the values, under the quantified values x: an atom's clause resolves its coded index against x by a case over1272 the d candidates (the linkage clause)."""1273 for q in range(len(code) - d):1274 i = d + q; c = code[i]; v = vals[q]1275 if c == "z":1276 if not any(code[i + 1] == str(j) and v == (x[j] == 0) for j in range(d)): return False1277 elif c == "t":1278 if not any(code[i + 1] == str(j) and v == ((x[j] + x[j]) % 3 == 1) for j in range(d)): return False1279 elif c == "e":1280 if not any(code[i + 1] == str(j1) and code[i + 2] == str(j2) and v == (x[j1] == x[j2]) for j1 in range(d) for j2 in range(d)): return False1281 elif c == "N":1282 if v != (not vals[q + 1]): return False1283 elif c == "C":1284 if v != (vals[q + 1] and vals[ends[q + 1] - d]): return False1285 elif v: return False # an index token carries the inert value1286 return True1287 def parses(code, d, search):1288 """The labellings of the ends that satisfy the structural clauses: by search over all of them, or the one candidate of the1289 right-to-left pass, checked against the clauses."""1290 n = len(code); k = n - d1291 if search: return [e for e in itertools.product(range(d + 1, n + 1), repeat=k) if structural(code, d, e)]1292 ends = [0] * k1293 for q in range(k - 1, -1, -1):1294 i = d + q; c = code[i]1295 if c in "zt": ends[q] = i + 21296 elif c == "e": ends[q] = i + 31297 elif c in "01": ends[q] = i + 11298 elif c == "N": ends[q] = ends[q + 1] if q + 1 < k else 01299 elif c == "C":1300 j = ends[q + 1] if q + 1 < k else 01301 ends[q] = ends[j - d] if d <= j < n else 01302 return [tuple(ends)] if all(d < e <= n for e in ends) and structural(code, d, tuple(ends)) else []1303 def parses_bt(code, d):1304 """EVERY labelling of the ends that satisfies the structural clauses, by backtracking from the right: the clause at a position1305 refers only to labels on its right, so a partial labelling is extended by every value that meets the clause there."""1306 n = len(code); k = n - d; out = []1307 def rec(q, ends):1308 if q < 0: out.append(tuple(ends[x] for x in range(k))); return1309 for e in range(d + 1, n + 1):1310 ends[q] = e1311 if clause(code, d, q, ends): rec(q - 1, ends)1312 ends.pop(q, None)1313 if k > 0: rec(k - 1, {})1314 return out1315 def values(code, d, ends, x, search):1316 """The labellings of the values consistent with the clauses under x."""1317 k = len(code) - d1318 if search: return [v for v in itertools.product((False, True), repeat=k) if valued(code, d, ends, v, x)]1319 vals = [False] * k1320 for q in range(k - 1, -1, -1):1321 i = d + q; c = code[i]1322 if c == "z": vals[q] = x[int(code[i + 1])] == 0 if int(code[i + 1]) < d else False1323 elif c == "t": vals[q] = (2 * x[int(code[i + 1])]) % 3 == 1 if int(code[i + 1]) < d else False1324 elif c == "e": vals[q] = x[int(code[i + 1])] == x[int(code[i + 2])] if max(int(code[i + 1]), int(code[i + 2])) < d else False1325 elif c == "N": vals[q] = not vals[q + 1]1326 elif c == "C": vals[q] = vals[q + 1] and vals[ends[q + 1] - d]1327 return [tuple(vals)] if valued(code, d, ends, tuple(vals), x) else []1328 def l_truth(code, mode):1329 """Truth by guessed labels: a prefix length d, checked against the token classes; the parse labels; and, under the uniform1330 pairing prefix whose copy clauses are read off the coded prefix, value labels rooted true. mode "all": every labelling of1331 ends and values is tried (the ends over the full product); "search": the same, the ends by backtracking; "pass": the one1332 candidate of the right-to-left pass, checked against the clauses."""1333 n = len(code)1334 for d in (1, 2):1335 if not (d < n and all(code[k] in "AE" for k in range(d)) and code[d] not in "AE"): continue1336 ps = parses(code, d, True) if mode == "all" else parses_bt(code, d) if mode == "search" else parses(code, d, False)1337 rooted = {} # the matrix of the paired sentence at x: some labelling is rooted true1338 def matrix(x): # (it reads x alone, so each x is labelled once)1339 if x not in rooted: rooted[x] = any(v[0] for e in ps for v in values(code, d, e, x + (0,) * (2 - d), mode != "pass"))1340 return rooted[x]1341 if paired(3, code[:d], matrix): return True1342 return False1343 n_comp = n_comp_wf = n_true = n_pairs = 01344 for L in range(1, 6): # every string of length <= 5: the labellings over the full product1345 for tup in itertools.product("AENCzte01", repeat=L):1346 code = "".join(tup); n_comp += 11347 want = d_truth(code); got = l_truth(code, "all")1348 ok &= got == (want is True) == l_truth(code, "pass") # the labelled truth holds exactly for the well-formed true codes1349 n_comp_wf += want is not None; n_true += want is True1350 for d in (1, 2): # and the backtracking search finds exactly the labellings of the full product1351 if d < L: n_pairs += 1; ok &= sorted(parses_bt(code, d)) == sorted(parses(code, d, True))1352 ok &= (n_comp, n_comp_wf, n_true, n_pairs) == (66429, 64, 36, 132759)1353 n6 = n6_wf = n6_true = 01354 for tup in itertools.product("AENCzte01", repeat=6): # every string of length 6, the labellings by the complete search:1355 code = "".join(tup); n6 += 1 # the shortest codes with a conjunction are among them1356 want = d_truth(code); ok &= l_truth(code, "search") == (want is True)1357 n6_wf += want is not None; n6_true += want is True1358 ok &= n6 == 531441 and 0 < n6_true < n6_wf1359 ok &= d_truth("ECCz0z0t0") is False and not l_truth("ECCz0z0t0", "search") # a false conjunction is not labelled true,1360 ok &= d_truth("ECz0z0z0") is None and not l_truth("ECz0z0z0", "search") # nor a conjunction followed by a stray atom1361 def matrices(size, d, memo={}):1362 """Every well-formed matrix of exactly `size` tokens over d variables."""1363 if (size, d) not in memo:1364 out = [c + str(i) for c in "zt" for i in range(d)] if size == 2 else [("e" + str(i) + str(j)) for i in range(d) for j in range(d)] if size == 3 else []1365 if size > 2: out += ["N" + m for m in matrices(size - 1, d)]1366 for a in range(2, size - 2): out += ["C" + m1 + m2 for m1 in matrices(a, d) for m2 in matrices(size - 1 - a, d)]1367 memo[(size, d)] = out1368 return memo[(size, d)]1369 n_big = n_big_true = n_edit = n_edit_wf = 01370 for d in (1, 2): # every well-formed code with a matrix of at most 7 tokens,1371 for pref in itertools.product("AE", repeat=d): # by the complete search and by the pass1372 for size in range(2, 8):1373 for mat in matrices(size, d):1374 code = "".join(pref) + mat; n_big += 11375 want = d_truth(code); ok &= want is not None and l_truth(code, "search") == want == l_truth(code, "pass"); n_big_true += want1376 eds = [code[:pos] + tok + code[pos + 1:] for pos in range(len(code)) for tok in "AENCzte01" if tok != code[pos]]1377 eds += [code + tail for tail in ("z0", "t0", "0", "N")] # every one-token edit, and four extensions: an ill-formed code is rejected1378 for ed in eds:1379 n_edit += 1; w2 = d_truth(ed); ok &= l_truth(ed, "search") == (w2 is True); n_edit_wf += w2 is not None1380 ok &= (n_big, n_big_true) == (1540, 654) and n_edit == 108048 and 0 < n_edit_wf < n_edit1381 # 25:G5 (p25032)1382 check("E2", "fragment truth by guessed labels, on small languages: on the propositional layer a consistent labelling exists exactly for the well-formed codes, is unique, and is rooted true exactly for the true ones (all 340 codes of length <= 4 over every labelling; all 87380 codes of length <= 8 by the right-to-left pass); with the variable indices coded as data, the labelled truth — parse labels, value labels, linkage clauses by cases, the pairing prefix — holds exactly for the well-formed true codes, against a separate direct evaluator over M_3: on all 66429 strings of length <= 5 over nine tokens (every labelling), on all 531441 strings of length 6 (every labelling, the ends by a complete backtracking search), on the 1540 well-formed codes with a matrix of at most 7 tokens, and on 108048 one-token edits and extensions of them", ok,1383 f"{n_codes} codes ({n_wf} well-formed) over every labelling; {n_long} by the pass; composition: {n_comp} strings ({n_comp_wf} well-formed, {n_true} true), {n6} strings of length 6 ({n6_wf} well-formed, {n6_true} true), {n_big} well-formed codes ({n_big_true} true), {n_edit} edits and extensions ({n_edit_wf} well-formed)")13841385# ------------------------------------------------------------------------------------------------------------1386# block F: second-order decidability and the trichotomy's middle cell (25:H2, H5) — Section 6.1387# F1: over a finite domain a second-order quantifier over k-ary relations ranges over the 2^(m^k) subsets of M^k, so1388# second-order sentences are decided by enumeration: the counts for five (m, k), and four sentences decided on |X| = 3.1389# F2: the theory "at least n elements, for every n" with a free unary predicate P — each finite part of it has models1390# with P empty and with P non-empty, so it decides neither Ex P(x) nor its negation, and Ax not P(x) completes it; the1391# theory of a finite model decides every sentence of the sample.1392def block_F():1393 """Block F — second-order decidability and the trichotomy's middle cell (EXACT): F1–F2."""1394 ok = True; det = []1395 for m, k in ((2, 1), (2, 2), (3, 1), (3, 2), (2, 3)):1396 pts = list(itertools.product(range(m), repeat=k))1397 rels = sum(1 for _ in itertools.product((0, 1), repeat=len(pts))) # every k-ary relation, enumerated1398 ok &= rels == 2 ** (m ** k); det.append(f"(m,k)=({m},{k}): {rels}")1399 X = range(3); pairs = [(i, j) for i in X for j in X]1400 found = {"order": False, "inj_not_onto": False, "all_have_min": True, "equiv_classes": set()}1401 n = n_fun = n_injf = n_onto = n_bij = 01402 for bits in itertools.product((0, 1), repeat=9):1403 R = {pq for pq, b in zip(pairs, bits) if b}; n += 11404 functional = all(sum((i, j) in R for j in X) == 1 for i in X)1405 if functional:1406 n_fun += 11407 injective = not any((i, j) in R and (i2, j) in R for j in X for i in X for i2 in X if i != i2) # no value is taken twice1408 onto = all(any((i, j) in R for i in X) for j in X) # every element is a value1409 n_injf += injective; n_onto += onto; n_bij += injective and onto1410 if injective and not onto: found["inj_not_onto"] = True # an injective function that is not onto: the scan finds none1411 irr = all((i, i) not in R for i in X)1412 tra = all((i, k2) in R for (i, j) in R for (j2, k2) in R if j == j2)1413 tot = all((i, j) in R or (j, i) in R for i in X for j in X if i != j)1414 if irr and tra and tot:1415 found["order"] = True1416 for sub in itertools.product((0, 1), repeat=3): # second-order over subsets: every non-empty subset has a least element1417 S = [x for x in X if sub[x]]1418 if S: found["all_have_min"] &= any(all(x == y or (x, y) in R for y in S) for x in S)1419 refl = all((i, i) in R for i in X); sym = all((j, i) in R for (i, j) in R)1420 if refl and sym and tra: found["equiv_classes"].add(frozenset(frozenset(j for j in X if (i, j) in R) for i in X))1421 ok &= n == 512 and found["order"] and not found["inj_not_onto"] and found["all_have_min"] and len(found["equiv_classes"]) == 51422 ok &= (n_fun, n_injf, n_onto, n_bij) == (27, 6, 6, 6) # 27 graphs of functions among the relations: 6 injective, 6 onto, the same 61423 # 25:H2 (p25036)1424 check("F1", "second-order decidability on a finite domain: a quantifier over k-ary relations ranges over 2^(m^k) relations (enumerated for five (m, k)); on 3 elements, over all 512 binary relations: a strict total order exists, every one well-orders the non-empty subsets, among the 27 functions the 6 injective ones are the 6 onto ones, and the equivalence relations are the 5 partitions", ok,1425 "; ".join(det))14261427 ok = True; det = []1428 at_least = lambda s, n: decide(s, "E" * n, lambda v: len(set(v)) == n) # the axiom "there are at least n elements", decided over a domain of s elements1429 n_struct = 01430 for N in range(1, 5): # the first N axioms, over every structure (domain of s <= 5 elements, a unary predicate P)1431 seen = {}1432 for s in range(1, 6):1433 sat = all(at_least(s, n) for n in range(1, N + 1))1434 ok &= sat == (s >= N) # the models of the first N axioms: the structures of at least N elements1435 for P in itertools.product((0, 1), repeat=s):1436 n_struct += 11437 if sat: seen.setdefault(s, set()).add(decide(s, "E", lambda v: P[v[0]] == 1)) # the value of Ex P(x) in the model1438 ok &= all(vals == {False, True} for vals in seen.values()) # in every model size both values occur: the N axioms decide neither Ex P(x) nor its negation1439 ok &= not all(at_least(N, n) for n in range(1, N + 2)) # no structure of N elements satisfies the next axiom1440 for s in seen: # the completing axiom Ax not P(x) leaves one value1441 ok &= {decide(s, "E", lambda v: P[v[0]] == 1) for P in itertools.product((0, 1), repeat=s) if decide(s, "A", lambda v: P[v[0]] == 0)} == {False}1442 det.append(f"N <= 4: {n_struct} structures decided; both values of Ex P(x) among the models of the first N axioms; none of N elements satisfies N+1 axioms")1443 ok &= n_struct == 4 * (2 + 4 + 8 + 16 + 32) == 2481444 for p in (2, 3, 5): # cell (iii): the theory of a finite model decides every sentence of the sample1445 ok &= all(decide(p, pat, mat) == want for _, pat, mat, want in sentences(p))1446 # 25:H5 (p25039)1447 check("F2", "the trichotomy's middle cell on its finite parts: the first N axioms 'at least n elements' (n <= N <= 4), decided over all 248 structures of at most 5 elements with a unary predicate P, have models with Ex P(x) true and with it false, so they decide neither it nor its negation, and Ax not P(x) settles it; no structure of N elements satisfies N+1 of the axioms; the theory of a finite model (M_2, M_3, M_5) gives every sentence of a sample of 8 its value", ok,1448 "; ".join(det))14491450# ------------------------------------------------------------------------------------------------ block G1451# block G: the window below the threshold (25:F7, F8, G8) — Section 5.2, Lemma decoders, Theorem instance, Corollary windowtruth.1452#1453# Language: +, * and the constants 0, ..., f (the elements 0..15) and g (16), over the field F_p. Alphabet: the 32 symbols1454# of SYMS. A variable is a letter (u, v, x) and an index of fixed width. A string is coded D symbols per element in1455# base 32, the pad symbol being the digit 0. The proofs, for every prime under the stated side conditions:1456# (1) seg_J(x, w) <=> x = w n for some 0 <= n < 2^J. J = 0: x = 0. Step: x = y + b w with b in {0, 1} and1457# y = 2w n', so x = w (2n' + b). Int_J(x) = seg_J(x, 1): for 2^J <= p it defines {0, ..., 2^J - 1}.1458# (2) inrange(t, N), for N <= 2^E and 2^(E+1) < p: t and m lie in [0, 2^E) and t + m + 1 = N in F_p; both sides are1459# below p as integers, so the equation holds in the integers and t < N. Conversely m = N - 1 - t.1460# (3) Pow(r, z), for 2^e <= p: by induction r = w sum b_j 2^j and z = prod c^(2^j b_j) for bits b_j; the bits of r are1461# unique, so z = beta^r and r < 2^e.1462# (4) Dig(y, r, s), for 2^(b n + 1) < p, n <= 2^e, 2^(e+1) <= p: if it holds then r < n, z = beta^r, z2 = beta^(n-1-r),1463# s < beta, lo < z, hi < z2, so lo + z (s + beta hi) is an integer below beta^n < p and equals y: s is digit r1464# of y. Conversely the digits of y < beta^n are witnesses.1465# (5) Diag(u, v), for p > 2^(5D+5) and every u_j < 32^D: the auxiliary variables are confined by (2) and by the1466# access formulas to ranges below 2^E, so every equation among them is an equation of integers. The cases (copy1467# before the blocks, in a block before and after the token, after the blocks; numeral; pad) partition the positions1468# below D k, and in each the symbol is unique. The clause on v forces every v_i < 32^D by (4). So Diag(u, v)1469# holds iff v codes F(u): the string of u with the token of u_i replaced by the numeral of the element u_i.1470# (6) The fixed point: delta carries its own layout constants as numerals of fixed width. The numerals of lambda denote1471# the coordinates of the code of delta. By (5), Diag(code delta, v) holds iff v = code lambda. So1472# F_p |= lambda iff theta(code lambda).1473# G1 model-checks the written formulas of (1)-(4) on small prime fields, exhaustively. G2 model-checks the written Diag1474# on F_257 (4 symbols, 3 per element) against the substitution computed from its definition, and builds the instance as1475# strings. G3 builds it with the longest theta. At the scale of the instance no model check is possible; there the1476# fixed point rests on (1)-(6).1477def _deep(fn):1478 """Run fn in a thread with a large stack: the formulas of block G nest tens of thousands of quantifiers."""1479 import threading1480 box = {}1481 def run():1482 try: box["r"] = fn()1483 except BaseException as e: box["e"] = e1484 lim, stack = sys.getrecursionlimit(), threading.stack_size()1485 sys.setrecursionlimit(1 << 22); threading.stack_size(1 << 29)1486 try:1487 t = threading.Thread(target=run); t.start(); t.join()1488 finally:1489 sys.setrecursionlimit(lim); threading.stack_size(stack)1490 if "e" in box: raise box["e"]1491 return box.get("r")14921493def _dense():1494 """The formulas of block G, their printer, a model checker for small prime fields, and the instance as strings."""1495 SYMS = " 0123456789abcdefg+*=()&|~EAuvx>" # code = index; ' ' pads1496 assert len(SYMS) == 32 and len(set(SYMS)) == 321497 CODE = {c: i for i, c in enumerate(SYMS)}1498 HEX = "0123456789abcdef"1499 CONSTVAL = {c: i for i, c in enumerate(HEX)}; CONSTVAL['g'] = 161500 HINT = {} # id(formula) -> (variable, bound term, formula): the formula implies 0 <= variable < bound15011502 def V(n): return ('var', n)1503 def C(ch): return ('const', ch)1504 def add(a, b): return ('add', a, b)1505 def mul(a, b): return ('mul', a, b)1506 def eq(a, b): return ('eq', a, b)1507 def AND(*fs): return ('and', list(fs))1508 def OR(*fs): return ('or', list(fs))1509 def imp(a, b): return ('imp', a, b)1510 def al(n, f): return ('all', n, f)1511 def ex(names, f):1512 for n in reversed(names if isinstance(names, (list, tuple)) else [names]): f = ('ex', n, f)1513 return f1514 ZERO, ONE = C('0'), C('1')15151516 def num(n, width):1517 """The Horner numeral of n in base 16 with exactly `width` digits: (c0+(g*(c1+(g*( ... 0)))))."""1518 assert 0 <= n < 16 ** width, (n, width)1519 t = ZERO1520 for i in reversed(range(width)): t = add(C(HEX[(n >> (4 * i)) & 15]), mul(C('g'), t))1521 return t15221523 def numstr(n, width):1524 return "".join("(" + HEX[(n >> (4 * i)) & 15] + "+(g*" for i in range(width)) + "0" + "))" * width15251526 def pr(node, out, sub=None):1527 k = node[0]1528 if k == 'var': out.append(sub.get(node[1], node[1]) if sub else node[1])1529 elif k == 'const': out.append(node[1])1530 elif k in ('add', 'mul'):1531 out.append('('); pr(node[1], out, sub); out.append('+' if k == 'add' else '*'); pr(node[2], out, sub); out.append(')')1532 elif k == 'eq': pr(node[1], out, sub); out.append('='); pr(node[2], out, sub)1533 elif k in ('and', 'or'):1534 out.append('(')1535 for i, f in enumerate(node[1]):1536 if i: out.append('&' if k == 'and' else '|')1537 pr(f, out, sub)1538 out.append(')')1539 elif k == 'imp': out.append('('); pr(node[1], out, sub); out.append('>'); pr(node[2], out, sub); out.append(')')1540 elif k == 'not': out.append('~'); pr(node[1], out, sub)1541 else: out.append('E' if k == 'ex' else 'A'); out.append(node[1]); pr(node[2], out, sub)15421543 def show(node, sub=None):1544 out = []; pr(node, out, sub); return "".join(out)15451546 # -- the model checker1547 class Ev:1548 """Truth of a formula in the field F_p. A quantifier runs over a candidate set that contains every value of its1549 variable on which the body (for a universal: the guard of the implication) can hold; each candidate is then1550 evaluated in full. Candidates come from equations solved for the variable (cand), or from a registered range1551 (HINT), which Part 1 verifies exhaustively on the same field."""1552 def __init__(s, p, naive=False): s.p = p; s.memo = {}; s.fvc = {}; s.fvt = {}; s.ct = {}; s.hints_used = 0; s.naive = naive1553 def fv(s, n):1554 r = s.fvc.get(id(n))1555 if r is not None: return r[1]1556 k = n[0]1557 if k == 'var': r = frozenset([n[1]])1558 elif k == 'const': r = frozenset()1559 elif k in ('add', 'mul', 'eq', 'imp'): r = s.fv(n[1]) | s.fv(n[2])1560 elif k in ('and', 'or'): r = frozenset().union(*[s.fv(f) for f in n[1]])1561 elif k == 'not': r = s.fv(n[1])1562 else: r = s.fv(n[2]) - {n[1]}1563 s.fvc[id(n)] = (n, r); return r # the node is kept alive, so its id is never reused1564 def tv(s, t, env):1565 k = t[0]1566 if k == 'var': return env[t[1]]1567 if k == 'const': return CONSTVAL[t[1]] % s.p1568 closed = not s.fv(t)1569 if closed and id(t) in s.ct: return s.ct[id(t)]1570 a = s.tv(t[1], env); b = s.tv(t[2], env)1571 r = (a + b) % s.p if k == 'add' else (a * b) % s.p1572 if closed: s.ct[id(t)] = r1573 return r1574 def ok(s, t, env, blocked): return all(v in env and v not in blocked for v in s.fv(t))1575 def solve(s, x, e, env, blocked):1576 A, B = e[1], e[2]1577 ia, ib = x in s.fv(A), x in s.fv(B)1578 if ia == ib: return None1579 if ib: A, B = B, A1580 if not s.ok(B, env, blocked): return None1581 tgt = s.tv(B, env); t = A1582 while t[0] != 'var':1583 l, r = t[1], t[2]1584 il, ir = x in s.fv(l), x in s.fv(r)1585 if il and ir: return None1586 other, nxt = (r, l) if il else (l, r)1587 if not s.ok(other, env, blocked): return None1588 ov = s.tv(other, env)1589 if t[0] == 'add': tgt = (tgt - ov) % s.p1590 else:1591 if ov == 0: return None1592 tgt = tgt * pow(ov, -1, s.p) % s.p1593 t = nxt1594 return {tgt}1595 def cand(s, x, f, env, blocked):1596 k = f[0]1597 if k == 'eq': return s.solve(x, f, env, blocked)1598 if k == 'and':1599 res = None1600 for g in f[1]:1601 if x not in s.fv(g):1602 if g[0] == 'eq' and s.ok(g, env, blocked) and s.tv(g[1], env) != s.tv(g[2], env): return set()1603 continue1604 c = s.cand(x, g, env, blocked)1605 if c is not None: res = c if res is None else (res & c)1606 return res1607 if k == 'or':1608 res = set()1609 for g in f[1]:1610 if x not in s.fv(g): return None1611 c = s.cand(x, g, env, blocked)1612 if c is None: return None1613 res |= c1614 return res1615 if k == 'ex':1616 if f[1] == x: return None1617 return s.cand(x, f[2], env, blocked | {f[1]})1618 return None1619 def domain(s, x, f, env):1620 if s.naive: return range(s.p) # every quantifier over the whole field1621 c = s.cand(x, f, env, frozenset())1622 if c is not None: return c1623 h = HINT.get(id(f))1624 if h is not None and h[0] == x and s.ok(h[1], env, frozenset()): s.hints_used += 1; return range(s.tv(h[1], env))1625 return range(s.p)1626 def ev(s, f, env):1627 k = f[0]1628 if k == 'eq': return s.tv(f[1], env) == s.tv(f[2], env)1629 if k == 'and':1630 for g in f[1]:1631 if not s.ev(g, env): return False1632 return True1633 if k == 'or':1634 for g in f[1]:1635 if s.ev(g, env): return True1636 return False1637 if k == 'not': return not s.ev(f[1], env)1638 if k == 'imp': return (not s.ev(f[1], env)) or s.ev(f[2], env)1639 fl = s.fvt.get(id(f))1640 if fl is None: fl = s.fvt[id(f)] = tuple(sorted(s.fv(f)))1641 key = (id(f),) + tuple(env[v] for v in fl)1642 r = s.memo.get(key)1643 if r is not None: return r1644 x, body = f[1], f[2]1645 had = x in env; old = env.get(x)1646 if k == 'ex':1647 r = False1648 for val in s.domain(x, body, env):1649 env[x] = val1650 if s.ev(body, env): r = True; break1651 else:1652 r = True1653 for val in (s.domain(x, body[1], env) if body[0] == 'imp' else range(s.p)):1654 env[x] = val1655 if not s.ev(body, env): r = False; break1656 if had: env[x] = old1657 else: env.pop(x, None)1658 s.memo[key] = r; return r16591660 # -- the formulas1661 class Gen:1662 def __init__(s, wx=2, cw=10): s.wx = wx; s.cw = cw1663 def X(s, i): return 'x' + format(i, '0%dx' % s.wx)1664 def K(s, n): return num(n, s.cw)1665 # -- x in {w*n : 0 <= n < 2^J}1666 def seg(s, x, w, J, P, Q):1667 if J == 0: return eq(V(x), ZERO)1668 y, w2 = P1669 return ex(y, AND(OR(eq(V(x), V(y)), eq(V(x), add(V(y), V(w)))),1670 ex(w2, AND(eq(V(w2), add(V(w), V(w))), s.seg(y, w2, J - 1, Q, P)))))1671 # -- Int_J(t): t in [0, 2^J) (true initial segment when 2^J <= p)1672 def Int(s, t, J):1673 X, W = s.X(0), s.X(1)1674 return ex([X, W], AND(eq(V(X), t), eq(V(W), ONE), s.seg(X, W, J, (s.X(2), s.X(3)), (s.X(4), s.X(5)))))1675 # -- 0 <= t < N, for N <= 2^E and 2^(E+1) < p1676 def inrange(s, t, N, E):1677 m, om = s.X(18), s.X(19)1678 return ex(m, AND(eq(add(add(t, V(m)), ONE), N),1679 al(om, imp(OR(eq(V(om), t), eq(V(om), V(m))), s.Int(V(om), E)))))1680 # -- z = (2^bbits)^r and 0 <= r < 2^e; needs 2^e <= p (the binary expansion of r is then unique)1681 def powrec(s, r, z, c, w, e, A, B):1682 if e == 0: return AND(eq(V(r), ZERO), eq(V(z), ONE))1683 r1, z1, w2, c2 = A1684 return ex([r1, z1], AND(OR(AND(eq(V(r), V(r1)), eq(V(z), V(z1))),1685 AND(eq(V(r), add(V(r1), V(w))), eq(V(z), mul(V(z1), V(c))))),1686 ex([w2, c2], AND(eq(V(w2), add(V(w), V(w))), eq(V(c2), mul(V(c), V(c))),1687 s.powrec(r1, z1, c2, w2, e - 1, B, A)))))1688 def Pow(s, rt, zt, bbits, e):1689 R, Z, Cc, W = (s.X(i) for i in (6, 7, 8, 9))1690 A = tuple(s.X(i) for i in (10, 11, 12, 13)); B = tuple(s.X(i) for i in (14, 15, 16, 17))1691 return ex([R, Z, Cc, W], AND(eq(V(R), rt), eq(V(Z), zt), eq(V(Cc), num(1 << bbits, 2)), eq(V(W), ONE),1692 s.powrec(R, Z, Cc, W, e, A, B)))1693 # -- st is digit number rt of yt in base 2^bbits, for yt < (2^bbits)^nd; needs 2^(bbits*nd+1) < p, nd <= 2^e and 2^(e+1) <= p1694 def Dig(s, yt, rt, st, bbits, nd, e):1695 z, z2, lo, hi, m1, m2, om, r2 = (s.X(i) for i in range(20, 28))1696 beta = num(1 << bbits, 2); J = bbits * nd1697 ints = al(om, imp(OR(eq(V(om), V(lo)), eq(V(om), V(m1)), eq(V(om), V(hi)), eq(V(om), V(m2))), s.Int(V(om), J)))1698 f4 = ex([m1, m2], AND(eq(add(add(V(lo), V(m1)), ONE), V(z)), eq(add(add(V(hi), V(m2)), ONE), V(z2)), ints))1699 f3 = ex([lo, hi], AND(eq(yt, add(V(lo), mul(V(z), add(st, mul(beta, V(hi)))))), f4))1700 f2 = ex(z2, AND(s.Pow(V(r2), V(z2), bbits, e), f3))1701 f1 = ex(z, AND(s.Pow(rt, V(z), bbits, e), f2))1702 return ex(r2, AND(eq(add(add(rt, V(r2)), ONE), s.K(nd)), s.inrange(st, beta, bbits), f1))1703 def access(s, jv, xv, cls, cnt, wtok, iw):1704 return ('or', [AND(eq(V(jv), num(i, iw)), eq(V(xv), V(cls + format(i, '0%dx' % wtok)))) for i in range(cnt)])1705 # -- Diag(u, v): the string coded by v is the string coded by u with the token of u_i replaced by the numeral of u_i1706 def diag(s, P):1707 q, i, r, y, sv, j, x, rr, t, io, ro, h, o, c, qs, mm = (s.X(n) for n in range(32, 48))1708 D, k, k1, H, S, B, R0, WU, N1, E = (P[n] for n in 'D k k1 H S B R0 WU N1 E'.split())1709 W = 8 * H + 1; B2 = B - WU + W; NL = N1 + k1 * (W - WU); NOUT = D * k1710 assert NL <= NOUT <= 1 << E and S + k1 * B <= N1 <= D * k1 and R0 + WU <= B1711 K = s.K; cd = P['codes']; sym = lambda ch: K(cd[ch])1712 rng = lambda tt, n: s.inrange(tt, K(n), E)1713 digA = lambda yt, rt, st: s.Dig(yt, rt, st, P['SB'], D, P['ea'])1714 digH = lambda yt, rt, st: s.Dig(yt, rt, st, P['NB'], H, P['eh'])1715 def exr(xn, n, *conj):1716 body = AND(rng(V(xn), n), *conj); HINT[id(body)] = (xn, K(n), body); return ('ex', xn, body)1717 numsym = OR(1718 exr(h, H, ex(o, AND(eq(V(t), add(mul(V(h), K(6)), V(o))), rng(V(o), 6),1719 OR(AND(eq(V(o), K(0)), eq(V(sv), sym('('))),1720 AND(eq(V(o), K(1)), ex(c, AND(digH(V(x), V(h), V(c)), eq(V(sv), add(V(c), sym('0')))))),1721 AND(eq(V(o), K(2)), eq(V(sv), sym('+'))),1722 AND(eq(V(o), K(3)), eq(V(sv), sym('('))),1723 AND(eq(V(o), K(4)), eq(V(sv), sym('g'))),1724 AND(eq(V(o), K(5)), eq(V(sv), sym('*'))))))),1725 AND(eq(V(t), K(6 * H)), eq(V(sv), sym('0'))),1726 exr(mm, 2 * H, eq(V(t), add(K(6 * H + 1), V(mm))), eq(V(sv), sym(')'))))1727 src = OR(AND(rng(V(q), S), eq(V(qs), V(q))),1728 exr(io, k1, ex(ro, AND(eq(V(q), add(add(K(S), mul(V(io), K(B2))), V(ro))), rng(V(ro), R0),1729 eq(V(qs), add(add(K(S), mul(V(io), K(B))), V(ro)))))),1730 exr(io, k1, ex(ro, AND(eq(V(q), add(add(K(S + R0 + W), mul(V(io), K(B2))), V(ro))), rng(V(ro), B2 - R0 - W),1731 eq(V(qs), add(add(K(S + R0 + WU), mul(V(io), K(B))), V(ro)))))),1732 exr(mm, N1 - S - k1 * B, eq(V(q), add(K(S + k1 * B2), V(mm))), eq(V(qs), add(K(S + k1 * B), V(mm)))))1733 copy = exr(rr, D, ex(qs, AND(eq(V(qs), add(mul(V(j), K(D)), V(rr))), src, digA(V(x), V(rr), V(sv)))))1734 numc = ex(t, AND(eq(V(q), add(add(K(S + R0), mul(V(j), K(B2))), V(t))), rng(V(t), W), numsym))1735 pad = ex(mm, AND(eq(V(q), add(K(NL), V(mm))), s.Int(V(mm), E), eq(V(sv), sym(' '))))1736 out = OR(pad, ex([j, x], AND(s.access(j, x, 'u', k1, P['wu'], P['iwu']), OR(copy, numc))))1737 body = ex([i, r], AND(eq(V(q), add(mul(V(i), K(D)), V(r))), rng(V(r), D),1738 ex(y, AND(s.access(i, y, 'v', k, P['wv'], P['iwv']), ex(sv, AND(digA(V(y), V(r), V(sv)), out))))))1739 guard = rng(V(q), NOUT); HINT[id(guard)] = (q, K(NOUT), guard)1740 return al(q, imp(guard, body))17411742 # -- the reference substitution, and an independent reader of printed formulas1743 def F_ref(us, P):1744 """The substitution on strings, from its definition (no case analysis on output positions)."""1745 D, k, k1, H, S, B, R0, WU, N1 = (P[n] for n in 'D k k1 H S B R0 WU N1'.split())1746 SB, NB, cd = P['SB'], P['NB'], P['codes']1747 sin = [(us[q // D] >> (SB * (q % D))) & ((1 << SB) - 1) for q in range(N1)]1748 def NUM(xv):1749 o = []1750 for hh in range(H): o += [cd['('], cd['0'] + ((xv >> (NB * hh)) & ((1 << NB) - 1)), cd['+'], cd['('], cd['g'], cd['*']]1751 return o + [cd['0']] + [cd[')']] * (2 * H)1752 out = sin[:S]1753 for ii in range(k1):1754 b = S + ii * B1755 out += sin[b:b + R0] + NUM(us[ii]) + sin[b + R0 + WU:b + B]1756 out += sin[S + k1 * B:N1]1757 out += [cd[' ']] * (D * k - len(out))1758 return out17591760 def pack(symlist, D, SB):1761 return [sum(c << (SB * r) for r, c in enumerate(symlist[i:i + D])) for i in range(0, len(symlist), D)]17621763 def primes_upto(n): return [q for q in range(2, n + 1) if all(q % d for d in range(2, int(q ** .5) + 1))]17641765 def read_back(s, wid):1766 """An independent reader of a printed formula (fixed name widths `wid` per letter): the formula as a tree."""1767 n = len(s); match = [0] * n; st = []1768 for i, c in enumerate(s):1769 if c == '(': st.append(i)1770 elif c == ')': match[st.pop()] = i1771 assert not st1772 def paren_is_term(i):1773 j = i + 11774 while True:1775 c = s[j]1776 if c == '(': j = match[j] + 1; continue1777 if c in '+*': return True1778 if c in '=&|>)': return False1779 j += 11780 def term(i):1781 c = s[i]1782 if c in wid: w = wid[c]; return ('var', s[i:i + 1 + w]), i + 1 + w1783 if c in CONSTVAL: return ('const', c), i + 11784 assert c == '(', (c, i)1785 a, i = term(i + 1); op = s[i]; assert op in '+*'; b, i = term(i + 1); assert s[i] == ')'1786 return ('add' if op == '+' else 'mul', a, b), i + 11787 def form(i):1788 c = s[i]1789 if c in 'EA':1790 v, j = term(i + 1); assert v[0] == 'var'; f, j = form(j); return ('ex' if c == 'E' else 'all', v[1], f), j1791 if c == '~': f, j = form(i + 1); return ('not', f), j1792 if c == '(' and not paren_is_term(i):1793 f, j = form(i + 1); fs = [f]; op = None1794 while s[j] != ')':1795 assert s[j] in '&|>' and op in (None, s[j]); op = s[j]; f, j = form(j + 1); fs.append(f)1796 if op == '>': assert len(fs) == 2; return ('imp', fs[0], fs[1]), j + 11797 return ('or' if op == '|' else 'and', fs), j + 11798 a, j = term(i); assert s[j] == '='; b, j = term(j + 1); return ('eq', a, b), j1799 f, j = form(0); assert j == n; return f1800 def same(a, b):1801 stack = [(a, b)]1802 while stack:1803 a, b = stack.pop()1804 if a[0] != b[0]:1805 if {a[0], b[0]} == {'and', 'or'} and len(a[1]) == len(b[1]) == 1: stack.append((a[1][0], b[1][0])); continue1806 return False1807 k = a[0]1808 if k in ('var', 'const'):1809 if a[1] != b[1]: return False1810 elif k in ('and', 'or'):1811 if len(a[1]) != len(b[1]): return False1812 stack.extend(zip(a[1], b[1]))1813 elif k in ('ex', 'all'):1814 if a[1] != b[1]: return False1815 stack.append((a[2], b[2]))1816 elif k == 'not': stack.append((a[1], b[1]))1817 else: stack.append((a[1], b[1])); stack.append((a[2], b[2]))1818 return True1819 def free_vars(node):1820 """The free variables of a formula or term, in one pass (a counter of the binders in force)."""1821 free, bound, stack = set(), {}, [(node, 0)]1822 while stack:1823 n, leaving = stack.pop()1824 if leaving: bound[n] -= 1; continue1825 k = n[0]1826 if k == 'var':1827 if not bound.get(n[1]): free.add(n[1])1828 elif k == 'const': pass1829 elif k in ('and', 'or'): stack.extend((f, 0) for f in n[1])1830 elif k in ('ex', 'all'): bound[n[1]] = bound.get(n[1], 0) + 1; stack.append((n[1], 1)); stack.append((n[2], 0))1831 elif k == 'not': stack.append((n[1], 0))1832 else: stack.append((n[1], 0)); stack.append((n[2], 0))1833 return free1834 def instance(D, k1, theta_of=None):1835 """delta(u) = Ev (Diag(u, v) & theta(v)) at D symbols per element, as a formula and as a string. The layout constants1836 S and |delta| are written with fixed width, so writing them does not move the layout. If delta does not fill u,1837 the formula is None and the string is the one built with placeholder constants (of the same length)."""1838 g = Gen(); SB, NB = 5, 41839 H = -(-SB * D // NB); W = 8 * H + 11840 wu, iwu, wv, iwv = 3, 3, 4, 41841 WU = 1 + wu; IDX = 8 * iwu + 11842 B = 1 + 3 + 1 + IDX + 1 + 3 + 1 + WU + 1 + 1; R0 = 1 + 3 + 1 + IDX + 1 + 3 + 11843 k = k1 + -(-k1 * (W - WU) // D) # v has room for the lambda of a delta that fills u1844 assert k1 <= 16 ** wu and k <= 16 ** wv1845 E = (D * k - 1).bit_length(); ea = (D - 1).bit_length(); eh = (H - 1).bit_length()1846 assert D <= 1 << ea and H <= 1 << eh and NB * H <= SB * D + 3 # side conditions of Dig; p > 2^(5D+5) gives the rest1847 vt = ['v%04x' % i for i in range(k)]; ut = ['u%03x' % i for i in range(k1)]1848 if theta_of is None: # the sample theta: v_0 + ... + v_(k-1) = 0, which depends on every coordinate1849 t = V(vt[0])1850 for nm in vt[1:]: t = add(t, V(nm))1851 theta = eq(t, ZERO)1852 else: theta = theta_of(vt)1853 P = dict(D=D, k=k, k1=k1, H=H, S=0, B=B, R0=R0, WU=WU, N1=D * k1, E=E, SB=SB, NB=NB, ea=ea, eh=eh, wu=wu, iwu=iwu, wv=wv, iwv=iwv, codes=CODE)1854 s0 = show(ex(vt, AND(g.diag(P), theta)))1855 P = dict(P, S=s0.index('u') - R0, N1=len(s0), W=W, theta_len=len(show(theta)))1856 if len(s0) > D * k1: return g, P, None, None, s0, vt, ut1857 dg = g.diag(P); delta = ex(vt, AND(dg, theta)); s = show(delta)1858 assert len(s) == len(s0) and s.index('u') - R0 == P['S']1859 return g, P, dg, delta, s, vt, ut1860 def instance_checks(D, k1, theta_of=None, reader=True, sample=200000):1861 """The instance as strings: a dict of verdicts and the numbers the labels state."""1862 g, P, dg, delta, s, vt, ut = instance(D, k1, theta_of)1863 k, H, S, B, R0, WU, N1, W = (P[n] for n in 'k H S B R0 WU N1 W'.split())1864 B2 = B - WU + W; NL = N1 + k1 * (W - WU); r = dict(P=P, N1=N1, NL=NL, k=k)1865 r['alphabet'] = set(s) <= set(SYMS) - {' '}1866 r['fills_u'] = N1 <= D * k11867 r['tokens'] = s.count('u') == k1 and all(s[S + i * B + R0:S + i * B + R0 + WU] == ut[i] for i in range(k1))1868 r['free'] = free_vars(delta) == set(ut) and free_vars(dg) == set(ut) | set(vt)1869 r['reader'] = same(read_back(s, {'x': 2, 'u': 3, 'v': 4}), delta) if reader else None1870 sp = s + ' ' * (D * k1 - N1)1871 us = [sum(CODE[c] << (5 * q) for q, c in enumerate(sp[i * D:(i + 1) * D])) for i in range(k1)]1872 r['code'] = all(u < 32 ** D for u in us) and "".join(SYMS[(us[q // D] >> (5 * (q % D))) & 31] for q in range(N1)) == s1873 nums = [numstr(u, H) for u in us]1874 r['numerals'] = (all(nums[i] == show(num(us[i], H)) for i in (0, 1, k1 // 2, k1 - 1)) and all(len(x) == W for x in nums) and1875 all(sum(HEX.index(nums[i][1 + 6 * h]) << (4 * h) for h in range(H)) == us[i] for i in range(k1)))1876 lam = show(delta, sub=dict(zip(ut, nums)))1877 parts = [s[:S]]1878 for i in range(k1):1879 b = S + i * B; parts += [s[b:b + R0], nums[i], s[b + R0 + WU:b + B]]1880 parts.append(s[S + k1 * B:])1881 r['lambda'] = lam == "".join(parts) and len(lam) == NL and 'u' not in lam1882 r['fills_v'] = NL <= D * k1883 def rule(q): # the case analysis written in Diag1884 if q >= NL: return ' '1885 if q < S: return sp[q]1886 if q < S + k1 * B2:1887 i, o = divmod(q - S, B2)1888 if o < R0: return sp[S + i * B + o]1889 if o < R0 + W:1890 t = o - R01891 if t < 6 * H:1892 h, w = divmod(t, 6)1893 return HEX[(us[i] >> (4 * h)) & 15] if w == 1 else "(?+(g*"[w]1894 return '0' if t == 6 * H else ')'1895 return sp[S + i * B + (o - R0 - W) + R0 + WU]1896 return sp[S + k1 * B + (q - S - k1 * B2)]1897 rnd = random.Random(1); lamp = lam + ' ' * (D * k - NL)1898 qs = set(rnd.randrange(D * k) for _ in range(sample))1899 for i in (0, 1, k1 // 3, k1 - 1):1900 for off in list(range(-3, R0 + 3)) + list(range(R0 + W - 3, B2 + 3)) + list(range(R0 + 6 * H - 8, R0 + 6 * H + 8)): qs.add(S + i * B2 + off)1901 qs |= set(range(max(0, S - 5), S + 5)) | set(range(NL - 5, min(NL + 5, D * k))) | {0, D * k - 1}1902 qs = [q for q in qs if 0 <= q < D * k]1903 r['cases'] = all(rule(q) == lamp[q] for q in qs); r['n_cases'] = len(qs)1904 r['ranges'] = D * k <= 1 << P['E'] and max(NL, S + k1 * B2, D * k) < 16 ** g.cw1905 r['parts'] = (sum(1 + len(n) for n in vt), len(show(dg)), P['theta_len'],1906 len(show(g.access('x21', 'x23', 'v', k, P['wv'], P['iwv']))), len(show(g.access('x25', 'x26', 'u', k1, P['wu'], P['iwu']))))1907 return r1908 import types1909 return types.SimpleNamespace(**locals())19101911def block_G():1912 """Block G — the window below the threshold (EXACT): G1–G3."""1913 _deep(_block_G)19141915def _block_G():1916 dd = _dense(); g = dd.Gen(); V, Ev, show = dd.V, dd.Ev, dd.show1917 x0, x1, x2 = "x20", "x21", "x22"1918 ok = True; det = []1919 n = 01920 for p in dd.primes_upto(131): # Int_J on every prime field up to 1311921 J = 01922 while (1 << J) <= p:1923 f = g.Int(V(x0), J); e = Ev(p)1924 ok &= {x for x in range(p) if e.ev(f, {x0: x})} == set(range(1 << J)); n += 1; J += 11925 ok &= n == 184 and all(len(show(g.Int(V(x0), J))) == 50 * J + 29 for J in range(8))1926 det.append(f"Int_J on {n} pairs (p, J), length 50J + 29")1927 n = 01928 for p, E in ((11, 2), (19, 3), (37, 4), (67, 5), (131, 6), (257, 7)): # inrange, every N <= 2^E, 2^(E+1) < p1929 e = Ev(p)1930 for N in range(0, (1 << E) + 1):1931 f = g.inrange(V(x0), g.K(N), E)1932 ok &= {x for x in range(p) if e.ev(f, {x0: x})} == set(range(N)); n += 11933 ok &= n == 258; det.append(f"inrange on {n} pairs (p, N)")1934 n = 01935 for p in (11, 19, 37): # Pow on all of F_p^21936 for bb in (1, 2, 4, 5):1937 for ee in (0, 1, 2, 3):1938 f = g.Pow(V(x0), V(x1), bb, ee); e = Ev(p)1939 for r in range(p):1940 for z in range(p):1941 ok &= e.ev(f, {x0: r, x1: z}) == (r < (1 << ee) and z == pow(1 << bb, r, p)); n += 11942 ok &= n == 29616; det.append(f"Pow on {n} triples (p, r, z)")1943 n = 01944 for p, bb, nd, ee in ((11, 1, 2, 1), (19, 1, 3, 2), (11, 2, 1, 0), (37, 1, 4, 2), (37, 2, 2, 1)): # Dig on all of F_p^31945 assert (1 << (bb * nd + 1)) < p and nd <= (1 << ee) and (1 << (ee + 1)) <= p1946 f = g.Dig(V(x0), V(x1), V(x2), bb, nd, ee); e = Ev(p); beta = 1 << bb1947 for y in range(p):1948 for r in range(p):1949 for s in range(p):1950 ok &= e.ev(f, {x0: y, x1: r, x2: s}) == (y < beta ** nd and r < nd and s == (y // beta ** r) % beta); n += 11951 ok &= n == 110827; det.append(f"Dig on {n} triples (y, r, s), five cases")1952 L = lambda bb, nd, ee: len(show(g.Dig(V(x0), V(x1), V(x2), bb, nd, ee)))1953 c0 = L(1, 1, 0) - 100; ce = L(1, 1, 1) - L(1, 1, 0) # the length of Dig: 50 b n + 50 b + ce e + c01954 ok &= all(L(bb, nd, ee) == 50 * bb * nd + 50 * bb + ce * ee + c0 for bb in (1, 2, 5) for nd in (1, 3, 8) for ee in (0, 2, 5))1955 det.append(f"length of Dig = 50bn + 50b + {ce}e + {c0}")1956 n = 01957 for p, mk, ar in ((11, lambda: g.Int(V(x0), 3), 1), (11, lambda: g.inrange(V(x0), g.K(3), 2), 1), (13, lambda: g.inrange(V(x0), g.K(4), 2), 1),1958 (7, lambda: g.Pow(V(x0), V(x1), 1, 1), 2), (11, lambda: g.Pow(V(x0), V(x1), 2, 2), 2),1959 (11, lambda: g.Dig(V(x0), V(x1), V(x2), 1, 2, 1), 3), (11, lambda: g.Dig(V(x0), V(x1), V(x2), 2, 1, 0), 3)):1960 f = mk(); e1 = Ev(p); e2 = Ev(p, naive=True) # the pruned checker against the plain one1961 for vals in itertools.product(range(p), repeat=ar):1962 env = dict(zip((x0, x1, x2), vals)); ok &= e1.ev(f, dict(env)) == e2.ev(f, dict(env)); n += 11963 fx = g.Dig(V(x0), V(x1), V(x2), 2, 3, 2); ok &= set(Ev(11).fv(fx)) == dd.free_vars(fx) == {x0, x1, x2}1964 ok &= n == 2867; det.append(f"pruned and plain checker agree on {n} assignments")1965 # 25:F7 (p25049)1966 check("G1", "decoders over a prime field, as written formulas model-checked on small fields: Int_J(x) <=> 0 <= x < 2^J on every prime p <= 131 and every J with 2^J <= p (184 pairs), of length 50J + 29; "1967 "inrange(x, N) <=> 0 <= x < N for every N <= 2^E on six fields with 2^(E+1) < p (258 pairs); Pow(r, z) <=> r < 2^e and z = (2^b)^r on all of F_p^2 (29 616 triples); "1968 "Dig(y, r, s) <=> y < beta^n, r < n and s the digit, on all of F_p^3 (110 827 triples, five cases), of length linear in b n and e; the pruned model checker agrees with the plain one (2867 assignments)", ok,1969 "; ".join(det))19701971 # Diag as a written formula on a small field: 4 symbols (2 bits), numerals in base 2, 3 symbols per element1972 p, SB, NB, D, k1 = 257, 2, 1, 3, 21973 H = -(-SB * D // NB); W = 8 * H + 1; S, B, R0, WU, N1 = 1, 2, 1, 1, D * k11974 NL = N1 + k1 * (W - WU); k = -(-NL // D); E = 71975 cd = {' ': 0, '0': 1, '(': 3, '+': 0, 'g': 3, '*': 2, ')': 1}1976 P = dict(D=D, k=k, k1=k1, H=H, S=S, B=B, R0=R0, WU=WU, N1=N1, E=E, SB=SB, NB=NB, ea=2, eh=3, wu=1, iwu=1, wv=2, iwv=2, codes=cd)1977 assert (1 << (SB * D + 1)) < p and (1 << (NB * H + 1)) < p and D * k <= (1 << E) and (1 << (E + 1)) < p1978 f = g.diag(P); e = Ev(p); ok = True1979 for N in range(0, (1 << E) + 1): # the ranges the checker's hints use, on this field1980 fr = g.inrange(V(x0), g.K(N), E)1981 ok &= {x for x in range(p) if e.ev(fr, {x0: x})} == set(range(N))1982 rnd = random.Random(20261004); n_true = n_false = 01983 us_list = [[0, 0], [63, 63], [27, 54]] + [[rnd.randrange(64), rnd.randrange(64)] for _ in range(2)]1984 def env_of(us, vs):1985 env = {'u%x' % a: us[a] for a in range(k1)}; env.update({'v%02x' % a: vs[a] for a in range(k)}); return env1986 def variant(vs, a, r, dlt):1987 w = list(vs); dgt = (w[a] >> (SB * r)) & 3; w[a] += (((dgt + dlt) & 3) - dgt) << (SB * r); return w1988 for us in us_list:1989 vs = dd.pack(dd.F_ref(us, P), D, SB); ok &= len(vs) == k and e.ev(f, env_of(us, vs)); n_true += 11990 muts = [variant(vs, rnd.randrange(k), rnd.randrange(D), rnd.randrange(1, 4)) for _ in range(6)]1991 w = list(vs); w[rnd.randrange(k)] += 64; muts.append(w) # a coordinate that codes no string1992 w = list(vs); w[rnd.randrange(k)] = p - 1; muts.append(w)1993 for w in muts: ok &= not e.ev(f, env_of(us, w)); n_false += 11994 us = us_list[3]; vs = dd.pack(dd.F_ref(us, P), D, SB); n_one = 01995 for a in range(k): # every v at one symbol's distance, at one u1996 for r in range(D):1997 for dlt in (1, 2, 3): ok &= not e.ev(f, env_of(us, variant(vs, a, r, dlt))); n_one += 11998 ok &= (k, n_true, n_false, n_one) == (34, 5, 40, 306)1999 ok_small = ok; det_small = f"|Diag| on F_257 = {len(show(f))} symbols, the checker's range hints used {e.hints_used} times, each range verified on that field"20002001 D, k1 = 1024, 40962002 r = dd.instance_checks(D, k1)2003 pre, ldiag, lth, lav, lau = r['parts']; k = r['k']2004 ok = all(r[c] for c in ('alphabet', 'fills_u', 'tokens', 'free', 'reader', 'code', 'numerals', 'lambda', 'fills_v', 'cases', 'ranges'))2005 ok &= (k, r['N1'], D * k1, r['NL'], D * k) == (45044, 3850485, 4194304, 45781237, 46125056)2006 ok &= r['N1'] == pre + ldiag + lth + 3 and D * k1 - r['N1'] + lth == 704170 and ok_small2007 per_u = (pre + lav + lau + lth) / k1 # symbols of delta per coordinate of u, without the decoding2008 # 25:F8 (p25050)2009 check("G2", "Diag(u, v) as a written formula, model-checked on F_257 (4 symbols, 3 per element, k1 = 2, k = 34) against the substitution computed from its definition: "2010 "it holds at v = code F(u) for 5 tuples u (three fixed, two seeded), fails at 40 other v (one symbol changed; a coordinate that codes no string) "2011 "and at each of the 306 tuples v at one symbol's distance from code F(u) at one u; "2012 "the instance at D = 1024 symbols per element, k1 = 4096, k = 45044, as strings (the sample theta: v_0 + ... + v_(k-1) = 0): delta is a string over the 32 symbols, read back "2013 "by an independent reader to the same formula, with the tuple u free; |delta| = 3 850 485 <= D k1 = 4 194 304; u is named at the k1 blocks of its access formula and nowhere else; "2014 "the numerals denote the code of delta; lambda = delta(numerals) by printed and by string substitution, a sentence of 45 781 237 <= D k = 46 125 056 symbols; "2015 "the cases written in Diag give lambda at a fixed sample of positions; a theta of up to 704 170 symbols leaves |delta| <= D k1", ok,2016 f"{det_small}; |delta| = prefix {pre} + Diag {ldiag} + theta {lth} + 3; Diag = access(v) {lav} + access(u) {lau} + decoding and layout {ldiag - lav - lau}; {r['n_cases']} positions sampled; E = {r['P']['E']}")20172018 def theta_max(vt): # theta = ~T of exactly 704 170 symbols2019 t = V(vt[0])2020 for nm in vt[1:]: t = dd.add(t, V(nm))2021 return ('not', dd.AND(dd.eq(t, dd.ZERO), *([dd.eq(V(vt[0]), V(vt[0]))] * 28651), dd.eq(dd.ZERO, dd.ZERO)))2022 r = dd.instance_checks(D, k1, theta_max, reader=False, sample=20000)2023 ok = all(r[c] for c in ('alphabet', 'fills_u', 'tokens', 'free', 'code', 'numerals', 'lambda', 'fills_v', 'cases', 'ranges'))2024 ok &= r['P']['theta_len'] == 704170 and r['N1'] == D * k1 and r['NL'] <= D * r['k'] and r['k'] == k2025 lo_T = sum(len(nm) for nm in ['v%04x' % i for i in range(k)]) # a formula in all k variables names each once2026 ok &= lo_T == 225220 and 700 < per_u < 8002027 g921 = dd.instance(921, k1); g922 = dd.instance(922, k1)2028 ok &= g921[3] is None and g921[1]['N1'] > 921 * k1 and g922[3] is not None and g922[1]['N1'] <= 922 * k12029 # 25:G8 (p25051)2030 check("G3", "truth in the window: with theta = ~T of exactly 704 170 symbols (T the sum equation, 28 651 trivial equations and 0=0) delta fills u exactly, |delta| = D k1 = 4 194 304, "2031 "and lambda fits v, so every T of at most 704 169 symbols has its fixed point with ~T; a formula in all k variables has at least 225 220 symbols; "2032 "the construction spends between 700 and 800 symbols of delta per coordinate of u, fits at D = 922 and not at D = 921 (k1 = 4096, the sample theta)", ok,2033 f"|lambda| = {r['NL']} <= {D * r['k']}; symbols of delta per coordinate of u, without the decoding: {per_u:.1f}; D = 921: |delta| = {g921[1]['N1']} > {921 * k1}; D = 922: {g922[1]['N1']} <= {922 * k1}")203420352036if __name__ == "__main__":2037 import time2038 want = [a.upper() for a in sys.argv[1:]] or sorted(BLOCK)2039 bad = [b for b in want if b not in BLOCK]2040 if bad: sys.exit(f"no block {', '.join(bad)}: the blocks are {', '.join(sorted(BLOCK))}")2041 t0 = time.time()2042 for b in want:2043 t = time.time(); _run_block(b); print(f" [block {b}: {time.time() - t:.1f} s]")2044 ok = summary(write=(want == sorted(BLOCK)), expect=[i for i in LEDGER if i[0] in want])2045 kinds = {}2046 for r in RESULTS: kinds[r["kind"]] = kinds.get(r["kind"], 0) + 12047 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 ""))2048 sys.exit(0 if ok else 1)2049