"""p29_finitism — the ledger file of 29-finitism (9 October 2026).

"The Undeclared Posit of Potential Infinity" (Akhtman, preprint pp202607.0670.v1). The paper's predicate ledger (Appendix A)
is docs/29-finitism/29-finitism-ledger.json. This file binds its predicates to the framework: the table of keys
(generated from the ledger by ci/make_ledgers.py), the test data, and the thirteen checks of four blocks, which call the
logic theme (frc/logic.py, frc/formation.py). Each check names the predicate(s) it witnesses (LEDGER) under a
`# 29:XN (<key>)` marker on the check that decides it (PREDICATES). The paper has no earlier validation package: this
file is its first witness, written with the ledger. The Lean side is the certificate
lean/FrcCore/Ledgers/P29Finitism.lean over the logic and foundation themes' keys.

    python3 -m frc.ledgers.p29_finitism         every block, the census; exit 1 if a check fails (≈ 30 s)
    python3 -m frc.ledgers.p29_finitism C       one block (A, B, C or D)
    from frc.ledgers.p29_finitism import R; R.predicate("29:C2")    one predicate: its blocks run once per session

Blocks:  A  the exhibits: the finite frame, Q, induction                   EXACT  (29:B4–B6)
         B  empirical idleness: records, the minimal realization, padding  EXACT  (29:C1–C4)
         C  the boundary and the buffer frame                              EXACT  (29:C6–C8, C10)
         D  bounded actualism: conservativity and determinacy              EXACT  (29:E2, E4; X1, X2)

The notebook frc/ledgers/p29_finitism.ipynb runs one predicate per cell, the cell's id its key (gate G13).
"""
import random, sys
from itertools import product

from frc.registry import Registry
from frc.logic import fval, table, random_formula, random_structure, successor_counterexample
from frc.formation import (passes, minimal, pad, double, swap, is_automorphism, count_invariant, swap_invariant, buffer,
                           chain, reachable, least_below, finite_induction_holds, records, record, random_universe,
                           random_passed_trace, sval2, sval2_table, so_arities, random_sformula, closed,
                           d0_eval, d0_eval_frame, d0_bound, random_d0)

# ---- generated by ci/make_ledgers.py from docs/29-finitism/29-finitism-ledger.json; edit the ledger, not this table ----
PAPER = "29-finitism"
KEYS = {"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 key
LEAN = {"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 them
# ---- end of the generated table ----

LEAN_ONLY = ()                  # the predicates with a Lean declaration and no python check (gate G12): none

# The paper's predicate ledger (Appendix A, predicates cited as 29:XN): the predicate(s) each check witnesses.
LEDGER = {
    "A1": "29:B4", "A2": "29:B5", "A3": "29:B6",
    "B1": "29:C1", "B2": "29:C2", "B3": "29:C3", "B4": "29:C4",
    "C1": "29:C6", "C2": "29:C7", "C3": "29:C8, 29:X1", "C4": "29:C10",
    "D1": "29:E2, 29:X2", "D2": "29:E4",
}

BLOCK = {"A": "the exhibits: the finite frame, Q, induction",           # check-id prefix -> the block (the function block_<letter> below)
         "B": "empirical idleness: records, the minimal realization, padding",
         "C": "the boundary and the buffer frame",
         "D": "bounded actualism: conservativity and determinacy"}

# the deciding check of each witnessed predicate (the other checks that touch it are corroboration)
PREDICATES = {
    "29:B4": "A1", "29:B5": "A2", "29:B6": "A3",
    "29:C1": "B1", "29:C2": "B2", "29:C3": "B3", "29:C4": "B4",
    "29:C6": "C1", "29:C7": "C2", "29:C8": "C3", "29:X1": "C3", "29:C10": "C4",
    "29:E2": "D1", "29:X2": "D1", "29:E4": "D2",
}

R = Registry("29", "finitism", LEDGER, PREDICATES, sources=[__file__])

SEED = 29
ALPHABETS = (2, 3, 5, 32)                 # s, the letters of an agent's alphabet
CAPACITIES = range(0, 12)                 # K, the record length

# ------------------------------------------------------------------------------------------------------------
# block A: the exhibits (29:B4, B5, B6)
# Section 2 of the paper: a finite initial segment of arithmetic (truncated successor, sum and product as graphs) has a
# complete and decidable theory and carries no injective successor missing 0; the cyclic variant's successor act is total
# and makes nothing new; Robinson's Q has no finite model; on every finite frame the least-number principle and the
# induction schema hold for all subsets.
@R.block("A", BLOCK["A"])
def block_A():
    """Block A — the exhibits (EXACT): A1–A3."""
    rng = random.Random(SEED)
    # A1 the finite segment [0, m) with the graphs of the truncated successor, sum and product: every sentence or its
    #    negation holds (decided by exhaustive evaluation, frc.logic.fval, and by the table method); no map of [0, m) into
    #    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)
    ok = True; det = []
    for m in range(1, 5):
        def rel(r, args, m=m):
            if r == 0: return len(args) == 2 and args[0] < m and args[1] == args[0] + 1       # successor's graph, overflow fails
            if r == 1: return len(args) == 3 and args[0] + args[1] == args[2]                 # sum's graph
            if r == 2: return len(args) == 3 and args[0] * args[1] == args[2]                 # product's graph
            return False
        M = (m, rel)
        for _ in range(40):
            phi = random_formula(rng, 3, 1)
            sent = ("all", phi)
            v = fval(M, (), sent)
            ok &= (v != fval(M, (), ("neg", sent)))                                      # complete and consistent
            ok &= v == (() in table(M, sent, 0))                                        # decided a second way
        ok &= successor_counterexample(m) is None
        cyc = [(x + 1) % m for x in range(m)]
        ok &= sorted(cyc) == list(range(m))                                             # a bijection: nothing new
        x, seen = 0, []
        while x not in seen: seen.append(x); x = cyc[x]
        ok &= len(seen) == m and x == 0                                                 # one m-cycle, back to the start
        det.append(f"m={m}: 40 sentences decided two ways, no injective successor missing 0, one {m}-cycle")
    # 29:B4 (p29006)
    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))

    # A2 no finite structure interprets Q: on n <= 7 no injective map of [0, n) into itself misses an element (all n^n maps);
    #    on n <= 3 no (domain D, zero Z, successor relation Sg) satisfies totality on D, Q2 injectivity and Q1 (Sg never reaches
    #    a zero) — all 2^n domains, 2^n zero sets and 2^(n^2) relations (29:B5)
    ok = all(successor_counterexample(n) is None for n in range(1, 8))
    found = 0
    for n in range(1, 4):
        for D in product([False, True], repeat=n):
            if not any(D): continue
            for Z in product([False, True], repeat=n):
                if not any(D[z] and Z[z] for z in range(n)): continue
                for Sg in product([False, True], repeat=n * n):
                    S = lambda x, y: Sg[x * n + y]
                    tot = all(any(D[y] and S(x, y) for y in range(n)) for x in range(n) if D[x])
                    inj = all(x == x2 for x in range(n) for x2 in range(n) for y in range(n)
                              if D[x] and D[x2] and S(x, y) and S(x2, y))
                    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))
                    if tot and inj and q1: found += 1
    ok &= found == 0
    # 29:B5 (p25010)
    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,
             f"relational interpretations found: {found}")

    # A3 induction is a theorem of every finite frame: every nonempty subset of [0, n) has a least element, and the induction
    #    schema holds for 500 random properties (the least counterexample refutes a closed-under-successor failure) (29:B6)
    ok = True
    for _ in range(500):
        n = rng.randrange(0, 16); P = [rng.randrange(2) == 0 for _ in range(n)]
        ok &= finite_induction_holds(P)
        fails = [x for x in range(n) if not P[x]]
        ok &= least_below([not p for p in P], n) == (fails[0] if fails else None)
        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,))
    # 29:B6 (p29007)
    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)

# ------------------------------------------------------------------------------------------------------------
# block B: empirical idleness (29:C1, C2, C3, C4)
# Section 4: an agent of capacity K over s letters holds fewer than s^(K+1) records; a check that passes in any universe
# passes in the minimal realization of its own trace (t objects, closed); the check is decided by exhaustive evaluation
# 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.
@R.block("B", BLOCK["B"])
def block_B():
    """Block B — empirical idleness (EXACT): B1–B4."""
    rng = random.Random(SEED + 1)
    # B1 the record count: sum_{i<=K} s^i < s^(K+1), also by the closed form of the geometric sum (29:C1)
    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)
    # 29:C1 (p29009)
    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)

    # B2 the minimal realization: 300 random universes of at most 8 objects, a trace that passes in each; the minimal
    #    realization has exactly t objects, is closed, and the check passes in it under the identity; on t <= 3 it is among
    #    all universes on t objects that realize the trace (29:C2)
    ok = True; n_traces = 0; searched = 0
    for _ in range(300):
        U = random_universe(rng, rng.randrange(2, 9))
        T, e = random_passed_trace(rng, U); t = T[0]
        assert passes(T, U, e)
        M = minimal(T)
        ok &= M[0] == t and closed(M) and passes(T, M, list(range(t)))
        if t <= 3:
            found = [list(f) for f in product([None] + list(range(t)), repeat=t) if passes(T, (t, list(f)), list(range(t)))]
            ok &= M[1] in found; searched += 1
        n_traces += 1
    # 29:C2 (p29010)
    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,
             f"{n_traces} traces, {searched} searched exhaustively")

    # B3 the asymmetry: the check reads t^2 atoms and terminates (its evaluation is a finite conjunction, counted), and the
    #    trace's atom table is a record of t^2 symbols; retained when t^2 <= K (29:C3)
    ok = True; cnt = 0
    for _ in range(200):
        U = random_universe(rng, rng.randrange(1, 8))
        T, e = random_passed_trace(rng, U); t = T[0]
        rec = record(T)
        ok &= len(rec) == t * t
        reads = sum(1 for i in range(t) for j in range(t))                              # the atoms the check reads
        ok &= reads == t * t and passes(T, U, e)
        ok &= (t * t <= 8) == (len(rec) <= 8)                                           # retained by an agent of capacity 8 iff t^2 <= 8
        cnt += 1
    # 29:C3 (p29011)
    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")

    # B4 padding: a passed check passes after any number of fresh formations, so for every B a realizing universe of more
    #    than B objects exists; the padded universe stays closed (29:C4)
    ok = True
    for _ in range(300):
        U = random_universe(rng, rng.randrange(1, 8))
        T, e = random_passed_trace(rng, U); t = T[0]
        M = minimal(T)
        for B in (0, 1, 5, 40):
            P = pad(M, B + 1)
            ok &= passes(T, P, list(range(t))) and P[0] > B and closed(P)
            ok &= passes(T, pad(U, B + 1), e)
    # 29:C4 (p29012)
    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)

# ------------------------------------------------------------------------------------------------------------
# block C: the boundary and the buffer frame (29:C6, C7, C8, C10)
# Lemma boundary: the disjoint double carries the swap, an automorphism without fixed points; a swap-invariant condition
# has an even number of satisfiers; the minimal realization holds only trace objects and a datum never formed has no
# preimage. Proposition illusion: the buffer frame of sigma seeds and D rounds. O3: the pigeonhole on records.
@R.block("C", BLOCK["C"])
def block_C():
    """Block C — the boundary and the buffer frame (EXACT): C1–C4."""
    rng = random.Random(SEED + 2)
    # C1 the double and its swap: an automorphism, fixed-point-free, of order two; the check passes in the double read in the
    #    first copy; 1,500 swap-invariant conditions have an even number of satisfiers, never one (29:C6)
    ok = True; conds = 0
    for _ in range(300):
        U = random_universe(rng, rng.randrange(1, 8)); n = U[0]
        W = double(U)
        sigma = [swap(U, x) for x in range(2 * n)]
        ok &= is_automorphism(W, sigma) and all(sigma[x] != x and sigma[sigma[x]] == x for x in range(2 * n))
        T, e = random_passed_trace(rng, U)
        ok &= passes(T, W, e)
        for _ in range(5):
            D0 = [rng.randrange(2) == 0 for _ in range(n)]; D = D0 + D0
            ok &= swap_invariant(W, D)
            c = count_invariant(W, D)
            ok &= c == 2 * sum(D0) and c != 1; conds += 1
    # 29:C6 (p29014)
    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,
             f"300 doubles, {conds} invariant conditions")

    # C2 the minimal realization confines: it has exactly the trace's t objects; a datum x the trace never forms has no
    #    preimage in it (29:C7)
    ok = True; cases = 0
    for _ in range(300):
        U = random_universe(rng, rng.randrange(1, 8))
        T, e = random_passed_trace(rng, U); t, atom = T
        M = minimal(T)
        ok &= M[0] == t
        for x in range(t):
            if not any(atom[i][x] for i in range(t)):
                ok &= all(M[1][y] != x for y in range(t)); cases += 1
    # 29:C7 (p29015)
    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")

    # C3 the buffer frame: sigma seeds and D rounds, sigma(D+1) formations; every object below level D has a fresh image
    #    one level up; k acts from a seed reach level k; the objects reachable in r acts are sigma(r+1); the instance
    #    (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)
    ok = True; frames = 0
    for sigma in (1, 2, 3):
        for D in (1, 2, 5, 17):
            M, form = buffer(sigma, D)
            ok &= M == sigma * (D + 1)
            seeds = [s * (D + 1) for s in range(sigma)]
            for r in range(D + 1):
                ok &= len(reachable((M, form), seeds, r)) == sigma * (r + 1)
            for s in range(sigma):
                for k in range(D + 1):
                    x = chain(sigma, D, s, k)
                    ok &= x == s * (D + 1) + k
                    if k < D: ok &= form[x] == x + 1 and x + 1 < M and (x + 1) % (D + 1) == x % (D + 1) + 1
                ok &= form[chain(sigma, D, s, D)] is None
            frames += 1
    ok &= 2 * 2 ** 4 < buffer(2, 17)[0] and 2 ** 4 < 17
    # 29:C8 (p29016), 29:X1 (p29026)
    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,
             f"{frames} frames")

    # 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)
    #    formations no reading of the frame into the records is injective — every map [0, M) -> [0, R) with R < M collides,
    #    checked on all R^M maps for M <= 5 and at (s, K, M) = (2, 3, 36) by counting (29:C10)
    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))
    s, K, M = 2, 3, 36
    ok &= records(s, K) < s ** (K + 1) < M and records(s, K) == 15
    # 29:C10 (p05013)
    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)

# ------------------------------------------------------------------------------------------------------------
# block D: bounded actualism (29:E2, E4; X2)
# Section 7: certificate conservativity — a Delta_0 sentence takes its standard value in every frame beyond its bound
# (5:B6), every schema instance below the bound is decided by evaluation, induction transfers instance-wise (B6);
# effective determinacy on a finite frame — the full second-order theory decided by exhaustive evaluation.
@R.block("D", BLOCK["D"])
def block_D():
    """Block D — bounded actualism (EXACT): D1–D2."""
    rng = random.Random(SEED + 3)
    # D1 conservativity: 400 random Delta_0 sentences take their standard value in the frames W_N for N = t+1, t+2, t+10
    #    above their bound t; 100 first-order sentences over random structures decided two ways; the induction schema on
    #    200 random properties (29:E2); hence no proof practice below the bound is lost (29:X2)
    ok = True; n_d0 = 0
    for _ in range(400):
        phi = random_d0(rng, 3, 0); b = d0_bound((), phi); v = d0_eval((), phi)
        ok &= all(d0_eval_frame(N, (), phi) == v for N in (b + 1, b + 2, b + 10)); n_d0 += 1
    for _ in range(100):
        M = random_structure(rng, rng.randrange(1, 4)); phi = ("all", random_formula(rng, 3, 1))
        ok &= fval(M, (), phi) == (() in table(M, phi, 0))
    for _ in range(200):
        P = [rng.randrange(2) == 0 for _ in range(rng.randrange(0, 12))]
        ok &= finite_induction_holds(P)
    # 29:E2 (p29022), 29:X2 (p29027)
    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")

    # D2 effective determinacy on a finite frame: 60 random second-order sentences (set and relation quantifiers of arity
    #    1 and 2) over structures of m <= 3 elements, decided by exhaustive evaluation over the 2^m subsets and the 2^(m^a)
    #    relations, and a second way by tables of satisfying assignments; each sentence or its negation holds (29:E4)
    ok = True; n_so = 0
    for _ in range(60):
        m = rng.randrange(1, 4); M = random_structure(rng, m)
        phi = random_sformula(rng, 3, 0, 0, 0)
        ok &= so_arities(phi) == (0, 0, 0)
        v = sval2(M, (), (), (), phi)
        ok &= v == (((), (), ()) in sval2_table(M, phi, 0, 0, 0, 2))
        ok &= sval2(M, (), (), (), ("neg", phi)) != v; n_so += 1
    # 29:E4 (p29024)
    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,
             f"{n_so} sentences")

if __name__ == "__main__":
    want = [a.upper() for a in sys.argv[1:]] or sorted(BLOCK)
    bad = [b for b in want if b not in BLOCK]
    if bad: sys.exit(f"no block {', '.join(bad)}: the blocks are {', '.join(sorted(BLOCK))}")
    for b in want: R.run_block(b)
    sys.exit(0 if R.summary(write=False, expect=list(LEDGER) if want == sorted(BLOCK) else None) else 1)