"""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; Z9 since 25-godel's migration, 20 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 Ω, and Z9, no compression: the
table of keys (generated from docs/00-ledger.json by ci/make_ledgers.py), the Lean proofs each key conjoins (PROOFS), the
structures, and the checks, which call the logic theme (frc/logic.py, frc/diagonal.py). The Lean side is
lean/FrcCore/Theme/Logic.lean, Theme/Diagonal.lean and Theme/Threshold.lean, the key file lean/FrcCore/Keys/Logic.lean
and the certificate lean/FrcCore/Ledgers/Master/Logic.lean.

Z9's four clauses and their witnesses: (i) no instance of the diagonal per symbol (25:F2; the core's template_size,
no_template, split_scale, no_self_reading); (ii) none coded a base-a digit per symbol from t(M) = d k*(M) on (25:F6;
dense_coding, digit_bound, admits_digits, kstar_max, threshold_digits, all in digit form); (iii) below t(M) the decoders
give an instance at 1,024 base-32 symbols per element, more than Ω's elements hold (25:F7 in the core for Int_J; 25:F8
and the comparison with Ω are read against the paper's I row F8 and the chart's A7, the comparison in digit counts:
window_beyond_totality, 82 digits against 1,024); (iv) fragment truth definable from above and not from far below
(25:G5, 25:G8, both I rows of the paper since 20 October 2026, corroborated by its checks E2, G2 and G3). No numeral
above Ω is formed: the window is compared with the chart's bound by the count of its base-32 digits.

    python3 -m frc.ledgers.master.logic        every block, the census; exit 1 if a check fails (≈ 12 s)

Blocks:  Q  Gödel vacuous over a finite structure: no Q, the theory decided     EXACT  (00:Z1)
         W  no compression: per symbol, in digit form, the window's digits        EXACT  (00:Z9)

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, formulas_M2
from frc.diagonal import k_star, threshold, name_cost, dense

# ---- 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", "Z9": "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<key> 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"],
    "Z9": ["FRC.Diagonal.template_size", "FRC.Diagonal.no_template", "FRC.Diagonal.split_scale", "FRC.Diagonal.no_self_reading",
           "FRC.Logic.dense_coding", "FRC.Logic.digit_bound", "FRC.Diagonal.admits_digits", "FRC.Diagonal.kstar_max",
           "FRC.Diagonal.threshold_digits", "FRC.Diagonal.window_beyond_totality"],
}

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", "W1": "00:Z9"}
BLOCKS = {"Q": "Gödel vacuous over a finite structure: no Q, the theory decided",
          "W": "no compression: the diagonal per symbol, the threshold in digit form, the window's digits"}
PREDICATES = {"00:Z1": "Q1", "00:Z9": "W1"}

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")


# ------------------------------------------------------------------------------------------------------------
# block W: no compression (00:Z9)
# (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 truth
# depends on all of them, so every formula of length <= 9 that defines it mentions all 2N variables (25:F2's instances;
# the core's template_size and no_template give the general accounting: the diagonal formula needs more than N symbols).
# (ii) in digit form: k*(a, d) by the search of F6 (frc.diagonal.k_star, the Lean's kstar), the digit bound
# 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,
# 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) defines
# {0, ..., 2^J - 1} on the small prime fields, model-checked as written; the chart's bound of Ω (00:A7, between 1.32 and
# 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 every
# element of Ω — the comparison in digit counts, no numeral above Ω formed.
@R.block("W", BLOCKS["W"])
def block_W():
    """Block W — no compression (EXACT): W1."""
    # 00:Z9 (p00187)
    ok = True; det = []
    # (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 variables
    for N in (1, 2):
        V = 2 * N; T, _ = formulas_M2(V, 9)
        pts = list(product(range(2), repeat=N))
        def bit(assign):                                   # the assignment (x, y) of 2N bits as the index of the truth table
            return sum(b << i for i, b in enumerate(assign))
        graphs = set()
        for f in product(range(len(pts)), repeat=len(pts)):
            if len(set(f)) != len(pts): continue           # injective
            mask = 0
            for i, x in enumerate(pts):
                mask |= 1 << bit(x + pts[f[i]])
            graphs.add(mask)
        full = (1 << V) - 1; n_def = 0; n_short = 0
        for length, fs in T.items():
            for tab, free, text in fs:
                if tab in graphs:
                    n_def += 1
                    ok &= free == full                     # every defining formula mentions all 2N variables
                    ok &= len(text) > N                    # and is longer than the N-tuple it would be coded by
                if free != full and tab in graphs: n_short += 1
        ok &= len(graphs) == {1: 2, 2: 24}[N] and n_def > 0 and n_short == 0
        det.append(f"N={N}: {len(graphs)} injective graphs, {n_def} defining formulas of length <= 9, all in {V} variables")
    # (ii) k* and t in digit form over the fifteen pairs the general bound leaves, and k* = 0 below five digits
    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)]
    ok &= len(pairs) == 15
    for a, d in pairs:
        k = k_star(a, d); t = threshold(a, d)
        ok &= 0 < k < a ** (d // 3 + 4) and t == d * k and t < a ** (d - 1)
        ok &= 3 * name_cost(k, a) < d * k                  # the admitted k* passes lambda's count
    ok &= all(k_star(a, d) == 0 for a in range(2, 6) for d in range(1, 5))
    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]) + ", ...")
    # (iii) the decoders on small prime fields, and the window's digit count against the chart's bound of Ω
    dd = dense(); g = dd.Gen(); V, Ev = dd.V, dd.Ev; n_dec = 0
    for p in dd.primes_upto(31):
        J = 0
        while (1 << J) <= p:
            f = g.Int(V("x20"), J); e = Ev(p)
            ok &= {x for x in range(p) if e.ev(f, {"x20": x})} == set(range(1 << J)); n_dec += 1; J += 1
    lo, hi = 132 * 10 ** 121, 133 * 10 ** 121                # the chart's bracket of Ω (00:A7), as integers
    digits = len(_digits32(hi))                                # base-32 digits of the upper bound
    ok &= 32 ** 81 <= lo and hi < 32 ** 82 and digits == 82 and 82 < 1024
    det.append(f"{n_dec} (p, J) decoders; Ω's chart bound has {digits} base-32 digits, the instance 1024 per element")
    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) "
            "mentions all 2N variables and exceeds N symbols; k*(a, d) in digit form with t = d k* < a^(d-1) over the fifteen "
            "pairs the general bound leaves, k* = 0 below five digits; Int_J decodes {0, ..., 2^J - 1} on the prime fields up to 31; "
            "the chart's bound of Ω has 82 base-32 digits against the instance's 1024 per element", ok, "; ".join(det))


def _digits32(n):
    """The base-32 digits of n, most significant first (the count the window is compared by)."""
    out = []
    while n: out.append(n % 32); n //= 32
    return out[::-1]


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)