diff --git a/research/qq16-physical-transition/PREDECESSORS.json b/research/qq16-physical-transition/PREDECESSORS.json new file mode 100644 index 0000000000..a7bd80b1a6 --- /dev/null +++ b/research/qq16-physical-transition/PREDECESSORS.json @@ -0,0 +1,46 @@ +{ + "schema_version": 1, + "scope": "Retained exact data and proof text only; no pending executable imports", + "files": [ + { + "pr": 4015, + "head": "0fff81d8997cef646538bcd4f60d7d455cf93b8e", + "source_path": "research/qq16-streaming-recovery/WORD.json", + "local": "vendor/pr4015/WORD.json", + "git_blob": "9a57a6f9c2fd8cdc4e5934408d78ef54e5f266b6", + "sha256": "272d8c1bd172c29044eb227ec6d67a882501250978234685e035158f4479aa58" + }, + { + "pr": 4015, + "head": "0fff81d8997cef646538bcd4f60d7d455cf93b8e", + "source_path": "research/qq16-streaming-recovery/RESULT.json", + "local": "vendor/pr4015/RESULT.json", + "git_blob": "e9b6b8ea6f5a7dc47d8547cd7ed255e3d5864f7d", + "sha256": "b4af55d3db3212e79f8f31108e048c5c2d4c32d520fc980ebaa66f47933ad622" + }, + { + "pr": 4015, + "head": "0fff81d8997cef646538bcd4f60d7d455cf93b8e", + "source_path": "research/qq16-streaming-recovery/PROOF.md", + "local": "vendor/pr4015/PROOF.md", + "git_blob": "8fd64e85e3e595403fe3ae4ed60b9ff368c9a3f5", + "sha256": "81f0fa19b19fa7302ba9c61f4f1b2e11758f973b964240ba48c16ae9b6997396" + }, + { + "pr": 3884, + "head": "2f25b8a68ee676031bcf590c2a95c96a3165dde6", + "source_path": "research/qq16-gaussian-axis-tapes/README.md", + "local": "vendor/pr3884/README.md", + "git_blob": "1c35a8005e4c60d6fa4ecbd3998cb2c6d86a2729", + "sha256": "4bb8a6ce64a01f4adb3749bbf72f3ed3b084d34e6c4c654ac4fa0738d12f540b" + }, + { + "pr": 3394, + "head": "daf052a106a8ff492bafdb4adaae1cc9ca5c9fff", + "source_path": "research/qq16-tagged-cover-routing/PROOF.md", + "local": "vendor/pr3394/PROOF.md", + "git_blob": "44725131a9ecb8b41533492efa7a83bd65aca9ae", + "sha256": "1b32c88e6c6ace2b41a1f2168a6754c329fb1bf9a5b64cf3fec53b31085604ea" + } + ] +} diff --git a/research/qq16-physical-transition/PROOF.md b/research/qq16-physical-transition/PROOF.md new file mode 100644 index 0000000000..2842ea5ebd --- /dev/null +++ b/research/qq16-physical-transition/PROOF.md @@ -0,0 +1,182 @@ +# First hosted-query copy: a paid local tape step and the missing adapter + +This closes one literal physical access/return obligation of PR4015 under an +explicit local window contract. It also identifies why the existing cover-router +and Gaussian-axis implementations do not supply that contract by composition. +It does not provide the actual global caller's windows or a complete native step. + +## Exact source boundary + +PR4015 head `0fff81d8997cef646538bcd4f60d7d455cf93b8e` has 3,813 events. +These are zero-based indices in that complete recovery word, not the outer +execution schedule. Its first streamed query uses port1, q=19, and work bank +Z10. The exact event slice is: + +| Event | Operation | +|---|---| +|1697|CLEAR Z2 into the query2/F16 frame| +|1704|CLEAR Z10 into current/F17| +|1705|Z10 += W1| +|1706|stage2 port1 forward affine cover map on Z10| +|1707|negative rank-one line at q=19 on Z10| +|1708|Z2 += Z10| +|1709–1711|Z3 += Z10; Z5 -= Z10; Z9 -= Z10| + +No event between1697 and1708 references Z2. Thus1708 is exactly the copy +Z2 := Z10, preserving Z10; it requires no read of the old Z2 value. Its source +and destination are both in F16 (axes9 through24) under the inherited full +phase proof. The original paid CLEAR1697 remains charged. Z2 becomes a live +query sum; it is not restored to zero or reinitialized by this optimization. +Later contributions still use ADD. The package authenticates the whole frozen +word and receipt, checks this intervening-reference census, and checks the +actual signed recipe. It does not rerun or claim a new proof of the full decoder. + +## Explicit local tagged-window contract + +Use the tagged record format stated by Dugongue/PR3394; this is a chosen +boundary hypothesis, not a claim that PR4015 already produces that format. +For positive integers n, lambda, M and stored component width W>=2, define + + S = M 2^(n lambda), d = n^2+n lambda, + L = d+2W+2, C = SL+2, H = C+gap, gap>=0. + +There are S records. Each has d tag bits, colon, W real-component bits, +W imaginary-component bits, and semicolon; left/right fences surround it. +Tags represent the same ordered owner/address set in both banks. Both +component fields use the same signed little-endian scale and width. The copy +is exact for arbitrary bits, so it needs no arithmetic range, divisibility or +carry premise. The source native call still needs its own signed-grid and +range proof; those premises have not been established here. + +On one physical tape, Z10 occupies [a,a+C-1], Z2 occupies +[a+H,a+H+C-1], and the intervening gap is included in a traversable reserved +envelope. All five other tapes are arbitrary spectators. The only active head +starts at a. Z2 payload bits are zero by the logical source boundary. Both +banks have intact valid tags/fences; Z10 contains the completed event1707 +result in the agreed encoding. Other content, including the gap, tags, and +exterior, is arbitrary subject to those format premises. + +This supplies no buffer and does not claim that abstract reserved-family IDs +establish these physical windows. It is a conditional implementation of1708. +In particular, the fact that the tagged router returns its head to its origin +is insufficient to prove that a completed native1707 does the same. + +## Literal controller and exact bill + +Compile a fixed schedule for these parameters and offsets. No address lookup +or instantaneous head reset occurs. The controller has one payload-bit register. +For every payload offset x, in increasing record/bit order: + +1. Move by unit steps to a+x and READ one bit. +2. Move by unit steps to a+H+x and WRITE that bit. + +Finally move by unit steps back to a and halt. There are P=2SW payload bits. +The first offset is x0=d+2; the last is xlast=(S-1)L+d+2+2W-1. +All source positions precede all destination positions. Initial travel is x0; +each paired transfer costs H; between transfers the cost is +H-(xnext-xprevious); the last return costs H+xlast. Therefore + + MOVE = x0 + PH + (P-1)H - (xlast-x0) + H+xlast + = 2PH+2(d+2). + READ = P, WRITE = P, + TOTAL = 2P(H+1)+2(d+2). + +Every visit remains inside the supplied envelope. Reads occur only in source +payload cells; writes occur only in destination payload cells. Hence all tags, +source content, gap and exterior are unchanged. The final head is a, and the +five spectator tapes and heads are unchanged. Each destination bit equals its +matching source bit, so the full encoded value and F16 query state are correct. +No initialization or cleanup is omitted: CLEAR1697 is inherited and paid; +there is no scratch allocation or dirty helper to return; the head return is +included. Nonuniform schedule compilation/control description is explicit and +unpriced as an all-size program-loading obligation. Counted READ/WRITE/MOVE +cell actions are not the total time of an admitted uniform compiler. + +The same paired-transfer protocol with a destination READ immediately before +each WRITE has identical movement and P additional reads. Source-proved zero +removes exactly **2SW READ actions**. This is a comparison to that explicitly +defined redundant-read protocol, not a claim of a general bit-adder tariff or +a change to PR4015's scalar allowance. The saving does not return in cleanup: +Z2 is intentionally retained as its query value. + +For any other permutation of the same paired transfers, telescoping gives +2PH+2xfirst. Thus starting at the smallest payload offset minimizes motion +within this one-bit shuttle class. This does not optimize other layouts, +multiple heads, buffered/cached payloads, fused passes or general algorithms. +The bound is quadratic in S for this bank-major layout. Consequently this +literal implementation is a conservative reference and an unattractive +full-cover access choice, not evidence for a favorable complete supplier. + +## The precise obstruction before this copy + +PR3394's actual tagged-map exit has one payload tape, three blank work tapes, +all heads at their respective origins, and the original sorted tags/fences. +PR3884's entry requires two distinct untagged real/imaginary data tapes with +contiguous W-bit components, four owned discardable scratch tapes, and all +six heads at their individual entry origins. Its numerator divisibility and +signed range conditions are caller premises. + +A direct composition already fails at the first symbol: the tagged tape's +origin contains `^`, not a two's-complement bit. Relocating the origin to its +first payload does not solve the problem. Real components have tagged stride +L=d+2W+2 but the bare real tape requires stride W. Translation changes an +origin, not a stride. For the actual n=73, lambda=1 and illustrative W=4, +d=5402 and L=5412. The first real component begins at5404. Its tagged successor +begins at10816, whereas a bare stream reads its successor at5408, the first +imaginary component. The fixture real1=0, imag0=1 witnesses a wrong read even +after the initial-origin issue is repaired. Moreover, one tape's interleaved +payload is not two independent data tapes: an injective spectator-tape +embedding cannot manufacture a second head on it. These are failures of the +verbatim predecessor ABI composition, not impossibility of a paid reformat. + +There is also an independent algebraic trap. Event1707 uses the actual +negative q=19 recipe: both basis column lists are +[19,2,4,8,16,32,64,128,256] and its left offset is19. PR3884's bare coordinate +axis must not replace this entire native event. On input2*real_delta0, the +negative q19 line has nonzero coordinates0 and19; the negative axis0 line has +nonzero coordinates0 and1. W>=3 satisfies the witness's even-numerator and +signed-range conditions. The checker verifies all512 real basis columns of +the supplied positive-axis-plus-two-wrapper recipe. This is a local operator +witness; it does not supply the physical wrapper placement or the full cover. + +ToikY/PR4002 supplies compensated canonical binary-lift phase tags. This +particular source recipe instead consists of explicit permutation wrappers +and a Gaussian rank-one child, with the negative affine offset already paid +symbolically. No K-to-J canonical-lift substitution is made here, so importing +those tags would not repair the tagged/raw storage mismatch. A future changed +native implementation must rebind its own phases and physical costs. + +It follows that adding PR3394's map tariff, PR3884's 32NW axis tariff, and this +copy tariff is **not** a completed1706→1707→1708 implementation. A specific +producer/adapter must first supply the untagged layout, distinct data heads, +four owned scratch windows, actual signed grid, both native wrappers, and a +returned common tagged representation/head for the accumulation. None is +charged zero. PR2722/2794's scalar word-address movement models also do not +supply this bit-layout conversion. + +## Evidence, decision and open next questions + +The checker imports no predecessor executable. It authenticates retained +head/blob/SHA data and text before use, checks the full source slice and zero +lifetime, meters every bit action in translated dirty-exterior fixtures, +compares the complete typed receipt, and rejects wrong offset, missing return, +source/tag overwrite and an intervening query use. Boundary tests cover source, +manifest and typed-receipt changes and normal/optimized read-only Git-free use. +Finite fixtures corroborate the general telescoping/footprint argument. + +Decision: close this exact copy protocol and stop the direct old-tariff +composition. The next useful step is a caller-owned layout adapter around the +actual q19 signed recipe, with head endpoints and width supplied by the caller; +repeating unbound sweep optimizations does not close that gap. The remainder +of the decoder, output ownership, physical allocation, numerical error, +productive-family coverage and both recursive suppliers remain open. No new +kappa, general tape lower bound, formal-kernel or human review is claimed. + +Credit PR4015's streaming/output-bank work; ywz65/PR2707 and Arham Tahir/PR2681 +for the native/full-recovery source; Ali Romman's QQ16 lineage; Dugongue/PR3394 +for tagged matrix-owner routing; Clear1nsight/PR3884 for the signed-bit axis; +Nick Petalas/PR2722 and Arham Tahir/PR2794 for distinct fixed-address methods; +and ToikY/PR4002 for the separately scoped phase-tag handoff. New analysis and +checker by Chris R / Clear1nsight with substantial OpenAI Codex assistance. +Apache-2.0. No predecessor execution or scientific admission is implied by +retaining its proof text and recipe data. diff --git a/research/qq16-physical-transition/README.md b/research/qq16-physical-transition/README.md new file mode 100644 index 0000000000..f1a4158656 --- /dev/null +++ b/research/qq16-physical-transition/README.md @@ -0,0 +1,42 @@ +# Actual first QQ16 query-copy tape boundary + +At PR4015's actual first streamed query, event1708 adds Z10 into Z2, which has +remained zero since its paid CLEAR1697. This source-bound result implements +that exact step as a closed bitwise copy between explicitly supplied tagged +bank-major windows, with source, tags, exterior and all heads preserved. + +For S=M*2^(n*lambda), d=n²+n*lambda, L=d+2W+2, C=SL+2, +inter-bank displacement H=C+gap and P=2SW payload bits, the literal one-bit +shuttle costs P READ, P WRITE and 2PH+2(d+2) MOVE actions. It removes P redundant +destination reads under the identical transfer schedule. No arithmetic scalar +or native child is removed, and the resulting query remains live. + +The same audit pins the preceding map1706 and negative q19 line1707. It gives +concrete header, stride and tape-head witnesses showing that PR3394's tagged +cover-router output does not meet PR3884's bare six-tape Gaussian-axis input. +A signed q19 basis witness also rejects replacing the whole native event with +a bare coordinate axis. A paid representation/native-wrapper adapter remains +necessary; summing those predecessor tariffs does not complete the transition. + +This is a conditional local physical step and a precise direct-composition +obstruction. Actual caller window provision, numerical widths, native/map +placement, other operations and supplier admission remain unproved. The chosen +bank-major shuttle is quadratic in full-cover size and is not promoted as a +favorable global layout. No new kappa or general optimality claim. + +Reproduce from the repository root: + + python3 -I -B research/qq16-physical-transition/verify.py + python3 -I -O -B research/qq16-physical-transition/test_verify.py + python3 -B scripts/research_package.py --package research/qq16-physical-transition + +See PROOF.md for the exact contract, all terms of the bill, attribution, +comparison limits, physical obstruction and open next questions. PREDECESSORS +pins retained pending-head data/text; no pending executable is imported. + +## Open next questions + +Bind a real caller's heads/windows and signed grid around +the first q19 normalization, then construct and price its layout conversion +and return. Family-level ownership/coverage must be supplied independently of +this local access protocol. Substantial OpenAI Codex assistance is disclosed. diff --git a/research/qq16-physical-transition/RESULT.json b/research/qq16-physical-transition/RESULT.json new file mode 100644 index 0000000000..57b4240176 --- /dev/null +++ b/research/qq16-physical-transition/RESULT.json @@ -0,0 +1,102 @@ +{ + "abi_obstruction": { + "first_symbol": "^ rather than a two-complement bit", + "independent_origin_translation": "cannot change stride L to W or split one payload tape into two heads", + "n73_lambda1_W4": { + "L": 5412, + "d": 5402, + "first_real_payload_offset": 5404, + "misread_field": "first imaginary component, e.g. 1 instead of second real component0", + "second_bare_real_offset": 5408, + "second_tagged_real_offset": 10816 + }, + "native_wrapper": "q19 negative recipe cannot be replaced by a bare coordinate axis" + }, + "contract": { + "C": "S*L+2", + "H": "C+gap, gap>=0", + "L": "d+2*W+2", + "M": ">=1", + "P": "2*S*W", + "S": "M*2^(n*lambda)", + "W": ">=2 stored bits/component", + "buffers": 0, + "d": "n*n+n*lambda", + "destination_window": "[a+H,a+H+C-1]", + "initial_and_final_head": "a", + "lambda": ">=1", + "n": ">=1", + "other_five_tapes": "arbitrary unchanged spectators", + "owned_gap": "included in traversable envelope", + "source_window": "[a,a+C-1]" + }, + "exact_cell_actions": { + "MOVE": "2*P*H+2*(d+2)", + "READ": "P", + "TOTAL": "2*P*(H+1)+2*(d+2)", + "WRITE": "P" + }, + "finite_meter": { + "cases": 10, + "cell_actions": 157760, + "controls": [ + "wrong destination offset", + "omit head return", + "overwrite source", + "overwrite tag", + "intervening destination use" + ], + "paired_transfer_orders": 24 + }, + "predecessor_heads": { + "3394": "daf052a106a8ff492bafdb4adaae1cc9ca5c9fff", + "3884": "2f25b8a68ee676031bcf590c2a95c96a3165dde6", + "4015": "0fff81d8997cef646538bcd4f60d7d455cf93b8e" + }, + "saving_against_identical_copy_with_destination_read": "P=2*S*W READ actions, no movement credit", + "scope": { + "no_global_optimality": true, + "no_new_kappa": true, + "proved": "one conditional local physical copy and direct-composition obstruction", + "unknown": [ + "actual caller windows/head placement", + "signed-grid and range at1707", + "tag/raw reformat", + "native wrapper movement", + "map1706 full physical admission", + "remaining accumulations/consumer/whole supplier" + ] + }, + "source_boundary": { + "aligned_add_frame": "F16, axes9 through24", + "bare_axis_witness": { + "bare_axis_nonzero_coordinates": [ + 0, + 1 + ], + "correct_nonzero_coordinates": [ + 0, + 19 + ], + "input": "2*real delta_0, W>=3" + }, + "copy_event": 1708, + "native_q": 19, + "native_recipe_columns_checked": 512, + "native_sign": -1, + "paid_zero_event": 1697, + "role": "Q1 in Z2", + "source_events": [ + 1704, + 1705, + 1706, + 1707, + 1708, + 1709, + 1710, + 1711 + ], + "work_bank": "Z10" + }, + "status": "PASS_SCOPED_PHYSICAL_COPY_AND_ABI_OBSTRUCTION" +} diff --git a/research/qq16-physical-transition/REVIEWS.json b/research/qq16-physical-transition/REVIEWS.json new file mode 100644 index 0000000000..8667523bbd --- /dev/null +++ b/research/qq16-physical-transition/REVIEWS.json @@ -0,0 +1,26 @@ +{ + "status": "PASS_BOUNDED_AI_REVIEWS", + "science_sha256": { + "verify.py": "7e50b8eddcc6c4479f1913370b1b3941eca4c472a18c6425700487a9e4219b87", + "PROOF.md": "f725bed3a941e30e6d36dfef03dd4ad29a9b2a7a4cfaddf35b1897b0897959b2", + "RESULT.json": "c9658de831443460d634b69b1d437a72d129ef455ddb30367166b18ed21cc59d" + }, + "reviews": [ + { + "reviewer": "Independent parallel rounded-trace agent", + "scope": "Read proof/code, derive copy formula and zero-query source binding, inspect retained3394/3884 contract mismatch, optimized warning-strict primary replay.", + "result": "No blocker within stated conditional contract." + }, + { + "reviewer": "Coordinating agent", + "scope": "Read proof/code/formula/ABI and optimized complete primary replay at frozen science hashes.", + "result": "No blocker. Initial receipt mismatch occurred during live editing; final frozen replay passed." + } + ], + "excluded": [ + "human review", + "formal-kernel review", + "actual caller window supply", + "complete physical native transition" + ] +} diff --git a/research/qq16-physical-transition/SOURCES.json b/research/qq16-physical-transition/SOURCES.json new file mode 100644 index 0000000000..0839f4876a --- /dev/null +++ b/research/qq16-physical-transition/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ] +} diff --git a/research/qq16-physical-transition/TASK.json b/research/qq16-physical-transition/TASK.json new file mode 100644 index 0000000000..5e3605fa8f --- /dev/null +++ b/research/qq16-physical-transition/TASK.json @@ -0,0 +1,86 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "joint-query-controller", + "question": "Can a literal QQ16 producer meet the proposed completed-output error budgets with dirty helpers and an affordable physical consumer?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/joint-query/README.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "docs/research/community-efficient1000-review.md", + "research/qq16-producer-defect-transfer/README.md" + ], + "methods": [ + "Derive one literal producer's completed-output defects and intermediate dirty-helper bounds, with its physical bill.", + "Design or audit one consumer, retention or hosting boundary and its complete cost for the pinned producer/decoder." + ], + "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 the revision-6 family record and #2965 producer-defect transfer after the local QQ16 decoder contract. Its author-checked output-error estimate does not implement producer interiors, bound dirty helpers, or pay for the consumer; independently check the implication used.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Pin one literal F0/B1 producer and its native-child contracts; derive the actual intermediate magnitude ledger and completed-output defects, including dirty helpers and correlations. Compare with #2965 budgets and price storage, movement, cleanup and F17 consumption. Stop with a precise missing bound if no producer contract supplies it; do not optimize another decoder precision constant in isolation.", + "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." + ], + "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" + ] + }, + "scope_status": "refined", + "actual_scope": "Bind PR4015 first query ADD1708 to an exact tagged-window bit-copy tariff and audit the preceding cover/native physical ABI.", + "scope_change_reason": "User-assigned actual physical transition audit after4015; one source-bound scalar access step plus a precise direct-composition obstruction.", + "bottleneck_link": "Existing cover-map and Gaussian-axis tariffs use incompatible layouts; the actual first streamed normalization and query copy need head/window and bit-layout contracts.", + "budget_minutes": 60, + "stop_rule": "Pin the first Z10 port and query write; close one literal copy with all movement/return or show the first incompatible predecessor ABI. Do not expand a full physical decoder or sweep search.", + "outcome": "completed", + "evidence": "Exact first-use census,512 signed native recipe columns, literal bit-tape metering and general closed-shuttle proof; concrete header/stride/head ABI obstruction.", + "author": "Chris R / Clear1nsight with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in source inspection, proof, checker/tests, independent agent review and publication.", + "open_questions": [ + { + "question": "Can an actual caller supply and return the tagged/raw layout around event1707?", + "why_it_matters": "The existing cover and axis tariffs cannot compose verbatim and the local copy contract is not supplied by the actual caller.", + "first_step": "Bind the q19 negative wrappers, independent data/scratch heads, signed grid and returned tagged output/head at the first Z10 query.", + "blocked_by": "Unproved physical allocation, encoding/reformat, native wrapper movement and numerical premises." + } + ], + "coordination": { + "assigned": true, + "priority_revision": 6, + "canonical_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "root_checkpoint": "2026-10-19T10:52Z", + "overlap": "Shared root PR/Discussion check; independent QQ16 Z2 physical search had no matches. Coverage partial, no novelty guarantee." + } +} diff --git a/research/qq16-physical-transition/VERIFICATION.json b/research/qq16-physical-transition/VERIFICATION.json new file mode 100644 index 0000000000..72fc5ff3ff --- /dev/null +++ b/research/qq16-physical-transition/VERIFICATION.json @@ -0,0 +1,40 @@ +{ + "status": "PASS_LOCAL_FROZEN_CHECKS", + "python": "3.12.3", + "commands": [ + { + "command": "python3 -I -B research/qq16-physical-transition/verify.py", + "result": "PASS" + }, + { + "command": "python3 -I -O -B research/qq16-physical-transition/verify.py", + "result": "PASS" + }, + { + "command": "python3 -I -O -B research/qq16-physical-transition/test_verify.py", + "result": "2 boundary groups PASS; normal/O Git-free read-only and8 rejecting CLI cases" + }, + { + "command": "python3 -B scripts/research_package.py --package research/qq16-physical-transition", + "result": "PASS_REGISTERED_RESEARCH_PACKAGE outcome=completed; boundary groups4.912s" + } + ], + "scientific_scope": "One explicit local copy tariff plus direct predecessor-ABI composition obstruction.", + "excluded": [ + "actual supplied physical windows", + "full native/map execution", + "uniform compiler cost", + "all-depth supplier admission", + "selected cold replay", + "new kappa", + "hosted CI (recorded separately after publication)" + ], + "workflow": { + "main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "priority_revision": 6, + "entry_checkpoint": "2026-10-19T10:52Z", + "submission_checkpoint": "2026-10-19T11:16Z", + "overlap": "Partial shared PR/Discussion checks plus targeted local search; no exhaustive novelty claim", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/pull/3985#issuecomment-6263114494" + } +} diff --git a/research/qq16-physical-transition/VERIFY.json b/research/qq16-physical-transition/VERIFY.json new file mode 100644 index 0000000000..a590db1d8a --- /dev/null +++ b/research/qq16-physical-transition/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Authenticated full source boundary, signed q19 recipe, exact physical bit/shuttle invoices, source/tag/exterior/head preservation and rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 60, + "checks": "Normal/optimized read-only Git-free replay; source/manifest/typed-receipt mutation and overwrite rejection." + } + ] +} diff --git a/research/qq16-physical-transition/test_verify.py b/research/qq16-physical-transition/test_verify.py new file mode 100644 index 0000000000..34621b8871 --- /dev/null +++ b/research/qq16-physical-transition/test_verify.py @@ -0,0 +1,49 @@ +#!/usr/bin/env python3 +"""Isolated integrity, semantic-boundary and read-only replay controls.""" +import hashlib +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest +HERE=Path(__file__).resolve().parent + +def run(path,opt=False,extra=()): + return subprocess.run([sys.executable,'-I','-B']+(['-O'] if opt else [])+[str(path/'verify.py'),*extra],capture_output=True,text=True,timeout=60,env={'PATH':'','PYTHONDONTWRITEBYTECODE':'1'}) + +def digest_tree(root): + return {str(p.relative_to(root)):hashlib.sha256(p.read_bytes()).hexdigest() for p in root.rglob('*') if p.is_file()} + +class Boundaries(unittest.TestCase): + def test_readonly_git_free_normal_and_optimized(self): + with tempfile.TemporaryDirectory() as temp: + target=Path(temp)/'package';shutil.copytree(HERE,target) + for p in target.rglob('*'):p.chmod(0o555 if p.is_dir() else 0o444) + target.chmod(0o555);before=digest_tree(target) + try: + for opt in (False,True): + result=run(target,opt);self.assertEqual(result.returncode,0,result.stdout+result.stderr) + self.assertIn('PASS_QQ16_PHYSICAL_TRANSITION',result.stdout) + self.assertEqual(before,digest_tree(target));self.assertFalse((Path(temp)/'.git').exists()) + finally: + target.chmod(0o755) + for p in target.rglob('*'):p.chmod(0o755 if p.is_dir() else 0o644) + def test_source_receipt_manifest_and_overwrite_reject(self): + for opt in (False,True): + for name in ('source','manifest','typed receipt','write'): + with self.subTest(opt=opt,name=name),tempfile.TemporaryDirectory() as temp: + target=Path(temp)/'package';shutil.copytree(HERE,target) + if name=='source': + p=target/'vendor/pr4015/WORD.json';p.write_bytes(p.read_bytes()+b' ') + elif name=='manifest': + p=target/'PREDECESSORS.json';p.write_bytes(p.read_bytes()+b' ') + elif name=='typed receipt': + p=target/'RESULT.json';r=json.loads(p.read_text());r['scope']['no_new_kappa']=1;p.write_text(json.dumps(r)) + result=run(target,opt,('--write',) if name=='write' else ()) + self.assertNotEqual(result.returncode,0,result.stdout) + self.assertNotIn('PASS_QQ16_PHYSICAL_TRANSITION',result.stdout) + +if __name__=='__main__':unittest.main(verbosity=2) diff --git a/research/qq16-physical-transition/vendor/pr3394/PROOF.md b/research/qq16-physical-transition/vendor/pr3394/PROOF.md new file mode 100644 index 0000000000..44725131a9 --- /dev/null +++ b/research/qq16-physical-transition/vendor/pr3394/PROOF.md @@ -0,0 +1,224 @@ +# A constructive tagged-stream cover router + +This is an informal mathematical proof with a cell-metered executable model. +The separate Lean theorem proves the algebraic inverse only. It does not +formalize the tape controller, its cost, or a complete multiplication supplier. + +## Exact entry contract and theorem + +Fix positive integers n, lambda and B, an invertible binary n-by-n matrix g, +and a binary column delta. Let D be any nonempty finite set of binary n-by-n +matrices closed under right multiplication by g and g inverse. No membership +oracle or enumeration of the ambient matrix space is supplied to the machine. +Put M = |D|, r = n lambda, N = 2^r, S = MN, d = n^2+r, and L = d+B+2. + +Each record consists of d tag bits, a colon, B arbitrary payload bits, and a +semicolon. Tags encode the owner matrix column by column, with row bits in +increasing order, followed by lambda n-bit payload addresses. The stream has +one left fence ^ and one right fence $. Initially it contains exactly one +record for every (owner,address) in D times (F_2^n)^lambda, in lexicographic tag +order. Payload bits are unrestricted. The tagged layout is an explicit entry +hypothesis; an untagged caller is not silently converted for free. + +The data tape and three work tapes have heads at their respective origins. +Each work window has C = SL+2 initially blank cells. Every tape exterior is +arbitrarily dirty. The fixed alphabet is {blank,0,1,^,$,:,;}. + +Write h = g inverse, u = h delta, and + + q = n nnz(h) + r (1 + wt(u)). + +There is a four-tape finite-control program, depending only on n, lambda, g +and delta, which genuinely halts, returns all heads to their origins, restores +all three work windows to blank, and leaves all tape exteriors unchanged. +Its data output has the original sorted tags and payload + + output(a,z_1,...,z_lambda) + = input(a g, z_1 XOR a delta, ..., z_lambda XOR a delta). + +Its transition count is at most + + T = S [(2d+2) q + (32d+32) L] + 64(d+1). + +At most 4C tape cells are used, including the input window; the work requirement +is three clean windows, not the single global buffer posited in PR3270. +The program family is nonuniform in n, lambda, g and delta. The statement is +uniform in M, B and all valid payload values. It is not an all-size uniform +compiler theorem. In particular, no unpriced universal interpreter is assumed. + +## 1. The correct push tag + +For an input record (e,w), give its output record tag + + a = e h, z_j = w_j XOR e(h delta). + +Then a g = e and z_j XOR a delta = w_j, by associativity and characteristic +two. This proves the desired pullback convention. Owners here are matrices: +replacing e by a 73-bit vector changes the source contract. + +The Lean theorem `QQ16CoverRoute.semidirect_pull_push` verifies exactly this +identity, without assuming that e is invertible. The source finite inverse +checks are separate from that universal statement. + +The push map is a bijection on the actual record set because D is right-closed. +It never pads to all 2^(n^2) matrices or treats one 512-coordinate local kernel +as a full cover. Arbitrary correlations between record payloads are harmless. + +Each output owner bit is an XOR of input owner bits. Repeating the columns of h +for each of n rows uses n nnz(h) input-bit reads. The r address outputs each +read their old address bit and the wt(u) relevant owner-row bits. Hence q is +exact, including all owner-dependent translation terms. + +## 2. Relabel with actual head moves + +`Machine.relabel` copies input into the first work tape. For each output tag bit, +its fixed coefficient positions are visited from the current record origin and +returned from individually. A read at position p costs p outward moves, one +read, p return moves and one parity update, at most 2d+2 transitions. It is not +a constant-cost array lookup. The parity is one finite-control bit. + +The output tag is then written, and the record payload is copied sequentially. +The controller scans to the semicolon; it never stores B or a payload word in +finite control. The non-parity work is bounded by 8L per record. Setup, the +right fence, and both origin returns give a total bound + + S [(2d+2)q + 12L] + 12. + +The coefficient lists are compilation parameters. Their generation and the +source inverse calculation do not occur inside an input-dependent execution. +They define a fixed machine, rather than an unknown runtime oracle. + +## 3. Stable binary partition and radix order + +For one tag position j, inspect that bit and return to the same record origin. +Append the complete record to queue 0 or queue 1, using two forward-only work +tapes. Then rewind, concatenate queue 0 followed by queue 1 into the first work +tape, and clear each consumed queue cell. Equal-bit records retain their order. +The input and output lengths are equal even when one queue is empty. + +Here is a conservative action bill for a single partition. Reads, writes, +finite parity updates and unit head moves are individually charged; moving two +heads counts twice. + +| Part | Bound, excluding fixed fence overhead | +|---|---:| +| Inspect tags and copy all records into the two queues | 6SL | +| Rewind input and both queues, with marker reads | 4SL | +| Copy records back and clear consumed queue cells | 6SL | +| Return/clear queue left fences | 2SL | +| Return the working tape head | 2SL | + +The fixed fence operations use fewer than 64 actions, so `32SL+64` bounds the +whole pass. The left fence of a queue is cleared only after it has been reached. +Clearing it earlier would invalidate the dirty-exterior/origin argument. + +Perform stable partitions at positions d-1, d-2, ..., 0. Inductively, after +processing position j, the records are ordered by the suffix beginning at j. +Thus all tags are sorted at the end. This is a streaming construction of sorting; +it does not call a random-access sorting oracle. The incorrect forward-order +control is included in the executable checks. + +## 4. Copy back, clean and halt + +Copy the sorted stream back onto the data tape while blanking the consumed +working cells. Keep its left fence until the final return. Both heads return +in lockstep using the data tape's intact left fence, then the last working fence +is blanked. This costs at most `8SL+12` actions. The queues are already blank. +The output tags equal the initial tag set and order, by the bijection in part 1. + +Combining the three bills gives + + S [(2d+2)q + (32d+20)L] + 64d + 24, + +which is below the advertised bound. Every visited position belongs to its +reserved window: forward copies stop at the right fence, and rewinds stop at +an intact left fence. The only writes are in these windows. This proves the +arbitrary-dirty-exterior assertion, not merely a zero-exterior test case. + +Every input-dependent loop is driven by a finite symbol and an end fence. +The finite tag-position loops and coefficient reads can be unrolled for the +fixed parameters. The remaining stored values are finitely many symbols and +one parity bit. Consequently this is an ordinary finite-control multitape +program; read/write/move instructions compile to literal transitions, and the +last control state has no outgoing transition. No payload array, unbounded +index, head reset or global arithmetic instruction is hidden in control. + +A direct unrolling has O(dq+d^2) instruction sites, independent of M and B. +This is a fixed-machine description claim, not a billed uniform program-loader +implementation. Code ingestion/control storage in an admitted recursive caller +remains outside the present contract. + +## 5. Reuse of the MathProof tape results + +The construction uses the absolute-coordinate unit-move semantics already +present in `MultitapeAbsolute20261014`, with each read represented by a stationary +transition and each move by one unit. The public portable `Absolute` module +proves equality of its transition count with the head-relative machine model. + +`MultitapeFrameRule20261014` supplies the precise finite-footprint principle: +completed runs transfer to arbitrary matching exteriors, retaining genuine +halting. Our marker argument supplies its footprint premise. The executable +meter also rejects every exterior access in its finite tests. + +`MultitapeTapeEmbedding20261014Next` supplies `lift_runs`, `lift_halts` and +`preserves_extra`: a four-tape run embeds into a larger fixed tape bank at the +same time, with arbitrary spectator tapes unchanged. It justifies reusing three +work tapes while other field tapes remain idle. The caller must still provide +exclusive clean work windows and the tagged entry layout. + +The shared DAG retrieves these canonical source declarations as SOURCE_ONLY; +that label is preserved. Their public portable proof versions were separately +kernel/audit checked in the PR2235 repair, under its own exact source manifest. +No new physical theorem is attributed to that old kernel receipt. PRECEDENTS.json +records the source hashes, statements used, public paths and evidence boundaries. + +## 6. Independent tape origins, with no conversion claim + +For any four integer origins a_i, supply the same local stream and work-window +contents at cells a_i through a_i+C-1, with head i initially at a_i. The identical +finite controller has the same cost, restores the work windows, returns head i +to a_i, and preserves every exterior. This is a useful placement corollary for +larger tape banks; the origins need not agree. + +Proof: replace each cell function c_i(x) by c_i(x-a_i) and its head h_i by +h_i+a_i. The scanned symbol is unchanged. A unit move changes both heads by +the same ±1; a write changes exactly the translated cell. Induction on each +literal transition therefore conjugates the run, with the identical state and +exact time. The terminal table lookup is also unchanged, so genuine halt is +preserved. Window membership and exterior equality translate with the cells. +This is the `relocate_step`/`relocate_completed` symmetry found in the canonical +`MultitapeRelocation20261015` source; its current inspection evidence is recorded +separately from the three publicly hash-matched toolkit modules. + +Both heads and the supplied tape contents are translated. The corollary does +not move an existing head to another entry window for free or prepare a layout. +No caller conversion or allocator has been added to the routing bill. + +## Application to the literal B1 cover maps + +The pinned joint-query certificate has 27,019 B1 events, 528 cover-map calls and +512 distinct map labels. All 512 right-action matrices g are invertible. For n = 73 and +lambda = 1, d = 5402. Separately represented matrix calculations reconstruct every +inverse and the sum of occurrence-weighted relabel reads, Q = 5,451,056. + +Here W denotes the actual stored bit width of one real component, including +sign/format bits; no numerical-grid guard is silently identified with it. +With B = 2W and N = 2^73, summing the routing bounds and one control handoff per call +gives the following conditional per-owner bill for those 528 calls: + + N (182578176 W + 552230342688) + 182578704. + +This is a safe per-owner upper bound: divide the total bill by M and use M ≥ 1 +for its fixed overhead. Owner-set closure is a premise, not reconstructed from a +materialized list of all cover owners. This prices only the cover-map subsequence, assuming that each call receives +the tagged ABI and three clean work windows. It does not execute the other B1 +events or establish that an admitted caller can allocate the layout. The common +four-tape footprint per call is `4 [M N (5402+2W+2)+2]` cells. Work buffers can +be reused serially, so they are not multiplied by 528. The tags and the two +extra buffers relative to PR3270 must not be dropped from an invoice. + +This is a constructive sufficient physical reference contract. It is not a +favorable complete supplier budget or a new kappa. PR3339's owner/idle continuation, +entry conversion, arithmetic, retention, the F17 consumer and all-size compilation +remain distinct costs and obligations. A further implementation round must first +bind and price one actual caller, rather than treating those costs as zero. diff --git a/research/qq16-physical-transition/vendor/pr3884/README.md b/research/qq16-physical-transition/vendor/pr3884/README.md new file mode 100644 index 0000000000..1c35a8005e --- /dev/null +++ b/research/qq16-physical-transition/vendor/pr3884/README.md @@ -0,0 +1,52 @@ +# QQ16 Gaussian-axis arithmetic on six physical bit tapes + +**Scope:** one exactly divisible, nonuniform tensor-axis line primitive, not an F0/B1 producer or an admitted recursive supplier. + +The [native reference](../qq16-native-rounded-components/vendor/native.py) defines, for every coordinate `x` and its partner `y=x xor (1<=1`, signed two's-complement little-endian component width `W>=2`, and an axis `0<=axis= 1 and lam >= 1 and 1 <= owners <= (1 << (n*n)) and width >= 2 and gap >= 0, 'parameter range') + d = n*n + n*lam + records = owners * (1 << (n*lam)) + length = d + 2*width + 2 + window = records*length + 2 + return d, records, length, window, window+gap + +def payload_positions(d, records, length, width): + return [1 + j*length + d + 1 + b for j in range(records) for b in range(2*width)] + +def expected_bill(d, records, width, displacement): + p = 2*records*width + return {'READ': p, 'WRITE': p, 'MOVE': 2*p*displacement + 2*(d+2), + 'TOTAL': 2*p*(displacement+1)+2*(d+2)} + +class Tape: + def __init__(self, cells, origin, allowed): + self.cells = dict(cells) + self.head = origin + self.origin = origin + self.allowed = allowed + self.count = Counter() + def move(self, position): + while self.head != position: + self.head += 1 if position > self.head else -1 + need(self.allowed[0] <= self.head <= self.allowed[1], 'exterior move') + self.count['MOVE'] += 1 + def read(self): + need(self.allowed[0] <= self.head <= self.allowed[1], 'exterior read') + self.count['READ'] += 1 + return self.cells[self.head] + def write(self, bit): + need(self.allowed[0] <= self.head <= self.allowed[1], 'exterior write') + self.count['WRITE'] += 1 + self.cells[self.head] = bit + +def fixture(n, lam, owners, width, gap=0, origin=0, redundant_read=False, mutant=None): + d,s,l,c,h = parameters(n,lam,owners,width,gap) + positions = payload_positions(d,s,l,width) + # Literal finite-alphabet tagged records; no header/tag is read. + cells = {origin+j: '_' for j in range(h+c)} + cells[origin-1] = '$' + cells[origin+h+c] = '^' + for base in (origin,origin+h): + cells[base]='^';cells[base+c-1]='$' + for j in range(s): + start=base+1+j*l + for bit in range(d):cells[start+bit]=(j >> (d-1-bit)) & 1 + cells[start+d]=':';cells[start+l-1]=';' + for k,x in enumerate(positions): + cells[origin+x] = (k*k+3*k+k//3+1) % 2 + cells[origin+h+x] = 0 + before = dict(cells) + machine = Tape(cells,origin,(origin,origin+h+c-1)) + for x in positions: + machine.move(origin+x) + bit = machine.read() + machine.move(origin+h+x+(1 if mutant=='wrong destination offset' else 0)) + if redundant_read: + need(machine.read() == 0, 'source-proved initial zero') + machine.write(bit) + if mutant != 'omit head return': + machine.move(origin) + if mutant == 'overwrite source': + machine.cells[origin+positions[0]] ^= 1 + if mutant == 'overwrite tag': + machine.cells[origin] = 0 + expected = dict(before) + for x in positions: + expected[origin+h+x] = before[origin+x] + need(machine.cells == expected, 'source/tags/exterior or destination mismatch') + need(machine.head == origin, 'head return') + bill = expected_bill(d,s,width,h) + if redundant_read: + bill['READ'] += len(positions) + bill['TOTAL'] += len(positions) + actual = dict(machine.count) + actual['TOTAL'] = sum(machine.count.values()) + need(actual == bill, 'literal action invoice') + return bill + +def act(columns, x): + y = 0 + for i,c in enumerate(columns): + if (x >> i) & 1: + y ^= c + return y + +def source_boundary(word, receipt): + expected = [ + ['clear','Z10','current'], ['add','Z10','W1','1'], + ['map','Z10',2,1,False], ['line','Z10',1,-1], + ['add','Z2','Z10','1'], ['add','Z3','Z10','1'], + ['add','Z5','Z10','-1'], ['add','Z9','Z10','-1']] + need(word[1704:1712] == expected, 'first query event slice') + need(word[1697] == ['clear','Z2','query2'], 'paid Z2 initialization') + need(not any('Z2' in e[1:3] for e in word[1698:1708]), 'Z2 used before first query copy') + need(receipt['hosting']['aliases']['D']=='Z10' and receipt['hosting']['aliases']['Q1']=='Z2', 'actual hosted roles') + recipe = [r for r in receipt['native_lowering']['signed_rank_one_recipes'] if 1707 in r['events']] + need(len(recipe)==1, 'unique actual native recipe') + r=recipe[0] + columns=[19,2,4,8,16,32,64,128,256] + need(r['q']==19 and r['sign']==-1 and r['left_offset']==19 and r['left_columns']==columns and r['right_columns']==columns, 'signed source recipe') + # Integer numerators are even for 2*delta_x, W>=3. Compare the actual + # signed kernel to its supplied positive-axis/permutation realization. + for x in range(512): + right=act(columns,x) + wrapped={act(columns,right)^19:(1,1),act(columns,right^1)^19:(1,-1)} + intended={x:(1,-1),x^19:(1,1)} + need(wrapped==intended, 'actual native wrapper relation') + direct_axis={0:(1,-1),1:(1,1)} + intended={0:(1,-1),19:(1,1)} + need(direct_axis != intended, 'bare-axis substitution witness') + return {'source_events':list(range(1704,1712)), 'copy_event':1708, + 'paid_zero_event':1697,'role':'Q1 in Z2','work_bank':'Z10', + 'aligned_add_frame':'F16, axes9 through24', + 'native_q':19,'native_sign':-1,'native_recipe_columns_checked':512, + 'bare_axis_witness':{'input':'2*real delta_0, W>=3', 'correct_nonzero_coordinates':[0,19], 'bare_axis_nonzero_coordinates':[0,1]}} + +def compute(): + pins=authenticate() + word=json.loads((HERE/'vendor/pr4015/WORD.json').read_text()) + receipt=json.loads((HERE/'vendor/pr4015/RESULT.json').read_text()) + need(len(word)==3813,'whole source word length') + boundary=source_boundary(word,receipt) + cases=0; totals=0 + for n,lam,owners,width,gap,origin in [(1,1,1,2,0,0),(2,1,1,3,0,-13),(2,1,2,4,7,29),(3,1,1,5,11,101),(2,1,3,3,2,-7)]: + new=fixture(n,lam,owners,width,gap,origin) + old=fixture(n,lam,owners,width,gap,origin,True) + _,s,_,_,_=parameters(n,lam,owners,width,gap) + need(old['TOTAL']-new['TOTAL']==2*s*width,'zero-destination read saving') + cases+=2;totals+=new['TOTAL']+old['TOTAL'] + direction_paths=0 + for order in permutations((2,3,7,8)): + head=0;motion=0 + for x in order: + motion+=abs(x-head)+12;head=12+x + motion+=head + need(motion==2*4*12+2*order[0], 'one-bit shuttle control identity') + direction_paths+=1 + rejected=[] + for mutant in ('wrong destination offset','omit head return','overwrite source','overwrite tag'): + try:fixture(2,1,1,3,2,13,mutant=mutant) + except ValueError:rejected.append(mutant) + else:raise ValueError('accepted physical mutant '+mutant) + bad=[list(e) for e in word];bad[1699]=['add','Z2','Z10','1'] + try:source_boundary(bad,receipt) + except ValueError:rejected.append('intervening destination use') + else:raise ValueError('accepted nonzero-query source mutation') + d,s,l,c,h=parameters(73,1,1,4) + # Sparse address witness needs no astronomical full-cover allocation. + first=d+2 + second_tagged=first+l + second_bare=first+4 + need(second_bare==first+4 and second_bare!=second_tagged,'record-stride obstruction') + return {'status':'PASS_SCOPED_PHYSICAL_COPY_AND_ABI_OBSTRUCTION', + 'source_boundary':boundary, + 'contract':{'n':'>=1','lambda':'>=1','M':'>=1','W':'>=2 stored bits/component', + 'S':'M*2^(n*lambda)','d':'n*n+n*lambda','L':'d+2*W+2','C':'S*L+2', + 'H':'C+gap, gap>=0','P':'2*S*W', + 'source_window':'[a,a+C-1]','destination_window':'[a+H,a+H+C-1]', + 'initial_and_final_head':'a','owned_gap':'included in traversable envelope', + 'buffers':0,'other_five_tapes':'arbitrary unchanged spectators'}, + 'exact_cell_actions':{'READ':'P','WRITE':'P','MOVE':'2*P*H+2*(d+2)','TOTAL':'2*P*(H+1)+2*(d+2)'}, + 'saving_against_identical_copy_with_destination_read':'P=2*S*W READ actions, no movement credit', + 'finite_meter':{'cases':cases,'cell_actions':totals,'paired_transfer_orders':direction_paths,'controls':rejected}, + 'abi_obstruction':{'first_symbol':'^ rather than a two-complement bit', + 'n73_lambda1_W4':{'d':d,'L':l,'first_real_payload_offset':first, + 'second_tagged_real_offset':second_tagged,'second_bare_real_offset':second_bare, + 'misread_field':'first imaginary component, e.g. 1 instead of second real component0'}, + 'independent_origin_translation':'cannot change stride L to W or split one payload tape into two heads', + 'native_wrapper':'q19 negative recipe cannot be replaced by a bare coordinate axis'}, + 'scope':{'proved':'one conditional local physical copy and direct-composition obstruction', + 'unknown':['actual caller windows/head placement','signed-grid and range at1707','tag/raw reformat','native wrapper movement','map1706 full physical admission','remaining accumulations/consumer/whole supplier'], + 'no_new_kappa':True,'no_global_optimality':True}, + 'predecessor_heads':{str(r['pr']):r['head'] for r in pins['files']}} + +def main(): + p=argparse.ArgumentParser();p.add_argument('--write',action='store_true');args=p.parse_args() + out=HERE/'RESULT.json' + if args.write:need(not out.exists(),'refuse overwrite') + result=compute() + if args.write: + need(not out.exists(),'refuse overwrite');out.write_text(json.dumps(result,indent=2,sort_keys=True)+'\n') + else:need(canonical(json.loads(out.read_text()))==canonical(result),'typed complete receipt') + print('PASS_QQ16_PHYSICAL_TRANSITION no_new_kappa') +if __name__=='__main__':main()