diff --git a/research/qq16-adjacent-add-bill/PROOF.md b/research/qq16-adjacent-add-bill/PROOF.md new file mode 100644 index 0000000000..b6f52a0e49 --- /dev/null +++ b/research/qq16-adjacent-add-bill/PROOF.md @@ -0,0 +1,44 @@ +# Frame bill for events 9894 and 9895 + +The forward core and the canonical word are the pinned inputs named in +`SOURCES.json`. Frames are lists of integer axes. Frame 0 is `[]` and frame 4 +is `[459]`. + +A climb from frame `a` to frame `b` of recorded rank `r` is legal only when +every axis of `a` lies in the `F_2`-span of the axes of `b` and +`r = |b| - |a| > 0`. It then sets that register's current frame to `b`. +A scalar operation annotated with frame `f` is legal only when every `L` +operand's current frame is already `f`. These are the checks in `verify.py`. + +Event 9894 is `['climb', 'A', 546, 0, 4, 1]`. It is the first climb in the +word, so every register is still at `start`. `start[546] = 0` and +`start[561] = 4`. Empty axes sit in the span of `[459]`, and `1 = 1 - 0`, +so the climb is legal and leaves `L546` in frame 4. `L561` is not the +climbed register. + +Event 9895 is `['scalar', ['add', ['L', 546], ['L', 561], -1, 1], 4]`. +Both current frames equal 4, so the annotation is legal. The event does not +write a new frame. No earlier scalar writes `L561`. The only earlier event +that names 561 is the entrance wrapper +`['residual_adapter', 'pre', 561, 4]`, which the same contract requires to +repeat the entrance frame. + +The retained coefficient count for a positive numerator and a power-of-two +denominator is: one clear, one step per bit after the leading bit, one step +per `1` bit, one step per halving, then `+2` for the signed accumulation and +the work clear. For absolute value 1 and denominator 1 that count is 4. +The invoice's real-step total is twice that count, so 8. The same count +applies to `+1`. + +The pair's rank histogram therefore gains one rank-1 child and no scalar +rank child. Adding `L561` back, with coefficient `+1` and the same frame, is +legal in that state and costs another 4 scalar steps. It restores the +post-climb value of `L546` and leaves both frames at 4. + +The recipe table contains `(old, new) = (0, 4)` at rank 1 and does not +contain `(4, 0)`. The published `final` vector puts both registers at frame +1. The forward replay that applies every climb reaches that vector, so the +word never uses a rank-decreasing climb to undo event 9894. + +No six-tape origin is read here. A zero frame delta is not a zero physical +layout bill. diff --git a/research/qq16-adjacent-add-bill/README.md b/research/qq16-adjacent-add-bill/README.md new file mode 100644 index 0000000000..a82c0dc81a --- /dev/null +++ b/research/qq16-adjacent-add-bill/README.md @@ -0,0 +1,69 @@ +# Adjacent F0 ADD after the first rank-positive climb + +**Partial frame bill. No new κ.** Selected conditional κ stays +`0.001672660197076918`. + +On the pinned forward core, event 9894 is the word's first climb: +`L546` from frame 0 (`[]`) to frame 4 (`[459]`), rank 1. Event 9895 is +`L546 -= L561` in frame 4. `L561` enters in frame 4 and is not climbed or +written before that ADD. Both operands already sit in the annotated frame, so +the retained nested-frame contract accepts the ADD with no second climb. + +The coefficient `-1/1` costs 4 scalar work steps and 8 real steps under the +retained bit-clear / bit-add / halving count. The sign does not add a step. +The climb is the pair's only rank child (`+1` at rank 1). Replaying every +climb and every `L` scalar in the forward word reproduces `final`. + +The in-frame inverse `L546 += L561` is legal at the same 4-step cost and +restores only the post-climb value. The pinned Clifford table has no child +`(4, 0)`. Both registers end at frame 1, not at `L546`'s entrance frame 0. + +This does not assign six-tape windows, meter the climb's kernel, or price a +consumer. Unknown physical layout cost is not zero. PR #3932 bound event 9894 +and left this ADD unpriced. PR #4114 ledgers rays `L359` and `L112`; it does +not replay this pair. + +## Scope and evidence + +Task `joint-query-controller`, scope **refined** to this one pair. The card's +allowed variation is one changed first pair. Base +`bb4bccbf42844d2801487450727c2f63e10d1d0f`, priority revision 6. Pins are in +[SOURCES.json](SOURCES.json). The argument is checked by +[verify.py](verify.py), not by a separate prose proof. + +## Reproduce + +From the repository root, CPython 3.12: + +```sh +python3.12 -B scripts/research_package.py --package research/qq16-adjacent-add-bill +``` + +Expected: + +```text +PASS_QQ16_ADJACENT_ADD_BILL climb=9894 add=9895 frame=4 axis=459 rank_child=1 scalar_work=4 real_steps=8 climbs_before_pair=0 reverse_child=absent word_climbs=3486 word_scalars=20089 no_new_kappa +PASS_REGISTERED_RESEARCH_PACKAGE research/qq16-adjacent-add-bill outcome=partial +``` + +Controls inside the verifier: the published final-frame vector, a unit / `3/1` / +`1/2` work triple, rejection of the ADD with the climb deleted, and rejection +if `L561` enters in frame 0. + +## Credit + +The forward word and frame table are the pinned joint-query / selected-replay +sources. PR #3932 (Chris R / Clear1nsight) named event 9895 as the unpriced +successor of event 9894. The nested-frame rule is the retained local checker +contract. New check by unpaidmoon, with substantial Cursor Grok assistance. +Apache-2.0. No independent human or formal-kernel review. + +## Open next questions + +1. What physical head moves does this ADD cost once `L546` and `L561` are + placed on real six-tape windows? Same-frame legality does not meter layout + or the climb's kernel. The blocker is PR #3932's unbound intervals and head + positions. +2. Which cleanup child returns `L546` from frame 4 to entrance frame 0? The + in-frame inverse does not. The forward contract only admits strict rank + increases, and no recipe child `(4, 0)` is present. diff --git a/research/qq16-adjacent-add-bill/SOURCES.json b/research/qq16-adjacent-add-bill/SOURCES.json new file mode 100644 index 0000000000..ff980d5a88 --- /dev/null +++ b/research/qq16-adjacent-add-bill/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "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" + }, + { + "path": "research/community-frontier1042-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b", + "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754" + }, + { + "path": "research/joint-query/certificate.json.gz", + "usage": "input", + "git_blob": "c6e876d8b48d768214deee265ade428f8983b566", + "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" + } + ] +} diff --git a/research/qq16-adjacent-add-bill/TASK.json b/research/qq16-adjacent-add-bill/TASK.json new file mode 100644 index 0000000000..d315f49985 --- /dev/null +++ b/research/qq16-adjacent-add-bill/TASK.json @@ -0,0 +1,85 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 6, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "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": "Price the one adjacent scalar ADD after the first rank-positive F0 climb: event 9895 is L546 -= L561 in frame 4, with no extra frame change.", + "scope_change_reason": "The card's first experiment asks for one literal F0 producer's intermediate bill. PR #3932 already binds climb event 9894 and leaves the next ADD unpriced. PR #4114 ledgers rays L359 and L112. This package prices only that named adjacent pair under the retained nested-frame contract.", + "bottleneck_link": "The native local words exist; a same-frame ADD is the first continuation after the unpaid rank-1 climb. Its frame bill says whether that continuation asks for another relocation before any consumer is priced.", + "budget_minutes": 60, + "stop_rule": "Stop after this one pair. Do not assign physical tape origins, replay the six-tape kernel, or price later adds that read L561.", + "outcome": "partial", + "evidence": "Source-bound frame replay of the pinned forward word: the ADD is legal with both operands already in frame 4, the climb is the only rank-1 child, and the coefficient -1/1 costs 4 retained scalar work steps. No recipe climbs from frame 4 back to frame 0.", + "author": "unpaidmoon", + "ai_assistance": "Cursor Grok 4.7 wrote the verifier and the note. No independent human or formal-kernel review.", + "open_questions": [ + { + "question": "What physical head moves does this ADD cost once L546 and L561 are placed on real six-tape windows?", + "why_it_matters": "Same-frame legality does not meter layout, encoding, or the climb's kernel. Unknown physical cost is not zero.", + "first_step": "Bind both registers to the two data windows named by PR #3932 and count head motion for one coordinatewise subtraction.", + "blocked_by": "PR #3932 leaves physical intervals, origins, and head positions unbound." + }, + { + "question": "Which cleanup child, if any, returns L546 from frame 4 to its entrance frame 0?", + "why_it_matters": "The in-frame inverse ADD restores only the post-climb value. Entrance restoration is a separate rank-decreasing step, and the pinned recipe table has no child (4, 0).", + "first_step": "Search the forward cleanup phase for a rank-decreasing return of register 546, or prove none exists.", + "blocked_by": "The forward contract only admits strict rank increases, so the return is not a forward climb." + } + ] +} diff --git a/research/qq16-adjacent-add-bill/VERIFY.json b/research/qq16-adjacent-add-bill/VERIFY.json new file mode 100644 index 0000000000..39e8ea14b6 --- /dev/null +++ b/research/qq16-adjacent-add-bill/VERIFY.json @@ -0,0 +1,17 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1042-audit/selected-replay.tar.gz", + "research/joint-query/certificate.json.gz" + ], + "commands": [ + { + "argv": ["{python}", "-B", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "Literal events 9894 and 9895, nested-frame legality of that ADD, scalar work 4, absent reverse child (4, 0), and controls that drop the climb, move L561, or change the coefficient." + } + ] +} diff --git a/research/qq16-adjacent-add-bill/verify.py b/research/qq16-adjacent-add-bill/verify.py new file mode 100644 index 0000000000..32480be3f2 --- /dev/null +++ b/research/qq16-adjacent-add-bill/verify.py @@ -0,0 +1,192 @@ +#!/usr/bin/env python3 +"""Price one adjacent F0 ADD after the first rank-positive climb. + +The retained local contract is the nested-frame rule used by the selected +word: a climb replaces a register's frame only by a strict rank increase, and +a scalar ADD may read only registers that already sit in its annotated frame. +This note does not admit a physical tape layout or a new kappa. +""" +import gzip +import hashlib +import io +import json +import tarfile +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +CERTIFICATE = "research/joint-query/certificate.json.gz" +ARCHIVE = "research/community-frontier1042-audit/selected-replay.tar.gz" +CERTIFICATE_SHA = "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" +ARCHIVE_SHA = "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754" +WORD_MEMBER = "slots/local/CANONICAL-WORD.json.gz" +WORD_SHA = "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219" +RECIPE_MEMBER = "slots/local/CLIFFORD-RECIPES.json" +RECIPE_SHA = "d0768f2164d5f64a2fdbec422f1cfde4e400818792f1904ca541958377243731" +CLIMB = ["climb", "A", 546, 0, 4, 1] +ADD = ["scalar", ["add", ["L", 546], ["L", 561], -1, 1], 4] +INVERSE = ["scalar", ["add", ["L", 546], ["L", 561], 1, 1], 4] +PREFIX_SHA = "15115954461f2cb93e2266822d82bfac1ab8de7d460ff78fcf594d21c61d2b53" +CLIMB_INDEX = 9894 +ADD_INDEX = 9895 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def digest(obj): + raw = json.dumps(obj, sort_keys=True, separators=(",", ":")).encode() + return hashlib.sha256(raw).hexdigest() + + +def load_bytes(path, sha, cap): + file = ROOT / path + need(file.is_file() and not file.is_symlink(), "source file: " + path) + raw = file.read_bytes() + need(len(raw) <= cap, "source cap: " + path) + need(hashlib.sha256(raw).hexdigest() == sha, "source sha: " + path) + return raw + + +def contained(old, new): + """True when every old axis lies in the F2-span of the new axes.""" + span = list(new) + for vector in old: + reduced = vector + for axis in span: + pivot = axis.bit_length() - 1 + if pivot >= 0 and (reduced >> pivot) & 1: + reduced ^= axis + if reduced: + return False + return True + + +def scalar_work(numerator, denominator): + """Retained coefficient bill: clear, bit doubles, bit adds, halvings, +2. + + The sign is inside the final +2, so +1 and -1 have the same count. + """ + need(numerator > 0 and denominator > 0, "positive coefficient parts") + need(denominator & (denominator - 1) == 0, "dyadic denominator") + count = 1 + for index, bit in enumerate(bin(numerator)[2:]): + if index: + count += 1 + if bit == "1": + count += 1 + count += denominator.bit_length() - 1 + return count + 2 + + +def replay(events, start, frames): + current = list(start) + climbs = 0 + scalars = 0 + for index, event in enumerate(events): + kind = event[0] + if kind == "climb": + _, _part, register, old, new, rank = event + need(current[register] == old, "climb leaves its recorded frame") + need(contained(frames[old], frames[new]), "climb is not nested") + need(rank == len(frames[new]) - len(frames[old]) > 0, "climb rank") + current[register] = new + climbs += 1 + elif kind == "scalar": + _gate, operation, frame = event + operands = [operation[1]] + if operation[0] in ("add", "copy"): + operands.append(operation[2]) + for token in operands: + if token[0] == "L": + need(current[token[1]] == frame, + "scalar operand leaves the annotated frame at " + str(index)) + scalars += 1 + return current, climbs, scalars + + +def main(): + certificate = json.loads(gzip.decompress(load_bytes(CERTIFICATE, CERTIFICATE_SHA, 8 * 1024**2))) + events = certificate["core_words"]["forward"] + need(events[CLIMB_INDEX] == CLIMB, "climb event changed") + need(events[ADD_INDEX] == ADD, "adjacent ADD changed") + need(digest(events[:CLIMB_INDEX]) == PREFIX_SHA, "prefix before the climb changed") + archive = load_bytes(ARCHIVE, ARCHIVE_SHA, 64 * 1024**2) + with tarfile.open(fileobj=io.BytesIO(archive), mode="r:gz") as tar: + word_info = tar.getmember(WORD_MEMBER) + recipe_info = tar.getmember(RECIPE_MEMBER) + need(word_info.isfile() and recipe_info.isfile(), "word members") + word_raw = tar.extractfile(word_info).read() + recipe_raw = tar.extractfile(recipe_info).read() + need(hashlib.sha256(word_raw).hexdigest() == WORD_SHA, "word sha") + need(hashlib.sha256(recipe_raw).hexdigest() == RECIPE_SHA, "recipe sha") + word = json.loads(gzip.decompress(word_raw)) + recipes = json.loads(recipe_raw) + frames = word["frames"] + start = word["start"] + need(frames[0] == [] and frames[4] == [459], "frame 0 and frame 4") + need(start[546] == 0 and start[561] == 4, "entrance frames") + children = {(child["old"], child["new"]): child for child in recipes["children"]} + need(children[(0, 4)]["rank"] == 1, "forward child rank") + need((4, 0) not in children, "reverse child unexpectedly present") + + moved_561 = [index for index, event in enumerate(events[:ADD_INDEX]) + if event[0] == "climb" and event[2] == 561] + need(moved_561 == [], "L561 climbs before the ADD") + writes_561 = [index for index, event in enumerate(events[:ADD_INDEX]) + if event[0] == "scalar" and event[1][1] == ["L", 561]] + need(writes_561 == [], "L561 is written before the ADD") + need(events[7963] == ["residual_adapter", "pre", 561, 4], "entrance wrapper") + + current, climbs, scalars = replay(events, start, frames) + need(current == word["final"], "replay misses the published final frames") + need(word["final"][546] == 1 and word["final"][561] == 1, "published endpoints") + climbs_before = sum(1 for event in events[:CLIMB_INDEX] if event[0] == "climb") + need(climbs_before == 0, "an earlier climb already moved a register") + before = replay(events[:CLIMB_INDEX], start, frames)[0] + need(before == list(start), "frames move before the first climb") + at_add = replay(events[:ADD_INDEX], start, frames)[0] + need(at_add[546] == 4 and at_add[561] == 4, "pair frames") + after = replay(events[:ADD_INDEX + 1], start, frames)[0] + need(after[546] == 4 and after[561] == 4, "the ADD does not change frames") + + work = scalar_work(1, 1) + real_steps = 2 * work + need(work == 4 and real_steps == 8, "unit coefficient work") + need(scalar_work(3, 1) == 6 and scalar_work(1, 2) == 5, "work controls") + + # Dropping the climb leaves L546 in frame 0, so the frame-4 ADD is illegal. + try: + replay([ADD], start, frames) + except ValueError as exc: + need("annotated frame" in str(exc), "missing-climb control") + else: + raise ValueError("ADD without the climb was accepted") + + # An entrance for L561 in frame 0 is also illegal: the source would move. + moved_start = list(start) + moved_start[561] = 0 + try: + replay(events[CLIMB_INDEX:ADD_INDEX + 1], moved_start, frames) + except ValueError as exc: + need("annotated frame" in str(exc), "moved-source control") + else: + raise ValueError("ADD with relocated L561 was accepted") + + _restored, _climbs, inverse_scalars = replay([INVERSE], at_add, frames) + need(inverse_scalars == 1 and scalar_work(1, 1) == work, "inverse work") + + print( + "PASS_QQ16_ADJACENT_ADD_BILL" + " climb=9894 add=9895 frame=4 axis=459" + " rank_child=1 scalar_work=%d real_steps=%d" + " climbs_before_pair=%d reverse_child=absent" + " word_climbs=%d word_scalars=%d" + " no_new_kappa" + % (work, real_steps, climbs_before, climbs, scalars) + ) + + +if __name__ == "__main__": + main()