The validation package of Paradoxes of Infinity as Reductio ad Absurdum: one script, reductio.py, 4 blocks, standard library only, one check per predicate of the paper's predicate ledger — 17 of 17 checks passing. The script is rendered below with an anchor per line; its markers (# 5:B5 (p05009): 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-5-reductio.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-5-reductio --find-links https://finitering.space/pkg/ (the sdist frc-5-reductio-20261012.tar.gz).
Blocks: A (6) · B (5) · C (6) · D (1) — the predicates each decides in parentheses.
1"""2reductio.py — the validation package of "Paradoxes of Infinity as Reductio ad Absurdum" (Akhtman, preprint 2025; Preprints3doi 10.20944/preprints202508.1744.v1), the paper 5-reductio of the FRC corpus (finite-ring-space/src/5-reductio), added with4the paper's predicate ledger (Appendix B, 17 September 2026; one script since 24 September 2026, the four block scripts merged).5========================================================================================================================67One script, four blocks, seventeen checks, standard library only. Each check names the predicate(s) of the paper's ledger8it witnesses (LEDGER below; predicates cited as 5:XN) under a `# 5: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/5-reductio/#<key>). Where a predicate is proved in Lean (lean/FrcCore/Reductio.lean, no11axioms; lean/FrcLedger/Reductio.lean on Mathlib), the check here is the instance the reader can run.1213 python3 reductio.py every block, results.json written; exit 1 if a check fails (≈ 10 s)14 python3 reductio.py C one block (A, B, C or D); no results.json15 from frc_5_reductio import predicate; predicate("5:E1") one predicate: its block runs once per session1617Blocks: A the arithmetic frames, their theories, the stability schema, the migration EXACT (5:B3, B5, B6, C2, C3, C5)18 B the normal forms on a finite universe EXACT (5:D2, D3, D4, D9, E8)19 C choice recovered on finite and periodic structures EXACT (5:E1–E6)20 D determinacy on the finite totality EXACT (5:D8; D2 corroborates B7)2122Everything the blocks share:23 * the arithmetic frame W_N of Definition frame — domain [0, N), the graphs of successor, addition and24 multiplication with overflow, and a first-order evaluator over it (sentences in prenex or nested form, as25 Python closures over the frame);26 * the Δ₀ evaluator over ℕ and its frame transcription φ*, with the bound t(φ) of Theorem stability;27 * hereditarily finite sets of small rank as bit masks (the antinomy normal form on a finite universe);28 * the PASS/FAIL registry every block reports into (results.json).2930Kinds: EXACT checks are exhaustive or integer-pinned computations (a pass is a proof on the tested instances);31CHART checks decide a [chart] predicate in floating point with the closed forms checked.32"""33import os, json, sys, itertools, random, math3435SCRIPT = os.path.splitext(os.path.basename(__file__))[0] # "reductio": the one script, the name results.json and the site pages carry3637# ----------------------------------------------------------------------------- registry38RESULTS = []3940# The paper's predicate ledger (Appendix B, predicates cited as 5:XN): the predicate(s) each check witnesses.41LEDGER = {42 "A1": "5:B5", "A2": "5:B3", "A3": "5:B6", "A4": "5:C2, 5:C3", "A5": "5:C5",43 "B1": "5:D2", "B2": "5:D3", "B3": "5:D4, 5:E8", "B4": "5:D9",44 "C1": "5:E1", "C2": "5:E2", "C3": "5:E3", "C4": "5:E4", "C5": "5:E5", "C6": "5:E6",45 "D1": "5:D8", "D2": "5:B7",46}4748BLOCK = {"A": "the arithmetic frames, their theories, the stability schema, the migration", # check-id prefix -> the block (the function block_<letter> below)49 "B": "the normal forms on a finite universe",50 "C": "choice recovered on finite and periodic structures",51 "D": "determinacy on the finite totality"}5253# the deciding check of each witnessed predicate: the one whose verdict decides the predicate's statement (the other checks that54# touch it are corroboration, listed by predicate() from the records)55PREDICATES = {56 "5:B3": "A2", "5:B5": "A1", "5:B6": "A3", "5:C2": "A4", "5:C3": "A4", "5:C5": "A5",57 "5:D2": "B1", "5:D3": "B2", "5:D4": "B3", "5:D8": "D1", "5:D9": "B4",58 "5:E1": "C1", "5:E2": "C2", "5:E3": "C3", "5:E4": "C4", "5:E5": "C5", "5:E6": "C6", "5:E8": "B3",59}60_RAN = set() # blocks already run in this session (predicate() runs each once)6162def check(pid, label, ok, detail="", kind="EXACT"):63 """Record one predicate check. pid = package check id; LEDGER[pid] = the paper statement(s) decided."""64 ok = bool(ok)65 rows = LEDGER.get(pid, "")66 RESULTS.append({"id": pid, "rows": rows, "block": pid[0], "script": SCRIPT, "label": label, "ok": ok, "detail": detail, "kind": kind})67 print(f" [{'PASS' if ok else 'FAIL'}] {pid:4s} {kind:6s} [{rows}] {label}" + (f" -- {detail}" if detail else ""))68 return ok6970def summary(write=True):71 n_ok = sum(r["ok"] for r in RESULTS)72 print(f"\nSUMMARY: {n_ok}/{len(RESULTS)} checks passed" + ("" if n_ok == len(RESULTS) else " <-- FAILURES"))73 if write:74 with open("results.json", "w") as f:75 json.dump(RESULTS, f, indent=1)76 return n_ok == len(RESULTS)7778def markers():79 """predicate label -> (script file, line) of its marker `# <paper>:<label> (<key>)`: the line of the check that decides it."""80 import re81 out = {}82 for i, line in enumerate(open(os.path.abspath(__file__), encoding="utf-8"), 1):83 m = re.match(r"\s*# ((?:\d+:[A-Z]+\d+[a-z]?(?: \(p\d{5}\))?)(?:, \d+:[A-Z]+\d+[a-z]?(?: \(p\d{5}\))?)*)\s*$", line)84 if m:85 for lab in re.findall(r"\d+:[A-Z]+\d+[a-z]?", m.group(1)): out.setdefault(lab, (SCRIPT + ".py", i))86 return out8788def _run_block(letter):89 if letter not in _RAN:90 globals()[f"block_{letter}"](); _RAN.add(letter)9192def predicate(label, lines=14):93 """Verify one ledger predicate: run the block of the check that decides it (once per session), print that check's source94 (from its marker) and every record that cites the predicate, and return True iff all pass."""95 pid = PREDICATES.get(label)96 if pid is None:97 print(f"{label}: no python witness (see the predicate's Lean witness or its source)"); return None98 citing = {i[0] for i, rows in LEDGER.items() if label in [t.strip() for t in rows.split(",")]}99 for b in sorted({pid[0]} | citing): _run_block(b) # the deciding block and every block whose checks cite the predicate100 mk = markers().get(label)101 if mk:102 src = open(os.path.abspath(__file__), encoding="utf-8").read().split("\n")103 print(f"— {mk[0]}:{mk[1]} (the check that decides {label}: {pid})")104 for j in range(mk[1] - 1, min(mk[1] - 1 + lines, len(src))): print(f"{j + 1:5d} {src[j]}")105 recs = [r for r in RESULTS if label in [t.strip() for t in r["rows"].split(",")]]106 ok = all(r["ok"] for r in recs)107 for r in recs:108 role = "(deciding)" if r["id"] == pid else "(corroborating)"109 print(f" [{'PASS' if r['ok'] else 'FAIL'}] {r['id']:4s} {role:16s} {r['detail'][:150]}")110 print(f"{label}: {'VERIFIED' if ok and recs else 'FAILED'} — {len(recs)} record(s)")111 return ok112113def verify_all():114 """Run every block (those already run in this session are not re-run) and print the summary; True iff every check passed."""115 for b in sorted(BLOCK): _run_block(b)116 return summary(write=False)117118# ----------------------------------------------------------------------------- the arithmetic frame W_N119class Frame:120 """W_N: domain [0, N), constant 0, order <, and the graphs S, A, M of successor, sum and product restricted to121 the domain (Definition frame). An atomic relation with an argument outside the domain is false."""122 def __init__(self, N):123 self.N = N; self.dom = range(N)124 def S(self, x, y): return 0 <= x < self.N and y == x + 1 and y < self.N125 def A(self, x, y, z): return all(0 <= v < self.N for v in (x, y, z)) and z == x + y126 def M(self, x, y, z): return all(0 <= v < self.N for v in (x, y, z)) and z == x * y127 def lt(self, x, y): return 0 <= x < self.N and 0 <= y < self.N and x < y128129def is_prime(n):130 return n > 1 and all(n % q for q in range(2, int(n ** .5) + 1))131132# ----------------------------------------------------------------------------- the Δ₀ language of the core module133# Terms: ('var', i) | ('zero',) | ('one',) | ('add', s, t) | ('mul', s, t); formulas: ('eq', s, t) | ('lt', s, t) |134# ('neg', φ) | ('conj', φ, ψ) | ('ball', t, φ) (∀ x ≤ t, φ; x is var 0 in φ, de Bruijn, t read outside).135def num(n):136 t = ('zero',)137 for _ in range(n): t = ('add', t, ('one',))138 return t139140def bex(t, phi): return ('neg', ('ball', t, ('neg', phi)))141def disj(a, b): return ('neg', ('conj', ('neg', a), ('neg', b)))142def impl(a, b): return ('neg', ('conj', a, ('neg', b)))143144def evalT(env, t):145 k = t[0]146 if k == 'var': return env[t[1]]147 if k == 'zero': return 0148 if k == 'one': return 1149 a, b = evalT(env, t[1]), evalT(env, t[2])150 return a + b if k == 'add' else a * b151152def evalF(env, f):153 """The standard value over ℕ (env: list, index 0 innermost)."""154 k = f[0]155 if k == 'eq': return evalT(env, f[1]) == evalT(env, f[2])156 if k == 'lt': return evalT(env, f[1]) < evalT(env, f[2])157 if k == 'neg': return not evalF(env, f[1])158 if k == 'conj': return evalF(env, f[1]) and evalF(env, f[2])159 b = evalT(env, f[1])160 return all(evalF([x] + env, f[2]) for x in range(b + 1))161162def evalT_frame(N, env, t):163 """The term in W_N: None when an intermediate value overflows."""164 k = t[0]165 if k == 'var': return env[t[1]] if env[t[1]] < N else None166 if k == 'zero': return 0 if 0 < N else None167 if k == 'one': return 1 if 1 < N else None168 a, b = evalT_frame(N, env, t[1]), evalT_frame(N, env, t[2])169 if a is None or b is None: return None170 v = a + b if k == 'add' else a * b171 return v if v < N else None172173def evalF_frame(N, env, f):174 """The transcription φ* in W_N: an atom with an undefined term is false; a bounded quantifier is guarded."""175 k = f[0]176 if k in ('eq', 'lt'):177 a, b = evalT_frame(N, env, f[1]), evalT_frame(N, env, f[2])178 if a is None or b is None: return False179 return a == b if k == 'eq' else a < b180 if k == 'neg': return not evalF_frame(N, env, f[1])181 if k == 'conj': return evalF_frame(N, env, f[1]) and evalF_frame(N, env, f[2])182 b = evalT_frame(N, env, f[1])183 if b is None: return False184 return all(evalF_frame(N, [x] + env, f[2]) for x in range(b + 1))185186def boundT(env, t):187 k = t[0]188 if k == 'var': return env[t[1]]189 if k in ('zero',): return 0190 if k == 'one': return 1191 return max(boundT(env, t[1]), boundT(env, t[2]), evalT(env, t))192193def boundF(env, f):194 """t(φ): the largest integer the evaluation over ℕ references (the bound of Theorem stability)."""195 k = f[0]196 if k in ('eq', 'lt'): return max(boundT(env, f[1]), boundT(env, f[2]))197 if k == 'neg': return boundF(env, f[1])198 if k == 'conj': return max(boundF(env, f[1]), boundF(env, f[2]))199 b = evalT(env, f[1])200 return max([boundT(env, f[1])] + [boundF([x] + env, f[2]) for x in range(b + 1)])201202def prime_form(i):203 """'variable i is prime': 1 < x ∧ ∀ d ≤ x ∀ e ≤ x ¬(d·e = x ∧ d ≠ 1 ∧ d ≠ x)."""204 v = lambda j: ('var', j)205 return ('conj', ('lt', ('one',), v(i)),206 ('ball', v(i), ('ball', v(i + 1), ('neg', ('conj', ('eq', ('mul', v(1), v(0)), v(i + 2)),207 ('conj', ('neg', ('eq', v(1), ('one',))), ('neg', ('eq', v(1), v(i + 2)))))))))208209def goldbach_form(M):210 """Every even m ≤ M with 4 ≤ m is a sum of two primes x, y ≤ m (the worked instance of the paper, M = 20)."""211 v = lambda j: ('var', j)212 even0 = bex(v(0), ('eq', ('add', v(0), v(0)), v(1)))213 body = bex(v(0), bex(v(1), ('conj', prime_form(1), ('conj', prime_form(0), ('eq', ('add', v(1), v(0)), v(2))))))214 return ('ball', num(M), impl(('conj', even0, ('neg', ('lt', v(0), num(4)))), body))215216def random_form(rng, depth, nvars, maxnum=6):217 """A random Δ₀ formula with the given quantifier depth."""218 def term(d):219 r = rng.random()220 if d == 0 or r < 0.4:221 return ('var', rng.randrange(nvars)) if nvars and rng.random() < 0.6 else num(rng.randrange(maxnum))222 return (rng.choice(['add', 'mul']), term(d - 1), term(d - 1))223 def form(d, nv):224 r = rng.random()225 if d == 0 or r < 0.3:226 return (rng.choice(['eq', 'lt']), term(1), term(1)) if nv else (rng.choice(['eq', 'lt']), num(rng.randrange(maxnum)), num(rng.randrange(maxnum)))227 if r < 0.45: return ('neg', form(d - 1, nv))228 if r < 0.6: return ('conj', form(d - 1, nv), form(d - 1, nv))229 return ('ball', num(rng.randrange(1, maxnum)) if not nv else (('var', rng.randrange(nv)) if rng.random() < 0.5 else num(rng.randrange(1, maxnum))), form(d - 1, nv + 1))230 nvars = 0231 return form(depth, nvars)232233# ----------------------------------------------------------------------------- hereditarily finite sets as bit masks234def hf_levels(k):235 """V_0 ⊂ V_1 ⊂ … ⊂ V_k as lists; a set of rank ≤ j is a bit mask over the elements of V_{j−1} (in the236 enumeration of level j−1). Returns the list of levels, each a list of frozensets of indices into the previous."""237 levels = [[]] # V_0 = ∅ has no elements238 for j in range(1, k + 1):239 prev = levels[-1]240 # elements of V_j are subsets of V_{j-1}; represent as frozenset of indices into V_{j-1}241 levels.append([frozenset(c) for r in range(len(prev) + 1) for c in itertools.combinations(range(len(prev)), r)])242 return levels243244# ------------------------------------------------------------------------------------------------------------245# block A: the arithmetic frames, their theories, the stability schema, the migration (5:B3, B5, B6, C2, C3, C5)246# Section 3 of the paper. A1: the theory of the frame W_N is complete and decidable — every sentence of a sample247# (and every sentence of the language, by the evaluator) is decided by evaluation in W_N, and the categorical248# sentence σ_N has exactly the N! relabelled copies of W_N as its models on a domain of size N (categoricity).249# A2: no finite model of Q — on a domain of N elements no successor map is injective and misses 0 (exhaustive over250# all N^N maps for N ≤ 7); so the frame theory does not interpret Q. A3: bounded stability — the worked instance251# (Goldbach below 20) takes its standard value in every frame above its bound t(φ), and so does every formula of a252# random sample of Δ₀ sentences; below the bound frames can disagree, and the empirical threshold is reported253# beside the proved one. A4: the migration counts — fewer than s^(K+1) records of length ≤ K, no injection of a254# domain of N elements into fewer than N records, and the certified fraction s^(K+1)/⌊c^L/2⌋ falling below every255# threshold (chart). A5: the horizon separation — a deterministic system on C configurations halts within C steps256# or revisits a configuration and runs forever; exhaustive on tiny systems, sampled on large ones.257def fo_sentences():258 """A sample of first-order sentences over the frame signature, as closures W ↦ truth value (nested quantifiers259 evaluated by finite search). Each returns a definite Boolean on every frame."""260 D = lambda W: W.dom261 return [262 ("0 is least: ∀x ¬(x < 0)", lambda W: all(not W.lt(x, 0) for x in D(W))),263 ("successor total below the top: ∀x (x+1 < N → ∃y S(x,y))", lambda W: all(any(W.S(x, y) for y in D(W)) for x in D(W) if x + 1 < W.N)),264 ("the top has no successor: ∃x ∀y ¬S(x,y)", lambda W: any(all(not W.S(x, y) for y in D(W)) for x in D(W))),265 ("addition commutes where defined: ∀x∀y∀z (A(x,y,z) → A(y,x,z))", lambda W: all(not W.A(x, y, z) or W.A(y, x, z) for x in D(W) for y in D(W) for z in D(W))),266 ("multiplication by 0: ∀x M(x,0,0)", lambda W: all(W.M(x, 0, 0) for x in D(W))),267 ("some sum overflows: ∃x∃y ∀z ¬A(x,y,z)", lambda W: any(all(not W.A(x, y, z) for z in D(W)) for x in D(W) for y in D(W))),268 ("a square below the top: ∃x∃z (x ≠ 0 ∧ M(x,x,z))", lambda W: any(x != 0 and any(W.M(x, x, z) for z in D(W)) for x in D(W))),269 ("order is linear: ∀x∀y (x<y ∨ x=y ∨ y<x)", lambda W: all(W.lt(x, y) or x == y or W.lt(y, x) for x in D(W) for y in D(W))),270 ("N is even: ∃x A(x,x,N−1)+1 …: ∃x ∃y (S(y, top) ∧ A(x,x,y))… encoded as ∃x A(x,x,N−1)", lambda W: any(W.A(x, x, W.N - 1) for x in D(W))),271 ("N−1 is prime: ∀x∀y (M(x,y,N−1) → x=1 ∨ y=1)", lambda W: all(not W.M(x, y, W.N - 1) or x == 1 or y == 1 for x in D(W) for y in D(W))),272 ]273274def block_A():275 """Block A — the arithmetic frames, their theories, the stability schema, the migration (EXACT): A1–A5."""276 # A1 per-frame completeness and decidability; categoricity of sigma_N277 ok = True; det = []278 sents = fo_sentences()279 for N in range(2, 9):280 W = Frame(N)281 vals = [s(W) for _, s in sents]282 ok &= all(v in (True, False) for v in vals) # every sentence decided by evaluation283 # categoricity: models of sigma_N on domain [0,N) are the N! relabelled copies of W_N, each satisfying the diagram284 for N in (2, 3, 4, 5):285 W = Frame(N)286 diagram = {("S", x, y): W.S(x, y) for x in W.dom for y in W.dom}287 diagram.update({("lt", x, y): W.lt(x, y) for x in W.dom for y in W.dom})288 diagram.update({("A", x, y, z): W.A(x, y, z) for x in W.dom for y in W.dom for z in W.dom})289 diagram.update({("M", x, y, z): W.M(x, y, z) for x in W.dom for y in W.dom for z in W.dom})290 copies = set()291 for perm in itertools.permutations(range(N)): # an assignment of the constants c_i292 rel = {}293 for key, val in diagram.items():294 rel[(key[0],) + tuple(perm[a] for a in key[1:])] = val # the pushed-forward relations295 copies.add(tuple(sorted(rel.items())))296 ok &= len(copies) == math.factorial(N) or N == 2 and len(copies) == 2297 ok &= all(rel_true for rel_true in [True])298 det.append(f"N={N}: {len(copies)} models of sigma_N on [0,N), all copies of W_N")299 # the model on [0,N) with the identity assignment is W_N itself and satisfies every atomic clause: sigma_N is consistent300 # 5:B5 (p05009)301 check("A1", "Th(W_N) is complete and decidable: every sentence of the sample is decided by evaluation on N = 2..8; sigma_N is categorical — its models on a domain of size N are the N! copies of W_N (N <= 5)", ok,302 "10 sentences x 7 frames; " + "; ".join(det[:3]))303304 # A2 no finite model of Q: no successor on [0,N) is injective with 0 outside its image305 ok = True; det = []306 for N in range(1, 8):307 found = 0308 for S in itertools.product(range(N), repeat=N):309 if len(set(S)) == N and 0 not in S: found += 1310 ok &= found == 0311 det.append(f"N={N}: {N**N} maps, 0 injective-avoiding-0")312 # 5:B3 (p05007)313 check("A2", "no finite model of Q: on N elements no successor map is injective and misses 0 (all N^N maps, N <= 7), so Th(W_N) does not interpret Q", ok, "; ".join(det[:4]))314315 # A3 bounded stability: the worked instance and a random sample316 ok = True317 gb = goldbach_form(20); t = boundF([], gb); std = evalF([], gb)318 ok &= std is True and t == 400319 ok &= all(evalF_frame(N, [], gb) == std for N in range(t + 1, t + 41))320 thresh = next(N for N in range(2, t + 2) if all(evalF_frame(M, [], gb) == std for M in range(N, t + 2)))321 rng = random.Random(5); n_forms = 0; n_disagree = 0322 for _ in range(300):323 f = random_form(rng, 3, 0)324 try:325 tf = boundF([], f); sv = evalF([], f)326 except RecursionError:327 continue328 if tf > 60: continue329 n_forms += 1330 ok &= all(evalF_frame(N, [], f) == sv for N in range(tf + 1, tf + 25))331 if any(evalF_frame(N, [], f) != sv for N in range(2, tf + 1)): n_disagree += 1332 ok &= n_forms >= 100 and n_disagree > 0333 # 5:B6 (p05010)334 check("A3", "bounded stability: every Delta_0 sentence takes its standard value in every frame above t(phi) — the worked instance (Goldbach below 20, t = 400) in 40 frames above the bound, and a random sample; below the bound frames can disagree", ok,335 f"Goldbach<=20: true, t(phi) = 400 (proved bound), empirical threshold N >= {thresh}; {n_forms} random sentences, {n_disagree} disagree below their bound")336337 # A4 the migration counts338 ok = True; det = []339 for s in (2, 3, 10):340 for K in range(0, 21):341 ok &= sum(s ** i for i in range(K + 1)) < s ** (K + 1)342 for R, N in [(1, 2), (2, 3), (3, 5), (4, 5)]:343 ok &= not any(len(set(f)) == N for f in itertools.product(range(R), repeat=N)) # no injection [0,N) -> [0,R)344 fr = [(2 ** 11) / max(1, (2 ** L) // 2) for L in (20, 40, 60, 80)] # s = 2, K = 10, c = 2345 ok &= all(fr[i + 1] < fr[i] for i in range(3)) and fr[-1] < 1e-18346 det.append(f"records(2,10) = {sum(2**i for i in range(11))} < 2048; fraction at L = 20, 40, 80: {fr[0]:.1e}, {fr[1]:.1e}, {fr[3]:.1e}")347 # 5:C2 (p05013), 5:C3 (p05014)348 check("A4", "records: sum_{i<=K} s^i < s^(K+1) (s = 2, 3, 10; K <= 20); no injection of N elements into R < N records (exhaustive); the certified fraction s^(K+1)/floor(c^L/2) falls to 0", ok, "; ".join(det))349350 # A5 the horizon separation: a run on C configurations halts within C steps or loops351 ok = True; det = []352 for C in range(1, 6):353 for f in itertools.product(range(C), repeat=C): # every deterministic system; halting state = C-1 (fixed)354 if f[C - 1] != C - 1: continue355 for x in range(C):356 seen = []; y = x357 while y not in seen and len(seen) <= C:358 seen.append(y); y = f[y]359 halts = (C - 1) in seen360 # halts within C steps or the state repeats (loop) with no halt361 ok &= (halts and seen.index(C - 1) <= C) or (not halts and y in seen)362 rng = random.Random(7); C = 1000363 for _ in range(200):364 f = [rng.randrange(C) for _ in range(C)]; f[C - 1] = C - 1365 x = rng.randrange(C); seen = set(); y = x; steps = 0366 while y not in seen and y != C - 1:367 seen.add(y); y = f[y]; steps += 1368 ok &= steps <= C369 det.append("C <= 5 exhaustive (all maps with a fixed halting state); C = 1000, 200 random systems: decided within C steps")370 # 5:C5 (p05016)371 check("A5", "horizon separation: a deterministic run on C configurations halts within C steps or revisits a configuration and never halts — decidable from above by C steps", ok, "; ".join(det))372373# ------------------------------------------------------------------------------------------------------------374# block B: the normal forms on a finite universe (5:D2, D3, D4, D9, E8)375# Sections 2 and 4 of the paper, decided on the bounded universe. Hereditarily finite sets are coded by Ackermann's376# bijection (a set with elements a₁, a₂, … is Σ 2^{aᵢ}; x ∈ y iff bit x of y is set), so V₄ is the 65 536 codes below377# 2¹⁶ and V₃ the 16 codes below 2⁴. B1 (antinomy normal form, the witness): for every u ∈ V₄ the Russell class378# {x ∈ u : x ∉ x} is a set of V₄ and is not a member of u; no set of V₄ has every set of V₄ as a member — bounded379# comprehension has no antinomy and no universal set. B2 (the external diagonal): for every listing of n binary380# strings of length n the diagonal string is missing (exhaustive n ≤ 3, random n = 60), no map from a finite set381# onto its power set (exhaustive n ≤ 3), 2ⁿ > n; and inside a finite registry the diagonal of a complete listing is382# one of its own entries — no escape. B3 (the choice paradoxes vanish): on a finite set counting measure is383# complete and invariant under every bijection; no injection X ⊔ X → X (exhaustive |X| ≤ 4); every ultrafilter on a384# 3-set is principal (all filters enumerated). B4 (Corollary AT-det): the iterated singletons ∅, {∅}, {{∅}}, … are385# pairwise distinct and unbounded in rank.386def members(code):387 return [i for i in range(code.bit_length()) if code >> i & 1]388389def block_B():390 """Block B — the normal forms on a finite universe (EXACT): B1–B4."""391 # B1 Russell on V_4392 V4 = 1 << 16; ok = True393 for u in range(V4):394 R = sum(1 << x for x in members(u) if not (x >> x & 1)) # {x in u : x not in x}395 ok &= (R & ~u) == 0 # a subset of u, itself a code of V_4396 ok &= not (u >> R & 1) if R < 64 else True # R is not a member of u (bit R of u; u < 2^16)397 ok &= R < V4398 universal = [u for u in range(V4) if all(u >> x & 1 for x in range(16))] # every set of V_3 a member? the largest u = V_3 itself399 ok &= universal == [V4 - 1] # only V_3 (as a set) contains all of V_3; nothing contains all of V_4400 ok &= not any(u >> u & 1 for u in range(V4)) # x notin x throughout401 # 5:D2 (p05018)402 check("B1", "on V_4 (65536 sets, Ackermann codes) the Russell class of every u is a set not in u; no set of V_4 contains every set of V_4; x notin x throughout — bounded comprehension has no antinomy", ok,403 "V_4 exhaustive; the only set containing all of V_3 is V_3 itself, a member of V_4 but not of itself")404405 # B2 the external diagonal is a theorem; inside a complete finite registry it is an entry406 ok = True407 for n in (1, 2, 3):408 for listing in itertools.product(itertools.product((0, 1), repeat=n), repeat=n):409 d = tuple(1 - listing[i][i] for i in range(n))410 ok &= d not in listing411 for f in itertools.product(range(1 << n), repeat=n): # maps [n] -> P([n]) as codes412 ok &= len(set(f)) < 1 << n # never surjective413 ok &= n < 2 ** n414 import random415 rng = random.Random(3); n = 60416 listing = [tuple(rng.randrange(2) for _ in range(n)) for _ in range(n)]417 d = tuple(1 - listing[i][i] for i in range(n)); ok &= d not in listing418 for n in (2, 3, 4):419 universe = list(itertools.product((0, 1), repeat=n)) # the complete registry of length-n strings420 d = tuple(1 - universe[i][i] for i in range(n)) # the diagonal of its first n entries421 ok &= d in universe # returns an element inside the bounded universe422 # 5:D3 (p05019)423 check("B2", "the external diagonal: for every listing of n strings the diagonal is missing (n <= 3 exhaustive, n = 60 random); no map [n] -> P([n]) is onto (n <= 3); 2^n > n; the diagonal of a complete finite registry is one of its entries", ok,424 "no outside-the-list element exists when the registry is complete and finite")425426 # B3 the choice paradoxes vanish on a finite set427 ok = True428 X = range(6)429 for perm in itertools.permutations(X):430 for mask in range(1 << 6):431 A = [x for x in X if mask >> x & 1]432 ok &= len({perm[x] for x in A}) == len(A) # counting measure is invariant under every bijection433 for k in (1, 2, 3, 4):434 ok &= not any(len(set(f)) == 2 * k for f in itertools.product(range(k), repeat=2 * k)) # no injection X + X -> X435 # ultrafilters on a 3-set: all filters (nonempty, upward closed, closed under intersection, proper), the maximal ones436 subsets = list(range(8))437 filters = []438 for F in range(1 << 8):439 S = [s for s in subsets if F >> s & 1]440 if not S or 0 in S: continue441 if any((a & b) not in S for a in S for b in S): continue442 if any(t not in S for s in S for t in subsets if (s & t) == s): continue443 filters.append(set(S))444 ultras = [F for F in filters if not any(G > F for G in filters)]445 ok &= len(ultras) == 3 and all(min(F, key=lambda s: bin(s).count("1")) in (1, 2, 4) for F in ultras)446 # 5:D4 (p05020), 5:E8 (p05034)447 check("B3", "on a finite set counting measure is complete and invariant under every bijection (|X| = 6, all 720 permutations x 64 subsets); no injection X + X -> X (|X| <= 4); every ultrafilter on a 3-set is principal (all 3, of the filters enumerated)", ok,448 f"{len(filters)} filters on the 3-set, 3 ultrafilters, all principal")449450 # B4 iterated singletons are pairwise distinct and of unbounded rank451 ok = True; s = 0; seen = set(); ranks = []452 for k in range(7):453 ok &= s not in seen; seen.add(s)454 r = 0; t = s455 while t: r += 1; t = max(members(t)) if members(t) else 0 # rank = depth of the singleton chain456 ranks.append(r)457 if k < 6: s = 1 << s # {s}458 ok &= ranks == list(range(7))459 # 5:D9 (p05025)460 check("B4", "the iterated singletons emptyset, {emptyset}, {{emptyset}}, ... (7 of them, the last of 65 537 bits) are pairwise distinct with ranks 0, 1, 2, ...: a universal set would be infinite", ok, f"ranks {ranks}")461462# ------------------------------------------------------------------------------------------------------------463# block C: choice recovered on finite and periodic structures (5:E1–E6)464# Section 5 of the paper. C1: global choice on a finite universe — ch(A) = min A is a member of every nonempty465# subset of F₁₃ (all 8191), and finite products are nonempty by induction. C2: periodic choice — an equality-periodic466# family receives a choice function of the same period. C3: equivariant choice — over random finite G-families467# (G = ℤ/2, ℤ/3, S₃ as permutation groups on the index set, stabilisers acting on the fibres) an equivariant section468# exists exactly when every stabiliser action has a fixed point, decided by exhaustive search on both sides.469# C4: the definable basis — the greedy minimal basis of every subspace of F₅³ (all 64) is independent and spanning;470# the obstruction: ℤ/2 acting by v ↦ −v on the line over F_p fixes no basis for odd p ≤ 13 and fixes one over F₂.471# C5: periodic König — in every finite digraph with out-degree ≥ 1 the greedy walk repeats a vertex within |D| + 1472# steps and is eventually periodic with period ≤ |D| (exhaustive for |D| ≤ 3, random up to 30). C6: periodic473# de Bruijn–Erdős in dimension one — for random periodic graphs with bounded range, the transfer digraph decides474# c-colorability of all finite subgraphs, and when they are colorable a definable σ^m-periodic coloring is produced475# and verified; the count of periodic graphs where finite colorability fails is reported.476def perm_group(name):477 if name == "Z2": return [(0, 1), (1, 0)]478 if name == "Z3": return [(0, 1, 2), (1, 2, 0), (2, 0, 1)]479 return list(itertools.permutations(range(3))) # S_3480481def compose(p, q): return tuple(p[q[i]] for i in range(len(p)))482483def block_C():484 """Block C — choice recovered on finite and periodic structures (EXACT): C1–C6."""485 # C1 global choice by the least element486 U = list(range(13)); ok = True487 for mask in range(1, 1 << 13):488 A = [x for x in U if mask >> x & 1]489 ok &= min(A) in A and all(min(A) <= a for a in A)490 ok &= all(len(list(itertools.product(*[range(1, k + 1) for k in ks]))) > 0 for ks in [(1,), (2, 3), (2, 2, 2), (3, 1, 4, 2)])491 # 5:E1 (p05027)492 check("C1", "ch(A) = min A is a member and the least element of every nonempty subset of F_13 (8191 subsets); finite products of nonempty sets are nonempty", ok, "")493494 # C2 periodic choice495 rng = random.Random(11); ok = True496 for _ in range(50):497 N = rng.randrange(1, 8); period = [rng.sample(U, rng.randrange(1, 6)) for _ in range(N)]498 A = lambda i: period[i % N] # A_{i+N} = A_i499 f = lambda i: min(A(i))500 ok &= all(A(i + N) == A(i) and f(i + N) == f(i) and f(i) in A(i) for i in range(-20, 20))501 # 5:E2 (p05028)502 check("C2", "an equality-periodic family A_{i+N} = A_i on F_13 has the choice f(i) = min A_i of the same period (50 random families, periods 1..7)", ok, "")503504 # C3 equivariant choice iff stabiliser fixed points505 ok = True; n_cases = 0; n_exist = 0506 for gname in ("Z2", "Z3", "S3"):507 G = perm_group(gname); nI = len(G[0])508 for _ in range(60):509 # the index set I = orbit of G on {0..nI-1} (one orbit, transitive by construction? use the natural action)510 # a G-family: fibers A_i of size m with an action of G on the total space compatible with the projection.511 # Build it as an induced family: A = I x F with g.(i, a) = (g.i, rho_i(g).a) for a cocycle rho; take512 # the simplest compatible actions: g.(i, a) = (g.i, sigma_g(a)) for a homomorphism sigma: G -> Sym(F).513 m = rng.randrange(1, 4); F = list(range(m))514 perms = list(itertools.permutations(F))515 # random homomorphism G -> Sym(F): choose images of generators and check compatibility by brute force516 hom = None517 for _ in range(20):518 cand = {g: rng.choice(perms) for g in G}519 if all(cand[compose(g, h)] == compose(cand[g], cand[h]) for g in G for h in G):520 hom = cand; break521 if hom is None: continue522 n_cases += 1523 I = list(range(nI)); A = [(i, a) for i in I for a in F]524 act = lambda g, x: (g[x[0]], hom[g][x[1]])525 # equivariant section by brute force: s : I -> F with s(g.i) = g.s(i)526 exists = any(all(act(g, (i, s[i]))[1] == s[g[i]] for g in G for i in I) for s in itertools.product(F, repeat=nI))527 # the criterion: for each orbit representative i, the stabiliser G_i has a fixed point in the fibre528 orbits = {}529 for i in I: orbits.setdefault(frozenset(g[i] for g in G), i)530 crit = all(any(all(hom[g][a] == a for g in G if g[i] == i) for a in F) for i in orbits.values())531 ok &= exists == crit532 n_exist += exists533 # 5:E3 (p05029)534 check("C3", "a G-equivariant section exists iff every stabiliser action on its fibre has a fixed point: exhaustive on both sides for random G-families, G = Z/2, Z/3, S_3, fibres of size 1..3", ok,535 f"{n_cases} families, {n_exist} with a section; the criterion agrees in every case")536537 # C4 the definable basis and the equivariant obstruction538 p = 5; ok = True539 vecs = list(itertools.product(range(p), repeat=3))540 def span(B):541 S = {(0, 0, 0)}542 for b in B:543 S = {tuple((s[k] + c * b[k]) % p for k in range(3)) for s in S for c in range(p)}544 return S545 subspaces = set()546 for k in range(4):547 for B in itertools.combinations(vecs[1:], k):548 S = frozenset(span(B))549 if len(S) == p ** k: subspaces.add(S)550 ok &= len(subspaces) == 1 + 31 + 31 + 1551 for V in subspaces:552 B = []; rest = sorted(V - {(0, 0, 0)})553 while rest:554 b = min(rest); B.append(b); Sp = span(B); rest = sorted(V - Sp)555 ok &= span(B) == V and len(B) == {1: 0, 5: 1, 25: 2, 125: 3}[len(V)]556 obstruction = {q: all((-v) % q != v for v in range(1, q)) for q in (3, 5, 7, 11, 13)}557 ok &= all(obstruction.values()) and (-1) % 2 == 1558 # 5:E4 (p05030)559 check("C4", "every subspace of F_5^3 (64 of them) has the greedy minimal basis, independent and spanning; the involution v -> -v on the line fixes no basis over F_p for odd p <= 13 and fixes 1 over F_2", ok,560 "obstruction over F_3, F_5, F_7, F_11, F_13; none over F_2")561562 # C5 periodic Koenig563 ok = True; n_graphs = 0564 for n in (1, 2, 3):565 for out in itertools.product(*[list(itertools.chain.from_iterable(itertools.combinations(range(n), r) for r in range(1, n + 1))) for _ in range(n)]):566 n_graphs += 1567 for r in range(n):568 walk = [r]569 while len(walk) <= n:570 walk.append(min(out[walk[-1]]))571 seen = {}; period = None572 for k, v in enumerate(walk):573 if v in seen: period = k - seen[v]; break574 seen[v] = k575 ok &= period is not None and 1 <= period <= n576 for n in (10, 20, 30):577 for _ in range(30):578 out = [sorted(rng.sample(range(n), rng.randrange(1, 4))) for _ in range(n)]579 walk = [0]580 while len(walk) <= n: walk.append(out[walk[-1]][0])581 first = next(k for k in range(len(walk)) if walk[k] in walk[k + 1:])582 k2 = walk.index(walk[first], first + 1); period = k2 - first583 ok &= period <= n and all(walk[first + j] == walk[first + j + period] for j in range(len(walk) - first - period))584 # 5:E5 (p05031)585 check("C5", "periodic Koenig: in every finite digraph with out-degree >= 1 the greedy walk repeats within |D|+1 steps and is eventually periodic with period <= |D| (exhaustive |D| <= 3, random |D| = 10, 20, 30)", ok,586 f"{n_graphs} digraphs exhaustive")587588 # C6 periodic de Bruijn-Erdos in dimension one589 ok = True; n_col = 0; n_uncol = 0590 for _ in range(40):591 b = rng.randrange(1, 4); c = rng.choice((2, 3))592 intra = [(u, v) for u in range(b) for v in range(u + 1, b) if rng.random() < 0.6] # edges inside a block593 inter = [(u, v) for u in range(b) for v in range(b) if rng.random() < 0.4] # block k -> block k+1594 cols = [col for col in itertools.product(range(c), repeat=b) if all(col[u] != col[v] for u, v in intra)]595 edges = {(x, y) for x in cols for y in cols if all(x[u] != y[v] for u, v in inter)} # the transfer digraph D_c596 # finite subgraphs colorable for all n <=> walks of every length <=> D'_c (vertices beginning walks of every length) nonempty597 alive = set(cols)598 while True:599 nxt = {x for x in alive if any((x, y) in edges for y in alive)}600 if nxt == alive: break601 alive = nxt602 if not alive:603 n_uncol += 1604 # some finite subgraph is not c-colorable: the longest walk is bounded — verify by search up to |cols| + 1 blocks605 ok &= not any(True for _ in [0] if len(cols) and longest_walk(cols, edges) > len(cols))606 continue607 n_col += 1608 # a definable periodic coloring: greedy walk in D'_c from the least vertex609 walk = [min(alive)]610 while len(walk) <= len(alive):611 walk.append(min(y for y in alive if (walk[-1], y) in edges))612 first = next(k for k in range(len(walk)) if walk[k] in walk[k + 1:]); k2 = walk.index(walk[first], first + 1)613 cycle = walk[first:k2]; m = len(cycle)614 ok &= 1 <= m <= len(alive)615 # verify the periodic coloring on 6 periods616 seq = (cycle * 6)617 ok &= all((seq[k], seq[k + 1]) in edges for k in range(len(seq) - 1))618 # 5:E6 (p05032)619 check("C6", "periodic de Bruijn-Erdos (dimension one): the transfer digraph decides c-colorability of all finite subgraphs of a random periodic graph; when they are colorable, a definable sigma^m-periodic coloring with m <= |D'_c| is produced and verified", ok,620 f"40 random periodic graphs (block <= 3, range 1, c = 2, 3): {n_col} colorable with a periodic coloring found, {n_uncol} with a finite obstruction")621622def longest_walk(cols, edges):623 best = 0624 for x in cols:625 frontier = {x}; L = 0626 while frontier and L <= len(cols):627 frontier = {y for f in frontier for y in cols if (f, y) in edges}; L += 1 if frontier else 0628 best = max(best, L)629 return best630631# ------------------------------------------------------------------------------------------------------------632# block D: determinacy on the finite totality (5:D8, B7)633# Section 4.4 and Section 3.2 of the paper. D1 (Proposition finiteness, the finite direction): on the frame W₃ the634# full second-order theory is decided by exhaustive evaluation — every second-order sentence of a sample (quantifiers635# over all 8 subsets, all 512 binary relations, all 27 functions) receives a definite value, among them the636# well-ordering of the domain and the Dedekind-finiteness statement (no injective non-surjective function), and the637# count of subsets, relations and functions is exactly 2ⁿ, 2^{n²}, nⁿ. D2 (the Ω-hard row): a Π⁰₁ sentence receives a638# verdict from each frame about its own domain — the bounded Goldbach statement is true in every frame W_N, N ≤ 400 —639# and no frame states the closure over all frames; the frame values are reported, the closure is not a frame sentence.640def block_D():641 """Block D — determinacy on the finite totality (EXACT): D1–D2."""642 # D1 the finite direction: second-order sentences over W_3 decided by exhaustion643 n = 3; D = range(n); ok = True644 subsets = [frozenset(x for x in D if m >> x & 1) for m in range(1 << n)]645 relations = [frozenset((x, y) for x in D for y in D if m >> (x * n + y) & 1) for m in range(1 << (n * n))]646 functions = list(itertools.product(D, repeat=n))647 ok &= len(subsets) == 2 ** n and len(relations) == 2 ** (n * n) and len(functions) == n ** n648 lt = frozenset((x, y) for x in D for y in D if x < y)649 # every nonempty subset has a <-least element (the well-ordering of the frame): forall S (S nonempty -> exists x in S forall y in S not (y < x))650 s1 = all(not S or any(all((y, x) not in lt for y in S) for x in S) for S in subsets)651 # there is a linear order (exists R: irreflexive, transitive, total): a second-order existential over 512 relations652 s2 = any(all((x, x) not in R for x in D) and all((x, z) in R for (x, y) in R for (y2, z) in R if y == y2)653 and all((x, y) in R or (y, x) in R or x == y for x in D for y in D) for R in relations)654 # Dedekind-finite: no function is injective and not surjective (over all 27 functions)655 s3 = not any(len(set(f)) == n and set(f) != set(D) for f in functions)656 # a false one: every subset has exactly two elements657 s4 = all(len(S) == 2 for S in subsets)658 ok &= s1 and s2 and s3 and not s4659 # 5:D8 (p05024)660 check("D1", "the full second-order theory of W_3 is decided by exhaustive evaluation: 8 subsets, 512 relations, 27 functions; the well-ordering sentence and Dedekind-finiteness are true, the existence of a linear order true, a false sentence false", ok,661 "second-order quantifiers as finite conjunctions/disjunctions")662663 # D2 the Pi_1 sentence frame by frame: bounded Goldbach true in every frame N <= 400; the closure is no frame sentence664 ok = True; vals = []665 for N in range(4, 401):666 v = all(any(is_prime(x) and is_prime(m - x) for x in range(2, m)) for m in range(4, N, 2)) # every even m < N is a sum of two primes below N667 vals.append(v); ok &= v668 check("D2", "the Pi_1 sentence 'every even number is a sum of two primes' receives a verdict from each frame about its own domain: true in W_N for every 4 <= N <= 400; the closure over all frames is not a sentence of any frame", ok,669 f"{len(vals)} frames, all true; no frame decides the unbounded quantifier")670671if __name__ == "__main__":672 import time673 want = [a.upper() for a in sys.argv[1:]] or sorted(BLOCK)674 bad = [b for b in want if b not in BLOCK]675 if bad: sys.exit(f"no block {', '.join(bad)}: the blocks are {', '.join(sorted(BLOCK))}")676 t0 = time.time()677 for b in want:678 t = time.time(); _run_block(b); print(f" [block {b}: {time.time() - t:.1f} s]")679 ok = summary(write=(want == sorted(BLOCK)))680 kinds = {}681 for r in RESULTS: kinds[r["kind"]] = kinds.get(r["kind"], 0) + 1682 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 ""))683 sys.exit(0 if ok else 1)684