diff --git a/research/p111-line7-query-price/NOTICE.md b/research/p111-line7-query-price/NOTICE.md new file mode 100644 index 0000000000..91d2acd964 --- /dev/null +++ b/research/p111-line7-query-price/NOTICE.md @@ -0,0 +1,15 @@ +SPDX-License-Identifier: Apache-2.0 + +The pinned word and centre seed are byte copies of Rohan Arun's PR #1525 at +`90d39a5603c7fbfd8d8d957e9732d9b6ebd6317f`, paths +`research/p111-early-merge-query/inputs/word-base.json.gz` and +`research/p111-early-merge-query/CENTRE-SEED.json`. That draft retains the +PR1297 word, the PR1134 arithmetic, and the PR1060 physical model, with the +notices in that package. Those predecessor files are not modified here. + +The containment test is the same subspace test as PR1060 `model.py`. This +package reimplements that one predicate; it does not vendor or replay the +PR1060 compiler. + +New checks and text: unpaidmoon, with substantial Cursor Grok assistance. +Apache-2.0. No independent human review is claimed. diff --git a/research/p111-line7-query-price/README.md b/research/p111-line7-query-price/README.md new file mode 100644 index 0000000000..0e760cfa3b --- /dev/null +++ b/research/p111-line7-query-price/README.md @@ -0,0 +1,82 @@ +# Line-span(7) query does not beat its zero-frame scatter + +**No new κ.** Selected conditional κ stays `781451/250000000`. Discussion #1166 +comment +[19143427](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19143427) +already stopped one triangular continuation of Rohan Arun's draft PR #1525 at +`90d39a5603c7fbfd8d8d957e9732d9b6ebd6317f`, and left the evidence in local paths. +This package replays that scatter identity from the pinned bytes and checks the +constructor fact the handoff left open: `model.move` rejects a descent from +`span(7)` to the zero frame. + +## Result + +Puncture 0 builds `q = (c61 + c63 + c31 + c256) / 2`. On the pinned word, the +copied query is the line `span(7)`. The retained cut is 176 zero-frame centre +ADDs, 22 from each of the eight centres. The triangular substitution + +- column 61 becomes twice itself, +- columns 63, 31 and 256 each lose column 61, + +reproduces every original scatter linear form. Each of the 112 outputs is a +vector on the 704 roles. This check does not replay section B. The corrected +matrix has 230 nonzero ADD entries, exactly 54 more. Those 54 split by support: +column 63 overlaps column 61 in 8 rows and cancels 4 of them (`+10`), while +columns 31 and 256 are disjoint from column 61 (`+22` each). JoyboyBrian's +handoff already recorded the 230-versus-176 census. The overlap split is checked +here. + +All 62 dirty columns of `q` already appear in those original outputs. A final +map that equals the original scatter therefore keeps every one of them. A final +map that zeroes any of them does not deliver the original target outputs. + +The PR1060 constructor `move` admits a change only when the old frame is +contained in the new one. `contained((7,), ())` is false, so that constructor +rejects moving the query register from `span(7)` to the zero frame. The handoff +priced the same conversion if a paid rank-1 copy is granted instead, and the +profiles it named are `{1: 4, 8: 1}` and `{1: 5, 8: 1}`. For every positive +integer power tariff those two multisets differ by exactly 1. The same strict +increase holds for every tariff that gives rank 1 a positive price and prices +no other rank differently. The 54 extra ADDs are further nonnegative scalar +cost on this matrix. + +## What this does not show + +This does not price a scatter that consumes the line-7 query directly, a +different correction matrix, whole-call owners, precision, tape, compiler, or +outer admission. It does not replay section B and it does not change the +selected frontier. The handoff's local scripts remain unpublished; these checks +recompute the scatter identity from the pinned word and centre seed. + +## Reproduction + +Python 3.12, standard library only: + +```sh +python3 -B research/p111-line7-query-price/verify.py +python3 -B scripts/research_package.py --package research/p111-line7-query-price +``` + +Expected first line: `PASS_P111_LINE7_QUERY_PRICE delta_adds 54 dirty_visible 62 line_to_zero_move False NO_NEW_KAPPA`. + +The word SHA-256 is `e8e6e78ff7422275c38324499e1f33fb2ecd30de9503aef2b8f1ee80d8c4df8e`. +Failure controls inside the verifier: omitting the three partner corrections +changes an output, and the containment test rejects the line-to-zero move. + +## Open next questions + +1. Can a continuation whose 22 query receivers stay at `span(7)` until their + original final frames are restored beat `{1: 4, 8: 1}` after every restoration + copy is charged? The scalar cut does not record those final frames. +2. Is there a correction other than this triangular substitution that preserves + the 112 output forms with no extra rank-1 child and fewer than 230 ADDs? + +## Credit + +Word, centre seed and query formula: Rohan Arun, PR #1525, with the retained +PR1297 / PR1134 / PR1060 lineage in that package's NOTICE. The triangular +relation, the 230-versus-176 census, and the conditional `{1: 4, 8: 1}` to +`{1: 5, 8: 1}` bill are JoyboyBrian's, comment 19143427; that note labelled its +checker local-only. Frame containment is the test in PR1060 `model.py` +(`contained`). This replay and the support split were prepared by unpaidmoon +with substantial Cursor Grok assistance. Apache-2.0. diff --git a/research/p111-line7-query-price/SOURCES.json b/research/p111-line7-query-price/SOURCES.json new file mode 100644 index 0000000000..8f6aa74f1b --- /dev/null +++ b/research/p111-line7-query-price/SOURCES.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "research/p111-line7-query-price/inputs/word-base.json.gz", + "usage": "input", + "pin": "head:af24d3b04e9d93906ed3c5a6262972fecfe5388a:research/p111-line7-query-price/inputs/word-base.json.gz", + "git_blob": "eacf8c773cb50637f93a762342b3b5f0853fe29a", + "sha256": "e8e6e78ff7422275c38324499e1f33fb2ecd30de9503aef2b8f1ee80d8c4df8e" + }, + { + "path": "research/p111-line7-query-price/inputs/CENTRE-SEED.json", + "usage": "input", + "pin": "head:af24d3b04e9d93906ed3c5a6262972fecfe5388a:research/p111-line7-query-price/inputs/CENTRE-SEED.json", + "git_blob": "d5bea849fdde3bb43d38ff44d7b5a2c34e754954", + "sha256": "228e178662fc01895bbcd8472a52114d3a3d11ea8c7ae44d99cd1c8cf9e89147" + } + ] +} diff --git a/research/p111-line7-query-price/TASK.json b/research/p111-line7-query-price/TASK.json new file mode 100644 index 0000000000..30af320040 --- /dev/null +++ b/research/p111-line7-query-price/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "joint-query-controller", + "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "query demand", + "active mode", + "5720", + "5745", + "5747", + "caller" + ], + "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": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "refined", + "actual_scope": "For the exact PR #1525 puncture-0 / pivot-61 query at span(7), does the triangular zero-frame canonicalization (double column 61 and subtract it from columns 63, 31 and 256) deliver the original scatter outputs at a paid profile better than {1: 4, 8: 1}?", + "scope_change_reason": "The catalogue asks whether any changed query demand or caller can remove real work while satisfying native chronology and restoration. Comment 19143427 already stopped this one canonicalization with local-only evidence and left a broader successor open. This package narrows to that stopped candidate: it publishes a replay of the scatter identity and checks that PR1060 model.move rejects the span(7) to zero descent. It does not rerun the active-mode injection excluded by the card.", + "bottleneck_link": "A complete paid profile for this query has to price the frame that holds q and every scatter ADD. This triangular zero-frame continuation keeps the original scatter outputs and, once a rank-1 copy is granted in place of the rejected move, adds one rank-1 child plus 54 ADDs. It is not a saving under a positive rank-1 tariff.", + "budget_minutes": 60, + "stop_rule": "Stop once the pinned word shows that the triangular substitution preserves all 112 scatter outputs, hence all 62 dirty columns, and that presenting the span(7) query to the zero-frame cut requires one extra rank-1 child. Do not search other correction matrices, targets left at span(7), or outer admission in this session.", + "outcome": "negative-result", + "evidence": "research/p111-line7-query-price/verify.py recomputes q, the 176-entry cut, the 230-entry triangular correction, the +10/+22/+22 support split, equality of all 112 scatter forms, a nonzero witness for each of the 62 dirty columns, and the rejected span(7)-to-zero move. Both python3 -B and python3 -O -B print PASS_P111_LINE7_QUERY_PRICE. Section B, the Clifford compiler, Lean, and the selected frontier are not replayed. The 230-versus-176 census and the conditional profile bill were already stated in discussion comment 19143427.", + "author": "unpaidmoon", + "ai_assistance": "Prepared by unpaidmoon with substantial Cursor Grok assistance. No independent human review.", + "open_questions": [ + { + "question": "Can a continuation whose 22 query receivers stay at span(7) until their original final frames are restored beat {1: 4, 8: 1} after every restoration copy is charged?", + "why_it_matters": "The zero-frame route loses because the constructor cannot move span(7) down to the zero frame. Leaving the receivers on the line might avoid that rank-1 copy, but only if restoration of the original final frames does not cost more.", + "first_step": "Recover the original final owner frame of each of the 22 query receivers from the pinned word and price one legal descent from span(7) to that frame.", + "blocked_by": "The scalar cut records frame None and does not store those final frames." + }, + { + "question": "Is there a correction other than this triangular substitution that preserves the 112 output forms with no extra rank-1 child and fewer than 230 ADDs?", + "why_it_matters": "The triangular matrix is one exact continuation, not a proof that every output-preserving scatter costs 230 ADDs.", + "first_step": "Fix the four centre values at q in slot 61 and the three unchanged partners, and search integer combinations of those columns that match the 112 original output forms with fewer than 230 nonzeros.", + "blocked_by": "Any such matrix still has to present q at a frame the constructor can legally read. This session does not search that family." + } + ] +} diff --git a/research/p111-line7-query-price/VERIFY.json b/research/p111-line7-query-price/VERIFY.json new file mode 100644 index 0000000000..2b22b6f727 --- /dev/null +++ b/research/p111-line7-query-price/VERIFY.json @@ -0,0 +1,17 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p111-line7-query-price/inputs/word-base.json.gz", + "research/p111-line7-query-price/inputs/CENTRE-SEED.json" + ], + "commands": [ + { + "argv": ["{python}", "-B", "{package}/verify.py"], + "timeout_seconds": 60, + "checks": "Recomputes q, the 176-entry cut, the triangular 230-entry correction, the exact +10/+22/+22 support split, equality of all 112 output forms on 704 coordinates, visibility of all 62 dirty columns, illegality of the span(7) to zero move, and the strict one-child profile increase. Omitting the partner correction must change an output." + } + ] +} diff --git a/research/p111-line7-query-price/inputs/CENTRE-SEED.json b/research/p111-line7-query-price/inputs/CENTRE-SEED.json new file mode 100644 index 0000000000..d5bea849fd --- /dev/null +++ b/research/p111-line7-query-price/inputs/CENTRE-SEED.json @@ -0,0 +1,172 @@ +{ + "status": "PASS_SCOPED_NONNESTED_CENTRE_QUERY_NATIVE", + "puncture": 0, + "terms": [ + { + "center": 61, + "weight": "1/2", + "frame": [ + 256, + 128, + 64, + 32, + 16, + 8, + 5, + 3 + ] + }, + { + "center": 63, + "weight": "1/2", + "frame": [ + 256, + 128, + 64, + 32, + 17, + 9, + 4, + 2 + ] + }, + { + "center": 31, + "weight": "1/2", + "frame": [ + 256, + 128, + 65, + 33, + 17, + 9, + 4, + 2 + ] + }, + { + "center": 256, + "weight": "1/2", + "frame": [ + 256, + 128, + 65, + 33, + 16, + 8, + 5, + 3 + ] + } + ], + "query_frame": [ + 2, + 5, + 9, + 16, + 32, + 64, + 128, + 256 + ], + "transport_profile": { + "2": 4 + }, + "rank_mass": 8, + "omitted_source_coefficient": "2", + "dirty_columns": 62, + "dirty_coefficients": { + "239": "-1", + "225": "-1", + "237": "-1", + "224": "2", + "255": "-1", + "241": "-1", + "253": "-1", + "240": "1", + "242": "1", + "271": "-2", + "256": "1", + "261": "1", + "270": "1", + "351": "-3", + "340": "1", + "350": "1", + "336": "1", + "367": "-1", + "356": "1", + "366": "1", + "352": "1", + "383": "-1", + "379": "1", + "368": "1", + "399": "-2", + "388": "1", + "398": "1", + "395": "1", + "227": "1", + "283": "-1", + "287": "-2", + "280": "-1", + "272": "1", + "299": "-1", + "303": "-2", + "292": "1", + "302": "1", + "400": "1", + "403": "2", + "409": "1", + "402": "-1", + "411": "1", + "416": "1", + "419": "1", + "425": "1", + "418": "-1", + "421": "1", + "430": "1", + "417": "1", + "429": "1", + "243": "1", + "319": "-2", + "435": "1", + "441": "1", + "434": "-1", + "437": "1", + "446": "1", + "433": "1", + "445": "1", + "267": "-1", + "431": "-1", + "447": "-1" + }, + "fixtures": [ + { + "trial": 0, + "forward_and_inverse_transpose": true, + "streaming_peak_temporaries": 2, + "weighted_accumulations": 4, + "source_copies": 4, + "temporary_discards": 5 + }, + { + "trial": 1, + "forward_and_inverse_transpose": true, + "streaming_peak_temporaries": 2, + "weighted_accumulations": 4, + "source_copies": 4, + "temporary_discards": 5 + } + ], + "optimistic_moment": "0.999971277929646601478394497346102075481621", + "optimistic_profile": { + "1": 2340, + "4": 130, + "3": 414, + "2": 508, + "5": 80, + "8": 7, + "7": 1 + }, + "optimistic_idle": 14274, + "scope": "Four source-stable whole-stream copies at nonnested frame transitions. Exact signed Pauli/global phase checks and two dense Gaussian fixtures in each orientation. The omitted source must be zero and dirty response compensated. Two-stream peak includes query accumulator and one live converted centre copy. Storage, all-size native recursion, nonmonotone owner hosting, full scatter and exact recovery/precision/analytic transfer are unadmitted. Favorable moment grants incompatible deletion/endpoint/hosting credits, not a new bound." +} \ No newline at end of file diff --git a/research/p111-line7-query-price/inputs/word-base.json.gz b/research/p111-line7-query-price/inputs/word-base.json.gz new file mode 100644 index 0000000000..eacf8c773c Binary files /dev/null and b/research/p111-line7-query-price/inputs/word-base.json.gz differ diff --git a/research/p111-line7-query-price/verify.py b/research/p111-line7-query-price/verify.py new file mode 100644 index 0000000000..72c5ba62cd --- /dev/null +++ b/research/p111-line7-query-price/verify.py @@ -0,0 +1,279 @@ +#!/usr/bin/env python3 +"""Price the PR1525 line-span(7) query against its zero-frame scatter. + +No new kappa. The triangular correction preserves every original scatter +output, including all 62 dirty columns, and the constructor forbids moving +that query from span(7) down to the zero frame. +""" +import gzip +import hashlib +import json +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path + +ROOT = Path(__file__).resolve().parent +WORD_SHA = "e8e6e78ff7422275c38324499e1f33fb2ecd30de9503aef2b8f1ee80d8c4df8e" +SEED_SHA = "228e178662fc01895bbcd8472a52114d3a3d11ea8c7ae44d99cd1c8cf9e89147" +CENTRES_IN_QUERY = (61, 63, 31, 256) +PARTNERS = (63, 31, 256) + + +def require(condition, message): + if not condition: + raise AssertionError(message) + + +def basis(rows): + pivots = {} + for value in rows: + while value: + bit = value.bit_length() - 1 + if bit in pivots: + value ^= pivots[bit] + else: + pivots[bit] = value + break + for bit in sorted(pivots): + for other in pivots: + if other > bit and (pivots[other] >> bit) & 1: + pivots[other] ^= pivots[bit] + return tuple(pivots[bit] for bit in sorted(pivots)) + + +def contained(left, right): + """Span(left) is contained in span(right). Same test as PR1060 model.py.""" + return len(basis(list(left) + list(right))) == len(basis(list(right))) + + +def add_row(dst, scale, src): + for index, value in src.items(): + total = dst.get(index, Q(0)) + scale * value + if total == 0: + dst.pop(index, None) + else: + dst[index] = total + + +def apply_op(rows, event): + if event[0] == "add": + add_row(rows[event[1]], Q(event[3], event[4]), rows[event[2]]) + else: + require(event[0] == "scale", event[0]) + rows[event[1]] = {i: value * Q(event[2], event[3]) for i, value in rows[event[1]].items()} + + +def scatter_matrix(word): + order = word["centers"] + require(order == [60, 61, 63, 224, 31, 240, 23, 256], order) + index = {centre: slot for slot, centre in enumerate(order)} + matrix = [[Q(0) for _ in order] for _ in range(112)] + receivers = {centre: [] for centre in order} + for event in word["cut"]: + require(event[0] == "add" and event[5] is None, event) + target = event[1] - 112 + require(0 <= target < 112, event[1]) + slot = index[event[2]] + matrix[target][slot] += Q(event[3], event[4]) + receivers[event[2]].append(event[1]) + return matrix, receivers + + +def column_nnz(matrix, slot): + return sum(1 for row in matrix if row[slot]) + + +def triangular(matrix, index): + """Substitute q = (c61 + c63 + c31 + c256) / 2 for the c61 readout.""" + query = index[61] + corrected = [] + for row in matrix: + new_row = row[:] + original = row[query] + new_row[query] = 2 * original + for partner in PARTNERS: + new_row[index[partner]] = row[index[partner]] - original + corrected.append(new_row) + return corrected + + +def support_delta(matrix, index, partner): + query = index[61] + slot = index[partner] + both = cancel = unequal = only_query = only_partner = 0 + for row in matrix: + left, right = row[query], row[slot] + if left and right: + both += 1 + if right - left == 0: + cancel += 1 + else: + unequal += 1 + elif left: + only_query += 1 + elif right: + only_partner += 1 + old = column_nnz(matrix, slot) + new = sum(1 for row in matrix if row[slot] - row[query]) + return { + "partner": partner, + "old_nnz": old, + "new_nnz": new, + "delta": new - old, + "overlap": both, + "cancellations": cancel, + "unequal_overlap": unequal, + "only_query": only_query, + "only_partner": only_partner, + } + + +def combine(matrix, vectors): + outputs = [] + for row in matrix: + acc = {} + for slot, weight in enumerate(row): + if weight: + add_row(acc, weight, vectors[slot]) + outputs.append(acc) + return outputs + + +def endpoint_line(frame): + return next( + mask + for mask in range(1, 512) + if all((mask & vector).bit_count() % 2 == 0 for vector in frame) + ) + + +def main(): + word_bytes = (ROOT / "inputs/word-base.json.gz").read_bytes() + seed_bytes = (ROOT / "inputs/CENTRE-SEED.json").read_bytes() + require(hashlib.sha256(word_bytes).hexdigest() == WORD_SHA, "word sha") + require(hashlib.sha256(seed_bytes).hexdigest() == SEED_SHA, "seed sha") + word = json.loads(gzip.decompress(word_bytes)) + seed = json.loads(seed_bytes) + require(seed["puncture"] == 0, seed["puncture"]) + require(seed["dirty_columns"] == 62, seed["dirty_columns"]) + require([item["center"] for item in seed["terms"]] == list(CENTRES_IN_QUERY), seed["terms"]) + require(all(item["weight"] == "1/2" for item in seed["terms"]), seed["terms"]) + + roles = 224 + word["report"]["R"] + require(roles == 704, roles) + rows = [{i: Q(1)} for i in range(roles)] + for event in word["precondition"] + word["A"]: + apply_op(rows, event) + + query = {} + for item in seed["terms"]: + add_row(query, Q(item["weight"]), rows[item["center"]]) + dirty = {i: value for i, value in query.items() if i >= 112} + require({str(i): str(value) for i, value in dirty.items()} == seed["dirty_coefficients"], "dirty census") + require(len(dirty) == 62, len(dirty)) + beta = seed["puncture"] + for source in range(112): + if source == beta: + continue + expected = Q(sum(a * b for a, b in zip(word["root_lines"][beta], word["root_lines"][source])), 2) + require(query.get(source, Q(0)) == expected, source) + + line = endpoint_line(seed["terms"][0]["frame"]) + require(line == 7 and basis((line,)) == (7,), line) + require(contained((7,), ()) is False, "span(7) is not contained in the zero frame") + require(contained((), (7,)) is True, "the zero frame is contained in span(7)") + + matrix, receivers = scatter_matrix(word) + index = {centre: slot for slot, centre in enumerate(word["centers"])} + require(all(len(receivers[centre]) == 22 and len(set(receivers[centre])) == 22 for centre in word["centers"]), "22 receivers") + require(sum(column_nnz(matrix, slot) for slot in range(8)) == 176, "S nnz") + for slot in range(8): + weights = Counter(str(row[slot]) for row in matrix if row[slot]) + require(set(weights) <= {"1/4", "-1/4"}, weights) + require(sum(weights.values()) == 22, weights) + + deltas = [support_delta(matrix, index, partner) for partner in PARTNERS] + require([item["delta"] for item in deltas] == [10, 22, 22], deltas) + require(sum(item["delta"] for item in deltas) == 54, deltas) + require(deltas[0]["cancellations"] == 4 and deltas[0]["overlap"] == 8, deltas[0]) + require(deltas[1]["overlap"] == 0 and deltas[2]["overlap"] == 0, deltas[1:]) + + corrected = triangular(matrix, index) + corrected_nnz = sum(1 for row in corrected for value in row if value) + require(corrected_nnz == 230, corrected_nnz) + require(column_nnz(corrected, index[61]) == 22, "query column") + doubled = Counter(str(row[index[61]]) for row in corrected if row[index[61]]) + require(doubled == Counter({"-1/2": 3, "1/2": 19}), doubled) + + old_vectors = [rows[centre] for centre in word["centers"]] + new_vectors = [query if centre == 61 else rows[centre] for centre in word["centers"]] + old_outputs = combine(matrix, old_vectors) + new_outputs = combine(corrected, new_vectors) + require(old_outputs == new_outputs, "triangular image differs from the original scatter") + + # The same identity fails if the partner correction is omitted. + uncorrected = [row[:] for row in matrix] + for row in uncorrected: + row[index[61]] = 2 * row[index[61]] + require(combine(uncorrected, new_vectors) != old_outputs, "missing partner correction should be visible") + + witnesses = {} + for column in sorted(dirty): + hits = [] + for target, form in enumerate(old_outputs): + coefficient = form.get(column, Q(0)) + if coefficient: + hits.append((112 + target, str(coefficient))) + break + require(len(hits) == 1, column) + witnesses[str(column)] = {"output_row": hits[0][0], "coefficient": hits[0][1]} + require(len(witnesses) == 62, len(witnesses)) + + # One shared rank-1 copy takes span(7) to a zero-frame register. The + # comparator profile is the four already-paid rank-1 centre moves plus the + # rank-8 copy. The extra child is exactly one rank 1. + old_profile = {1: 4, 8: 1} + new_profile = {1: 5, 8: 1} + require(new_profile[1] - old_profile[1] == 1 and new_profile[8] == old_profile[8], "profile delta") + # For every tariff that sends rank 1 to a positive value and ignores no + # other change, the new multiset costs exactly that positive value more. + for exponent in range(1, 9): + old_mass = 4 * (1 ** exponent) + 8 ** exponent + new_mass = 5 * (1 ** exponent) + 8 ** exponent + require(new_mass - old_mass == 1, exponent) + + receipt = { + "status": "PASS_P111_LINE7_QUERY_PRICE", + "word_sha256": WORD_SHA, + "seed_sha256": SEED_SHA, + "source_pr": 1525, + "source_head": "90d39a5603c7fbfd8d8d957e9732d9b6ebd6317f", + "endpoint_line": [7], + "move_line_to_zero_legal": False, + "move_zero_to_line_legal": True, + "scatter_nnz": 176, + "triangular_nnz": 230, + "scatter_add_delta": 54, + "partner_deltas": deltas, + "query_receivers": 22, + "dirty_columns": 62, + "dirty_columns_visible_in_original_outputs": 62, + "dirty_witnesses": witnesses, + "comparator_profile": old_profile, + "zero_frame_copy_profile": new_profile, + "profile_delta": {1: 1}, + "no_new_kappa": True, + } + print( + receipt["status"], + "delta_adds", receipt["scatter_add_delta"], + "dirty_visible", receipt["dirty_columns_visible_in_original_outputs"], + "line_to_zero_move", receipt["move_line_to_zero_legal"], + "NO_NEW_KAPPA", + flush=True, + ) + return receipt + + +if __name__ == "__main__": + main()