master.logic.py — py

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; Z9 since 25-godel's migration, 20 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 Ω, and Z9, no compression: the6table of keys (generated from docs/00-ledger.json by ci/make_ledgers.py), the Lean proofs each key conjoins (PROOFS), the7structures, and the checks, which call the logic theme (frc/logic.py, frc/diagonal.py). The Lean side is8lean/FrcCore/Theme/Logic.lean, Theme/Diagonal.lean and Theme/Threshold.lean, the key file lean/FrcCore/Keys/Logic.lean9and the certificate lean/FrcCore/Ledgers/Master/Logic.lean.1011Z9's four clauses and their witnesses: (i) no instance of the diagonal per symbol (25:F2; the core's template_size,12no_template, split_scale, no_self_reading); (ii) none coded a base-a digit per symbol from t(M) = d k*(M) on (25:F6;13dense_coding, digit_bound, admits_digits, kstar_max, threshold_digits, all in digit form); (iii) below t(M) the decoders14give an instance at 1,024 base-32 symbols per element, more than Ω's elements hold (25:F7 in the core for Int_J; 25:F815and the comparison with Ω are read against the paper's I row F8 and the chart's A7, the comparison in digit counts:16window_beyond_totality, 82 digits against 1,024); (iv) fragment truth definable from above and not from far below17(25:G5, 25:G8, both I rows of the paper since 20 October 2026, corroborated by its checks E2, G2 and G3). No numeral18above Ω is formed: the window is compared with the chart's bound by the count of its base-32 digits.1920    python3 -m frc.ledgers.master.logic        every block, the census; exit 1 if a check fails (≈ 12 s)2122Blocks:  Q  Gödel vacuous over a finite structure: no Q, the theory decided     EXACT  (00:Z1)23         W  no compression: per symbol, in digit form, the window's digits        EXACT  (00:Z9)2425The notebook frc/ledgers/master/logic.ipynb runs one row per cell, the cell's id its key (gate G13).26"""27import random28import sys29from itertools import product3031from frc.registry import Registry32from frc.logic import fval, table, random_formula, random_structure, successor_counterexample, formulas_M233from frc.diagonal import k_star, threshold, name_cost, dense3435# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----36BLOCK = "Z"37KEYS = {"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 key38LEAN = {"Z1": "core", "Z9": "core"}       # the rows with a Lean declaration: the libraries whose key files prove them39# ---- end of the generated table ----4041# The Lean proofs of the rows' keys: the theorems of the themes that each key conjoins (lean/make_keys.py writes the keys42# 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.43PROOFS = {44    "Z1": ["FRC.Logic.no_finite_successor", "FRC.Logic.no_finite_Q", "FRC.Logic.no_interpretation",45           "FRC.Logic.fin_theory_decidable", "FRC.Logic.fin_theory_complete", "FRC.Logic.fin_theory_consistent"],46    "Z9": ["FRC.Diagonal.template_size", "FRC.Diagonal.no_template", "FRC.Diagonal.split_scale", "FRC.Diagonal.no_self_reading",47           "FRC.Logic.dense_coding", "FRC.Logic.digit_bound", "FRC.Diagonal.admits_digits", "FRC.Diagonal.kstar_max",48           "FRC.Diagonal.threshold_digits", "FRC.Diagonal.window_beyond_totality"],49}5051LEAN_ONLY = ()                  # the rows with a Lean declaration and no python check (gate G12): none5253SIZES = [1, 2, 3, 4]            # the random structures' sizes54FORMULAS = 600                  # random formulas per size55MAPS = 6                        # every map [0, n) → [0, n) for n ≤ MAPS5657LEDGER = {"Q1": "00:Z1", "Q2": "00:Z1", "Q3": "00:Z1", "W1": "00:Z9"}58BLOCKS = {"Q": "Gödel vacuous over a finite structure: no Q, the theory decided",59          "W": "no compression: the diagonal per symbol, the threshold in digit form, the window's digits"}60PREDICATES = {"00:Z1": "Q1", "00:Z9": "W1"}6162R = Registry("00", "logic", LEDGER, PREDICATES, sources=[__file__])636465def _shell_structure(p):66    """The shell 𝔽_p as a relational structure: relation 0 the graph of the successor x ↦ x + 1, relation 1 the zero,67    relation 2 the graph of x ↦ 2x."""68    def rel(r, args):69        if r == 0: return len(args) == 2 and (args[0] + 1) % p == args[1]70        if r == 1: return len(args) == 1 and args[0] == 071        if r == 2: return len(args) == 2 and 2 * args[0] % p == args[1]72        return False73    return p, rel747576# ------------------------------------------------------------------------------------------------------------77# block Q: Gödel vacuous over a finite structure (00:Z1)78# a finite structure carries no injective successor missing an element, so it interprets no Q; its first-order theory is79# decided by exhaustive evaluation, complete and consistent (Logic.lean: no_finite_successor, fin_theory_decidable,80# fin_theory_complete, fin_theory_consistent).81@R.block("Q", BLOCKS["Q"])82def block_Q():83    """Block Q — Gödel vacuous over a finite structure (EXACT): Q1–Q3."""84    # 00:Z1 (p00186)85    rng = random.Random(1)86    bad, n_checked = [], 087    for m in SIZES:88        for t in range(3):89            M = random_structure(rng, m)90            for _ in range(FORMULAS // 3):91                k = rng.randrange(1, 3)92                phi = random_formula(rng, 5, k)93                T = table(M, phi, k)94                for a in product(range(m), repeat=k):95                    v, w = fval(M, a, phi), fval(M, a, ("neg", phi))96                    n_checked += 197                    if v != (a in T) or v == w: bad.append((m, phi, a))98    succ = [n for n in range(1, MAPS + 1) if successor_counterexample(n) is not None]99    R.check("Q1", f"random structures on 1–4 elements, {FORMULAS} random formulas each size: the exhaustive evaluation agrees with "100            "the satisfying tables built bottom-up, and exactly one of φ, ¬φ holds; every map [0, n) → [0, n), n ≤ "101            f"{MAPS}: none is injective and misses an element", not bad and not succ,102            f"{n_checked} evaluations; exceptions {bad[:2]}; successor counterexamples at n = {succ}")103    # Q2 the shells 𝔽_p: Q's axiom "0 is no successor" is false, and the successor is injective104    bad = []105    for p in (5, 13, 17, 29):106        M = _shell_structure(p)107        q1 = ("all", ("all", ("neg", ("conj", ("rel", 0, (1, 0)), ("rel", 1, (0,))))))    # ∀x ∀y ¬(S x = y ∧ y = 0)108        inj = ("all", ("all", ("all", ("neg", ("conj", ("conj", ("rel", 0, (2, 0)), ("rel", 0, (1, 0))), ("neg", ("eq", 2, 1)))))))109        if fval(M, (), q1) or not fval(M, (), inj) or table(M, q1, 0) or not table(M, inj, 0): bad.append(p)110    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 "111            "∀x S x ≠ 0 is false, by both evaluators: the shell interprets no Q through its successor", not bad,112            f"exceptions {bad}")113    # Q3 sentences of the shell 𝔽_13 decided: 2 000 random sentences, each true or false, never both114    M = _shell_structure(13)115    bad, true = [], 0116    for _ in range(2000):117        phi = ("all", random_formula(rng, 4, 1))118        v = fval(M, (), phi)119        true += v120        if v == fval(M, (), ("neg", phi)) or v != (() in table(M, phi, 0)): bad.append(phi)121    R.check("Q3", "the shell 𝔽₁₃ with its successor, its zero and its doubling: 2 000 random sentences, each decided by both "122            "evaluators, exactly one of σ, ¬σ true", not bad, f"{true} true, {2000 - true} false")123124125# ------------------------------------------------------------------------------------------------------------126# block W: no compression (00:Z9)127# (i) per symbol: over M_2 the graph of an injective map on M_2^N (N = 1, 2) is a relation in 2N coordinates whose truth128# depends on all of them, so every formula of length <= 9 that defines it mentions all 2N variables (25:F2's instances;129# the core's template_size and no_template give the general accounting: the diagonal formula needs more than N symbols).130# (ii) in digit form: k*(a, d) by the search of F6 (frc.diagonal.k_star, the Lean's kstar), the digit bound131# k* < a^(floor(d/3)+4) and t(a, d) = d k* < a^(d-1) over the fifteen pairs (a, d) the general bound leaves (a <= 5,132# 5 <= d <= 12 with 6 d a^(floor(d/3)+1) > a^(d-1)), and k* = 0 below five digits.  (iii) the window: Int_J(x) defines133# {0, ..., 2^J - 1} on the small prime fields, model-checked as written; the chart's bound of Ω (00:A7, between 1.32 and134# 1.33 x 10^123) has 82 base-32 digits, so one element of the instance's field, at 1,024 digits, holds more than every135# element of Ω — the comparison in digit counts, no numeral above Ω formed.136@R.block("W", BLOCKS["W"])137def block_W():138    """Block W — no compression (EXACT): W1."""139    # 00:Z9 (p00187)140    ok = True; det = []141    # (i) the graphs of the injective maps on M_2^N, N = 1, 2, among the formulas of length <= 9 over M_2 in 2N variables142    for N in (1, 2):143        V = 2 * N; T, _ = formulas_M2(V, 9)144        pts = list(product(range(2), repeat=N))145        def bit(assign):                                   # the assignment (x, y) of 2N bits as the index of the truth table146            return sum(b << i for i, b in enumerate(assign))147        graphs = set()148        for f in product(range(len(pts)), repeat=len(pts)):149            if len(set(f)) != len(pts): continue           # injective150            mask = 0151            for i, x in enumerate(pts):152                mask |= 1 << bit(x + pts[f[i]])153            graphs.add(mask)154        full = (1 << V) - 1; n_def = 0; n_short = 0155        for length, fs in T.items():156            for tab, free, text in fs:157                if tab in graphs:158                    n_def += 1159                    ok &= free == full                     # every defining formula mentions all 2N variables160                    ok &= len(text) > N                    # and is longer than the N-tuple it would be coded by161                if free != full and tab in graphs: n_short += 1162        ok &= len(graphs) == {1: 2, 2: 24}[N] and n_def > 0 and n_short == 0163        det.append(f"N={N}: {len(graphs)} injective graphs, {n_def} defining formulas of length <= 9, all in {V} variables")164    # (ii) k* and t in digit form over the fifteen pairs the general bound leaves, and k* = 0 below five digits165    pairs = [(a, d) for a in range(2, 6) for d in range(5, 13) if 6 * d * a ** (d // 3 + 1) > a ** (d - 1)]166    ok &= len(pairs) == 15167    for a, d in pairs:168        k = k_star(a, d); t = threshold(a, d)169        ok &= 0 < k < a ** (d // 3 + 4) and t == d * k and t < a ** (d - 1)170        ok &= 3 * name_cost(k, a) < d * k                  # the admitted k* passes lambda's count171    ok &= all(k_star(a, d) == 0 for a in range(2, 6) for d in range(1, 5))172    det.append("fifteen pairs: " + ", ".join(f"({a},{d}) k*={k_star(a, d)} t={threshold(a, d)}<{a ** (d - 1)}" for a, d in pairs[:4]) + ", ...")173    # (iii) the decoders on small prime fields, and the window's digit count against the chart's bound of Ω174    dd = dense(); g = dd.Gen(); V, Ev = dd.V, dd.Ev; n_dec = 0175    for p in dd.primes_upto(31):176        J = 0177        while (1 << J) <= p:178            f = g.Int(V("x20"), J); e = Ev(p)179            ok &= {x for x in range(p) if e.ev(f, {"x20": x})} == set(range(1 << J)); n_dec += 1; J += 1180    lo, hi = 132 * 10 ** 121, 133 * 10 ** 121                # the chart's bracket of Ω (00:A7), as integers181    digits = len(_digits32(hi))                                # base-32 digits of the upper bound182    ok &= 32 ** 81 <= lo and hi < 32 ** 82 and digits == 82 and 82 < 1024183    det.append(f"{n_dec} (p, J) decoders; Ω's chart bound has {digits} base-32 digits, the instance 1024 per element")184    R.check("W1", "No compression: over M_2 every formula of length <= 9 defining the graph of an injective map on M_2^N (N = 1, 2) "185            "mentions all 2N variables and exceeds N symbols; k*(a, d) in digit form with t = d k* < a^(d-1) over the fifteen "186            "pairs the general bound leaves, k* = 0 below five digits; Int_J decodes {0, ..., 2^J - 1} on the prime fields up to 31; "187            "the chart's bound of Ω has 82 base-32 digits against the instance's 1024 per element", ok, "; ".join(det))188189190def _digits32(n):191    """The base-32 digits of n, most significant first (the count the window is compared by)."""192    out = []193    while n: out.append(n % 32); n //= 32194    return out[::-1]195196197if __name__ == "__main__":198    blocks = [a for a in sys.argv[1:] if a in R.blocks]199    if blocks:200        for b in blocks: R.run_block(b)201        sys.exit(0 if R.summary(write=False) else 1)202    sys.exit(0 if R.verify_all() else 1)203