From 5d0674b5615de25d89ce912df234e501b0e8c024 Mon Sep 17 00:00:00 2001 From: Cinna Davis Date: Fri, 23 Oct 2026 05:57:36 -0500 Subject: [PATCH] Calibrate paid owned contacts with shared late native maps and retain one bounded screen --- .../owned-kernel-shared-map/DISCOVERY.json | 80 ++++++++++ research/owned-kernel-shared-map/README.md | 117 ++++++++++++++ research/owned-kernel-shared-map/SOURCES.json | 36 +++++ research/owned-kernel-shared-map/TASK.json | 75 +++++++++ research/owned-kernel-shared-map/VERIFY.json | 38 +++++ research/owned-kernel-shared-map/discover.py | 43 +++++ .../owned-kernel-shared-map/shared_maps.py | 149 ++++++++++++++++++ research/owned-kernel-shared-map/verify.py | 69 ++++++++ 8 files changed, 607 insertions(+) create mode 100644 research/owned-kernel-shared-map/DISCOVERY.json create mode 100644 research/owned-kernel-shared-map/README.md create mode 100644 research/owned-kernel-shared-map/SOURCES.json create mode 100644 research/owned-kernel-shared-map/TASK.json create mode 100644 research/owned-kernel-shared-map/VERIFY.json create mode 100644 research/owned-kernel-shared-map/discover.py create mode 100644 research/owned-kernel-shared-map/shared_maps.py create mode 100644 research/owned-kernel-shared-map/verify.py diff --git a/research/owned-kernel-shared-map/DISCOVERY.json b/research/owned-kernel-shared-map/DISCOVERY.json new file mode 100644 index 0000000000..083d92ac22 --- /dev/null +++ b/research/owned-kernel-shared-map/DISCOVERY.json @@ -0,0 +1,80 @@ +{ + "actual_local_energy": 0.0, + "changed_contract": "Nonmonotone persistent contacts, all8 paid owned inputs, shared late G; frozen native prelude boundaries", + "changed_native_rank_tables": 52, + "fixed_helper_side": "none", + "floating_dual_bound": 0.0, + "free_shared_late_maps": 72, + "functionals": [ + 1 + ], + "helpers": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "message": "Optimization terminated successfully. (HiGHS Status 7: Optimal)", + "mode": "kernel", + "owned_copies": [ + { + "frame": 254, + "node": 10846, + "role": 92 + }, + { + "frame": 274, + "node": 10871, + "role": 57 + }, + { + "frame": 619, + "node": 10896, + "role": 81 + }, + { + "frame": 279, + "node": 10921, + "role": 224 + }, + { + "frame": 621, + "node": 10946, + "role": 11 + }, + { + "frame": 280, + "node": 10971, + "role": 240 + }, + { + "frame": 624, + "node": 10996, + "role": 9 + }, + { + "frame": 281, + "node": 11021, + "role": 256 + } + ], + "paid": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "pair_terms": 14480, + "preserved_prelude_lines": 12, + "scipy": "1.18.1", + "scope": "BOUNDED_FLOATING_DISCOVERY_ONLY_SHARED_G_SYNTHESIS_AND_NATIVE_ADMISSION_UNRUN", + "seconds": 0.9278902219957672, + "selected_nodes": [], + "solver_objective": 0.0, + "source_sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05", + "status": 0, + "tested_saving": 0.00302177585, + "variable_contacts": 9188 +} diff --git a/research/owned-kernel-shared-map/README.md b/research/owned-kernel-shared-map/README.md new file mode 100644 index 0000000000..6bf27fea70 --- /dev/null +++ b/research/owned-kernel-shared-map/README.md @@ -0,0 +1,117 @@ +# Owned nonmonotone contacts with shared late native maps + +This is an exact rank/invoice model with optional floating discovery. It +combines changes that the earlier owned common-kernel prototype separated: +nonmonotone persistent contact transports, eight variable owned COPY charts +with their full paid center ranks, and one consistent late native G per +operator. Both helper boundaries are variable. Every earlier native boundary +is held fixed, including the twelve nontrivial shared prelude line pairs. +All former zero persistent edges remain represented and charged. + +One bounded functional-1 solve returned the unchanged source, with zero +selected contacts and a floating full-invoice delta of zero. It used 9,188 +binary contact variables and 14,480 pair terms, finishing in 0.928 seconds +under the 120-second cap. `DISCOVERY.json` is numerical search evidence, +not an exact optimality certificate, a universal barrier or a higher kappa. +The selected conditional kappa remains .00302015. No wider scan was run. + +## Exact model and cost + +For source subspace U, each contact chooses U or its intersection with the +common kernel. Persistent transitions and whole helper residuals have actual +canonical relative Fourier rank d(A,B)=dim A+dim B-2dim(A intersect B), as in +the retained general Gaussian contact model. All eight COPY contacts may +move; their CLEAR initializes zero at that chart and their unchanged opposite +owned chart stays zero. Each changed center is priced by its FULL r^t, not +a rank-subtracted bridge price. Other owned contacts stay fixed. + +Every native operator has one released positive late occurrence. Other +occurrences are frozen at the original line/zero/full boundaries. When there +is a preserved prelude line, the same invertible G must satisfy G(a)=b. For +late input A, desired output B, k=dim A and l=dim B, the minimum physical +relative rank over such G is + +``` +abs(k-l) + 2*defect. +``` + +Without a preserved line, defect=0. With it, put sa=[a in A], sb=[b in B]. +For k<=l, defect=0 exactly when 0<=sb-sa<=(kl, use the inverse +condition 0<=sa-sb<=(ll, apply the same argument to G^-1. +The unrestricted case follows by mapping the smaller space into the larger. + +One chosen G per operator can cover its fixed zero/full occurrences and its +single nontrivial line pair as well as its late contact. The model minimizes +over that G per binary late assignment. An actual winning candidate would +still have to construct those matrices and emit signed physical instructions; +this package emits no new supplier and grants no phase/native admission. + +## Calibration and reproduction + +Registered verification uses only Python's standard library: + +```sh +python3 -B scripts/research_package.py --package research/owned-kernel-shared-map +python3 -I -B research/owned-kernel-shared-map/verify.py +python3 -I -O -B research/owned-kernel-shared-map/verify.py +``` + +It checks the native minimum formula against every invertible map and every +ordered binary-subspace pair in dimensions one through three, with and +without G(1)=1: 570 exact minima over 175 invertible maps. Independent input +and output coordinate changes normalize any nonzero prescribed a,b to that +line case. It also checks the equal-dimension/wrong-line rejection, every +source node alignment, all eight changed-center charges and the complete +source paid/helper histograms. For functional1, shared-map freedom improves +52 native tables relative to the predecessor's fixed G tables. + +Optional discovery was run with Python3.12.3, NumPy2.5.4 and SciPy1.18.1: + +```sh +python3 research/owned-kernel-shared-map/discover.py --functional 1 --seconds 120 +``` + +Install optional solver dependencies in an isolated environment if reproducing +that numerical result. The registered commands never install or run a solver. +The search uses the predecessor's signed-cut MILP at saving .00302177585; +`DISCOVERY.json` retains the complete actual paid/helper re-evaluation. +Floating status0 and dual0 are not a rigorous sign or exact power proof. + +## Sources and limits + +Live sources are pinned in `SOURCES.json`: Cao Yifan's unchanged round-three +word plus the general Gaussian contact model and optional solver. No frozen +source is edited. Credit Cinna Davis's earlier general contact model and +owned prototype at8052b4818, Cao Yifan's both-boundary/shared-map programs, +Dugongue's chart grammar, the native/controller lineage, Matarener, zxv, +Jacob Alan Sussman and all retained E8/scalar/Clifford/compiler authors. +Substantial OpenAI Codex assistance; no subagents; Apache-2.0. + +The related [PR5140 owned-wire floor](https://github.com/CrocSwap/integer-mult-bounds/pull/5140) +assumes monotone persistent L paths. This experiment explicitly drops that +hypothesis and is not excluded by the floor. Conversely this single numerical +kernel test does not prove a no-gain theorem for independent contact subspaces +or any larger domain. Native absolute phases, both full literal endpoints, +owned restoration, precision, compiler and outer funding are unrun for any +positive candidate. Unknown costs are not zero. + +## Open next questions + +- Does a rigorous weak-duality certificate exist for this exact one-kernel + model and price? First inspect the continuous relaxation and recover a + rational interval-valid certificate if tight. Solver optimality alone is + insufficient; that proof would still have only this model's scope. +- Can a different scalar/common-contact contract or independent nonmonotone + subspaces yield a favorable complete invoice? Compare another mechanism + before expanding this search; record one changed hypothesis and exact cost + gate. Do not automatically rerun all 511 kernels. Actual shared G synthesis, + signed native replay and full supplier/outer admission remain required. diff --git a/research/owned-kernel-shared-map/SOURCES.json b/research/owned-kernel-shared-map/SOURCES.json new file mode 100644 index 0000000000..415695daac --- /dev/null +++ b/research/owned-kernel-shared-map/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/general-gaussian-contact-search/discover.py", + "usage": "input", + "git_blob": "7c0fdc00f3f8df27b088b7ecda81d0644e6e786f", + "sha256": "6bfc81fecbf40b208688455796618cc3ab19d7e79453ccc2909b3856bf31d7db" + }, + { + "path": "research/general-gaussian-contact-search/model.py", + "usage": "input", + "git_blob": "a69138e4014424235345f3301fbe6b097caa1b8c", + "sha256": "7cc29edccb3679b2a5c9defeeb0a2ec6bcef9b01b97c2390bebc48f366395f1f" + }, + { + "path": "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "usage": "input", + "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e", + "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" + } + ] +} diff --git a/research/owned-kernel-shared-map/TASK.json b/research/owned-kernel-shared-map/TASK.json new file mode 100644 index 0000000000..cce005e481 --- /dev/null +++ b/research/owned-kernel-shared-map/TASK.json @@ -0,0 +1,75 @@ +{ + "schema_version": 1, + "task_id": "centre-path-sharing", + "priority_revision": 7, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "original_card": { + "id": "centre-path-sharing", + "question": "Can the 64-per-call centre path (eight rank-8 COPY/ERASE totals through the private temporary) be shared across calls or shrunk?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt", + "certificates/selected-result.json" + ], + "methods": [ + "Derive a fully charged favorable relaxation for sharing one centre path across k calls, including restoration, hosting and precision.", + "Prove a lower bound on copied information per call for the selected decoder contract." + ], + "acceptance_gate": "Show the changed centre charge and copy profile per call with every added restoration or hosting cost charged, and its ceiling via ceiling.ceiling(centre=...). A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write the per-call centre charge and copy children for sharing across k = 2 calls, charge the sharing overhead, and screen it; stop this route if even the ideal sharing gains under 10%. Ideal budgets: free 2.80x, shared by two 1.90x (levers.py).", + "bottleneck_link": "The centre path consumes 64 of about 99.6 unpaid coordinates per call, i.e. about 64% of the raw deficit.", + "allowed_variations": [ + "One sharing pattern across a fixed number of calls.", + "One reduced copied-total contract for the existing decoder.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Removing copies without a replacement contract for the decoder's copied totals.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "centre path", + "copied totals", + "private temporary", + "shared centre", + "batching" + ] + }, + "scope_status": "refined", + "actual_scope": "One common-kernel nonmonotone contact model with all eight paid owned COPY inputs and shared late native maps preserving frozen prelude boundaries; exact calibration plus one bounded functional-1 floating test.", + "scope_change_reason": "The monotone owned-wire floor closes monotone center savings. The older511-functional owned prototype held G fixed; this changes G jointly and reconstructs all charges before one bounded solve.", + "bottleneck_link": "Tests whether removing native rank mismatch penalties can pay for nonmonotone source conversions while lowering actual center ranks; all extra jobs remain in the full paid-minus-helper moment.", + "budget_minutes": 30, + "stop_rule": "One functional-1 solve, at most120seconds. Stop on no gain; no automatic wider kernel scan or physical implementation follows.", + "outcome": "partial", + "evidence": "verify.py exact570native minima and full source invoices; DISCOVERY.json zero selected contacts and floating delta0; no exact optimality or new kappa.", + "author": "Cinna Davis / 1337isnot1337, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in model, code, proof, experiments and writing. No subagents, independent human or proof-kernel acceptance.", + "open_questions": [ + { + "question": "Can the one-kernel model admit an exact weak-duality certificate?", + "why_it_matters": "Floating status0 and dual0 do not establish exact optimality.", + "first_step": "Inspect the continuous relaxation, recover a dual and validate every inequality with rigorous rank-power intervals if it is tight.", + "blocked_by": "A rational checkable dual and strict/zero coefficient handling; this would remain a scoped negative result." + }, + { + "question": "Can a changed scalar/common-contact contract or independent nonmonotone subspaces yield a favorable complete invoice?", + "why_it_matters": "The one-functional common-kernel domain does not cover those changes.", + "first_step": "Compare a different mechanism and state one changed hypothesis with a complete favorable cost gate before expanding search.", + "blocked_by": "Actual shared G synthesis, both literal signed native/owned endpoints and fully funded compiler/precision/outer admission." + } + ], + "canonical_thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4611#discussioncomment-19143793", + "upstream_checked_utc": "2026-10-23T10:57:14.055312+00:00" +} diff --git a/research/owned-kernel-shared-map/VERIFY.json b/research/owned-kernel-shared-map/VERIFY.json new file mode 100644 index 0000000000..07182ce94d --- /dev/null +++ b/research/owned-kernel-shared-map/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/general-gaussian-contact-search/discover.py", + "research/general-gaussian-contact-search/model.py", + "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "570 exact native minima over all small invertible maps, complete baseline and eight actual changed-center charges; no solver." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Same exact rank/invoice calibration with assertions disabled." + } + ] +} diff --git a/research/owned-kernel-shared-map/discover.py b/research/owned-kernel-shared-map/discover.py new file mode 100644 index 0000000000..6b858451e9 --- /dev/null +++ b/research/owned-kernel-shared-map/discover.py @@ -0,0 +1,43 @@ +#!/usr/bin/env python3 +"""One bounded floating solve. Never a theorem or admitted supplier. + +Apache-2.0; substantial OpenAI Codex assistance and retained source credit. +""" +import argparse +import importlib.util +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import shared_maps as S + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--functional', type=int, default=1) + ap.add_argument('--seconds', type=float, default=120.) + args = ap.parse_args() + S.need(1 <= args.functional <= 511 and 0 < args.seconds <= 120, 'Bounded single discovery solve') + spec = importlib.util.spec_from_file_location('owned_shared_prior_discover', S.PRIOR / 'discover.py') + prior = importlib.util.module_from_spec(spec) + spec.loader.exec_module(prior) + prior.M = S.M + S.M.build = S.build + model = S.build(S.payload(), [args.functional]) + summary = {'free_shared_late_maps': len(model['shared_late_maps']), + 'preserved_prelude_lines': len(model['prelude_lines']), + 'changed_native_rank_tables': model['changed_native_tables'], + 'owned_copies': model['owned_copies']} + print(json.dumps(summary, sort_keys=True), flush=True) + result = prior.solve(S.SOURCE, [args.functional], args.seconds, 'none', 'kernel') + result.update(summary) + result['changed_contract'] = 'Nonmonotone persistent contacts, all8 paid owned inputs, shared late G; frozen native prelude boundaries' + result['scope'] = 'BOUNDED_FLOATING_DISCOVERY_ONLY_SHARED_G_SYNTHESIS_AND_NATIVE_ADMISSION_UNRUN' + (HERE / 'DISCOVERY.json').write_text(json.dumps(result, indent=2, sort_keys=True) + '\n') + print(json.dumps({k: v for k, v in result.items() if k != 'selected_nodes'}, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/owned-kernel-shared-map/shared_maps.py b/research/owned-kernel-shared-map/shared_maps.py new file mode 100644 index 0000000000..0d259bab5b --- /dev/null +++ b/research/owned-kernel-shared-map/shared_maps.py @@ -0,0 +1,149 @@ +"""Optional discovery model: nonmonotone owned contacts and shared late G. + +Cinna Davis / 1337isnot1337, substantial OpenAI Codex assistance; Apache-2.0. +Reuses the credited general Gaussian model without changing its source bytes. +Owned release follows the earlier prototype at8052b4818, reimplemented here. +""" +from collections import Counter, defaultdict +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path +import sys + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PRIOR = ROOT / 'research/general-gaussian-contact-search' +SOURCE = ROOT / 'research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz' + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate(): + for row in json.loads((HERE / 'SOURCES.json').read_text())['files']: + if row['usage'] == 'input': + need(hashlib.sha256((ROOT / row['path']).read_bytes()).hexdigest() == row['sha256'], + 'Pinned live source: ' + row['path']) + + +authenticate() +spec = importlib.util.spec_from_file_location('owned_shared_prior_model', PRIOR / 'model.py') +M = importlib.util.module_from_spec(spec) +spec.loader.exec_module(M) +original_build = M.build + + +def minimum_rank(A, B, line=None): + """min_G d(GA,B), optionally with G(a)=b; A/B are bitset subspaces.""" + k, l = M.dimension(A), M.dimension(B) + if line is None: + return abs(k - l) + a, b = line + sa, sb = (A >> a) & 1, (B >> b) & 1 + if k <= l: + maximal_intersection = 0 <= sb - sa <= int(k < l) + else: + maximal_intersection = 0 <= sa - sb <= int(l < k) + return abs(k - l) + (0 if maximal_intersection else 2) + + +def trace(payload, model): + """Align chronological scalar and native nodes against the actual graph.""" + c = payload['canonical'] + cursor = 2 + len(c['start']) + copies, centers, warps = [], [], [] + for i, e in enumerate(payload['programs']['forward']): + if e[0] == 'scalar': + need(model['nodes'][cursor] == e[2], 'Exact scalar node alignment') + if e[1][0] == 'copy': + need(e[1][1] == ['C', 0] and e[1][2][0] == 'L', 'Actual owned source') + copies.append({'node': cursor, 'frame': e[2], 'role': e[1][2][1]}) + cursor += 1 + elif e[0] == 'warp': + need(model['nodes'][cursor:cursor + 2] == e[3:5], 'Exact native node alignment') + warps.append({'event': i, 'operator': e[2], 'input': cursor, + 'output': cursor + 1, 'frames': e[3:5]}) + cursor += 2 + elif e[0] == 'center': + centers.append(e) + need(cursor + len(c['final']) == len(model['nodes']), 'Complete occurrence graph') + need(len(copies) == len(centers) == 8, 'Eight separate owned lifetimes') + for row, e in zip(copies, centers): + need(e == ['center', 0, row['frame'], 0, 8], 'Actual descending rank-eight center') + return copies, warps + + +def build(payload, forms): + model = original_build(payload, forms) + p0, h0 = M.invoice(model, []) + copies, warps = trace(payload, model) + frames = payload['canonical']['frames'] + frozen = set(model['fixed']) + grouped = defaultdict(list) + for w in warps: + grouped[abs(w['operator'])].append(w) + selected, lines = {}, {} + for operator, occurrences in grouped.items(): + candidates = [w for w in occurrences if any(len(frames[f]) not in (0, 9) for f in w['frames'])] + chosen = max(candidates, key=lambda w: len(frames[w['frames'][0]])) + need(chosen['operator'] > 0, 'Positive selected late native occurrence') + selected[chosen['input'], chosen['output']] = operator + others = [w for w in candidates if w is not chosen] + if others: + pairs = {(w['frames'][0], w['frames'][1]) if w['operator'] > 0 + else (w['frames'][1], w['frames'][0]) for w in others} + need(len(pairs) == 1, 'One preserved shared prelude line pair') + a, b = next(iter(pairs)) + need(len(frames[a]) == len(frames[b]) == 1, 'Actual fixed prelude line') + lines[operator] = frames[a][0], frames[b][0] + for w in occurrences: + if w is not chosen: + frozen.update((w['input'], w['output'])) + need(len(selected) == 72 and len(lines) == 12, 'All72 shared late maps and12 prelude constraints') + changed = 0 + new_edges = [] + for kind, a, b, ranks in model['edges']: + if kind == 'warp' and (a, b) in selected: + operator = selected[a, b] + fa, fb = model['nodes'][a], model['nodes'][b] + A = [model['old_spaces'][fa], model['new_spaces'][fa]] + B = [model['old_spaces'][fb], model['new_spaces'][fb]] + fresh = [minimum_rank(A[i], B[j], lines.get(operator)) + for i, j in ((0, 0), (1, 0), (0, 1), (1, 1))] + need(fresh[0] == 0 and all(x <= y for x, y in zip(fresh, ranks)), + 'Incumbent feasible in shared-map relaxation') + changed += fresh != ranks + ranks = fresh + new_edges.append((kind, a, b, ranks)) + model['edges'] = new_edges + model['centers'] = {} + for row in copies: + n, f = row['node'], row['frame'] + need(n in frozen, 'Owned COPY starts frozen') + frozen.remove(n) + sink = len(model['nodes']) + model['nodes'].append(0) + frozen.add(sink) + old = M.dimension(model['old_spaces'][f]) + new = M.dimension(model['new_spaces'][f]) + # The solver prices every paid table by full r^t. In particular a + # variable center must not use a rank-subtracted bridge price. + model['edges'].append(('center', n, sink, [old, new, old, new])) + model['fixed'] = sorted(frozen) + model['shared_late_maps'] = selected + model['prelude_lines'] = lines + model['owned_copies'] = copies + model['changed_native_tables'] = changed + p, h = M.invoice(model, []) + need(p == p0 == Counter({1: 2201, 2: 412, 3: 510, 4: 127, 5: 40, 8: 8}), 'Whole baseline paid profile') + need(h == h0 == Counter({4: 28, 7: 7, 8: 47, 9: 326}), 'All408 independent productive helpers') + return model + + +def payload(): + return json.loads(gzip.decompress(SOURCE.read_bytes())) diff --git a/research/owned-kernel-shared-map/verify.py b/research/owned-kernel-shared-map/verify.py new file mode 100644 index 0000000000..9a5952d026 --- /dev/null +++ b/research/owned-kernel-shared-map/verify.py @@ -0,0 +1,69 @@ +#!/usr/bin/env python3 +"""Exact rank-table and invoice calibration; no search or supplier admission. + +Apache-2.0; substantial OpenAI Codex assistance and retained source credit. +""" +from itertools import product +import json +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import shared_maps as S + + +def rank(vectors): + pivots = {} + for v in vectors: + while v: + p = v.bit_length() - 1 + if p in pivots: + v ^= pivots[p] + else: + pivots[p] = v + break + return len(pivots) + + +def geometry(): + comparisons = maps = 0 + for n in (1, 2, 3): + spaces = {frozenset({0})} + for v in range(1, 1 << n): + for old in list(spaces): + if v not in old: + spaces.add(frozenset(set(old) | {x ^ v for x in old})) + groups = [cols for cols in product(range(1, 1 << n), repeat=n) if rank(cols) == n] + maps += len(groups) + for A in spaces: + images = [(cols[0] == 1, S.M.mask(S.M.mv(cols, x) for x in A)) for cols in groups] + for B in spaces: + amask, bmask = S.M.mask(A), S.M.mask(B) + free = min(S.M.fourier_rank(image, bmask) for _, image in images) + line = min(S.M.fourier_rank(image, bmask) for fixed, image in images if fixed) + S.need(S.minimum_rank(amask, bmask) == free, 'Exact unconstrained native minimum') + S.need(S.minimum_rank(amask, bmask, (1, 1)) == line, 'Exact shared-line native minimum') + comparisons += 2 + S.need(S.minimum_rank(S.M.mask({0, 1}), S.M.mask({0, 2}), (1, 1)) == 2, + 'Equal dimensions cannot evade a preserved line') + return {'minimum_comparisons': comparisons, 'invertible_maps': maps} + + +def main(): + model = S.build(S.payload(), [1]) + paid, helpers = S.M.invoice(model, []) + S.need(len(model['owned_copies']) == 8, 'Eight owned inputs released') + for row in model['owned_copies']: + S.need(row['node'] not in model['fixed'], 'Owned source is actually variable') + changed, _ = S.M.invoice(model, [row['node']]) + S.need(changed[8] == 7 and changed[7] == 1, 'Actual changed center rank charged') + print(json.dumps({'status': 'PASS_SHARED_MAP_RANK_AND_BASELINE_CALIBRATION_ONLY', + 'geometry': geometry(), 'paid': dict(paid), 'helpers': dict(helpers), + 'changed_native_tables': model['changed_native_tables'], + 'free_shared_late_maps': len(model['shared_late_maps']), + 'preserved_prelude_lines': len(model['prelude_lines']), + 'new_kappa': False}, sort_keys=True)) + + +if __name__ == '__main__': + main()