From 986eb22defccc4578b2c634835c03e69377df171 Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Sun, 18 Oct 2026 21:35:25 -0500 Subject: [PATCH] Add selected centre decoder demand floor audit --- .../README.md | 105 +++++ .../RESULT.json | 132 ++++++ .../SOURCES.json | 42 ++ .../TASK.json | 67 +++ .../VERIFY.json | 24 ++ .../verify.py | 394 ++++++++++++++++++ 6 files changed, 764 insertions(+) create mode 100644 research/centre-selected-provider-demand-floor/README.md create mode 100644 research/centre-selected-provider-demand-floor/RESULT.json create mode 100644 research/centre-selected-provider-demand-floor/SOURCES.json create mode 100644 research/centre-selected-provider-demand-floor/TASK.json create mode 100644 research/centre-selected-provider-demand-floor/VERIFY.json create mode 100644 research/centre-selected-provider-demand-floor/verify.py diff --git a/research/centre-selected-provider-demand-floor/README.md b/research/centre-selected-provider-demand-floor/README.md new file mode 100644 index 0000000000..0acbfb8e77 --- /dev/null +++ b/research/centre-selected-provider-demand-floor/README.md @@ -0,0 +1,105 @@ +# Exact information floor for the selected gauge44 centre decoder + +## Question and result + +For one invocation of the currently selected `gauge44` local provider, how many +independent scalar channels must an exact linear replacement deliver to +preserve the centre phase's updates to consumer rows 112 through 223? + +The answer is exactly eight. The selected provider copies eight distinct source +rows into private centres, and its 112-by-8 consumer-demand matrix has rational +rank eight in both forward and backward orientations. Any exact linear +factorization through `m` scalar channels has rank at most `m`; therefore +`m >= 8`. The selected provider attains this information bound with eight +totals. Each total is carried by a rank-8 centre macro, so the selected profile +spends 64 rank units per invocation. + +In matrix form, if a replacement uses an encoder `E` with `m` scalar outputs +and a linear decoder `F` to preserve this endpoint, then `D = F E`, whence +`8 = rank(D) <= rank(E) <= m`. + +The 64-unit statement is an observed profile and a conditional floor for +replacements that retain the selected rank-8-per-channel carrier contract. The +rank computation alone does not prove that every changed decoder graph or +outside-code factorization must pay 64. The P112 copy-rank theorem has an +explicit root-code factorization interface; applying it to a changed decoder +requires proving that decoder meets that interface. This package claims the +unconditional information floor of eight channels for the stated linear +contract. + +## Contract and source binding + +The contract is the `centers` phase in +`research/gauge44-slots-t16/evidence/local/LOCAL-PROGRAMS.json.gz`, dispatched +by all calls in the selected global template to provider `gauge44`. The source +manifest named by `certificates/selected-result.json` hashes both the global +template and local program. The verifier checks those hashes, checks that the +inline provider program equals the separately pinned local program, and checks +each call's provider and orientation hash. + +Forward totals use source rows `(92, 57, 81, 224, 11, 240, 9, 256)` and private +centres `C_0` through `C_7`, mapped by the selected global template to the +physical private range `[7168, 7176)`. The eight rank-8 centre events have +frames 413 through 420. Each total contributes to 28 distinct consumer rows with +coefficient `+1/4` or `-1/4`; the union of the consumer rows is exactly 112 +through 223. The backward gather matrix is entrywise equal to the forward +fanout matrix and restores the same eight source rows. + +An exact nonzero minor uses rows `(112, 117, 118, 120, 113, 116, 115, 123)`; +its determinant is `-1/16384`, so the matrix has rank eight. Multiplying that +determinant by `4^8` gives `-4`. + +This is source-current work complementary to PR #3120 (head +`6e36982ccc888bdb4dc15982322d8fe1aed392b4`): that PR computed the same kind of +demand rank from a frozen archived template. Its archived local program is a +different input from the local program bound by the current selected source, so +this verifier re-derives the claim from the current provider rather than +importing that archive's binding. + +## Verification + +From the repository root: + +~~~sh +python3 -B research/centre-selected-provider-demand-floor/verify.py +python3 scripts/research_package.py --package research/centre-selected-provider-demand-floor --check-only +~~~ + +The verifier uses only the Python standard library and exact rational +arithmetic. It checks the selected-record and source-manifest pins, provider +dispatch, source and restore rows, all 224 fanout/gather terms, the exact rank +and minor, and two rank-dropping mutations. It does not run the selected cold +replay or any k-call cost calculation. + +## Scope and limitations + +- The lower bound is for linear scalar-copy interfaces that preserve this + exact 112-row endpoint and allow the eight named source-row values as + independent inputs. +- It proves at least eight independent channels. A 64-unit lower bound for a + changed implementation additionally needs a proof that its factors satisfy + the fixed rank-8 root-code charge model. +- No physical cross-call sharing eligibility, restoration bill, hosting, + precision, tape cost, supplier admission, or new kappa is established. +- The selected-source local check records 716 columns; this package does not + independently rerun that source check or the full selected replay. + +## Open next questions + +Can the exact selected 112-by-8 demand be represented by a changed decoder whose +copy channels fall outside the fixed rank-8 root-code factor model while +preserving the endpoint and all source/restoration obligations? This decides +whether the observed 64-unit charge extends beyond the retained carrier +contract. First derive the full factor interface for one concrete replacement +and price its exact matrix. The blocker is that no changed decoder is supplied +by this per-call audit. + +## Credit + +Selected construction and source line: PR #1094 and the review bound by the +selected record. Demand-rank predecessor: Aaron Wang's PR #3120, which this +package rebinds to the current selected provider. The conditional root-code +cost model is from `research/p112-batch-centre-floor/PROOF.md`; its credit chain +remains with PR #845, PR #1098, PR #968, and PR #1180. Prepared by OpenAI Codex +laptop-07 for Cinna Davis; substantial AI assistance, no human or proof-assistant +review claimed. Apache-2.0. diff --git a/research/centre-selected-provider-demand-floor/RESULT.json b/research/centre-selected-provider-demand-floor/RESULT.json new file mode 100644 index 0000000000..06b72a7f92 --- /dev/null +++ b/research/centre-selected-provider-demand-floor/RESULT.json @@ -0,0 +1,132 @@ +{ + "centre_path": { + "centre_frames_forward": [ + 413, + 414, + 415, + 416, + 417, + 418, + 419, + 420 + ], + "centre_ranks": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + "coefficients": [ + "-1/4", + "1/4" + ], + "consumer_rows": [ + 112, + 223 + ], + "consumers_per_total": [ + 28, + 28, + 28, + 28, + 28, + 28, + 28, + 28 + ], + "physical_private_scratch_range": [ + 7168, + 7176 + ], + "private_scratch": [ + "C0", + "C1", + "C2", + "C3", + "C4", + "C5", + "C6", + "C7" + ], + "source_rows_forward": [ + 92, + 57, + 81, + 224, + 11, + 240, + 9, + 256 + ], + "source_rows_restored_backward": [ + 92, + 57, + 81, + 224, + 11, + 240, + 9, + 256 + ], + "totals_per_invocation": 8 + }, + "controls": { + "merge_two_demand_columns_rank": 7, + "zero_one_demand_column_rank": 7 + }, + "decoder": { + "calls": 72, + "checked_input_columns": 716, + "events_per_orientation": { + "backward": 46772, + "forward": 46772 + }, + "global_template_version": "round20-R492-asynchronous-whole-owner-v1", + "orientations": { + "backward": 32, + "forward": 40 + }, + "provider_id": "gauge44" + }, + "demand": { + "backward_equals_forward": true, + "independent_rows": [ + 112, + 117, + 118, + 120, + 113, + 116, + 115, + 123 + ], + "minor_determinant": "-1/16384", + "minor_determinant_times_4_pow_8": -4, + "rank_backward": 8, + "rank_forward": 8, + "shape": [ + 112, + 8 + ] + }, + "lower_bound": { + "charged_floor_scope": "64 only under the retained rank-8-per-channel carrier restriction; arbitrary changed decoder factors are not covered", + "exact_linear_scalar_channels_per_invocation": 8, + "selected_rank_8_centre_charge_per_invocation": 64 + }, + "scope": "Exact linear-information floor for the selected gauge44 provider's pinned 112-row centre endpoint. No cross-call physical eligibility or universal cost bound for changed decoder graphs.", + "source_binding": { + "assembly_sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "global_template_sha256": "f713f8e66aaeaebb8202fe72bf36c7d23497152497342c27892e0fda3092f95b", + "local_programs_sha256": "172dc3d23e437909ddc01d07b12ede735afbb5bb6145f1ddf5c2e03097dfebe2", + "selected_kappa": "836330098538459/500000000000000000", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "selected_source_manifest_sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + "status": "PASS_SELECTED_PROVIDER_CENTRE_DEMAND_RANK" +} diff --git a/research/centre-selected-provider-demand-floor/SOURCES.json b/research/centre-selected-provider-demand-floor/SOURCES.json new file mode 100644 index 0000000000..00fe8bdf13 --- /dev/null +++ b/research/centre-selected-provider-demand-floor/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "input", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/gauge44-slots-t16/evidence/global/GLOBAL-TEMPLATE.json.gz", + "usage": "input", + "git_blob": "424c2df489364ea5b29e0df9841e6fe91a517df4", + "sha256": "f713f8e66aaeaebb8202fe72bf36c7d23497152497342c27892e0fda3092f95b" + }, + { + "path": "research/gauge44-slots-t16/evidence/local/LOCAL-PROGRAMS.json.gz", + "usage": "input", + "git_blob": "d511f2afa49f9eed010e91eed590a15252506470", + "sha256": "172dc3d23e437909ddc01d07b12ede735afbb5bb6145f1ddf5c2e03097dfebe2" + } + ] +} diff --git a/research/centre-selected-provider-demand-floor/TASK.json b/research/centre-selected-provider-demand-floor/TASK.json new file mode 100644 index 0000000000..989a797a97 --- /dev/null +++ b/research/centre-selected-provider-demand-floor/TASK.json @@ -0,0 +1,67 @@ +{ + "schema_version": 1, + "task_id": "centre-path-sharing", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "centre-path-sharing", + "question": "Can the 64-per-call centre path (eight rank-8 COPY/ERASE totals through the private temporary) be shared across calls or shrunk?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt", + "certificates/selected-result.json" + ], + "methods": [ + "Derive a fully charged favorable relaxation for sharing one centre path across k calls, including restoration, hosting and precision.", + "Prove a lower bound on copied information per call for the selected decoder contract." + ], + "acceptance_gate": "Show the changed centre charge and copy profile per call with every added restoration or hosting cost charged, and its ceiling via ceiling.ceiling(centre=...). 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", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write the per-call centre charge and copy children for sharing across k = 2 calls, charge the sharing overhead, and screen it; stop this route if even the ideal sharing gains under 10%. Ideal budgets: free 2.80x, shared by two 1.90x (levers.py).", + "bottleneck_link": "The centre path consumes 64 of about 99.6 unpaid coordinates per call, i.e. about 64% of the raw deficit.", + "allowed_variations": [ + "One sharing pattern across a fixed number of calls.", + "One reduced copied-total contract for the existing decoder.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Removing copies without a replacement contract for the decoder's copied totals.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "centre path", + "copied totals", + "private temporary", + "shared centre", + "batching" + ] + }, + "scope_status": "refined", + "actual_scope": "For one invocation of the current selected gauge44 provider, derive the exact linear information rank of the centre phase from its source-bound 112-row consumer endpoint, and state the resulting lower bound on copied scalar channels.", + "scope_change_reason": "The assigned complementary scope is method 2 at one explicit decoder contract. I pinned the current selected provider and its input/output map; k-call sharing prices are left to the separately assigned worker.", + "bottleneck_link": "The selected local profile pays eight rank-8 centre macros (64 rank units) per invocation. The demand rank decides whether that decoder can use fewer independent copied totals.", + "budget_minutes": 60, + "stop_rule": "Stop after the selected record, source manifest, provider dispatch and local program are hash-bound and the exact forward/backward demand rank and nonzero minor are reproduced. Do not extend into cross-call pricing or changed decoder graphs.", + "outcome": "completed", + "evidence": "README.md and RESULT.json; verify.py recomputes the exact current-provider demand rank, source rows, consumer rows and nonzero minor from the two source-manifest-bound files. Direct verification passed on Python 3.14.8 and the package metadata/pin check passed; registered Python 3.12 replay was unavailable on this host.", + "author": "OpenAI Codex laptop-07 for Cinna Davis", + "ai_assistance": "Substantial OpenAI Codex assistance in source audit, derivation, exact arithmetic, verification and packaging.", + "open_questions": [ + { + "question": "Can a changed exact decoder for this 112-by-8 demand use copy factors outside the fixed rank-8 root-code charge model while preserving the endpoint and source/restoration obligations?", + "why_it_matters": "The demand-rank result forces eight independent scalar channels, while the selected 64-unit profile uses eight rank-8 carriers. A changed factor class could alter the charged rank without reducing information rank.", + "first_step": "Specify one concrete alternative factor interface and derive its complete exact matrix and per-term support charges.", + "blocked_by": "No alternative decoder or proof that every admissible replacement falls under the P112 root-code model is supplied by this per-call audit." + } + ] +} diff --git a/research/centre-selected-provider-demand-floor/VERIFY.json b/research/centre-selected-provider-demand-floor/VERIFY.json new file mode 100644 index 0000000000..a8526f6f38 --- /dev/null +++ b/research/centre-selected-provider-demand-floor/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "research/gauge44-slots-t16/evidence/global/GLOBAL-TEMPLATE.json.gz", + "research/gauge44-slots-t16/evidence/local/LOCAL-PROGRAMS.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Selected-result/source-manifest binding; current gauge44 dispatch and embedded local-program equality; exact forward/backward demand rank, minor, source restoration, and rank-dropping controls." + } + ] +} diff --git a/research/centre-selected-provider-demand-floor/verify.py b/research/centre-selected-provider-demand-floor/verify.py new file mode 100644 index 0000000000..78eca8eb05 --- /dev/null +++ b/research/centre-selected-provider-demand-floor/verify.py @@ -0,0 +1,394 @@ +#!/usr/bin/env python3 +"""Recompute the exact centre-demand rank for the selected gauge44 provider.""" +import gzip +import hashlib +import json +import sys +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SELECTED = "certificates/selected-result.json" +SOURCE_MANIFEST = "research/community-frontier1094-audit/SELECTED-SOURCE.json" +ASSEMBLY = "research/community-frontier1094-audit/ASSEMBLY.json" +GLOBAL = "research/gauge44-slots-t16/evidence/global/GLOBAL-TEMPLATE.json.gz" +LOCAL = "research/gauge44-slots-t16/evidence/local/LOCAL-PROGRAMS.json.gz" +EXPECTED_COMMIT = "20ecf2891d80b5acf18d980b2164fb44ea7faa90" +EXPECTED_SELECTED_SHA256 = "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" +EXPECTED_SOURCE_SHA256 = "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" +EXPECTED_GLOBAL_SHA256 = "f713f8e66aaeaebb8202fe72bf36c7d23497152497342c27892e0fda3092f95b" +EXPECTED_LOCAL_SHA256 = "172dc3d23e437909ddc01d07b12ede735afbb5bb6145f1ddf5c2e03097dfebe2" +EXPECTED_ASSEMBLY_SHA256 = "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" +SOURCE_ROWS = (92, 57, 81, 224, 11, 240, 9, 256) +CONSUMER_ROWS = tuple(range(112, 224)) +MINOR_ROWS = (112, 117, 118, 120, 113, 116, 115, 123) +CENTRES = 8 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def sha256(data): + return hashlib.sha256(data).hexdigest() + + +def json_file(path): + return json.loads((ROOT / path).read_text(encoding="utf-8")) + + +def gzip_json(path): + return json.loads(gzip.decompress((ROOT / path).read_bytes())) + + +def source_binding(): + pins = json_file(f"{HERE.relative_to(ROOT)}/SOURCES.json") + need(pins["base_commit"] == EXPECTED_COMMIT, "package base commit changed") + inputs = {row["path"]: row["sha256"] for row in pins["files"] + if row["usage"] == "input"} + expected = { + SELECTED: EXPECTED_SELECTED_SHA256, + SOURCE_MANIFEST: EXPECTED_SOURCE_SHA256, + ASSEMBLY: EXPECTED_ASSEMBLY_SHA256, + GLOBAL: EXPECTED_GLOBAL_SHA256, + LOCAL: EXPECTED_LOCAL_SHA256, + } + need(set(inputs) == set(expected), "package inputs differ from pinned source set") + for path, digest in expected.items(): + need(inputs[path] == digest, f"SOURCES.json pin changed for {path}") + need(sha256((ROOT / path).read_bytes()) == digest, f"source byte drift: {path}") + + record = json_file(SELECTED) + need(record["source_manifest"] == SOURCE_MANIFEST, "selected source manifest changed") + need(record["certificate"] == ASSEMBLY, "selected certificate path changed") + need(record["certificate_sha256"] == EXPECTED_ASSEMBLY_SHA256, + "selected certificate digest changed") + manifest = json_file(SOURCE_MANIFEST) + files = manifest["files"] + need(files.get(GLOBAL) == EXPECTED_GLOBAL_SHA256, + "selected source manifest does not bind the global template") + need(files.get(LOCAL) == EXPECTED_LOCAL_SHA256, + "selected source manifest does not bind the local program") + need(record["kappa"] == "836330098538459/500000000000000000", + "selected record no longer names the launch-pinned result") + return { + "base_commit": EXPECTED_COMMIT, + "selected_record_sha256": EXPECTED_SELECTED_SHA256, + "selected_source_manifest_sha256": EXPECTED_SOURCE_SHA256, + "assembly_sha256": EXPECTED_ASSEMBLY_SHA256, + "global_template_sha256": EXPECTED_GLOBAL_SHA256, + "local_programs_sha256": EXPECTED_LOCAL_SHA256, + "selected_kappa": record["kappa"], + } + + +def location(value, kind): + return (isinstance(value, list) and len(value) == 2 and value[0] == kind + and isinstance(value[1], int)) + + +def scalar_ops(segment): + for pos, event in enumerate(segment): + if isinstance(event, list) and len(event) >= 2 and event[0] == "scalar": + if isinstance(event[1], list) and event[1]: + yield pos, event[1] + + +def centre_segment(events, orientation): + markers = [i for i, event in enumerate(events) + if event == ["phase", "centers"]] + need(len(markers) == 1, "expected one centers phase") + start = markers[0] + 1 + end = next((i for i in range(start, len(events)) + if isinstance(events[i], list) and len(events[i]) == 2 + and events[i][0] == "phase"), len(events)) + segment = events[start:end] + centers = [(i, e) for i, e in enumerate(segment) + if isinstance(e, list) and e and e[0] == "center"] + need(len(segment) == 256, "centre phase event count changed") + need(len(centers) == CENTRES, "centre event count changed") + by_id = {event[1]: (pos, event) for pos, event in centers} + need(set(by_id) == set(range(CENTRES)), "centre ids are not 0..7") + for k, (pos, event) in by_id.items(): + need(event[-1] == 8, f"centre {k} is not rank 8") + if orientation == "forward": + need(event[2:4] == [413 + k, 0], f"forward centre frame changed: {k}") + else: + need(event[2:4] == [0, 413 + k], f"backward centre frame changed: {k}") + return segment, by_id + + +def parse_orientation(events, orientation): + segment, centers = centre_segment(events, orientation) + ops = list(scalar_ops(segment)) + sources = [] + demand = {k: [] for k in range(CENTRES)} + + for k in range(CENTRES): + center_pos, _ = centers[k] + scratch = ["C", k] + clears = [(pos, op) for pos, op in ops + if op[0] == "clear" and len(op) == 2 and op[1] == scratch] + need(len(clears) == 2, f"private centre clear/restore count changed: C{k}") + if orientation == "forward": + copies = [(pos, op) for pos, op in ops + if op[0] == "copy" and len(op) == 3 + and op[1] == scratch and location(op[2], "L")] + need(len(copies) == 1, f"forward source copy count changed: C{k}") + copy_pos, copy_op = copies[0] + clear_positions = sorted(pos for pos, _ in clears) + need(clear_positions[0] < copy_pos, f"forward C{k} is copied before clear") + need(copy_pos < center_pos, f"forward C{k} is copied after its centre") + sources.append(copy_op[2][1]) + + writes_k = [(pos, op) for pos, op in ops + if op[0] == "add" and len(op) == 5 + and location(op[1], "L") and op[2] == scratch + and op[3] in (-1, 1) and op[4] == 4] + need(len(writes_k) == 28, f"forward fanout count changed: C{k}") + need(all(pos > center_pos for pos, _ in writes_k), + f"forward C{k} fanout precedes its centre") + rows = [op[1][1] for _, op in writes_k] + need(len(set(rows)) == 28, f"forward C{k} repeats a consumer") + need(clear_positions[1] > max(pos for pos, _ in writes_k), + f"forward C{k} is not cleared after fanout") + demand[k] = [(op[1][1], Fraction(op[3], op[4])) for _, op in writes_k] + else: + gathers = [(pos, op) for pos, op in ops + if op[0] == "add" and len(op) == 5 + and op[1] == scratch and location(op[2], "L") + and op[3] in (-1, 1) and op[4] == 4] + need(len(gathers) == 28, f"backward gather count changed: C{k}") + clear_positions = sorted(pos for pos, _ in clears) + need(clear_positions[0] < min(pos for pos, _ in gathers), + f"backward C{k} is read before clear") + need(all(pos < center_pos for pos, _ in gathers), + f"backward C{k} gather follows its centre") + rows = [op[2][1] for _, op in gathers] + need(len(set(rows)) == 28, f"backward C{k} repeats a consumer") + demand[k] = [(op[2][1], Fraction(op[3], op[4])) for _, op in gathers] + + restores = [(pos, op) for pos, op in ops + if op[0] == "add" and len(op) == 5 + and location(op[1], "L") and op[2] == scratch] + need(len(restores) == 1, f"backward source restore count changed: C{k}") + restore_pos, restore_op = restores[0] + need(restore_pos > center_pos and restore_op[3:] == [-1, 1], + f"backward source restoration changed: C{k}") + need(clear_positions[1] > restore_pos, + f"backward C{k} is not cleared after source restoration") + sources.append(restore_op[1][1]) + + if orientation == "forward": + observed = [] + for _, op in ops: + if op[0] == "add" and len(op) == 5 and location(op[1], "L") \ + and op[1][1] in CONSUMER_ROWS: + need(location(op[2], "C") and op[3] in (-1, 1) and op[4] == 4, + "forward centre phase has an unmodelled consumer update") + observed.append((op[1][1], op[2][1], Fraction(op[3], op[4]))) + expected = [(row, k, coefficient) for k, entries in demand.items() + for row, coefficient in entries] + need(sorted(observed) == sorted(expected), + "forward demand matrix omits or duplicates a consumer update") + else: + observed = [] + for _, op in ops: + if op[0] == "add" and len(op) == 5 and location(op[2], "L") \ + and op[2][1] in CONSUMER_ROWS: + need(location(op[1], "C") and op[3] in (-1, 1) and op[4] == 4, + "backward centre phase has an unmodelled consumer read") + observed.append((op[2][1], op[1][1], Fraction(op[3], op[4]))) + expected = [(row, k, coefficient) for k, entries in demand.items() + for row, coefficient in entries] + need(sorted(observed) == sorted(expected), + "backward demand matrix omits or duplicates a consumer read") + + rows = sorted({row for entries in demand.values() for row, _ in entries}) + matrix = {row: [Fraction(0) for _ in range(CENTRES)] for row in rows} + for k, entries in demand.items(): + for row, coefficient in entries: + matrix[row][k] += coefficient + return tuple(sources), rows, matrix, [centers[k][1] for k in range(CENTRES)] + + +def rank_and_rows(matrix, rows): + work = [[matrix[row][col] for col in range(CENTRES)] for row in rows] + labels = list(rows) + rank = 0 + for col in range(CENTRES): + pivot = next((i for i in range(rank, len(work)) if work[i][col]), None) + if pivot is None: + continue + work[rank], work[pivot] = work[pivot], work[rank] + labels[rank], labels[pivot] = labels[pivot], labels[rank] + value = work[rank][col] + work[rank] = [x / value for x in work[rank]] + for i in range(len(work)): + if i != rank and work[i][col]: + factor = work[i][col] + work[i] = [x - factor * y for x, y in zip(work[i], work[rank])] + rank += 1 + return rank, labels[:rank] + + +def determinant(square): + work = [list(row) for row in square] + value = Fraction(1) + for col in range(len(work)): + pivot = next((i for i in range(col, len(work)) if work[i][col]), None) + need(pivot is not None, "reported minor is singular") + if pivot != col: + work[col], work[pivot] = work[pivot], work[col] + value = -value + scale = work[col][col] + value *= scale + work[col] = [x / scale for x in work[col]] + for i in range(col + 1, len(work)): + factor = work[i][col] + if factor: + work[i] = [x - factor * y for x, y in zip(work[i], work[col])] + return value + + +def matrix_rank(matrix, rows): + return rank_and_rows(matrix, rows)[0] + + +def compute(): + binding = source_binding() + global_template = gzip_json(GLOBAL) + programs = gzip_json(LOCAL) + provider = global_template["local_providers"]["gauge44"] + scratch_namespace = global_template["private_namespace"]["centers"] + need(scratch_namespace == [7168, 7176], "physical private-centre namespace changed") + need(provider["centers"] == list(SOURCE_ROWS), "provider source-row declaration changed") + need(provider["local_programs_sha256"] == EXPECTED_LOCAL_SHA256, + "provider local-program digest changed") + need(provider["local_programs"] == programs, + "inline gauge44 provider differs from selected LOCAL-PROGRAMS") + need(global_template["provider_dispatch"].startswith("For each indivisible local_cover_sweep"), + "selected provider dispatch contract changed") + + calls = global_template["calls"] + orientations = {direction: sum(c["orientation"] == direction for c in calls) + for direction in ("forward", "backward")} + need(len(calls) == 72 and orientations == {"forward": 40, "backward": 32}, + "selected call schedule changed") + for call in calls: + need(call["provider_id"] == "gauge44", "a selected call uses another provider") + direction = call["orientation"] + need(direction in programs, "call has unknown orientation") + checked = provider["local_program_checks"][direction] + need(call["local_program_sha256"] == checked["sha256"], + "call local-program hash differs from provider check") + need(checked["events"] == len(programs[direction]), + "provider event count differs from local program") + need(checked["all_columns"] == 716, "selected local interface column count changed") + need(checked["private_centers_cleared"], "private centre clearing is not certified") + + global_programs = provider["local_programs"] + forward = parse_orientation(global_programs["forward"], "forward") + backward = parse_orientation(global_programs["backward"], "backward") + sources_f, rows_f, matrix_f, centres_f = forward + sources_b, rows_b, matrix_b, centres_b = backward + need(sources_f == sources_b == SOURCE_ROWS, "source/restore row tuple changed") + need(len(set(sources_f)) == CENTRES, "source rows are not independent distinct coordinates") + need(set(sources_f).isdisjoint(CONSUMER_ROWS), "source and consumer coordinates overlap") + need(rows_f == rows_b == list(CONSUMER_ROWS), "consumer rows changed") + need(matrix_f == matrix_b, "backward gather differs from forward fanout") + need([(e[1], e[2], e[-1]) for e in centres_f] + == [(e[1], e[3], e[-1]) for e in centres_b], + "forward/backward centre ids, frames or ranks differ") + for k in range(CENTRES): + nonzero = [matrix_f[row][k] for row in rows_f if matrix_f[row][k]] + need(len(nonzero) == 28 and all(x in (Fraction(1, 4), Fraction(-1, 4)) + for x in nonzero), + f"coefficient column changed: {k}") + + rank, minor_rows = rank_and_rows(matrix_f, rows_f) + need(rank == CENTRES, "selected demand rank is below eight") + need(tuple(minor_rows) == MINOR_ROWS, "independent-row witness changed") + minor = [[matrix_f[row][col] for col in range(CENTRES)] for row in minor_rows] + minor_det = determinant(minor) + need(minor_det == Fraction(-1, 16384), "exact nonzero minor determinant changed") + + zeroed = {row: list(values) for row, values in matrix_f.items()} + for row in rows_f: + zeroed[row][0] = Fraction(0) + merged = {row: list(values) for row, values in matrix_f.items()} + for row in rows_f: + merged[row][1] = merged[row][0] + zero_rank = matrix_rank(zeroed, rows_f) + merged_rank = matrix_rank(merged, rows_f) + need(zero_rank == merged_rank == 7, "rank-dropping controls did not reduce rank to seven") + + checks = provider["local_program_checks"] + need(all(checks[d]["paid_profile"].get("8") == 8 for d in ("forward", "backward")), + "selected rank-8 centre profile changed") + return { + "status": "PASS_SELECTED_PROVIDER_CENTRE_DEMAND_RANK", + "source_binding": binding, + "decoder": { + "provider_id": "gauge44", + "global_template_version": global_template["version"], + "calls": len(calls), + "orientations": orientations, + "events_per_orientation": {d: len(global_programs[d]) + for d in ("forward", "backward")}, + "checked_input_columns": 716, + }, + "centre_path": { + "totals_per_invocation": CENTRES, + "source_rows_forward": list(sources_f), + "source_rows_restored_backward": list(sources_b), + "private_scratch": ["C0", "C1", "C2", "C3", "C4", "C5", "C6", "C7"], + "physical_private_scratch_range": scratch_namespace, + "centre_ranks": [event[-1] for event in centres_f], + "centre_frames_forward": [event[2] for event in centres_f], + "consumer_rows": [rows_f[0], rows_f[-1]], + "consumers_per_total": [28] * CENTRES, + "coefficients": ["-1/4", "1/4"], + }, + "demand": { + "shape": [len(rows_f), CENTRES], + "rank_forward": rank, + "rank_backward": rank, + "backward_equals_forward": True, + "independent_rows": list(minor_rows), + "minor_determinant": str(minor_det), + "minor_determinant_times_4_pow_8": int(minor_det * 4 ** CENTRES), + }, + "lower_bound": { + "exact_linear_scalar_channels_per_invocation": CENTRES, + "selected_rank_8_centre_charge_per_invocation": CENTRES * 8, + "charged_floor_scope": "64 only under the retained rank-8-per-channel carrier restriction; arbitrary changed decoder factors are not covered", + }, + "controls": { + "zero_one_demand_column_rank": zero_rank, + "merge_two_demand_columns_rank": merged_rank, + }, + "scope": "Exact linear-information floor for the selected gauge44 provider's pinned 112-row centre endpoint. No cross-call physical eligibility or universal cost bound for changed decoder graphs.", + } + + +def main(): + result = compute() + rendered = json.dumps(result, indent=1, sort_keys=True) + "\n" + target = HERE / "RESULT.json" + if sys.argv[1:] == ["--write"]: + target.write_text(rendered, encoding="utf-8") + else: + need(target.read_text(encoding="utf-8") == rendered, + "RESULT.json differs from exact recomputation; run verify.py --write") + print("PASS_SELECTED_PROVIDER_CENTRE_DEMAND_RANK rank=8 channels>=8 minor=-1/16384 observed_rank8_charge=64") + + +if __name__ == "__main__": + try: + main() + except (OSError, ValueError, KeyError, TypeError, ZeroDivisionError) as exc: + print(f"FAIL_SELECTED_PROVIDER_CENTRE_DEMAND_RANK: {exc}") + raise SystemExit(1)