Prove a restored partial Y-exit round trip does not lower the paid moment (no κ)

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.

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.

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"
+    }
+  ]
+}

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."
+    }
+  ]
+}

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."
+    }
+  ]
+}