"""master/quantum — a ledger file of the master's block F, quantum: the rows the quantum theme proves (ledger migration,
task LM28, 6 October 2026).

The master's block F is bound by this file (the quantum theme). It binds F2, multi-body registration, and F5, the graded registration law (task LM42, 7 October 2026; its source 39-s173 is
unpublished, named and not linked, Q04): the table of keys
(generated from docs/00-ledger.json by ci/make_ledgers.py), the Lean proofs its key conjoins (PROOFS), the cycles, and
the checks, which call the quantum theme (frc/quantum.py). The Lean side is lean/FrcCore/Theme/Quantum.lean, the key
file lean/FrcCore/Keys/Quantum.lean and the certificate lean/FrcCore/Ledgers/Master/Quantum.lean.

    python3 -m frc.ledgers.master.quantum        every block, the census; exit 1 if a check fails

Blocks:  J  the unequal-cycle composite: joint recurrence, gcd offset, dephasing     EXACT  (00:F2)
         R  the graded registration law: depth, home, sign, visibility              EXACT  (00:F5)

The notebook frc/ledgers/master/quantum.ipynb runs one row per cell, the cell's id its key (gate G13).
"""
import random
import sys
from math import gcd, lcm

from frc import arith
from frc.registry import Registry
from frc.quantum import joint_period, orbits, offset, reach, root_of_unity, character_sums, components, depth, home

# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----
BLOCK = "F"
KEYS = {"F1": "p00059", "F2": "p00191", "F4": "p00062", "F5": "p00194", "F6": "p00064"}       # every row of the block: its label and its accession key
LEAN = {"F2": "core", "F5": "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 = {
    "F2": ["FRC.Quantum.joint_recurrence", "FRC.Quantum.joint_least", "FRC.Quantum.pair_offset",
           "FRC.Quantum.dephasing"],
    "F5": ["FRC.Quantum.absorbed", "FRC.Quantum.unique_home", "FRC.Quantum.two_part_homes", "FRC.Quantum.sign_both",
           "FRC.Quantum.visibility_cap", "FRC.Quantum.registration_instances"],
}

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

PAIRS = 30                      # every pair of periods a, b ≤ PAIRS
TRIPLES = 10                    # every triple of periods ≤ TRIPLES

SUBJECTS = 6000                 # the Subjects p ≡ 1 (mod 4) with κ odd below it, every Object q ≡ 1 (mod 4) with q² < p

LEDGER = {"J1": "00:F2", "J2": "00:F2", "J3": "00:F2", "R1": "00:F5", "R2": "00:F5", "R3": "00:F5"}
BLOCKS = {"J": "the unequal-cycle composite: joint recurrence, gcd offset, dephasing",
          "R": "the graded registration law: depth, home, sign, visibility"}
PREDICATES = {"00:F2": "J1", "00:F5": "R1"}

R = Registry("00", "quantum", LEDGER, PREDICATES, sources=[__file__])


def _prime_1_mod(N):
    q = N + 1
    while not arith.is_prime(q): q += N
    return q


# ------------------------------------------------------------------------------------------------------------
# block J: the unequal-cycle composite (00:F2)
# the joint recurrence is the lcm of the periods; two joint states share an orbit exactly when their offsets agree
# modulo g, g T = a b; every character the drive moves sums to zero over every joint recurrence (Quantum.lean:
# joint_recurrence, joint_least, pair_offset, dephasing).
@R.block("J", BLOCKS["J"])
def block_J():
    """Block J — the unequal-cycle composite (EXACT): J1–J3."""
    # 00:F2 (p00060)
    bad = []
    for a in range(1, PAIRS + 1):
        for b in range(1, PAIRS + 1):
            T = joint_period([a, b])
            g = a * b // T
            orbs = orbits(a, b)
            ok = T == lcm(a, b) and g == gcd(a, b) and g * T == a * b
            ok &= all((t % a == 0 and t % b == 0) == (t % T == 0) for t in range(3 * a * b))
            ok &= len(orbs) == g and all(len(o) == T for o in orbs)
            ok &= all(len({offset(x, y, g) for x, y in o}) == 1 for o in orbs)
            ok &= len({offset(o[0][0], o[0][1], g) for o in orbs}) == g
            if not ok: bad.append((a, b))
    bad3 = [(a, b, c) for a in range(1, TRIPLES + 1) for b in range(1, TRIPLES + 1) for c in range(1, TRIPLES + 1)
            if joint_period([a, b, c]) != lcm(a, b, c)]
    R.check("J1", f"every pair of periods a, b ≤ {PAIRS}: the joint recurrences are exactly the multiples of T = lcm(a, b); "
            "the joint drive has g = gcd(a, b) orbits of T states, g T = a b, each orbit one offset class (x − y) mod g, "
            f"the g classes all occupied; every triple ≤ {TRIPLES}: the joint period is lcm(a, b, c)", not bad and not bad3,
            f"{PAIRS * PAIRS} pairs, {TRIPLES ** 3} triples; exceptions {bad[:3]} {bad3[:3]}")
    # J2 a second method: reachability by search against the offset criterion, random pairs up to 200
    rng = random.Random(28)
    bad = []
    for _ in range(300):
        a, b = rng.randrange(1, 200), rng.randrange(1, 200)
        g = gcd(a, b)
        x, y, x2, y2 = rng.randrange(a), rng.randrange(b), rng.randrange(a), rng.randrange(b)
        if (reach(x, y, x2, y2, a, b) is not None) != ((x + y2) % g == (x2 + y) % g): bad.append((a, b))
    R.check("J2", "300 random pairs of periods below 200 and random states: a chronon carries (x, y) to (x', y') exactly when "
            "(x + y') ≡ (x' + y) mod g, by search", not bad, f"exceptions {bad[:3]}")
    # J3 dephasing: every character of ℤ/a × ℤ/b in 𝔽_q, q ≡ 1 (mod lcm(a, b))
    tot, moved, bad = 0, 0, []
    for a, b in [(4, 6), (12, 232), (5, 7), (8, 12), (10, 14)]:
        T = lcm(a, b); q = _prime_1_mod(T)
        for M in (T, a * b):
            sums = character_sums(q, a, b, M)
            tot += len(sums)
            moved += sum(1 for m, _ in sums if m)
            if not all((s == 0) if m else (s == M % q) for m, s in sums): bad.append((a, b, M))
    R.check("J3", "the cycles (4, 6), (12, 232), (5, 7), (8, 12), (10, 14) in 𝔽_q with q ≡ 1 mod lcm: every character the drive "
            "moves sums to zero along it over one joint period T and over the product period a b; the others give T or a b",
            not bad, f"{moved} of {tot} character sums cancel; exceptions {bad}")




# ------------------------------------------------------------------------------------------------------------
# block R: the graded registration law (00:F5; 39-s173, rows B1–B5)
# an Object component ℓᵃ registers at depth d = ord_{ℓᵃ}(p): d = 1 absorbed in C_{p−1}, its image unique; d = 2 for odd
# ℓ on the boost torus C_{p+1}, the home unique (gcd(p − 1, p + 1) = 2); a 2-component past the quarter off both tori;
# the sign on both faces; the cap 2 where p² < Ω < p³ (Quantum.lean: absorbed, unique_home, two_part_homes, sign_both,
# visibility_cap, registration_instances).
@R.block("R", BLOCKS["R"])
def block_R():
    """Block R — the graded registration law (EXACT): R1–R3."""
    # 00:F5 (p00194)
    bad, n_towers, n_comp, seen = [], 0, 0, {"absorbed": 0, "torus": 0, "quadratic": 0, "beyond": 0}
    for p in range(13, SUBJECTS, 4):
        if not arith.is_prime(p) or ((p - 1) // 4) % 2 == 0: continue
        for q in range(5, p, 4):
            if q * q >= p: break
            if not arith.is_prime(q): continue
            n_towers += 1
            for face in (q - 1, q + 1):
                for l, a, n in components(face):
                    n_comp += 1
                    d, h = depth(n, p), home(n, p)
                    seen[h] += 1
                    ok = (d == 1) == (h == "absorbed")                                   # d = 1 iff absorbed
                    if l > 2: ok &= (d == 2) == (h == "torus")                          # odd ℓ: d = 2 iff on the boost torus
                    else: ok &= (n <= 4) == (h == "absorbed") and h != "torus" if n > 2 else h == "absorbed"
                    ok &= (h != "quadratic" or d == 2) and (h != "beyond" or d > 2)
                    if not ok: bad.append((q, p, n, d, h))
            ok = pow(p - 1, p - 1, p) == 1 and pow(p - 1, p + 1, p) == 1 and gcd(p - 1, p + 1) == 2
            if not ok: bad.append((q, p, "sign"))
    R.check("R1", f"every Subject p ≡ 1 (mod 4) with κ odd below {SUBJECTS}, every Object q ≡ 1 (mod 4) prime with q² < p, every "
            "primary component ℓᵃ of q − 1 and q + 1: depth 1 iff absorbed in C_{p−1}; for odd ℓ depth 2 iff on the boost torus "
            "C_{p+1}, gcd(p − 1, p + 1) = 2; the 2-components 2 and 4 absorbed, 8 and beyond on neither torus; the sign on both "
            "faces", not bad, f"{n_towers} towers, {n_comp} components {seen}; exceptions {bad[:3]}")
    # R2 the instances (39:B2, B3, B5): decided directly
    roots4 = sorted(x for x in range(1, 173) if pow(x, 4, 173) == 1)
    ok = (depth(7, 173), depth(7, 181), depth(7, 197)) == (6, 2, 1) and roots4 == [1, 80, 93, 172]
    ok &= home(4, 173) == "absorbed" and home(3, 173) == "torus" and home(7, 173) == "beyond"           # hydrogen, q = 13
    ok &= all(depth(n, 173) <= 2 for f in (4, 6) for _, _, n in components(f))                           # the proton, q = 5
    ok &= 5 * 5 > 13                                                                                      # (5, 13) refused
    R.check("R2", "the instances: the depth of hydrogen's interior 7 is 6 at 173, 2 at 181, 1 at 197; the quarter absorbed at 173 "
            "with the images {1, 80, 93, 172}, the triality on the torus, the 7 beyond; the proton whole (depth ≤ 2); (5, 13) "
            "refused, 25 > 13", ok, f"4th roots of unity in 𝔽_173: {roots4}")
    # R3 the cap: p² < Ω < p³ on the minimal tower and the laboratory tower; every saturating tower p² < Ω ≤ (p + 1)²
    ok = 173 ** 2 < 30089 <= 174 ** 2 and 30089 < 173 ** 3 and 1373 ** 2 < 2408561 < 1373 ** 3
    ok &= all((p + 1) ** 2 < p ** 3 for p in range(3, 2000))
    R.check("R3", "the visibility cap 2: (173, 30 089) saturating, 173² < Ω ≤ 174² < 173³; the laboratory (1 373, 2 408 561) "
            "with p² < Ω < p³; (p + 1)² < p³ for every 3 ≤ p < 2000", ok, "")

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)