diff --git a/research/shared-chart-centre-visit/PROOF.md b/research/shared-chart-centre-visit/PROOF.md new file mode 100644 index 0000000000..dea4f8901a --- /dev/null +++ b/research/shared-chart-centre-visit/PROOF.md @@ -0,0 +1,101 @@ +# One shared exit-chart visit still loses + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. + +This is a scoped negative result in the chart model of +`research/center-chain-terminal-feasibility`. It does not change κ, admit a +caller, or replay the Clifford compiler. The selected conditional exponent +stays `60403/20000000`. + +## What #4839 already charges + +After the normalized #4694/#4698 word, centre `j` exits on the empty chart +with value `z_j + R_j x`. The support of `R_j` is 56 X coordinates plus one +pivot helper. Each affected Y coordinate carries a nonzero multiple of that +centre. The strip-all policy moves every one of those registers to the empty +chart, subtracts, and restores it. + +For centre 0 that bill is `112` width-8 transports and `114` width-9 +transports, against one optimistic rank-8 reward. The same sign holds for +every singleton, every pair, and the full set of eight centres. + +## The changed word + +The source frames give a stricter geometry than “one strip per register”: + +- Chart 0 is the empty frame. +- Chart 1 is one width-9 frame, and the empty frame is strictly contained in it. +- All 57 observation supports of every centre, including the pivot, exit on chart 1. +- Each of the 112 affected Y charts is a distinct width-8 frame strictly contained in chart 1. The dimension gap is 1. + +The retained evaluator charges a transport only when the two frames are +nested, and the recursive width is the difference of their lengths. A common +chart is required for an ADD. Transport does not change the scalar +coefficient vector; it changes only the chart label. + +So the following word is legal. For a selected set `S`: + +1. Transport each selected centre from chart 0 to chart 1. Width 9. +2. Subtract that centre’s whole observation at chart 1. +3. For each distinct affected Y field, hop that field from its chart up to chart 1, subtract every selected centre that touches it, and hop back. Each hop has width 1. +4. Transport each selected centre back to chart 0. Width 9. + +Every original exit chart is restored. No register is created or discarded. +X registers are never moved. The scalar map is exactly the strip-all map, +because the same coefficients are subtracted and transport contributes the +identity on coefficients. + +## Bill + +Let `s = |S|`, let `n_Y` be the number of distinct affected Y fields, and let +`t = 1 - C` with `C` in `[0, 1]`. The new recursive requests are + +```text +2 n_Y of width 1, +2 s of width 9. +``` + +The optimistic new reward remains `s` rank-8 jobs, the same grant used by +#4839, including a free positive-job normalization. Scalar ADDs, routing, +storage and precision are given cost zero in this screen. The resulting +incremental moment is at most + +```text +Delta(t) = s * 8^t - 2 n_Y - 2 s * 9^t. +``` + +For real `t >= 0`, `9^t >= 8^t >= 1`. Therefore + +```text +Delta(t) <= -s * 8^t - 2 n_Y <= -s - 2 n_Y. +``` + +The census, checked on all 37 selections, is: + +| Selection | `n_Y` | Added requests | `Delta` upper bound | Same bound if both width-9 moves are free | +| --- | ---: | --- | ---: | ---: | +| Each singleton | 56 | 112 width 1 + 2 width 9 | -113 | -104 | +| Each pair | 88 | 176 width 1 + 4 width 9 | -178 | -160 | +| All eight | 112 | 224 width 1 + 16 width 9 | -232 | -160 | + +The free-round-trip column uses only `8^t <= 8`, so `s * 8^t - 2 n_Y <= 8 s - 2 n_Y`. The width-9 charges are not what keeps the sign negative. One rank-8 reward is worth at most 8 on this interval, and the width-1 hops alone cost `2 n_Y >= 112`. + +The old strip bill for centre 0 was `112` width-8 requests and `114` width-9 requests. The same endpoint is now `112` width-1 requests and `2` width-9 requests. That is a real reduction, and it is still strictly negative on the whole interval. + +## Finite certificate + +`verify.py` rebuilds the normalized source word from the pinned #4694 emitter and the pinned helper-normalization header. For every one of the 37 selections it checks: + +- the shared-visit endpoint equals the declared target; +- the strip-all endpoint equals that same target; +- the gatewise raw inverse transpose of the shared visit equals the transpose of the two-sided scalar inverse; +- the paid widths are exactly the counts above; +- six malformed tails are rejected: a missing X term, a missing Y correction, an ADD on the empty chart against a chart-1 register, a width-8 charge for the width-9 centre hop, a centre hop that claims to start on chart 1 before arrival, and a width-2 charge for a width-1 Y hop. + +The source profile remains `{1:2201, 2:412, 3:510, 4:127, 5:40, 8:8}`. The joint 379+379 normalization is not removed. + +## What this does not show + +This is not a lower bound for every heterogeneous producer. A word that changes Y’s exit frames, changes which registers may share a chart, or changes the demanded outputs can have a different bill. The evaluator’s rule that transport preserves scalar coefficients is the predecessor’s rule; this package does not replace it with a fresh phase-aware Clifford execution. Chart 1’s frame was already one of the frames lowered in #4839, but those recipes are not rerun here. + +Direct hops between two Y charts are not used. Those charts need not be nested, and this schedule does not need them: every Y chart meets chart 1 in one rank. diff --git a/research/shared-chart-centre-visit/README.md b/research/shared-chart-centre-visit/README.md new file mode 100644 index 0000000000..5350936551 --- /dev/null +++ b/research/shared-chart-centre-visit/README.md @@ -0,0 +1,83 @@ +# Shared exit-chart visit for the centre-chain observation + +**Scoped negative result. No new κ.** The selected conditional exponent stays +`60403/20000000`. + +#4839 shows that stripping every touched register of the heterogeneous +centre-chain terminal loses on `C in [0,1]`. Its open question is whether one +changed physical word can avoid those chart strips and still preserve the +observations, the centre-to-Y corrections, and the original returns. + +This package gives one such word. Every observation support already exits on +chart 1, and every affected Y chart is a width-8 subspace of chart 1. Each +selected centre makes one width-9 round trip onto chart 1. Each distinct Y +field makes a width-1 hop up to that chart, subtracts, and hops back. The +scalar endpoint matches the strip-all terminal on all eight singletons, all +28 pairs, and the octet. The raw inverse transpose matches for the same 37 +words. + +The incremental moment stays negative. For centre 0 the new bill is 112 +width-1 requests and 2 width-9 requests, against one optimistic rank-8 +reward. Its upper bound on `t = 1-C in [0,1]` is `-113`. Granting the width-9 +round trip for free still leaves `-104`, because one rank-8 reward is worth +at most 8 and the width-1 hops cost 112. The strip-all bill for the same +endpoint was 112 width-8 requests and 114 width-9 requests. + +The argument and the exact census are in [PROOF.md](PROOF.md). The machine +receipt is [RESULT.json](RESULT.json). + +## Scope and evidence + +Task card: `complex-new-helper-inventory`, refined to handoff +[#1166 comment 19133212](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133212) +and the first open question of #4839. The scope change is recorded in +[TASK.json](TASK.json). This does not beat a packing ceiling and does not +propose a new helper alphabet outside the retained chart model. + +Base commit `ff3cc58e370d0f678e529246f8c73e8094e18fcf`. Live inputs are the +#4694 emitter, its ABI and native payload, and the helper-normalization +header. Pins are in [SOURCES.json](SOURCES.json). + +Not run: a fresh Clifford lowering, a rounded or fixed-tape execution, and +any compiler or outer admission check. Unknown costs are not treated as a +reason to continue this schedule. The sign is already negative with those +costs set to zero. + +## Reproduce + +Python 3.12, standard library, from the repository root. The registered +command takes about one minute here. + +```sh +python3 -B scripts/research_package.py --package research/shared-chart-centre-visit --check-only +python3 -B scripts/research_package.py --package research/shared-chart-centre-visit +python3 -B research/shared-chart-centre-visit/verify.py +``` + +The direct command prints `PASS_SHARED_CHART_CENTRE_VISIT_STILL_LOSES no_new_kappa`. + +## Open next questions + +1. Can a producer whose Y registers do not each occupy a private width-8 + subspace of chart 1 avoid the 112 width-1 hops while restoring every + demanded output? The present loss survives even if the centre’s width-9 + round trip is free, so another visit to chart 1 is not the missing saving. + First step: name a source-bound exit frame in which at least two affected + Y fields already coincide, and price one correction there. Blocked by the + actual frames: the 112 Y charts are pairwise distinct. +2. Does a changed output contract, rather than a changed transport, delete + the centre-to-Y corrections? First step: state which of the 56 centre-0 Y + outputs may legally stay contaminated, and reprice only the retained + corrections. Blocked until that demand is part of the caller, not an + omission inside this terminal. + +## Credit + +The terminal loss, evaluator contract and 640-input offer are Chris R / +Clear1nsight’s #4839, using Cinna Davis’s #4694/#4698 interface and Cao +Yifan / intqwq’s #4610 route, with the retained helper-normalization and +Clifford lineage named in that package. This package does not modify those +sources. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. New work is +Apache-2.0. diff --git a/research/shared-chart-centre-visit/RESULT.json b/research/shared-chart-centre-visit/RESULT.json new file mode 100644 index 0000000000..12c2df2dc9 --- /dev/null +++ b/research/shared-chart-centre-visit/RESULT.json @@ -0,0 +1,812 @@ +{ + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "centre0": { + "distinct_Y": 56, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 57, + "scalar_adds": 113, + "selected": [ + 0 + ], + "shared_added_requests": { + "1": 112, + "9": 2 + }, + "strip_added_requests": { + "8": 112, + "9": 114 + }, + "uniform_upper_bound": -113, + "upper_bound_if_width9_free": -104 + }, + "compiler_route": "unchanged; no outer admission", + "controls": [ + "missing data observation", + "missing centre-to-Y correction", + "empty-chart ADD against a chart-1 support", + "undercharged centre transport", + "centre hop before arrival", + "overcharged Y hop" + ], + "groups_checked": 37, + "joint_normalization_gates": 758, + "model": "retained nested-chart ADD/transport evaluator; no fresh Clifford replay", + "new_kappa": null, + "octet": { + "distinct_Y": 112, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 120, + "scalar_adds": 904, + "selected": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "shared_added_requests": { + "1": 224, + "9": 16 + }, + "strip_added_requests": { + "8": 224, + "9": 240 + }, + "uniform_upper_bound": -232, + "upper_bound_if_width9_free": -160 + }, + "pair_distinct_Y": 88, + "pair_uniform_upper_bound": -178, + "screens": [ + { + "distinct_Y": 56, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 57, + "scalar_adds": 113, + "selected": [ + 0 + ], + "shared_added_requests": { + "1": 112, + "9": 2 + }, + "strip_added_requests": { + "8": 112, + "9": 114 + }, + "uniform_upper_bound": -113, + "upper_bound_if_width9_free": -104 + }, + { + "distinct_Y": 56, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 57, + "scalar_adds": 113, + "selected": [ + 1 + ], + "shared_added_requests": { + "1": 112, + "9": 2 + }, + "strip_added_requests": { + "8": 112, + "9": 114 + }, + "uniform_upper_bound": -113, + "upper_bound_if_width9_free": -104 + }, + { + "distinct_Y": 56, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 57, + "scalar_adds": 113, + "selected": [ + 2 + ], + "shared_added_requests": { + "1": 112, + "9": 2 + }, + "strip_added_requests": { + "8": 112, + "9": 114 + }, + "uniform_upper_bound": -113, + "upper_bound_if_width9_free": -104 + }, + { + "distinct_Y": 56, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 57, + "scalar_adds": 113, + "selected": [ + 3 + ], + "shared_added_requests": { + "1": 112, + "9": 2 + }, + "strip_added_requests": { + "8": 112, + "9": 114 + }, + "uniform_upper_bound": -113, + "upper_bound_if_width9_free": -104 + }, + { + "distinct_Y": 56, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 57, + "scalar_adds": 113, + "selected": [ + 4 + ], + "shared_added_requests": { + "1": 112, + "9": 2 + }, + "strip_added_requests": { + "8": 112, + "9": 114 + }, + "uniform_upper_bound": -113, + "upper_bound_if_width9_free": -104 + }, + { + "distinct_Y": 56, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 57, + "scalar_adds": 113, + "selected": [ + 5 + ], + "shared_added_requests": { + "1": 112, + "9": 2 + }, + "strip_added_requests": { + "8": 112, + "9": 114 + }, + "uniform_upper_bound": -113, + "upper_bound_if_width9_free": -104 + }, + { + "distinct_Y": 56, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 57, + "scalar_adds": 113, + "selected": [ + 6 + ], + "shared_added_requests": { + "1": 112, + "9": 2 + }, + "strip_added_requests": { + "8": 112, + "9": 114 + }, + "uniform_upper_bound": -113, + "upper_bound_if_width9_free": -104 + }, + { + "distinct_Y": 56, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 57, + "scalar_adds": 113, + "selected": [ + 7 + ], + "shared_added_requests": { + "1": 112, + "9": 2 + }, + "strip_added_requests": { + "8": 112, + "9": 114 + }, + "uniform_upper_bound": -113, + "upper_bound_if_width9_free": -104 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 0, + 1 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 0, + 2 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 0, + 3 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 0, + 4 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 0, + 5 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 0, + 6 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 0, + 7 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 1, + 2 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 1, + 3 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 1, + 4 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 1, + 5 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 1, + 6 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 1, + 7 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 2, + 3 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 2, + 4 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 2, + 5 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 2, + 6 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 2, + 7 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 3, + 4 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 3, + 5 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 3, + 6 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 3, + 7 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 4, + 5 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 4, + 6 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 4, + 7 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 5, + 6 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 5, + 7 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 88, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 90, + "scalar_adds": 226, + "selected": [ + 6, + 7 + ], + "shared_added_requests": { + "1": 176, + "9": 4 + }, + "strip_added_requests": { + "8": 176, + "9": 180 + }, + "uniform_upper_bound": -178, + "upper_bound_if_width9_free": -160 + }, + { + "distinct_Y": 112, + "moment_expression": "s*8^t - 2*n_Y - 2*s*9^t", + "observation_supports": 120, + "scalar_adds": 904, + "selected": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "shared_added_requests": { + "1": 224, + "9": 16 + }, + "strip_added_requests": { + "8": 224, + "9": 240 + }, + "uniform_upper_bound": -232, + "upper_bound_if_width9_free": -160 + } + ], + "source_paid": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "status": "PASS_SHARED_CHART_CENTRE_VISIT_STILL_LOSES" +} diff --git a/research/shared-chart-centre-visit/SOURCES.json b/research/shared-chart-centre-visit/SOURCES.json new file mode 100644 index 0000000000..e4e91492a4 --- /dev/null +++ b/research/shared-chart-centre-visit/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "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/center-helper-normal-form/inputs/ABI.json", + "usage": "input", + "git_blob": "ec16f7eea7d4ad1164da89b19e2021ca5f7551a6", + "sha256": "704ae450c795ed9e5eb477f924eadc209a2418f5ee4e475a4607910afdc2fdc1" + }, + { + "path": "research/center-helper-normal-form/inputs/retained_verify.py", + "usage": "input", + "git_blob": "357cbff9874ce920c5b5ad839fd47d3f9c728bcb", + "sha256": "f5a67954f19dddc688460b91e5c1729d7820755c53313159ed136e4447021214" + }, + { + "path": "research/center-helper-normal-form/inputs/round3-native.json.gz", + "usage": "input", + "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e", + "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" + }, + { + "path": "research/center-helper-normal-form/verify.py", + "usage": "input", + "git_blob": "effd566f5e85803493d7b841945a91ee1a5a0af8", + "sha256": "ff1075bd06c1ba0612983a8510639c9c7865265a0de3a01c0f87d5df0c4a534a" + }, + { + "path": "research/center-chain-terminal-feasibility/PROOF.md", + "usage": "provenance", + "git_blob": "0e2e77171adaab4214aa08e238475f24fdc57d8a", + "sha256": "ba3122bfc47e67afff9f54f761ea0ffa8580f2112361d17cecf3f65feafdcf75" + }, + { + "path": "research/center-chain-terminal-feasibility/README.md", + "usage": "provenance", + "git_blob": "ca78de7d38bfbee1313a1933396242c13c426f8d", + "sha256": "00de7499e59f57d0f66ecc24a9194cd149c705a37d567b49f5cbaaa71a42d1e9" + }, + { + "path": "research/center-chain-terminal-feasibility/verify.py", + "usage": "provenance", + "git_blob": "6ad4e8f9b516839acccdc5508faf443173b32f35", + "sha256": "a83cb28279499d75c7ebf469d4a14605e0aac76843f1b1cdafea9fd1e3634d9b" + } + ] +} diff --git a/research/shared-chart-centre-visit/TASK.json b/research/shared-chart-centre-visit/TASK.json new file mode 100644 index 0000000000..fba30be473 --- /dev/null +++ b/research/shared-chart-centre-visit/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. 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": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "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": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "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": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "refined", + "actual_scope": "After the #4839 strip-all loss, price one physical word that visits the common chart-1 exit of the centre-chain observation instead of stripping every support, retains every centre-to-Y correction and original return, and test its incremental moment.", + "scope_change_reason": "The catalogue card asks for a new local cost interface. The live handoff 19133212 and #4839's first open question ask for one concrete word that changes the strip costs of this terminal. This package prices that word inside the retained chart model and stops because the moment stays negative.", + "bottleneck_link": "A profitable heterogeneous centre consumer would be a new complex-side local profile. This schedule removes the rank-8 Y strips and all but two rank-9 observation transports, and the remaining width-1 hops still exceed the optimistic rank-8 reward, so it does not supply that profile.", + "budget_minutes": 60, + "stop_rule": "Stop if the changed word's optimistic incremental moment is negative throughout C in [0,1], including the relaxation that makes the width-9 round trip free.", + "outcome": "negative-result", + "evidence": "verify.py prints PASS_SHARED_CHART_CENTRE_VISIT_STILL_LOSES and matches RESULT.json. All 37 selections match the strip-all endpoint and the raw inverse transpose. Centre 0 costs 112 width-1 hops plus 2 width-9 transports; the uniform upper bound is -113, and -104 if the width-9 round trip is free.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance.", + "open_questions": [ + { + "question": "Can a producer whose affected Y registers are not 112 private width-8 subspaces of chart 1 avoid the width-1 hops while restoring every demanded output?", + "why_it_matters": "The width-9 centre round trip is not the obstruction: the moment stays negative even if those two transports are free.", + "first_step": "Name a source-bound exit frame in which at least two affected Y fields already coincide, and price one correction on that shared frame.", + "blocked_by": "In the pinned frames the 112 Y charts are pairwise distinct subspaces of chart 1." + }, + { + "question": "Does a changed output contract delete centre-to-Y corrections instead of transporting them?", + "why_it_matters": "Every retained correction currently costs two width-1 hops, and 112 hops already exceed one rank-8 reward.", + "first_step": "State which of centre 0's 56 Y outputs may legally remain contaminated, then reprice only the retained corrections.", + "blocked_by": "That permission has to come from the caller contract. Omitting a correction inside this terminal changes the endpoint." + } + ] +} diff --git a/research/shared-chart-centre-visit/VERIFY.json b/research/shared-chart-centre-visit/VERIFY.json new file mode 100644 index 0000000000..64b3640bc0 --- /dev/null +++ b/research/shared-chart-centre-visit/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/center-helper-normal-form/inputs/ABI.json", + "research/center-helper-normal-form/inputs/retained_verify.py", + "research/center-helper-normal-form/inputs/round3-native.json.gz", + "research/center-helper-normal-form/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "37 shared-visit endpoints, strip-all agreement, raw duals, paid widths, moment bounds, and six rejection controls" + } + ] +} diff --git a/research/shared-chart-centre-visit/verify.py b/research/shared-chart-centre-visit/verify.py new file mode 100644 index 0000000000..5e56bbe5a1 --- /dev/null +++ b/research/shared-chart-centre-visit/verify.py @@ -0,0 +1,437 @@ +#!/usr/bin/env python3 +"""Price one shared exit-chart visit for the centre-chain observation. + +The #4839 strip-all terminal moves every X support and pivot down to the empty +chart. Those supports already share chart 1, and every affected Y chart is a +width-8 subspace of that same chart. This word parks each selected centre on +chart 1 and lifts each Y by one nested rank. The endpoint matches the strip +policy. The incremental moment stays strictly negative even if the centre's +width-9 round trip is free. No new kappa. + +Chris R / Clear1nsight's evaluator contract in +research/center-chain-terminal-feasibility/verify.py is reimplemented here +with attribution; that package is not modified. Apache-2.0. +Prepared by unpaidmoon with substantial Cursor Grok assistance. +""" +from collections import Counter, defaultdict +from fractions import Fraction as Q +from hashlib import sha256 +from pathlib import Path +import itertools +import json +import sys +import types + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SRC = ROOT / 'research/center-helper-normal-form' +N = 640 + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load(path, name): + out = types.ModuleType(name) + out.__file__ = str(path) + sys.modules[name] = out + exec(compile(path.read_bytes(), str(path), 'exec'), out.__dict__) + return out + + +def authenticate(): + pins = json.loads((HERE / 'SOURCES.json').read_text(encoding='utf-8')) + need(pins['base_commit'] == json.loads((HERE / 'TASK.json').read_text(encoding='utf-8'))['base_commit'], + 'TASK and SOURCES base commits differ') + for row in pins['files']: + if row['usage'] != 'input': + continue + raw = (ROOT / row['path']).read_bytes() + need(sha256(raw).hexdigest() == row['sha256'], 'changed live input ' + row['path']) + return pins + + +def plus(dst, src, coefficient=Q(1)): + for key, value in tuple(src.items()): + value = dst.get(key, Q(0)) + coefficient * value + if value: + dst[key] = value + else: + dst.pop(key, None) + + +def identity(): + return [{i: Q(1)} for i in range(N)] + + +def mm(a, b): + out = [] + for row in a: + new = {} + for j, value in row.items(): + plus(new, b[j], value) + out.append(new) + return out + + +def transpose(a): + out = [{} for _ in a] + for i, row in enumerate(a): + for j, value in row.items(): + out[j][i] = value + return out + + +def rank(rows): + pivots = {} + for x in rows: + while x: + k = x.bit_length() - 1 + if k not in pivots: + pivots[k] = x + break + x ^= pivots[k] + return len(pivots) + + +def span(basis): + need(rank(basis) == len(basis), 'independent chart basis') + out = {0} + for v in basis: + out |= {x ^ v for x in tuple(out)} + return out + + +def evaluate(events, starts, final, frames): + """Retained nested-chart evaluator: transport changes only the chart label.""" + rows = [{(i, ()): Q(1)} for i in range(N)] + charts = list(starts) + spaces = list(map(span, frames)) + paid = Counter() + for e in events: + op, dst = e[:2] + if op == 'add': + _, _, src, q, f = e + need(dst != src and charts[dst] == charts[src] == f, 'actual scalar common chart') + plus(rows[dst], rows[src], q) + elif op == 'scale': + _, _, q, f = e + need(charts[dst] == f and q != 0, 'invertible scale chart') + rows[dst] = {k: q * v for k, v in rows[dst].items()} + elif op == 'transport': + _, _, a, b, width = e + need(charts[dst] == a and (spaces[a] < spaces[b] or spaces[b] < spaces[a]), + 'nested physical chart move') + need(width == abs(len(frames[a]) - len(frames[b])), 'derive recursive width') + paid[width] += 1 + charts[dst] = b + elif op == 'warp': + _, _, letter, a, b = e + need(charts[dst] == a, 'actual warp chart') + new = {} + for (i, word), value in rows[dst].items(): + word = word[1:] if word and word[0] == -letter else (letter,) + word + plus(new, {(i, word): value}) + rows[dst] = new + charts[dst] = b + else: + raise ValueError('unknown actual operation') + need(charts == final, 'every endpoint chart restored') + need(all(not word for row in rows for i, word in row), 'all source warp words cancel') + return [{i: v for (i, word), v in row.items()} for row in rows], paid + + +def target(abi, observations, selected): + out = identity() + for i in range(112): + out[112 + i][i] = Q(1) + for i, row in enumerate(abi['B_rows']): + plus(out[i], {j: Q(v) for j, v in row if j - 632 not in selected}) + for j, row in enumerate(observations): + if j not in selected: + plus(out[632 + j], row) + return out + + +def inverse(a): + unit = identity() + k = [dict(row) for row in a] + for i in range(N): + plus(k[i], unit[i], Q(-1)) + k2 = mm(k, k) + need(not any(mm(k2, k)), 'cube-zero endpoint') + inv = identity() + for i in range(N): + plus(inv[i], k[i], Q(-1)) + plus(inv[i], k2[i]) + need(mm(inv, a) == mm(a, inv) == unit, 'two-sided inverse') + return inv + + +def raw_dual(events): + """Predecessor tail convention: swap each ADD and leave transports in order.""" + out = [] + for e in events: + if e[0] == 'add': + out.append(('add', e[2], e[1], -e[3], e[4])) + elif e[0] == 'scale': + out.append(('scale', e[1], 1 / e[2], e[3])) + else: + need(e[0] == 'transport', 'no extra warp hidden in the tail') + out.append(e) + return out + + +def rejected(fn): + try: + fn() + except ValueError: + return True + return False + + +def y_terms(abi, centre): + terms = [] + for i, row in enumerate(abi['B_rows']): + for k, v in row: + if k == centre: + terms.append((i, centre, Q(v))) + return terms + + +def shared_tail(selected, observations, abi, final, frames): + """Park every selected centre on chart 1, correct there, then restore. + + Each affected Y chart is a width-8 subspace of chart 1, so the Y register + makes one width-1 hop up, subtracts, and hops back. The centre's own + empty-chart round trip is one width-9 hop each way. + """ + events = [] + y_by_field = defaultdict(list) + obs_fields = [] + for j in selected: + centre = 632 + j + need(final[centre] == 0, 'centre exits at the empty chart') + events.append(('transport', centre, 0, 1, len(frames[1]) - len(frames[0]))) + for i, value in sorted(observations[j].items()): + need(final[i] == 1, 'observation support exits at chart 1') + events.append(('add', centre, i, -value, 1)) + obs_fields.append(i) + for field, owner, value in y_terms(abi, centre): + y_by_field[field].append((owner, value)) + y_fields = sorted(y_by_field) + need(set(y_fields).isdisjoint(obs_fields), 'Y fields are distinct from the observation supports') + for field in y_fields: + hop = len(frames[1]) - len(frames[final[field]]) + events.append(('transport', field, final[field], 1, hop)) + for owner, value in y_by_field[field]: + events.append(('add', field, owner, -value, 1)) + events.append(('transport', field, 1, final[field], hop)) + for j in selected: + events.append(('transport', 632 + j, 1, 0, len(frames[1]) - len(frames[0]))) + return events, y_fields, obs_fields + + +def strip_tail(selected, observations, abi, final, frames): + """The predecessor policy: strip every touched field, correct, restore.""" + y_by_field = defaultdict(list) + obs_fields = [] + for j in selected: + centre = 632 + j + for i, value in observations[j].items(): + obs_fields.append(i) + for field, owner, value in y_terms(abi, centre): + y_by_field[field].append((owner, value)) + touched = sorted(set(obs_fields) | set(y_by_field)) + events = [('transport', i, final[i], 0, len(frames[final[i]])) for i in touched] + for j in selected: + centre = 632 + j + events.extend(('add', centre, i, -value, 0) for i, value in sorted(observations[j].items())) + for field, owner, value in y_terms(abi, centre): + events.append(('add', field, owner, -value, 0)) + events.extend(('transport', i, 0, final[i], len(frames[final[i]])) for i in touched) + return events + + +def moment_upper(selected_count, y_count): + """Delta = s*8^t - 2 n_Y - 2 s*9^t for t = 1-C in [0,1]. + + On that interval 1 <= 8^t <= 9^t. The 9^t terms therefore dominate the + reward, and the largest value is the t = 0 number -s - 2 n_Y. + """ + need(selected_count > 0 and y_count > 2 * selected_count, 'Y supports exceed the reward count') + upper = -selected_count - 2 * y_count + # Dropping the two width-9 charges leaves s*8^t - 2 n_Y <= 8 s - 2 n_Y. + free_round_trip = 8 * selected_count - 2 * y_count + need(upper < 0 and free_round_trip < 0, 'both relaxations stay negative') + return upper, free_round_trip + + +def paid_dict(counter): + return {str(k): counter[k] for k in sorted(counter)} + + +def run(): + pins = authenticate() + normal = load(SRC / 'verify.py', 'centre_normalizer') + engine = load(SRC / 'inputs/retained_verify.py', 'frozen_centre_emitter') + engine.HERE = SRC + payload = engine.load() + frames = payload['canonical']['frames'] + need(frames[0] == [] and len(frames[1]) == 9, 'chart 0 is empty and chart 1 has width 9') + need(span(frames[0]) < span(frames[1]), 'empty chart is strictly nested in chart 1') + abi = json.loads((SRC / 'inputs/ABI.json').read_text(encoding='utf-8')) + rows = [{i: Q(v) for i, v in row} for row in abi['R_rows']] + cold = {i for i in range(224, 632) + if payload['canonical']['start'][i] == 0 and payload['canonical']['final'][i] == 1} + header, det, _ = normal.make_header(rows, cold) + footer = normal.inverse_header(header, 1) + need(len(header) == len(footer) == 379 and det == 64, 'whole joint normalization stays charged') + starts, _centers, source = engine.emit(payload) + _, _, dual_source = engine.emit(payload, dual=True) + final = payload['canonical']['final'] + [0] * 8 + observations = [{i: v for i, v in rows[j].items() if i < 224} | {normal.J[j]: Q(1)} + for j in range(8)] + for j, piv in enumerate(normal.J): + need(final[piv] == 1 and all(final[i] == 1 for i in observations[j]), + 'every observation support exits at chart 1') + for field, _owner, _value in y_terms(abi, 632 + j): + need(len(frames[final[field]]) == 8, 'each affected Y chart has width 8') + need(span(frames[final[field]]) < span(frames[1]), 'each Y chart is strictly inside chart 1') + need(len(frames[1]) - len(frames[final[field]]) == 1, 'Y hop into chart 1 has width 1') + word = header + source + footer + dual_prefix = normal.dual_header(header) + dual_source + normal.dual_header(footer) + original, old_paid = evaluate(word, starts, final, frames) + need(original == target(abi, observations, set()), 'full normalized source ABI') + need(old_paid == Counter(engine.PAID), 'source recursive profile') + groups = [(j,) for j in range(8)] + list(itertools.combinations(range(8), 2)) + [tuple(range(8))] + need(len(groups) == 37, 'eight singletons, twenty-eight pairs and the octet') + screens = [] + for group in groups: + selected = set(group) + shared, y_fields, obs_fields = shared_tail(selected, observations, abi, final, frames) + stripped = strip_tail(selected, observations, abi, final, frames) + wanted = target(abi, observations, selected) + shared_rows, shared_paid = evaluate(word + shared, starts, final, frames) + strip_rows, strip_paid = evaluate(word + stripped, starts, final, frames) + need(shared_rows == wanted == strip_rows, 'shared visit and strip policy share the endpoint') + dual_rows, dual_paid = evaluate(dual_prefix + raw_dual(shared), starts, final, frames) + need(dual_rows == transpose(inverse(wanted)) and dual_paid == shared_paid, + 'raw inverse transpose of the shared visit') + delta = shared_paid - old_paid + strip_delta = strip_paid - old_paid + need(delta == Counter({1: 2 * len(y_fields), 9: 2 * len(selected)}), + 'shared visit pays two width-9 centre moves and two width-1 Y hops') + upper, free_round_trip = moment_upper(len(selected), len(y_fields)) + screens.append({ + 'selected': list(group), + 'observation_supports': len(set(obs_fields)), + 'distinct_Y': len(y_fields), + 'shared_added_requests': paid_dict(delta), + 'strip_added_requests': paid_dict(strip_delta), + 'moment_expression': 's*8^t - 2*n_Y - 2*s*9^t', + 'uniform_upper_bound': upper, + 'upper_bound_if_width9_free': free_round_trip, + 'scalar_adds': sum(1 for e in shared if e[0] == 'add'), + }) + chosen = screens[0] + need(chosen['selected'] == [0], 'first screen is centre 0') + need(chosen['distinct_Y'] == 56 and chosen['shared_added_requests'] == {'1': 112, '9': 2}, + 'centre 0 replaces the strip bill by one width-9 round trip and 112 width-1 hops') + need(chosen['strip_added_requests'] == {'8': 112, '9': 114}, 'strip policy bill for centre 0') + need(chosen['uniform_upper_bound'] == -113 and chosen['upper_bound_if_width9_free'] == -104, + 'centre-0 moment upper bound') + pair_bounds = {row['uniform_upper_bound'] for row in screens if len(row['selected']) == 2} + octet = screens[-1] + need(octet['selected'] == list(range(8)) and octet['distinct_Y'] == 112 + and octet['shared_added_requests'] == {'1': 224, '9': 16} + and octet['uniform_upper_bound'] == -232 + and octet['upper_bound_if_width9_free'] == -160, 'octet shared visit') + # The predecessor's pair census had 88 distinct Y fields. Keep that fact + # visible; every pair in this schedule uses that same count. + need({row['distinct_Y'] for row in screens if len(row['selected']) == 2} == {88}, + 'every pair meets 88 distinct Y fields') + need(pair_bounds == {-178}, 'every pair upper bound is -178') + need({row['upper_bound_if_width9_free'] for row in screens if len(row['selected']) == 2} == {-160}, + 'every pair still loses if the width-9 round trips are free') + + tail, y_fields, _obs = shared_tail({0}, observations, abi, final, frames) + wanted = target(abi, observations, {0}) + dropped = False + missing = [] + for event in tail: + if not dropped and event[0] == 'add' and event[1] == 632 and event[2] < 224: + dropped = True + continue + missing.append(event) + need(dropped and evaluate(word + missing, starts, final, frames)[0] != wanted, + 'omitted X observation rejected') + missing_y = [e for e in tail if not (e[0] == 'add' and e[1] == y_fields[0])] + need(evaluate(word + missing_y, starts, final, frames)[0] != wanted, + 'omitted centre-to-Y correction rejected') + need(rejected(lambda: evaluate(word + [('add', 632, 0, Q(-1), 0)], starts, final, frames)), + 'ADD at the empty chart while X remains on chart 1 rejected') + need(rejected(lambda: evaluate(word + [('transport', 632, 0, 1, 8)], starts, final, frames)), + 'undercharged chart-1 width rejected') + y_chart = final[y_fields[0]] + # The centre is still on the empty chart here, so a hop that claims to + # start on chart 1 is rejected. The legal width-1 Y hop is inside the word. + need(rejected(lambda: evaluate( + word + [('transport', 632, 1, y_chart, 1)], starts, final, frames)), + 'centre cannot leave chart 1 before it arrives there') + short = [] + replaced = False + for event in tail: + if not replaced and event[0] == 'transport' and event[1] == y_fields[0] and event[2] != 0: + short.append((event[0], event[1], event[2], event[3], event[4] + 1)) + replaced = True + else: + short.append(event) + need(replaced and rejected(lambda: evaluate(word + short, starts, final, frames)), + 'overcharged Y hop rejected') + controls = [ + 'missing data observation', + 'missing centre-to-Y correction', + 'empty-chart ADD against a chart-1 support', + 'undercharged centre transport', + 'centre hop before arrival', + 'overcharged Y hop', + ] + return { + 'status': 'PASS_SHARED_CHART_CENTRE_VISIT_STILL_LOSES', + 'new_kappa': None, + 'base_commit': pins['base_commit'], + 'model': 'retained nested-chart ADD/transport evaluator; no fresh Clifford replay', + 'source_paid': paid_dict(old_paid), + 'joint_normalization_gates': 758, + 'groups_checked': len(screens), + 'centre0': chosen, + 'pair_distinct_Y': 88, + 'pair_uniform_upper_bound': -178, + 'octet': octet, + 'screens': screens, + 'controls': controls, + 'compiler_route': 'unchanged; no outer admission', + } + + +def main(): + import argparse + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--out', type=Path) + args = parser.parse_args() + value = json.loads(json.dumps(run())) + if args.out: + need(not args.out.exists(), 'fresh output file required') + args.out.write_text(json.dumps(value, indent=2, sort_keys=True) + '\n', encoding='utf-8') + else: + expected = json.loads((HERE / 'RESULT.json').read_text(encoding='utf-8')) + canonical = lambda item: json.dumps(item, sort_keys=True, separators=(',', ':'), ensure_ascii=False) + need(canonical(value) == canonical(expected), 'exact scientific receipt') + print('PASS_SHARED_CHART_CENTRE_VISIT_STILL_LOSES no_new_kappa') + + +if __name__ == '__main__': + main()