The ledger file frc/ledgers/p25_godel.py of Incompleteness Without Infinity, rendered with an anchor per line: the marked lines (# 25:C2 (p25010): a predicate and its accession key) are the checks that decide the predicates of the paper's predicate ledger — 24 of 24 checks passing; the predicates' theorems are the declarations of Godel in the core. ▶ run the predicates on Google Colab.
1"""p25_godel — the ledger file of 25-godel (the 25-godel migration, 20 October 2026).23"Incompleteness Without Infinity" (Akhtman, preprint 2026; Preprints doi 10.20944/preprints202607.0850.v1). The paper's4predicate ledger is docs/25-godel/25-godel-ledger.json. This file binds its python-witnessed predicates to the framework:5the table of keys (generated from the ledger by ci/make_ledgers.py) and the checks of seven blocks, twenty-four in all,6every one EXACT. The checks call the logic theme: frc/logic.py holds the running example M_p with its tables read on7demand, the prenex evaluator that builds the whole evaluation object and counts its matrix evaluations, every formula8over M_2 up to a length with its truth table and free variables, the independent reader of the written formula, the9closed terms over {1, +} as trees, and the certificate format of the wrap lemma with its verifier; frc/diagonal.py holds10the name costs, k*(M) and t(M) by the same search as the Lean's, the decoders and the dense-coded instance of Section 5.211with their printer, reader and model checker. Each check names the predicate(s) it witnesses (LEDGER) and carries a12`# 25:XN (<key>)` marker when it decides one (PREDICATES). A consequence row of the paper (C3, G6, H4, J2) is named on13the marker of the check of the row it rests on.1415The paper's validation package src/25-godel (one script, godel.py) stays the published witness until the paper's release16pins the framework; the blocks here are its blocks, check for check, with the shared machinery moved to the themes and17the labels shortened to one sentence each, the enumerated counts in the detail of the record. Where a check works on a18sample, its label says so and the sample is fixed: the sentences of A2, C5 and F2, the completions of two certificates in19B3 (seeded), the maps at N = 3 in D2 (every 37th), the matrix family over M_5 in E1, the positions of lambda in G2 and20G3 (seeded). D3 and D5 decide ranges of structures and the base cases of t(M) < m; the comment of block D carries the21proofs for every structure, and the Lean side proves them for every alphabet and every digit count. The comment above22frc.diagonal.dense carries the proofs for the fields of the instance, where no model check is possible.2324The Lean side, under the rule of this paper that every T row has a core proof: the theme files lean/FrcCore/Theme/Logic.lean25(the finite theories, their decidability and completeness), Theme/Reach.lean (the certificate traces, the wrap, aliasing,26the reach bound, the length horizon, the evaluation ceiling, the global clause, the trichotomy's middle cell),27Theme/Diagonal.lean (the syntax with its mention cost, the template, the no-compression theorem, the decoders Int_J) and28Theme/Threshold.lean (the name-cost bound, k*(M), t(M) < a^(d-1)); on Mathlib lean/FrcLedger/Theme/Logic.lean (the29cardinal forms); the keys in Keys/Logic.lean of both libraries, the certificates Ledgers/P25Godel.lean. The rows F8, G8,30G5 and H3 of the paper carry no Lean theorem and are retagged I in the ledger of 20 October 2026; the checks G2, G3 and31E2 here stay as their corroboration.3233No numeral above Ω ∼ 10¹²³ is formed: the comparison of the window with the chart bound is made in digit counts (8234base-32 digits against 1,024), the instance of G2 and G3 is a string, never a number.3536 python3 -m frc.ledgers.p25_godel every block, the census; exit 1 if a check fails (≈ 130 s: D 20 s, E 33 s, G 75 s)37 python3 -m frc.ledgers.p25_godel D one block (A to G)38 from frc.ledgers.p25_godel import R; R.predicate("25:F6") one predicate: its blocks run once per session3940Blocks: A Gödel's hypotheses over a finite structure (Section 3) (25:C1, C2, C3, C5)41 B the part and the whole: collisions, aliasing, the wrap (Section 4) (25:D1, D3, D4, J2)42 C the reach bound and the horizon's counting facts (Sections 5.1, 5.3, 5.4) (25:E1, E2, E4, G1, G2, G7)43 D the diagonal under finitude: mention cost, the template, density (5.2) (25:F1, F2, F3, F4, F6, G6)44 E fragment truth: the pairing prefix and the guessed labels (Section 5.3) (25:G4, G5)45 F second-order decidability and the trichotomy's middle cell (Section 6) (25:H2, H4, H5)46 G the window below the threshold: decoders, the dense-coded instance (5.2) (25:F7, F8, G8)4748Checks: 24, all EXACT. The notebook frc/ledgers/p25_godel.ipynb runs one predicate per cell, the cell's id its key (gate G13).49"""50import sys, itertools, math, random51from fractions import Fraction5253from frc.registry import Registry54from frc.logic import (catalan, trees, tree_value, tree_text, decide, sentences, VARS, formulas_M2, read_formula,55 Mp, lookup, verify, term_of, eval_term, eval_step, small_world, commutative)56from frc.diagonal import name_cost, delta_names, lambda_names, admits, fit_table, last_k, deep, dense5758# ---- generated by ci/make_ledgers.py from docs/25-godel/25-godel-ledger.json; edit the ledger, not this table ----59PAPER = "25-godel"60KEYS = {"A1": "p25001", "A2": "p25002", "A3": "p25003", "A4": "p25004", "B1": "p25005", "B2": "p25006", "B3": "p25007", "B4": "p25008", "B5": "p25009", "C1": "p25010", "C2": "p25011", "C3": "p25012", "C4": "p25013", "C5": "p25014", "D1": "p25015", "D2": "p25016", "D3": "p25017", "D4": "p25018", "E1": "p25019", "E2": "p25020", "E3": "p25021", "E4": "p25022", "F1": "p25023", "F2": "p25024", "F3": "p25025", "F4": "p25048", "F5": "p25027", "F6": "p25047", "F7": "p25049", "F8": "p25050", "G1": "p25028", "G2": "p25029", "G3": "p25030", "G4": "p25031", "G5": "p25032", "G6": "p25033", "G7": "p25034", "G8": "p25051", "H1": "p25035", "H2": "p25036", "H3": "p25037", "H4": "p25038", "H5": "p25039", "J1": "p25040", "J2": "p25041", "J3": "p25042", "J4": "p25043", "J5": "p25044"} # every row of the ledger: its label and its accession key61LEAN = {"C1": "core, ml", "C2": "core, ml", "C3": "core, ml", "C5": "core, ml", "D1": "core, ml", "D3": "core, ml", "D4": "core", "E1": "core, ml", "E2": "core, ml", "E4": "core", "F1": "core", "F2": "core", "F3": "core", "F4": "core, ml", "F6": "core", "F7": "core", "G1": "core", "G2": "core", "G4": "core", "G6": "core", "G7": "core", "H2": "core, ml", "H4": "core, ml", "H5": "core", "J2": "core"} # the rows with a Lean declaration: the libraries whose key files prove them62# ---- end of the generated table ----6364LEAN_ONLY = () # the predicates with a Lean declaration and no python check (gate G12): none6566# The paper's predicate ledger (Appendix A; predicates cited as 25:XN): the predicate(s) each check witnesses. A consequence67# row (C3, G6, H4, J2) is named on the checks of the rows it rests on (decision D4 of the blueprint, 20 October 2026).68LEDGER = {69 "A1": "25:C1, 25:C3", "A2": "25:C2, 25:C3", "A3": "25:C5",70 "B1": "25:D1", "B2": "25:D3", "B3": "25:D4, 25:J2",71 "C1": "25:E1", "C2": "25:E2", "C3": "25:E4", "C4": "25:G1", "C5": "25:G2", "C6": "25:G7",72 "D1": "25:F1", "D2": "25:F2", "D3": "25:F4", "D4": "25:F3, 25:G6", "D5": "25:F6",73 "E1": "25:G4", "E2": "25:G5",74 "F1": "25:H2, 25:H4", "F2": "25:H5",75 "G1": "25:F7", "G2": "25:F8", "G3": "25:G8",76}7778# the package record (godel.<id>) each check reproduces: the ids are the package's79FAMILY = {pid: f"godel.{pid}" for pid in LEDGER}8081BLOCK = {"A": "Gödel's hypotheses over a finite structure",82 "B": "the part and the whole: collisions, aliasing, the wrap",83 "C": "the reach bound and the horizon's counting facts",84 "D": "the diagonal under finitude: mention cost, the template, density",85 "E": "fragment truth: the pairing prefix and the guessed labels",86 "F": "second-order decidability and the trichotomy's middle cell",87 "G": "the window below the threshold: decoders, the dense-coded instance"}8889# the deciding check of each witnessed predicate (the other checks that touch it are corroboration)90PREDICATES = {91 "25:C1": "A1", "25:C2": "A2", "25:C3": "A1", "25:C5": "A3",92 "25:D1": "B1", "25:D3": "B2", "25:D4": "B3", "25:J2": "B3",93 "25:E1": "C1", "25:E2": "C2", "25:E4": "C3", "25:G1": "C4", "25:G2": "C5", "25:G7": "C6",94 "25:F1": "D1", "25:F2": "D2", "25:F4": "D3", "25:F3": "D4", "25:G6": "D4", "25:F6": "D5",95 "25:G4": "E1", "25:G5": "E2",96 "25:H2": "F1", "25:H4": "F1", "25:H5": "F2",97 "25:F7": "G1", "25:F8": "G2", "25:G8": "G3",98}99100R = Registry("25", "godel", LEDGER, PREDICATES, sources=[__file__])101102P_SMALL, P_MID, P_BIG = 13, 1000033, 10**18 + 9 # the three sizes of M_p the blocks share (the package's constants)103T_EXACT = {} # (a, m) -> (d, fit_table), computed in D3 and read in D5 (block D)104105# ------------------------------------------------------------------------------------------------------------106# block A: Gödel's hypotheses over a finite structure (25:C1, C2, C5) — Section 3 of the paper.107# A1: no finite structure carries a successor that is injective and omits an element (exhaustive over all N^N maps,108# N ≤ 7), so no finite structure is a model of Q, and none interprets it. A2: the theory of M_p is decided by exhaustive109# evaluation — every sentence of a sample takes the value number theory gives it, the evaluation object has m^q leaves at110# quantifier depth q, exactly one of a sentence and its negation is true; and the characterising sentence σ_M, evaluated111# as a sentence in every structure on 3 elements, holds exactly in the structures isomorphic to M, and in none of 1 or 2112# 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 length113# at most m+1 admit no injective numbering into M — while truth is given externally by a finite table.114@R.block("A", BLOCK["A"])115def block_A():116 """Block A — Gödel's hypotheses over a finite structure (EXACT): A1–A3."""117 # A1 no finite model of Q: injective maps on a finite set are onto; the chain 0, S0, SS0, … repeats118 ok = True; det = []; n_maps = n_chain = 0119 for N in range(1, 8):120 n_inj = n_miss = 0121 for S in itertools.product(range(N), repeat=N):122 n_maps += 1123 if len(set(S)) == N:124 n_inj += 1125 ok &= set(S) == set(range(N)) # injective => surjective126 if 0 not in S: n_miss += 1 # a successor of Q: injective with 0 outside its range127 ok &= n_inj == math.factorial(N) and n_miss == 0128 det.append(f"N={N}: {N**N} maps, {n_inj} injective, all onto")129 for N in range(1, 7): # the numerals 0, S0, …, S^N 0 are not pairwise distinct, whatever S130 for S in itertools.product(range(N), repeat=N):131 n_chain += 1132 x, seen = 0, [0]133 for _ in range(N): x = S[x]; seen.append(x)134 ok &= len(set(seen)) < len(seen)135 ok &= n_maps == 873612 and n_chain == 50069 # 1 + 4 + 27 + … + 7^7 maps; 1 + 4 + … + 6^6 chains136 # 25:C1 (p25010), 25:C3 (p25012)137 R.check("A1", "No finite model of Q: on a carrier of N elements every injective map is onto, so no successor is injective and misses 0, and the N+1 numerals 0, S0, ..., S^N 0 repeat under every S (all maps, N <= 7 and N <= 6)", ok,138 "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)" + "; " + ("; ".join(det[3:])))139140 # A2 completeness and decidability of Th(M_p); the evaluation object has m^q leaves; sigma_M is categorical141 ok = True; det = []; n_sent = 0142 for p in (5, 7, 13):143 for text, pat, mat, want in sentences(p):144 cnt = [0]; v = decide(p, pat, mat, cnt); n_sent += 1145 ok &= v == want and cnt[0] == p ** len(pat) # decided, with the evaluation object of size m^q146 dual = "".join("E" if c == "A" else "A" for c in pat)147 ok &= decide(p, dual, lambda vals, mat=mat: not mat(vals)) == (not v) # exactly one of the sentence and its negation is true148 det.append(f"p={p}: 8 sentences decided, depth-3 objects of {p**3} leaves")149 ok &= n_sent == 24150 # the characterising sentence sigma_M, evaluated as a sentence in a structure (c0, c1, o) on n elements: there are pairwise distinct151 # 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.152 # `distinct` and `closure` switch its first and last clause off, for the controls.153 def sigma(M_tab, n, c0, c1, tab, distinct=True, closure=True):154 for xs in (itertools.permutations(range(n), 3) if distinct else itertools.product(range(n), repeat=3)):155 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)) \156 and (not closure or all(y in xs for y in range(n))): return True157 return False158 def iso_forced(M_tab, c0, c1, tab):159 """Isomorphism to M tested a second way: M is generated by its constants (2 = 1 o 1), so an isomorphism is forced to be160 0 -> c0, 1 -> c1, 2 -> c1 o c1; it is one iff that map is a bijection carrying every table entry."""161 f = (c0, c1, tab[3 * c1 + c1])162 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))163 Z3 = [[(a + b) % 3 for b in range(3)] for a in range(3)]164 NC = [[0, 1, 2], [2, 2, 0], [1, 0, 0]] # a second structure: a non-commutative table with 1 o 1 = 2165 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))166 models = {}167 for name, M_tab in (("Z_3", Z3), ("NC", NC)):168 n_mod = total = 0169 for c0 in range(3):170 for c1 in range(3):171 for tab in itertools.product(range(3), repeat=9): # every structure (c0, c1, o) on 3 elements172 total += 1; sg = sigma(M_tab, 3, c0, c1, tab)173 ok &= sg == iso_forced(M_tab, c0, c1, tab) # the models of sigma_M are exactly the structures isomorphic to M174 n_mod += sg175 ok &= total == 3 * 3 * 3 ** 9 == 177147 and n_mod == math.factorial(3)176 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 model177 # smaller structures: the distinctness clause excludes them. Without it sigma_M holds in the one-element structure178 # (every table equation collapses to the point); with it, in no structure of one or two elements.179 n1 = sigma(M_tab, 1, 0, 0, (0,)); n1_open = sigma(M_tab, 1, 0, 0, (0,), distinct=False)180 n2 = n2_scanned = 0181 for c0 in range(2):182 for c1 in range(2):183 for tab in itertools.product(range(2), repeat=4): n2_scanned += 1; n2 += sigma(M_tab, 2, c0, c1, tab)184 ok &= (n1, n1_open, n2, n2_scanned) == (False, True, 0, 64)185 # larger structures: the closure clause excludes them. Every one-element extension of M (4^7 completions of the new row186 # and column) satisfies sigma_M without its closure clause, and none satisfies sigma_M.187 ext = ext_open = ext_scanned = 0188 for new in itertools.product(range(4), repeat=7):189 tab = [0] * 16190 for a in range(3):191 for b in range(3): tab[4 * a + b] = M_tab[a][b]192 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]193 ext_scanned += 1; ext += sigma(M_tab, 4, 0, 1, tab); ext_open += sigma(M_tab, 4, 0, 1, tab, closure=False)194 ok &= (ext, ext_open, ext_scanned) == (0, 16384, 16384)195 models[name] = n_mod196 # 25:C2 (p25011), 25:C3 (p25012)197 R.check("A2", "Th(M_p) is decided by exhaustive evaluation (p = 5, 7, 13): a sample of sentences takes the values number theory gives, exactly one of a sentence and its negation is true, and sigma_M holds exactly in the structures isomorphic to M among all structures on 3 elements", ok,198 "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)" + "; " + ("; ".join(det) + f"; models of sigma among 177147 structures: {models}; 64 structures of 2 elements and 16384 extensions to 4 elements: none"))199200 # A3 the sentences outnumber the elements; truth is an external table201 ok = True; n_maps = 0202 def value(sent):203 """The truth value of ~…~F, by recursion on the written sentence (F is the false constant)."""204 return False if sent == "F" else not value(sent[1:])205 for m in range(2, 6):206 sents = ["~" * k + "F" for k in range(m + 1)] # F, ~F, ~~F, …: m+1 sentences of length <= m+1207 ok &= len(set(sents)) == m + 1 and max(map(len, sents)) == m + 1208 for f in itertools.product(range(m), repeat=m + 1): # every numbering of them into M209 n_maps += 1210 ok &= len(set(f)) < m + 1 # is not injective211 table = {sent: value(sent) for sent in sents} # the external truth table: m+1 entries, computed from the sentences212 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, alternating213 ok &= n_maps == 2 ** 3 + 3 ** 4 + 4 ** 5 + 5 ** 6 == 16738214 # 25:C5 (p25014)215 R.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 maps, m = 2..5), and their truth is a finite external table computed from the written sentences", ok,216 "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" + "; " + (f"{n_maps} numberings scanned, none injective"))217# ------------------------------------------------------------------------------------------------------------218# block B: the part and the whole (25:D1, D3, D4; corroborates J2) — Section 4.219# B1: an agent with a^K storage states in a structure of m > a^K elements has no injective encoding (every map on six220# instances; at a^K = m the injective readings are the bijections). B2: every total reading has a fibre of at least221# ⌈m/a^K⌉ ≥ 2 elements, some reading attains the bound, and every element outside a maximal faithfully represented range222# is an alias of one inside it. B3: the wrap — for a certificate checked by table lookups, the223# structure M' on the cited elements (the tables agreeing with M on the cited entries, completed arbitrarily) accepts the224# same record by the same steps and makes its end sentence true: under EVERY completion for a certificate over Z_5, under225# a fixed sample of completions for two larger ones; an axiom asserted on syntactic recognition is accepted there too,226# and its truth does not transport.227@R.block("B", BLOCK["B"])228def block_B():229 """Block B — the part and the whole: collisions, aliasing, the wrap (EXACT): B1–B3."""230 # B1 the relational diagonal: a^K < m leaves no injective encoding231 ok = True; det = []; n_all = 0232 for a, K, m in ((2, 1, 3), (2, 2, 5), (3, 1, 4), (2, 2, 6), (5, 1, 6), (2, 2, 7)):233 states = a ** K; n = 0234 assert states < m235 for rho in itertools.product(range(states), repeat=m): # every assignment of storage states to the m elements236 n += 1237 ok &= any(rho[x] == rho[y] for x in range(m) for y in range(x)) # identifies two of them238 det.append(f"a^K={states}<m={m}: {n} readings"); n_all += n239 ok &= n_all == 2 ** 3 + 4 ** 5 + 3 ** 4 + 4 ** 6 + 5 ** 6 + 4 ** 7 == 37218240 n_inj = sum(1 for rho in itertools.product(range(4), repeat=4) if len(set(rho)) == 4)241 ok &= n_inj == 24 # the control: with as many states as elements, 4! readings are injective242 # 25:D1 (p25015)243 R.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 maps on six instances), and with a^K = m = 4 the injective readings are the bijections", ok,244 "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" + "; " + ("; ".join(det[:4])))245246 # B2 aliasing with multiplicity247 ok = True; det = []; n_all = 0248 for m, Rs in ((4, 2), (5, 2), (5, 3), (6, 3), (7, 2), (7, 3), (6, 4), (5, 4)):249 need = -(-m // Rs); least = m # ceil(m / R)250 for rho in itertools.product(range(Rs), repeat=m):251 n_all += 1252 big = max(sum(1 for x in range(m) if rho[x] == y) for y in range(Rs))253 ok &= big >= need; least = min(least, big) # some reading stands for at least ceil(m/R) elements254 ok &= least == need >= 2 # the bound is attained, and it is at least 2255 det.append(f"m={m}, R={Rs}: largest fibre >= {need}, attained")256 ok &= n_all == 2 ** 4 + 2 ** 5 + 3 ** 5 + 3 ** 6 + 2 ** 7 + 3 ** 7 + 4 ** 6 + 4 ** 5 == 8455257 # a maximal faithfully represented range: a set S of elements on which the reading is injective and which no larger set with258 # that property contains. Every element outside it is read as an element inside it (an alias).259 n_max = 0260 for m, Rs in ((4, 2), (5, 2), (5, 3), (6, 3), (5, 4), (6, 4)):261 for rho in itertools.product(range(Rs), repeat=m):262 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")]263 for mask in faithful:264 if any(t != mask and t & mask == mask for t in faithful): continue # a larger faithful set contains S: not maximal265 S = [x for x in range(m) if (mask >> x) & 1]; out = [x for x in range(m) if not (mask >> x) & 1]266 n_max += 1267 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 alias268 ok &= n_max == 31203269 # 25:D3 (p25017)270 R.check("B2", "Aliasing: every total reading of m elements by R < m states has a fibre of at least ceil(m/R) >= 2 elements and some reading attains it (eight instances), and every element outside a maximal faithful range is read as one inside it (six instances)", ok,271 "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)" + "; " + ("; ".join(det)))272273 # B3 the wrap: the same certificate, with its warrant, in a small world274 ok = True; det = []275 r = 2 # the largest operation arity276 # (i) a certificate over M_13: ((1+1)+1)*(1+1) = (1+1)*((1+1)+1)277 rec = [("c", 1), ("o", "+", 0, 0, 2), ("o", "+", 1, 0, 3), ("o", "*", 2, 1, 6), ("o", "*", 1, 2, 6), ("=", 3, 4)]278 M = Mp(13); acc, vals, cited, elems, n_look = verify(rec, M)279 ok &= acc and len(elems) <= n_look <= len(rec) # an operand is an earlier step, so each lookup cites at most one new280 # element: within the lemma's bound of r+1 elements per lookup281 rng = random.Random(25); n_fill = 0282 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] * 40283 for f in fills:284 fill = f or (lambda op, x, y, U: rng.choice(U))285 W = small_world(cited, elems, "+*", fill); n_fill += 1286 acc2, vals2, cited2, elems2, n2 = verify(rec, W)287 ok &= acc2 and vals2 == vals and cited2 == cited # accepted by the same steps, the same lookups, the same results288 ok &= eval_term(W, term_of(rec, 3)) == eval_term(W, term_of(rec, 4)) # the end sentence is true in M'289 ok &= n_fill == 42290 bad_val = rec[:3] + [("o", "*", 2, 1, 7)] # the controls: a record cut at a wrong product, and a false end sentence (3 = 6),291 bad_end = rec[:-1] + [("=", 2, 3)] # are rejected in M and in the last small world292 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]293 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)")294 # (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)*t295 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 i296 for _ in range(7):297 rec.append(("o", "*", len(rec) - 1, len(rec) - 1, v * v % p)); v = v * v % p; size.append(2 * size[-1] + 3)298 i_t = len(rec) - 1299 rec.append(("o", "+", i_t, 0, (v + 1) % p)); i_s = len(rec) - 1; size.append(size[i_t] + 1 + 3)300 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))301 end_len = 2 * (size[i_t] + size[i_s] + 3) + 1 # the end sentence written out: a few thousand symbols302 acc, vals, cited, elems, n_look = verify(rec, M)303 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 p304 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 residue305 n_fill2 = 0306 for f in fills[:12]:307 fill = f or (lambda op, x, y, U: rng.choice(U))308 W = small_world(cited, elems, "+*", fill); n_fill2 += 1309 acc2, vals2, cited2, _, _ = verify(rec, W)310 ok &= acc2 and vals2 == vals and cited2 == cited311 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 tables312 ok &= n_fill2 == 12313 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")314 # (iii) every completion, exhaustively: 1+(1+1) = (1+1)+1 over (Z_5; 0, 1, +)315 rec = [("c", 1), ("o", "+", 0, 0, 2), ("o", "+", 0, 1, 3), ("o", "+", 1, 0, 3), ("=", 2, 3)]316 M = Mp(5, "+"); acc, vals, cited, elems, n_look = verify(rec, M); U = sorted(elems)317 free = [(x, y) for x in U for y in U if ("+", x, y) not in cited]318 n_all = n_true = 0319 for choice in itertools.product(U, repeat=len(free)):320 tab = dict(zip(free, choice))321 W = small_world(cited, elems, "+", lambda op, x, y, U: tab[(x, y)])322 acc2, vals2, _, _, _ = verify(rec, W); n_all += 1323 n_true += acc2 and eval_term(W, term_of(rec, 2)) == eval_term(W, term_of(rec, 3))324 ok &= acc and n_all == len(U) ** len(free) == 729 and n_true == n_all # a locally sound certificate keeps its truth under every completion325 # (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)326 COMM = "AxAy x+y=y+x"; D_AX = (COMM,)327 rec_ax = [("c", 1), ("o", "+", 0, 0, 2), ("o", "+", 1, 0, 3), ("ax", COMM)]328 acc, vals, cited, elems, _ = verify(rec_ax, M, D_AX); U = sorted(elems)329 free = [(x, y) for x in U for y in U if ("+", x, y) not in cited]330 n_acc = n_comm = n_w = 0331 for choice in itertools.product(U, repeat=len(free)):332 tab = dict(zip(free, choice))333 W = small_world(cited, elems, "+", lambda op, x, y, U: tab[(x, y)]); n_w += 1334 n_acc += verify(rec_ax, W, D_AX)[0]; n_comm += commutative(W)335 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 worlds336 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 accepted337 # (v) the display case of the neutrality theorem: a description T whose axiom rules assert the successor axioms of Q. Its record is338 # accepted by the same syntactic check over M_13, where the axioms are false (0 = S(12))339 T_Q = ("S injective", "0 not in the range of S")340 succ = lambda x: (x + 1) % 13341 q_inj = len({succ(x) for x in range(13)}) == 13; q_zero = all(succ(x) != 0 for x in range(13))342 ok &= verify([("ax", T_Q[0]), ("ax", T_Q[1])], Mp(13), T_Q)[0] and q_inj and not q_zero343 # 25:D4 (p25018), 25:J2 (p25041)344 R.check("B3", "The wrap: a certificate checked by table lookups is accepted by the same steps, with a true end sentence, in the structure M' on its cited elements, under every completion over Z_5 and fixed samples over M_13 and M_p (p = 10^18+9); a wrong product or a false end sentence is rejected in both worlds", ok,345 "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" + "; " + ("; ".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)"))346# ------------------------------------------------------------------------------------------------------------347# 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.348# C1: the closed terms over {1, +} with l leaves are the C_{l-1} full binary trees, all of value l mod p, giving349# 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 number350# (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 evaluation351# calculus the universal rule applies to the full set of its m premises alone, so a global clause has a derivation of352# length m+1 > H for every budget H < m. C4: truths longer than a budget B, built and written out — no record of length353# <= B contains one. C5: the one-rule system D_tt accepts exactly the true sentences, each in one line, and step-checks354# by m^q evaluations. C6: the two counting cells of the decomposition table that are not predicates of their own — bounded355# consistency by exhaustive search, with the candidate count of its brute certificate, and reach against the budget.356@R.block("C", BLOCK["C"])357def block_C():358 """Block C — the reach bound and the horizon's counting facts (EXACT): C1–C6."""359 # C1 abundance of truths360 ok = True; det = []; n_trees = 0361 for l in range(1, 11):362 ts = trees(l); n_trees += len(ts)363 ok &= len(ts) == len(set(ts)) == catalan(l - 1) # the terms with l leaves are the full binary trees: Catalan C_{l-1}364 for p in (2, 3, 5, 13):365 ok &= {tree_value(t, p) for t in ts} == {l % p} # all of one value, l mod p366 ok &= all(len(tree_text(t)) == 4 * l - 3 for t in ts) # written out: 4l-3 symbols, an equation t = t' 8l-5367 ok &= n_trees == 6918368 det.append(f"l <= 10: {n_trees} trees enumerated, each of value l mod p for p = 2, 3, 5, 13")369 ok &= all(catalan(l - 1) >= 2 ** (l - 2) for l in range(2, 501)) # C_{l-1} >= 2^{l-2}370 pair = lambda l: catalan(l - 1) * (catalan(l - 1) - 1) // 2371 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)372 for L in range(43, 4001): # the truths of length <= L: the cohort at l = floor((L+5)/8) leaves373 l = (L + 5) // 8374 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}375 # 25:E1 (p25019)376 R.check("C1", "Abundance: the closed terms over {1, +} with l leaves are the Catalan(l-1) trees, all of value l mod p (l <= 10; p = 2, 3, 5, 13), the cohort of true equations C(C_{l-1}, 2) >= 2^l for 6 <= l <= 500, so the truths of length <= L number at least 2^{L/9} (43 <= L <= 4000)", ok,377 "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)" + "; " + ("; ".join(det) + f"; cohort at l = 6: {pair(6)} >= 64, at l = 4: {pair(4)} < 16"))378379 # C2 vanishing reach380 ok = True; det = []381 for a, Bmax in ((2, 12), (3, 7), (5, 5)):382 for B in range(Bmax + 1):383 n = sum(1 for k in range(B + 1) for _ in itertools.product(range(a), repeat=k)) # the strings of length <= B, enumerated384 ok &= n == (a ** (B + 1) - 1) // (a - 1) < a ** (B + 1)385 a, B = 2, 20; certs = a ** (B + 1)386 f12, f24, f48 = (Fraction(certs, pair(l)) for l in (12, 24, 48))387 ok &= f12 < 1 and f24 < Fraction(1, 10 ** 6) and f48 < f24 < f12388 for N in (10 ** 3, 10 ** 6, 10 ** 12, 10 ** 100):389 l0 = next(l for l in range(6, 2000) if certs * N < pair(l))390 ok &= all(certs * N < pair(l) for l in range(l0, l0 + 60)) # below 1/N from l0 on391 det.append(f"< 1/{'10^' + str(len(str(N)) - 1)} from l = {l0}")392 # 25:E2 (p25020)393 R.check("C2", "Vanishing reach: the records of length <= B over a letters number (a^{B+1}-1)/(a-1) < a^{B+1} (a = 2, 3, 5), and at a = 2, B = 20 the certified fraction of the equation cohort falls below 1 at l = 12, below 10^-6 at l = 24 and below each tested 1/N from a first l on", ok,394 "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" + "; " + (f"fraction at l = 12: {f12.numerator}/{f12.denominator}; " + "; ".join(det)))395396 # C3 a global clause in the bare evaluation calculus397 ok = True; det = []398 def bare_accepts(deriv, p, phi=lambda x, p: (x + 0) % p == x):399 """The bare evaluation calculus on the clause Ax x+0=x: a premise ("inst", c) is checked by one lookup; the universal rule400 ("all",) is accepted only when a premise for every element of the structure stands before it."""401 have = set()402 for st in deriv:403 if st[0] == "inst":404 if not phi(st[1], p): return False405 have.add(st[1])406 elif st[0] == "all":407 if have != set(range(p)): return False408 else: return False409 return bool(deriv) and deriv[-1] == ("all",)410 for p in (5, 13, 101, 1009):411 deriv = [("inst", c) for c in range(p)] + [("all",)] # the m premises phi(c), one per element, then the universal rule412 ok &= bare_accepts(deriv, p) and len(deriv) == p + 1 and all(len(deriv) > H for H in range(p))413 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 apply414 det.append(f"m={p}: length {len(deriv)}")415 n_sub = 0416 for p in (5, 13): # every subset of the premises: the rule applies to the full set alone417 for mask in range(2 ** p):418 n_sub += 1419 ok &= bare_accepts([("inst", c) for c in range(p) if (mask >> c) & 1] + [("all",)], p) == (mask == 2 ** p - 1)420 ok &= n_sub == 2 ** 5 + 2 ** 13 == 8224421 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,422 ok &= not bare_accepts([("inst", c) for c in range(5)], 5) # and premises without the universal step derive no global clause423 def rich_accepts(deriv, p):424 """A richer system: the bare calculus with one more rule, which asserts the clause as an axiom on syntactic recognition."""425 return deriv == [("ax", "Ax x+0=x")] or bare_accepts(deriv, p)426 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 derivation427 # 25:E4 (p25022)428 R.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 (m = 5, 13; every single omission for m = 101, 1009), so the derivation has length m+1 beyond every budget H < m, while an axiom rule derives the clause in one line", ok,429 "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" + "; " + ("; ".join(det) + f"; {n_sub} premise sets"))430431 # C4 the length horizon: truths longer than the budget, built and measured432 ok = True; det = []433 def comb(l, left):434 """The left comb ((1+1)+1)+… or the right comb 1+(1+(…)) with l leaves, as a tree."""435 t = 1436 for _ in range(l - 1): t = (t, 1) if left else (1, t)437 return t438 for B in (20, 100, 1000):439 l = (B + 5) // 8 + 1440 L, Rt = comb(l, True), comb(l, False)441 eq = tree_text(L) + "=" + tree_text(Rt) # the equation, written out442 ok &= L != Rt and len(eq) > B # longer than every record of length <= B, which would have to contain it443 ok &= all(tree_value(L, p) == tree_value(Rt, p) for p in (P_SMALL, P_MID)) # and true in M_p444 ok &= len(eq) - 8 <= B # the comb pair one leaf shorter fits: the horizon sits at this length445 det.append(f"B={B}: a true equation of {len(eq)} symbols")446 # 25:G1 (p25028)447 R.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, written out, is true in M_13 and M_1000033 and longer than B, so no record of length <= B contains it", ok,448 "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" + "; " + ("; ".join(det)))449450 # C5 the evaluation ceiling: the one-rule system D_tt451 ok = True; det = []452 for p in (5, 7):453 pool = {}; expect = {} # the sample and its negations: text -> (pattern, matrix); the value number theory gives each454 for text, pat, mat, want in sentences(p):455 pool[text] = (pat, mat); expect[text] = want456 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 want457 cost = [0]458 def dtt_accepts(deriv):459 """D_tt: every line is a sentence asserted outright, its side condition truth under exhaustive evaluation."""460 return all(decide(p, *pool[line], cost) for line in deriv)461 ok &= all(dtt_accepts([t]) == expect[t] for t in pool) # D_tt derives exactly the true sentences: sound, and complete on the sample462 truths = [t for t in pool if expect[t]]463 ok &= len(pool) == 16 and len(truths) == 8464 for t in truths:465 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 q466 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 derivation467 det.append(f"p={p}: 8 truths each derived in one line, 8 falsehoods rejected, step-check {p}^q evaluations (q = 3: {p**3})")468 # 25:G2 (p25029)469 R.check("C5", "The evaluation ceiling: the one-rule system D_tt accepts exactly the sentences number theory makes true (a sample over M_5, M_7), each true one derived in one line that is the sentence itself, while the step check of the rule performs m^q evaluations at depth q", ok,470 "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" + "; " + ("; ".join(det)))471472 # C6 the decomposition's counting cells: bounded consistency by exhaustive search; its brute certificate; reach against the budget473 ok = True474 M = Mp(5); n_rec = n_acc = n_false = n_absurd = n_absurd_acc = n_cut = 0475 def ext(rec, depth):476 """Every record of at most `depth` further term steps followed by an end step."""477 nonlocal n_rec, n_acc, n_false, n_absurd, n_absurd_acc, n_cut, ok478 k = len(rec)479 for i in range(k):480 for j in range(k):481 full = rec + [("=", i, j)]; n_rec += 1482 acc, vals, _, _, _ = verify(full, M)483 absurd = term_of(full, i) == ("c", 0) and term_of(full, j) == ("c", 1) # the record ends in the absurdity 0 = 1484 n_absurd += absurd485 if acc:486 n_acc += 1; n_absurd_acc += absurd487 n_false += eval_term(M, term_of(full, i)) != eval_term(M, term_of(full, j)) # the end sentence, evaluated from the tables488 if depth == 0: return489 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)]:490 if st[0] == "o" and lookup(M, st[1], verify(rec, M)[1][st[2]], verify(rec, M)[1][st[3]]) != st[4]:491 n_rec += 1; n_cut += 1; ok &= not verify(rec + [st], M)[0] # a step with a wrong value is rejected492 continue493 ext(rec + [st], depth - 1)494 ext([], 3)495 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 record496 ok &= n_absurd == 34 and n_absurd_acc == 0 # Con: 34 candidates end in 0 = 1, and none is accepted497 n_strings = 0498 for a in (2, 3): # the brute certificate of Con_H lists every candidate record of length <= H:499 for H in range(1, 11): # their number, counted by enumeration, exceeds the budget H500 n = sum(1 for k in range(H + 1) for _ in itertools.product(range(a), repeat=k)); n_strings += n501 ok &= n == (a ** (H + 1) - 1) // (a - 1) > H502 ok &= n_strings == 136935503 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 lengths504 reach = lambda B: sum(1 for L in eqs if L <= B) # those that fit in a budget of B symbols505 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 …506 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 = 1507 # 25:G7 (p25034)508 R.check("C6", "The decomposition's counting cells: bounded consistency decided by exhaustive search over the records of at most three term steps over M_5, the brute certificate of Con_H listing more than H candidate records (a = 2, 3; H <= 10), and the reflexivity instances growing with every 8 symbols (3 <= B < 68)", ok,509 "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" + "; " + (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)}"))510# ------------------------------------------------------------------------------------------------------------511# block D: the diagonal under finitude (25:F1, F2, F3, F4, F6) — Section 5.2.512# D1: mention cost — a coordinate on which the truth of a formula depends is a variable that occurs free in it: on a family of513# formulas over M_3 and on EVERY formula of length <= 9 over M_2 in four variables, each written out and read back by the514# independent reader. D2: the no-compression theorem on built instances — the graph of every injective map on M_2^N depends515# on all 2N coordinates; every formula that defines such a graph mentions all 2N variables; the diagonal formula written out516# from each of them computes theta at the diagonal image, names each coordinate of v at least three times and each of u at517# 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.518# D3: density — an injective coding of the a^n strings into k-tuples needs m^k >= a^n (below it every coding collides), so519# 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 least520# 2c(k) + c(k+k1) symbols, and its instance lambda at least 3c(k) + k1. D4: quotation exceeds mention — over EVERY formula521# of length <= 9 in six variables, the truth depends on fewer coordinates than the formula has symbols. D5: the threshold522# lies inside the count — the two costs fit their codes for no k beyond k*(M), no instance codes lambda at a length523# n >= t(M) = d k*(M), and t(M) < m in every structure.524#525# The statements of D3 and D5 hold for every alphabet a >= 2 and every structure; the checks decide ranges and the base526# 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 >= 1527# 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).528# The codes. The code of delta is the k1-tuple that fills u; it codes a string of some length n1 >= |delta|. The code of529# lambda is a k-tuple, the argument of theta; it codes a string of length n >= |lambda|. An injective coding of the strings530# 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.531# The count. In delta the block binds the k coordinates of v, Diag has k1 + k argument places and theta has k: each532# coordinate of v is named three times and each of u once, by k + k1 distinct names. Of k + k1 distinct names the k + k1533# shortest cost least, and the weight 3 goes to the k shortest: |delta| >= 2c(k) + c(k+k1). In lambda the places of u hold534# k1 closed terms of at least one symbol: |lambda| >= 3c(k) + k1. So an instance needs535# 2c(k) + c(k+k1) < d k1 and 3c(k) + k1 < dk,536# 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,537# N(k) = 2c(k) + c(2k), and implies the second.538# (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 j539# 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, and540# 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 gives541# 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 =542# 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, so543# N(k)/k does not decrease: at one scale the k that pass form an initial segment.544# (ii) No instance at n >= t(M) = d k*(M). An instance has k <= k*(M) by definition and n < dk, whatever the two545# injective codings.546# (iii) t(M) < m. For d <= 4 there is no instance: c(j) >= j, so the second inequality gives 3k + k1 < 4k, k1 < k, and547# 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,548# 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 a549# (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 fifteen550# pairs (a, d), all with a <= 5, which D5 decides directly, and holds at every larger a (J < d - 1 again). So551# t(M) < a^(d-1) <= m.552# Below, at one scale. For k <= floor(a^floor((d-1)/4) / 2) the 2k names have at most floor((d-1)/4) letters, so553# N(k) <= (d-1)k, which is at most the largest n with a^n <= m^k: the count leaves these k open.554# The cut 2^400 of the ranges is a test parameter.555@R.block("D", BLOCK["D"])556def block_D():557 """Block D — the diagonal under finitude: mention cost, the template, density (EXACT): D1–D5."""558 # D1 mention cost: a family over M_3, then every short formula over M_2559 m, V = 3, 3560 assigns = list(itertools.product(range(m), repeat=V)); idx = {a: i for i, a in enumerate(assigns)}561 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)]562 terms = list(leaf)563 for op, f in (("+", lambda x, y: (x + y) % m), ("*", lambda x, y: (x * y) % m)):564 for s in leaf:565 for t in leaf:566 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]))567 # a formula is (truth table over the 27 assignments, length in symbols, free variables)568 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]569 def neg(f): return (tuple(not b for b in f[0]), f[1] + 1, f[2])570 def ex(i, f): # Ev_i phi: 2 more symbols; v_i is bound571 tab = tuple(any(f[0][idx[a[:i] + (c,) + a[i + 1:]]] for c in range(m)) for a in assigns)572 return (tab, f[1] + 2, f[2] - {i})573 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])574 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]575 family = list(atoms) + [neg(f) for f in atoms] + [ex(i, f) for i in range(V) for f in atoms]576 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]577 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]578 def depends(tab, i):579 return any(tab[idx[a]] != tab[idx[a[:i] + (c,) + a[i + 1:]]] for a in assigns for c in range(m))580 ok = True; n_dep = [0] * (V + 1); n_idle = 0581 for tab, length, free in family:582 dep = {i for i in range(V) if depends(tab, i)}583 ok &= dep <= free # truth depends on coordinate i => v_i occurs (free)584 n_dep[len(dep)] += 1; n_idle += dep != free # the converse fails: a variable can occur idly (v0 = v0)585 ok &= len(family) == 53925 and n_dep == [31839, 13872, 7566, 648] and n_idle == 21903586 # every formula of length <= 9 over M_2 in four variables, written out. The enumeration's truth table and free variables are587 # first checked against the independent reader of the written formula, under every assignment; then the lemma.588 forms, swap = formulas_M2(4, 9); n2 = n2_dep = 0; by_free = [0] * 5589 for L, fs in forms.items():590 for tab, fv, tx in fs:591 n2 += 1592 reads = [read_formula(tx, 0, {VARS[i]: (a >> i) & 1 for i in range(4)}) for a in range(16)]593 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))594 free = reads[0][2]595 ok &= free == frozenset(VARS[i] for i in range(4) if (fv >> i) & 1) # the free variables, read off the written formula596 dep = [i for i in range(4) if swap(tab, i) != tab]597 ok &= all(VARS[i] in free for i in dep) # a coordinate read is a variable occurring free598 n2_dep += bool(dep); by_free[len(free)] += 1599 ok &= n2 == 17820 and n2_dep == 8820 and by_free == [4604, 8344, 4128, 720, 24]600 # 25:F1 (p25023)601 R.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 formulas over M_3 and on all formulas of length <= 9 over M_2 in four variables, each written out and read back by an independent reader; the converse fails", ok,602 "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)" + "; " + (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}"))603604 # D2 the no-compression theorem on built instances605 ok = True; n_maps = 0606 def graph_depends(d, N):607 """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."""608 rel = lambda u, v: v == d[u]609 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)]610 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)]611 return dep_u + dep_v612 for N in (1, 2, 3):613 for k, d in enumerate(itertools.permutations(range(1 << N))): # the injective maps on M_2^N (N = 3: every 37th of the 40320)614 if N == 3 and k % 37: continue615 n_maps += 1; ok &= all(graph_depends(d, N)) # the diagonal relation depends on every one of its 2N coordinates616 ok &= graph_depends((0,) * (1 << N), N) == [False] * N + [True] * N # the control: the graph of a constant map reads no coordinate of u617 ok &= n_maps == 2 + 24 + 1090618 # 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 N2619 # (N2 = N: the theorem's template; N2 > N: the scales split). Diag ranges over EVERY formula of length <= 9 whose relation is the620 # graph of an injective map u -> v, theta over EVERY formula of length <= 5 in v alone that reads each coordinate of v.621 built = []; n_delta = 0; census = {}; least_occ = (99, 99)622 for N, N2 in ((1, 1), (2, 2), (1, 2)):623 V = N + N2; forms, swap = formulas_M2(V, 9); u_side, v_side = 1 << N, 1 << N2624 u_names, v_names = VARS[:N], VARS[N:V]625 def as_map(tab):626 """The injective map d: M_2^N -> M_2^N2 whose graph the table is, or None."""627 d = []628 for u in range(u_side):629 vs = [v for v in range(v_side) if (tab >> (u + u_side * v)) & 1]630 if len(vs) != 1: return None631 d.append(vs[0])632 return tuple(d) if len(set(d)) == u_side else None633 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]634 thetas = [(L, tx) for L, fs in forms.items() if L <= 5 for tab, fv, tx in fs635 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 variable636 ok &= len(diags) > 0 and len(thetas) > 0637 for Ld, dtx, d in diags:638 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 variables639 for Lt, ttx in thetas:640 ok &= set(v_names) <= {c for c in ttx if c in VARS} and Lt >= N2 # the written theta mentions every coordinate of v641 for Ld, dtx, d in diags:642 for Lt, ttx in thetas:643 delta = "".join("E" + x for x in v_names) + "(" + dtx + "&" + ttx + ")" # delta(u) = Ev (Diag(u, v) & theta(v)), written out644 n_delta += 1645 for u in range(u_side):646 got = read_formula(delta, 0, {u_names[i]: (u >> i) & 1 for i in range(N)})647 want = read_formula(ttx, 0, {v_names[i]: (d[u] >> i) & 1 for i in range(N2)})648 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 u649 occ_v = min(delta.count(x) for x in v_names); occ_u = min(delta.count(x) for x in u_names)650 ok &= occ_v >= 3 and occ_u >= 1 # each coordinate of v is named three times (block, Diag, theta), each of u once651 least_occ = (min(least_occ[0], occ_v), min(least_occ[1], occ_u))652 ok &= len(delta) == 2 * N2 + 3 + Ld + Lt # the written length: the block, the conjunction, Diag, theta653 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-tuple654 census[(N, N2)] = (len(diags), min(L for L, _, _ in diags), len(thetas))655 built.append(f"(N, N2) = ({N}, {N2}): {len(diags)} formulas define a diagonal relation (shortest {census[(N, N2)][1]} symbols), {len(thetas)} formulas theta")656 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 == 2880657 ok &= least_occ == (3, 1) # the counts 3 and 1 are attained658 # 25:F2 (p25024)659 R.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 sample at N = 3), every defining formula of length <= 9 mentions all 2N variables, and each diagonal formula Ev (Diag & theta) names every coordinate of v three times and of u once, so its code is no N-tuple", ok,660 "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" + "; " + (f"{n_maps} injective maps; " + "; ".join(built) + f"; {n_delta} diagonal formulas written out"))661662 # D3 density and the name count of the template663 ok = True664 n_cases = n_codings = 0665 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 cases666 src = list(itertools.product(range(a), repeat=n)); n_states = m ** k667 assert n_states < len(src) and n_states ** len(src) <= 400000668 n_cases += 1669 for f in itertools.product(range(n_states), repeat=len(src)):670 n_codings += 1; ok &= len(set(f)) < len(src)671 ok &= n_cases == 5 and n_codings == 3 ** 4 + 2 ** 3 + 4 ** 8 + 4 ** 9 + 5 ** 8 == 718394672 n_inj = sum(1 for f in itertools.product(range(4), repeat=4) if len(set(f)) == 4)673 ok &= n_inj == 24 # the control: at m^k = a^n = 4 injective codings exist674 # the digit bound. d is the digit count of m in base a: a^(d-1) <= m < a^d. The longest strings an injective coding675 # by k-tuples reaches have the largest n with a^n <= m^k letters, and (d-1)k <= n < dk.676 T_EXACT.clear(); n_pairs = 0677 for a, top in ((2, 500), (3, 400), (4, 400), (5, 700)): # every structure in a range, in exact integers678 for m in range(a, top + 1):679 d = 1680 while a ** d <= m: d += 1681 upto = 2 * 6 * a ** (d // 3 + 1) # every k up to twice the bound (i) of D5682 fit = fit_table(m, a, d, upto)683 for k in range(1, upto + 1):684 n_pairs += 1; n = fit[k]685 ok &= a ** n <= m ** k < a ** (n + 1) and (d - 1) * k <= n < d * k686 T_EXACT[(a, m)] = (d, fit)687 ok &= len(T_EXACT) == 499 + 398 + 397 + 696 == 1990 and n_pairs == 425112688 # the name count of the template, in integers. With k coordinates in v and k1 in u the diagonal formula names k + k1689 # distinct variables, each coordinate of v three times and each of u once (D2). Every ordering of k + k1 names chosen690 # among the k + k1 + 2 shortest, the first k of an ordering given to v: the least cost in delta is delta_names, the691 # least in lambda (a one-symbol term in each place of u) is lambda_names, and one ordering attains both.692 n_ord = 0; least = []; pairs = ((1, 1), (2, 2), (3, 3), (1, 2), (2, 1), (1, 3), (3, 1), (2, 3), (3, 2))693 for a in (2, 3):694 for k, k1 in pairs:695 pool = [L for L in range(1, 6) for _ in range(a ** L)][:k + k1 + 2]696 costs = set()697 for c in itertools.combinations(range(len(pool)), k + k1):698 for p in itertools.permutations([pool[x] for x in c]):699 n_ord += 1; costs.add((3 * sum(p[:k]) + sum(p[k:]), 3 * sum(p[:k]) + k1))700 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)701 ok &= (delta_names(k, k1, a), lambda_names(k, k1, a)) in costs702 least.append((min(x for x, y in costs), min(y for x, y in costs)))703 ok &= n_ord == 52824704 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)]705 # 25:F4 (p25048)706 R.check("D3", "Density: an injective coding of the a^n strings into k-tuples needs m^k >= a^n, so n < dk for d the digit count of m in base a (1990 structures, a = 2..5), and the diagonal formula's least name costs in delta and in lambda are 2c(k) + c(k+k1) and 3c(k) + k1 (a = 2, 3; k, k1 <= 3)", ok,707 "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" + "; " + (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)))))708709 # D4 quotation exceeds mention: every formula of length <= 9 in six variables710 ok = True711 forms, swap = formulas_M2(6, 9); n6 = 0; least = {}; most = {}; hist = [0] * 7712 for L, fs in forms.items():713 for tab, fv, tx in fs:714 n6 += 1715 r = read_formula(tx, 0, {})716 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)717 fl = [i for i in range(6) if (fv >> i) & 1]718 for bits in range(1, 1 << len(fl)): # every assignment to the free variables (the others 0)719 a = sum(1 << i for j, i in enumerate(fl) if (bits >> j) & 1)720 ok &= read_formula(tx, 0, {VARS[i]: 1 for i in fl if (a >> i) & 1})[0] == bool((tab >> a) & 1)721 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 free722 k = sum(1 for i in range(6) if swap(tab, i) != tab) # the number of coordinates the truth depends on723 hist[k] += 1724 ok &= k < L # fewer than the formula has symbols725 least[k] = min(least.get(k, L), L); most[L] = max(most.get(L, 0), k)726 ok &= n6 == 65600 and least == {0: 3, 1: 3, 2: 3, 3: 7, 4: 9} # the shortest formula reading k coordinates727 ok &= hist == [28430, 16320, 16170, 4320, 360, 0, 0] # the formulas by the number of coordinates read728 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 four729 # 25:F3 (p25025), 25:G6 (p25033)730 R.check("D4", "Quotation exceeds mention: over all formulas of length <= 9 over M_2 in six variables the truth depends on fewer coordinates than the formula has symbols; the shortest formulas reading 2, 3, 4 coordinates have 3, 7, 9 symbols, and none of at most 9 symbols reads five", ok,731 "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" + "; " + (f"{n6} formulas; least length by coordinates read: {least}; most coordinates read by length: {most}"))732733 # D5 the threshold lies inside the count. An instance with k coordinates in v and k1 in u needs lambda_names < dk and734 # delta_names < d k1 (admits). k*(M) is the largest k for which some k1 admits; it depends on a and d alone.735 ok = True736 n_mono = 0; ends = []737 for a in (2, 3, 4, 5): # one scale: N(k)/k does not decrease, N(k) = delta_names(k, k)738 for k in range(1, 20001):739 n_mono += 1; ok &= delta_names(k + 1, k + 1, a) * k >= delta_names(k, k, a) * (k + 1)740 ends.append(delta_names(20001, 20001, a))741 ok &= n_mono == 80000 and ends == [1029078, 686271, 556370, 486813]742 kstar = {}; n_direct = n_bound = n_scan = n_scan_k = n_scan_k1 = 0; left = []; inside = []743 for a in range(2, 41): # by digit count: every alphabet a <= 40, every d >= 1 with a^d <= 2^400744 d = 1745 while a ** d <= 2 ** 400:746 n_direct += 1747 b3, b4 = 6 * a ** (d // 3 + 1), 6 * a ** (d // 4 + 1) # the bounds (i)748 k_one = last_k(d, a, strict=True) # one scale: the largest k with N(k) < dk749 ok &= k_one < b4750 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 on751 by_bound = d * b3 <= a ** (d - 1)752 scanned = d <= 12 and b3 <= 10000753 if scanned: # k*(M) by a scan of every k below twice the bound754 scan = range(1, 2 * b3); n_scan += 1; n_scan_k += len(scan); good = []; one = 0755 for k in scan:756 reach = d * k - 1 - 3 * name_cost(k, a) # lambda's inequality allows the k1 <= reach757 ok &= not admits(k, max(reach, 0) + 1, d, a) # and no further k1758 for k1 in range(1, reach + 1): # every such k1759 n_scan_k1 += 1760 if admits(k, k1, d, a):761 if not good or good[-1] != k: good.append(k)762 if k1 == k: one = k763 K = max(good, default=0); kstar[(a, d)] = K764 ok &= good == list(range(1, K + 1)) and K < b3 # an initial segment, ending below the bound765 ok &= d * K < a ** (d - 1) # directly: t(M) = d k*(M) < a^(d-1) <= m766 inside.append((Fraction(d * K, a ** (d - 1)), a, d))767 ok &= (K == 0) == (d <= 4) and one == k_one <= K # the one-scale threshold found both ways, at most k*(M)768 if d >= 13: n_bound += 1; ok &= by_bound769 elif d >= 5 and not by_bound: left.append((a, d))770 ok &= scanned or (d >= 5 and by_bound) # every case is decided by the scan or by the bound771 d += 1772 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)773 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)]774 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]775 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]776 # the structures of D3, in exact integers: every instance the names leave open, a^n <= m^k and a^n1 <= m^k1 exactly777 n_inst = n_one = n_try = n_k = n_below = 0; share = []; slack = None778 for (a, m), (d, fit) in T_EXACT.items():779 K = kstar[(a, d)]; t = d * K780 ok &= t < m and (K == 0) == (m < a ** 4)781 one = 0782 for k in range(1, len(fit)): # every k up to twice the bound783 n_k += 1784 reach = fit[k] - 3 * name_cost(k, a) # every k1 with lambda's symbols within the reach of k-tuples: k1 <= reach785 ok &= reach <= len(fit) - 1 # the table covers them all786 for k1 in range(1, reach + 1):787 n_try += 1788 if delta_names(k, k1, a) <= fit[k1]: # an instance left open: delta's symbols within the reach of k1-tuples789 n_inst += 1; one += k1 == k790 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)791 slack = t - fit[k] if slack is None else min(slack, t - fit[k])792 n_one += one793 for k in range(1, a ** ((d - 1) // 4) // 2 + 1): # below, at one scale: each of these k is left open794 n_below += 1; ok &= lambda_names(k, k, a) <= delta_names(k, k, a) <= fit[k]795 share.append((Fraction(t, m), a, m))796 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)797 # 25:F6 (p25047)798 R.check("D5", "The threshold lies inside the count: k*(M) is the largest k that some k1 admits in digit form and t(M) = d k*(M), with k*(M) < 6a^(floor(d/3)+1) and t(M) < a^(d-1) <= m at every a <= 40 and a^d <= 2^400 (by scan where d <= 12, by the bound beyond), and in exact integers no instance codes lambda at a length n >= t(M) (the 1990 structures of D3)", ok,799 "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))" + "; " + (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"))800# ------------------------------------------------------------------------------------------------------------801# block E: fragment truth (25:G4, G5) — Section 5.3.802# E1: the prefix simulation — the sentence with the uniform prefix Ay1 Ex1 … Ayd Exd and the clause x_i = y_i at the803# universal positions, evaluated as written, decides what the coded prefix Q1 … Qd decides: every pattern against EVERY804# matrix over M_2 (depth <= 3) and M_3 (depth <= 2), and against a matrix family over M_5. E2: the guessed labels — a805# labelling consistent with the position-local clauses and rooted true exists exactly for the well-formed true codes, and806# it is unique; and the composition of the label layers with the pairing prefix agrees with direct truth on every string807# of length <= 6 of a small language, conjunctions included.808@R.block("E", BLOCK["E"])809def block_E():810 """Block E — fragment truth: the pairing prefix and the guessed labels (EXACT): E1–E2."""811 def paired(m, pattern, matrix):812 """The sentence of the lemma's right-hand side, evaluated by the shared evaluator: the uniform prefix Ay1 Ex1 … Ayd Exd over813 the matrix [ AND_{i: Q_i = A} x_i = y_i & psi(x) ], the copy clauses standing in the matrix."""814 d = len(pattern)815 def mat(v): # v = (y1, x1, …, yd, xd)816 ys, xs = v[0::2], v[1::2]817 return all(xs[i] == ys[i] for i in range(d) if pattern[i] == "A") and matrix(tuple(xs))818 return decide(m, "AE" * d, mat)819 ok = True; n = 0; det = []820 for m, dmax in ((2, 3), (3, 2)):821 for d in range(1, dmax + 1):822 pts = list(itertools.product(range(m), repeat=d))823 for bits in range(2 ** len(pts)): # every matrix: every subset of M^d824 S = {pt for k, pt in enumerate(pts) if (bits >> k) & 1}825 for pat in itertools.product("AE", repeat=d):826 n += 1827 ok &= decide(m, "".join(pat), lambda v: v in S) == paired(m, pat, lambda v: v in S)828 det.append(f"M_{m}: every matrix to depth {dmax}")829 n5 = 0830 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 S831 for cs in ((1, 2), (3, 1), (1, 1), (2, 3), (4, 1), (0, 1)):832 for smask in range(32):833 S = {t for t in range(5) if (smask >> t) & 1}834 mat = lambda v, cs=cs, S=S: sum(c * x for c, x in zip(cs, v)) % 5 in S835 n5 += 1; ok &= decide(5, "".join(pat), mat) == paired(5, pat, mat)836 ok &= n == 4184 and n5 == 768837 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 clauses838 for S in ({(0, 0)}, {(0, 1), (1, 0)}) for pat in itertools.product("AE", repeat=2)) # the uniform prefix decides something else839 ok &= wrong > 0840 # 25:G4 (p25031)841 R.check("E1", "The prefix simulation: the sentence Ay1 Ex1 ... Ayd Exd [x_i = y_i at the coded universal positions & psi(x)] agrees with Q1 z1 ... Qd zd psi(z) on every pattern and matrix over M_2 (depth <= 3) and M_3 (depth <= 2) and on a family over M_5; without the copy clauses the two differ", ok,842 "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" + "; " + (f"{n} exhaustive instances ({'; '.join(det)}) + {n5} over M_5"))843844 # E2 the guessed labels: propositional layer, then the composition with the prefix and the environments845 def parse(s, i=0):846 """Polish notation over T, F, N (negation), C (conjunction): (value, next position) or None."""847 if i >= len(s): return None848 c = s[i]849 if c in "TF": return (c == "T", i + 1)850 if c == "N":851 r = parse(s, i + 1); return None if r is None else (not r[0], r[1])852 if c == "C":853 r1 = parse(s, i + 1)854 if r1 is None: return None855 r2 = parse(s, r1[1]); return None if r2 is None else (r1[0] and r2[0], r2[1])856 return None857 def direct(s):858 r = parse(s); return None if r is None or r[1] != len(s) else r[0]859 def consistent(s, ends, vals):860 """The position-local clauses: ends[i] = the end of the subformula opening at i, vals[i] = its value."""861 n = len(s)862 for i, c in enumerate(s):863 if c in "TF":864 if not (ends[i] == i + 1 and vals[i] == (c == "T")): return False865 elif c == "N":866 if i + 1 >= n or not (ends[i] == ends[i + 1] and vals[i] == (not vals[i + 1])): return False867 elif c == "C":868 if i + 1 >= n: return False869 j = ends[i + 1]870 if j >= n or not (ends[i] == ends[j] and vals[i] == (vals[i + 1] and vals[j])): return False871 return True872 def labellings(s, root=None):873 n = len(s); out = 0874 for ends in itertools.product(range(1, n + 1), repeat=n):875 if ends[0] != n: continue876 for vals in itertools.product((False, True), repeat=n):877 if root is not None and vals[0] != root: continue878 out += consistent(s, ends, vals)879 return out880 ok = True; n_codes = n_wf = 0881 for L in range(1, 5):882 for tup in itertools.product("TFNC", repeat=L):883 s = "".join(tup); n_codes += 1; d = direct(s)884 if d is None: ok &= labellings(s) == 0 # an ill-formed code admits no labelling885 else:886 n_wf += 1887 ok &= labellings(s) == 1 and labellings(s, True) == (1 if d else 0) # exactly the labelling of its parse tree; rooted true iff true888 ok &= (n_codes, n_wf) == (340, 24)889 def backward(s):890 """The one candidate labelling, computed right to left from the clauses; None if a clause cannot be met."""891 n = len(s); ends = [0] * n; vals = [False] * n892 for i in range(n - 1, -1, -1):893 c = s[i]894 if c in "TF": ends[i], vals[i] = i + 1, c == "T"895 elif c == "N":896 if i + 1 >= n: return None897 ends[i], vals[i] = ends[i + 1], not vals[i + 1]898 else:899 if i + 1 >= n or ends[i + 1] >= n: return None900 j = ends[i + 1]; ends[i], vals[i] = ends[j], vals[i + 1] and vals[j]901 return (vals[0] if ends[0] == n else None)902 n_long = 0903 for L in range(1, 9):904 for tup in itertools.product("TFNC", repeat=L):905 s = "".join(tup); n_long += 1906 b = backward(s); d = direct(s)907 ok &= (b is None) == (d is None) and b == d # the pass labels exactly the well-formed codes, with their values908 ok &= n_long == 87380909 # 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 d910 # 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`911 # (x_i = x_j), the indices written as the tokens 0, 1. Truth is computed twice, by two separate routines.912 ARITY = {"z": 1, "t": 1, "e": 2}913 def d_matrix(code, i, env, d):914 """Direct: parse the matrix from position i and evaluate it; (value, next position), or None if ill-formed."""915 if i >= len(code): return None916 c = code[i]917 if c in ARITY:918 ix = code[i + 1:i + 1 + ARITY[c]]919 if len(ix) < ARITY[c] or any(ch not in "01" or int(ch) >= d for ch in ix): return None920 x = [env[int(ch)] for ch in ix]921 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])922 if c == "N":923 r = d_matrix(code, i + 1, env, d); return None if r is None else (not r[0], r[1])924 if c == "C":925 r1 = d_matrix(code, i + 1, env, d)926 if r1 is None: return None927 r2 = d_matrix(code, r1[1], env, d); return None if r2 is None else (r1[0] and r2[0], r2[1])928 return None929 def d_truth(code):930 d = 0931 while d < len(code) and code[d] in "AE": d += 1932 if d not in (1, 2): return None933 wf = d_matrix(code, d, (0, 0), d)934 if wf is None or wf[1] != len(code): return None935 return decide(3, code[:d], lambda v: d_matrix(code, d, tuple(v) + (0,) * (2 - d), d)[0])936 def clause(code, d, q, ends):937 """The position-local clause on the parse label of matrix position d + q (ends[q]: the end of the subformula opening there).938 It refers to labels at positions to its right only."""939 n = len(code); i = d + q; c = code[i]; e = ends[q]940 if q == 0 and e != n: return False # the root: the matrix ends where the code ends941 if c in "zt": return i + 1 < n and code[i + 1] in "01" and e == i + 2942 if c == "e": return i + 2 < n and code[i + 1] in "01" and code[i + 2] in "01" and e == i + 3943 if c == "N": return i + 1 < n and code[i + 1] in "NCzte" and e == ends[q + 1]944 if c == "C":945 if not (i + 1 < n and code[i + 1] in "NCzte"): return False946 j = ends[q + 1]947 return j < n and code[j] in "NCzte" and e == ends[j - d]948 if c in "01": # an index token: owned by the atom before it, its own labels inert949 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")950 return own and e == i + 1951 return False # a quantifier token inside the matrix952 def structural(code, d, ends):953 """The clauses on the ends (the parse labels), at every matrix position."""954 return ends[0] == len(code) and all(clause(code, d, q, ends) for q in range(len(code) - d))955 def valued(code, d, ends, vals, x):956 """The clauses on the values, under the quantified values x: an atom's clause resolves its coded index against x by a case over957 the d candidates (the linkage clause)."""958 for q in range(len(code) - d):959 i = d + q; c = code[i]; v = vals[q]960 if c == "z":961 if not any(code[i + 1] == str(j) and v == (x[j] == 0) for j in range(d)): return False962 elif c == "t":963 if not any(code[i + 1] == str(j) and v == ((x[j] + x[j]) % 3 == 1) for j in range(d)): return False964 elif c == "e":965 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 False966 elif c == "N":967 if v != (not vals[q + 1]): return False968 elif c == "C":969 if v != (vals[q + 1] and vals[ends[q + 1] - d]): return False970 elif v: return False # an index token carries the inert value971 return True972 def parses(code, d, search):973 """The labellings of the ends that satisfy the structural clauses: by search over all of them, or the one candidate of the974 right-to-left pass, checked against the clauses."""975 n = len(code); k = n - d976 if search: return [e for e in itertools.product(range(d + 1, n + 1), repeat=k) if structural(code, d, e)]977 ends = [0] * k978 for q in range(k - 1, -1, -1):979 i = d + q; c = code[i]980 if c in "zt": ends[q] = i + 2981 elif c == "e": ends[q] = i + 3982 elif c in "01": ends[q] = i + 1983 elif c == "N": ends[q] = ends[q + 1] if q + 1 < k else 0984 elif c == "C":985 j = ends[q + 1] if q + 1 < k else 0986 ends[q] = ends[j - d] if d <= j < n else 0987 return [tuple(ends)] if all(d < e <= n for e in ends) and structural(code, d, tuple(ends)) else []988 def parses_bt(code, d):989 """EVERY labelling of the ends that satisfies the structural clauses, by backtracking from the right: the clause at a position990 refers only to labels on its right, so a partial labelling is extended by every value that meets the clause there."""991 n = len(code); k = n - d; out = []992 def rec(q, ends):993 if q < 0: out.append(tuple(ends[x] for x in range(k))); return994 for e in range(d + 1, n + 1):995 ends[q] = e996 if clause(code, d, q, ends): rec(q - 1, ends)997 ends.pop(q, None)998 if k > 0: rec(k - 1, {})999 return out1000 def values(code, d, ends, x, search):1001 """The labellings of the values consistent with the clauses under x."""1002 k = len(code) - d1003 if search: return [v for v in itertools.product((False, True), repeat=k) if valued(code, d, ends, v, x)]1004 vals = [False] * k1005 for q in range(k - 1, -1, -1):1006 i = d + q; c = code[i]1007 if c == "z": vals[q] = x[int(code[i + 1])] == 0 if int(code[i + 1]) < d else False1008 elif c == "t": vals[q] = (2 * x[int(code[i + 1])]) % 3 == 1 if int(code[i + 1]) < d else False1009 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 False1010 elif c == "N": vals[q] = not vals[q + 1]1011 elif c == "C": vals[q] = vals[q + 1] and vals[ends[q + 1] - d]1012 return [tuple(vals)] if valued(code, d, ends, tuple(vals), x) else []1013 def l_truth(code, mode):1014 """Truth by guessed labels: a prefix length d, checked against the token classes; the parse labels; and, under the uniform1015 pairing prefix whose copy clauses are read off the coded prefix, value labels rooted true. mode "all": every labelling of1016 ends and values is tried (the ends over the full product); "search": the same, the ends by backtracking; "pass": the one1017 candidate of the right-to-left pass, checked against the clauses."""1018 n = len(code)1019 for d in (1, 2):1020 if not (d < n and all(code[k] in "AE" for k in range(d)) and code[d] not in "AE"): continue1021 ps = parses(code, d, True) if mode == "all" else parses_bt(code, d) if mode == "search" else parses(code, d, False)1022 rooted = {} # the matrix of the paired sentence at x: some labelling is rooted true1023 def matrix(x): # (it reads x alone, so each x is labelled once)1024 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"))1025 return rooted[x]1026 if paired(3, code[:d], matrix): return True1027 return False1028 n_comp = n_comp_wf = n_true = n_pairs = 01029 for L in range(1, 6): # every string of length <= 5: the labellings over the full product1030 for tup in itertools.product("AENCzte01", repeat=L):1031 code = "".join(tup); n_comp += 11032 want = d_truth(code); got = l_truth(code, "all")1033 ok &= got == (want is True) == l_truth(code, "pass") # the labelled truth holds exactly for the well-formed true codes1034 n_comp_wf += want is not None; n_true += want is True1035 for d in (1, 2): # and the backtracking search finds exactly the labellings of the full product1036 if d < L: n_pairs += 1; ok &= sorted(parses_bt(code, d)) == sorted(parses(code, d, True))1037 ok &= (n_comp, n_comp_wf, n_true, n_pairs) == (66429, 64, 36, 132759)1038 n6 = n6_wf = n6_true = 01039 for tup in itertools.product("AENCzte01", repeat=6): # every string of length 6, the labellings by the complete search:1040 code = "".join(tup); n6 += 1 # the shortest codes with a conjunction are among them1041 want = d_truth(code); ok &= l_truth(code, "search") == (want is True)1042 n6_wf += want is not None; n6_true += want is True1043 ok &= n6 == 531441 and 0 < n6_true < n6_wf1044 ok &= d_truth("ECCz0z0t0") is False and not l_truth("ECCz0z0t0", "search") # a false conjunction is not labelled true,1045 ok &= d_truth("ECz0z0z0") is None and not l_truth("ECz0z0z0", "search") # nor a conjunction followed by a stray atom1046 def matrices(size, d, memo={}):1047 """Every well-formed matrix of exactly `size` tokens over d variables."""1048 if (size, d) not in memo:1049 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 []1050 if size > 2: out += ["N" + m for m in matrices(size - 1, d)]1051 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)]1052 memo[(size, d)] = out1053 return memo[(size, d)]1054 n_big = n_big_true = n_edit = n_edit_wf = 01055 for d in (1, 2): # every well-formed code with a matrix of at most 7 tokens,1056 for pref in itertools.product("AE", repeat=d): # by the complete search and by the pass1057 for size in range(2, 8):1058 for mat in matrices(size, d):1059 code = "".join(pref) + mat; n_big += 11060 want = d_truth(code); ok &= want is not None and l_truth(code, "search") == want == l_truth(code, "pass"); n_big_true += want1061 eds = [code[:pos] + tok + code[pos + 1:] for pos in range(len(code)) for tok in "AENCzte01" if tok != code[pos]]1062 eds += [code + tail for tail in ("z0", "t0", "0", "N")] # every one-token edit, and four extensions: an ill-formed code is rejected1063 for ed in eds:1064 n_edit += 1; w2 = d_truth(ed); ok &= l_truth(ed, "search") == (w2 is True); n_edit_wf += w2 is not None1065 ok &= (n_big, n_big_true) == (1540, 654) and n_edit == 108048 and 0 < n_edit_wf < n_edit1066 # 25:G5 (p25032)1067 R.check("E2", "Fragment truth by guessed labels on small languages: a consistent labelling exists exactly for the well-formed codes, is unique and is rooted true exactly for the true ones, on the propositional layer (codes of length <= 8) and with the variable indices coded as data, against a direct evaluator over M_3", ok,1068 "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" + "; " + (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)"))1069# ------------------------------------------------------------------------------------------------------------1070# block F: second-order decidability and the trichotomy's middle cell (25:H2, H5) — Section 6.1071# F1: over a finite domain a second-order quantifier over k-ary relations ranges over the 2^(m^k) subsets of M^k, so1072# second-order sentences are decided by enumeration: the counts for five (m, k), and four sentences decided on |X| = 3.1073# F2: the theory "at least n elements, for every n" with a free unary predicate P — each finite part of it has models1074# 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; the1075# theory of a finite model decides every sentence of the sample.1076@R.block("F", BLOCK["F"])1077def block_F():1078 """Block F — second-order decidability and the trichotomy's middle cell (EXACT): F1–F2."""1079 ok = True; det = []1080 for m, k in ((2, 1), (2, 2), (3, 1), (3, 2), (2, 3)):1081 pts = list(itertools.product(range(m), repeat=k))1082 rels = sum(1 for _ in itertools.product((0, 1), repeat=len(pts))) # every k-ary relation, enumerated1083 ok &= rels == 2 ** (m ** k); det.append(f"(m,k)=({m},{k}): {rels}")1084 X = range(3); pairs = [(i, j) for i in X for j in X]1085 found = {"order": False, "inj_not_onto": False, "all_have_min": True, "equiv_classes": set()}1086 n = n_fun = n_injf = n_onto = n_bij = 01087 for bits in itertools.product((0, 1), repeat=9):1088 Rel = {pq for pq, b in zip(pairs, bits) if b}; n += 11089 functional = all(sum((i, j) in Rel for j in X) == 1 for i in X)1090 if functional:1091 n_fun += 11092 injective = not any((i, j) in Rel and (i2, j) in Rel for j in X for i in X for i2 in X if i != i2) # no value is taken twice1093 onto = all(any((i, j) in Rel for i in X) for j in X) # every element is a value1094 n_injf += injective; n_onto += onto; n_bij += injective and onto1095 if injective and not onto: found["inj_not_onto"] = True # an injective function that is not onto: the scan finds none1096 irr = all((i, i) not in Rel for i in X)1097 tra = all((i, k2) in Rel for (i, j) in Rel for (j2, k2) in Rel if j == j2)1098 tot = all((i, j) in Rel or (j, i) in Rel for i in X for j in X if i != j)1099 if irr and tra and tot:1100 found["order"] = True1101 for sub in itertools.product((0, 1), repeat=3): # second-order over subsets: every non-empty subset has a least element1102 S = [x for x in X if sub[x]]1103 if S: found["all_have_min"] &= any(all(x == y or (x, y) in Rel for y in S) for x in S)1104 refl = all((i, i) in Rel for i in X); sym = all((j, i) in Rel for (i, j) in Rel)1105 if refl and sym and tra: found["equiv_classes"].add(frozenset(frozenset(j for j in X if (i, j) in Rel) for i in X))1106 ok &= n == 512 and found["order"] and not found["inj_not_onto"] and found["all_have_min"] and len(found["equiv_classes"]) == 51107 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 61108 # 25:H2 (p25036), 25:H4 (p25038)1109 R.check("F1", "Second-order decidability on a finite domain: a quantifier over k-ary relations ranges over 2^(m^k) relations (five (m, k)), and over all binary relations on 3 elements a strict total order exists, the injective functions are the onto ones, and the equivalence relations are the partitions", ok,1110 "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" + "; " + ("; ".join(det)))11111112 ok = True; det = []1113 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 elements1114 n_struct = 01115 for N in range(1, 5): # the first N axioms, over every structure (domain of s <= 5 elements, a unary predicate P)1116 seen = {}1117 for s in range(1, 6):1118 sat = all(at_least(s, n) for n in range(1, N + 1))1119 ok &= sat == (s >= N) # the models of the first N axioms: the structures of at least N elements1120 for P in itertools.product((0, 1), repeat=s):1121 n_struct += 11122 if sat: seen.setdefault(s, set()).add(decide(s, "E", lambda v: P[v[0]] == 1)) # the value of Ex P(x) in the model1123 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 negation1124 ok &= not all(at_least(N, n) for n in range(1, N + 2)) # no structure of N elements satisfies the next axiom1125 for s in seen: # the completing axiom Ax not P(x) leaves one value1126 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}1127 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")1128 ok &= n_struct == 4 * (2 + 4 + 8 + 16 + 32) == 2481129 for p in (2, 3, 5): # cell (iii): the theory of a finite model decides every sentence of the sample1130 ok &= all(decide(p, pat, mat) == want for _, pat, mat, want in sentences(p))1131 # 25:H5 (p25039)1132 R.check("F2", "The trichotomy's middle cell on its finite parts: the first N axioms 'at least n elements' (N <= 4), decided over all structures of at most 5 elements with a unary P, decide neither Ex P(x) nor its negation, no structure of N elements satisfies N+1 of them, and the theory of a finite model gives every sampled sentence its value", ok,1133 "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" + "; " + ("; ".join(det)))11341135# ------------------------------------------------------------------------------------------------ block G1136# G1 model-checks the written formulas of (1)-(4) on small prime fields, exhaustively. G2 model-checks the written Diag1137# on F_257 (4 symbols, 3 per element) against the substitution computed from its definition, and builds the instance as1138# strings. G3 builds it with the longest theta. At the scale of the instance no model check is possible; there the1139# fixed point rests on (1)-(6).1140@R.block("G", BLOCK["G"])1141def block_G():1142 """Block G — the window below the threshold (EXACT): G1–G3; the printer and the reader run in a deep thread."""1143 deep(_block_G)11441145def _block_G():1146 dd = dense(); g = dd.Gen(); V, Ev, show = dd.V, dd.Ev, dd.show1147 x0, x1, x2 = "x20", "x21", "x22"1148 ok = True; det = []1149 n = 01150 for p in dd.primes_upto(131): # Int_J on every prime field up to 1311151 J = 01152 while (1 << J) <= p:1153 f = g.Int(V(x0), J); e = Ev(p)1154 ok &= {x for x in range(p) if e.ev(f, {x0: x})} == set(range(1 << J)); n += 1; J += 11155 ok &= n == 184 and all(len(show(g.Int(V(x0), J))) == 50 * J + 29 for J in range(8))1156 det.append(f"Int_J on {n} pairs (p, J), length 50J + 29")1157 n = 01158 for p, E in ((11, 2), (19, 3), (37, 4), (67, 5), (131, 6), (257, 7)): # inrange, every N <= 2^E, 2^(E+1) < p1159 e = Ev(p)1160 for N in range(0, (1 << E) + 1):1161 f = g.inrange(V(x0), g.K(N), E)1162 ok &= {x for x in range(p) if e.ev(f, {x0: x})} == set(range(N)); n += 11163 ok &= n == 258; det.append(f"inrange on {n} pairs (p, N)")1164 n = 01165 for p in (11, 19, 37): # Pow on all of F_p^21166 for bb in (1, 2, 4, 5):1167 for ee in (0, 1, 2, 3):1168 f = g.Pow(V(x0), V(x1), bb, ee); e = Ev(p)1169 for r in range(p):1170 for z in range(p):1171 ok &= e.ev(f, {x0: r, x1: z}) == (r < (1 << ee) and z == pow(1 << bb, r, p)); n += 11172 ok &= n == 29616; det.append(f"Pow on {n} triples (p, r, z)")1173 n = 01174 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^31175 assert (1 << (bb * nd + 1)) < p and nd <= (1 << ee) and (1 << (ee + 1)) <= p1176 f = g.Dig(V(x0), V(x1), V(x2), bb, nd, ee); e = Ev(p); beta = 1 << bb1177 for y in range(p):1178 for r in range(p):1179 for s in range(p):1180 ok &= e.ev(f, {x0: y, x1: r, x2: s}) == (y < beta ** nd and r < nd and s == (y // beta ** r) % beta); n += 11181 ok &= n == 110827; det.append(f"Dig on {n} triples (y, r, s), five cases")1182 L = lambda bb, nd, ee: len(show(g.Dig(V(x0), V(x1), V(x2), bb, nd, ee)))1183 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 + c01184 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))1185 det.append(f"length of Dig = 50bn + 50b + {ce}e + {c0}")1186 n = 01187 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),1188 (7, lambda: g.Pow(V(x0), V(x1), 1, 1), 2), (11, lambda: g.Pow(V(x0), V(x1), 2, 2), 2),1189 (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)):1190 f = mk(); e1 = Ev(p); e2 = Ev(p, naive=True) # the pruned checker against the plain one1191 for vals in itertools.product(range(p), repeat=ar):1192 env = dict(zip((x0, x1, x2), vals)); ok &= e1.ev(f, dict(env)) == e2.ev(f, dict(env)); n += 11193 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}1194 ok &= n == 2867; det.append(f"pruned and plain checker agree on {n} assignments")1195 # 25:F7 (p25049)1196 R.check("G1", "Decoders over a prime field as written formulas, model-checked on small fields: Int_J(x) <=> x < 2^J (p <= 131, 2^J <= p), inrange(x, N) <=> x < N, Pow(r, z) <=> r < 2^e and z = (2^b)^r, Dig(y, r, s) <=> s is digit r of y, each of length linear in its parameters; the pruned model checker agrees with the plain one", ok,1197 "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; 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); 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)" + "; " + ("; ".join(det)))11981199 # Diag as a written formula on a small field: 4 symbols (2 bits), numerals in base 2, 3 symbols per element1200 p, SB, NB, D, k1 = 257, 2, 1, 3, 21201 H = -(-SB * D // NB); W = 8 * H + 1; S, B, R0, WU, N1 = 1, 2, 1, 1, D * k11202 NL = N1 + k1 * (W - WU); k = -(-NL // D); E = 71203 cd = {' ': 0, '0': 1, '(': 3, '+': 0, 'g': 3, '*': 2, ')': 1}1204 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)1205 assert (1 << (SB * D + 1)) < p and (1 << (NB * H + 1)) < p and D * k <= (1 << E) and (1 << (E + 1)) < p1206 f = g.diag(P); e = Ev(p); ok = True1207 for N in range(0, (1 << E) + 1): # the ranges the checker's hints use, on this field1208 fr = g.inrange(V(x0), g.K(N), E)1209 ok &= {x for x in range(p) if e.ev(fr, {x0: x})} == set(range(N))1210 rnd = random.Random(20261004); n_true = n_false = 01211 us_list = [[0, 0], [63, 63], [27, 54]] + [[rnd.randrange(64), rnd.randrange(64)] for _ in range(2)]1212 def env_of(us, vs):1213 env = {'u%x' % a: us[a] for a in range(k1)}; env.update({'v%02x' % a: vs[a] for a in range(k)}); return env1214 def variant(vs, a, r, dlt):1215 w = list(vs); dgt = (w[a] >> (SB * r)) & 3; w[a] += (((dgt + dlt) & 3) - dgt) << (SB * r); return w1216 for us in us_list:1217 vs = dd.pack(dd.F_ref(us, P), D, SB); ok &= len(vs) == k and e.ev(f, env_of(us, vs)); n_true += 11218 muts = [variant(vs, rnd.randrange(k), rnd.randrange(D), rnd.randrange(1, 4)) for _ in range(6)]1219 w = list(vs); w[rnd.randrange(k)] += 64; muts.append(w) # a coordinate that codes no string1220 w = list(vs); w[rnd.randrange(k)] = p - 1; muts.append(w)1221 for w in muts: ok &= not e.ev(f, env_of(us, w)); n_false += 11222 us = us_list[3]; vs = dd.pack(dd.F_ref(us, P), D, SB); n_one = 01223 for a in range(k): # every v at one symbol's distance, at one u1224 for r in range(D):1225 for dlt in (1, 2, 3): ok &= not e.ev(f, env_of(us, variant(vs, a, r, dlt))); n_one += 11226 ok &= (k, n_true, n_false, n_one) == (34, 5, 40, 306)1227 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"12281229 D, k1 = 1024, 40961230 r = dd.instance_checks(D, k1)1231 pre, ldiag, lth, lav, lau = r['parts']; k = r['k']1232 ok = all(r[c] for c in ('alphabet', 'fills_u', 'tokens', 'free', 'reader', 'code', 'numerals', 'lambda', 'fills_v', 'cases', 'ranges'))1233 ok &= (k, r['N1'], D * k1, r['NL'], D * k) == (45044, 3850485, 4194304, 45781237, 46125056)1234 ok &= r['N1'] == pre + ldiag + lth + 3 and D * k1 - r['N1'] + lth == 704170 and ok_small1235 per_u = Fraction(pre + lav + lau + lth, k1) # symbols of delta per coordinate of u, without the decoding (exact)1236 # 25:F8 (p25050)1237 R.check("G2", "Diag(u, v) as a written formula, model-checked on F_257 against the substitution computed from its definition, holds at v = code F(u) and fails at every tested other v; the instance at D = 1024 symbols per element (k1 = 4096, k = 45044) is a string read back by an independent reader with |delta| <= D k1 and |lambda| <= D k", ok,1238 "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: 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) and at each of the 306 tuples v at one symbol's distance from code F(u) at one u; 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 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; 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; 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" + "; " + (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']}"))12391240 def theta_max(vt): # theta = ~T of exactly 704 170 symbols1241 t = V(vt[0])1242 for nm in vt[1:]: t = dd.add(t, V(nm))1243 return ('not', dd.AND(dd.eq(t, dd.ZERO), *([dd.eq(V(vt[0]), V(vt[0]))] * 28651), dd.eq(dd.ZERO, dd.ZERO)))1244 r = dd.instance_checks(D, k1, theta_max, reader=False, sample=20000)1245 ok = all(r[c] for c in ('alphabet', 'fills_u', 'tokens', 'free', 'code', 'numerals', 'lambda', 'fills_v', 'cases', 'ranges'))1246 ok &= r['P']['theta_len'] == 704170 and r['N1'] == D * k1 and r['NL'] <= D * r['k'] and r['k'] == k1247 lo_T = sum(len(nm) for nm in ['v%04x' % i for i in range(k)]) # a formula in all k variables names each once1248 ok &= lo_T == 225220 and 700 < per_u < 8001249 g921 = dd.instance(921, k1); g922 = dd.instance(922, k1)1250 ok &= g921[3] is None and g921[1]['N1'] > 921 * k1 and g922[3] is not None and g922[1]['N1'] <= 922 * k11251 # 25:G8 (p25051)1252 R.check("G3", "Truth in the window: with theta = ~T of exactly 704 170 symbols delta fills u exactly 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, and the construction fits at D = 922 and not at D = 921", ok,1253 "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, 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; 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)" + "; " + (f"|lambda| = {r['NL']} <= {D * r['k']}; symbols of delta per coordinate of u, without the decoding: {per_u.numerator}/{per_u.denominator}; D = 921: |delta| = {g921[1]['N1']} > {921 * k1}; D = 922: {g922[1]['N1']} <= {922 * k1}"))125412551256if __name__ == "__main__":1257 want = [a.upper() for a in sys.argv[1:]] or sorted(BLOCK)1258 bad = [b for b in want if b not in BLOCK]1259 if bad: sys.exit(f"no block {', '.join(bad)}: the blocks are {', '.join(sorted(BLOCK))}")1260 for b in want: R.run_block(b)1261 sys.exit(0 if R.summary(write=False, expect=list(LEDGER) if want == sorted(BLOCK) else None) else 1)1262