"""master/super — a ledger file of the master's block G, the superconductivity rows: the rows the super theme proves, developed
in the master (19 October 2026; 34-super is unpublished and has no paper ledger).

The master's superconductivity rows of block G are bound by this file. It binds G19 (structure: superconductivity as
split-torus confinement — the dual map the quarter-turn transform, the charge-2 condensate a phase-singlet leaving the
residual ℤ₂ with flux h/2e, the vortex line tension vanishing at the self-dual point β* = ½ ln(1 + √2)) and G20 (duality:
the Q₄ quarter-turn on the charge–flux lattice, the Josephson–phase-slip dictionary and the metrology closure on q_c² = 4,
the Airy vortex-core ladder): the table of keys (generated from docs/00-ledger.json by ci/make_ledgers.py), the Lean
proofs each key conjoins (PROOFS), and the checks, which call the super theme (frc/super.py), the frame theme's transform
(frc/fourier.py) and, for the readings, the chart theme (frc/chart_super.py). The Lean side is
lean/FrcCore/Theme/Super.lean with the frame theme's Transform.lean, the key file lean/FrcCore/Keys/Super.lean and the
certificate lean/FrcCore/Ledgers/Master/Super.lean. Both rows are T rows of block G, so their keys are the core's; the
continuum readings (τ(β) in floating point, the universal numbers, the ladder's decimal ratio) are the rows' charts,
decided here in python alone (gate G08). The checks reproduce 34-super's scripts m1–m7 record for record.

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

Blocks:  S  structure: the dual map, the winding kernel, the residual ℤ₂, the self-dual point   EXACT, CHART  (00:G19)
         D  duality: the quarter-turn, the metrology closure, the Airy ladder                     EXACT, CHART  (00:G20)

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

from frc.registry import Registry
from frc import super as S
from frc import chart_super as CS

# ---- generated by ci/make_ledgers.py from docs/00-ledger.json; edit the ledger, not this table ----
BLOCK = "G"
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"}       # every row of the block: its label and its accession key
LEAN = {"G19": "core", "G20": "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 = {
    "G19": ["FRC.Shell.Frame.F_sq", "FRC.Shell.Frame.J_sq",                                       # 34-super C1: the dual map is the quarter-turn transform, F² = J, F⁴ = I
            "FRC.Super.winding_pairs", "FRC.Super.residual_two", "FRC.Super.self_dual_point"],     # C3, C4, C5: the inverse pairs, the residual ℤ₂, the self-dual point
    "G20": ["FRC.Super.symplectic_quarter_turn", "FRC.Super.metrology_closure", "FRC.Super.airy_ladder_sturm"],   # C9, C10, D1
}

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

LEDGER = {"S1": "00:G19", "S2": "00:G19", "D1": "00:G20", "D2": "00:G20"}
BLOCKS = {"S": "structure: the dual map, the winding kernel, the residual ℤ₂, the self-dual point",
          "D": "duality: the quarter-turn, the metrology closure, the Airy ladder"}
PREDICATES = {"00:G19": "S1", "00:G20": "D1"}

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

SUBSTRATES = [16, 28, 40, 52, 88, 100]       # q = p − 1 for the primes p ≡ 5 (mod 12) of 34-super's m1: 17, 29, 41, 53, 89, 101
FRAMES = [(17, 3), (29, 2)]                  # the shells of the first two substrates with a drive (frc.shell.generators)


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


# ------------------------------------------------------------------------------------------------------------
# block S: structure (00:G19)
@R.block("S", BLOCKS["S"])
def block_S():
    """Block S — structure: S1 the exact content (EXACT), S2 the tension and the universal numbers (CHART)."""
    # 00:G19 (p00088)
    maps = [S.dual_map(p, g) for p, g in FRAMES]
    kernels = {q: S.winding_kernel(q, 2) for q in SUBSTRATES}
    triples = {q: S.winding_kernel(q, 3)[0] for q in SUBSTRATES[:3]}
    residuals = {q: S.residual(q) for q in SUBSTRATES}
    sd = S.self_dual_point()
    dual = all(m == (True, True, True) for m in maps)
    pairs = all(kernels[q] == (q, True) for q in SUBSTRATES) and all(triples[q] == q ** 2 for q in triples)
    z2 = all(residuals[q] == [0, q // 2] for q in SUBSTRATES) and all((2 * 1) % q != 0 for q in SUBSTRATES)
    point = sd["prod"] == sd["one"] and sd["diff"] == (2, 0) and sd["tanh"] == sd["w"] and sd["quad"] == (0, 0)
    R.check("S1", "the structure's exact content: on the shells 𝔽₁₇ and 𝔽₂₉ (q = 16, 28) the dual map is the quarter-turn transform, "
            "F² = J and F⁴ = I in ℤ_p (34-super C1, Transform.lean); on every substrate q = 16, 28, 40, 52, 88, 100 the two-body "
            "composites of total winding 0 are the q inverse pairs (k, −k), the three-body ones number q² (C3); the charge-2 "
            "condensate leaves the residual {b : 2b ≡ 0 (mod q)} = {0, q/2} ≅ ℤ₂ with the unit vortex confined — the flux "
            "quantum h/2e (C4); in ℤ[√2], (1 + √2)(√2 − 1) = 1, (1 + √2) − (√2 − 1) = 2, (2 + √2)(√2 − 1) = √2 and "
            "x² − 2x − 1 = 0 at x = 1 + √2: sinh 2β* = 1, tanh β* = √2 − 1 and τ(β*) = ln 1 = 0 at β* = ½ ln(1 + √2), the "
            "Kramers–Wannier self-dual point (C5)",
            dual and pairs and z2 and point,
            f"F² = J, F⁴ = I on {[p for p, _ in FRAMES]}; kernels {dict((q, kernels[q][0]) for q in SUBSTRATES)}; residuals {residuals[16]}, {residuals[100]}; "
            f"(1+√2)(√2−1) = {sd['prod']}, tanh β* = {sd['tanh']} = √2 − 1")
    # S2 chart: the tension τ(β) = 2β + ln tanh β in floating point (m2, m3), and the universal numbers (m3, m4, m8)
    b = CS.beta_star(); r = CS.self_dual_readings(); prof, below = CS.tension_profile(); u = CS.universal_numbers()
    tiny, milli = Q(1, 10 ** 12), Q(1, 1000)
    tension = (_near(Q(r["sinh"]), 0, tiny) and _near(Q(r["tanh"]), 0, tiny) and _near(Q(r["tau0"]), 0, tiny)
               and all(v > 0 for v in prof) and all(prof[i + 1] > prof[i] for i in range(len(prof) - 1)) and below < 0
               and _near(Q(r["tau8"]), 0, Q(1, 10 ** 6)))
    involution = all(_near(Q(x), 0, tiny) for x in r["involution"]) and _near(Q(r["fixed"]), 0, tiny) and r["swap"] < 0
    numbers = _near(Q(u["jump"]), Q("0.6366197723675813"), tiny) and _near(Q(u["gap_ratio"]), Q(CS.GAP_RATIO_BCS), milli) and _near(Q(u["heat_jump"]), Q(CS.HEAT_JUMP_BCS), milli)
    R.check("S2", "[chart] β* = ½ ln(1 + √2) = 0.4407 in floating point: sinh 2β* = 1, tanh β* = √2 − 1 and τ(β*) = 0 to 10⁻¹²; the vortex "
            "line tension τ(β) = 2β + ln tanh β is positive and increasing at β* + 0.001 … β* + 2 and tends to 2β (16 at β = 8), "
            "negative at β* − 0.05: the vortex confined in the superconducting phase, deconfined at β*, which is T_c; the "
            "Kramers–Wannier map sinh 2β sinh 2β̃ = 1 is an involution with β* its fixed point, swapping the two phases; the "
            "universal numbers: the stiffness jump 2/π = 0.6366, the BCS gap ratio 2π/e^γ = 3.528, the heat jump 12/(7ζ(3)) = 1.426",
            tension and involution and numbers,
            f"β* = {CS.fmt(b, '.6f')}, τ(β*) = {CS.fmt(r['tau0'], '.1e')}, τ at β* + 0.2 = {CS.fmt(prof[2], '.4f')}; 2/π = {CS.fmt(u['jump'], '.4f')}, 2π/e^γ = {CS.fmt(u['gap_ratio'], '.4f')}, 12/(7ζ(3)) = {CS.fmt(u['heat_jump'], '.4f')}",
            kind="CHART")


# ------------------------------------------------------------------------------------------------------------
# block D: duality (00:G20)
@R.block("D", BLOCKS["D"])
def block_D():
    """Block D — duality: D1 the exact content (EXACT), D2 the ladder's decimal reading (CHART)."""
    # 00:G20 (p00089)
    turns = {q: S.symplectic(q) for q in SUBSTRATES[:2]}
    m = S.metrology()
    brackets = S.airy_ladder(200, 16, [("1.018", "1.019"), ("3.246", "3.247")], [("2.337", "2.338")])
    ev, od, (lo, hi) = brackets
    quarter = all(turns[q] == (True, True, True, True) for q in turns)
    closure = all(v.is_zero() for v in m.values())
    ladder = ev == [(0, 1), (1, 2)] and od == [(0, 1)] and Q("0.687") < lo < hi < Q("0.691") and hi < 1
    R.check("D1", "the duality's exact content: on ℤ_q ⊕ ℤ_q for q = 16 and 28, over every point, S(a, b) = (b, −a) has S² = −I and "
            "S⁴ = I, preserves the Dirac pairing ab′ − a′b (mod q) over every pair of points, and maps the condensate (2, 0) to the "
            "double flux (0, −2) and the unit vortex (0, 1) to the unit charge (1, 0): the Q₄ quarter-turn, charge ↔ flux, "
            "Wilson ↔ 't Hooft (34-super C9); as polynomial identities with e⁻¹ and h⁻¹ as variables, (2e)(h/2e) = h, the "
            "Josephson step V_n = n f/K_J = n(h/2e)f and its S-image, the phase-slip step I_n = n(2e)f, multiply to n²f²h, and "
            "the metrology triangle K_J R_K Q = (2e/h)(h/e²)Q closes on 4 = q_c² for Q = 2e and on 2 for Q = e (C10); Sturm's "
            "count of the even (Neumann) and odd (Dirichlet) finite operators −u″ + x u on N = 200 sites of [0, 16], in exact "
            "rational arithmetic, places one eigenvalue in each of (1.018, 1.019), (2.337, 2.338), (3.246, 3.247), so the vortex-core "
            "ladder has ρ = (E₃ − E₂)/(E₂ − E₁) in (0.687, 0.691) — below the equal spacing 1 of the harmonic minigap (D1)",
            quarter and closure and ladder,
            f"S on q = {list(turns)}: {turns[16]}; closures {[k for k, v in m.items() if v.is_zero()]}; counts {ev}, {od}; ρ in ({CS.fmt(lo, '.4f')}, {CS.fmt(hi, '.4f')})")
    # D2 chart: the ladder by bisection on the float Sturm counts at N = 200 and N = 400, the Airy zeros, the BCS reference
    (e1, e2, e3, rho), zeros = CS.airy_ladder(200, 16); (_, _, _, rho4), _ = CS.airy_ladder(400, 20)
    rz = CS.airy_ratio(); airy = Q("0.690")
    levels = all(_near(Q(e), Q(z), Q(2, 1000)) for e, z in zip((e1, e2, e3), zeros)) and lo < Q(rho) < hi
    reading = _near(Q(rz), airy, Q(1, 1000)) and _near(Q(rho), airy, Q(2, 1000)) and _near(Q(rho4), airy, Q(1, 1000)) and Q(rz) < Q("0.95") and abs(1 - Q(rz)) > Q(1, 4)
    spacing = (e2 - e1) > (e3 - e2) > 0
    R.check("D2", "[chart] the ladder read in floating point: at N = 200 the three levels agree with the Airy zeros |a′₁| = 1.0188, "
            "|a₁| = 2.3381, |a′₂| = 3.2482 to 2 × 10⁻³ and ρ falls inside the exact bracket; from the zeros ρ = 0.690 (34-super's "
            "m6), at N = 400 on [0, 20] ρ = 0.690 to 10⁻³; the spacings shrink (E₂ − E₁ > E₃ − E₂): the confinement reading, "
            "against ρ = 1 of the equally spaced Caroli–de Gennes–Matricon minigap, separated by more than 0.25 — the "
            "vortex-core spectroscopy that decides between them",
            levels and reading and spacing,
            f"E = ({CS.fmt(e1, '.4f')}, {CS.fmt(e2, '.4f')}, {CS.fmt(e3, '.4f')}), ρ = {CS.fmt(rho, '.4f')} (N = 200), {CS.fmt(rho4, '.4f')} (N = 400), {CS.fmt(rz, '.4f')} from the zeros; BCS 1",
            kind="CHART")


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)