The ledger file frc/ledgers/p05_reductio.py of Paradoxes of Infinity as Reductio ad Absurdum, rendered with an anchor per line: the marked lines (# 5:C2 (p5010): a predicate and its accession key) are the checks that decide the predicates of the paper's predicate ledger — 17 of 17 checks passing; the predicates' theorems are the declarations of Reductio in the core. ▶ run the predicates on Google Colab.
1"""p05_reductio — the ledger file of 5-reductio (the 5-reductio migration, 21 October 2026).23"Paradoxes of Infinity as Reductio ad Absurdum" (Akhtman, preprint 2025; Preprints doi 10.20944/preprints202508.1744.v1).4The paper's predicate ledger is docs/5-reductio/5-reductio-ledger.json. This file binds its python-witnessed predicates5to the framework: the table of keys (generated from the ledger by ci/make_ledgers.py) and the checks of four blocks,6seventeen in all, every one EXACT. The checks call the logic theme: frc/logic.py holds the arithmetic frame W_N and the7Δ₀ constructors, frc/formation.py the Δ₀ evaluators over ℕ and in a frame with the bound t(φ) (the core's evalT, evalF,8evalF?, boundF), frc/sets.py the hereditarily finite sets by Ackermann's coding, the Russell class, the iterated9singletons, counting measure, the small permutation groups and the transfer digraph's walks. Each check names the10predicate(s) it witnesses (LEDGER) and carries a `# 5:XN (<key>)` marker when it decides one (PREDICATES). The11consequence row D5 (the reductio principle) is named on the checks of the witnesses it rests on: A1 (Th(W_N), 5:B5),12B1 (bounded comprehension, 5:D2) and B3 (counting measure, 5:E8).1314The paper's validation package src/5-reductio (one script, reductio.py) stays the published witness until the paper's15release pins the framework; the blocks here are its blocks, check for check, with the shared machinery moved to the16themes. Two changes of the arithmetic: the certified fraction of A4 is computed as an exact rational and tested in the17finite form of 5:C3 (below 1/N as soon as 2 s^(K+1) N ≤ c^L), and the random samples of A3 and C6 draw their coins by18randrange, so no float enters (gate G09); the samples are fixed by their seeds. Where a check works on a sample, its19label says so.2021The Lean side, under the rule of this paper that every T row has a core proof: the theme files lean/FrcCore/Theme/Logic.lean22(the finite theories, no finite Q, the records count, the pigeonhole, the least element, the iteration lemmas),23Theme/SecondOrder.lean (the full second-order theory of a finite structure), Theme/Reach.lean (the vanishing certified24fraction in finite form), Theme/Sets.lean (the antinomy as a theorem of separation, hereditarily finite sets as trees,25the iterated singletons, counting measure, no doubling, principal ultrafilters), Theme/Equivariant.lean (the equivariant26section criterion) and Theme/Transfer.lean (the transfer digraph's periodic walk); on Mathlib lean/FrcMathlib/Theme/Logic.lean27and the paper module FrcMathlib/Reductio.lean; the keys in Keys/Logic.lean of both libraries, the certificates28Ledgers/P05Reductio.lean. The rows B2, D4 and D7 of the paper carry no Lean theorem (Rosser's theorem, Vitali and29Banach–Tarski, the forced exit under Det) and are retagged I in the ledger of 21 October 2026; the check B3 stays as30D4's corroboration.3132No numeral above Ω ∼ 10¹²³ is formed.3334 python3 -m frc.ledgers.p05_reductio every block, the census; exit 1 if a check fails (≈ 10 s)35 python3 -m frc.ledgers.p05_reductio B one block (A to D)36 from frc.ledgers.p05_reductio import R; R.predicate("5:D2") one predicate: its blocks run once per session3738Blocks: A the arithmetic frames, their theories, the stability schema, the migration (5:B3, B5, B6, C2, C3, C5, D5)39 B the normal forms on a finite universe (5:D2, D3, D4, D9, E8, D5)40 C choice recovered on finite and periodic structures (5:E1–E6)41 D determinacy on the finite totality (5:D8; D2 corroborates B7)4243Checks: 17, all EXACT. The notebook frc/ledgers/p05_reductio.ipynb runs one predicate per cell, the cell's id its key (gate G13).44"""45import sys, itertools, random, math46from fractions import Fraction4748from frc.registry import Registry49from frc.arith import is_prime50from frc.logic import Frame, num, bex, disj, impl, prime_form, goldbach_form, random_form51from frc.formation import d0_eval as evalF, d0_eval_frame as evalF_frame, d0_bound as boundF52from frc.sets import hf_levels, members, perm_group, compose, longest_walk5354# ---- generated by ci/make_ledgers.py from docs/5-reductio/5-reductio-ledger.json; edit the ledger, not this table ----55PAPER = "5-reductio"56KEYS = {"A1": "p05001", "A2": "p05002", "A3": "p05003", "A4": "p05004", "B1": "p05005", "B2": "p05006", "B3": "p05007", "B4": "p05008", "B5": "p05009", "B6": "p05010", "B7": "p05011", "C1": "p05012", "C2": "p05013", "C3": "p05014", "C4": "p05015", "C5": "p05016", "D1": "p05017", "D2": "p05018", "D3": "p05019", "D4": "p05020", "D5": "p05021", "D6": "p05022", "D7": "p05023", "D8": "p05024", "D9": "p05025", "D10": "p05026", "E1": "p05027", "E2": "p05028", "E3": "p05029", "E4": "p05030", "E5": "p05031", "E6": "p05032", "E7": "p05033", "E8": "p05034", "F1": "p05035", "F2": "p05036", "F3": "p05037", "T1": "p05041"} # every row of the ledger: its label and its accession key57LEAN = {"B3": "core, ml", "B5": "core, ml", "B6": "core", "C2": "core, ml", "C3": "core", "C5": "core", "D2": "core", "D3": "core, ml", "D5": "core", "D8": "core, ml", "D9": "core", "E1": "core, ml", "E2": "core, ml", "E3": "core, ml", "E4": "core, ml", "E5": "core", "E6": "core", "E8": "core, ml"} # the rows with a Lean declaration: the libraries whose key files prove them58# ---- end of the generated table ----5960LEAN_ONLY = () # the predicates with a Lean declaration and no python check (gate G12): none6162# The paper's predicate ledger (Appendix B; predicates cited as 5:XN): the predicate(s) each check witnesses. The consequence63# row D5 is named on the checks of the witnesses it rests on (the blueprint of 21 October 2026, finding 1).64LEDGER = {65 "A1": "5:B5, 5:D5", "A2": "5:B3", "A3": "5:B6", "A4": "5:C2, 5:C3", "A5": "5:C5",66 "B1": "5:D2, 5:D5", "B2": "5:D3", "B3": "5:D4, 5:E8, 5:D5", "B4": "5:D9",67 "C1": "5:E1", "C2": "5:E2", "C3": "5:E3", "C4": "5:E4", "C5": "5:E5", "C6": "5:E6",68 "D1": "5:D8", "D2": "5:B7",69}7071# the package record (reductio.<id>) each check reproduces: the ids are the package's72FAMILY = {pid: f"reductio.{pid}" for pid in LEDGER}7374BLOCK = {"A": "the arithmetic frames, their theories, the stability schema, the migration",75 "B": "the normal forms on a finite universe",76 "C": "choice recovered on finite and periodic structures",77 "D": "determinacy on the finite totality"}7879# the deciding check of each witnessed predicate (the other checks that touch it are corroboration)80PREDICATES = {81 "5:B3": "A2", "5:B5": "A1", "5:B6": "A3", "5:C2": "A4", "5:C3": "A4", "5:C5": "A5",82 "5:D2": "B1", "5:D3": "B2", "5:D4": "B3", "5:D5": "B1", "5:D8": "D1", "5:D9": "B4",83 "5:E1": "C1", "5:E2": "C2", "5:E3": "C3", "5:E4": "C4", "5:E5": "C5", "5:E6": "C6", "5:E8": "B3",84 "5:B7": "D2",85}8687R = Registry("5", "reductio", LEDGER, PREDICATES, sources=[__file__])8889# ------------------------------------------------------------------------------------------------------------90# block A: the arithmetic frames, their theories, the stability schema, the migration (5:B3, B5, B6, C2, C3, C5)91# Section 3 of the paper. A1: the theory of the frame W_N is complete and decidable — every sentence of a sample92# (and every sentence of the language, by the evaluator) is decided by evaluation in W_N, and the categorical93# sentence σ_N has exactly the N! relabelled copies of W_N as its models on a domain of size N (categoricity).94# A2: no finite model of Q — on a domain of N elements no successor map is injective and misses 0 (exhaustive over95# all N^N maps for N ≤ 7); so the frame theory does not interpret Q. A3: bounded stability — the worked instance96# (Goldbach below 20) takes its standard value in every frame above its bound t(φ), and so does every formula of a97# random sample of Δ₀ sentences; below the bound frames can disagree, and the empirical threshold is reported98# beside the proved one. A4: the migration counts — fewer than s^(K+1) records of length ≤ K, no injection of a99# domain of N elements into fewer than N records, and the certified fraction s^(K+1)/⌊c^L/2⌋ falling below every100# threshold (chart). A5: the horizon separation — a deterministic system on C configurations halts within C steps101# or revisits a configuration and runs forever; exhaustive on tiny systems, sampled on large ones.102def fo_sentences():103 """A sample of first-order sentences over the frame signature, as closures W ↦ truth value (nested quantifiers104 evaluated by finite search). Each returns a definite Boolean on every frame."""105 D = lambda W: W.dom106 return [107 ("0 is least: ∀x ¬(x < 0)", lambda W: all(not W.lt(x, 0) for x in D(W))),108 ("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)),109 ("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))),110 ("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))),111 ("multiplication by 0: ∀x M(x,0,0)", lambda W: all(W.M(x, 0, 0) for x in D(W))),112 ("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))),113 ("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))),114 ("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))),115 ("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))),116 ("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))),117 ]118119@R.block("A", BLOCK["A"])120def block_A():121 """Block A — the arithmetic frames, their theories, the stability schema, the migration (EXACT): A1–A5."""122 # A1 per-frame completeness and decidability; categoricity of sigma_N123 ok = True; det = []124 sents = fo_sentences()125 for N in range(2, 9):126 W = Frame(N)127 vals = [s(W) for _, s in sents]128 ok &= all(v in (True, False) for v in vals) # every sentence decided by evaluation129 # categoricity: models of sigma_N on domain [0,N) are the N! relabelled copies of W_N, each satisfying the diagram130 for N in (2, 3, 4, 5):131 W = Frame(N)132 diagram = {("S", x, y): W.S(x, y) for x in W.dom for y in W.dom}133 diagram.update({("lt", x, y): W.lt(x, y) for x in W.dom for y in W.dom})134 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})135 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})136 copies = set()137 for perm in itertools.permutations(range(N)): # an assignment of the constants c_i138 rel = {}139 for key, val in diagram.items():140 rel[(key[0],) + tuple(perm[a] for a in key[1:])] = val # the pushed-forward relations141 copies.add(tuple(sorted(rel.items())))142 ok &= len(copies) == math.factorial(N) or N == 2 and len(copies) == 2143 ok &= all(rel_true for rel_true in [True])144 det.append(f"N={N}: {len(copies)} models of sigma_N on [0,N), all copies of W_N")145 # the model on [0,N) with the identity assignment is W_N itself and satisfies every atomic clause: sigma_N is consistent146 # 5:B5 (p05009), 5:D5 (p05021)147 R.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,148 "10 sentences x 7 frames; " + "; ".join(det[:3]))149150 # A2 no finite model of Q: no successor on [0,N) is injective with 0 outside its image151 ok = True; det = []152 for N in range(1, 8):153 found = 0154 for S in itertools.product(range(N), repeat=N):155 if len(set(S)) == N and 0 not in S: found += 1156 ok &= found == 0157 det.append(f"N={N}: {N**N} maps, 0 injective-avoiding-0")158 # 5:B3 (p05007)159 R.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]))160161 # A3 bounded stability: the worked instance and a random sample162 ok = True163 gb = goldbach_form(20); t = boundF([], gb); std = evalF([], gb)164 ok &= std is True and t == 400165 ok &= all(evalF_frame(N, [], gb) == std for N in range(t + 1, t + 41))166 thresh = next(N for N in range(2, t + 2) if all(evalF_frame(M, [], gb) == std for M in range(N, t + 2)))167 rng = random.Random(5); n_forms = 0; n_disagree = 0168 for _ in range(300):169 f = random_form(rng, 3, 0)170 try:171 tf = boundF([], f); sv = evalF([], f)172 except RecursionError:173 continue174 if tf > 60: continue175 n_forms += 1176 ok &= all(evalF_frame(N, [], f) == sv for N in range(tf + 1, tf + 25))177 if any(evalF_frame(N, [], f) != sv for N in range(2, tf + 1)): n_disagree += 1178 ok &= n_forms >= 100 and n_disagree > 0179 # 5:B6 (p05010)180 R.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,181 f"Goldbach<=20: true, t(phi) = 400 (proved bound), empirical threshold N >= {thresh}; {n_forms} random sentences, {n_disagree} disagree below their bound")182183 # A4 the migration counts184 ok = True; det = []185 for s in (2, 3, 10):186 for K in range(0, 21):187 ok &= sum(s ** i for i in range(K + 1)) < s ** (K + 1)188 for Rr, N in [(1, 2), (2, 3), (3, 5), (4, 5)]:189 ok &= not any(len(set(f)) == N for f in itertools.product(range(Rr), repeat=N)) # no injection [0,N) -> [0,R)190 recs = sum(2 ** i for i in range(11)) # s = 2, K = 10: the records191 fr = [Fraction(recs, max(1, (2 ** L) // 2)) for L in (20, 40, 60, 80)] # the certified fraction, exact, c = 2192 ok &= all(fr[i + 1] < fr[i] for i in range(3)) and fr[-1] < Fraction(1, 10 ** 18)193 for N in (10, 10 ** 3, 10 ** 6, 10 ** 12): # the finite form of 5:C3: below 1/N as soon as 2 s^(K+1) N <= c^L194 Lmin = next(Lx for Lx in range(1, 200) if 2 * 2 ** 11 * N <= 2 ** Lx)195 ok &= recs * N < 2 ** Lmin // 2 and all(recs * N < 2 ** Lx // 2 for Lx in range(Lmin, Lmin + 20))196 ok &= not recs * N < 2 ** (Lmin - 1) // 2 or 2 * 2 ** 11 * N <= 2 ** (Lmin - 1)197 det.append(f"records(2,10) = {recs} < 2048; fraction at L = 20, 40, 80: {fr[0]}, {fr[1]}, {fr[3]}; below 1/N from L = {next(Lx for Lx in range(1, 200) if 2 * 2 ** 11 * 10 ** 6 <= 2 ** Lx)} on at N = 10^6")198 # 5:C2 (p05013), 5:C3 (p05014)199 R.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) is below 1/N as soon as 2 s^(K+1) N <= c^L (N = 10, 10^3, 10^6, 10^12 at s = 2, K = 10, c = 2)", ok, "; ".join(det))200201 # A5 the horizon separation: a run on C configurations halts within C steps or loops202 ok = True; det = []203 for C in range(1, 6):204 for f in itertools.product(range(C), repeat=C): # every deterministic system; halting state = C-1 (fixed)205 if f[C - 1] != C - 1: continue206 for x in range(C):207 seen = []; y = x208 while y not in seen and len(seen) <= C:209 seen.append(y); y = f[y]210 halts = (C - 1) in seen211 # halts within C steps or the state repeats (loop) with no halt212 ok &= (halts and seen.index(C - 1) <= C) or (not halts and y in seen)213 rng = random.Random(7); C = 1000214 for _ in range(200):215 f = [rng.randrange(C) for _ in range(C)]; f[C - 1] = C - 1216 x = rng.randrange(C); seen = set(); y = x; steps = 0217 while y not in seen and y != C - 1:218 seen.add(y); y = f[y]; steps += 1219 ok &= steps <= C220 det.append("C <= 5 exhaustive (all maps with a fixed halting state); C = 1000, 200 random systems: decided within C steps")221 # 5:C5 (p05016)222 R.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))223224225# ------------------------------------------------------------------------------------------------------------226# block B: the normal forms on a finite universe (5:D2, D3, D4, D9, E8)227# Sections 2 and 4 of the paper, decided on the bounded universe. Hereditarily finite sets are coded by Ackermann's228# 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 below229# 2¹⁶ and V₃ the 16 codes below 2⁴. B1 (antinomy normal form, the witness): for every u ∈ V₄ the Russell class230# {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 — bounded231# comprehension has no antinomy and no universal set. B2 (the external diagonal): for every listing of n binary232# strings of length n the diagonal string is missing (exhaustive n ≤ 3, random n = 60), no map from a finite set233# onto its power set (exhaustive n ≤ 3), 2ⁿ > n; and inside a finite registry the diagonal of a complete listing is234# one of its own entries — no escape. B3 (the choice paradoxes vanish): on a finite set counting measure is235# complete and invariant under every bijection; no injection X ⊔ X → X (exhaustive |X| ≤ 4); every ultrafilter on a236# 3-set is principal (all filters enumerated). B4 (Corollary AT-det): the iterated singletons ∅, {∅}, {{∅}}, … are237# pairwise distinct and unbounded in rank.238@R.block("B", BLOCK["B"])239def block_B():240 """Block B — the normal forms on a finite universe (EXACT): B1–B4."""241 # B1 Russell on V_4242 V4 = 1 << 16; ok = True243 for u in range(V4):244 Rs = sum(1 << x for x in members(u) if not (x >> x & 1)) # {x in u : x not in x}245 ok &= (Rs & ~u) == 0 # a subset of u, itself a code of V_4246 ok &= not (u >> Rs & 1) if Rs < 64 else True # R is not a member of u (bit R of u; u < 2^16)247 ok &= Rs < V4248 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 itself249 ok &= universal == [V4 - 1] # only V_3 (as a set) contains all of V_3; nothing contains all of V_4250 ok &= not any(u >> u & 1 for u in range(V4)) # x notin x throughout251 # 5:D2 (p05018), 5:D5 (p05021)252 R.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,253 "V_4 exhaustive; the only set containing all of V_3 is V_3 itself, a member of V_4 but not of itself")254255 # B2 the external diagonal is a theorem; inside a complete finite registry it is an entry256 ok = True257 for n in (1, 2, 3):258 for listing in itertools.product(itertools.product((0, 1), repeat=n), repeat=n):259 d = tuple(1 - listing[i][i] for i in range(n))260 ok &= d not in listing261 for f in itertools.product(range(1 << n), repeat=n): # maps [n] -> P([n]) as codes262 ok &= len(set(f)) < 1 << n # never surjective263 ok &= n < 2 ** n264 import random265 rng = random.Random(3); n = 60266 listing = [tuple(rng.randrange(2) for _ in range(n)) for _ in range(n)]267 d = tuple(1 - listing[i][i] for i in range(n)); ok &= d not in listing268 for n in (2, 3, 4):269 universe = list(itertools.product((0, 1), repeat=n)) # the complete registry of length-n strings270 d = tuple(1 - universe[i][i] for i in range(n)) # the diagonal of its first n entries271 ok &= d in universe # returns an element inside the bounded universe272 # 5:D3 (p05019)273 R.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,274 "no outside-the-list element exists when the registry is complete and finite")275276 # B3 the choice paradoxes vanish on a finite set277 ok = True278 X = range(6)279 for perm in itertools.permutations(X):280 for mask in range(1 << 6):281 A = [x for x in X if mask >> x & 1]282 ok &= len({perm[x] for x in A}) == len(A) # counting measure is invariant under every bijection283 for k in (1, 2, 3, 4):284 ok &= not any(len(set(f)) == 2 * k for f in itertools.product(range(k), repeat=2 * k)) # no injection X + X -> X285 # ultrafilters on a 3-set: all filters (nonempty, upward closed, closed under intersection, proper), the maximal ones286 subsets = list(range(8))287 filters = []288 for F in range(1 << 8):289 S = [s for s in subsets if F >> s & 1]290 if not S or 0 in S: continue291 if any((a & b) not in S for a in S for b in S): continue292 if any(t not in S for s in S for t in subsets if (s & t) == s): continue293 filters.append(set(S))294 ultras = [F for F in filters if not any(G > F for G in filters)]295 ok &= len(ultras) == 3 and all(min(F, key=lambda s: bin(s).count("1")) in (1, 2, 4) for F in ultras)296 # 5:D4 (p05020), 5:E8 (p05034), 5:D5 (p05021)297 R.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,298 f"{len(filters)} filters on the 3-set, 3 ultrafilters, all principal")299300 # B4 iterated singletons are pairwise distinct and of unbounded rank301 ok = True; s = 0; seen = set(); ranks = []302 for k in range(7):303 ok &= s not in seen; seen.add(s)304 r = 0; t = s305 while t: r += 1; t = max(members(t)) if members(t) else 0 # rank = depth of the singleton chain306 ranks.append(r)307 if k < 6: s = 1 << s # {s}308 ok &= ranks == list(range(7))309 # 5:D9 (p05025)310 R.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}")311312313# ------------------------------------------------------------------------------------------------------------314# block C: choice recovered on finite and periodic structures (5:E1–E6)315# Section 5 of the paper. C1: global choice on a finite universe — ch(A) = min A is a member of every nonempty316# subset of F₁₃ (all 8191), and finite products are nonempty by induction. C2: periodic choice — an equality-periodic317# family receives a choice function of the same period. C3: equivariant choice — over random finite G-families318# (G = ℤ/2, ℤ/3, S₃ as permutation groups on the index set, stabilisers acting on the fibres) an equivariant section319# exists exactly when every stabiliser action has a fixed point, decided by exhaustive search on both sides.320# C4: the definable basis — the greedy minimal basis of every subspace of F₅³ (all 64) is independent and spanning;321# 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₂.322# C5: periodic König — in every finite digraph with out-degree ≥ 1 the greedy walk repeats a vertex within |D| + 1323# steps and is eventually periodic with period ≤ |D| (exhaustive for |D| ≤ 3, random up to 30). C6: periodic324# de Bruijn–Erdős in dimension one — for random periodic graphs with bounded range, the transfer digraph decides325# c-colorability of all finite subgraphs, and when they are colorable a definable σ^m-periodic coloring is produced326# and verified; the count of periodic graphs where finite colorability fails is reported.327@R.block("C", BLOCK["C"])328def block_C():329 """Block C — choice recovered on finite and periodic structures (EXACT): C1–C6."""330 # C1 global choice by the least element331 U = list(range(13)); ok = True332 for mask in range(1, 1 << 13):333 A = [x for x in U if mask >> x & 1]334 ok &= min(A) in A and all(min(A) <= a for a in A)335 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)])336 # 5:E1 (p05027)337 R.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, "")338339 # C2 periodic choice340 rng = random.Random(11); ok = True341 for _ in range(50):342 N = rng.randrange(1, 8); period = [rng.sample(U, rng.randrange(1, 6)) for _ in range(N)]343 A = lambda i: period[i % N] # A_{i+N} = A_i344 f = lambda i: min(A(i))345 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))346 # 5:E2 (p05028)347 R.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, "")348349 # C3 equivariant choice iff stabiliser fixed points350 ok = True; n_cases = 0; n_exist = 0351 for gname in ("Z2", "Z3", "S3"):352 G = perm_group(gname); nI = len(G[0])353 for _ in range(60):354 # the index set I = orbit of G on {0..nI-1} (one orbit, transitive by construction? use the natural action)355 # a G-family: fibers A_i of size m with an action of G on the total space compatible with the projection.356 # Build it as an induced family: A = I x F with g.(i, a) = (g.i, rho_i(g).a) for a cocycle rho; take357 # the simplest compatible actions: g.(i, a) = (g.i, sigma_g(a)) for a homomorphism sigma: G -> Sym(F).358 m = rng.randrange(1, 4); F = list(range(m))359 perms = list(itertools.permutations(F))360 # random homomorphism G -> Sym(F): choose images of generators and check compatibility by brute force361 hom = None362 for _ in range(20):363 cand = {g: rng.choice(perms) for g in G}364 if all(cand[compose(g, h)] == compose(cand[g], cand[h]) for g in G for h in G):365 hom = cand; break366 if hom is None: continue367 n_cases += 1368 I = list(range(nI)); A = [(i, a) for i in I for a in F]369 act = lambda g, x: (g[x[0]], hom[g][x[1]])370 # equivariant section by brute force: s : I -> F with s(g.i) = g.s(i)371 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))372 # the criterion: for each orbit representative i, the stabiliser G_i has a fixed point in the fibre373 orbits = {}374 for i in I: orbits.setdefault(frozenset(g[i] for g in G), i)375 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())376 ok &= exists == crit377 n_exist += exists378 # 5:E3 (p05029)379 R.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,380 f"{n_cases} families, {n_exist} with a section; the criterion agrees in every case")381382 # C4 the definable basis and the equivariant obstruction383 p = 5; ok = True384 vecs = list(itertools.product(range(p), repeat=3))385 def span(B):386 S = {(0, 0, 0)}387 for b in B:388 S = {tuple((s[k] + c * b[k]) % p for k in range(3)) for s in S for c in range(p)}389 return S390 subspaces = set()391 for k in range(4):392 for B in itertools.combinations(vecs[1:], k):393 S = frozenset(span(B))394 if len(S) == p ** k: subspaces.add(S)395 ok &= len(subspaces) == 1 + 31 + 31 + 1396 for V in subspaces:397 B = []; rest = sorted(V - {(0, 0, 0)})398 while rest:399 b = min(rest); B.append(b); Sp = span(B); rest = sorted(V - Sp)400 ok &= span(B) == V and len(B) == {1: 0, 5: 1, 25: 2, 125: 3}[len(V)]401 obstruction = {q: all((-v) % q != v for v in range(1, q)) for q in (3, 5, 7, 11, 13)}402 ok &= all(obstruction.values()) and (-1) % 2 == 1403 # 5:E4 (p05030)404 R.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,405 "obstruction over F_3, F_5, F_7, F_11, F_13; none over F_2")406407 # C5 periodic Koenig408 ok = True; n_graphs = 0409 for n in (1, 2, 3):410 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)]):411 n_graphs += 1412 for r in range(n):413 walk = [r]414 while len(walk) <= n:415 walk.append(min(out[walk[-1]]))416 seen = {}; period = None417 for k, v in enumerate(walk):418 if v in seen: period = k - seen[v]; break419 seen[v] = k420 ok &= period is not None and 1 <= period <= n421 for n in (10, 20, 30):422 for _ in range(30):423 out = [sorted(rng.sample(range(n), rng.randrange(1, 4))) for _ in range(n)]424 walk = [0]425 while len(walk) <= n: walk.append(out[walk[-1]][0])426 first = next(k for k in range(len(walk)) if walk[k] in walk[k + 1:])427 k2 = walk.index(walk[first], first + 1); period = k2 - first428 ok &= period <= n and all(walk[first + j] == walk[first + j + period] for j in range(len(walk) - first - period))429 # 5:E5 (p05031)430 R.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,431 f"{n_graphs} digraphs exhaustive")432433 # C6 periodic de Bruijn-Erdos in dimension one434 ok = True; n_col = 0; n_uncol = 0435 for _ in range(40):436 b = rng.randrange(1, 4); c = rng.choice((2, 3))437 intra = [(u, v) for u in range(b) for v in range(u + 1, b) if rng.randrange(5) < 3] # edges inside a block438 inter = [(u, v) for u in range(b) for v in range(b) if rng.randrange(5) < 2] # block k -> block k+1439 cols = [col for col in itertools.product(range(c), repeat=b) if all(col[u] != col[v] for u, v in intra)]440 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_c441 # finite subgraphs colorable for all n <=> walks of every length <=> D'_c (vertices beginning walks of every length) nonempty442 alive = set(cols)443 while True:444 nxt = {x for x in alive if any((x, y) in edges for y in alive)}445 if nxt == alive: break446 alive = nxt447 if not alive:448 n_uncol += 1449 # some finite subgraph is not c-colorable: the longest walk is bounded — verify by search up to |cols| + 1 blocks450 ok &= not any(True for _ in [0] if len(cols) and longest_walk(cols, edges) > len(cols))451 continue452 n_col += 1453 # a definable periodic coloring: greedy walk in D'_c from the least vertex454 walk = [min(alive)]455 while len(walk) <= len(alive):456 walk.append(min(y for y in alive if (walk[-1], y) in edges))457 first = next(k for k in range(len(walk)) if walk[k] in walk[k + 1:]); k2 = walk.index(walk[first], first + 1)458 cycle = walk[first:k2]; m = len(cycle)459 ok &= 1 <= m <= len(alive)460 # verify the periodic coloring on 6 periods461 seq = (cycle * 6)462 ok &= all((seq[k], seq[k + 1]) in edges for k in range(len(seq) - 1))463 # 5:E6 (p05032)464 R.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,465 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")466467# ------------------------------------------------------------------------------------------------------------468# block D: determinacy on the finite totality (5:D8, B7)469# Section 4.4 and Section 3.2 of the paper. D1 (Proposition finiteness, the finite direction): on the frame W₃ the470# full second-order theory is decided by exhaustive evaluation — every second-order sentence of a sample (quantifiers471# over all 8 subsets, all 512 binary relations, all 27 functions) receives a definite value, among them the472# well-ordering of the domain and the Dedekind-finiteness statement (no injective non-surjective function), and the473# count of subsets, relations and functions is exactly 2ⁿ, 2^{n²}, nⁿ. D2 (the Ω-hard row): a Π⁰₁ sentence receives a474# verdict from each frame about its own domain — the bounded Goldbach statement is true in every frame W_N, N ≤ 400 —475# and no frame states the closure over all frames; the frame values are reported, the closure is not a frame sentence.476@R.block("D", BLOCK["D"])477def block_D():478 """Block D — determinacy on the finite totality (EXACT): D1–D2."""479 # D1 the finite direction: second-order sentences over W_3 decided by exhaustion480 n = 3; D = range(n); ok = True481 subsets = [frozenset(x for x in D if m >> x & 1) for m in range(1 << n)]482 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))]483 functions = list(itertools.product(D, repeat=n))484 ok &= len(subsets) == 2 ** n and len(relations) == 2 ** (n * n) and len(functions) == n ** n485 lt = frozenset((x, y) for x in D for y in D if x < y)486 # 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))487 s1 = all(not S or any(all((y, x) not in lt for y in S) for x in S) for S in subsets)488 # there is a linear order (exists R: irreflexive, transitive, total): a second-order existential over 512 relations489 s2 = any(all((x, x) not in Rel for x in D) and all((x, z) in Rel for (x, y) in Rel for (y2, z) in Rel if y == y2)490 and all((x, y) in Rel or (y, x) in Rel or x == y for x in D for y in D) for Rel in relations)491 # Dedekind-finite: no function is injective and not surjective (over all 27 functions)492 s3 = not any(len(set(f)) == n and set(f) != set(D) for f in functions)493 # a false one: every subset has exactly two elements494 s4 = all(len(S) == 2 for S in subsets)495 ok &= s1 and s2 and s3 and not s4496 # 5:D8 (p05024)497 R.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,498 "second-order quantifiers as finite conjunctions/disjunctions")499500 # D2 the Pi_1 sentence frame by frame: bounded Goldbach true in every frame N <= 400; the closure is no frame sentence501 ok = True; vals = []502 for N in range(4, 401):503 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 N504 vals.append(v); ok &= v505 # 5:B7 (p05011)506 R.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,507 f"{len(vals)} frames, all true; no frame decides the unbounded quantifier")508509510if __name__ == "__main__":511 want = [a.upper() for a in sys.argv[1:]] or sorted(BLOCK)512 bad = [b for b in want if b not in BLOCK]513 if bad: sys.exit(f"no block {', '.join(bad)}: the blocks are {', '.join(sorted(BLOCK))}")514 for b in want: R.run_block(b)515 sys.exit(0 if R.summary(write=False, expect=list(LEDGER) if want == sorted(BLOCK) else None) else 1)516