logic.py — frc/ledgers/master

1"""master/logic — a ledger file of the master's block Z, the horizon: the rows the logic theme proves (ledger migration,2task LM26, 6 October 2026).34Block Z is bound by one file per theme whose key file proves its rows: frc/ledgers/master/horizon.py (the horizon5theme) and this file (the logic theme). This file binds Z1, Gödel vacuous over the finite Ω: the table of keys6(generated from docs/00-ledger.json by ci/make_ledgers.py), the Lean proofs its key conjoins (PROOFS), the structures,7and the checks, which call the logic theme (frc/logic.py). The Lean side is lean/FrcCore/Theme/Logic.lean, the key file8lean/FrcCore/Keys/Logic.lean and the certificate lean/FrcCore/Ledgers/Master/Logic.lean.910    python3 -m frc.ledgers.master.logic        every block, the census; exit 1 if a check fails1112Blocks:  Q  Gödel vacuous over a finite structure: no Q, the theory decided     EXACT  (00:Z1)1314The notebook frc/ledgers/master/logic.ipynb runs one row per cell, the cell's id its key (gate G13).15"""16import random17import sys18from itertools import product1920from frc.registry import Registry21from frc.logic import fval, table, random_formula, random_structure, successor_counterexample2223# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----24BLOCK = "Z"25KEYS = {"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 key26LEAN = {"Z1": "core"}       # the rows with a Lean declaration: the libraries whose key files prove them27# ---- end of the generated table ----2829# The Lean proofs of the rows' keys: the theorems of the themes that each key conjoins (lean/make_keys.py writes the keys30# FRC.Ledger.p<key> from them). The master's block file is the binding's source, as a paper's \lean{} cells are its own.31PROOFS = {32    "Z1": ["FRC.Logic.no_finite_successor", "FRC.Logic.no_finite_Q", "FRC.Logic.no_interpretation",33           "FRC.Logic.fin_theory_decidable", "FRC.Logic.fin_theory_complete", "FRC.Logic.fin_theory_consistent"],34}3536LEAN_ONLY = ()                  # the rows with a Lean declaration and no python check (gate G12): none3738SIZES = [1, 2, 3, 4]            # the random structures' sizes39FORMULAS = 600                  # random formulas per size40MAPS = 6                        # every map [0, n) → [0, n) for n ≤ MAPS4142LEDGER = {"Q1": "00:Z1", "Q2": "00:Z1", "Q3": "00:Z1"}43BLOCKS = {"Q": "Gödel vacuous over a finite structure: no Q, the theory decided"}44PREDICATES = {"00:Z1": "Q1"}4546R = Registry("00", "logic", LEDGER, PREDICATES, sources=[__file__])474849def _shell_structure(p):50    """The shell 𝔽_p as a relational structure: relation 0 the graph of the successor x ↦ x + 1, relation 1 the zero,51    relation 2 the graph of x ↦ 2x."""52    def rel(r, args):53        if r == 0: return len(args) == 2 and (args[0] + 1) % p == args[1]54        if r == 1: return len(args) == 1 and args[0] == 055        if r == 2: return len(args) == 2 and 2 * args[0] % p == args[1]56        return False57    return p, rel585960# ------------------------------------------------------------------------------------------------------------61# block Q: Gödel vacuous over a finite structure (00:Z1)62# a finite structure carries no injective successor missing an element, so it interprets no Q; its first-order theory is63# decided by exhaustive evaluation, complete and consistent (Logic.lean: no_finite_successor, fin_theory_decidable,64# fin_theory_complete, fin_theory_consistent).65@R.block("Q", BLOCKS["Q"])66def block_Q():67    """Block Q — Gödel vacuous over a finite structure (EXACT): Q1–Q3."""68    # 00:Z1 (p00186)69    rng = random.Random(1)70    bad, n_checked = [], 071    for m in SIZES:72        for t in range(3):73            M = random_structure(rng, m)74            for _ in range(FORMULAS // 3):75                k = rng.randrange(1, 3)76                phi = random_formula(rng, 5, k)77                T = table(M, phi, k)78                for a in product(range(m), repeat=k):79                    v, w = fval(M, a, phi), fval(M, a, ("neg", phi))80                    n_checked += 181                    if v != (a in T) or v == w: bad.append((m, phi, a))82    succ = [n for n in range(1, MAPS + 1) if successor_counterexample(n) is not None]83    R.check("Q1", f"random structures on 1–4 elements, {FORMULAS} random formulas each size: the exhaustive evaluation agrees with "84            "the satisfying tables built bottom-up, and exactly one of φ, ¬φ holds; every map [0, n) → [0, n), n ≤ "85            f"{MAPS}: none is injective and misses an element", not bad and not succ,86            f"{n_checked} evaluations; exceptions {bad[:2]}; successor counterexamples at n = {succ}")87    # Q2 the shells 𝔽_p: Q's axiom "0 is no successor" is false, and the successor is injective88    bad = []89    for p in (5, 13, 17, 29):90        M = _shell_structure(p)91        q1 = ("all", ("all", ("neg", ("conj", ("rel", 0, (1, 0)), ("rel", 1, (0,))))))    # ∀x ∀y ¬(S x = y ∧ y = 0)92        inj = ("all", ("all", ("all", ("neg", ("conj", ("conj", ("rel", 0, (2, 0)), ("rel", 0, (1, 0))), ("neg", ("eq", 2, 1)))))))93        if fval(M, (), q1) or not fval(M, (), inj) or table(M, q1, 0) or not table(M, inj, 0): bad.append(p)94    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 "95            "∀x S x ≠ 0 is false, by both evaluators: the shell interprets no Q through its successor", not bad,96            f"exceptions {bad}")97    # Q3 sentences of the shell 𝔽_13 decided: 2 000 random sentences, each true or false, never both98    M = _shell_structure(13)99    bad, true = [], 0100    for _ in range(2000):101        phi = ("all", random_formula(rng, 4, 1))102        v = fval(M, (), phi)103        true += v104        if v == fval(M, (), ("neg", phi)) or v != (() in table(M, phi, 0)): bad.append(phi)105    R.check("Q3", "the shell 𝔽₁₃ with its successor, its zero and its doubling: 2 000 random sentences, each decided by both "106            "evaluators, exactly one of σ, ¬σ true", not bad, f"{true} true, {2000 - true} false")107108109if __name__ == "__main__":110    blocks = [a for a in sys.argv[1:] if a in R.blocks]111    if blocks:112        for b in blocks: R.run_block(b)113        sys.exit(0 if R.summary(write=False) else 1)114    sys.exit(0 if R.verify_all() else 1)115