From 2d5b12d44fdb6de790016c716700568432d94393 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 10 Nov 2026 13:26:31 +0000 Subject: [PATCH] Prove a restored partial Y-exit round trip does not lower the paid moment. On the pinned round-three centre word, every nonempty subset of the rank-8 Y exits raises the exponent-1 moment when final charts stay, and the scalar pins force a 2k increase at every exponent. No kappa change. Co-authored-by: unpaidmoon --- research/y-exit-partial-round-trip/PROOF.md | 115 +++++++ research/y-exit-partial-round-trip/README.md | 83 ++++++ .../y-exit-partial-round-trip/SOURCES.json | 30 ++ research/y-exit-partial-round-trip/TASK.json | 81 +++++ .../y-exit-partial-round-trip/VERIFY.json | 21 ++ research/y-exit-partial-round-trip/verify.py | 280 ++++++++++++++++++ 6 files changed, 610 insertions(+) create mode 100644 research/y-exit-partial-round-trip/PROOF.md create mode 100644 research/y-exit-partial-round-trip/README.md create mode 100644 research/y-exit-partial-round-trip/SOURCES.json create mode 100644 research/y-exit-partial-round-trip/TASK.json create mode 100644 research/y-exit-partial-round-trip/VERIFY.json create mode 100644 research/y-exit-partial-round-trip/verify.py diff --git a/research/y-exit-partial-round-trip/PROOF.md b/research/y-exit-partial-round-trip/PROOF.md new file mode 100644 index 0000000000..8044c84d66 --- /dev/null +++ b/research/y-exit-partial-round-trip/PROOF.md @@ -0,0 +1,115 @@ +# A restored partial Y-exit round trip does not lower the paid moment + +This is a paid-moment obstruction for one finite schedule. It is not a new κ, +not a decoder of the selected #6030 word, and not a claim about every centre +word. The selected value stays `781451/250000000`. + +The schedule is the pinned round-three centre word +`research/sol1337-contact-frontier/inputs/round3-native.json.gz`, SHA-256 +`7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05`, emitted by +the retained centre extension +`research/sol1337-contact-frontier/vendor/retained_verify.py`. Cao Yifan / +intqwq, PR #4610, is the source of the word. The all-112 round trip, and the +question this note answers, are +`research/y-exit-rank-lift-obstruction`. + +## Hypotheses + +A chart is one of the word's recorded frames. Its dimension is the length of +its basis. The retained span check makes that basis independent. A transport +from chart `A` to chart `B` is legal only when the two spans are strictly +nested, and its width is `abs(dim A - dim B)`. That width is the rank of the +paid child. A warp may change the current chart, but every warp considered +here preserves dimension. The emitted word has 240 warps, and each of them +does. A scalar add, scale, or warp pins every participating role to the chart +recorded on that event. + +The emitted final charts stay in force: roles `0..631` end on +`canonical["final"]`, and the eight centre roles `632..639` end on the empty +chart `0`. In particular every rank-8 Y exit is restored. Roles `112..223` +are the Y block and roles `224..631` are the helper block, in the retained +centre-extension indexing. + +## The emitted walk meets the variation bound + +On one role, dimension changes only on transports, and each transport +contributes exactly its width to the total variation. A walk from dimension +`s` to dimension `t` therefore has rank mass at least `abs(t - s)`. Equality +holds exactly when the walk is monotone. + +The checker walks all 640 roles on the emitted events. Every role meets +equality, the eight centre roles are a single downward step of width 8 onto +chart 0, and every other role only increases dimension. The total rank mass +is 5327, which is also the exponent-1 paid moment of the retained histogram + +```text +{1: 2201, 2: 412, 3: 510, 4: 127, 5: 40, 8: 8}. +``` + +There is one frame of dimension 9, frame 1. Each of the 112 Y exits is a +distinct dimension-8 chart strictly inside that frame, and each Y role runs +from the empty chart to its exit. A round trip from that exit to frame 1 and +back is two nested width-1 transports. Any non-monotone integer walk from 0 +to 8 has variation at least 10, because a variation strictly above the net +change jumps by at least 2. + +## Exponent 1, with helper calls rewritten or deleted + +Let a schedule use only nested transports of width `abs(Δ dim)` and +dimension-preserving warps, and let it preserve every start chart and every +emitted final chart. Its exponent-1 paid moment equals its rank mass, and +that mass is at least 5327. The emitted schedule attains 5327. + +If `k ≥ 1` of the Y roles are not monotone, their extra variation contributes +at least `2k`, so the moment is at least `5327 + 2k`. A restored round trip +of any nonempty set of Y exits is one such schedule: those roles visit frame +1 and return, and the other final charts can stay monotone. Deleting or +rewriting helper transports cannot fund the difference while the helper +final charts stay, because those roles are already at their net variation. +Deleting a helper scalar add does not remove a paid child; it changes the +operator, and it still leaves the dimension lower bound in place. + +So no chart-preserving route that round-trips one or more rank-8 Y exits +lowers the exponent-1 paid moment. The optimistic credit in the predecessor, +deleting the eight width-8 centre transports for 64 rank mass, drops the +centre roles off chart 0. It is not available under this endpoint. Even if +that credit were granted, `k ≥ 33` would still leave a positive gap at +exponent 1, since `2·33 - 64 = 2`. The chart-preserving argument does not +need that credit, and it covers every nonempty `k`, including `k = 1`. + +## The scalar program fixes the histogram at every exponent + +A stronger statement holds when the emitted scalar, scale, and warp events +stay in order, on their recorded charts. Every one of the 3298 transports is +followed, before the next transport of that role, by a participant event +whose chart is the transport's arrival chart. The checker counts one such +next pin for every transport. Some of those gaps also contain a +same-dimension warp, after an add on the arrival chart; the warp does not +remove the pin, and the following transport leaves the post-warp chart. + +Removing a transport therefore leaves that next pin on the wrong chart. +Replacing the step costs at least the same width, because the width is +already the dimension gap. The paid histogram is forced. + +Inserting a round trip after a Y role's last pinned event, out to frame 1 and +back, restores that exit and does not move any earlier pin. The checker does +this for Y role 112. The retained matrix is unchanged, and the histogram +gains exactly two rank-1 children. A rank-1 child contributes `1^θ = 1` at +every real exponent `θ`. The paid moment therefore rises by exactly `2k` at +every `θ` in `(0, 1]`, for a restored round trip of `k` exits, whenever the +other transports stay. + +That is the route named by the predecessor's first open question, including +the clause that helper targets stay fixed. Helper-transport deletion is not +an extra degree of freedom under those pins. + +## What is not claimed + +No selected-word decoder, native phase, or κ changes. Unknown caller, +precision, and tape costs are not set to zero; the paid side of the inserted +round trip is already strictly higher. The one-way move onto frame 1, which +does not restore the rank-8 exits, is still the predecessor's second +question. A warp that changed dimension would be a different alphabet; the +emitted warps do not, and this note does not construct one. The argument is +this word's event list plus the variation lemma. It is not a search, and it +does not enumerate other centre words. diff --git a/research/y-exit-partial-round-trip/README.md b/research/y-exit-partial-round-trip/README.md new file mode 100644 index 0000000000..be8fe41fa9 --- /dev/null +++ b/research/y-exit-partial-round-trip/README.md @@ -0,0 +1,83 @@ +# A restored partial Y-exit round trip does not lower the paid moment + +**Scoped proof on one finite schedule. No new κ.** The selected value stays +`781451/250000000`. + +On the pinned round-three centre word, with every emitted final chart kept, +a round trip of any nonempty set of the 112 rank-8 Y exits through frame 1 +raises the exponent-1 paid moment by at least twice the number of exits. +When the emitted scalar, scale, and warp events stay on their recorded +charts, the paid histogram itself is forced, and the same round trip raises +the paid moment by exactly `2k` at every exponent in `(0, 1]`. Deleting a +helper transport cannot pay for that increase while the helper's final chart +stays. The selected frontier is unchanged. + +The argument is in [PROOF.md](PROOF.md). The checker walks the emitted +events and replays one inserted round trip. It does not trust the counts +above as inputs. + +## Scope and evidence + +Catalogue card `complex-rank-shape-decoder`, priority revision 8, base +commit `17469fff78c22941280f04d39dc5a1faee09c840`. Scope status: +**changed**. The card asks whether a decoder or coframe change improves the +full signed moment. This package does not build that decoder. It answers the +first open question of +[research/y-exit-rank-lift-obstruction](../y-exit-rank-lift-obstruction): +whether moving only some Y exits, or also deleting helper calls, can clear +a paid moment while restoring every rank-8 Y exit. The reason is in +[TASK.json](TASK.json). + +The all-112 round trip in that package costs 224 rank-1 children against an +optimistic centre credit of 64. That credit drops the centre roles off the +empty chart. The partial route was not priced. Here the endpoint keeps +every final chart, so the centre credit is not spent, and every nonempty +subset loses. + +Source pins are in [SOURCES.json](SOURCES.json). The catalogue and selected +record are provenance at the base commit. Full Git history is needed to +resolve them. The word and the retained emitter are live inputs. + +## Reproduce + +Python 3.12, standard library, from the repository root: + +```sh +python3 -B research/y-exit-partial-round-trip/verify.py +python3 -O -B research/y-exit-partial-round-trip/verify.py +python3 -B scripts/research_package.py --package research/y-exit-partial-round-trip --check-only +python3 -B scripts/research_package.py --package research/y-exit-partial-round-trip +``` + +The marker is `PASS_Y_EXIT_PARTIAL_ROUND_TRIP` with `y=112`, +`forced_transports=3298`, `rank_mass=5327`, and +`moment_increase_per_exit=2`. + +The positive fixture inserts the frame-1 round trip on Y role 112 after its +last pinned event. The matrix matches the retained replay, and the histogram +gains two rank-1 children. Controls reject deleting one transport, a width-2 +reading of the frame-1 gap, and the empty exit set. Not run: a physical +caller, Lean, Docker, and `make frontier6030-verify`. +`scripts/research_selected_baseline.py` is a binding check only. + +## Open next questions + +1. Can the one-way move of every Y exit onto frame 1 be accepted as an + endpoint? The predecessor already shows a rank-mass gap of at least 48, + and that move replaces each rank-8 exit by frame 1. The restored-exit + argument here does not apply. The first step is the same comparison of + one Y role's exit chart before and after the one-way transport. +2. Does a dimension-changing warp, outside the 240 same-dimension warps on + this word, give an unpaid path from a Y exit to frame 1? No such warp is + constructed here. The first step is one retained warp opcode whose source + and destination charts differ in dimension, or a proof that the native + alphabet forbids that pair. + +## Credit + +The word is Cao Yifan / intqwq, PR #4610. The emitter and the width law are +the retained centre extension. The all-Y obstruction and the open question +are `research/y-exit-rank-lift-obstruction`, which credits discussion #1166 +comment 19133861, Chris R / Clear1nsight, for the 224-against-64 stop. +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +No independent human review or proof-kernel check is claimed. diff --git a/research/y-exit-partial-round-trip/SOURCES.json b/research/y-exit-partial-round-trip/SOURCES.json new file mode 100644 index 0000000000..ca6b9e24ea --- /dev/null +++ b/research/y-exit-partial-round-trip/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/sol1337-contact-frontier/inputs/round3-native.json.gz", + "usage": "input", + "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e", + "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" + }, + { + "path": "research/sol1337-contact-frontier/vendor/retained_verify.py", + "usage": "input", + "git_blob": "357cbff9874ce920c5b5ad839fd47d3f9c728bcb", + "sha256": "f5a67954f19dddc688460b91e5c1729d7820755c53313159ed136e4447021214" + } + ] +} diff --git a/research/y-exit-partial-round-trip/TASK.json b/research/y-exit-partial-round-trip/TASK.json new file mode 100644 index 0000000000..51dcae086e --- /dev/null +++ b/research/y-exit-partial-round-trip/TASK.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "On the pinned round-three centre word, a restored round trip of any nonempty subset of the 112 rank-8 Y exits through frame 1 does not lower the exponent-1 paid moment while every emitted final chart stays. With the emitted scalar, scale, and warp pins kept, the paid histogram is forced and the moment rises by exactly 2k at every exponent in (0, 1].", + "scope_change_reason": "The card asks for a decoder or coframe change that improves the signed moment. This package does not build that decoder. It answers the partial Y-exit question left open by research/y-exit-rank-lift-obstruction, on the #4610 round-three word rather than on the selected #6030 word.", + "bottleneck_link": "A favourable complex itinerary has to clear a complete signed bill. Moving any nonempty set of these Y exits and restoring them raises the exponent-1 paid moment, so the route stops before a selected-word decoder or a kappa claim.", + "budget_minutes": 60, + "stop_rule": "Stop once every nonempty restored Y-exit round trip is shown to raise the exponent-1 moment under the emitted final charts. Do not search a new #6030 decoder, and do not accept the one-way frame-1 endpoint.", + "outcome": "negative-result", + "evidence": "python3 -B research/y-exit-partial-round-trip/verify.py prints PASS_Y_EXIT_PARTIAL_ROUND_TRIP. PROOF.md records the variation lemma and the pinned-chart argument. The checker replays one inserted round trip and matches the retained matrix.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance with the proof and the checker. The word and the retained emitter are predecessor source.", + "open_questions": [ + { + "question": "Can the one-way move of every Y exit onto frame 1 be accepted as an endpoint?", + "why_it_matters": "That move still leaves a gap of at least 48 in the predecessor account, but it replaces each rank-8 Y exit by frame 1, so the restored-exit theorem does not apply.", + "first_step": "Compare one Y role's exit chart before and after the one-way transport and state whether the retained endpoint allows frame 1.", + "blocked_by": "The retained endpoint uses the rank-8 Y charts. Accepting frame 1 is a changed endpoint contract." + }, + { + "question": "Does one retained warp opcode change dimension, and could that warp carry a Y exit to frame 1 without a paid transport?", + "why_it_matters": "The variation bound charges only transports. All 240 emitted warps preserve dimension. A dimension-changing warp would be a different alphabet.", + "first_step": "Find one emitted warp whose source and destination charts differ in dimension, or show that the native warp alphabet forbids that pair.", + "blocked_by": "No dimension-changing warp is present on this word, and none is constructed here." + } + ] +} diff --git a/research/y-exit-partial-round-trip/VERIFY.json b/research/y-exit-partial-round-trip/VERIFY.json new file mode 100644 index 0000000000..afb92ebe9c --- /dev/null +++ b/research/y-exit-partial-round-trip/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/sol1337-contact-frontier/inputs/round3-native.json.gz", + "research/sol1337-contact-frontier/vendor/retained_verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Walk all 640 roles, force each of the 3298 transports by its next pin, insert one restored Y-exit round trip, match the retained matrix, and reject a deleted transport." + } + ] +} diff --git a/research/y-exit-partial-round-trip/verify.py b/research/y-exit-partial-round-trip/verify.py new file mode 100644 index 0000000000..41837428dd --- /dev/null +++ b/research/y-exit-partial-round-trip/verify.py @@ -0,0 +1,280 @@ +#!/usr/bin/env python3 +"""A restored partial Y-exit round trip does not lower the paid moment. + +The round-three word and the retained emitter are predecessor inputs. This +checker recomputes the chart walk. It does not trust the counts in PROOF.md +as inputs. Failures raise ValueError, including under python -O. +""" + +from collections import Counter +from hashlib import sha256 +from pathlib import Path +import gzip +import importlib.util +import json + +ROOT = Path(__file__).resolve().parents[2] +HERE = Path(__file__).resolve().parent +WORD = ROOT / "research/sol1337-contact-frontier/inputs/round3-native.json.gz" +ENGINE = ROOT / "research/sol1337-contact-frontier/vendor/retained_verify.py" + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load_engine(): + spec = importlib.util.spec_from_file_location("retained_centre_verify", ENGINE) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def authenticate(engine): + pins = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")) + by_path = {row["path"]: row for row in pins["files"]} + for path in (WORD, ENGINE): + rel = path.relative_to(ROOT).as_posix() + raw = path.read_bytes() + need(sha256(raw).hexdigest() == by_path[rel]["sha256"], "changed input " + rel) + raw = WORD.read_bytes() + need(sha256(raw).hexdigest() == engine.SOURCE_HASH, "word hash disagrees with the retained emitter") + return json.loads(gzip.decompress(raw)) + + +def required_chart(event, role): + kind = event[0] + if kind in ("add", "copy"): + if role in (event[1], event[2]): + return event[4] + elif kind == "scale": + if role == event[1]: + return event[3] + elif kind == "warp": + if role == event[1]: + return event[3] + elif kind == "transport": + if role == event[1]: + return event[2] + return None + + +def participant(event, role): + return required_chart(event, role) is not None + + +def survey(engine, payload, starts, events): + frames = payload["canonical"]["frames"] + final = payload["canonical"]["final"] + dims = [len(basis) for basis in frames] + spaces = list(map(engine.span, frames)) + ambient = payload["canonical"]["h"] + block = payload["canonical"]["v"] + need(ambient == 9 and block == 112, "ambient dimension and block length") + full = [index for index, basis in enumerate(frames) if len(basis) == ambient] + need(full == [1], "one retained rank-9 frame") + full_id = full[0] + y_ids = [final[role] for role in range(block, 2 * block)] + need(len(set(y_ids)) == block, "112 distinct Y exit charts") + for chart in y_ids: + need(dims[chart] == ambient - 1, "every Y exit chart has dimension 8") + need(spaces[chart] < spaces[full_id], "every Y exit chart sits inside frame 1") + need(abs(dims[chart] - dims[full_id]) == 1, "the frame-1 round trip has width 1 each way") + + histogram = Counter() + forced = 0 + warp_count = sum(1 for event in events if event[0] == "warp") + for event in events: + if event[0] == "warp": + need(dims[event[3]] == dims[event[4]], "emitted warp preserves dimension") + mass = 0 + for role in range(640): + end = final[role] if role < 632 else 0 + current = starts[role] + variation = 0 + transport_at = [index for index, event in enumerate(events) + if event[0] == "transport" and event[1] == role] + first = transport_at[0] if transport_at else len(events) + for item in events[:first]: + chart = required_chart(item, role) + if chart is None: + continue + need(current == chart, "pin before the first transport") + if item[0] == "warp" and item[1] == role: + current = item[4] + for nth, index in enumerate(transport_at): + event = events[index] + source, dest, width = event[2], event[3], event[4] + need(current == source, "transport departs from the chart the walk reached") + need(spaces[source] < spaces[dest] or spaces[dest] < spaces[source], "strict nesting") + need(width == abs(dims[dest] - dims[source]) and width >= 1, "width is the positive dimension gap") + nxt = transport_at[nth + 1] if nth + 1 < len(transport_at) else len(events) + pins = [item for item in events[index + 1:nxt] if required_chart(item, role) is not None] + need(pins, "every transport is followed by a pinned use of its arrival chart") + need(required_chart(pins[0], role) == dest, "the next pin requires the arrival chart") + forced += 1 + variation += width + histogram[width] += 1 + current = dest + for item in pins: + chart = required_chart(item, role) + need(current == chart, "later pin in this gap is on the walked chart") + if item[0] == "warp" and item[1] == role: + current = item[4] + need(current == end, "walk ends on the emitted final chart") + net = abs(dims[end] - dims[starts[role]]) + need(variation == net, "role rank mass equals the net dimension change") + mass += variation + if block <= role < 2 * block: + need(dims[starts[role]] == 0 and dims[end] == 8, "Y role runs from dimension 0 to 8") + need(events[[index for index, event in enumerate(events) if participant(event, role)][-1]][0] == "add", + "Y role's last pin is an add on the exit chart") + need(forced == sum(histogram.values()) == 3298, "every transport is forced by the next pin") + need(mass == 5327, "emitted rank mass meets the variation lower bound") + need(dict(histogram) == engine.PAID, "walked histogram is the retained paid invoice") + need(warp_count == 240, "every emitted warp was a same-dimension chart change") + return {"full_id": full_id, "histogram": histogram, "mass": mass, "forced": forced} + + +def insert_round_trip(events, role, full_id, frames): + """After the role's last pinned event, visit frame 1 and return.""" + last = None + for index, event in enumerate(events): + if participant(event, role): + last = index + need(last is not None, "Y role has a pinned event") + # The walk's chart after `last` is the exit. Read it from that event. + event = events[last] + if event[0] == "transport" and event[1] == role: + chart = event[3] + elif event[0] == "warp" and event[1] == role: + chart = event[4] + else: + chart = required_chart(event, role) + need(len(frames[chart]) == 8, "insertion starts on the rank-8 exit") + need(len(frames[full_id]) == 9, "frame 1 has dimension 9") + added = [("transport", role, chart, full_id, 1), + ("transport", role, full_id, chart, 1)] + return events[:last + 1] + added + events[last + 1:], chart + + +def replay_matrix(engine, payload, starts, events, expect_paid): + """Same chart and row rules as the retained replay, with an explicit histogram.""" + from fractions import Fraction as Q + + rows = [{(i, ()): Q(1)} for i in range(engine.N)] + current = starts[:] + frames = payload["canonical"]["frames"] + spaces = list(map(engine.span, frames)) + paid = Counter() + for event in events: + kind, role = event[:2] + if kind in ("add", "copy"): + _, _, source, coefficient, frame = event + need(role != source and current[role] == current[source] == frame, + "scalar common chart") + need(kind == "add", "this schedule has no baseline copy") + engine.plus(rows[role], rows[source], coefficient) + elif kind == "scale": + _, _, coefficient, frame = event + need(current[role] == frame and coefficient != 0, "scale chart") + rows[role] = {key: coefficient * value for key, value in rows[role].items()} + elif kind == "transport": + _, _, source, dest, width = event + need(current[role] == source, "paid source chart") + need(spaces[source] < spaces[dest] or spaces[dest] < spaces[source], "nested") + need(width == abs(len(frames[source]) - len(frames[dest])), "width") + paid[width] += 1 + current[role] = dest + else: + _, _, symbol, source, dest = event + need(kind == "warp" and current[role] == source, "warp source chart") + out = {} + for (variable, word), value in rows[role].items(): + word = word[1:] if word and word[0] == -symbol else (symbol,) + word + engine.plus(out, {(variable, word): value}) + rows[role] = out + current[role] = dest + finals = payload["canonical"]["final"] + [0] * 8 + need(current == finals, "all 640 output charts") + need(dict(paid) == expect_paid, "paid histogram") + decoded = [{i: value for (i, _), value in row.items()} for row in rows] + return decoded + + +def moment_increase(exit_count): + need(type(exit_count) is int and exit_count >= 1, "nonempty exit set") + # Each added child has rank 1, and 1**theta == 1 for every real theta. + return 2 * exit_count + + +def controls(engine, payload, starts, events, facts): + frames = payload["canonical"]["frames"] + full_id = facts["full_id"] + role = 112 + augmented, chart = insert_round_trip(events, role, full_id, frames) + original_paid = dict(facts["histogram"]) + raised = dict(original_paid) + raised[1] = raised[1] + 2 + original_rows = replay_matrix(engine, payload, starts, events, original_paid) + engine_rows = engine.replay(payload, starts, events) + need(original_rows == engine_rows, "local replay matches the retained matrix") + moved_rows = replay_matrix(engine, payload, starts, augmented, raised) + need(moved_rows == original_rows, "one restored round trip preserves the operator") + need(moment_increase(1) == 2 and moment_increase(112) == 224, "moment increase is twice the exit count") + need(moment_increase(33) - 64 == 2, "even the optimistic centre credit loses for 33 exits at theta 1") + + # Deleting the first transport leaves the next pin on the wrong chart. + first = next(index for index, event in enumerate(events) if event[0] == "transport") + skipped = events[:first] + events[first + 1:] + rejected = False + try: + replay_matrix(engine, payload, starts, skipped, original_paid) + except ValueError: + rejected = True + need(rejected, "deleting one transport misses a pinned chart") + + # A centre transport is the unique step onto the empty chart. + centre = next(event for event in events if event[0] == "transport" and event[1] == 632) + need(centre[3] == 0 and centre[4] == 8, "centre role 632 ends by a width-8 step onto chart 0") + + def bad_width(): + need(abs(len(frames[chart]) - len(frames[full_id])) == 2, "wrong width") + + rejected = False + try: + bad_width() + except ValueError: + rejected = True + need(rejected, "width 2 is not the frame-1 gap") + + def empty_set(): + moment_increase(0) + + rejected = False + try: + empty_set() + except ValueError: + rejected = True + need(rejected, "the empty exit set is not a partial round trip") + + +def main(): + engine = load_engine() + payload = authenticate(engine) + starts, centers, events = engine.emit(payload) + need(len(centers) == 8 and len(starts) == 640, "eight centre inputs") + facts = survey(engine, payload, starts, events) + controls(engine, payload, starts, events, facts) + print( + "PASS_Y_EXIT_PARTIAL_ROUND_TRIP " + "y=112 forced_transports=3298 " + "rank_mass=5327 moment_increase_per_exit=2 " + "one_exit_preserves_operator=true " + "histogram_forced=true no_new_kappa=true" + ) + + +if __name__ == "__main__": + main()