From a8c75dd7c964855cc9b03c210575be27c65467e4 Mon Sep 17 00:00:00 2001 From: Chris R Date: Mon, 19 Oct 2026 22:17:51 +1100 Subject: [PATCH] Bind first selected gauge44 provider and rule out fixed QQ16 role conjugacy --- research/qq16-provider-binding/README.md | 156 ++++++++++++ research/qq16-provider-binding/RESULT.json | 69 ++++++ research/qq16-provider-binding/SOURCES.json | 48 ++++ research/qq16-provider-binding/TASK.json | 85 +++++++ research/qq16-provider-binding/VERIFY.json | 40 ++++ research/qq16-provider-binding/test_verify.py | 60 +++++ research/qq16-provider-binding/verify.py | 224 ++++++++++++++++++ 7 files changed, 682 insertions(+) create mode 100644 research/qq16-provider-binding/README.md create mode 100644 research/qq16-provider-binding/RESULT.json create mode 100644 research/qq16-provider-binding/SOURCES.json create mode 100644 research/qq16-provider-binding/TASK.json create mode 100644 research/qq16-provider-binding/VERIFY.json create mode 100644 research/qq16-provider-binding/test_verify.py create mode 100644 research/qq16-provider-binding/verify.py diff --git a/research/qq16-provider-binding/README.md b/research/qq16-provider-binding/README.md new file mode 100644 index 0000000000..09db1cf29e --- /dev/null +++ b/research/qq16-provider-binding/README.md @@ -0,0 +1,156 @@ +# First selected gauge44 provider versus corrected QQ16 F0 + +The literal first selected provider is not corrected QQ16 F0. At the +constant-character, common-cover specialization its data map is +`G(x,y)=(x,y+x)`. The corrected QQ16 map Q has trace 120, whereas G has +trace 224. Including all 480 arbitrary persistent helpers gives traces +600 and 704. Thus **no fixed invertible role change conjugates these two +maps**, even if that role change mixes the data and all borrowed helpers. +The first direct output mismatch is already X_0, before any B1 decoder cut. + +This is a scoped negative result and exact local invoice, not a new supplier, +an unrestricted impossibility theorem, or a selected-frontier change. + +## Actual source and boundary + +The base is `20ecf2891d80b5acf18d980b2164fb44ea7faa90`. The verifier binds +`calls[0]` in the pinned selected archive's +`t16/global/hosted/GLOBAL-TEMPLATE.json.gz`: time 0, replica 0, stage 0, +provider gauge44, orientation forward. Its forward program hash is +`071ecdacc0bb3ac16046aad4119ed551a945cb0ed6c57002a548a3e2232503d8`. +The embedded provider program equals the separate selected gauge44 program. +This selects actual source coefficients, not a similarly named abstract shear. + +There are 704 distinct physical owner IDs: L_0,...,L_111 are X, L_112,..., +L_223 are Y, and L_224,...,L_703 are borrowed helpers. The first 224 IDs are +0,...,223 and their owner descriptors are `[1,0,p mod 112]`. Each remaining +helper retains its literal owner descriptor. The eight C registers are +separate owned private values. The source `CANONICAL-WORD.json.gz` supplies +all 704 input and output frame IDs; the receipt pins both full frame arrays +and the full owner list by canonical JSON SHA256. Frame IDs are not treated +as equal merely because their contents agree at the specialization. + +The inherited [bridge convention](../joint-query/evidence/BRIDGE-REVIEW.md) +fixes the constant Fourier character: each native line is +`C_a=((1+i)I+(1-i)T_a)/2`, hence C_a(1)=1; translations and signed products +also fix it. Cover permutations fix arrays constant over covers. The +common-chart scalar specialization therefore supplies a necessary test for +role-only correspondences that preserve this subspace. The verifier executes +all scalar instructions in their actual order and specializes the declared +native events to identity. This does not reverify native child kernels or +the global hosting theorem. + +All 712 independent formal inputs are retained during replay. Both outputs +have identity rows on all 480 helpers and zero rows on all eight private +values. Data outputs are independent of initial helper and private values. +Native helper frames can change; identity here means their specialized +logical content. The full 712-dimensional maps discard private inputs and +are not asserted invertible. + +## Exact first mismatch and mapping class + +Let A and T be the eight selected sets in the QQ16 packet, U their +96-port complement, R its actual 8-by-112 centre matrix, and K=R^T/4. +The independent formula check gives + +``` +f = R x +X'_U = x_U - K_U f +X'_A = K_A R_T x_T +X'_T = K_T f +Y'_U = y_U + X'_U +Y'_S = y_S + x_S - X'_S (S = A union T) +``` + +In particular, selected gauge44 returns `X'_0=x_0`, whereas QQ16 returns +`X'_0=(x_76-x_81+x_87+x_92)/2`. Input x_0=1 with every other data and helper +symbol zero is already decisive. + +The excluded class consists of a **single fixed invertible matrix P on the +704 persistent specialized roles**, used at both entrance and exit. It +would require `P^-1 G P=Q`; trace invariance contradicts 704 != 600. +This includes permutations, signed/diagonal role gauges, and arbitrary +invertible constant mixing of those roles. A physical correspondence whose +restriction is such an invertible P also fails this necessary test. +Different entrance and exit encodings, a noninvertible relation, a change +of native representation that does not preserve the tested subspace, and +paid adapters are outside this class. No claim of a complete program +bisimulation or all-purpose representation obstruction is made. + +## Paid repair obligation and local invoice + +The exact rank of Q-G on the 224 data roles is 24. A proof of its kernel is +short: equality requires x_S=0 from the selected Y equations, then +R_U x_U=0 from the U equations. Since R_U K_U=12I, that kernel has dimension +96-8=88 in x and all 112 dimensions in y. Thus its dimension is 200. +The verifier also establishes rank 24 directly by rational elimination and +checks that Q is invertible. Any post-adapter E with E Q=G must consequently +have `rank(E-I)=24`. A product of rank-one elementary updates requires at +least 24 such factors, by rank subadditivity. This is an algebraic lower +bound, not a full physical invoice or an adapter implementation. + +| Exact local item | Selected gauge44 | Corrected QQ16 F0 | +| --- | ---: | ---: | +| Real scalar primitive allowance | 198766 | 211210 | +| Extra scalar allowance before any repair | 0 | 12444 | +| Source centre children | eight H8 | zero | +| Added selected native lines | zero | eight H1 | +| Borrowed helper outputs | 480 returned | 480 returned | +| Owned private outputs | eight zero | eight zero | + +Persistent climb/adapter/residual-adapter event lists are compared exactly +and are unchanged. The scalar allowances count the full literal words, +including private clearing and dirty-helper correction. The native difference +`-8 H8 + 8 H1` is conditional on a valid replacement: the missing boundary +repair cannot be omitted from a construction budget. No native saving, +physical repair cost, or global advantage is certified here. + +The requested matched boundary through B1 therefore stops at F0. Carrying +an unmatched source state into a B1 decoder would assume the correspondence +this check disproves. A new round needs either paid distinct boundary maps +or an explicitly broader correspondence and its physical price. + +## Reproduction and validation + +``` +python3 -I -O -Werror -B research/qq16-provider-binding/verify.py --controls +python3 -B scripts/research_package.py --package research/qq16-provider-binding +``` + +Every live input is hashed before parsing; no predecessor Python module is +imported. Exact source and output hashes are in SOURCES.json and RESULT.json. +The normal replay is read-only; `--write` creates only this +package's receipt when absent and refuses to overwrite an existing receipt. The controls independently mutate a selected-source +coefficient and a QQ16 wrapper coefficient and require both to fail. +The registered test also verifies a Git-free source export and rejects a +changed source hash and a changed receipt, including a Boolean/integer type +substitution. No complete selected cold replay or formal theorem proof is +claimed or needed for this isolated obstruction package. + +## Attribution and overlap + +The selected physical archive, original corrected joint-query construction, +and its scalar/native/bridge reviews are retained unchanged and credited to +their original contributors. This extends the selected-caller missing-binding +audit (#3976) by evaluating the actual first provider and supplying a precise +mapping-class obstruction. It does not repeat the query decoder optimization +in #4003 or the zero-extra-owned-register decoder of #4015 +(`0fff81d8997cef646538bcd4f60d7d455cf93b8e`). The fixed-104-owner, +one-common-query-frame formal-moment obstruction in tekuuu's #4030 +(`12df564caa8918453de658fe49601de6a9227017`) concerns a different consumer +class; no result from that pending package is assumed here. + +Chris R / Clear1nsight with substantial OpenAI Codex assistance supplied this package. +New code and prose are Apache-2.0. No independent human review is claimed. + +## Open next questions + +1. Can distinct, paid entrance and exit maps bind QQ16 F0 to this exact + selected call? Start by constructing E=GQ^-1 in the specialized algebra, + then bind its native frames, owner routes, scratch returns and full cost. + The rank-24 obligation and +12444 scalar delta prevent treating it as free; + no affordable physical lift is yet available. +2. Can an end-to-end source substitution change the first provider and its + caller contract instead? Start from this literal F0 mismatch and name the + exact downstream selected work replaced. A first B1 consumer match and + complete family budget are prerequisites for another decoder round. diff --git a/research/qq16-provider-binding/RESULT.json b/research/qq16-provider-binding/RESULT.json new file mode 100644 index 0000000000..71bc31b468 --- /dev/null +++ b/research/qq16-provider-binding/RESULT.json @@ -0,0 +1,69 @@ +{ + "QQ16_added_native_lines": 8, + "QQ16_scalar_real_primitives": 211210, + "arbitrary_helpers_returned": 480, + "archive_member_sha256": { + "t16/global/base/providers/gauge44/CANONICAL-WORD.json.gz": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219", + "t16/global/base/providers/gauge44/LOCAL-PROGRAMS.json.gz": "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a", + "t16/global/hosted/GLOBAL-TEMPLATE.json.gz": "73f47a1e60b1e4ea66dbca9a497c411c8e6adc7984e276a437a10a9a7a13b47a" + }, + "data_difference_rank": 24, + "data_traces": [ + 224, + 120 + ], + "first_mismatch": { + "QQ16": "(X_76-X_81+X_87+X_92)/2", + "output": "X_0", + "selected": "X_0" + }, + "independent_input_symbols": 712, + "minimum_rank_one_factors_for_post_adapter": 24, + "persistent_traces": [ + 704, + 600 + ], + "post_adapter_rank_minus_identity": 24, + "private_outputs_zero": 8, + "scalar_delta": 12444, + "schema_version": 1, + "scope": "Exact first source call and constant-character common-cover specialization; fixed invertible role conjugacy only. No physical adapter, B1 match, or supplier is constructed.", + "source_call": { + "local_program_sha256": "071ecdacc0bb3ac16046aad4119ed551a945cb0ed6c57002a548a3e2232503d8", + "orientation": "forward", + "pair": 0, + "provider_id": "gauge44", + "replica": 0, + "stage": 0, + "time": 0, + "window": { + "local_axes": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8 + ], + "prefix_axes": [] + } + }, + "source_center_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + "source_final_frames_sha256": "feef65df95af9ae193a9988edb5a7e9d3c607c8e4b7ffab3f3ef610dc184f1be", + "source_owner_list_sha256": "b0a39b7a3e5f5f4b7ab8c38d87de9ab66ec1499b3c0f3e50090d08c3dcfe62b3", + "source_scalar_real_primitives": 198766, + "source_start_frames_sha256": "bf49fb9bd01d22ae305cd0909e13409c6ffe0290fc1c2a35928e2c6162758f54", + "status": "scoped obstruction; no frontier change" +} diff --git a/research/qq16-provider-binding/SOURCES.json b/research/qq16-provider-binding/SOURCES.json new file mode 100644 index 0000000000..c541badd1c --- /dev/null +++ b/research/qq16-provider-binding/SOURCES.json @@ -0,0 +1,48 @@ +{ + "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" + }, + { + "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" + }, + { + "path": "research/joint-query/evidence/BRIDGE-REVIEW.md", + "usage": "input", + "git_blob": "86139908c418235588045324f0873de6ac9f9707", + "sha256": "d01b5f4959f7c91f835496d050dfae3eeab9dee2f581571c316a42571eaa1cd3" + }, + { + "path": "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "usage": "input", + "git_blob": "a6805c58f23132f9420efebf90f5b7e863c2e179", + "sha256": "9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75" + }, + { + "path": "research/joint-query/evidence/SCALAR-REVIEW.md", + "usage": "input", + "git_blob": "e060789dfa3deafc49002b9f127de89800578bd1", + "sha256": "aa7b9f74430b56c42e1099029a501a9b6be9ab56b81bfdc681e4c2e6ff5bc97d" + } + ] +} diff --git a/research/qq16-provider-binding/TASK.json b/research/qq16-provider-binding/TASK.json new file mode 100644 index 0000000000..27e43636e2 --- /dev/null +++ b/research/qq16-provider-binding/TASK.json @@ -0,0 +1,85 @@ +{ + "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 the literal first selected gauge44 forward provider to corrected QQ16 F0 and test fixed invertible persistent-role conjugacy.", + "scope_change_reason": "The actual source-provider match is required before importing a B1 decoder cut; this tests that prerequisite directly.", + "bottleneck_link": "A decoder budget cannot replace source work until the actual F0 boundary and its repair price are bound.", + "budget_minutes": 60, + "stop_rule": "Stop at the first exact mismatch or scoped correspondence obstruction; do not optimize an unbound decoder.", + "outcome": "negative-result", + "evidence": "RESULT.json; verify.py; exact 712-symbol replay and rank/trace proof in README.md", + "author": "Chris R / Clear1nsight with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for analysis, code, and prose; no independent human review claimed.", + "open_questions": [ + { + "question": "Can distinct paid boundary maps bind this literal source provider?", + "why_it_matters": "A valid source substitution needs matching boundaries.", + "first_step": "Construct GQ^-1 at the specialization and price a native lift.", + "blocked_by": "No native frame/owner/cleanup implementation or favorable full invoice." + }, + { + "question": "Can an end-to-end caller change replace selected first-provider work?", + "why_it_matters": "A different caller may permit a broader correspondence.", + "first_step": "Name the exact downstream work replaced and bind the first B1 input.", + "blocked_by": "No matched B1 boundary or family-level budget." + } + ] +} diff --git a/research/qq16-provider-binding/VERIFY.json b/research/qq16-provider-binding/VERIFY.json new file mode 100644 index 0000000000..f5b60f5958 --- /dev/null +++ b/research/qq16-provider-binding/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1042-audit/selected-replay.tar.gz", + "research/joint-query/certificate.json.gz", + "research/joint-query/evidence/BRIDGE-REVIEW.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "research/joint-query/evidence/SCALAR-REVIEW.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py", + "--controls" + ], + "timeout_seconds": 120, + "checks": "Pinned literal source, all712 symbols, independent QQ16 formula, exact trace/rank and coefficient mutation controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Git-free read-only export replay and source/receipt/type rejection controls." + } + ] +} diff --git a/research/qq16-provider-binding/test_verify.py b/research/qq16-provider-binding/test_verify.py new file mode 100644 index 0000000000..d4bda10c88 --- /dev/null +++ b/research/qq16-provider-binding/test_verify.py @@ -0,0 +1,60 @@ +"""Bounded export and mutation controls; no Git and no emitter imports.""" +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent + +def need(ok, message): + if not ok: + raise ValueError(message) + +def run(root, optimized, ok, reason=''): + command = [sys.executable, '-I'] + (['-O'] if optimized else []) + ['-Werror','-B',str(root/'research/qq16-provider-binding/verify.py')] + result = subprocess.run(command,cwd=root,capture_output=True,text=True,timeout=80) + need((result.returncode==0)==ok, result.stdout+result.stderr) + if reason: + need(reason in result.stderr,'wrong rejection: '+result.stderr) + +with tempfile.TemporaryDirectory(prefix='qq16-provider-binding-') as name: + export = Path(name) + package = export/'research/qq16-provider-binding' + package.mkdir(parents=True) + for src in HERE.iterdir(): + if src.is_file(): + shutil.copyfile(src,package/src.name) + manifest = json.loads((HERE/'VERIFY.json').read_text()) + for rel in manifest['inputs']: + dest = export/rel + dest.parent.mkdir(parents=True,exist_ok=True) + shutil.copyfile(ROOT/rel,dest) + need(not (export/'.git').exists(),'Git-free export') + files = list(export.rglob('*')) + hashes = {str(p.relative_to(export)):hashlib.sha256(p.read_bytes()).hexdigest() for p in files if p.is_file()} + try: + for p in files: + p.chmod(0o555 if p.is_dir() else 0o444) + run(export,False,True) + run(export,True,True) + overwrite = subprocess.run([sys.executable,'-I','-O','-B',str(package/'verify.py'),'--write'],cwd=export,capture_output=True,text=True,timeout=5) + need(overwrite.returncode != 0 and 'refusing to overwrite existing RESULT.json' in overwrite.stderr,'existing receipt overwrite accepted') + need(hashes=={str(p.relative_to(export)):hashlib.sha256(p.read_bytes()).hexdigest() for p in export.rglob('*') if p.is_file()},'read-only export changed') + finally: + for p in files: + p.chmod(0o755 if p.is_dir() else 0o644) + receipt = package/'RESULT.json' + original = receipt.read_bytes() + changed = json.loads(original) + changed['schema_version'] = True + receipt.write_text(json.dumps(changed)) + run(export,True,False,'complete typed receipt') + receipt.write_bytes(original) + packet = export/'research/joint-query/certificate.json.gz' + packet.write_bytes(packet.read_bytes()+b'bad') + run(export,True,False,'source SHA256') +print('PASS Git-free read-only normal/optimized export and source/typed-receipt controls') diff --git a/research/qq16-provider-binding/verify.py b/research/qq16-provider-binding/verify.py new file mode 100644 index 0000000000..e91e378cf7 --- /dev/null +++ b/research/qq16-provider-binding/verify.py @@ -0,0 +1,224 @@ +"""Exact pinned first-provider specialization; standard library only. + +Apache-2.0. Chris R / Clear1nsight with substantial OpenAI Codex assistance. +No source emitter or predecessor verifier is executed. +""" +import argparse +from collections import Counter +from copy import deepcopy +from fractions import Fraction as F +import gzip +import hashlib +import json +from pathlib import Path +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +ARCHIVE = 'research/community-frontier1042-audit/selected-replay.tar.gz' +PACKET = 'research/joint-query/certificate.json.gz' +PREFIX = 't16/global/base/providers/gauge44/' + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def digest(data): + return hashlib.sha256(data).hexdigest() + + +def canon(obj): + return json.dumps(obj, sort_keys=True, separators=(',', ':')).encode() + + +def add(a, b, c=F(1)): + out = a.copy() + for j, v in b.items(): + out[j] = out.get(j, F(0)) + c*v + if not out[j]: + del out[j] + return out + + +def rank(rows): + pivots = {} + for original in rows: + row = original.copy() + while row: + j = min(row) + if j not in pivots: + c = row[j] + pivots[j] = {k: v/c for k, v in row.items()} + break + row = add(row, pivots[j], -row[j]) + return len(pivots) + + +def register(token): + kind, i = token + need(kind in ('L', 'C') and type(i) is int and 0 <= i < (704 if kind == 'L' else 8), 'register namespace') + return i + (704 if kind == 'C' else 0) + + +def replay(events): + # All 712 symbols, including arbitrary incoming private values. Their + # final zero rows prove independence from those discarded private inputs. + rows = [{i: F(1)} for i in range(712)] + for event in events: + kind = event[0] + if kind != 'scalar': + need(kind in ('climb', 'center', 'phase', 'adapter', 'residual_adapter', 'native_line'), 'unknown native event') + # Constant-character/common-cover specialization. The inherited + # operator convention fixes that character, including all phases. + continue + gate = event[1] + op, target = gate[:2] + at = register(target) + if op == 'clear': + need(at >= 704, 'only private cells may be cleared') + rows[at] = {} + elif op == 'scale': + c = F(gate[2], gate[3]) + need(c != 0, 'invertible scalar scale') + rows[at] = {j: c*v for j, v in rows[at].items()} + else: + need(op in ('copy', 'add'), 'known scalar gate') + source = register(gate[2]) + need(at != source, 'distinct scalar operands') + rows[at] = rows[source].copy() if op == 'copy' else add(rows[at], rows[source], F(gate[3], gate[4])) + return rows + + +def expanded(packet): + out = [] + for event in packet['programs']['F_0']: + if event[0] == 'retained_core': + need(event[1:3] == ['forward', 0], 'F0 forward retained core') + out.extend(packet['core_words']['forward']) + else: + need(event[0] in ('cover_sweep', 'private_sweep'), 'known F0 wrapper') + out.extend(event[2]) + return out + + +def scalar_cost(events): + total = 0 + for event in events: + if event[0] != 'scalar': + continue + gate = event[1] + if gate[0] in ('clear', 'copy'): + total += 2 + continue + c = F(gate[3], gate[4]) if gate[0] == 'add' else F(gate[2], gate[3]) + a, b = abs(c.numerator), c.denominator + need(a > 0 and b & (b-1) == 0, 'nonzero dyadic scalar') + if gate[0] == 'add': + total += 2*(2+a.bit_length()+a.bit_count()+b.bit_length()-1) + else: + need(a & (a-1) == 0, 'signed power-of-two scale') + total += 2*(abs(a.bit_length()-b.bit_length())+(c < 0)) + return total + + +def validate(source, packet): + g, q = replay(source), replay(expanded(packet)) + basis = [{i: F(1)} for i in range(712)] + expected = basis[:112]+[add(basis[112+i], basis[i]) for i in range(112)]+basis[224:704]+[{} for _ in range(8)] + need(g == expected, 'selected gauge44 is the unit forward shear at specialization') + need(q[224:704] == basis[224:704] and q[704:] == [{} for _ in range(8)], 'QQ16 restores all helpers and private outputs') + need(all(j < 224 for row in q[:224] for j in row), 'data independent of helper/private inputs') + r = [{int(j): F(v) for j,v in row.items()} for row in packet['R_rows']] + k = [{int(j): F(v) for j,v in row.items()} for row in packet['K_rows']] + A, T, U = (packet[key] for key in ('A_ports','T_ports','U_ports')) + need(A == [0,7,20,27,36,46,57,111] and T == [21,37,47,76,81,87,92,110], 'selected role sets') + need(sorted(A+T+U) == list(range(112)), 'partition') + ru_ku = [{j: sum(row.get(p,0)*k[p].get(j,0) for p in U) for j in range(8)} for row in r] + need(ru_ku == [{j:F(12 if i==j else 0) for j in range(8)} for i in range(8)], 'R_U K_U = 12 I') + def combination(row, values): + out = {} + for j,v in row.items(): + out = add(out, values[j], v) + return out + x, y = basis[:112], basis[112:224] + f = [combination(row, x) for row in r] + rt = [combination({j:v for j,v in row.items() if j in T}, x) for row in r] + kf, kt = ([combination(row, vals) for row in k] for vals in (f, rt)) + xx = [add(x[p], kf[p], -1) if p in U else kt[p] if p in A else kf[p] for p in range(112)] + yy = [add(y[p], xx[p]) if p in U else add(add(y[p], x[p]),xx[p],-1) for p in range(112)] + need(q[:224] == xx+yy, 'literal QQ16 equals independent source-matrix formula') + need(rank(q[:224]) == 224, 'QQ16 data map invertible') + delta_rank = rank([add(a,b,-1) for a,b in zip(q[:224],g[:224])]) + traces = [sum(rows[i].get(i,0) for i in range(704)) for rows in (g,q)] + need(delta_rank == 24 and traces == [704,600], 'exact conjugacy obstruction') + need(q[0] == {76:F(1,2),81:F(-1,2),87:F(1,2),92:F(1,2)} and g[0] == {0:F(1)}, 'first direct row mismatch') + return {'data_traces': [224,120], 'persistent_traces': list(map(int,traces)), 'first_mismatch': {'output':'X_0','selected':'X_0','QQ16':'(X_76-X_81+X_87+X_92)/2'}, 'data_difference_rank':delta_rank, 'post_adapter_rank_minus_identity':delta_rank, 'minimum_rank_one_factors_for_post_adapter':delta_rank, 'independent_input_symbols':712, 'arbitrary_helpers_returned':480, 'private_outputs_zero':8, 'source_scalar_real_primitives':scalar_cost(source), 'QQ16_scalar_real_primitives':scalar_cost(expanded(packet)), 'source_center_ranks':[e[4] for e in source if e[0]=='center'], 'QQ16_added_native_lines':sum(e[0]=='native_line' for e in expanded(packet))} + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--write', action='store_true') + parser.add_argument('--controls', action='store_true') + args = parser.parse_args() + if args.write: + need(not (HERE/'RESULT.json').exists(), 'refusing to overwrite existing RESULT.json') + pins = json.loads((HERE/'SOURCES.json').read_text()) + for item in pins['files']: + if item['usage'] == 'input': + need(digest((ROOT/item['path']).read_bytes()) == item['sha256'], 'source SHA256: '+item['path']) + member_hashes = {} + with tarfile.open(ROOT/ARCHIVE,'r:gz') as archive: + def member(name): + entries = [x for x in archive.getmembers() if x.name == name] + need(len(entries)==1 and entries[0].isfile(), 'unique regular source member') + payload = archive.extractfile(entries[0]).read() + member_hashes[name] = digest(payload) + return json.loads(gzip.decompress(payload)) + template = member('t16/global/hosted/GLOBAL-TEMPLATE.json.gz') + programs = member(PREFIX+'LOCAL-PROGRAMS.json.gz') + word = member(PREFIX+'CANONICAL-WORD.json.gz') + packet = json.loads(gzip.decompress((ROOT/PACKET).read_bytes())) + call = template['calls'][0] + need((call['provider_id'],call['orientation'],call['replica'],call['stage'],call['time']) == ('gauge44','forward',0,0,0), 'literal first source call') + need(template['local_providers']['gauge44']['local_programs'] == programs, 'embedded selected provider bytes') + need(digest(canon(programs['forward'])) == call['local_program_sha256'], 'literal forward program hash') + need(len(call['owners']) == 704 and len(set(owner[0] for owner in call['owners'])) == 704, '704 distinct physical owners') + need(call['owners'][:224] == [[p,[1,0,p%112]] for p in range(224)], 'first data role owners') + need(len(word['start']) == len(word['final']) == 704, '704 source frame entries') + native = ('climb', 'adapter', 'residual_adapter') + need([e for e in programs['forward'] if e[0] in native] == [e for e in packet['core_words']['forward'] if e[0] in native], 'unchanged persistent native events') + receipt = validate(programs['forward'],packet) + receipt.update({'schema_version':1,'scope':'Exact first source call and constant-character common-cover specialization; fixed invertible role conjugacy only. No physical adapter, B1 match, or supplier is constructed.', 'source_call':{k:v for k,v in call.items() if k!='owners'},'source_owner_list_sha256':digest(canon(call['owners'])),'source_start_frames_sha256':digest(canon(word['start'])),'source_final_frames_sha256':digest(canon(word['final'])),'archive_member_sha256':member_hashes,'scalar_delta':12444,'status':'scoped obstruction; no frontier change'}) + need(receipt['QQ16_scalar_real_primitives']-receipt['source_scalar_real_primitives']==receipt['scalar_delta'], 'complete scalar delta') + if args.controls: + bad = deepcopy(programs['forward']) + first = next(e for e in bad if e[0]=='scalar' and e[1][0]=='add') + first[1][3] *= -1 + try: + validate(bad,packet) + except ValueError: + pass + else: + raise ValueError('source coefficient mutation accepted') + badp = deepcopy(packet) + first = next(e for e in badp['programs']['F_0'][1][2] if e[0]=='scalar') + first[1][3] *= -1 + try: + validate(programs['forward'],badp) + except ValueError: + pass + else: + raise ValueError('QQ16 coefficient mutation accepted') + print('PASS provider and QQ16 coefficient mutation controls') + if args.write: + with (HERE/'RESULT.json').open('x') as output: + output.write(json.dumps(receipt,indent=2,sort_keys=True)+'\n') + else: + need(canon(json.loads((HERE/'RESULT.json').read_text())) == canon(receipt), 'complete typed receipt') + print('PASS first selected provider binding; trace704 !=600; rank24; source198766 QQ16211210') + + +if __name__ == '__main__': + main()