p29_finitism.py — frc/ledgers

1"""p29_finitism — the ledger file of 29-finitism (9 October 2026).23"The Undeclared Posit of Potential Infinity" (Akhtman, preprint pp202607.0670.v1). The paper's predicate ledger (Appendix A)4is docs/29-finitism/29-finitism-ledger.json. This file binds its predicates to the framework: the table of keys5(generated from the ledger by ci/make_ledgers.py), the test data, and the thirteen checks of four blocks, which call the6logic theme (frc/logic.py, frc/formation.py). Each check names the predicate(s) it witnesses (LEDGER) under a7`# 29:XN (<key>)` marker on the check that decides it (PREDICATES). The paper has no earlier validation package: this8file is its first witness, written with the ledger. The Lean side is the certificate9lean/FrcCore/Ledgers/P29Finitism.lean over the logic and foundation themes' keys.1011    python3 -m frc.ledgers.p29_finitism         every block, the census; exit 1 if a check fails (≈ 30 s)12    python3 -m frc.ledgers.p29_finitism C       one block (A, B, C or D)13    from frc.ledgers.p29_finitism import R; R.predicate("29:C2")    one predicate: its blocks run once per session1415Blocks:  A  the exhibits: the finite frame, Q, induction                   EXACT  (29:B4–B6)16         B  empirical idleness: records, the minimal realization, padding  EXACT  (29:C1–C4)17         C  the boundary and the buffer frame                              EXACT  (29:C6–C8, C10)18         D  bounded actualism: conservativity and determinacy              EXACT  (29:E2, E4; X1, X2)1920The notebook frc/ledgers/p29_finitism.ipynb runs one predicate per cell, the cell's id its key (gate G13).21"""22import random, sys23from itertools import product2425from frc.registry import Registry26from frc.logic import fval, table, random_formula, random_structure, successor_counterexample27from frc.formation import (passes, minimal, pad, double, swap, is_automorphism, count_invariant, swap_invariant, buffer,28                           chain, reachable, least_below, finite_induction_holds, records, record, random_universe,29                           random_passed_trace, sval2, sval2_table, so_arities, random_sformula, closed,30                           d0_eval, d0_eval_frame, d0_bound, random_d0)3132# ---- generated by ci/make_ledgers.py from docs/29-finitism/29-finitism-ledger.json; edit the ledger, not this table ----33PAPER = "29-finitism"34KEYS = {"A1": "p29001", "A2": "p29002", "B1": "p29003", "B2": "p29004", "B3": "p29005", "B4": "p29006", "B5": "p25010", "B6": "p29007", "B7": "p29008", "C1": "p29009", "C2": "p29010", "C3": "p29011", "C4": "p29012", "C5": "p29013", "C6": "p29014", "C7": "p29015", "C8": "p29016", "C9": "p29017", "C10": "p05013", "D1": "p29018", "D2": "p29019", "D3": "p29020", "E1": "p29021", "E2": "p29022", "E3": "p29023", "E4": "p29024", "E5": "p29025", "X1": "p29026", "X2": "p29027"}       # every row of the ledger: its label and its accession key35LEAN = {"B4": "core", "B5": "core", "B6": "core", "C2": "core", "C3": "core", "C4": "core", "C6": "core", "C7": "core", "C8": "core", "C10": "core", "E2": "core", "E4": "core", "X1": "core", "X2": "core"}       # the rows with a Lean declaration: the libraries whose key files prove them36# ---- end of the generated table ----3738LEAN_ONLY = ()                  # the predicates with a Lean declaration and no python check (gate G12): none3940# The paper's predicate ledger (Appendix A, predicates cited as 29:XN): the predicate(s) each check witnesses.41LEDGER = {42    "A1": "29:B4", "A2": "29:B5", "A3": "29:B6",43    "B1": "29:C1", "B2": "29:C2", "B3": "29:C3", "B4": "29:C4",44    "C1": "29:C6", "C2": "29:C7", "C3": "29:C8, 29:X1", "C4": "29:C10",45    "D1": "29:E2, 29:X2", "D2": "29:E4",46}4748BLOCK = {"A": "the exhibits: the finite frame, Q, induction",           # check-id prefix -> the block (the function block_<letter> below)49         "B": "empirical idleness: records, the minimal realization, padding",50         "C": "the boundary and the buffer frame",51         "D": "bounded actualism: conservativity and determinacy"}5253# the deciding check of each witnessed predicate (the other checks that touch it are corroboration)54PREDICATES = {55    "29:B4": "A1", "29:B5": "A2", "29:B6": "A3",56    "29:C1": "B1", "29:C2": "B2", "29:C3": "B3", "29:C4": "B4",57    "29:C6": "C1", "29:C7": "C2", "29:C8": "C3", "29:X1": "C3", "29:C10": "C4",58    "29:E2": "D1", "29:X2": "D1", "29:E4": "D2",59}6061R = Registry("29", "finitism", LEDGER, PREDICATES, sources=[__file__])6263SEED = 2964ALPHABETS = (2, 3, 5, 32)                 # s, the letters of an agent's alphabet65CAPACITIES = range(0, 12)                 # K, the record length6667# ------------------------------------------------------------------------------------------------------------68# block A: the exhibits (29:B4, B5, B6)69# Section 2 of the paper: a finite initial segment of arithmetic (truncated successor, sum and product as graphs) has a70# complete and decidable theory and carries no injective successor missing 0; the cyclic variant's successor act is total71# and makes nothing new; Robinson's Q has no finite model; on every finite frame the least-number principle and the72# induction schema hold for all subsets.73@R.block("A", BLOCK["A"])74def block_A():75    """Block A — the exhibits (EXACT): A1–A3."""76    rng = random.Random(SEED)77    # A1 the finite segment [0, m) with the graphs of the truncated successor, sum and product: every sentence or its78    #    negation holds (decided by exhaustive evaluation, frc.logic.fval, and by the table method); no map of [0, m) into79    #    itself is injective and misses 0; the cycle: x -> x+1 mod m is a bijection, one m-cycle, every object an image (29:B4)80    ok = True; det = []81    for m in range(1, 5):82        def rel(r, args, m=m):83            if r == 0: return len(args) == 2 and args[0] < m and args[1] == args[0] + 1       # successor's graph, overflow fails84            if r == 1: return len(args) == 3 and args[0] + args[1] == args[2]                 # sum's graph85            if r == 2: return len(args) == 3 and args[0] * args[1] == args[2]                 # product's graph86            return False87        M = (m, rel)88        for _ in range(40):89            phi = random_formula(rng, 3, 1)90            sent = ("all", phi)91            v = fval(M, (), sent)92            ok &= (v != fval(M, (), ("neg", sent)))                                      # complete and consistent93            ok &= v == (() in table(M, sent, 0))                                        # decided a second way94        ok &= successor_counterexample(m) is None95        cyc = [(x + 1) % m for x in range(m)]96        ok &= sorted(cyc) == list(range(m))                                             # a bijection: nothing new97        x, seen = 0, []98        while x not in seen: seen.append(x); x = cyc[x]99        ok &= len(seen) == m and x == 0                                                 # one m-cycle, back to the start100        det.append(f"m={m}: 40 sentences decided two ways, no injective successor missing 0, one {m}-cycle")101    # 29:B4 (p29006)102    R.check("A1", "the finite segment: complete and decidable theory (two evaluators agree on 160 sentences), no injective successor missing 0; the cycle: total, bijective, one m-cycle", ok, "; ".join(det))103104    # A2 no finite structure interprets Q: on n <= 7 no injective map of [0, n) into itself misses an element (all n^n maps);105    #    on n <= 3 no (domain D, zero Z, successor relation Sg) satisfies totality on D, Q2 injectivity and Q1 (Sg never reaches106    #    a zero) — all 2^n domains, 2^n zero sets and 2^(n^2) relations (29:B5)107    ok = all(successor_counterexample(n) is None for n in range(1, 8))108    found = 0109    for n in range(1, 4):110        for D in product([False, True], repeat=n):111            if not any(D): continue112            for Z in product([False, True], repeat=n):113                if not any(D[z] and Z[z] for z in range(n)): continue114                for Sg in product([False, True], repeat=n * n):115                    S = lambda x, y: Sg[x * n + y]116                    tot = all(any(D[y] and S(x, y) for y in range(n)) for x in range(n) if D[x])117                    inj = all(x == x2 for x in range(n) for x2 in range(n) for y in range(n)118                              if D[x] and D[x2] and S(x, y) and S(x2, y))119                    q1 = all(not Z[y] for x in range(n) for y in range(n) if D[x] and D[y] and S(x, y))120                    if tot and inj and q1: found += 1121    ok &= found == 0122    # 29:B5 (p25010)123    R.check("A2", "no finite structure interprets Q: no injective successor missing 0 on n <= 7 (all n^n maps); no relational interpretation (D, Z, Sg) with totality, Q2 and Q1 on n <= 3", ok,124             f"relational interpretations found: {found}")125126    # A3 induction is a theorem of every finite frame: every nonempty subset of [0, n) has a least element, and the induction127    #    schema holds for 500 random properties (the least counterexample refutes a closed-under-successor failure) (29:B6)128    ok = True129    for _ in range(500):130        n = rng.randrange(0, 16); P = [rng.randrange(2) == 0 for _ in range(n)]131        ok &= finite_induction_holds(P)132        fails = [x for x in range(n) if not P[x]]133        ok &= least_below([not p for p in P], n) == (fails[0] if fails else None)134        ok &= all(least_below(P, n) is None or (P[least_below(P, n)] and not any(P[y] for y in range(least_below(P, n)))) for _ in (0,))135    # 29:B6 (p29007)136    R.check("A3", "on [0, n), n < 16: every nonempty subset has a least element (500 random subsets), and a property true at 0 and closed under successor below n holds below n", ok)137138# ------------------------------------------------------------------------------------------------------------139# block B: empirical idleness (29:C1, C2, C3, C4)140# Section 4: an agent of capacity K over s letters holds fewer than s^(K+1) records; a check that passes in any universe141# passes in the minimal realization of its own trace (t objects, closed); the check is decided by exhaustive evaluation142# of its t^2 atoms and the trace is a record of t^2 symbols; padding by any number of fresh formations keeps it passing.143@R.block("B", BLOCK["B"])144def block_B():145    """Block B — empirical idleness (EXACT): B1–B4."""146    rng = random.Random(SEED + 1)147    # B1 the record count: sum_{i<=K} s^i < s^(K+1), also by the closed form of the geometric sum (29:C1)148    ok = all(records(s, K) < s ** (K + 1) and records(s, K) == (s ** (K + 1) - 1) // (s - 1) for s in ALPHABETS for K in CAPACITIES)149    # 29:C1 (p29009)150    R.check("B1", "fewer than s^(K+1) records of at most K symbols over s letters, s in {2, 3, 5, 32}, K < 12 (48 pairs)", ok)151152    # B2 the minimal realization: 300 random universes of at most 8 objects, a trace that passes in each; the minimal153    #    realization has exactly t objects, is closed, and the check passes in it under the identity; on t <= 3 it is among154    #    all universes on t objects that realize the trace (29:C2)155    ok = True; n_traces = 0; searched = 0156    for _ in range(300):157        U = random_universe(rng, rng.randrange(2, 9))158        T, e = random_passed_trace(rng, U); t = T[0]159        assert passes(T, U, e)160        M = minimal(T)161        ok &= M[0] == t and closed(M) and passes(T, M, list(range(t)))162        if t <= 3:163            found = [list(f) for f in product([None] + list(range(t)), repeat=t) if passes(T, (t, list(f)), list(range(t)))]164            ok &= M[1] in found; searched += 1165        n_traces += 1166    # 29:C2 (p29010)167    R.check("B2", "a passed check passes in the finite universe of its own trace, t(r) objects, closed, read by the identity: 300 random traces; on t <= 3 the minimal realization found by exhaustive search", ok,168             f"{n_traces} traces, {searched} searched exhaustively")169170    # B3 the asymmetry: the check reads t^2 atoms and terminates (its evaluation is a finite conjunction, counted), and the171    #    trace's atom table is a record of t^2 symbols; retained when t^2 <= K (29:C3)172    ok = True; cnt = 0173    for _ in range(200):174        U = random_universe(rng, rng.randrange(1, 8))175        T, e = random_passed_trace(rng, U); t = T[0]176        rec = record(T)177        ok &= len(rec) == t * t178        reads = sum(1 for i in range(t) for j in range(t))                              # the atoms the check reads179        ok &= reads == t * t and passes(T, U, e)180        ok &= (t * t <= 8) == (len(rec) <= 8)                                           # retained by an agent of capacity 8 iff t^2 <= 8181        cnt += 1182    # 29:C3 (p29011)183    R.check("B3", "the check of a trace evaluates its t^2 atoms and terminates; the trace is itself a record of t^2 symbols, retained by an agent of capacity K iff t^2 <= K (200 traces)", ok, f"{cnt} traces")184185    # B4 padding: a passed check passes after any number of fresh formations, so for every B a realizing universe of more186    #    than B objects exists; the padded universe stays closed (29:C4)187    ok = True188    for _ in range(300):189        U = random_universe(rng, rng.randrange(1, 8))190        T, e = random_passed_trace(rng, U); t = T[0]191        M = minimal(T)192        for B in (0, 1, 5, 40):193            P = pad(M, B + 1)194            ok &= passes(T, P, list(range(t))) and P[0] > B and closed(P)195            ok &= passes(T, pad(U, B + 1), e)196    # 29:C4 (p29012)197    R.check("B4", "a passed check passes unchanged after padding by B + 1 fresh formations, B in {0, 1, 5, 40}, from the minimal realization and from the original universe (300 traces): no bound is entailed", ok)198199# ------------------------------------------------------------------------------------------------------------200# block C: the boundary and the buffer frame (29:C6, C7, C8, C10)201# Lemma boundary: the disjoint double carries the swap, an automorphism without fixed points; a swap-invariant condition202# has an even number of satisfiers; the minimal realization holds only trace objects and a datum never formed has no203# preimage. Proposition illusion: the buffer frame of sigma seeds and D rounds. O3: the pigeonhole on records.204@R.block("C", BLOCK["C"])205def block_C():206    """Block C — the boundary and the buffer frame (EXACT): C1–C4."""207    rng = random.Random(SEED + 2)208    # C1 the double and its swap: an automorphism, fixed-point-free, of order two; the check passes in the double read in the209    #    first copy; 1,500 swap-invariant conditions have an even number of satisfiers, never one (29:C6)210    ok = True; conds = 0211    for _ in range(300):212        U = random_universe(rng, rng.randrange(1, 8)); n = U[0]213        W = double(U)214        sigma = [swap(U, x) for x in range(2 * n)]215        ok &= is_automorphism(W, sigma) and all(sigma[x] != x and sigma[sigma[x]] == x for x in range(2 * n))216        T, e = random_passed_trace(rng, U)217        ok &= passes(T, W, e)218        for _ in range(5):219            D0 = [rng.randrange(2) == 0 for _ in range(n)]; D = D0 + D0220            ok &= swap_invariant(W, D)221            c = count_invariant(W, D)222            ok &= c == 2 * sum(D0) and c != 1; conds += 1223    # 29:C6 (p29014)224    R.check("C1", "the double of a universe carries the swap: an automorphism, no fixed point, order two; the check passes in the double; a swap-invariant condition has an even number of satisfiers, never exactly one", ok,225             f"300 doubles, {conds} invariant conditions")226227    # C2 the minimal realization confines: it has exactly the trace's t objects; a datum x the trace never forms has no228    #    preimage in it (29:C7)229    ok = True; cases = 0230    for _ in range(300):231        U = random_universe(rng, rng.randrange(1, 8))232        T, e = random_passed_trace(rng, U); t, atom = T233        M = minimal(T)234        ok &= M[0] == t235        for x in range(t):236            if not any(atom[i][x] for i in range(t)):237                ok &= all(M[1][y] != x for y in range(t)); cases += 1238    # 29:C7 (p29015)239    R.check("C2", "the minimal realization has the trace's objects and nothing else; a datum the trace never forms has no preimage there", ok, f"{cases} unformed data checked")240241    # C3 the buffer frame: sigma seeds and D rounds, sigma(D+1) formations; every object below level D has a fresh image242    #    one level up; k acts from a seed reach level k; the objects reachable in r acts are sigma(r+1); the instance243    #    (sigma, D) = (2, 17): M = 36 > 2 * 2^4 and D > 2^4 (29:C8); hence "one can always continue" below the horizon (29:X1)244    ok = True; frames = 0245    for sigma in (1, 2, 3):246        for D in (1, 2, 5, 17):247            M, form = buffer(sigma, D)248            ok &= M == sigma * (D + 1)249            seeds = [s * (D + 1) for s in range(sigma)]250            for r in range(D + 1):251                ok &= len(reachable((M, form), seeds, r)) == sigma * (r + 1)252            for s in range(sigma):253                for k in range(D + 1):254                    x = chain(sigma, D, s, k)255                    ok &= x == s * (D + 1) + k256                    if k < D: ok &= form[x] == x + 1 and x + 1 < M and (x + 1) % (D + 1) == x % (D + 1) + 1257                ok &= form[chain(sigma, D, s, D)] is None258            frames += 1259    ok &= 2 * 2 ** 4 < buffer(2, 17)[0] and 2 ** 4 < 17260    # 29:C8 (p29016), 29:X1 (p29026)261    R.check("C3", "the buffer frame (sigma seeds, D rounds): sigma(D+1) formations, every object below level D formed one level up, k acts reach level k, sigma(r+1) objects reachable in r acts; (2, 17): M = 36 > 32, 17 > 16", ok,262             f"{frames} frames")263264    # C4 the pigeonhole: an agent of capacity K over s letters holds fewer than s^(K+1) records; in a frame of M > s^(K+1)265    #    formations no reading of the frame into the records is injective — every map [0, M) -> [0, R) with R < M collides,266    #    checked on all R^M maps for M <= 5 and at (s, K, M) = (2, 3, 36) by counting (29:C10)267    ok = all(any(f[i] == f[j] for i in range(M) for j in range(i)) for M in range(2, 6) for Rn in range(1, M) for f in product(range(Rn), repeat=M))268    s, K, M = 2, 3, 36269    ok &= records(s, K) < s ** (K + 1) < M and records(s, K) == 15270    # 29:C10 (p05013)271    R.check("C4", "every map of M objects into R < M records collides (all R^M maps, M <= 5); at (s, K, M) = (2, 3, 36) the agent holds 15 < 16 < 36 records, so no injective reading of the frame exists", ok)272273# ------------------------------------------------------------------------------------------------------------274# block D: bounded actualism (29:E2, E4; X2)275# Section 7: certificate conservativity — a Delta_0 sentence takes its standard value in every frame beyond its bound276# (5:B6), every schema instance below the bound is decided by evaluation, induction transfers instance-wise (B6);277# effective determinacy on a finite frame — the full second-order theory decided by exhaustive evaluation.278@R.block("D", BLOCK["D"])279def block_D():280    """Block D — bounded actualism (EXACT): D1–D2."""281    rng = random.Random(SEED + 3)282    # D1 conservativity: 400 random Delta_0 sentences take their standard value in the frames W_N for N = t+1, t+2, t+10283    #    above their bound t; 100 first-order sentences over random structures decided two ways; the induction schema on284    #    200 random properties (29:E2); hence no proof practice below the bound is lost (29:X2)285    ok = True; n_d0 = 0286    for _ in range(400):287        phi = random_d0(rng, 3, 0); b = d0_bound((), phi); v = d0_eval((), phi)288        ok &= all(d0_eval_frame(N, (), phi) == v for N in (b + 1, b + 2, b + 10)); n_d0 += 1289    for _ in range(100):290        M = random_structure(rng, rng.randrange(1, 4)); phi = ("all", random_formula(rng, 3, 1))291        ok &= fval(M, (), phi) == (() in table(M, phi, 0))292    for _ in range(200):293        P = [rng.randrange(2) == 0 for _ in range(rng.randrange(0, 12))]294        ok &= finite_induction_holds(P)295    # 29:E2 (p29022), 29:X2 (p29027)296    R.check("D1", "400 Delta_0 sentences keep their standard value in every frame beyond their bound (N = t+1, t+2, t+10); 100 schema instances decided two ways; the induction schema on 200 properties", ok, f"{n_d0} sentences")297298    # D2 effective determinacy on a finite frame: 60 random second-order sentences (set and relation quantifiers of arity299    #    1 and 2) over structures of m <= 3 elements, decided by exhaustive evaluation over the 2^m subsets and the 2^(m^a)300    #    relations, and a second way by tables of satisfying assignments; each sentence or its negation holds (29:E4)301    ok = True; n_so = 0302    for _ in range(60):303        m = rng.randrange(1, 4); M = random_structure(rng, m)304        phi = random_sformula(rng, 3, 0, 0, 0)305        ok &= so_arities(phi) == (0, 0, 0)306        v = sval2(M, (), (), (), phi)307        ok &= v == (((), (), ()) in sval2_table(M, phi, 0, 0, 0, 2))308        ok &= sval2(M, (), (), (), ("neg", phi)) != v; n_so += 1309    # 29:E4 (p29024)310    R.check("D2", "the full second-order theory of a finite structure (m <= 3) decided by exhaustive evaluation over its 2^m subsets and 2^(m^a) relations: 60 sentences agree with the table method, each or its negation holds", ok,311             f"{n_so} sentences")312313if __name__ == "__main__":314    want = [a.upper() for a in sys.argv[1:]] or sorted(BLOCK)315    bad = [b for b in want if b not in BLOCK]316    if bad: sys.exit(f"no block {', '.join(bad)}: the blocks are {', '.join(sorted(BLOCK))}")317    for b in want: R.run_block(b)318    sys.exit(0 if R.summary(write=False, expect=list(LEDGER) if want == sorted(BLOCK) else None) else 1)319