"""master/logic — a ledger file of the master's block Z, the horizon: the rows the logic theme proves (ledger migration, task LM26, 6 October 2026). Block Z is bound by one file per theme whose key file proves its rows: frc/ledgers/master/horizon.py (the horizon theme) and this file (the logic theme). This file binds Z1, Gödel vacuous over the finite Ω: the table of keys (generated from docs/00-ledger.json by ci/make_ledgers.py), the Lean proofs its key conjoins (PROOFS), the structures, and the checks, which call the logic theme (frc/logic.py). The Lean side is lean/FrcCore/Theme/Logic.lean, the key file lean/FrcCore/Keys/Logic.lean and the certificate lean/FrcCore/Ledgers/Master/Logic.lean. python3 -m frc.ledgers.master.logic every block, the census; exit 1 if a check fails Blocks: Q Gödel vacuous over a finite structure: no Q, the theory decided EXACT (00:Z1) The notebook frc/ledgers/master/logic.ipynb runs one row per cell, the cell's id its key (gate G13). """ import random import sys from itertools import product from frc.registry import Registry from frc.logic import fval, table, random_formula, random_structure, successor_counterexample # ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ---- BLOCK = "Z" KEYS = {"Z1": "p00186", "Z2": "p00110", "Z3": "p00111", "Z4": "p00112", "Z5": "p27021", "Z6": "p00114", "Z7": "p00115", "Z8": "p00116", "Z9": "p00187", "Z10": "p20043", "Z11": "p00135"} # every row of the block: its label and its accession key LEAN = {"Z1": "core"} # the rows with a Lean declaration: the libraries whose key files prove them # ---- end of the generated table ---- # The Lean proofs of the rows' keys: the theorems of the themes that each key conjoins (lean/make_keys.py writes the keys # FRC.Ledger.p from them). The master's block file is the binding's source, as a paper's \lean{} cells are its own. PROOFS = { "Z1": ["FRC.Logic.no_finite_successor", "FRC.Logic.no_finite_Q", "FRC.Logic.no_interpretation", "FRC.Logic.fin_theory_decidable", "FRC.Logic.fin_theory_complete", "FRC.Logic.fin_theory_consistent"], } LEAN_ONLY = () # the rows with a Lean declaration and no python check (gate G12): none SIZES = [1, 2, 3, 4] # the random structures' sizes FORMULAS = 600 # random formulas per size MAPS = 6 # every map [0, n) → [0, n) for n ≤ MAPS LEDGER = {"Q1": "00:Z1", "Q2": "00:Z1", "Q3": "00:Z1"} BLOCKS = {"Q": "Gödel vacuous over a finite structure: no Q, the theory decided"} PREDICATES = {"00:Z1": "Q1"} R = Registry("00", "logic", LEDGER, PREDICATES, sources=[__file__]) def _shell_structure(p): """The shell 𝔽_p as a relational structure: relation 0 the graph of the successor x ↦ x + 1, relation 1 the zero, relation 2 the graph of x ↦ 2x.""" def rel(r, args): if r == 0: return len(args) == 2 and (args[0] + 1) % p == args[1] if r == 1: return len(args) == 1 and args[0] == 0 if r == 2: return len(args) == 2 and 2 * args[0] % p == args[1] return False return p, rel # ------------------------------------------------------------------------------------------------------------ # block Q: Gödel vacuous over a finite structure (00:Z1) # a finite structure carries no injective successor missing an element, so it interprets no Q; its first-order theory is # decided by exhaustive evaluation, complete and consistent (Logic.lean: no_finite_successor, fin_theory_decidable, # fin_theory_complete, fin_theory_consistent). @R.block("Q", BLOCKS["Q"]) def block_Q(): """Block Q — Gödel vacuous over a finite structure (EXACT): Q1–Q3.""" # 00:Z1 (p00186) rng = random.Random(1) bad, n_checked = [], 0 for m in SIZES: for t in range(3): M = random_structure(rng, m) for _ in range(FORMULAS // 3): k = rng.randrange(1, 3) phi = random_formula(rng, 5, k) T = table(M, phi, k) for a in product(range(m), repeat=k): v, w = fval(M, a, phi), fval(M, a, ("neg", phi)) n_checked += 1 if v != (a in T) or v == w: bad.append((m, phi, a)) succ = [n for n in range(1, MAPS + 1) if successor_counterexample(n) is not None] R.check("Q1", f"random structures on 1–4 elements, {FORMULAS} random formulas each size: the exhaustive evaluation agrees with " "the satisfying tables built bottom-up, and exactly one of φ, ¬φ holds; every map [0, n) → [0, n), n ≤ " f"{MAPS}: none is injective and misses an element", not bad and not succ, f"{n_checked} evaluations; exceptions {bad[:2]}; successor counterexamples at n = {succ}") # Q2 the shells 𝔽_p: Q's axiom "0 is no successor" is false, and the successor is injective bad = [] for p in (5, 13, 17, 29): M = _shell_structure(p) q1 = ("all", ("all", ("neg", ("conj", ("rel", 0, (1, 0)), ("rel", 1, (0,)))))) # ∀x ∀y ¬(S x = y ∧ y = 0) inj = ("all", ("all", ("all", ("neg", ("conj", ("conj", ("rel", 0, (2, 0)), ("rel", 0, (1, 0))), ("neg", ("eq", 2, 1))))))) if fval(M, (), q1) or not fval(M, (), inj) or table(M, q1, 0) or not table(M, inj, 0): bad.append(p) R.check("Q2", "the shells 5, 13, 17 and 29 with the successor x ↦ x + 1 as a relation: the successor is injective and Q's axiom " "∀x S x ≠ 0 is false, by both evaluators: the shell interprets no Q through its successor", not bad, f"exceptions {bad}") # Q3 sentences of the shell 𝔽_13 decided: 2 000 random sentences, each true or false, never both M = _shell_structure(13) bad, true = [], 0 for _ in range(2000): phi = ("all", random_formula(rng, 4, 1)) v = fval(M, (), phi) true += v if v == fval(M, (), ("neg", phi)) or v != (() in table(M, phi, 0)): bad.append(phi) R.check("Q3", "the shell 𝔽₁₃ with its successor, its zero and its doubling: 2 000 random sentences, each decided by both " "evaluators, exactly one of σ, ¬σ true", not bad, f"{true} true, {2000 - true} false") if __name__ == "__main__": blocks = [a for a in sys.argv[1:] if a in R.blocks] if blocks: for b in blocks: R.run_block(b) sys.exit(0 if R.summary(write=False) else 1) sys.exit(0 if R.verify_all() else 1)