Scoped negative result: PR626 jp8 and ck A/B frames admit no next complex tick at fixed order (exact duals, no new κ)

research/complex-k492-frame-bound/README.md

@@ -0,0 +1,67 @@
+# Fixed-order A/B frame exclusion for the selected PR626 complex providers
+
+**Scoped negative result; no new κ.** Base `66849e1475c930fd7732b1a0067ffee7e1e95f60`. Sprint track: complex supplier (OS seed 23).
+
+## Claim
+
+Take the emitted programs of the two selected #626 complex providers: **jp8**, used in 64 of the 72 calls, and **ck**, used in 8. Use both orientations. The macro list, order and operands stay fixed, as do every start frame, final frame and target level, each centre chain, and the frame of every macro outside phases A and B. Any frame in F_2^9 may then be assigned to any A or B scalar macro, simultaneously. No assignment that is legal under `hpe_audit_local.py`'s frame rules yields a native complex moment below one at
+
+    b_next = 102387919519255428911/62500000000000000000000
+
+This is the next 10^-24 grid point above #626's accepted endpoint. With owners, widths, the bit supplier and the outer assembly unchanged, frame-only reassignment therefore cannot raise the binding complex endpoint, and so cannot raise the selected κ.
+
+## Proof (finite, exact)
+
+1. **Domains.** Forward joins from the fixed starts and pins give `lo_i`, and backward meets from the finals and pins give `hi_i`. Every legal frame satisfies `lo_i <= G_i <= hi_i`. In these words `dim(hi/lo) <= 3`. The verifier enumerates every subspace in each interval and checks completeness: 2, 5 or 16 choices per macro (`model.py`).
+2. **LP.** For each component of free macros, the local-polytope LP uses variables x(i,G), plus nested pair variables y on consecutive macros of a register (counted with multiplicity). Every legal assignment is a 0/1 point of this LP. Each register's total climb is fixed, so the paid local moment equals sum n_k c_k plus a constant, where c_k = k^(1-b) - k. The common positive factor m^b/(mW) is dropped.
+3. **Duals.** Each component has a rational dual whose entries are linear forms in c_2..c_9. The verifier checks two things. First, every reduced cost is >= 0 at b_next, using two rational engines: its own atanh/alternating-series engine, and the pinned repository `moment.py`. Second, the dual objective equals the literal #626 baseline as an exact coefficient-vector identity. By weak duality, every legal assignment costs at least as much as the baseline.
+4. **Global step.** Using the pinned #626 `ASSEMBLY.json` profile, both engines put the baseline global moment minus one at about +6.49e-25 at b_next. Every child term increases with b. So for each call, each reassignment has a local moment at least the baseline's at b_next, and the reassigned supplier is rejected at b_next and above.
+
+Small components (63 for jp8 and 96 for ck, per orientation) are also brute-forced over all legal assignments as an independent cross-check.
+
+## Reproduce
+
+```sh
+python3 -B research/complex-k492-frame-bound/verify.py            # committed inputs, ~30 s, stdlib only
+python3 -B research/complex-k492-frame-bound/verify.py --controls # six controls must be rejected
+```
+
+Expected: `PASS_FIXED_ORDER_AB_FRAME_EXCLUSION_PR626` and `PASS_CONTROLS 6 of 6 rejected`. `--work DIR` checks fresh outputs of `research/complex-k492-owner-repair/verify.sh DIR` instead.
+
+The inputs are the jp8/ck `CANONICAL-WORD` and `LOCAL-PROGRAMS` files. Their gzip SHA-256 equals the hashes recorded in `research/community-k492-audit/pr626/replay/mixed-global/base/providers/*/INDEPENDENT-LOCAL-REPLAY.json`, and the decompressed payload hashes are pinned in `SOURCES.json`.
+
+This was validated in two ways: the full #626 provider replay was run fresh on macOS with Python 3.12, and its outputs matched; and the verifier was run on Python 3.11 and 3.15. Running with `-O` is refused.
+
+The six controls are:
+- a dropped component
+- an inflated dual
+- an incomplete domain
+- the accepted (rather than next) endpoint
+- a legal but worse baseline, which the duals must not certify
+- the wrong word
+
+`gen_duals.py` (needs highspy/scipy) nominates the duals; it is deterministic, reproducing the pinned payload hash. `explore/exact.py` (needs ortools) solves the same exact model with CP-SAT and reports the baseline objective as optimal for both words. It is a solver cross-check, not part of the proof.
+
+## Exploratory findings (not shipped as checks)
+
+- A per-register rank-path relaxation, which drops shared geometry, leaves gaps on 410 jp8 registers.
+- A coupled dimension-only relaxation claims a large spurious gain, which shrinks after pair-span cuts but does not vanish.
+- Greedy and annealed block moves and a flag-structured frame family all found no improvement.
+
+So the geometric subspace constraints are what close the gap, which is why the full subspace LP is needed.
+
+## Scope
+
+Not covered:
+- scalar rewrites, reordering, or changed cuts or centres
+- frames of zero-frame precondition, cleanup-tail and full-frame-cleanup macros
+- changed starts or finals (and so widths), owners, hosting or the invoice
+- the bit supplier, other words (for example the open #645/#659/#685 lineages), or other outer theorems
+
+The result holds at the fixed exponent b_next, not for all exponents. All inherited all-size, compiler, realization, hosting, precision, tape and analytic assumptions remain. This is a finite certificate, not a Lean proof.
+
+## Credit
+
+The method follows chafreaky's #557 (`research/frame-domain-ceiling`, PR551 word): complete F_2 domains, an LP relaxation and symbolic exact duals. This package is a new implementation against the emitted #626 programs. Concurrent #698 (thakrarsagar) proves ck B-phase optimality at fixed end-of-B frames for all exponents; this result independently corroborates it at b_next and adds jp8, joint A/B freedom and the global next-tick exclusion. #661 (yuj1r0) is the bit analogue.
+
+The suppliers and their lineage are Jeremy Kothe (#622), Chafik Boukhalfa (#626), DreamingOfClouds, icekylinx and the selected-record contributors. Prepared with substantial AI assistance (Anthropic Claude). Apache-2.0.

research/complex-k492-frame-bound/RESULT.json

@@ -0,0 +1,102 @@
+{
+  "accepted_complex_endpoint": "65528268492323474503/40000000000000000000000",
+  "excluded_complex_endpoint": "102387919519255428911/62500000000000000000000",
+  "global_moment_minus_one_at_excluded": {
+    "engine_a": [
+      "0.0000000000000000000000006493109174788603",
+      "0.0000000000000000000000006493109174788604"
+    ],
+    "repo_engine": [
+      "0.0000000000000000000000006493109174788603",
+      "0.0000000000000000000000006493109174788604"
+    ]
+  },
+  "programs": {
+    "ck/backward": {
+      "brute_forced_components": 96,
+      "brute_forced_legal_assignments": 629,
+      "components": 114,
+      "distinct_reduced_cost_forms": 543,
+      "domain_frames": 2694,
+      "free_macros_with_choices": 884,
+      "local_profile": {
+        "1": 2596,
+        "2": 552,
+        "3": 304,
+        "4": 160,
+        "5": 70,
+        "6": 8,
+        "8": 8
+      },
+      "lp_columns": 9713,
+      "lp_rows": 7288,
+      "macros": 22748,
+      "register_rank_mass": 5650
+    },
+    "ck/forward": {
+      "brute_forced_components": 96,
+      "brute_forced_legal_assignments": 629,
+      "components": 114,
+      "distinct_reduced_cost_forms": 543,
+      "domain_frames": 2694,
+      "free_macros_with_choices": 884,
+      "local_profile": {
+        "1": 2596,
+        "2": 552,
+        "3": 304,
+        "4": 160,
+        "5": 70,
+        "6": 8,
+        "8": 8
+      },
+      "lp_columns": 9713,
+      "lp_rows": 7288,
+      "macros": 22748,
+      "register_rank_mass": 5650
+    },
+    "jp8/backward": {
+      "brute_forced_components": 63,
+      "brute_forced_legal_assignments": 133,
+      "components": 81,
+      "distinct_reduced_cost_forms": 432,
+      "domain_frames": 3518,
+      "free_macros_with_choices": 1296,
+      "local_profile": {
+        "1": 2512,
+        "2": 400,
+        "3": 448,
+        "4": 160,
+        "5": 70,
+        "6": 8,
+        "8": 8
+      },
+      "lp_columns": 12433,
+      "lp_rows": 10228,
+      "macros": 23505,
+      "register_rank_mass": 5694
+    },
+    "jp8/forward": {
+      "brute_forced_components": 63,
+      "brute_forced_legal_assignments": 133,
+      "components": 81,
+      "distinct_reduced_cost_forms": 432,
+      "domain_frames": 3518,
+      "free_macros_with_choices": 1296,
+      "local_profile": {
+        "1": 2512,
+        "2": 400,
+        "3": 448,
+        "4": 160,
+        "5": 70,
+        "6": 8,
+        "8": 8
+      },
+      "lp_columns": 12433,
+      "lp_rows": 10228,
+      "macros": 23505,
+      "register_rank_mass": 5694
+    }
+  },
+  "scope": "Every simultaneous reassignment of A/B scalar-macro frames of the emitted PR626 jp8 and ck provider programs, with macro list/order/operands, starts, finals, target levels, centre chains and all non-A/B macro frames fixed. No scalar rewrite, reordering, width/owner/hosting change, other supplier or outer theorem is covered.",
+  "status": "PASS_FIXED_ORDER_AB_FRAME_EXCLUSION_PR626"
+}

research/complex-k492-frame-bound/SOURCES.json

@@ -0,0 +1,44 @@
+{
+  "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60",
+  "selected_record": {
+    "path": "certificates/selected-result.json",
+    "sha256": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53"
+  },
+  "assembly": {
+    "path": "research/community-k492-audit/pr626/replay/ASSEMBLY.json",
+    "sha256": "6127732e2fcdd470dab349c1c51d03cd9f0787ad0309b1b4a7c811a908028f4e"
+  },
+  "duals_payload_sha256": "de05d858cb1670712847f6618752a08cb320cb55149c47d87dfe044e8aae6b4d",
+  "inputs": {
+    "jp8": {
+      "CANONICAL-WORD": {
+        "payload_sha256": "fb4a8d14ed2a8048698bea6ae16f86163a1aa6c80f2eb622222eee5cdbce9b3b",
+        "gzip_sha256": "7a3fec1022d3b2b1bd986302a327735ec521d17b043f4a5acb96253a56f6193c"
+      },
+      "LOCAL-PROGRAMS": {
+        "payload_sha256": "efe45ce7fb025a6f53cc9eb54e951ac2211a5ed927e689a049e4f68ca680654b",
+        "gzip_sha256": "fa0c196f65bd6ec1424fdf7d789f6972075c7bb02bf43f573ea85eafab31be98"
+      },
+      "pr626_receipt": {
+        "path": "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/INDEPENDENT-LOCAL-REPLAY.json",
+        "canonical_word_sha256": "7a3fec1022d3b2b1bd986302a327735ec521d17b043f4a5acb96253a56f6193c",
+        "local_programs_sha256": "fa0c196f65bd6ec1424fdf7d789f6972075c7bb02bf43f573ea85eafab31be98"
+      }
+    },
+    "ck": {
+      "CANONICAL-WORD": {
+        "payload_sha256": "9bbc75dede090cfd7a0a0252424ea9d9f6211e2350d2a801d4e4f2f0784167c7",
+        "gzip_sha256": "ae3018c0646be06f47d345bb8baf0e6ea9220096a949fa30a8f7656aa4ad6f45"
+      },
+      "LOCAL-PROGRAMS": {
+        "payload_sha256": "854f17274092263dc25e60367f4cd0d29f60a8446becd17cc1883ebed7a97900",
+        "gzip_sha256": "b5da54e049cc127a1065190a647cb71cac0c6ba03d9ccdb71719f4fcbfa886f3"
+      },
+      "pr626_receipt": {
+        "path": "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/INDEPENDENT-LOCAL-REPLAY.json",
+        "canonical_word_sha256": "ae3018c0646be06f47d345bb8baf0e6ea9220096a949fa30a8f7656aa4ad6f45",
+        "local_programs_sha256": "b5da54e049cc127a1065190a647cb71cac0c6ba03d9ccdb71719f4fcbfa886f3"
+      }
+    }
+  }
+}

research/complex-k492-frame-bound/engine.py

@@ -0,0 +1,115 @@
+"""Two rational enclosures of the adjusted child cost c_k(b) = k^(1-b) - k (standard library only).
+
+For the complex recurrence the width-k child contributes M_k = (k/(mW)) (m/k)^b, so
+M_k - k M_1 = (m^b/(mW)) c_k with a positive common factor. Since every register's
+total climb is fixed, minimising sum n_k M_k is minimising sum n_k c_k (c_0 = c_1 = 0).
+
+Engine A: own atanh logarithm series and alternating exponential series.
+Engine B: the pinned repository engine (research/complex-k492-owner-repair/vendor/multicold/engines/moment.py),
+          via its exact moment() enclosures of M_k and M_1.
+"""
+import hashlib, importlib.util
+from functools import lru_cache
+from fractions import Fraction as Q
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parents[2]
+REPO_ENGINE = ROOT / 'research/complex-k492-owner-repair/vendor/multicold/engines/moment.py'
+REPO_ENGINE_SHA256 = '81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482'
+B_ACCEPTED = Q('65528268492323474503/40000000000000000000000')   # PR626 native complex endpoint
+B_NEXT = Q('102387919519255428911/62500000000000000000000')      # next 10^-24 grid point, rejected by PR626
+M_DIM, W_LIVE = 73, 7168
+DEN = Q(1, 2 ** 200)
+
+
+@lru_cache(None)
+def _ln_bounds(k):
+    """ln k = 2 atanh(z), z=(k-1)/(k+1): positive odd series; tail <= next term / (1 - z^2)."""
+    if k == 1: return Q(0), Q(0)
+    z = Q(k - 1, k + 1); s = Q(0); t = z; j = 1
+    while True:
+        s += t / j; t *= z * z; j += 2
+        tail = t / j / (1 - z * z)
+        if tail < DEN: return 2 * s, 2 * (s + tail)
+
+
+def _down(x, bits=256):
+    return Q((x.numerator << bits) // x.denominator, 1 << bits)
+
+
+def _up(x, bits=256):
+    return -_down(-x, bits)
+
+
+def _exp_neg_bounds(x):
+    """bounds of exp(-x) for 0 <= x < 1: alternating series with decreasing terms.
+    Callers pass dyadic x; exp(-x) is decreasing, so outward rounding of x is done by the caller."""
+    assert 0 <= x < 1
+    s = Q(1); t = Q(1); j = 1; lo = hi = None
+    while True:
+        t = t * x / j; s = s - t if j % 2 else s + t
+        if j % 2: lo = s
+        else: hi = s
+        if lo is not None and hi is not None and t < DEN: return lo, hi
+        j += 1
+
+
+def engine_a(b):
+    out = {}
+    for k in range(0, 10):
+        if k < 2: out[k] = (Q(0), Q(0)); continue
+        l, u = _ln_bounds(k)
+        e_lo, _ = _exp_neg_bounds(_up(b * u)); _, e_hi = _exp_neg_bounds(_down(b * l))
+        out[k] = (k * e_lo - k, k * e_hi - k)
+    return out
+
+
+def _repo():
+    spec = importlib.util.spec_from_file_location('repo_moment', REPO_ENGINE)
+    m = importlib.util.module_from_spec(spec); spec.loader.exec_module(m); return m
+
+
+def engine_b(b):
+    """c_k scaled by (mW)/m^b: uses M_k enclosures; returns enclosures of (mW) (M_k - k M_1) / m^b."""
+    R = _repo(); out = {}
+    l1, u1 = R.moment({1: 1}, M_DIM, W_LIVE, b)
+    # m^b bounds from the same engine: M_1 = (1/(mW)) m^b
+    mb_lo, mb_hi = l1 * M_DIM * W_LIVE, u1 * M_DIM * W_LIVE
+    for k in range(0, 10):
+        if k < 2: out[k] = (Q(0), Q(0)); continue
+        lk, uk = R.moment({k: 1}, M_DIM, W_LIVE, b)
+        lo = (lk - k * u1) * M_DIM * W_LIVE; hi = (uk - k * l1) * M_DIM * W_LIVE
+        # divide by m^b > 0 (both bounds are negative for k >= 2)
+        assert hi < 0
+        out[k] = (lo / mb_lo, hi / mb_hi)
+    return out
+
+
+def adjusted_bounds(b=B_NEXT):
+    A = engine_a(b)
+    return {k: A[k][0] for k in A}, {k: A[k][1] for k in A}
+
+
+def nonnegative(v, engines):
+    """sum_{k=2..9} v[k-2] c_k >= 0, proved by every engine (zero form accepted symbolically)"""
+    if not any(v): return True
+    for E in engines:
+        s = Q(0)
+        for k in range(2, 10):
+            x = v[k - 2]
+            if x: s += x * (E[k][0] if x > 0 else E[k][1])
+        if s < 0: return False
+    return True
+
+
+def moment_a(H, b, m=M_DIM, W=W_LIVE):
+    """engine-A enclosure of the native moment sum_r (r n/(mW)) (m/r)^b"""
+    lo = hi = Q(0)
+    lm_lo, lm_hi = _ln_bounds(m)
+    for r, n in H.items():
+        lr_lo, lr_hi = _ln_bounds(r)
+        x_lo, x_hi = b * (lm_lo - lr_hi), b * (lm_hi - lr_lo)    # b ln(m/r) >= 0
+        # exp(x) = 1/exp(-x)
+        e1_lo, e1_hi = _exp_neg_bounds(_up(x_hi)); e2_lo, e2_hi = _exp_neg_bounds(_down(x_lo))
+        p = Q(r * n, m * W); lo += p / e2_hi; hi += p / e1_lo
+    return lo, hi

research/complex-k492-frame-bound/explore/exact.py

@@ -0,0 +1,56 @@
+#!/usr/bin/env python3
+"""Discovery cross-check: exact fixed-order A/B frame model solved by CP-SAT (needs ortools).
+
+Not used by verify.py; CP-SAT optimality is a solver report, not a certificate.
+Every free macro picks one subspace of its complete interval [lo, hi]; consecutive
+free macros on a register must be nested. Objective: maximise -sum c_k(b) over
+register climbs (c_k = k^(1-b) - k), scaled to integers.
+
+usage: explore/exact.py DATA_WORD_DIR forward|backward SECONDS
+"""
+import sys
+from collections import Counter
+from pathlib import Path
+sys.path.insert(0, str(Path(__file__).resolve().parents[1]))
+import model as Mo
+import engine as E
+from ortools.sat.python import cp_model
+
+lo_, hi_ = E.adjusted_bounds()
+W = {k: round(-float(lo_[k]) * 10 ** 9) for k in range(10)}
+
+
+def solve(c, F, nodes, lo, hi, seconds):
+    m = cp_model.CpModel(); n = 2 * c['v'] + c['R']; seq = Mo.chains(c, nodes)
+    free = [i for i, nd in enumerate(nodes) if nd[1] is None and len(lo[i]) < len(hi[i])]
+    dom = {i: Mo.between(lo[i], hi[i]) for i in free}; x = {}; dv = {}
+    for i in free:
+        x[i] = m.NewIntVar(0, len(dom[i]) - 1, ''); dims = [len(g) for g in dom[i]]
+        dv[i] = m.NewIntVar(min(dims), max(dims), ''); m.AddElement(x[i], dims, dv[i]); m.AddHint(x[i], dom[i].index(nodes[i][2]))
+    D = lambda i: dv[i] if i in dv else len(nodes[i][2])
+    obj = []; done = set()
+    for r in range(n):
+        s = seq[r]
+        for a, b in zip(s, s[1:]):
+            if a in x and b in x and (a, b) not in done:
+                done.add((a, b))
+                m.AddAllowedAssignments([x[a], x[b]], [(p, q) for p, g in enumerate(dom[a]) for q, h in enumerate(dom[b]) if Mo.contains(h, g)])
+        chain = [len(F[c['start'][r]])] + [D(i) for i in s] + [len(F[c['final'][r]])]
+        for u, w in zip(chain, chain[1:]):
+            if isinstance(u, int) and isinstance(w, int): obj.append(W[w - u]); continue
+            zs = [(t, m.NewBoolVar('')) for t in range(10)]
+            m.AddExactlyOne(z for t, z in zs); m.Add(w - u == sum(t * z for t, z in zs)); obj.extend(W[t] * z for t, z in zs)
+    m.Maximize(sum(obj))
+    s = cp_model.CpSolver(); s.parameters.max_time_in_seconds = seconds; s.parameters.num_workers = 8; st = s.Solve(m)
+    fr = [nd[2] for nd in nodes]
+    for i in free: fr[i] = dom[i][s.Value(x[i])]
+    return s.StatusName(st), s.ObjectiveValue(), s.BestObjectiveBound(), fr
+
+
+if __name__ == '__main__':
+    c, ev = Mo.load(sys.argv[1], sys.argv[2]); F, nodes, climbs, center = Mo.extract(c, ev); lo, hi = Mo.intervals(c, F, nodes)
+    H0 = Mo.profile(c, F, nodes, [nd[2] for nd in nodes]); base = sum(W[k] * z for k, z in H0.items())
+    st, val, bd, fr = solve(c, F, nodes, lo, hi, float(sys.argv[3]))
+    H1 = Mo.profile(c, F, nodes, fr)
+    print(st, 'objective', val, 'bound', bd, 'baseline', base, 'solution profile', dict(sorted(H1.items())),
+          'changed frames', sum(fr[i] != nd[2] for i, nd in enumerate(nodes)))