"""master/chart — the ledger file of the chart clauses of the master's rows A7, L1, L3, L8 and P1: the readings the
chart theme certifies (ledger migration, task LM30, 6 October 2026; A7 bound 8 October 2026).

The chart theme serves the scale import, the cosmology rows and the prediction rows, so this file binds rows of three
blocks, A, L and P (BLOCK = "ALP"). The rows are an import (A7), realisations (L1, L3, L8) and a prediction (P1): A7's
datum is used without reproof and the file binds its chart numerals, S and Ω from the fit's Λ and the Planck length,
and derives the ledger's ln Ω = 283.5, the numeral L8's tilt reads; each other row is staked by a chart computation, and the file binds that computation, not the realisation. It holds the table of keys (generated from docs/00-ledger.json and, for the
prediction rows, docs/predictions.json by ci/make_ledgers.py), the Mathlib theorems each row's key conjoins (CHART), and
the checks, which call the chart theme (frc/chart.py). The Lean side is lean/FrcLedger/Theme/Chart.lean, the key file
lean/FrcLedger/Keys/Chart.lean and the certificate lean/FrcLedger/Ledgers/Master/Chart.lean (tier 2: Mathlib's reals).

    python3 -m frc.ledgers.master.chart        every block, the census; exit 1 if a check fails
    python3 -m frc.ledgers.master.chart B      one block (S, A, B, C or D)

Blocks:  S  the scale import's numerals S = 3π/(Λ ℓ_P²), Ω = 4S + 1; the ledger's ln Ω   CHART  (00:A7, L8)
         A  the floor a₀ = cH₀/2π at the entailed rate                                CHART  (00:L1)
         B  the octant record depth and its outputs: Ω_Λ, the locus, H₀                CHART  (00:L3)
         C  the primordial tilt at the ledger's ln Ω                                   CHART  (00:L8)
         D  the running floor a₀(z) ∝ H(z) and the Tully–Fisher zero-point            CHART  (00:P1)

Each block decides its row in exact rational arithmetic (the certified brackets) and corroborates it in floating point.
The notebook frc/ledgers/master/chart.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 chart as C

# ---- generated by ci/make_ledgers.py from docs/00-ledger.json and docs/predictions.json; edit the ledger, not this table ----
BLOCK = "ALP"
KEYS = {"A1": "p00001", "A2": "p00004", "A3": "p00003", "A4": "p00197", "A5": "p00188", "A6": "p00008", "A7": "p00009", "A8": "p00010", "A9": "p00161", "A10": "p00162", "A11": "p00163", "A12": "p00164", "A13": "p00196", "L1": "p00192", "L2": "p00085", "L3": "p00193", "L4": "p00087", "L5": "p00130", "L8": "p00148", "P1": "p00133", "P2": "p00061", "P3": "p00180", "P4": "p00091"}       # every row of the blocks: its label and its accession key
LEAN = {"A7": "ml", "L1": "ml", "L3": "ml", "L8": "ml", "P1": "ml"}       # the rows with a Lean declaration: the libraries whose key files prove them
# ---- end of the generated table ----

# The Mathlib theorems of the rows' keys: the chart clauses each key conjoins (lean/make_keys.py writes the keys
# FRC.LedgerML.p<key> from them). Not PROOFS: the rows are realisations staked by a chart computation, and PROOFS binds
# theorem rows to core keys (gate G08).
CHART = {
    "A7": ["FRC.Chart.scale_import"],
    "L1": ["FRC.Chart.floor_value", "FRC.Chart.floor_fine"],
    "L3": ["FRC.Chart.octant_chart", "FRC.Chart.landing_bracket", "FRC.Chart.landing_fine", "FRC.Chart.age_rate_locus",
           "FRC.Chart.locus_bracket", "FRC.Chart.octant_inversion", "FRC.Chart.hubble_landing", "FRC.Chart.hubble_stellar"],
    "L8": ["FRC.Chart.tilt_ledger", "FRC.Chart.efold_count"],
    "P1": ["FRC.Chart.running_floor"],
}

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

LEDGER = {"S1": "00:A7", "S2": "00:A7", "S3": "00:L8",
          "A1": "00:L1", "A2": "00:L1", "B1": "00:L3", "B2": "00:L3", "C1": "00:L8", "C2": "00:L8", "D1": "00:P1", "D2": "00:P1"}
BLOCKS = {"S": "the scale import's numerals: S = 3π/(Λ ℓ_P²), Ω = 4S + 1, ln Ω",
          "A": "the floor a₀ = cH₀/2π at the entailed rate",
          "B": "the octant record depth and its outputs: Ω_Λ, the locus, H₀",
          "C": "the primordial tilt at the ledger's ln Ω",
          "D": "the running floor a₀(z) ∝ H(z) and the Tully–Fisher zero-point"}
PREDICATES = {"00:A7": "S1", "00:L1": "A1", "00:L3": "B1", "00:L8": "C1", "00:P1": "D1"}

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


def _inside(b, lo, hi):
    """lo < b[0] and b[1] < hi: the bracket b lies strictly inside (lo, hi)."""
    return lo < b[0] and b[1] < hi


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


# ------------------------------------------------------------------------------------------------------------
# block S: the scale import's chart numerals (00:A7) and the ledger's ln Ω (00:L8)
# the datum is the fit's Λ = 1.088 × 10⁻⁵² m⁻² (Planck 2018) with ℓ_P = 1.616255 × 10⁻³⁵ m: r_H = c/H_Λ = √(3/Λ),
# S = π (r_H/ℓ_P)² = 3π/(Λ ℓ_P²) = 3.3 × 10¹²², Ω = 4S + 1 = 1.3 × 10¹²³ (Chart.lean: scale_import); ln Ω = 283.5, the
# numeral L8's tilt reads, derived from the same import (ln_omega_ledger).
@R.block("S", BLOCKS["S"])
def block_S():
    """Block S — the scale import's chart numerals (CHART): S1–S3."""
    # 00:A7 (p00009)
    S, Om, ln = C.entropy_bracket(), C.omega_bracket(), C.ln_omega_bracket()
    r, h = C.horizon_radius_bracket(), C.hubble_lambda_bracket()
    ok = (_inside(S, Q("3.31e122"), Q("3.32e122")) and _inside(Om, Q("1.32e123"), Q("1.33e123"))
          and _inside(r, Q("1.660e26"), Q("1.661e26")) and _inside(h, Q("55.70"), Q("55.71"))
          and Om[0] == 4 * S[0] + 1 and Om[1] == 4 * S[1] + 1)
    R.check("S1", "in rational arithmetic (π by Machin): from Λ = 1.088 × 10⁻⁵² m⁻² and ℓ_P = 1.616255 × 10⁻³⁵ m, 1.660 < r_H/10²⁶ m < 1.661 "
            "and 55.70 < H_Λ < 55.71 km/s/Mpc; 3.31 < S/10¹²² = 3π/(Λ ℓ_P²)/10¹²² < 3.32, the row's 3.3 × 10¹²²; Ω = 4S + 1 with "
            "1.32 < Ω/10¹²³ < 1.33, the row's 1.3 × 10¹²³",
            ok, f"S in ({C.show(S[0], '.6e')}, {C.show(S[1], '.6e')}); Ω in ({C.show(Om[0], '.6e')}, {C.show(Om[1], '.6e')})", kind="CHART")
    # S2 floating point, and the paper's reading: 14-entropy's instrument 1 tabulates r_H = 1.66 × 10²⁶ m, S = 3.3 × 10¹²²
    Sf = Q(C.entropy())
    ok = (_near(Sf, S[0], S[0] / 10 ** 12) and _near(Sf, Q("3.3e122"), Q("0.05e122")) and _near(4 * Sf + 1, Q("1.3e123"), Q("0.05e123")))
    R.check("S2", "floating point: S agrees with the rational bracket to 10⁻¹²; within half a unit of the row's rounded numerals "
            "3.3 × 10¹²² and 1.3 × 10¹²³", ok, f"S = {C.show(Sf, '.6e')}", kind="CHART")
    # S3 (00:L8) the ledger's constant ln Ω = 283.5, which the tilt reads, derived from the import: the bracket in rational
    # arithmetic (ln by the artanh series with the tail bound), the float to 10⁻⁹, and the constant as the bracket rounded
    lnf = Q(C.ln_omega())
    ok = (_inside(ln, Q("283.50"), Q("283.51")) and _near(lnf, ln[0], Q(1, 10 ** 9)) and _near(ln[0], C.LN_OMEGA, Q(5, 100))
          and _near(ln[1], C.LN_OMEGA, Q(5, 100)) and C.LN_OMEGA == Q(2835, 10))
    R.check("S3", "the ledger's ln Ω = 283.5 (frc/chart.py, LN_OMEGA), read by the tilt of 00:L8, derived from the import: in rational "
            "arithmetic 283.50 < ln Ω = ln(4S + 1) < 283.51, the float agrees to 10⁻⁹, and the constant is the bracket rounded to "
            "one decimal (both ends within 0.05)", ok, f"ln Ω in ({C.show(ln[0], '.6f')}, {C.show(ln[1], '.6f')}), LN_OMEGA = {C.show(C.LN_OMEGA, '.1f')}", kind="CHART")


# ------------------------------------------------------------------------------------------------------------
# block A: the floor (00:L1)
# a₀ = cH₀/2π at the channel-1 rate H₀ = 67.4 km s⁻¹ Mpc⁻¹: between 1.04 and 1.045 × 10⁻¹⁰ m s⁻², 13 % low against the
# fitted 1.20 × 10⁻¹⁰ and 0.7σ of its systematic 0.24 × 10⁻¹⁰ (Chart.lean: floor_value, floor_fine).
@R.block("A", BLOCKS["A"])
def block_A():
    """Block A — the floor (CHART): A1, A2."""
    # 00:L1 (p00084)
    a = C.floor_bracket()
    fit, err = C.A0_FIT
    ratio, deficit = (a[0] / fit, a[1] / fit), ((fit - a[1]) / err, (fit - a[0]) / err)
    ok = _inside(a, Q("1.04e-10"), Q("1.045e-10")) and _inside(ratio, Q("0.868"), Q("0.870")) and _inside(deficit, Q("0.65"), Q("0.67"))
    R.check("A1", "a₀ = cH₀/2π at the channel-1 rate H₀ = 67.4 km/s/Mpc, in rational arithmetic with π by Machin's formula: 1.04 < a₀/10⁻¹⁰ < 1.045; "
            "a₀ over the fitted 1.20 × 10⁻¹⁰ in (0.868, 0.870), 13 % low; the deficit over the systematic 0.24 × 10⁻¹⁰ in "
            "(0.65, 0.67), the row's 0.7σ", ok, f"a₀ in ({C.show(a[0], '.6e')}, {C.show(a[1], '.6e')}) m/s²", kind="CHART")
    # A2 floating point; and the floor at the landing H₀ of block B (67.35) rounds to the same 1.04 × 10⁻¹⁰
    a0, a0b = C.floor(), C.floor(C.hubble())
    ok = _near(a0, a[0], a[0] / 10 ** 12) and _near(a0b, Q("1.04e-10"), Q("0.005e-10")) and _near(C.sigma(a0, C.A0_FIT), Q("-0.66"), Q("0.01"))
    R.check("A2", "floating point: a₀ agrees with the rational bracket to 10⁻¹²; at the landing H₀ = 67.35 of the octant (00:L3) the floor is "
            "still 1.04 × 10⁻¹⁰; the deficit is −0.66σ", ok, f"a₀ = {a0:.5e}, at the landing {a0b:.5e}", kind="CHART")


# ------------------------------------------------------------------------------------------------------------
# block B: the octant record depth and its outputs (00:L3)
# the depth S/2 chronons is (π/4) r_H/c in the chart; Ω_Λ = tanh²(3π/8) = 0.684, 0.19σ from 0.685 ± 0.007; the locus
# t H₀ = (π/4)/tanh(3π/8) = 0.950; read on the stellar age 13.61 ± 0.34 Gyr it gives H₀ = 68.2 ± 1.7, the ladder's
# 73.0 ± 1.0 at 2.4σ; read on 13.79 Gyr the channel-1 67.4 (Chart.lean: octant_chart, landing_bracket, landing_fine,
# age_rate_locus, locus_bracket, octant_inversion, hubble_landing, hubble_stellar).
@R.block("B", BLOCKS["B"])
def block_B():
    """Block B — the octant record depth and its outputs (CHART): B1, B2."""
    # 00:L3 (p00181)
    rng = random.Random(30)
    conv = all((Q(S, 2) / (4 * S)) * 2 == Q(1, 4) for S in [rng.randrange(1, 10 ** 30) for _ in range(200)])   # (S/2)/(4S)·2π = π/4
    t, ol, loc = C.tanh_octant_bracket(), C.omega_lambda_bracket(), C.locus_bracket()
    h1, h0 = C.hubble_bracket(), C.hubble_bracket(C.STELLAR_AGE[0])
    err, pull = C.rate_error_bracket(), C.ladder_pull_bracket()
    dev = ((C.OMEGA_L_FIT[0] - ol[1]) / C.OMEGA_L_FIT[1], (C.OMEGA_L_FIT[0] - ol[0]) / C.OMEGA_L_FIT[1])
    ok = (conv and _inside(t, Q("0.82685"), Q("0.826851")) and _inside(ol, Q("0.68368"), Q("0.68369"))
          and _inside(dev, Q("0.186"), Q("0.19")) and _inside(loc, Q("0.949866"), Q("0.949868"))
          and _inside(h1, Q("67.35"), Q("67.36")) and _inside(h0, Q("68.24"), Q("68.25"))
          and _inside(err, Q("1.70"), Q("1.71")) and _inside(pull, Q("2.40"), Q("2.42")))
    R.check("B1", "in rational arithmetic (π by Machin, e^{3π/4} by its Taylor series with the tail bound): (S/2)/(4S) · 2π = π/4 "
            "for 200 random S; 0.82685 < tanh(3π/8) < 0.826851; 0.68368 < Ω_Λ = tanh²(3π/8) < 0.68369, between 0.186σ and 0.19σ "
            "below 0.685 ± 0.007; 0.949866 < (π/4)/tanh(3π/8) < 0.949868; on the stellar age 13.61 Gyr (Julian years) "
            "68.24 < H₀ < 68.25 km/s/Mpc, the age's ±0.34 carried to between 1.70 and 1.71, and the Cepheid ladder's "
            "73.0 ± 1.0 between 2.40σ and 2.42σ above it (errors combined with ±1.7); on 13.79 Gyr 67.35 < H₀ < 67.36",
            ok, f"Ω_Λ in ({C.show(ol[0], '.8f')}, {C.show(ol[1], '.8f')}); H₀ in ({C.show(h0[0], '.5f')}, {C.show(h0[1], '.5f')})", kind="CHART")
    # B2 floating point; the rival chart's identity lands on π/4 at Ω_Λ (the inversion, 14:C7) and the row's rounded numerals
    quarter = C.pi_bracket()[0] / 4
    age = C.lcdm_age(C.omega_lambda())
    hs = C.hubble(C.STELLAR_AGE[0])
    ok = (_near(C.omega_lambda(), ol[0], Q(1, 10 ** 12)) and _near(age, quarter, Q(1, 10 ** 12)) and _near(C.omega_lambda(), Q("0.684"), Q("0.0005"))
          and _near(hs, Q("68.2"), Q("0.05")) and _near(hs * C.STELLAR_AGE[1] / C.STELLAR_AGE[0], Q("1.7"), Q("0.05"))
          and _near(C.hubble(), Q("67.4"), Q("0.05")) and _near(C.sigma(C.omega_lambda(), C.OMEGA_L_FIT), Q("-0.19"), Q("0.005"))
          and _near(C.sigma(C.LADDER_FIT[0], (hs, (C.H0_ERR ** 2 + C.LADDER_FIT[1] ** 2) ** Q(1, 2))), Q("2.4"), Q("0.05")))
    R.check("B2", "floating point: Ω_Λ agrees with the rational bracket to 10⁻¹²; the rival chart's age (2/3) artanh √Ω_Λ equals π/4 there to "
            "10⁻¹²; the row's numerals: Ω_Λ = 0.684, −0.19σ, H₀ = 68.2 ± 1.7 on the stellar age, the ladder at 2.4σ from it, and "
            "the channel-1 67.4 on 13.79 Gyr", ok,
            f"Ω_Λ = {C.omega_lambda():.6f}, (2/3) artanh √Ω_Λ − π/4 = {C.show(age - quarter, '.1e')}, H₀ = {hs:.3f} on the stellar age", kind="CHART")


# ------------------------------------------------------------------------------------------------------------
# block C: the primordial tilt (00:L8)
# n_s − 1 = −π²/ln Ω at ln Ω = 283.5: −0.0348, +0.07σ from −0.0351 ± 0.0042; the count ½ ln Ω excluded at 8.2σ
# (Chart.lean: tilt_ledger).
@R.block("C", BLOCKS["C"])
def block_C():
    """Block C — the primordial tilt (CHART): C1, C2."""
    # 00:L8 (p00148)
    mag = C.tilt_bracket()
    fit, err = C.TILT_FIT
    dev = ((-fit - mag[1]) / err, (-fit - mag[0]) / err)
    half = C.tilt_bracket(C.LN_OMEGA / 2)
    exc = ((half[0] + fit) / err, (half[1] + fit) / err)
    ok = _inside(mag, Q("0.03481"), Q("0.03482")) and _inside(dev, Q("0.068"), Q("0.069")) and _inside(exc, Q("8.2"), Q("8.25"))
    R.check("C1", "in rational arithmetic: at ln Ω = 283.5, 0.03481 < π²/ln Ω < 0.03482 (n_s − 1 = −0.0348); the deviation from "
            "−0.0351 ± 0.0042 between +0.068σ and +0.069σ; the count ½ ln Ω off by between 8.2σ and 8.25σ", ok,
            f"π²/ln Ω in ({C.show(mag[0], '.7f')}, {C.show(mag[1], '.7f')})", kind="CHART")
    # C2 floating point; 21-gravity's own reading at ln Ω = 281 (122 ln 10) gives −0.0351 and 8.4σ, its chart
    s1, s2 = C.sigma(C.tilt(), C.TILT_FIT), C.sigma(C.tilt(C.LN_OMEGA / 2), C.TILT_FIT)
    s3 = C.sigma(C.tilt(Q(281) / 2), C.TILT_FIT)
    ok = (_near(C.tilt(), Q("-0.0348"), Q("0.00005")) and _near(s1, Q("0.07"), Q("0.005")) and _near(s2, Q("-8.2"), Q("0.05"))
          and _near(C.tilt(Q(281)), Q("-0.0351"), Q("0.00005")) and _near(s3, Q("-8.4"), Q("0.05")))
    R.check("C2", "floating point: −π²/283.5 = −0.0348, +0.07σ, ½ ln Ω at −8.2σ; at 21-gravity's ln Ω = 281 the same form "
            "gives −0.0351 and −8.4σ (the paper's reading)", ok, f"tilt {C.tilt():.5f}, {s1:+.3f}σ, half {s2:+.2f}σ; at 281: {s3:+.2f}σ",
            kind="CHART")


# ------------------------------------------------------------------------------------------------------------
# block D: the running floor (00:P1)
# a₀(z) = cH(z)/2π and v⁴ = G M a₀ give a₀(z)/a₀(0) = H(z)/H(0) and (v(z)/v(0))⁴ = H(z)/H(0): the zero-point evolves as
# E(z)^{1/4} (Chart.lean: running_floor).
@R.block("D", BLOCKS["D"])
def block_D():
    """Block D — the running floor (CHART): D1, D2."""
    # 00:P1 (p00133)
    rng = random.Random(31)
    p_lo, p_hi = C.pi_bracket()
    bad = 0
    for _ in range(300):
        pi_ = p_lo + (p_hi - p_lo) * Q(rng.randrange(1, 1000), 1000)          # any value of π: it cancels
        c, G, M = Q(C.C_LIGHT), Q(rng.randrange(1, 10 ** 6), 10 ** 16), Q(rng.randrange(1, 10 ** 6))
        H = [Q(rng.randrange(1, 10 ** 9), 10 ** 27) for _ in range(5)]          # H(z) at five redshifts, any positive values
        a = [c * h / (2 * pi_) for h in H]
        v4 = [G * M * x for x in a]                                              # v⁴ = G M a₀ at fixed baryonic mass
        bad += any(a[k] / a[0] != H[k] / H[0] or v4[k] / v4[0] != H[k] / H[0] for k in range(5))
    R.check("D1", "in rational arithmetic, 300 random cases: with a₀(z) = cH(z)/2π and v⁴ = G M a₀ at fixed M, a₀(z)/a₀(0) = "
            "H(z)/H(0) and (v(z)/v(0))⁴ = H(z)/H(0) exactly at five redshifts, for any π, c, G, M and positive H(z)",
            bad == 0, f"{bad} failures", kind="CHART")
    # D2 floating point: E(z)^{1/4} in flat ΛCDM; at 32-dark's chart Ω_Λ = 0.7 the zero-point shifts +7 %, +15 %, +31 % at
    # z = 0.5, 1, 2 (32:P1); at the octant's Ω_Λ = 0.6837 it shifts +7 %, +16 %, +32 %; a constant floor shifts nothing
    s7 = [round(100 * (C.tully_fisher_shift(z, Q(7, 10)) - 1)) for z in (Q(1, 2), 1, 2)]
    so = [round(100 * (C.tully_fisher_shift(z, C.omega_lambda()) - 1)) for z in (Q(1, 2), 1, 2)]
    ok = s7 == [7, 15, 31] and so == [7, 16, 32]
    R.check("D2", "floating point: the Tully–Fisher zero-point E(z)^{1/4} − 1 at z = 0.5, 1, 2 is +7, +15, +31 % at Ω_Λ = 0.7 "
            "(32:P1's chart) and +7, +16, +32 % at the octant's Ω_Λ = tanh²(3π/8)", ok, f"Ω_Λ = 0.7: {s7}; octant: {so}", 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)