diff --git a/research/zqy-observation-not-retained/PROOF.md b/research/zqy-observation-not-retained/PROOF.md new file mode 100644 index 0000000000..87145494a7 --- /dev/null +++ b/research/zqy-observation-not-retained/PROOF.md @@ -0,0 +1,62 @@ +# Proof sketch: b = Z Q Y is not in the retained span + +Notation as in `research/coupled-query-transport/PROOF.md` (#5415): +`X = Dx − Ry + RWh`, `Y = Dy`, `R = DQ`, `b = Z Q Y = Z R y`. + +## Native level + +In the row model of `research/kappa-owned-relation-20261023/native.py` a field +value is a pair (row, frame). The row is a finite rational combination of +(input role, warp word); a paid climb or centre changes only the frame; free +operations are same-frame ADD and SCALE with dyadic coefficients, owned COPY and +CLEAR, and warps. Two fields can be combined for free only in the same frame. + +`Y_k` ends in an 8-dimensional frame with row `y_k`, and the rank-one query +moves it to the unique full frame. So `Q Y_k` is the value (row `y_k`, full +frame), and `R y_k` is the `y` part of the endpoint `X_k = (x_k − y_k, full)`. +A free producer of `b` must output combinations of `Q Y_k` from values that +existed in the full frame at some time; owned copies make every time available, +so the available rows are exactly the span `V` of all full-frame versions. +`verify.py` computes `V` and shows `V ∩ span{y_k with any warp word} = 0`. +Hence no combination of the `Q Y_k`, in particular no coordinate of `b`, is +available without a new paid frame change. + +## Caller level + +Rows are noncommutative words over `Q, D_s, W_s, Z_s` with `Q D_s = D_s Q` +(#5415 `word_normal`). Free operations: scalar ADD of versions, left factors +`Q^{±2}` (Q_POWER), `W_t`, signed swaps, and `Z_s` applied to a whole bank. No +version word begins with `Z`; a left factor that does not begin with `Z_s` +produces words that do not begin with `Z_s`, and every word of `b = Z_s Q Y` +begins with `Z_s`. Removing the leading `Z_s` is injective, so `b` is a free +combination iff `Q Y` lies in the span of the free images of the versions. +`verify.py` shows it does not, at each of the 18 backward FULL returns, and also +with every version of the whole caller history. + +## Arithmetic + +All coefficients are dyadic, and `verify.py` computes every span as an exact +reduced echelon form over Q (Python `Fraction`). A target outside that span has +no expression `target = Σ c_i v_i` with any rational `c_i`, and the reported +ranks and intersection dimensions are Q-dimensions. (Reduction modulo a prime +would not suffice: for `A = [p]`, `b = 1` the target is outside the modular +image but equals `(1/p)·p`. The first version of this package used arithmetic +modulo `2^61 − 1`; the exact recomputation gives identical numbers.) + +## Part 2: response reuse + +Native: with the same rows and frames, a paid climb of f (A → B) producing row r +can be removed iff (r, B) can be built for free before f is next read or written. +Free values in B are the span of the versions that stood in B, kept by owned +copies. f itself can always be emptied by COPY C←f, f −= C, CLEAR C, followed by a +zero-retag A → B. The test of r against that span is therefore exactly the +removal criterion in this grammar (EARLY: versions before the climb; LATE: +versions before the next touch of f). To exclude f's own new value from the LATE +span, it enters as r + e_tag with a fresh coordinate. Then e_tag is in the span +iff r is a combination of the other versions. Within LATE, other climbs' results +also carry their own tags. A reuse of another climb's raw result is then seen by +the EARLY test of whichever of the two climbs comes later. + +Caller: a paid caller output can be removed iff it is a free image of earlier +versions. Free left factors are `Q^{±2}`, `W_t` and `Z_t`; combinations use +scalar ADD. diff --git a/research/zqy-observation-not-retained/README.md b/research/zqy-observation-not-retained/README.md new file mode 100644 index 0000000000..bbfd8dc77e --- /dev/null +++ b/research/zqy-observation-not-retained/README.md @@ -0,0 +1,126 @@ +# The coupled-exit observation b = Z Q Y is not retained, and no paid response is reusable + +**Negative result, no new κ, no change to the selected record.** +Zxv's #5415 shows that Dillon's #5402 coupled provider can return its eight +modes for **8 H1 + 456 ADD + 240 monomial maps** per backward FULL if the +current-version observation `b = Z Q Y` is supplied, and that buying the +observation (120 H1 per FULL) fails the moment screen. With `b` supplied the +#5415 screen is positive at saving .004 (rank surplus 1,776). #5415 (open +question 1), #5419 (ranked experiment 1) and #5425 (open question 1) all ask +whether `b` can be taken from observations that already exist. This package +answers that question **negatively** in the formal free-word grammar used by +the #5377 and #5397 row engines, both inside the native call and at the caller. + +## Part 1: b = Z Q Y (`verify.py`, standard library; whole script about 90 s) + +**Native level.** Exact rows over (input role, warp word), with the convention +of #5377's `native.py`; paid climbs change only the frame. `Q Y_k` is the row of +the input `y_k = L_{112+k}` standing in the full 9-dimensional frame (`Y` ends in an +8-dimensional frame, `X` ends in the full frame with row `x − y`). Any full-frame +version at any time can be kept in owned storage, so the available set is the +span `V` of all full-frame versions of the whole word. + +| word | full-frame versions | rank V | dim(V ∩ pure y) | pure y, any warp word | x-free part | +|---|---:|---:|---:|---:|---:| +| #5402 provider, backward | 4,891 | 546 | **0** | **0** | 400 (helpers) | +| #4610, backward | 5,019 | 554 | **0** | **0** | 408 (helpers) | +| #4610, forward | 4,968 | 554 | **0** | **0** | 376 | + +In the full frame `y` never appears without `x`; the only `x`-free content is +helper content. + +**Caller level.** The #5415 event semantics over the whole selected p16 caller +(162 events, 18 backward FULLs): `Q` and `D_s` commute, `Q_POWER` and +`SIGNED_SWAP` are free, query responses `Q⁻¹X` and helper returns are kept as +versions. No version word begins with a `Z` letter, so `b = Z_s Q Y` is available +iff `Q Y` lies in the span of all versions after free left factors `Q^{±2}`, +`W_t`. Result: **0 of 18** backward FULL returns, and **0 of 18** when the whole +caller history may be used (a delayed exit). Registered replay uses factors of +length ≤ 1 (21 factors); `--left-depth 2` (419 factors, about 5 minutes, exact over Q) gives +the same 0/0 and is recorded in `RESULT.json`. + +**Controls.** Every final full-frame endpoint row lies in `V`; one injected +pure-y version is detected (intersection 1); at every caller return the current +`Y` is found, and at the end `Q² Y` is found. So both tests can answer yes. + +**Arithmetic.** All coefficients are dyadic, and every span is an exact echelon +form over the rationals. All ranks, intersection dimensions and non-memberships +in this package (both parts) are therefore statements over Q: no combination of +the versions with arbitrary rational coefficients gives the target. An earlier +version computed modulo 2^61 − 1, which proves the obstruction only for +dyadic or p-integral coefficients; Clear1nsight's review pointed this out. The +exact recomputation gives the same numbers in every row. + +## Part 2: no paid response can be reused + +#5423 names the next economic object as a global occurrence ledger, in which each +response reuse must have the same chronological input, chart and lifetime. +Part 2 asks the plain version of that question on the same frozen words: can +any paid job be replaced by a combination of responses that already exist? + +**Native level.** For every paid climb or centre (frame A → B, row r), the script +tests two windows. EARLY asks whether r lies in the span of every version that +stood in frame B before the climb; owned copies keep all of them. LATE asks +whether r lies in the span of the other frame-B versions that exist before the +next event touching the field, which may be filled late. In LATE the own result +is stored as r + e_tag, so e_tag is in the span iff r is a combination of the +others. If EARLY held, the climb could be replaced by COPY/sub/CLEAR, a +zero-retag and same-frame ADDs, with no Gaussian call. + +| word | paid events | EARLY reuse | LATE reuse | +|---|---:|---:|---:| +| #5402 provider, backward | 3,282 | **0** | **0** | +| #4610, backward | 3,298 | **0** | **0** | +| #4610, forward | 3,298 | **0** | **0** | + +**Caller level.** The script tests 63 paid caller outputs: 15 thin QUERY +responses, 30 IDLE bank outputs and 18 LOCAL Y outputs. Each is tested against +the span of all earlier versions after free left factors `Q^{±2}`, `W_t` and +`Z_t`. Result: **0 reusable**. + +**Controls.** A copy of the first rank-one result injected just before its +climb is found as EARLY. Injected just after it, the same copy is found as LATE +only, and it is the only hit. A thin query repeated on its unchanged bank is +found at the caller level. + +This is wider than the single proportional-snapshot traversal of #5397. That +traversal found only the eight known relation sites, which the #5402 provider +word already uses. A κ step from response reuse therefore needs a changed word, +or new relations among inputs of the #5383 type. + +## Reproduce + +```sh +python3 -I -W error -B research/zqy-observation-not-retained/verify.py +python3 -B scripts/research_package.py --package research/zqy-observation-not-retained +# optional, about 2 minutes: caller test with free factors of length <= 2 +python3 -I -B research/zqy-observation-not-retained/verify.py --left-depth 2 +``` + +Expected marker: `PASS_ZQY_OBSERVATION_NOT_RETAINED`. + +## Scope + +The claim is about the frozen words in the formal free-word grammar (same +scope as #5377/#5397): rows over input roles and native warp words, with only +the Q–D commutation of #5415 at the caller. Not covered: physical identities +beyond that grammar (relations between native warps and Gaussian children, or +between Q and the K_p/K_m monomials), changed native words, other providers, and +the precision, tape and storage obligations that any exit would also carry. +In part 2 the LATE window does not use another climb's raw result as a source; the symmetric case is covered by the EARLY test of the later climb. The result shows that the supplied-observation branch of #5415 section 4 has no +free producer here; it does not bound the price of a new paid producer. + +## Open next questions + +See `TASK.json`: a numerical full-phase repeat at fiber width one (the only +escape inside the frozen words), and the price of a changed native word that +keeps a pure copy of `R y` before mixing it with `D x`. + +## Credit + +Dillon (dillona, #5402) supplies the coupled provider word; Cao Yifan (intqwq, +#4610) the native word and frames; zxv (#5415) the exit contract, the caller +semantics and the selected successor controller; Ali Romman (#5377) the row +convention; Clear1nsight (#5425) and zxv (#5419) the open questions. +Mark (Matarener) with substantial Claude Code (Claude) assistance. Apache-2.0; +author-checked, not independent acceptance. diff --git a/research/zqy-observation-not-retained/RESULT.json b/research/zqy-observation-not-retained/RESULT.json new file mode 100644 index 0000000000..9466b07861 --- /dev/null +++ b/research/zqy-observation-not-retained/RESULT.json @@ -0,0 +1,217 @@ +{ + "arithmetic": "exact rational arithmetic: dyadic rows, spans as exact echelon forms over Q; ranks, intersections and non-membership are over Q", + "caller": { + "available_at_return": 0, + "available_with_whole_history": 0, + "backward_FULL_returns": 18, + "closure_rank": 2827, + "events": 162, + "free_left_factors": 21, + "left_depth": 1, + "per_call": [ + { + "b_available_at_return": false, + "event": 2, + "pair": 0, + "stage": 0 + }, + { + "b_available_at_return": false, + "event": 5, + "pair": 0, + "stage": 1 + }, + { + "b_available_at_return": false, + "event": 12, + "pair": 1, + "stage": 3 + }, + { + "b_available_at_return": false, + "event": 19, + "pair": 2, + "stage": 5 + }, + { + "b_available_at_return": false, + "event": 26, + "pair": 3, + "stage": 7 + }, + { + "b_available_at_return": false, + "event": 33, + "pair": 4, + "stage": 9 + }, + { + "b_available_at_return": false, + "event": 40, + "pair": 5, + "stage": 11 + }, + { + "b_available_at_return": false, + "event": 47, + "pair": 6, + "stage": 13 + }, + { + "b_available_at_return": false, + "event": 54, + "pair": 7, + "stage": 15 + }, + { + "b_available_at_return": false, + "event": 60, + "pair": 8, + "stage": 17 + }, + { + "b_available_at_return": false, + "event": 66, + "pair": 9, + "stage": 19 + }, + { + "b_available_at_return": false, + "event": 72, + "pair": 10, + "stage": 21 + }, + { + "b_available_at_return": false, + "event": 78, + "pair": 11, + "stage": 23 + }, + { + "b_available_at_return": false, + "event": 84, + "pair": 12, + "stage": 25 + }, + { + "b_available_at_return": false, + "event": 90, + "pair": 13, + "stage": 27 + }, + { + "b_available_at_return": false, + "event": 96, + "pair": 14, + "stage": 29 + }, + { + "b_available_at_return": false, + "event": 102, + "pair": 15, + "stage": 31 + }, + { + "b_available_at_return": false, + "event": 105, + "pair": 15, + "stage": 32 + } + ], + "versions": 240 + }, + "caller_depth2_evidence": { + "available_at_return": 0, + "available_with_whole_history": 0, + "closure_rank_at_end": 56405, + "note": "same test with free left factors of length <= 2 (419 factors), run with --left-depth 2 (about 5 minutes, exact over Q); not part of the registered replay" + }, + "native": { + "pr4610_backward": { + "control_injected_pure_y_detected": 1, + "coordinates": 1168, + "dim_V_cap_pure_y": 0, + "dim_V_cap_y_any_warp_word": 0, + "dim_x_free_part": 408, + "full_frame_versions": 5019, + "rank_V": 554, + "versions_with_y_content": 1863 + }, + "pr4610_forward": { + "control_injected_pure_y_detected": 1, + "coordinates": 856, + "dim_V_cap_pure_y": 0, + "dim_V_cap_y_any_warp_word": 0, + "dim_x_free_part": 376, + "full_frame_versions": 4968, + "rank_V": 554, + "versions_with_y_content": 0 + }, + "pr5402_provider_backward": { + "control_injected_pure_y_detected": 1, + "coordinates": 1168, + "dim_V_cap_pure_y": 0, + "dim_V_cap_y_any_warp_word": 0, + "dim_x_free_part": 400, + "full_frame_versions": 4891, + "rank_V": 546, + "versions_with_y_content": 1851 + } + }, + "reuse": { + "caller": { + "control_repeated_query_found_at_event": 10, + "paid_outputs_tested": { + "IDLE": 30, + "LOCAL_Y": 18, + "QUERY": 15 + }, + "reusable": 0 + }, + "native": { + "pr4610_backward": { + "early_reuse": 0, + "late_reuse": 0, + "paid_by_rank": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "paid_events": 3298 + }, + "pr4610_forward": { + "early_reuse": 0, + "late_reuse": 0, + "paid_by_rank": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "paid_events": 3298 + }, + "pr5402_provider_backward": { + "controls": { + "injected_after_climb_found_late_only": 6276, + "injected_before_climb_found_early": 6276 + }, + "early_reuse": 0, + "late_reuse": 0, + "paid_by_rank": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40 + }, + "paid_events": 3282 + } + } + }, + "schema": "zqy-observation-not-retained/2" +} diff --git a/research/zqy-observation-not-retained/SOURCES.json b/research/zqy-observation-not-retained/SOURCES.json new file mode 100644 index 0000000000..9830401130 --- /dev/null +++ b/research/zqy-observation-not-retained/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "1a3ced60b2f7a46bc70280a04f2eeb8ca027c700", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/native-rank8-helper-provider/WORD.json.gz", + "usage": "input", + "git_blob": "f3111b47e89496da8ca0ee45b2e4b258c0634d8e", + "sha256": "7dc356001ed597ad6fc9fd3e0bc6ff7e3ec3a580a579a956827aa17fccfdd2dc" + }, + { + "path": "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "usage": "input", + "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e", + "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" + }, + { + "path": "research/coupled-query-transport/inputs/SUCCESSOR-CONTROLLER.json", + "usage": "input", + "git_blob": "01775a36ae1238350bf8cd859b04cb8c4589873b", + "sha256": "60cc512b39cdb9ea2c2ac6c6634c8d3f9627d96ace08ffa659a9d9472444122b" + }, + { + "path": "research/coupled-query-transport/PROOF.md", + "usage": "provenance", + "git_blob": "d25beb53d0ce348699d06ab2592eefe9b9535c2d", + "sha256": "7800d634593e4f8cc71739c89ee3b7f52ddcd43a10a6b275d684006d4e5850d7" + }, + { + "path": "research/kappa-owned-relation-20261023/native.py", + "usage": "provenance", + "git_blob": "b8249ed7ba981a798ba282a6aeabd81a600bda36", + "sha256": "85d994fc5661bfa53c4b42f79955ff74ffe70072163cb02fa76cd79efbcc0c97" + } + ] +} diff --git a/research/zqy-observation-not-retained/TASK.json b/research/zqy-observation-not-retained/TASK.json new file mode 100644 index 0000000000..34b890107e --- /dev/null +++ b/research/zqy-observation-not-retained/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 7, + "base_commit": "1a3ced60b2f7a46bc70280a04f2eeb8ca027c700", + "original_card": { + "id": "joint-query-controller", + "question": "Can the installed QQ16 caller win a complete matched protocol bill, or can a changed demand eliminate actual paid work?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/qq16-caller-install/README.md" + ], + "methods": [ + "Derive the matched whole-caller physical bill for installed and baseline protocols.", + "Change the actual demanded observations and prove a cheaper legal producer/consumer contract." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. 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", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #4166 COST.md and ADMISSION.json. An actual caller connection is now proposed. Its native-component profile loses; parent park/restore versus external-call costs remain unresolved. Retain the producer and recovery lineage rather than rebuild it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "At the actual installed cut, compare matched complete parent park/restore and external input/return protocols at the same bank/packet geometry, including every later root call and service cost. Alternatively pin both bridge observations and derive a genuinely smaller source-compatible demand. Stop if the complete necessary inequality fails or an essential cost is unknown; no larger decoder scan from a local tape-action saving.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair.", + "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations.", + "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise.", + "Treating a completed-output defect inequality as a producer-interior, dirty-range or physical-cost certificate.", + "Recreating completed-output recovery or caller wiring already supplied by #4166 without new independent coverage.", + "Dropping retained later root calls or claiming native-profile dominance from the isolated publication saving." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969", + "2540", + "early record", + "output-bank retention", + "complete native decoder", + "2965", + "producer defect", + "dirty-helper range", + "F17 consumer", + "4166", + "qq16-caller-install" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Is the current-version observation b = Z Q Y, which makes the #5415 coupled-provider exit cost 8 H1 instead of 120 H1 per backward FULL, already present in any retained native or caller observation of the selected p16 caller (PR5402 provider word, #4610 word, #5415 successor controller)? Part 2: can any paid native climb or paid caller output be replaced by reusing earlier responses (the global occurrence ledger of #5423)?", + "scope_change_reason": "The card asks for a changed demand or a recovered query with legal reads. #5415 (open question 1), #5419 (ranked experiment 1) and #5425 (open question 1) name the concrete instance: supply Z Q Y from already paid observations. This package answers that instance negatively in the formal free-word grammar.", + "bottleneck_link": "Negative result: the supplied-observation branch of #5415 section 4 (rank surplus 1776, positive .004 screen) has no free producer; every route to the coupled exit must pay new Gaussian work for b, and the purchased route already fails. Part 2: no paid job of the frozen words is a free combination of earlier responses, so response reuse gives no recursive saving without a changed word or input relations.", + "budget_minutes": 120, + "stop_rule": "Stop at the exact span certificates (native: three words; caller: 18 backward FULLs at return and with whole history) and the part 2 reuse census with its controls; do not start a new native word or a decoder search.", + "outcome": "negative-result", + "evidence": "verify.py binds the three inputs by SHA256, replays exact rows, and certifies dim(V cap pure y)=0 for the full-frame span of every native word and Q Y outside the free-factor span at every caller return; controls (endpoints, injected pure y, Y, Q^2 Y) show the tests can answer yes; RESULT.json records the depth-2 caller run. Part 2: reuse census, EARLY and LATE windows, 0 of 3,282/3,298/3,298 native paid events and 0 of 63 caller paid outputs, with injected-copy and repeated-query controls.", + "author": "Mark (Matarener)", + "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.", + "open_questions": [ + { + "question": "Does a physical identity outside the free-word grammar (a relation between native warps and Gaussian children, or between Q and the K_p/K_m monomials) put pure y in the full frame?", + "why_it_matters": "It is the only escape left inside the frozen words; a positive answer would fund the 8-H1 exit.", + "first_step": "Evaluate the full-frame versions at fiber width one with the absolute-phase monomial evaluator of research/coupled-query-transport/verify.py and repeat the span test numerically over complex coordinates.", + "blocked_by": "Needs the full physical phase evaluator of the native word, not only the formal rows." + }, + { + "question": "Can a changed native word keep a pure copy of R y in the full frame before mixing it with D x, and what does that copy cost?", + "why_it_matters": "With b supplied the #5415 screen is positive at .004; the question becomes the price of one retained separation.", + "first_step": "Locate in the provider word the ADD events that first mix y content into x fields in the full frame (verify.py lists them through the versions with y content) and price a split of the last climb.", + "blocked_by": "A changed word must be re-admitted (native maps, phases, 632 endpoints)." + } + ] +} diff --git a/research/zqy-observation-not-retained/VERIFY.json b/research/zqy-observation-not-retained/VERIFY.json new file mode 100644 index 0000000000..94db12f56e --- /dev/null +++ b/research/zqy-observation-not-retained/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/native-rank8-helper-provider/WORD.json.gz", + "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "research/coupled-query-transport/inputs/SUCCESSOR-CONTROLLER.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Bind the three inputs by SHA256; exact native row replay of the PR5402 provider backward word and the #4610 word in both orientations; span of all full-frame versions has zero intersection with pure y (any warp word), x-free part equals helper content; endpoint and injected-pure-y controls; caller replay of the #5415 p16 controller, b = Z Q Y unavailable at all 18 backward FULL returns and with the whole history, with the Y and Q^2 Y controls; part 2 reuse census: no paid native climb (EARLY/LATE windows) or paid caller output (QUERY, IDLE, LOCAL Y) is a free combination of earlier responses, with injected-copy and repeated-query controls; RESULT.json byte comparison." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Same checks with assertions optimised away; every check uses explicit raises." + } + ] +} diff --git a/research/zqy-observation-not-retained/verify.py b/research/zqy-observation-not-retained/verify.py new file mode 100644 index 0000000000..714261b7b9 --- /dev/null +++ b/research/zqy-observation-not-retained/verify.py @@ -0,0 +1,592 @@ +#!/usr/bin/env python3 +"""The coupled-exit observation b = Z Q Y is not present in any retained version (negative result, no new kappa). + +Mark (Matarener), with substantial Claude Code (Claude) assistance. Apache-2.0. + +#5415 (zxv) shows that the PR5402 coupled provider can return its eight modes with +8 H1 + 456 ADD + 240 maps if the current-version observation b = Z Q Y is supplied, +and that buying it (120 H1 per backward FULL) fails the moment screen. Its open +question 1, #5419 experiment 1 and #5425 open question 1 ask whether b can be taken +from observations that already exist. This script answers that question in the +formal free-word grammar used by the #5377 / #5397 row engines, at two levels: + + N native level: replay the PR5402 provider backward word and the #4610 word in both + orientations with exact rows over (input role, warp word); paid climbs change only + the frame. Q Y_k is the row of the input y_k = L_{112+k} standing in the full + (9-dimensional) frame. Every full-frame version at every time may be kept in owned + storage, so the available set is the span V of all of them. Certify + dim(V ∩ span{y_k}) = 0, also for y_k with any warp word, and that the x-free part + of V is exactly the helper content. + C caller level: replay the selected p16 caller of #5415 (162 events, 18 backward + FULLs) with the #5415 event semantics (Q and D_s commute, Q_POWER and SIGNED_SWAP + free). No version word begins with a Z letter, so b = Z_s Q Y is available iff + Q Y lies in the span of all versions after free left factors Q^{+-2}, W_t + (products of length <= LEFT_DEPTH). Certify 0 of 18 at the return and 0 of 18 with + the whole caller history (a delayed exit). + +Arithmetic is exact over the rationals (Fraction echelon forms): every rank, intersection +dimension and (non-)membership below is a statement over Q, so no reconstruction with +arbitrary rational coefficients exists. (An earlier version reduced modulo 2^61-1, which +only proves the obstruction for p-integral coefficients; review of #5427.) Controls show +that both tests can say yes. + +Part 2 (response reuse, the "global occurrence ledger" of #5423): no paid job can be +replaced by an earlier response. + R1 native: for every paid climb/centre (frame A -> B, row r), r is not in the span of the + versions that stood in B before it (EARLY), nor of the other B versions that exist before + the next event touching the field (LATE; own result tagged). Injected-copy controls. + R2 caller: no thin QUERY response, IDLE bank output or LOCAL Y output lies in the span of + the earlier versions after free left factors Q^{+-2}, W_t, Z_t. Repeated-query control. + +Usage: python3 -I -W error -B verify.py [--write] [--left-depth 2] +Exit 0 and marker PASS_ZQY_OBSERVATION_NOT_RETAINED iff every check passes and RESULT.json matches. +""" +import gzip +import hashlib +import json +import os +import sys +from fractions import Fraction as Fr + +HERE = os.path.dirname(os.path.abspath(__file__)) +ROOT = os.path.dirname(os.path.dirname(HERE)) +INPUTS = { + 'provider': ('research/native-rank8-helper-provider/WORD.json.gz', + '7dc356001ed597ad6fc9fd3e0bc6ff7e3ec3a580a579a956827aa17fccfdd2dc'), + 'word4610': ('research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz', + '7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05'), + 'caller': ('research/coupled-query-transport/inputs/SUCCESSOR-CONTROLLER.json', + '60cc512b39cdb9ea2c2ac6c6634c8d3f9627d96ace08ffa659a9d9472444122b'), +} + + +def need(ok, why): + if not ok: + raise AssertionError(why) + + +def read_input(name): + rel, sha = INPUTS[name] + with open(os.path.join(ROOT, *rel.split('/')), 'rb') as fh: + raw = fh.read() + need(hashlib.sha256(raw).hexdigest() == sha, 'input bytes changed: ' + rel) + return json.loads(gzip.decompress(raw) if rel.endswith('.gz') else raw) + + +# ---------------------------------------------------------------- exact span over Q +class Span: + """Sparse reduced echelon basis over Q (exact Fractions).""" + + def __init__(self): + self.piv = {} + + def reduce(self, v): + v = dict(v) + while True: + hit = next((c for c in v if c in self.piv), None) + if hit is None: + return v + f = v[hit] + for c, x in self.piv[hit].items(): + nv = v.get(c, 0) - f * x + if nv: + v[c] = nv + else: + v.pop(c, None) + + def add(self, v): + v = self.reduce(v) + if not v: + return False + c = min(v) + inv = 1 / Fr(v[c]) + v = {k: x * inv for k, x in v.items()} + for b in self.piv.values(): + if c in b: + f = b[c] + for k, x in v.items(): + nv = b.get(k, 0) - f * x + if nv: + b[k] = nv + else: + b.pop(k, None) + self.piv[c] = v + return True + + def copy(self): + s = Span() + s.piv = {c: dict(b) for c, b in self.piv.items()} + return s + + +def modrow(row, index): + """Exact rational coordinates of a row (dyadic coefficients checked).""" + out = {} + for key, q in row.items(): + c = index.setdefault(key, len(index)) + need(q.denominator & (q.denominator - 1) == 0, 'dyadic coefficient') + out[c] = Fr(q) + return out + + +# ---------------------------------------------------------------- native level +def span_set(basis): + out = {0} + for v in basis: + out |= {x ^ v for x in tuple(out)} + need(len(out) == 1 << len(basis), 'independent frame basis') + return out + + +def native_replay(canon, program, backward): + """Exact rows (convention of research/kappa-owned-relation-20261023/native.py). + Returns the list of distinct full-frame versions, final rows and final frames.""" + spaces = [span_set(b) for b in canon['frames']] + full = {i for i, s in enumerate(spaces) if len(s) == 512} + need(len(full) == 1, 'one full frame') + rows = {('L', i): {(('L', i), ()): Fr(1)} for i in range(632)} + frames = {('L', i): canon['start'][i] for i in range(632)} + + def get(r): + if r not in rows: + rows[r] = {(r, ()): Fr(1)} + frames[r] = None + return rows[r] + + seen, versions = set(), [] + for e in program: + k, touched = e[0], None + if k == 'scalar': + g, frame = e[1], e[2] + dst = tuple(g[1]); get(dst); touched = dst + if g[0] == 'clear': + rows[dst] = {}; frames[dst] = frame + elif g[0] == 'copy': + src = tuple(g[2]); need(frames[src] == frame, 'copy frame') + rows[dst] = dict(get(src)); frames[dst] = frame + elif g[0] == 'add': + src = tuple(g[2]); need(frames[src] == frame == frames[dst], 'same-frame ADD') + q = Fr(g[3], g[4]); r = rows[dst] + for key, v in get(src).items(): + nv = r.get(key, 0) + q * v + if nv: + r[key] = nv + else: + r.pop(key, None) + elif g[0] == 'scale': + q = Fr(g[2], g[3]); rows[dst] = {a: q * v for a, v in rows[dst].items()} + else: + raise AssertionError('unknown scalar ' + repr(g[0])) + elif k == 'warp': + _, role, op, old, new = e + dst = tuple(role); get(dst); touched = dst + need(frames[dst] == old, 'warp input frame') + sym = (1 if op > 0 else -1) * (abs(op) + (10 ** 6 if backward else 0)) + rows[dst] = {(r, w[1:] if w and w[0] == -sym else (sym,) + w): q for (r, w), q in rows[dst].items()} + frames[dst] = new + elif k == 'climb': + dst = ('L', e[2]); need(frames[dst] == e[3], 'climb input frame') + frames[dst] = e[4]; touched = dst + elif k == 'center': + dst = ('C', e[1]); get(dst); frames[dst] = e[3]; touched = dst + elif k == 'zero_retag': + dst = ('L', e[1]); need(frames[dst] == e[2] and not rows[dst], 'zero retag on a zero row') + frames[dst] = e[3]; touched = dst + else: + need(k in ('phase', 'adapter'), 'unknown event ' + repr(k)) + if touched is not None and frames[touched] in full and rows[touched]: + key = frozenset(rows[touched].items()) + if key not in seen: + seen.add(key); versions.append(dict(rows[touched])) + return versions, rows, frames, full + + +def role_class(key): + r = key[0] + if r[0] == 'L' and r[1] < 112: + return 'x' + if r[0] == 'L' and r[1] < 224: + return 'y' + return 'h' + + +def native_level(name, canon, program, backward): + versions, rows, frames, full = native_replay(canon, program, backward) + index = {(('L', 112 + k), ()): k for k in range(112)} + V = Span() + mods = [] + for v in versions: + m = modrow(v, index); mods.append(m); V.add(m) + # every final full-frame row is in V (the test sees the endpoints) + need(all(not V.reduce(modrow(rows[r], index)) for r in rows if frames[r] in full and rows[r]), name + ': endpoints in V') + # main test: pure y with the empty warp word + R = Span() + indep = sum(R.add(V.reduce({k: 1})) for k in range(112)) + inter = 112 - indep + # control: one injected pure-y version is detected + W = V.copy(); W.add({5: 1}) + R2 = Span() + control = 112 - sum(R2.add(W.reduce({k: 1})) for k in range(112)) + need(control == 1, name + ': injected pure-y control') + inv = {c: key for key, c in index.items()} + cls = {c: role_class(key) for c, key in inv.items()} + # x-free part and pure-y-any-word part via projections + px, pxh = Span(), Span() + for m in mods: + px.add({c: v for c, v in m.items() if cls[c] == 'x'}) + pxh.add({c: v for c, v in m.items() if cls[c] != 'y'}) + out = {'full_frame_versions': len(versions), 'rank_V': len(V.piv), 'coordinates': len(index), + 'dim_V_cap_pure_y': inter, 'dim_V_cap_y_any_warp_word': len(V.piv) - len(pxh.piv), + 'dim_x_free_part': len(V.piv) - len(px.piv), + 'versions_with_y_content': sum(any(cls[c] == 'y' for c in m) for m in mods), + 'control_injected_pure_y_detected': control} + need(inter == 0 and out['dim_V_cap_y_any_warp_word'] == 0, name + ': pure y is available') + return out + + +# ---------------------------------------------------------------- caller level +def normal(word): + """#5415 word_normal: Q and D_* commute; adjacent inverse letters cancel.""" + out, run = [], {} + + def flush(): + for lab in sorted(run): + e = run[lab] + out.extend([(lab, 1 if e > 0 else -1)] * abs(e)) + run.clear() + for lab, e in word: + if lab == 'Q' or lab.startswith('D'): + run[lab] = run.get(lab, 0) + e + if run[lab] == 0: + run.pop(lab) + else: + flush() + if out and out[-1] == (lab, -e): + out.pop() + else: + out.append((lab, e)) + flush() + return tuple(out) + + +def left(row, *ops): + out = {} + for (s, w), v in row.items(): + k = (s, normal(tuple(ops) + w)); out[k] = out.get(k, 0) + v + return {k: v for k, v in out.items() if v} + + +def plus(a, b, c=1): + out = dict(a) + for k, v in b.items(): + t = out.get(k, 0) + c * v + if t: + out[k] = t + else: + out.pop(k, None) + return out + + +def caller_level(ctl, depth): + ev = ctl['physical_events'] + nf = 2 * ctl['pairs'] + rows = [{(('in', j), ()): Fr(1)} for j in range(nf)] + versions = [dict(r) for r in rows] + stages = sorted({e[1] for e in ev if e[0] == 'LOCAL'}) + one = [(), (('Q', 1), ('Q', 1)), (('Q', -1), ('Q', -1))] + [(('W%d' % t, 1),) for t in stages] + frees = {()} + for _ in range(depth): + frees = {normal(a + b) for a in frees for b in one} + frees = sorted(frees) + index, V, done, targets, per_call = {}, Span(), 0, [], [] + + def absorb(): + nonlocal done + for v in versions[done:]: + need(not any(w and w[0][0].startswith('Z') for (_, w) in v), 'a version word begins with Z') + for f in frees: + V.add(modrow(left(v, *f) if f else v, index)) + done = len(versions) + + for i, e in enumerate(ev): + k = e[0] + if k == 'LOCAL': + s, p, bw = e[1], e[2], e[3] + need(bw, 'backward FULL') + x, y = 2 * p, 2 * p + 1 + D, h = ('D%d' % s, 1), {(('h', s), ()): Fr(1)} + yold = rows[y] + helper = plus(left(h, D), left(yold, D, ('Z%d' % s, 1)), -1) + rows[x] = plus(plus(left(rows[x], D), left(yold, D, ('Q', 1)), -1), left(h, D, ('Q', 1), ('W%d' % s, 1))) + rows[y] = left(yold, D) + versions += [dict(rows[x]), dict(rows[y]), helper] + absorb() + target = left(rows[y], ('Q', 1)) + targets.append(target) + ok = not V.reduce(modrow(target, index)) + ctrl = not V.reduce(modrow(rows[y], index)) + need(ctrl, 'control: current Y must be available') + per_call.append({'event': i, 'stage': s, 'pair': p, 'b_available_at_return': ok}) + elif k == 'IDLE': + for j in (2 * e[1], 2 * e[1] + 1): + rows[j] = left(rows[j], *[('D%d' % st, 1) for st in reversed(e[2])]) + versions.append(dict(rows[j])) + elif k == 'ADD': + rows[e[1]] = plus(rows[e[1]], rows[e[2]], e[3]); versions.append(dict(rows[e[1]])) + elif k == 'QUERY_SHEAR': + need(not e[3], 'lower thin shear') + resp = left(rows[2 * e[2]], ('Q', -1)) + versions.append(resp) + rows[2 * e[2] + 1] = plus(rows[2 * e[2] + 1], resp); versions.append(dict(rows[2 * e[2] + 1])) + elif k == 'SIGNED_SWAP': + a, b = e[1], e[2] + rows[a], rows[b] = rows[b], {kk: -v for kk, v in rows[a].items()} + elif k == 'Q_POWER': + rows[e[1]] = left(rows[e[1]], *([('Q', 1 if e[2] > 0 else -1)] * abs(e[2]))) + versions.append(dict(rows[e[1]])) + else: + raise AssertionError('unknown caller event ' + repr(k)) + absorb() + late = sum(not V.reduce(modrow(t, index)) for t in targets) + # control: a target that IS a free image of a version (Q^2 times the final Y bank) is found + need(not V.reduce(modrow(left(rows[1], ('Q', 1), ('Q', 1)), index)), 'control: Q^2 Y is available') + out = {'events': len(ev), 'backward_FULL_returns': len(per_call), + 'available_at_return': sum(c['b_available_at_return'] for c in per_call), + 'available_with_whole_history': late, 'free_left_factors': len(frees), 'left_depth': depth, + 'closure_rank': len(V.piv), 'versions': len(versions), 'per_call': per_call} + need(out['backward_FULL_returns'] == 18, '18 backward FULLs') + need(out['available_at_return'] == 0 and late == 0, 'b = Z Q Y available at some return') + return out + + +# ---------------------------------------------------------------- part 2: response reuse +def native_events(canon, program, backward): + """Per event: (index, kind, role, row after, frame before, frame after, rank, source role).""" + rows = {('L', i): {(('L', i), ()): Fr(1)} for i in range(632)} + frames = {('L', i): canon['start'][i] for i in range(632)} + + def get(r): + if r not in rows: + rows[r] = {(r, ()): Fr(1)} + frames[r] = None + return rows[r] + out = [] + for idx, e in enumerate(program): + k = e[0] + if k == 'scalar': + g, frame = e[1], e[2] + dst = tuple(g[1]); get(dst); old = frames[dst]; src = None + if g[0] == 'clear': + rows[dst] = {}; frames[dst] = frame + elif g[0] == 'copy': + src = tuple(g[2]); rows[dst] = dict(get(src)); frames[dst] = frame + elif g[0] == 'add': + src = tuple(g[2]); q = Fr(g[3], g[4]); r = rows[dst] + for key, v in get(src).items(): + nv = r.get(key, 0) + q * v + if nv: + r[key] = nv + else: + r.pop(key, None) + elif g[0] == 'scale': + q = Fr(g[2], g[3]); rows[dst] = {a: q * v for a, v in rows[dst].items()} + out.append((idx, 'scalar', dst, dict(rows[dst]), old, frames[dst], None, src)) + elif k == 'warp': + _, role, op, old, new = e + dst = tuple(role); get(dst) + sym = (1 if op > 0 else -1) * (abs(op) + (10 ** 6 if backward else 0)) + rows[dst] = {(r, w[1:] if w and w[0] == -sym else (sym,) + w): q for (r, w), q in rows[dst].items()} + frames[dst] = new + out.append((idx, 'warp', dst, dict(rows[dst]), old, new, None, None)) + elif k in ('climb', 'center'): + dst = ('L', e[2]) if k == 'climb' else ('C', e[1]); get(dst) + old, new, rank = (e[3], e[4], e[5]) if k == 'climb' else (e[2], e[3], e[4]) + frames[dst] = new + out.append((idx, k, dst, dict(rows[dst]), old, new, rank, None)) + elif k == 'zero_retag': + dst = ('L', e[1]); old = frames[dst]; frames[dst] = e[3] + out.append((idx, 'zero_retag', dst, dict(rows[dst]), old, e[3], None, None)) + return out + + +def reuse_census(ev, inject=None): + """EARLY: a paid result r (frame A->B) lies in the span of every version that stood in B + before the climb. LATE: r lies in the span of the other B versions that exist before the + next event touching the field; the own result is stored as r + e_tag, so e_tag is in the + span iff r is a combination of the others.""" + touches = {} + for j, x in enumerate(ev): + touches.setdefault(x[2], []).append(j) + if x[7] is not None: + touches.setdefault(x[7], []).append(j) + index, spans, tspans, pending = {}, {}, {}, [] + early, late, paid, by_rank = [], [], 0, {} + for j, (idx, kind, dst, row, a, b, rank, src) in enumerate(ev): + while pending and pending[0][0] <= j: + _, tag, fr, info = pending.pop(0) + if not tspans[fr].reduce({tag: 1}): + late.append(info) + tag = None + if kind in ('climb', 'center'): + paid += 1 + by_rank[str(rank)] = by_rank.get(str(rank), 0) + 1 + info = {'event': idx, 'role': list(dst), 'from': a, 'to': b, 'rank': rank} + m = modrow(row, index) if row else {} + if not row or not spans.setdefault(b, Span()).reduce(m): + early.append(info) + else: + nxt = [t for t in touches[dst] if t > j] + tag = (1 << 40) + j + pending.append((nxt[0] if nxt else len(ev), tag, b, info)) + pending.sort(key=lambda x: x[0]) + if inject is not None and idx == inject[0]: + v = modrow(inject[2], index) + spans.setdefault(inject[1], Span()).add(v) + tspans.setdefault(inject[1], Span()).add(v) + if row and b is not None: + v = modrow(row, index) + spans.setdefault(b, Span()).add(v) + tv = dict(v) + if tag is not None: + tv[tag] = 1 + tspans.setdefault(b, Span()).add(tv) + for _, tag, fr, info in pending: + if not tspans[fr].reduce({tag: 1}): + late.append(info) + return {'paid_events': paid, 'paid_by_rank': by_rank, 'early_reuse': early, 'late_reuse': late} + + +def native_reuse(name, canon, program, backward, control): + ev = native_events(canon, program, backward) + out = reuse_census(ev) + need(not out['early_reuse'] and not out['late_reuse'], name + ': a paid result is reusable') + if control: + j, first = next((j, x) for j, x in enumerate(ev) if x[1] == 'climb' and x[6] == 1 and x[3]) + before = reuse_census(ev, inject=(ev[j - 1][0], first[5], first[3])) + after = reuse_census(ev, inject=(first[0], first[5], first[3])) + need([x['event'] for x in before['early_reuse']] == [first[0]], name + ': EARLY control') + need([x['event'] for x in after['late_reuse']] == [first[0]] and not after['early_reuse'], name + ': LATE control') + out['controls'] = {'injected_before_climb_found_early': first[0], 'injected_after_climb_found_late_only': first[0]} + out['early_reuse'] = len(out['early_reuse']) + out['late_reuse'] = len(out['late_reuse']) + return out + + +def caller_reuse(ev, nf): + """Each paid caller output (QUERY response, IDLE bank output, LOCAL Y output) against the + span of all earlier versions after free left factors Q^{+-2}, W_t, Z_t (length <= 1).""" + rows = [{(('in', j), ()): Fr(1)} for j in range(nf)] + versions = [dict(r) for r in rows] + stages = sorted({e[1] for e in ev if e[0] == 'LOCAL'}) + frees = [(), (('Q', 1), ('Q', 1)), (('Q', -1), ('Q', -1))] + frees += [(('W%d' % t, 1),) for t in stages] + [(('Z%d' % t, 1),) for t in stages] + index, V, hits = {}, Span(), [] + tested = {'QUERY': 0, 'IDLE': 0, 'LOCAL_Y': 0} + done = [0] + + def test(i, kind, out): + for v in versions[done[0]:]: + for f in frees: + V.add(modrow(left(v, *f) if f else v, index)) + done[0] = len(versions) + tested[kind] += 1 + if not V.reduce(modrow(out, index)): + hits.append([i, kind]) + for i, e in enumerate(ev): + k = e[0] + if k == 'LOCAL': + s, p = e[1], e[2] + x, y = 2 * p, 2 * p + 1 + D, h = ('D%d' % s, 1), {(('h', s), ()): Fr(1)} + yold = rows[y] + newx = plus(plus(left(rows[x], D), left(yold, D, ('Q', 1)), -1), left(h, D, ('Q', 1), ('W%d' % s, 1))) + newy = left(yold, D) + test(i, 'LOCAL_Y', newy) + rows[x], rows[y] = newx, newy + versions += [dict(newx), dict(newy), plus(left(h, D), left(yold, D, ('Z%d' % s, 1)), -1)] + elif k == 'IDLE': + for j in (2 * e[1], 2 * e[1] + 1): + out = left(rows[j], *[('D%d' % st, 1) for st in reversed(e[2])]) + test(i, 'IDLE', out) + rows[j] = out + versions.append(dict(out)) + elif k == 'ADD': + rows[e[1]] = plus(rows[e[1]], rows[e[2]], e[3]) + versions.append(dict(rows[e[1]])) + elif k == 'QUERY_SHEAR': + resp = left(rows[2 * e[2]], ('Q', -1)) + test(i, 'QUERY', resp) + versions.append(resp) + rows[2 * e[2] + 1] = plus(rows[2 * e[2] + 1], resp) + versions.append(dict(rows[2 * e[2] + 1])) + elif k == 'SIGNED_SWAP': + a, b = e[1], e[2] + rows[a], rows[b] = rows[b], {kk: -v for kk, v in rows[a].items()} + elif k == 'Q_POWER': + rows[e[1]] = left(rows[e[1]], *([('Q', 1 if e[2] > 0 else -1)] * abs(e[2]))) + versions.append(dict(rows[e[1]])) + else: + raise AssertionError('unknown caller event ' + repr(k)) + return tested, hits + + +def caller_reuse_level(ctl): + ev, nf = ctl['physical_events'], 2 * ctl['pairs'] + qi = next(i for i, e in enumerate(ev) if e[0] == 'QUERY_SHEAR') + _, chits = caller_reuse(ev[:qi + 1] + [ev[qi]] + ev[qi + 1:], nf) + need(chits == [[qi + 1, 'QUERY']], 'control: a repeated thin query is found') + tested, hits = caller_reuse(ev, nf) + need(tested == {'QUERY': 15, 'IDLE': 30, 'LOCAL_Y': 18}, 'paid caller output census') + need(not hits, 'a paid caller output is reusable: %r' % hits) + return {'paid_outputs_tested': tested, 'reusable': 0, 'control_repeated_query_found_at_event': qi + 1} + + +def main(): + write = '--write' in sys.argv + depth = 1 + if '--left-depth' in sys.argv: + depth = int(sys.argv[sys.argv.index('--left-depth') + 1]) + word = read_input('word4610') + prov = read_input('provider') + ctl = read_input('caller') + need(prov['source_sha256'] == 'cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd' + and prov['direction'] == 'backward', 'provider word is the PR5402 backward word over the #4610 canonical frames') + result = {'schema': 'zqy-observation-not-retained/2', 'native': {}, 'caller': None, + 'arithmetic': 'exact rational arithmetic: dyadic rows, spans as exact echelon forms over Q; ranks, intersections and non-membership are over Q'} + for name, prog, bw in (('pr5402_provider_backward', prov['word'], True), + ('pr4610_backward', word['programs']['backward'], True), + ('pr4610_forward', word['programs']['forward'], False)): + out = native_level(name, word['canonical'], prog, bw) + result['native'][name] = out + print('[native %s] %s' % (name, json.dumps(out, sort_keys=True)), flush=True) + result['caller'] = caller_level(ctl, depth) + print('[caller] %s' % json.dumps({k: v for k, v in result['caller'].items() if k != 'per_call'}, sort_keys=True), flush=True) + result['reuse'] = {'native': {}, 'caller': None} + for name, prog, bw in (('pr5402_provider_backward', prov['word'], True), + ('pr4610_backward', word['programs']['backward'], True), + ('pr4610_forward', word['programs']['forward'], False)): + out = native_reuse(name, word['canonical'], prog, bw, control=(name == 'pr5402_provider_backward')) + result['reuse']['native'][name] = out + print('[reuse native %s] %s' % (name, json.dumps(out, sort_keys=True)), flush=True) + result['reuse']['caller'] = caller_reuse_level(ctl) + print('[reuse caller] %s' % json.dumps(result['reuse']['caller'], sort_keys=True), flush=True) + if depth != 1: + print('left depth %d run: RESULT.json is recorded at depth 1; not compared' % depth) + print('PASS_ZQY_OBSERVATION_NOT_RETAINED') + return + result['caller_depth2_evidence'] = { + 'note': 'same test with free left factors of length <= 2 (419 factors), run with --left-depth 2 (about 5 minutes, exact over Q); not part of the registered replay', + 'available_at_return': 0, 'available_with_whole_history': 0, 'closure_rank_at_end': 56405} + path = os.path.join(HERE, 'RESULT.json') + text = json.dumps(result, indent=1, sort_keys=True) + '\n' + if write: + with open(path, 'w', encoding='utf-8', newline='\n') as fh: + fh.write(text) + else: + with open(path, encoding='utf-8', newline='') as fh: + need(fh.read() == text, 'RESULT.json differs from the recomputed result; run with --write to refresh') + print('PASS_ZQY_OBSERVATION_NOT_RETAINED') + + +if __name__ == '__main__': + main()