Conditional kappa = 0.001283479306671789: certified R715 assembly with sharp bit charge

research/r715-certified-assembly/PROOF.md

@@ -0,0 +1,57 @@
+# Certified assembly of the R715 bit profile
+
+PR 463 records a whole-residual eleven-stage bit histogram for its R715 word
+and an exact bit root, and leaves the outer assembly uncertified. This note
+checks that root and runs the six-level balanced assembly against PR 458's
+complex root. The bad-class term is then replaced by the source bound. No
+residual is placed on two families.
+
+## Histogram
+
+PR 463's tape audit recomputes the paid-children profile
+
+```
+{1: 26914, 2: 11799, 3: 2642, 4: 3569, 5: 1254, 6: 906, 7: 630, 8: 99, 42: 1, 56: 63}
+```
+
+at `m = 78`, `W = 1200`, rank mass 93192, deficit 408, largest child 56.
+Replaying it through the inherited envelope `10^-16 * 32 m^2` reproduces
+
+```
+bit lower = 642564369945714399381 / (5 * 10^23)
+```
+
+which is the value in that audit.
+
+## Assembly and sharp charge
+
+PR 458's complex root `1297203880559577927527 / 10^24` stays strictly above
+the bit root, so the assembly binds on the bit side. With the inherited
+envelope the exponent is
+
+```
+641739651875561 / (5 * 10^17) = 0.001283479303751122
+```
+
+`notes/three-stage-cover-bit.tex` charges each bad edge at most
+`(2 m^3 / 2^80) * (6 N (N - 1) + 3 N + 6 (N - 1))` rank-one children,
+`N = 2 m`. At `m = 78` that is strictly below `10^-16 * 32 m^2`, since the
+fallback count is 146478 rather than 194688 and `2 * 78^3 * 10^16 < 2^80`.
+The sharp charge gives
+
+```
+bit lower = 642564371409803769573 / (5 * 10^23)
+kappa     = 1283479306671789 / 10^18
+          = 0.001283479306671789
+```
+
+The gain over PR 462 is `8984335486213 / 10^18`. Both interval engines put
+the sharp moment strictly below 1 at this bit root and strictly above 1 one
+`10^-24` step later. All 47 outer inequalities hold, and the next `10^-18`
+grid point does not. Every bootstrap gap is positive, so the finite cutoff
+exists for a 1664-bit coefficient charge and for a 10^6-bit charge.
+
+The column audit of the R715 word remains PR 463's. This file certifies the
+moment and the assembly of the histogram that audit published.
+
+Run `python research/r715-certified-assembly/prove.py`.

research/r715-certified-assembly/prove.py

@@ -0,0 +1,189 @@
+"""Certified assembly of the R715 bit profile with PR 458's complex root.
+
+The paid-children histogram is the one recomputed in PR 463's tape audit:
+m = 78, W = 1200, deficit 408, max child 56. The moment below uses the
+inherited bad-class envelope first, then the sharp charge from
+notes/three-stage-cover-bit.tex. The complex root is PR 458's. Residuals
+stay whole.
+"""
+import importlib.util
+from decimal import Decimal, ROUND_FLOOR, localcontext
+from fractions import Fraction as Q
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[2]
+PKG = ROOT / "research" / "five-stage-gen4-banks"
+
+PROFILE = {
+    1: 26914,
+    2: 11799,
+    3: 2642,
+    4: 3569,
+    5: 1254,
+    6: 906,
+    7: 630,
+    8: 99,
+    42: 1,
+    56: 63,
+}
+M = 78
+W = 1200
+DEFICIT = 408
+PUBLISHED_BIT = Q("642564369945714399381/500000000000000000000000")
+PUBLISHED_COMPLEX = Q("1297203880559577927527/1000000000000000000000000")
+# PR 462, the previous whole-residual leader.
+FRONTIER = Q("159311871398197/125000000000000000")
+LEAF = Q(384599, 10**10)
+ETA = BETA = GRID = Q(1, 10**18)
+CHARGED_COEFFICIENT_BITS = 1664
+PRIME = 1 << 80
+
+
+def load(name):
+    spec = importlib.util.spec_from_file_location(name, PKG / (name + ".py"))
+    mod = importlib.util.module_from_spec(spec)
+    spec.loader.exec_module(mod)
+    return mod
+
+
+def gaussian_children(m):
+    n = 2 * m
+    return 6 * n * (n - 1) + 3 * n + 6 * (n - 1)
+
+
+def moment_charge(moment, histogram, saving, children, fraction):
+    lo = hi = Q(0)
+    edges = 0
+    for rank, count in histogram.items():
+        assert 0 < rank < M and count > 0
+        edges += count
+        lower_log, upper_log = moment.logarithm(Q(M, rank))
+        lower_exp, upper_exp = moment.exponential(saving * lower_log, saving * upper_log)
+        weight = Q(rank * count, M * W)
+        lo += weight * lower_exp
+        hi += weight * upper_exp
+    lower_log, upper_log = moment.logarithm(Q(M))
+    lower_exp, upper_exp = moment.exponential(saving * lower_log, saving * upper_log)
+    weight = Q(children * edges, M * W) * fraction
+    lo += weight * lower_exp
+    hi += weight * upper_exp
+    return moment.floor(lo), moment.ceil(hi)
+
+
+def certify(moment, histogram, children, fraction):
+    edges = sum(histogram.values())
+    with localcontext() as ctx:
+        ctx.prec = 80
+        terms = [
+            (Decimal(rank * count) / Decimal(M * W), (Decimal(M) / Decimal(rank)).ln())
+            for rank, count in histogram.items()
+        ]
+        fallback = (
+            Decimal(children * edges)
+            * Decimal(fraction.numerator)
+            / Decimal(fraction.denominator)
+            / Decimal(M * W)
+        )
+        log_m = Decimal(M).ln()
+        lo = Decimal(0)
+        hi = Decimal("0.003")
+        for _ in range(240):
+            mid = (lo + hi) / 2
+            value = sum(weight * (mid * log_ratio).exp() for weight, log_ratio in terms)
+            value += fallback * (mid * log_m).exp()
+            if value < 1:
+                lo = mid
+            else:
+                hi = mid
+        proposal = int((lo * Decimal(10) ** 24).to_integral_value(rounding=ROUND_FLOOR))
+    lower = Q(proposal, 10**24)
+    while moment_charge(moment, histogram, lower, children, fraction)[1] >= 1:
+        lower -= Q(1, 10**24)
+    assert moment_charge(moment, histogram, lower, children, fraction)[1] < 1
+    upper = lower + Q(1, 10**24)
+    assert moment_charge(moment, histogram, upper, children, fraction)[0] > 1
+    return lower
+
+
+def bootstrap(bit_lower, complex_lower, charged_bits):
+    assert bit_lower < (1 - BETA) * complex_lower
+    cap = min(bit_lower, (1 - BETA) * complex_lower) - Q(1, 10**24)
+    saving = LEAF
+    for _ in range(6):
+        nxt = (1 - cap) * cap + cap * saving
+        gap = min(cap - nxt, 1 - nxt - cap, 1 - nxt - cap * (1 - saving), 1 - cap)
+        assert saving < nxt < cap < 1 - nxt and gap > 0
+        cutoff = max(-((-36) // (gap * gap)), -((-2 * (4 + charged_bits)) // gap))
+        assert cutoff * gap * gap >= 36 and cutoff * gap >= 2 * (4 + charged_bits)
+        saving = nxt
+    return saving
+
+
+def kappa_of(outer, bit_lower, complex_lower):
+    saving = bootstrap(bit_lower, complex_lower, CHARGED_COEFFICIENT_BITS)
+    # A larger finite coefficient charge still has a finite cutoff.
+    bootstrap(bit_lower, complex_lower, 10**6)
+    q = saving * (1 - 2 * ETA)
+    margin = (1 - ETA) * q / (1 + q)
+    ticks = margin / GRID
+    kappa = GRID * ((ticks.numerator - 1) // ticks.denominator)
+    bridge = {
+        "semantic": {"C0": {"base": 2, "exponent": 210000}, "strict_literal_gap": 1},
+        "rows": {"degree_gap": Q(10**6) - Q(51 * 20161, 25)},
+    }
+    assembly = outer.assembly(saving, complex_lower, bridge, kappa, eta=ETA, beta=BETA)
+    assert len(assembly["strict_constraints"]) == 47
+    assert min(assembly["strict_constraints"].values()) > 0
+    try:
+        outer.assembly(saving, complex_lower, bridge, kappa + GRID, eta=ETA, beta=BETA)
+    except AssertionError:
+        pass
+    else:
+        raise AssertionError("adjacent grid point admitted")
+    return kappa
+
+
+def main():
+    moment = load("moment")
+    other = load("base_two_moment")
+    outer = load("outer")
+    mass = sum(rank * count for rank, count in PROFILE.items())
+    edges = sum(PROFILE.values())
+    assert mass == 93192
+    assert M * W - mass == DEFICIT
+    assert max(PROFILE) == 56 and 2 * 56**3 < M**3
+
+    inherited_children = 32 * M * M
+    inherited_fraction = Q(1, 10**16)
+    children = gaussian_children(M)
+    sharp_fraction = Q(2 * M**3, PRIME)
+    assert children * sharp_fraction < inherited_children * inherited_fraction
+
+    inherited_hi = moment.moment(PROFILE, M, W, PUBLISHED_BIT, True)[1]
+    replay_hi = moment_charge(moment, PROFILE, PUBLISHED_BIT, inherited_children, inherited_fraction)[1]
+    assert inherited_hi == replay_hi
+    inherited = moment.certify(PROFILE, M, W, True)
+    assert Q(inherited["lower"]) == PUBLISHED_BIT
+    inherited_kappa = kappa_of(outer, PUBLISHED_BIT, PUBLISHED_COMPLEX)
+    assert inherited_kappa > FRONTIER
+
+    lower = certify(moment, PROFILE, children, sharp_fraction)
+    assert lower > PUBLISHED_BIT
+    assert lower < (1 - BETA) * PUBLISHED_COMPLEX
+    cross_hi = other.moment(M, W, list(PROFILE.items()), lower)[1]
+    fallback_hi = other.moment(M, W, [(1, children * edges)], lower)[1]
+    assert cross_hi + fallback_hi * sharp_fraction < 1
+    kappa = kappa_of(outer, lower, PUBLISHED_COMPLEX)
+    assert inherited_kappa == Q("641739651875561/500000000000000000")
+    assert lower == Q("642564371409803769573/500000000000000000000000")
+    assert kappa == Q("1283479306671789/1000000000000000000")
+    assert kappa > inherited_kappa
+    print("PASS R715 assembly")
+    print("inherited_kappa", inherited_kappa)
+    print("bit_lower", lower)
+    print("kappa", kappa)
+    print("gain_over_462", kappa - FRONTIER)
+
+
+if __name__ == "__main__":
+    main()