From 2c06582c2c3e7dc23107ad0cee562ace5de853b0 Mon Sep 17 00:00:00 2001 From: Matarener <52912325+Matarener@users.noreply.github.com> Date: Sat, 24 Oct 2026 13:29:14 +0300 Subject: [PATCH 1/5] Certify that the coupled-exit observation b = Z Q Y is not retained (negative result, no new kappa) Adds research/zqy-observation-not-retained, answering #5415 open question 1, #5419 experiment 1 and #5425 open question 1 in the formal free-word grammar: no full-frame version of the PR5402 provider word or the #4610 word (both orientations) contains pure y content, and b = Z Q Y is outside the free span of all caller versions at every one of the 18 backward FULL returns, also with the whole caller history. Co-Authored-By: Claude Opus 5.5 (1M context) --- .../zqy-observation-not-retained/PROOF.md | 41 ++ .../zqy-observation-not-retained/README.md | 85 ++++ .../zqy-observation-not-retained/RESULT.json | 162 ++++++++ .../zqy-observation-not-retained/SOURCES.json | 48 +++ .../zqy-observation-not-retained/TASK.json | 96 +++++ .../zqy-observation-not-retained/VERIFY.json | 23 ++ .../zqy-observation-not-retained/verify.py | 391 ++++++++++++++++++ 7 files changed, 846 insertions(+) create mode 100644 research/zqy-observation-not-retained/PROOF.md create mode 100644 research/zqy-observation-not-retained/README.md create mode 100644 research/zqy-observation-not-retained/RESULT.json create mode 100644 research/zqy-observation-not-retained/SOURCES.json create mode 100644 research/zqy-observation-not-retained/TASK.json create mode 100644 research/zqy-observation-not-retained/VERIFY.json create mode 100644 research/zqy-observation-not-retained/verify.py diff --git a/research/zqy-observation-not-retained/PROOF.md b/research/zqy-observation-not-retained/PROOF.md new file mode 100644 index 0000000000..956aa2a166 --- /dev/null +++ b/research/zqy-observation-not-retained/PROOF.md @@ -0,0 +1,41 @@ +# 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. Reduction modulo the odd prime `2^61 − 1` is a +ring map on such rationals, so a rational identity `target = Σ c_i v_i` maps to +an identity modulo p. The computed non-membership modulo p therefore implies +non-membership over the rationals. diff --git a/research/zqy-observation-not-retained/README.md b/research/zqy-observation-not-retained/README.md new file mode 100644 index 0000000000..7736a416e4 --- /dev/null +++ b/research/zqy-observation-not-retained/README.md @@ -0,0 +1,85 @@ +# The coupled-exit observation b = Z Q Y is not retained anywhere + +**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. + +## What is checked (`verify.py`, about 15 s, standard library) + +**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 2 minutes) 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; spans are computed modulo the prime +2^61 − 1. An identity over the rationals reduces to one modulo p, so +non-membership modulo p implies non-membership over the rationals. + +## 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. +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..50de183714 --- /dev/null +++ b/research/zqy-observation-not-retained/RESULT.json @@ -0,0 +1,162 @@ +{ + "arithmetic": "exact dyadic rows, spans modulo 2^61-1 (non-membership mod p implies non-membership 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 2 minutes); 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 + } + }, + "schema": "zqy-observation-not-retained/1" +} 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..7907625750 --- /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)?", + "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.", + "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 their 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.", + "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..689beb4742 --- /dev/null +++ b/research/zqy-observation-not-retained/VERIFY.json @@ -0,0 +1,23 @@ +{ + "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": 300, + "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; RESULT.json byte comparison." + }, + { + "argv": ["{python}", "-I", "-O", "-W", "error", "-B", "{package}/verify.py"], + "timeout_seconds": 300, + "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..25fc6c545d --- /dev/null +++ b/research/zqy-observation-not-retained/verify.py @@ -0,0 +1,391 @@ +#!/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 modulo the prime 2^61-1. All coefficients are dyadic, so an identity over +the rationals reduces to one modulo p; non-membership modulo p therefore implies +non-membership over the rationals. Controls show that both tests can say yes. + +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)) +P = (1 << 61) - 1 +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 modulo p +class Span: + """Sparse reduced echelon basis modulo P.""" + + 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) % P + 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 = pow(v[c], P - 2, P) + v = {k: x * inv % P 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) % P + 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): + out = {} + for key, q in row.items(): + c = index.setdefault(key, len(index)) + need(q.denominator & (q.denominator - 1) == 0, 'dyadic coefficient') + out[c] = q.numerator % P * pow(q.denominator % P, P - 2, P) % P + 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 + + +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/1', 'native': {}, 'caller': None, + 'arithmetic': 'exact dyadic rows, spans modulo 2^61-1 (non-membership mod p implies non-membership 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) + 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 2 minutes); 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() From 2b6316dadcee3b66ce976336d8b134be684d7898 Mon Sep 17 00:00:00 2001 From: Matarener <52912325+Matarener@users.noreply.github.com> Date: Sat, 24 Oct 2026 13:35:00 +0300 Subject: [PATCH 2/5] Point the current CI section at frontier5413 (exact repair from #5420) Canonical main still names make frontier4610-verify while the selected record requires frontier5413-verify, so the shared onboarding test fails before any package replay. This reuses byte-for-byte the docs/ci-verification.md repair of #5420 (head baa8fbb8345c2fab0bc213479539c338d4c80443, Clear1nsight); no scientific file changes. Co-Authored-By: Claude Opus 5.5 (1M context) --- docs/ci-verification.md | 34 +++++++++++++++++++++++++++++++++- 1 file changed, 33 insertions(+), 1 deletion(-) diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 494b7ca1d4..3bf623230e 100644 --- a/docs/ci-verification.md +++ b/docs/ci-verification.md @@ -1,8 +1,40 @@ # CI verification -## Current selected-family replay: #4610 with #5241 +## Current selected-family replay: #5413 with #5407 and #5414 The [selected record](../certificates/selected-result.json) binds conditional +κ = 0.003027288235, the [promotion and scope](research/pr-intake-evidence/pr5413-promotion/PROMOTION.md), +[explicit source closure](../certificates/frontier5413-source.json), +[review validation](research/pr-intake-evidence/pr5413-promotion/VALIDATION.json), and +[integration receipt](research/pr-intake-evidence/pr5413-promotion/INTEGRATION.json). + +`make frontier5413-verify` authenticates the selected source manifest, derives +the certificate from frozen numerical evidence, and exports the complete +three-package execution closure. It replays #5407's five-stage provider audit, +#5413's eight-stage admission, and #5414's independent companion screen serially. +The exported inputs are checked again afterward. Source-bound #4610/#5241 and +earlier BIT/native/compiler/tape/analytic foundation coverage is explicitly +reused; its historical suites are not rerun. + +Each package runs under an external sampled 1 GiB aggregate descendant-memory +guard, with timeouts of 660 seconds for the provider and primary packages and +120 seconds for the companion. On macOS the replay uses the reviewed RLIMIT_AS +adapter; on Linux it invokes the unmodified package wrappers. The recorded +successful local macOS replay does not establish a hosted Linux pass. + +The [frontier5413 workflow](../.github/workflows/frontier5413.yml) is manual-only, +uses Python 3.12 on Ubuntu, materializes the declared source closure, and uploads +receipts and logs. Its status is separate from local validation and recorded in +the integration receipt. Routine donor PRs do not launch this selected replay. + +`make selected-record-check` verifies metadata and source/proof hashes. It does +not execute the operators or prove the five inherited framework assumptions. +The finite checks do not establish the full integer multiplication theorem, +and the uniform word remains unmaterialized. + +## Historical selected-family replay: #4610 with #5241 + +The historical [selected record](../certificates/checkpoints/frontier4610.json) binds conditional κ = 0.0030217758, the [review](research/pr-intake-evidence/pr4610/PROOF-REVIEW.md), [explicit source closure](../certificates/frontier4610-source.json), [review validation](research/pr-intake-evidence/pr4610/VALIDATION.json), and From 389578f2d3ef075495ce76f08100ac50e18f7d40 Mon Sep 17 00:00:00 2001 From: Matarener <52912325+Matarener@users.noreply.github.com> Date: Sat, 24 Oct 2026 13:53:37 +0300 Subject: [PATCH 3/5] Add part 2: no paid native or caller response is reusable (response-reuse census) For every paid climb/centre of the PR5402 provider word and the #4610 word (both orientations), the result is not in the span of earlier versions in its target frame, neither before the climb nor before the next touch of the field; no thin query, IDLE or LOCAL Y output of the p16 caller is a free combination of earlier versions. Injected-copy and repeated-query controls. Answers the global occurrence-ledger question of #5423 on the frozen words. Co-Authored-By: Claude Opus 5.5 (1M context) --- .../zqy-observation-not-retained/PROOF.md | 18 ++ .../zqy-observation-not-retained/README.md | 43 +++- .../zqy-observation-not-retained/RESULT.json | 57 ++++- .../zqy-observation-not-retained/TASK.json | 8 +- .../zqy-observation-not-retained/VERIFY.json | 25 ++- .../zqy-observation-not-retained/verify.py | 201 +++++++++++++++++- 6 files changed, 338 insertions(+), 14 deletions(-) diff --git a/research/zqy-observation-not-retained/PROOF.md b/research/zqy-observation-not-retained/PROOF.md index 956aa2a166..df5c291257 100644 --- a/research/zqy-observation-not-retained/PROOF.md +++ b/research/zqy-observation-not-retained/PROOF.md @@ -39,3 +39,21 @@ All coefficients are dyadic. Reduction modulo the odd prime `2^61 − 1` is a ring map on such rationals, so a rational identity `target = Σ c_i v_i` maps to an identity modulo p. The computed non-membership modulo p therefore implies non-membership over the rationals. + +## 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 index 7736a416e4..192aaa4a43 100644 --- a/research/zqy-observation-not-retained/README.md +++ b/research/zqy-observation-not-retained/README.md @@ -1,4 +1,4 @@ -# The coupled-exit observation b = Z Q Y is not retained anywhere +# 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 @@ -11,7 +11,7 @@ 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. -## What is checked (`verify.py`, about 15 s, standard library) +## 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 @@ -47,6 +47,43 @@ pure-y version is detected (intersection 1); at every caller return the current 2^61 − 1. An identity over the rationals reduces to one modulo p, so non-membership modulo p implies non-membership over the rationals. +## 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 @@ -66,7 +103,7 @@ 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. -The result shows that the supplied-observation branch of #5415 section 4 has no +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 diff --git a/research/zqy-observation-not-retained/RESULT.json b/research/zqy-observation-not-retained/RESULT.json index 50de183714..f5af2a0490 100644 --- a/research/zqy-observation-not-retained/RESULT.json +++ b/research/zqy-observation-not-retained/RESULT.json @@ -158,5 +158,60 @@ "versions_with_y_content": 1851 } }, - "schema": "zqy-observation-not-retained/1" + "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/TASK.json b/research/zqy-observation-not-retained/TASK.json index 7907625750..34b890107e 100644 --- a/research/zqy-observation-not-retained/TASK.json +++ b/research/zqy-observation-not-retained/TASK.json @@ -70,13 +70,13 @@ ] }, "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)?", + "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.", + "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 their controls; do not start a new native word or a decoder search.", + "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.", + "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": [ diff --git a/research/zqy-observation-not-retained/VERIFY.json b/research/zqy-observation-not-retained/VERIFY.json index 689beb4742..94db12f56e 100644 --- a/research/zqy-observation-not-retained/VERIFY.json +++ b/research/zqy-observation-not-retained/VERIFY.json @@ -10,13 +10,28 @@ ], "commands": [ { - "argv": ["{python}", "-I", "-W", "error", "-B", "{package}/verify.py"], - "timeout_seconds": 300, - "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; RESULT.json byte comparison." + "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": 300, + "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 index 25fc6c545d..791a136c27 100644 --- a/research/zqy-observation-not-retained/verify.py +++ b/research/zqy-observation-not-retained/verify.py @@ -28,6 +28,14 @@ the rationals reduces to one modulo p; non-membership modulo p therefore implies non-membership over the rationals. 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. """ @@ -349,6 +357,188 @@ def absorb(): 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 @@ -359,7 +549,7 @@ def main(): 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/1', 'native': {}, 'caller': None, + result = {'schema': 'zqy-observation-not-retained/2', 'native': {}, 'caller': None, 'arithmetic': 'exact dyadic rows, spans modulo 2^61-1 (non-membership mod p implies non-membership over Q)'} for name, prog, bw in (('pr5402_provider_backward', prov['word'], True), ('pr4610_backward', word['programs']['backward'], True), @@ -369,6 +559,15 @@ def main(): 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') From dacc35b1f35c2b4bc2e3910520ba5cf46a020bed Mon Sep 17 00:00:00 2001 From: Matarener <52912325+Matarener@users.noreply.github.com> Date: Sat, 24 Oct 2026 20:36:15 +0300 Subject: [PATCH 4/5] Compute every ZQY span exactly over Q instead of modulo 2^61-1 Review of #5427: non-membership modulo p only excludes p-integral coefficients. The span engine now keeps exact Fraction echelon forms, so all ranks, intersections and non-memberships (both parts) are over Q. Every recorded number is unchanged, including the optional depth-2 run (closure rank 56405, 0 of 18). Co-Authored-By: Claude Opus 5.5 (1M context) --- .../zqy-observation-not-retained/PROOF.md | 11 +++++--- .../zqy-observation-not-retained/README.md | 12 +++++--- .../zqy-observation-not-retained/RESULT.json | 4 +-- .../zqy-observation-not-retained/verify.py | 28 ++++++++++--------- 4 files changed, 32 insertions(+), 23 deletions(-) diff --git a/research/zqy-observation-not-retained/PROOF.md b/research/zqy-observation-not-retained/PROOF.md index df5c291257..87145494a7 100644 --- a/research/zqy-observation-not-retained/PROOF.md +++ b/research/zqy-observation-not-retained/PROOF.md @@ -35,10 +35,13 @@ with every version of the whole caller history. ## Arithmetic -All coefficients are dyadic. Reduction modulo the odd prime `2^61 − 1` is a -ring map on such rationals, so a rational identity `target = Σ c_i v_i` maps to -an identity modulo p. The computed non-membership modulo p therefore implies -non-membership over the rationals. +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 diff --git a/research/zqy-observation-not-retained/README.md b/research/zqy-observation-not-retained/README.md index 192aaa4a43..bbfd8dc77e 100644 --- a/research/zqy-observation-not-retained/README.md +++ b/research/zqy-observation-not-retained/README.md @@ -36,16 +36,20 @@ versions. No version word begins with a `Z` letter, so `b = Z_s Q Y` is availabl 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 2 minutes) gives +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; spans are computed modulo the prime -2^61 − 1. An identity over the rationals reduces to one modulo p, so -non-membership modulo p implies non-membership over the rationals. +**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 diff --git a/research/zqy-observation-not-retained/RESULT.json b/research/zqy-observation-not-retained/RESULT.json index f5af2a0490..9466b07861 100644 --- a/research/zqy-observation-not-retained/RESULT.json +++ b/research/zqy-observation-not-retained/RESULT.json @@ -1,5 +1,5 @@ { - "arithmetic": "exact dyadic rows, spans modulo 2^61-1 (non-membership mod p implies non-membership over Q)", + "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, @@ -124,7 +124,7 @@ "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 2 minutes); not part of the registered replay" + "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": { diff --git a/research/zqy-observation-not-retained/verify.py b/research/zqy-observation-not-retained/verify.py index 791a136c27..714261b7b9 100644 --- a/research/zqy-observation-not-retained/verify.py +++ b/research/zqy-observation-not-retained/verify.py @@ -24,9 +24,11 @@ (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 modulo the prime 2^61-1. All coefficients are dyadic, so an identity over -the rationals reduces to one modulo p; non-membership modulo p therefore implies -non-membership over the rationals. Controls show that both tests can say yes. +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. @@ -48,7 +50,6 @@ HERE = os.path.dirname(os.path.abspath(__file__)) ROOT = os.path.dirname(os.path.dirname(HERE)) -P = (1 << 61) - 1 INPUTS = { 'provider': ('research/native-rank8-helper-provider/WORD.json.gz', '7dc356001ed597ad6fc9fd3e0bc6ff7e3ec3a580a579a956827aa17fccfdd2dc'), @@ -72,9 +73,9 @@ def read_input(name): return json.loads(gzip.decompress(raw) if rel.endswith('.gz') else raw) -# ---------------------------------------------------------------- exact span modulo p +# ---------------------------------------------------------------- exact span over Q class Span: - """Sparse reduced echelon basis modulo P.""" + """Sparse reduced echelon basis over Q (exact Fractions).""" def __init__(self): self.piv = {} @@ -87,7 +88,7 @@ def reduce(self, v): return v f = v[hit] for c, x in self.piv[hit].items(): - nv = (v.get(c, 0) - f * x) % P + nv = v.get(c, 0) - f * x if nv: v[c] = nv else: @@ -98,13 +99,13 @@ def add(self, v): if not v: return False c = min(v) - inv = pow(v[c], P - 2, P) - v = {k: x * inv % P for k, x in v.items()} + 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) % P + nv = b.get(k, 0) - f * x if nv: b[k] = nv else: @@ -119,11 +120,12 @@ def copy(self): 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] = q.numerator % P * pow(q.denominator % P, P - 2, P) % P + out[c] = Fr(q) return out @@ -550,7 +552,7 @@ def main(): 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 dyadic rows, spans modulo 2^61-1 (non-membership mod p implies non-membership over Q)'} + '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)): @@ -573,7 +575,7 @@ def main(): 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 2 minutes); not part of the registered replay', + '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' From b1a46d30b41eab1836a8a9b32412e2eb40b5345d Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Sun, 25 Oct 2026 07:14:34 +0000 Subject: [PATCH 5/5] Record that the queue-oct24a hold on #5427 names the modular head. The retained receipt still binds open PR 5427 to 389578f2. The exact-Q repair dacc35b1f is that head's child and is not in main. The other three waiting-revision rows are unchanged and unretained. No closure. Co-authored-by: unpaidmoon --- research/pr5427-hold-head-receipt/README.md | 94 +++++++++++ .../pr5427-hold-head-receipt/SOURCES.json | 58 +++++++ research/pr5427-hold-head-receipt/TASK.json | 60 +++++++ research/pr5427-hold-head-receipt/VERIFY.json | 21 +++ research/pr5427-hold-head-receipt/verify.py | 155 ++++++++++++++++++ 5 files changed, 388 insertions(+) create mode 100644 research/pr5427-hold-head-receipt/README.md create mode 100644 research/pr5427-hold-head-receipt/SOURCES.json create mode 100644 research/pr5427-hold-head-receipt/TASK.json create mode 100644 research/pr5427-hold-head-receipt/VERIFY.json create mode 100644 research/pr5427-hold-head-receipt/verify.py diff --git a/research/pr5427-hold-head-receipt/README.md b/research/pr5427-hold-head-receipt/README.md new file mode 100644 index 0000000000..b18632c9b1 --- /dev/null +++ b/research/pr5427-hold-head-receipt/README.md @@ -0,0 +1,94 @@ +# Receipt for the four queue-oct24a holds, and the changed head of #5427 + +**Task:** `overlap-receipt`, refined to one existing intake receipt. +**Base:** canonical main `32890bc5de034ab8fc93ac88ead7279a6a416d04`. +**No new κ. No closure, merge, or ledger edit.** + +The 2026-10-24 queue snapshot +`docs/research/pr-intake-evidence/queue-oct24a-20261024.json` records 20 +decisions, of which four are `waiting_revision`: #4580, #4612, #5427 and +#5432. The central ledger on this base still has those four open, +partially reviewed, and not installed. Three of those recorded heads were +still the GitHub heads when this note was written. **#5427 was not.** + +## What the retained receipt says + +| PR | Author on the receipt | Recorded head | Retained on this base | +|---|---|---|---| +| [#4580](https://github.com/CrocSwap/integer-mult-bounds/pull/4580) | Matarener | `55de56abdfd9cd7fb83758241793c18b9ae9ce71` | nothing | +| [#4612](https://github.com/CrocSwap/integer-mult-bounds/pull/4612) | Matarener | `0e0df631da41a1f9ed3489e8df532189c2643cbf` | nothing | +| [#5427](https://github.com/CrocSwap/integer-mult-bounds/pull/5427) | Matarener | `389578f2d3ef075495ce76f08100ac50e18f7d40` | nothing | +| [#5432](https://github.com/CrocSwap/integer-mult-bounds/pull/5432) | hevlyo | `6532b45ce9f3259d7408594ec480a140ec81e0e2` | nothing | + +#5427's unresolved question is still Clear1nsight's Part 1 qualification: +the head claims rational-span consequences from one modular calculation, the +counterexample is `A=[p]`, `b=1`, and Part 2 is not independently accepted. +Credit for that comment stays with Chris R / Clear1nsight. Credit for the +ZQY census stays with Mark / Matarener. + +## What changed after the receipt + +GitHub on 2026-10-25 showed #5427 at +`e0192de5d97e5ac09f42d26d9ceedee6377c77e2` +(updated 2026-10-24T17:50:50Z). That commit's parents are exactly + +- `dacc35b1f35c2b4bc2e3910520ba5cf46a020bed` — "Compute every ZQY span exactly over Q instead of modulo 2^61-1", whose parent is the recorded head `389578f2`; +- `32890bc5de034ab8fc93ac88ead7279a6a416d04` — this receipt's base. + +`dacc35b1f` is not contained in the base. The recorded hold therefore +describes `389578f2` and does not describe the head that was live during +this check. The intake rule that a different head wakes an entry applies +to #5427 only. It does not, on these pins, apply to #4580, #4612 or #5432: +those three GitHub heads matched the receipt on the same observation. + +On `dacc35b1f` the false sentence "non-membership modulo p therefore +implies non-membership over the rationals" is gone from `PROOF.md`. The +proof states the `A=[p]`, `b=1` counterexample. `verify.py` no longer +assigns `P = (1 << 61) - 1` or takes a modular inverse. Its `Span.add` +reports that `1` lies in the rational span of `p = 2^61-1`. An independent +one-line check agrees: `p ≡ 0` modulo `p`, while `(1/p)·p = 1` over `Q`. + +## Author-checker replay, not acceptance + +At `e0192de5`, in `/tmp` on CPython 3.12.3: + +```sh +python3 -I -W error -B research/zqy-observation-not-retained/verify.py +``` + +exited 0 and printed `PASS_ZQY_OBSERVATION_NOT_RETAINED`. The script +compares its recomputation with the committed `RESULT.json`, so the +recorded ranks matched that run. This is one replay of Matarener's +checker. It is not an independent census, not a review of Part 2's +EARLY/LATE or caller-output reading, and not a reason to merge. The +`--left-depth 2` run and the optimised command were not run. The package +was absent from base `32890bc5`. + +## Reproduce this receipt + +```sh +python3 -B research/pr5427-hold-head-receipt/verify.py +python3 -B scripts/research_package.py --package research/pr5427-hold-head-receipt --check-only +``` + +Expected marker: `PASS_PR5427_HOLD_HEAD_RECEIPT`. + +The checker reads the two receipt files, checks the commit parents above, +and runs the one-column rational dependence on the repaired `Span` class. +It does not contact GitHub. A later push of #5427 can move the live head +without changing this historical observation. + +## Open next questions + +Re-read #5427 at `e0192de5` before any closure. The arithmetic sentence that +blocked `389578f2` is not the text of `dacc35b1f`, but Part 2 was never +accepted, and a passing author checker is not that acceptance. The blocker +is a maintainer review of the new head; this receipt does not perform it. + +## Credit + +The queue-oct24a snapshot and the ledger rows are the maintained intake +record on `32890bc5`. Clear1nsight wrote the Part 1 qualification at +`389578f2`. Mark / Matarener wrote the ZQY package and the exact-Q repair. +The package scaffold is Douglas Colkitt's. Prepared by unpaidmoon with +substantial Cursor Grok assistance. Apache-2.0. No selected-frontier change. diff --git a/research/pr5427-hold-head-receipt/SOURCES.json b/research/pr5427-hold-head-receipt/SOURCES.json new file mode 100644 index 0000000000..8c1bee9912 --- /dev/null +++ b/research/pr5427-hold-head-receipt/SOURCES.json @@ -0,0 +1,58 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "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": "docs/research/pr-intake-evidence/queue-oct24a-20261024.json", + "usage": "input", + "git_blob": "f5f1ed6ba8330714a11f499c9849503101d80639", + "sha256": "65f6edd08052d7160a5318badea7c982e91252891a2cb02f7d8d24a8efc660e5" + }, + { + "path": "docs/research/pr-ledger.json", + "usage": "input", + "git_blob": "0ef27eee22300a0a512af129a0d8778ae4af46ab", + "sha256": "30af48f6f9bb64c698feeeafcf5c68e5ff76f6175f8757ee6ff45566152d1529" + }, + { + "path": "research/zqy-observation-not-retained/verify.py", + "usage": "provenance", + "pin": "head:389578f2d3ef075495ce76f08100ac50e18f7d40:research/zqy-observation-not-retained/verify.py", + "git_blob": "791a136c2711854e53a021a0040a976c4ded233b", + "sha256": "40fd198b79490c5897feb45cd8b6fbe9cf3f8f5c9e0215efb2b9973c8e92106a" + }, + { + "path": "research/zqy-observation-not-retained/PROOF.md", + "usage": "provenance", + "pin": "head:389578f2d3ef075495ce76f08100ac50e18f7d40:research/zqy-observation-not-retained/PROOF.md", + "git_blob": "df5c291257f1957427ec1be4a5b2549464e0473d", + "sha256": "2aa0021037d3b3fa7419322d00fa0191cd064076eaf031175275ea0bfd902eab" + }, + { + "path": "research/zqy-observation-not-retained/verify.py", + "usage": "provenance", + "pin": "head:dacc35b1f35c2b4bc2e3910520ba5cf46a020bed:research/zqy-observation-not-retained/verify.py", + "git_blob": "714261b7b91a58cff6bffcd2c9dbd7f88f3cf345", + "sha256": "ae307d2474a9cb6e5ea1ae3f723f2c28e22c04678672b757eaa675fa7b59363a" + }, + { + "path": "research/zqy-observation-not-retained/PROOF.md", + "usage": "provenance", + "pin": "head:dacc35b1f35c2b4bc2e3910520ba5cf46a020bed:research/zqy-observation-not-retained/PROOF.md", + "git_blob": "87145494a75de26c10991d890341977ea3a193dc", + "sha256": "8eda309451f20ac25aff3746752060b95151799f65a6537dc59cb0aff758f25c" + } + ] +} diff --git a/research/pr5427-hold-head-receipt/TASK.json b/research/pr5427-hold-head-receipt/TASK.json new file mode 100644 index 0000000000..19696b8c88 --- /dev/null +++ b/research/pr5427-hold-head-receipt/TASK.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "task_id": "overlap-receipt", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "overlap-receipt", + "question": "What exact content and credit of a small named PR set has already been retained?", + "starting_points": [ + "docs/research/pr-ledger.md", + "CONTRIBUTORS.md" + ], + "methods": [ + "Compare exact heads and retained artifacts to write a source-bound disposition receipt.", + "Audit an existing receipt for missing content or predecessor attribution." + ], + "acceptance_gate": "Separate complete integration, partial retention and changed heads; make no autonomous closures.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read one small PR set in the ledger and identify exact reviewed heads and unresolved content.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Compare that set to retained artifacts; produce a complete or explicitly partial disposition receipt.", + "bottleneck_link": "Reliable overlap evidence preserves credit and prevents repeated review of already-retained material.", + "allowed_variations": [ + "One small related PR family or one existing integration receipt." + ], + "scope_change_triggers": [ + "Treating matching titles or one shared blob as proof of full incorporation." + ], + "overlap_terms": [ + "overlap receipt", + "partial integration", + "attribution" + ] + }, + "scope_status": "refined", + "actual_scope": "Audit the four waiting_revision rows of the queue-oct24a receipt and separate #5427's recorded modular head from its exact-Q child.", + "scope_change_reason": "The catalogue card allows one existing integration receipt. This audit names that receipt, the four unretained heads, and the one head that moved. It does not survey a new PR family or recommend a closure.", + "bottleneck_link": "Side result for review routing. A stale modular obstruction on #5427 mis-states whether the ZQY observation is rationally unavailable; that question is adjacent to a supplied-observation screen, but this receipt does not change kappa.", + "budget_minutes": 60, + "stop_rule": "Stop after the four-row receipt. Do not replay the ZQY census inside this package, edit the ledger, or close #5427.", + "outcome": "completed", + "evidence": "Verifier checks the pinned ledger and queue-oct24a rows, the parent link 389578f2 -> dacc35b1f -> e0192de5, removal of the false modular implication, and the repaired Span on A=[p], b=1. One author-checker replay at e0192de5 printed PASS_ZQY_OBSERVATION_NOT_RETAINED and is not acceptance.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance with the receipt, the checker, and the one author-checker replay.", + "open_questions": [ + { + "question": "Does the exact-Q text at e0192de5 discharge only the Part 1 arithmetic hold, leaving Part 2 unaccepted?", + "why_it_matters": "Closing #5427 from the old sentence would treat a changed head as reviewed, and accepting Part 2 from a shared Span class would go beyond Clear1nsight's stated boundary.", + "first_step": "Re-read PROOF.md Part 2 and the EARLY/LATE caller tests at e0192de5, using the author replay only as a numerical control.", + "blocked_by": "This receipt does not review Part 2 and does not recommend a GitHub state change." + } + ] +} diff --git a/research/pr5427-hold-head-receipt/VERIFY.json b/research/pr5427-hold-head-receipt/VERIFY.json new file mode 100644 index 0000000000..c8bca83ab8 --- /dev/null +++ b/research/pr5427-hold-head-receipt/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "docs/research/pr-intake-evidence/queue-oct24a-20261024.json", + "docs/research/pr-ledger.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Four waiting_revision heads remain unretained in the pinned ledger and queue-oct24a snapshot; #5427's repair commit is the child of the recorded head and is not in the base; the false modular implication stays on the old proof; the repaired Span accepts 1 in the rational span of 2^61-1 and rejects an off-axis target." + } + ] +} diff --git a/research/pr5427-hold-head-receipt/verify.py b/research/pr5427-hold-head-receipt/verify.py new file mode 100644 index 0000000000..e5821fc4b8 --- /dev/null +++ b/research/pr5427-hold-head-receipt/verify.py @@ -0,0 +1,155 @@ +#!/usr/bin/env python3 +"""Receipt check for the four waiting-revision rows in queue-oct24a. + +The retained ledger and intake snapshot still name PR #5427 head +389578f2. That head's child, dacc35b1f, replaces the modular span with an +exact rational span. This checker does not replay the ZQY census and does +not close the pull request. +""" + +import json +import os +import subprocess + +OLD = "389578f2d3ef075495ce76f08100ac50e18f7d40" +REPAIR = "dacc35b1f35c2b4bc2e3910520ba5cf46a020bed" +LIVE = "e0192de5d97e5ac09f42d26d9ceedee6377c77e2" +BASE = "32890bc5de034ab8fc93ac88ead7279a6a416d04" +PKG = "research/zqy-observation-not-retained" +FALSE_IMPLICATION = ( + "The computed non-membership modulo p therefore implies\n" + "non-membership over the rationals." +) +COUNTEREXAMPLE = "for `A = [p]`, `b = 1` the target is outside the modular" +HOLDS = { + 4580: "55de56abdfd9cd7fb83758241793c18b9ae9ce71", + 4612: "0e0df631da41a1f9ed3489e8df532189c2643cbf", + 5427: OLD, + 5432: "6532b45ce9f3259d7408594ec480a140ec81e0e2", +} + +ROOT = os.path.dirname(os.path.dirname(os.path.dirname(os.path.abspath(__file__)))) + + +def fail(message): + raise SystemExit(message) + + +def git(*args): + result = subprocess.run( + ["git", *args], cwd=ROOT, check=False, capture_output=True, text=True, + ) + if result.returncode != 0: + fail(args[0] + " failed: " + (result.stderr or result.stdout).strip()) + return result.stdout.strip() + + +def show(rev, path): + return subprocess.check_output( + ["git", "show", rev + ":" + path], cwd=ROOT, + ).decode("utf-8") + + +def ancestor(commit, descendant): + result = subprocess.run( + ["git", "merge-base", "--is-ancestor", commit, descendant], + cwd=ROOT, check=False, + ) + return result.returncode == 0 + + +def load_span(source): + start = source.index("class Span:") + end = source.index("\ndef modrow(") + namespace = {} + exec( + "from fractions import Fraction as Fr\nP = (1 << 61) - 1\n" + source[start:end], + namespace, + ) + return namespace["Span"], namespace["Fr"] + + +def member(span_cls, rows, target): + span = span_cls() + for row in rows: + span.add(dict(row)) + return span.reduce(dict(target)) == {} + + +def receipt_rows(): + ledger = json.loads( + open(os.path.join(ROOT, "docs/research/pr-ledger.json"), encoding="utf-8").read() + ) + intake = json.loads( + open( + os.path.join(ROOT, "docs/research/pr-intake-evidence/queue-oct24a-20261024.json"), + encoding="utf-8", + ).read() + ) + by_number = {row["number"]: row for row in ledger["pull_requests"]} + contributions = {row["number"]: row for row in intake["contributions"]} + for number, head in HOLDS.items(): + if number not in by_number or number not in contributions: + fail("missing receipt row " + str(number)) + recorded = by_number[number] + decision = contributions[number] + if recorded["current_head"] != head or recorded["reviewed_head"] != head: + fail("ledger head moved for " + str(number)) + if recorded["github_state"] != "OPEN" or recorded["disposition"] != "partially_reviewed": + fail("ledger state changed for " + str(number)) + if recorded["closure"] is not None or recorded["integration_location"]: + fail("PR " + str(number) + " is recorded as retained") + if decision["head"] != head or decision["lane"] != "waiting_revision": + fail("intake row changed for " + str(number)) + text = by_number[5427]["unresolved_question"] + if "A=[p]" not in text or "b=1" not in text or "Q certificate" not in text: + fail("ledger no longer states the modular-arithmetic hold") + if "Part 2 is not independently accepted" not in text: + fail("ledger dropped the Part 2 boundary") + + +def commit_chain(): + if git("rev-parse", REPAIR + "^") != OLD: + fail("repair commit is not the child of the recorded head") + parents = git("rev-parse", LIVE + "^@").split() + if parents != [REPAIR, BASE]: + fail("live head parents are " + " ".join(parents)) + if ancestor(REPAIR, BASE): + fail("repair commit is already contained in the receipt base") + if not ancestor(OLD, REPAIR) or not ancestor(BASE, LIVE): + fail("expected ancestry does not hold") + + +def arithmetic(): + old_proof = show(OLD, PKG + "/PROOF.md") + new_proof = show(REPAIR, PKG + "/PROOF.md") + old_code = show(OLD, PKG + "/verify.py") + new_code = show(REPAIR, PKG + "/verify.py") + if FALSE_IMPLICATION not in old_proof or FALSE_IMPLICATION in new_proof: + fail("false modular implication is not confined to the recorded head") + if COUNTEREXAMPLE not in new_proof or COUNTEREXAMPLE in old_proof: + fail("reviewer counterexample is not stated on the repair head") + if "pow(v[c], P - 2, P)" not in old_code or "pow(v[c], P - 2, P)" in new_code: + fail("modular inverse is not confined to the recorded checker") + if "P = (1 << 61) - 1" not in old_code or "P = (1 << 61) - 1" in new_code: + fail("prime modulus assignment is not confined to the recorded checker") + new_span, fraction = load_span(new_code) + prime = (1 << 61) - 1 + if not member(new_span, [{0: fraction(prime)}], {0: fraction(1)}): + fail("repaired Span missed the rational dependence 1 = (1/p) p") + if member(new_span, [{0: fraction(1)}], {1: fraction(1)}): + fail("repaired Span reported a vector outside a one-coordinate span") + # Independent of either checker: the Fp image of [p] is 0, while 1 = (1/p)·p over Q. + if prime % prime != 0 or fraction(1, prime) * prime != 1: + fail("counterexample arithmetic failed") + + +def main(): + receipt_rows() + commit_chain() + arithmetic() + print("PASS_PR5427_HOLD_HEAD_RECEIPT") + + +if __name__ == "__main__": + main()