diff --git a/research/receiver-all-length-floor/PEERS.json b/research/receiver-all-length-floor/PEERS.json new file mode 100644 index 0000000000..3c1b9e75f6 --- /dev/null +++ b/research/receiver-all-length-floor/PEERS.json @@ -0,0 +1,26 @@ +{ + "scope": "Pinned receipt comparison only; peer code is not executed or certified.", + "attribution": "Concurrent mihir-s-05/OpenAI Codex investigations #4577 and #4572; Apache-2.0.", + "receipts": [ + { + "pr": 4581, + "head": "b154350fbf1e7d49118851ab899a733727483289", + "source_path": "research/receiver-window-all-length-floor/RESULT.json", + "url": "https://github.com/mihir-s-05/integer-mult-bounds/blob/b154350fbf1e7d49118851ab899a733727483289/research/receiver-window-all-length-floor/RESULT.json", + "git_blob": "3fec4b9b5177745b11d84214c438ff926e264694", + "payload_sha256": "da70c9292df9922377a0bf0fd1a208562a0c5861de7eca8ddac4a7fde29d568b", + "archive_sha256": "b810f7ee8bba3bdfb999f4d35b521e29172f54c65cd1527132c09dbc9bbe59e8", + "local": "peers/pr4581-RESULT.json.gz" + }, + { + "pr": 4582, + "head": "23c515a3c071a6bfdd1fe80bc67cea55f6d43643", + "source_path": "research/receiver-window-all-length-floor/RESULT.json", + "url": "https://github.com/mihir-s-05/integer-mult-bounds/blob/23c515a3c071a6bfdd1fe80bc67cea55f6d43643/research/receiver-window-all-length-floor/RESULT.json", + "git_blob": "3e13f2b641f605fc8c42359389042c2d131e3d5c", + "payload_sha256": "2d1e520641a6bfbcd2ba84654a1a34f34a4c32592dc731acd943cce658c705fc", + "archive_sha256": "b5618ca25c893614e47e4dce33465e31c1a677fe50ac0791eec749ab3a61b845", + "local": "peers/pr4582-RESULT.json.gz" + } + ] +} diff --git a/research/receiver-all-length-floor/README.md b/research/receiver-all-length-floor/README.md new file mode 100644 index 0000000000..0686c9747d --- /dev/null +++ b/research/receiver-all-length-floor/README.md @@ -0,0 +1,229 @@ +# Independent receiver-window floor and peer-certificate comparison + +This package independently corroborates the concurrent all-length results in +[#4581](https://github.com/CrocSwap/integer-mult-bounds/pull/4581) and +[#4582](https://github.com/CrocSwap/integer-mult-bounds/pull/4582), and supplies +an executable comparison of their pinned receipts. All three implementations +agree on every window boundary, incumbent bill and terminal rank partition. +The contribution adds a separate three-ancestry model and exhaustive small +geometric inclusion controls, with no exclusive novelty or priority claim. + +**Every eligible window has zero paid-cost headroom for any finite shear word +on the same three fields, with the same monotone frame boundaries.** There is +no word-length or coefficient cap. The incumbent minimizes every increasing +concave rank cost `f`, with `f(0)=0`; in particular `f(r)=r^(1-C)` for +`0 <= C < 1`. No new kappa or selected-frontier change is claimed. + +This closes the length/coefficient direction left by [#4546](https://github.com/CrocSwap/integer-mult-bounds/pull/4546) +and [#4567](https://github.com/CrocSwap/integer-mult-bounds/pull/4567), within their +fixed three-field monotone contract. Those packages enumerate bounded scalar +words. This package discards scalar coefficients and the exact endpoint after +retaining necessary temporal ancestry, then exhausts a finite acyclic frame +relaxation. It is a scoped exclusion, not a general barrier to better suppliers. + +## Contract and theorem + +The three persistent fields are `(a,b,x)`, with arbitrary initial values. Their +entrance and exit frames `S_i <= E_i` are binary subspaces of `F_2^9`. Each +constant-coefficient shear `y_i += c*y_j` requires a common frame for its two +operands. Each field's frame only grows by inclusion. Every positive movement +of dimension `r` is charged `f(r)`, including the final movement to `E_i`. +The required endpoint is `a += ca*x; b += cb*x`, with `ca,cb` in `{+1,-1}` and +`x` restored. Replacement coefficients can be arbitrary constants; the proof +does not bound their magnitudes or charge their scalar cost. + +For each of the 128 eligible adjacent pairs freshly extracted from main's +PR4470 constructor (123 phase-B and 5 cleanup-tail), every such replacement +has cost at least the incumbent's. The incumbent itself satisfies the boundary +contract, so the minimum is attained. The proof has four parts. + +### 1. Temporal ancestry is necessary + +Initially give field `i` the marker set `{i}`. At a contact of `i,j`, replace +both marker sets by their union. This is deliberately generous: a shear moves +information in only one direction and cancellations may remove information. +Induction on gates shows that every actual nonzero input dependency remains in +the marker set. Since both receiver outputs depend nontrivially on the original +`x`, their final marker sets must contain marker 2 (bit 4 in the checker). +Restoring `x` and cancelling unwanted dependencies are additional constraints +that the relaxation omits. + +Each current frame also contains the sum of the entrance subspaces associated +with its markers. Initially this is equality. A common contact frame contains +both previous frames, so their union of markers preserves this property. +This geometric induction is valid even when a scalar coefficient cancels. + +### 2. A finite graph contains every legal path + +A state consists of three marker bitmasks `M_i` and three current contact +dimensions `d_i`. For contact `i,j`, put `M=M_i union M_j`. Its frame must contain +`L=sum(S_k : k in M)` and be contained in `U=E_i intersection E_j`. Reject the +transition if `L` is not contained in `U`. Otherwise permit every integer + +`max(d_i,d_j,dim L) <= d <= dim U`. + +Set both operand dimensions to `d`, both marker sets to `M`, and charge each +positive gap `d-d_i`, `d-d_j`. We forget incidence constraints on the unknown +current frames, so this can admit extra paths, never exclude an actual one. +Once both receivers contain the source marker, termination charges every +positive gap `dim(E_i)-d_i`. + +A state-changing transition strictly increases +`sum(d_i) + sum(|M_i|)`, bounded by 36. A transition leaving the state unchanged +has zero frame cost and can be deleted: the relaxed endpoint depends only on +the markers. Thus all finite words, however long, map into this finite DAG. +The checker retains every attainable rank partition, not just a heuristic +minimum. The sum of its ranks must equal `sum(dim E_i - dim S_i)`. + +Extra monotone movements between contacts are compressed into one jump. This +cannot raise cost: for an increasing concave `f` with `f(0)=0`, +`f(u+v) <= f(u)+f(v)`. To see this for integer ranks, the first `v` discrete +slopes dominate the `v` slopes starting at `u`. This also covers split terminal +movements. Consequently the relaxed cost is a lower bound on actual cost. + +### 3. Integer capped-rank sums certify all concave tariffs + +For each relaxed partition `p` and incumbent partition `o`, the checker proves +equal rank mass and, for every `k=1,...,9`, + +`sum(min(r,k) for r in o) <= sum(min(r,k) for r in p)`. + +Let `s_k=f(k)-f(k-1)`. Concavity and monotonicity give +`s_1 >= ... >= s_9 >= 0`. The exact identity + +`f(r) = s_9*r + sum((s_k-s_(k+1))*min(r,k), k=1,...,8)` + +proves the cost order by nonnegative linear combination. Thus the certificate +uses integers only, with no root rounding or sampled exponents. It includes +the predecessors' `C=0.00302015` and every `0 <= C < 1`. + +### 4. Source-bound application and attainment + +[SOURCES.json](SOURCES.json) authenticates all seven constructor inputs before +execution. The constructor supplies candidate frames and the forward program; +its acceptance engine is not invoked. The new extractor uses chronological +entrances and per-role next-use lists for exits (including warp pre-frames). +It independently checks the incumbent's actual subspace containment and ranks. + +[RESULT.json](RESULT.json) records all 128 window indices, roles, signs, +canonical entrance/contact/exit bases, incumbent partitions and relaxed +partitions. In total there are **1,603 states and 239 window/partition pairs**; +the largest individual graph has 45 states. Every incumbent is admitted and +every integer comparison passes. Partition-count frequencies are +`{1:93, 2:9, 3:6, 4:2, 5:13, 7:4, 9:1}`. Different windows may overlap; +their gains or costs must not be summed as disjoint modifications. + +## Verification + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/receiver-all-length-floor +``` + +The registered replay freshly extracts the windows and compares every receipt +field without rewriting it. Both registered Python commands use isolated mode; +the constructor child also gets a fresh bytecode cache namespace. The second +command runs semantic controls under `-O` with explicit checks/unittest: + +- A separate forward traversal over actual `F_2^2` subspaces covers all 1,728 + triples of comparable entrance/exit pairs (664 have a terminal path). + Every actual geometric partition is admitted by the dimension relaxation. +- The shape of window 10557 rejects the tempting cheaper partition `(1,2)` + when the old bill is `(1,1,1)`. Forgetting temporal source ancestry admits + it. Connectedness alone can contact `a,b` before `x` arrives, leaving `a` + without the required source contribution. +- Omitting an exit payment fails rank mass; incompatible equal-dimensional + frames and shrinking boundaries fail; zero-dimensional source propagation + and a next-use/warp extraction fixture pass. +- All 220 decreasing nine-step slope sequences over `{0,1/3,2/3,1}` satisfy + the exact cost expansion. A corrupted constructor input is rejected before + execution. + +The finite controls support the implementation; the all-length statement +rests on the inductions and finite-state reduction above. No formal-kernel or +independent human verification is claimed. `--write` is an authoring option, +not part of the registered replay. + +Local validation on Windows with CPython 3.12.0 passed the metadata/source-pin +check, full registered replay and all six optimized controls. A one-time +development cross-check matched all 128 indices, roles, signs, complete +subspaces and incumbent bills against #4567's separately loaded extractor at +the pinned head. That comparison is corroboration, not a replay dependency. + +## Executable comparison with concurrent certificates + +The submission refresh found [#4572](https://github.com/CrocSwap/integer-mult-bounds/discussions/4572), +[#4577](https://github.com/CrocSwap/integer-mult-bounds/discussions/4577) and the +static-contact proof in [#4574](https://github.com/CrocSwap/integer-mult-bounds/discussions/4574). +They are concurrent investigations of the same conclusion. This package was +already implemented when discovered and is offered as independent corroboration. +It does not claim to have independently audited their proof code. + +[PEERS.json](PEERS.json) pins the exact source Git blobs and SHA256 payloads for +two committed receipts, retained as unchanged gzip-compressed inputs under +`peers/`. [compare_peers.py](compare_peers.py) authenticates those bytes, expands +bases to complete binary subspaces (basis order may differ), and compares all +128 identities, phases, roles, signs, entrances, contacts, exits, incumbent +bills and 239 terminal partitions with this package's freshly verified receipt. +It executes no peer code. This is the third registered command, also runnable +directly with `python -I -O -B research/receiver-all-length-floor/compare_peers.py`. + +| Certificate | Exact head | Reported states | Matched window/partition pairs | +|---|---|---:|---:| +| #4581, directed source dependence | `b154350fbf1e7d49118851ab899a733727483289` | 1,303 | 239 | +| #4582, bidirectional source dependence | `23c515a3c071a6bfdd1fe80bc67cea55f6d43643` | 1,496 | 239 | +| This package, all three entrance-ancestry masks | See this PR head | 1,603 | 239 | + +State counts are representation-dependent, not an improvement measure. The +executable comparison certifies the common projected data, not equivalence of +all intermediate states or peer tests. The peer receipts are package-local +immutable inputs; the generic runner includes them in package invalidation and +export, while their external-origin Git blob checks are explicit in the +comparison code. They do not add pending source-history dependencies. + +## Scope, overlap, and credit + +Canonical base: `f626db5c3a3d781d8f7695038776c621651f75e1`, priority revision 7. +Coordination: [Discussion #4573](https://github.com/CrocSwap/integer-mult-bounds/discussions/4573). +The handoff-first selection and exact predecessor heads are in [TASK.json](TASK.json). +The initial overlap refresh covered 355 open PR bodies and 3,470 Discussion +records; all 5,860 tracked top-level package README/TASK notes were then +materialized and searched. The 08:08-08:09 UTC submission refresh covered 358 +open PRs and 3,493 Discussion records and revealed the concurrent work above. +Canonical main and the priority revision were unchanged. Coverage is a dated +search, not proof of novelty. #4567's head `58695721e3cf9d5101440dd53a3ea5bbcc0e9313` +adds nonadjacent and contact-retiming checks outside this fixed adjacent scope. +The older R420 all-length cleanup floor and P111 receiver census concern +different targets and tariffs; neither covers these PR4470 frame contracts. + +The historical baseline helper was attempted but stopped at absent source +packages in the sparse checkout. It is not reported as a pass. The selected +record, review, source manifest, claim and reproduction entry point were read; +the selected full cold replay is outside this local result. The selected record +remains `23/10000`. Native all-column correctness, physical lowering, stock, +precision, fixed tape, compiler and outer transfer are not reverified here. +There is no conclusion about extra fields, nonmonotone frames, changed +boundaries, nonadjacent windows, or simultaneous overlapping rewrites. + +Credit Chris R / Clear1nsight's #4546 fixed-window relaxation; Ryanson +Jonathan's #4567 broader finite census and explanation motivating this +all-length question; Cinna Davis's #4470 construction and retiming lineage; +zxv's receiver-sharing/productive-helper work; Jacob Alan Sussman and the +retained native, Clifford, geometry and outer contributors. Predecessor code +was read during development; a local probe reused #4567's extraction for +comparison. The committed extractor, state graph and cost checker are new, +and import no #4546/#4567 acceptance code. This is a separate implementation, +not a separately launched audit team. Prepared for mihir-s-05 with substantial +OpenAI Codex assistance. Apache-2.0; retained source notices are unchanged. +Credit the concurrent #4572/#4582, #4577/#4581 and #4574 investigations as well; +the compressed peer receipts retain their exact authored payloads and origin. + +## Open next questions + +Further word-length or coefficient sweeps in these fixed contracts have no +headroom under the stated tariff. A useful follow-up must explicitly change +the contract: for example, one additional field with fully charged entry, +exit, restoration and consumer work. Derive that optimistic complete budget +before implementing a search. This certificate does not decide that changed +model. [TASK.json](TASK.json) records the first step and blockers. diff --git a/research/receiver-all-length-floor/RESULT.json b/research/receiver-all-length-floor/RESULT.json new file mode 100644 index 0000000000..be079e0bcf --- /dev/null +++ b/research/receiver-all-length-floor/RESULT.json @@ -0,0 +1,141 @@ +{ + "status": "PASS_RECEIVER_ALL_LENGTH_CONCAVE_FLOOR", + "window_count": 128, + "state_count": 1603, + "partition_count": 239, + "boundary_sha256": "8cdc8a25f3d880fc398fe21aaf3c2c4668d9d453102ba7b6e5cae00cbdb578ae", + "word_length_cap": null, + "coefficient_cap": null, + "cost_scope": "Every increasing concave rank weight f with f(0)=0; in particular r^q for 0 0 and size & (size - 1) == 0, "power-of-two frame size") + return size.bit_length() - 1 + + +def constructor_data(): + # -B alone does not prevent cached imports. This child has a fresh cache + # namespace as well as isolated Python and authenticated source inputs. + code = ( + "import json,sys;sys.path.insert(0,sys.argv[1]);" + "import native_joint;candidate,programs,*_=native_joint.construct();" + "print(json.dumps([candidate,programs['forward']]))" + ) + with tempfile.TemporaryDirectory(prefix="receiver-floor-pyc-") as cache: + completed = subprocess.run( + [sys.executable, "-I", "-B", "-X", "pycache_prefix=" + cache, "-c", code, + str(ROOT / "research/joint-helper-lattice")], + check=True, capture_output=True, text=True, encoding="utf-8", timeout=120, + ) + return json.loads(completed.stdout) + + +def contacts(event): + """Persistent uses: (role, frame required before operation, frame after).""" + if event[0] == "scalar": + gate = event[1] + require(gate[0] in ("add", "copy", "scale", "clear"), "known scalar kind") + require(gate[0] != "clear" or gate[1][0] != "L", "no persistent clear") + roles = gate[1:3] if gate[0] in ("add", "copy") else gate[1:2] + return [(r[1], event[2], event[2]) for r in roles if r[0] == "L"] + if event[0] == "warp": + require(event[1][0] == "L", "persistent warp") + return [(event[1][1], event[3], event[4])] + return [] + + +def extract_windows(candidate, program): + """Next-use lists bind exits; chronology supplies entrances. + + Indices follow the inherited convention: the program with climbs removed. + Climb costs are reconstructed from the actual contact frames. + """ + events = [e for e in program if e[0] != "climb"] + uses = [[] for _ in candidate["start"]] + use_positions = [[] for _ in candidate["start"]] + for position, event in enumerate(events): + for role, before, _ in contacts(event): + uses[role].append(before) + use_positions[role].append(position) + frame_spaces = [span(basis) for basis in candidate["frames"]] + current = list(candidate["start"]) + phase = None + windows = [] + for position, event in enumerate(events): + if event[0] == "phase": + phase = event[1] + pair = events[position:position + 2] + if phase in ("B", "cleanup_tail") and len(pair) == 2 and all( + e[0] == "scalar" and e[1][0] == "add" for e in pair): + first, second = (e[1] for e in pair) + if all(r[0] == "L" for g in (first, second) for r in g[1:3]): + a, x, b, y = first[1][1], first[2][1], second[1][1], second[2][1] + coefficients = [] + for gate in (first, second): + numerator, denominator = gate[3:5] + require(denominator != 0, "nonzero coefficient denominator") + if abs(numerator) != abs(denominator): + break + coefficients.append(1 if numerator * denominator > 0 else -1) + if x == y and len({a, b, x}) == 3 and len(coefficients) == 2: + owners = (a, b, x) + exits = [] + for role in owners: + next_use = bisect_right(use_positions[role], position + 1) + exits.append(uses[role][next_use] if next_use < len(uses[role]) + else candidate["final"][role]) + windows.append({ + "index": position, "phase": phase, "roles": list(owners), + "coefficients": coefficients, + "starts": tuple(frame_spaces[current[r]] for r in owners), + "ends": tuple(frame_spaces[f] for f in exits), + "frames": tuple(frame_spaces[e[2]] for e in pair), + }) + for role, _, after in contacts(event): + current[role] = after + return windows + + +def incumbent_profile(window): + current = list(window["starts"]) + ranks = [] + for (i, j), frame in zip(((0, 2), (1, 2)), window["frames"]): + for role in (i, j): + require(current[role] <= frame, "incumbent contact containment") + gap = dimension(frame) - dimension(current[role]) + if gap: + ranks.append(gap) + current[role] = frame + for frame, end in zip(current, window["ends"]): + require(frame <= end, "incumbent exit containment") + gap = dimension(end) - dimension(frame) + if gap: + ranks.append(gap) + return tuple(sorted(ranks)) + + +def relaxed_profiles(starts, ends, required=(4, 4, 0)): + """All finite contact words, quotiented by a strictly increasing state. + + masks[i] records initial roles that can have met role i along a temporal + undirected contact path. This overapproximates scalar information flow. + dims[i] is the current contact dimension. No coefficients or word cap. + """ + if not all(s <= e for s, e in zip(starts, ends)): + return frozenset(), 0 + end_dims = tuple(map(dimension, ends)) + joins = {mask: span(v for i in range(3) if mask & (1 << i) for v in starts[i]) + for mask in range(1, 8)} + + @lru_cache(None) + def visit(masks, dims): + profiles = set() + if all(mask & needed == needed for mask, needed in zip(masks, required)): + profiles.add(tuple(sorted(e - d for d, e in zip(dims, end_dims) if e > d))) + for i, j in PAIRS: + merged = masks[i] | masks[j] + lower = joins[merged] + upper = ends[i] & ends[j] + if not lower <= upper: + continue + for contact_dim in range(max(dims[i], dims[j], dimension(lower)), dimension(upper) + 1): + next_masks, next_dims = list(masks), list(dims) + next_masks[i] = next_masks[j] = merged + next_dims[i] = next_dims[j] = contact_dim + next_state = (tuple(next_masks), tuple(next_dims)) + if next_state == (masks, dims): + continue # zero-cost self-loop; no remaining endpoint constraint + rank_before = sum(dims) + sum(mask.bit_count() for mask in masks) + rank_after = sum(next_dims) + sum(mask.bit_count() for mask in next_masks) + require(rank_after > rank_before, "strictly increasing state rank") + gaps = tuple(contact_dim - dims[k] for k in (i, j) if contact_dim > dims[k]) + for tail in visit(*next_state): + profiles.add(tuple(sorted(gaps + tail))) + return frozenset(profiles) + + profiles = visit((1, 2, 4), tuple(map(dimension, starts))) + mass = sum(end_dims) - sum(map(dimension, starts)) + require(all(sum(p) == mass for p in profiles), "all terminal gaps charged") + return profiles, visit.cache_info().currsize + + +def concave_floor(old, other): + """Integer certificate for every increasing concave f with f(0)=0. + + Equal mass and ordered capped-rank sums imply the cost ordering. + README proves the discrete-slope expansion; no floating point is used. + """ + return (sum(old) == sum(other) and all( + sum(min(r, cap) for r in old) <= sum(min(r, cap) for r in other) + for cap in range(1, 10))) + + +def boundary_record(window): + def basis(space): + out, generated = [], {0} + for vector in sorted(space): + if vector not in generated: + out.append(vector) + generated.update(x ^ vector for x in tuple(generated)) + require(generated == space, "canonical basis spans frame") + return out + names = {"starts": "start_bases", "ends": "exit_bases", "frames": "contact_bases"} + return {names.get(key, key): ([basis(s) for s in value] if key in names else value) + for key, value in window.items()} + + +def compute(): + authenticate() + windows = extract_windows(*constructor_data()) + require(len(windows) == 128, "128 eligible source windows") + require(len({w["index"] for w in windows}) == 128, "unique window indices") + require(Counter(w["phase"] for w in windows) == {"B": 123, "cleanup_tail": 5}, "phase census") + rows = [] + for window in windows: + old = incumbent_profile(window) + profiles, states = relaxed_profiles(window["starts"], window["ends"]) + require(old in profiles, "incumbent admitted at " + str(window["index"])) + require(all(concave_floor(old, p) for p in profiles), "concave floor at " + str(window["index"])) + rows.append({**boundary_record(window), "incumbent_ranks": list(old), + "relaxed_rank_partitions": [list(p) for p in sorted(profiles)], + "states": states, "concave_floor": True}) + return {"status": "PASS_RECEIVER_ALL_LENGTH_CONCAVE_FLOOR", "windows": rows, + "window_count": len(rows), "state_count": sum(r["states"] for r in rows), + "partition_count": sum(len(r["relaxed_rank_partitions"]) for r in rows), + "boundary_sha256": hashlib.sha256(canonical([boundary_record(w) for w in windows])).hexdigest(), + "word_length_cap": None, "coefficient_cap": None, + "cost_scope": "Every increasing concave rank weight f with f(0)=0; in particular r^q for 0