"""master/flavour — a ledger file of the master's rows G15, G17 and P3, the flavour rows the flavour theme proves
(28-flavour's migration, 17 October 2026; the author's decision D7 of its blueprint).

The master's block G is bound by several files, one per theme whose key file proves its rows (task LM25): the
interactions file binds G11, G12 and G16, this file binds G15 (flavour, structure) and G17 (flavour, exact ratios), and
the prediction row P3 (flavour, targets) from docs/predictions.json (BLOCK = "GP"). It holds the table of keys
(generated from docs/00-ledger.json and docs/predictions.json by ci/make_ledgers.py), the Lean proofs each core key
conjoins (PROOFS: G15, G17), the Mathlib theorems P3's key conjoins (CHART), and the checks, which call the flavour
theme (frc/flavour.py), the horizon theme (frc/ladder.py) and the chart theme (frc/chart_flavour.py). The Lean side is
lean/FrcCore/Theme/Flavour.lean and lean/FrcLedger/Theme/Flavour.lean, the key files lean/FrcCore/Keys/Flavour.lean and
lean/FrcLedger/Keys/Chart.lean, the certificates lean/FrcCore/Ledgers/Master/Flavour.lean and
lean/FrcLedger/Ledgers/Master/Flavour.lean. The paper's own checks are frc/ledgers/p28_flavour.py.

    python3 -m frc.ledgers.master.flavour        every block, the census; exit 1 if a check fails
    python3 -m frc.ledgers.master.flavour F      one block (F, R or T)

Blocks:  F  flavour, structure: the seesaw's transpose fixed point and the closed role ladder     EXACT  (00:G15)
         R  flavour, exact ratios: the norms, the colour count, the magic matrix, the texture      EXACT  (00:G17)
         T  flavour, targets: the double ratio and the m₁ = 0 floor                                CHART  (00:P3)

The notebook frc/ledgers/master/flavour.ipynb runs one row per cell, the cell's id its key (gate G13).
"""
import random
import sys
from fractions import Fraction as Q

from frc.registry import Registry
from frc import arith
from frc import flavour as FL
from frc import ladder as LD
from frc import chart_flavour as CFL

# ---- generated by ci/make_ledgers.py from docs/00-ledger.json and docs/predictions.json; edit the ledger, not this table ----
BLOCK = "GP"
KEYS = {"G1": "p00178", "G2": "p00067", "G3": "p00068", "G4": "p00069", "G5": "p00070", "G6": "p00071", "G7": "p27043", "G8": "p00073", "G9": "p00074", "G10": "p00075", "G11": "p27020", "G12": "p00155", "G13": "p00078", "G14": "p00079", "G15": "p00080", "G16": "p00081", "G17": "p00179", "G18": "p00083", "G19": "p00088", "G20": "p00089", "G21": "p00090", "P1": "p00133", "P2": "p00061", "P3": "p00180", "P4": "p00091"}       # every row of the blocks: its label and its accession key
LEAN = {"G15": "core", "G17": "core", "P3": "ml"}       # 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 core key conjoins (lean/make_keys.py writes
# the keys FRC.Ledger.p<key> from them).
PROOFS = {
    "G15": ["FRC.Flavour.transpose_fixed_point", "FRC.Flavour.seesaw_circulant", "FRC.Interactions.koide_two_thirds",
            "FRC.Ladder.tower_reduces"],
    "G17": ["FRC.Interactions.koide_two_thirds", "FRC.Flavour.norm_one_sub_i", "FRC.Flavour.norm_one_sub_omega",
            "FRC.Flavour.colour_count", "FRC.Flavour.trimaximal", "FRC.Flavour.jarlskog_sq", "FRC.Flavour.texture_exponents",
            "FRC.Flavour.trace_double", "FRC.Flavour.trace_triple"],
}

# The Mathlib theorems of P3's key: the chart clauses it conjoins (the readings of measured data).
CHART = {
    "P3": ["FRC.FlavourML.gj_ratio", "FRC.FlavourML.neutrino_floor"],
}

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

LEDGER = {"F1": "00:G15", "F2": "00:G15", "R1": "00:G17", "R2": "00:G17", "T1": "00:P3"}
BLOCKS = {"F": "flavour, structure: the seesaw's transpose fixed point and the closed role ladder",
          "R": "flavour, exact ratios: the norms, the colour count, the magic matrix, the texture",
          "T": "flavour, targets: the double ratio and the m₁ = 0 floor"}
PREDICATES = {"00:G15": "F1", "00:G17": "R1", "00:P3": "T1"}

R = Registry("00", "flavour", LEDGER, PREDICATES, sources=[__file__])
RNG = random.Random(17)
SHELLS = (17, 53, 89)


def _within(x, centre, tol): return abs(Q(x) - Q(centre)) < Q(tol)


# ------------------------------------------------------------------------------------------------------------
# block F: flavour, structure (00:G15)
@R.block("F", BLOCKS["F"])
def block_F():
    """Block F — flavour, structure (EXACT): F1, F2."""
    # F1 the seesaw fixes Q_ν = 2/3: with M_R = c m_D the seesaw collapses to c² det(m_D) m_Dᵀ (20 random rational
    #    circulants), the transpose circulant has the Dirac eigenvalues, and the signed Koide identity holds for them
    ok = True
    for _ in range(20):
        mD = FL.random_circ(RNG); c = Q(RNG.randint(1, 9), RNG.randint(1, 5))
        ok &= FL.transpose_fixed_point(c, mD) and FL.seesaw_closure(mD, FL.random_circ(RNG))[0]
        a, b = FL.QOmega(Q(RNG.randint(1, 9))), FL.QOmega(Q(RNG.randint(-9, 9), RNG.randint(1, 5)), Q(RNG.randint(-9, 9), RNG.randint(1, 5)))
        ok &= FL.transpose_eigen(a, b, b.conj())
        lam = [l.x for l in FL.eigenvalues(a, b, b.conj())]
        ok &= (3 * sum(x * x for x in lam) == 2 * sum(lam) ** 2) == (2 * b.norm() == a.x * a.x)
    for p in SHELLS:                                                          # the Dirac amplitude: Q = 2/3 exactly on the shells
        S = FL.Shell(p); ok &= S.koide_point(1, Q(1, 2))[1] == S.frac(Q(2, 3))
    # 00:G15 (p00080)
    R.check("F1", "the seesaw fixes Q_ν = 2/3: with M_R = c m_D (the 126 alignment) the seesaw m_D·adj(M_R)·m_Dᵀ is c² det(m_D) m_Dᵀ, "
            "whose eigenvalues are the Dirac eigenvalues λ_{−k} (20 random rational circulants), so the colourless Dirac amplitude "
            "2N(b) = a², Q = 2/3 exact on F_17, F_53, F_89, is the neutrinos' (the transpose fixed point)", ok,
            "the seesaw of circulants is circulant; the amplitude is preserved, the phase reset")

    # F2 the role-ladder ordering and the mixing's reduction: the ladder of roles closes on F_13, F_53, F_157, F_421 (no
    #    fifth role; the three generative roles the generations), the role depths (2, 1, 0) give the texture exponents,
    #    and the trimaximal column is the protected one
    ok = True
    for p in (13, 53, 157, 421):
        g, n = arith.primitive_root(p), p - 1
        ok &= all(LD.tower(g, j, p)[0] == LD.tower(g, j, p)[1] for j in range(n)) and any(pow(g, j, p) >= n for j in range(n))
    down, up, Ed, Eu = FL.texture_exponents(); v, u, notprop = FL.protected_column()
    ok &= down == (4, 2, 0) and up == (8, 4, 0) and v and u and notprop
    R.check("F2", "the role-ladder ordering and the mixing's reduction: the tower g^(g^j) is read modulo p − 1 on F_13, F_53, F_157, "
            "F_421 (the ladder closes, three generative roles), the depths (2, 1, 0) give the exponents (4, 2, 0) and (8, 4, 0) of "
            "the role-depth texture, and the shift fixes the trimaximal column (1, 1, 1) alone", ok, "the mixing reduces to the "
            "texture, the lopsided entry and the protected column; the phases stay Ω-hard (Z6)")


# ------------------------------------------------------------------------------------------------------------
# block R: flavour, exact ratios (00:G17)
@R.block("R", BLOCKS["R"])
def block_R():
    """Block R — flavour, exact ratios (EXACT): R1, R2."""
    # R1 Koide 2/3 and the norms: Q = 2/3 ⟺ 2N(b) = a² and N(1 − i) = 2, N(1 − ω) = 3 on the shells; the colour count 3;
    #    the magic matrix trimaximal with J² = 1/108 in Q(ω) and 4(−νh²) = 3 in F_p
    ok = all(FL.norms_two_three(p) and FL.jarlskog_framed(p) for p in SHELLS)
    for p in SHELLS:
        S = FL.Shell(p); ok &= S.koide_point(1, Q(1, 2))[1] == S.frac(Q(2, 3)) and S.koide_point(1, Q(3, 4))[1] == S.frac(Q(5, 6))
    dc, ec, nine = FL.colour_count(); tri, q, J2 = FL.magic_matrix()
    ok &= (dc, ec, nine) == (3, 1, 9) and tri and q and J2 == Q(1, 108)
    # 00:G17 (p00179)
    R.check("R1", "the exact ratios: Q = 2/3 exactly at 2N(b) = a² and Q = 5/6 at 4N(b) = 3a² on F_17, F_53, F_89; the squared "
            "amplitudes N(1 − i) = 2 and N(1 − ω) = 3; the Georgi–Jarlskog factor the colour count 3 against 1 on the sixteen; the "
            "magic matrix trimaximal with J² = 1/108 in Q(ω) and 4(−νh²) = 3 in F_p", ok,
            "the split and non-split norms, the colour triplet, the cube-root phase")

    # R2 the λ-texture from role depths and the locks: the exponents (4, 2, 0), (8, 4, 0); the lock relations as trace
    #    identities on every unit of F_{p²}
    down, up, Ed, Eu = FL.texture_exponents()
    ok = down == (4, 2, 0) and up == (8, 4, 0) and all(FL.trace_relations(p) for p in SHELLS)
    R.check("R2", "the λ-texture from the role depths (2, 1, 0): the exponents (4, 2, 0) and (8, 4, 0); the charged sectors' lock "
            "1 : 1/2 : 1/3 as the trace relations T(z²) = T(z)² − 2, T(z³) = T(z)³ − 3T(z) of a unit, exhaustive on F_{17²}, F_{53²}, "
            "F_{89²}", ok, "c_ℓ = 2c_d² − 1 = 4c_u³ − 3c_u between the cube invariants")


# ------------------------------------------------------------------------------------------------------------
# block T: flavour, targets (00:P3)
@R.block("T", BLOCKS["T"])
def block_T():
    """Block T — flavour, targets (CHART): T1."""
    gj, msd, btau = CFL.gj_double_ratio(); tot, m2, m3 = CFL.neutrino_floor(); dl, dd, du, dup = CFL.phase_lock()
    ok = _within(gj, "10.34", "0.02") and Q("0.10") < Q(gj) / 9 - 1 < Q("0.20") and _within(tot, "58.8", "0.05")
    ok &= _within(Q(dd) / Q(dl), "0.496", "0.002") and _within(Q(du) / Q(dl), "0.335", "0.002")
    # 00:P3 (p00180)
    R.check("T1", "[chart] the flavour targets: the Georgi–Jarlskog double ratio 10.34 against 9 (the open 15 % excess, between 10 % "
            "and 20 %); the m₁ = 0 floor Σm_ν = 58.8 meV at NuFIT 6.0; the locks 0.496 and 0.335 in the MS-bar working scheme", ok,
            f"double ratio {gj:.2f}, floor {tot:.1f} meV, locks {dd / dl:.3f}, {du / dl:.3f}", kind="CHART")


if __name__ == "__main__":
    want = [a.upper() for a in sys.argv[1:]] or sorted(BLOCKS)
    bad = [b for b in want if b not in BLOCKS]
    if bad: sys.exit(f"no block {', '.join(bad)}: the blocks are {', '.join(sorted(BLOCKS))}")
    for b in want: R.run_block(b)
    sys.exit(0 if R.summary(write=False, expect=list(LEDGER) if want == sorted(BLOCKS) else None) else 1)