diff --git a/research/unit-ring-dirty-fanout/README.md b/research/unit-ring-dirty-fanout/README.md new file mode 100644 index 0000000000..70ce8559a0 --- /dev/null +++ b/research/unit-ring-dirty-fanout/README.md @@ -0,0 +1,203 @@ +# Exact dirty-fanout tariffs over unital rings + +This contribution is produced by Nick Petalas. Apache-2.0. + +**Scoped proof with exact finite corroboration; no new kappa.** Ross +Richardson's [PR3121](https://github.com/CrocSwap/integer-mult-bounds/pull/3121) +proves the stationary directed-tariff optimum for a common XOR value. Here +the same optimum holds over every nonzero unital ring, including +noncommutative rings, with different unit target coefficients. The new +step is a free-module dirt-cut argument and an ordered coefficient ratio. +The predecessor's binary result and graph optimization are credited methods, +rather than new results or replay deliverables. + +## Contract and result + +Let R be any ring with 1 != 0. There are exactly q >= 1 dirty rows, initially +arbitrary independent a_i in R^w, w >= 1. A preserved disjoint source supplies +arbitrary p in R^w. Multiplication of coefficients is on the left. A fixed +finite straight-line word may use + +```text +ADD(i,j,alpha): A_i <- A_i + alpha A_j, i != j, alpha in R, +P(i,beta): A_i <- A_i + beta p, beta in R. +``` + +Every ADD on j -> i costs c_ij > 0 and every P at i costs mu_i > 0. These +are finite stationary complete prices, independent of the coefficient. +The endpoint must be A_i = a_i + lambda_i p for specified two-sided units +lambda_i in R. All q rows are required outputs. There are no other helpers, +free basis changes, CLEAR, COPY, adaptive control or intermediate observers. +The word must work for all entry dirt and all p. Scalar applications and +their inverses must already be included in the declared complete tariffs. + +The exact optimum over all allowed words, including arbitrary interleavings, +repeated calls and nonunit gate coefficients, is + +```text +min over directed rooted spanning forests F: + sum_(roots i) mu_i + 2 sum_(arcs j -> i in F) c_ij. +``` + +Thus unequal unit demands, zero divisors and noncommutativity do not add a +source insertion or edge occurrence under this coefficient-independent +contract. Over a field this covers every list of nonzero scalar demands. +A separately required inverse has the same tariff and must be paid again. + +## Proof + +Project each row onto its q entry-dirt symbols. Its coefficient matrix M +starts at I_q. An ADD left-multiplies M by I_q + alpha E_ij, with inverse +I_q - alpha E_ij. A source call leaves M unchanged. Therefore every prefix +matrix is invertible over R, and its rows form a free left-module basis of +R^q. This uses neither division nor a field rank argument. Equality of +coefficient matrices follows from the all-input contract by setting one +dirty symbol to 1 and the others and p to zero. + +Let O be the set of rows receiving at least one source insertion. It is +nonempty. Fix a nonempty S disjoint from O. With no incoming ADD to S, +its p coefficients remain zero. This contradicts the nonzero target +coefficient on every row in S. + +There also cannot be exactly one incoming ADD. Before that gate, internal +ADDs preserve the S-row module W_S = span_R{e_i : i in S}; outgoing ADDs +leave S unchanged. Suppose the sole incoming gate is j -> i with coefficient +alpha. If alpha = 0, it cannot deliver p, as in the zero-incoming case. +Otherwise its source row m_j belongs to the full free basis and is outside +the S subset of that basis. In that basis, alpha m_j has coefficient alpha +on m_j, so it cannot belong to W_S, even if alpha is a zero divisor. +Replacing m_i by m_i + alpha m_j therefore changes the S-row module. +All subsequent internal ADDs preserve the changed module and outgoing +gates leave it unchanged. The final dirt matrix I_q would restore W_S, +which is impossible. Every such S needs at least two incoming occurrences. + +Apply Edmonds' finite prescribed-root disjoint-branching theorem to the +directed ADD occurrence multigraph, with two identical root sets O. Its +cut condition is exactly the preceding statement for S disjoint from O; +for S meeting O it asks for zero incoming arcs. It supplies two +occurrence-disjoint spanning forests rooted at O. If f(O) is the cheapest +such forest, the ADD bill is at least 2 f(O). Every row in O costs at least +one source insertion, proving the claimed lower bound. Parallel occurrences +count separately. This external graph theorem is the same dependency used +by PR3121; no new graph-theorem proof or formal-kernel verification is claimed. +Its precise finite statement is retained in the pinned +[predecessor proof](../dirty-anchor-edge-tariffs/PROOF.md#lemma-2-cuts-force-two-paid-directed-forests). + +For attainment choose a forest and set + +```text +r_ij = lambda_i lambda_j^(-1), for each parent arc j -> i. +``` + +In children-before-parents order, subtract r_ij A_j from A_i. Each parent +still contains its original dirt when used, so the prepared nonroot row is +a_i - r_ij a_j. Insert lambda_i p at each root. Undo preparation in literal +reverse order, adding r_ij times the restored parent. Induction gives + +```text +(a_i - r_ij a_j) + r_ij (a_j + lambda_j p) + = a_i + lambda_i p. +``` + +The order lambda_i lambda_j^(-1) is essential. Every edge costs twice and +every root once. Negating coefficients and reversing the entire word gives +its inverse, with the same prices. Minimizing over forests proves equality. + +## Finite evidence and boundaries + +The first working example is a three-row chain over Z/4 with demands +(3,1,3). Five paid gates realize the endpoint for arbitrary entry dirt. +The verifier evaluates symbolic ring coefficients, so each checked word +covers every payload width and every value of its independent input symbols +in that ring. This does not turn the finite word census into the universal +proof above. + +The fixed checks enumerate every rooted forest on q = 1,...,5. For each +forest they test cyclic shifts of the ordered unit list as demands, with +both the forward map and its literal inverse. There are 2,882 words per +ring Z/3, Z/4 and Z/6, and 8,646 over M2(F2). These demand lists are declared +fixtures, not an exhaustive enumeration of all heterogeneous unit lists. + +A separately implemented modular affine-state search permits every nonzero +ADD and insertion coefficient, arbitrary order and arbitrary multiplicity. +It exhausts 48 two-row tariff instances over Z/3, Z/4 and Z/6, with all four +prices in {1,4}. It checks all four unit-demand pairs per instance, 192 +comparisons total, visiting 98,688 states across the instances. This search +does not assume a forest form. Its arithmetic uses direct modular integers, +independently of the ring-table word interpreter. + +Five boundary groups check reversed noncommutative coefficient order, +missing dirt restoration, the nonunit-demand boundary, nonunit rejection +by the constructor, and cyclic parent rejection. The nonunit boundary is +an exact finite counterexample to dropping the unit hypothesis. Over Z/4, +with demands (2,1), mu = (1,9) and both directed ADD prices 1, unrestricted +shortest paths give optimum 4; the unit formula would give 3. The word + +```text +A_1 -= A_0; P(0,1); A_1 += A_0; P(0,1) +``` + +attains 4. No all-ring nonunit-demand formula is claimed. In M2(F2), encoded +row-major matrices 6 and 7 give correct ratio 11 and reversed ratio 13. +The latter fails the required arbitrary-dirt endpoint. + +## Reproduce + +From the repository root, using CPython 3.12 and the standard library: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py \ + --package research/unit-ring-dirty-fanout +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B \ + research/unit-ring-dirty-fanout/verify.py +``` + +Expected marker: PASS_UNIT_RING_DIRTY_FANOUT. The manifest runs normal and +optimized warning-strict checks. RESULT.json is generated by the verifier +and binds the proof, metadata and verifier hashes. Normal checking writes +nothing. `--output PATH` creates an absent external receipt and refuses to +overwrite an existing file. Provenance documents are pinned historical +references; no predecessor executable or network access is needed by the +direct scientific checker. Package metadata checks require Git history. + +## Scope and credit + +Credit Ross Richardson #3121 and #3063 for the XOR tariff, dirt-cut method +and destination-only boundary; Cinna Davis #1944 for dirty-output anchors +and #1968 for separate several-term accumulation; Anthony #774 and Oscar +Fennell #759 for forest compensation and their retained synthesis lineage. +Tekalign #3130 supplies the direct cut-certificate and classical optimizer +application. Edmonds supplies disjoint branching. These results are cited, +not rechecked deliverables. Exact retained document pins and predecessor +heads are in SOURCES.json and TASK.json. No priority for forest synthesis +or general graph optimization is claimed. + +This is an algebraic interface extension. Complete tariffs must include +coefficient application, source access, routing, frames, precision, scratch +cleanup and physical head return when applicable. No actual caller, +physical supplier, all-size tape realization, complete moment invoice or +selected-frontier change is supplied. The selected kappa stays 0.00302015. +Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +The nonunit-demand optimum and a physical caller with coefficient-independent +complete prices remain open. Start with the displayed Z/4 demand and a +declared price matrix for the first; start with one actual caller's full +bill for the second. The unit-ratio obstruction and the absent physical +tariffs are the respective blockers. TASK.json records the concrete first +steps and relevance. Stop this construction round at the proved extension. + +## Engineering constraints + +Power-of-Ten rule 3 has a managed-runtime deviation: Python exact objects, +heaps and JSON allocate dynamically. Ring size is at most 16; word tests +have at most five rows and nine gates; forest enumeration has at most +5^5 candidate parent functions. A two-row modular search stores at most +6^6 states, with at most 20 outgoing gates per state. Its heap-pop bound +is 1 + 20*6^6, and successful relaxation bounds heap pushes by the same +quantity. There is no recursion, service, background process or dynamic +code evaluation. Standard-library allocation internals are not audited. +The verifier's standard-library dataclass and argparse dispatch have fixed +targets. A larger ring, row count or external input format must add new +explicit capacity and arithmetic limits before expanding these bounds. diff --git a/research/unit-ring-dirty-fanout/RESULT.json b/research/unit-ring-dirty-fanout/RESULT.json new file mode 100644 index 0000000000..1c17c8a41a --- /dev/null +++ b/research/unit-ring-dirty-fanout/RESULT.json @@ -0,0 +1,103 @@ +{ + "file_sha256": { + "README.md": "70764fb3def04ba1b0a51e95cb023358fdaed5100d2440feecbaab0e85a9a5fe", + "SOURCES.json": "643a5efb86d1f7035caf0353089db792c42a8b7684c62b84083668e774f70e1e", + "TASK.json": "58cdcadf83d5dd1fbf3de8b8951c14f57e77b2dba363ffe3e45a1c393272a7c8", + "VERIFY.json": "0dd5db1967a6d8eb910675a95002dab89defa28c2a845b5d1ad499f720f2c2ce", + "verify.py": "bbe6c845c289bb48a908cfbe5e6961c6cc12de1c42ddec7f2fcef6a969b9172a" + }, + "result": { + "boundaries": { + "control_groups": 5, + "correct_ratio": 11, + "first_Z4_chain_gates": 5, + "inapplicable_forest_value": 3, + "incorrect_ratio": 13, + "noncommuting_units": [ + 6, + 7 + ], + "nonunit_Z4_cost": 4 + }, + "claim_type": "scoped proof with exact finite corroboration", + "new_kappa": false, + "shortest_paths": { + "affine_states_across_instances": 98688, + "state_counts": { + "3:1,1,1,1": 216, + "3:1,1,1,4": 216, + "3:1,1,4,1": 216, + "3:1,1,4,4": 216, + "3:1,4,1,1": 216, + "3:1,4,1,4": 216, + "3:1,4,4,1": 216, + "3:1,4,4,4": 216, + "3:4,1,1,1": 216, + "3:4,1,1,4": 216, + "3:4,1,4,1": 216, + "3:4,1,4,4": 216, + "3:4,4,1,1": 216, + "3:4,4,1,4": 216, + "3:4,4,4,1": 216, + "3:4,4,4,4": 216, + "4:1,1,1,1": 768, + "4:1,1,1,4": 768, + "4:1,1,4,1": 768, + "4:1,1,4,4": 768, + "4:1,4,1,1": 768, + "4:1,4,1,4": 768, + "4:1,4,4,1": 768, + "4:1,4,4,4": 768, + "4:4,1,1,1": 768, + "4:4,1,1,4": 768, + "4:4,1,4,1": 768, + "4:4,1,4,4": 768, + "4:4,4,1,1": 768, + "4:4,4,1,4": 768, + "4:4,4,4,1": 768, + "4:4,4,4,4": 768, + "6:1,1,1,1": 5184, + "6:1,1,1,4": 5184, + "6:1,1,4,1": 5184, + "6:1,1,4,4": 5184, + "6:1,4,1,1": 5184, + "6:1,4,1,4": 5184, + "6:1,4,4,1": 5184, + "6:1,4,4,4": 5184, + "6:4,1,1,1": 5184, + "6:4,1,1,4": 5184, + "6:4,1,4,1": 5184, + "6:4,1,4,4": 5184, + "6:4,4,1,1": 5184, + "6:4,4,1,4": 5184, + "6:4,4,4,1": 5184, + "6:4,4,4,4": 5184 + }, + "tariff_instances": 48, + "unit_demand_comparisons": 192 + }, + "words": [ + { + "endpoint_sha256": "05b9977fd1355f2808a5faab00091bf20a1764f8b17f8d35d6048f4400c00d18", + "ring": "Z/3", + "words": 2882 + }, + { + "endpoint_sha256": "306d257d8ff7b6cb38cc0d5b9a7bb93dcd0d505778fb142a17d103bad95543f6", + "ring": "Z/4", + "words": 2882 + }, + { + "endpoint_sha256": "fb8f57d16897b8dea6b922e39c1ff2865cc9e741b96fe0516822aa9b412de33c", + "ring": "Z/6", + "words": 2882 + }, + { + "endpoint_sha256": "5de83a8eaceb59193b580e0290893989256026778ba00a88db13e7c2eb8193d9", + "ring": "M2(F2)", + "words": 8646 + } + ] + }, + "schema_version": 1 +} diff --git a/research/unit-ring-dirty-fanout/SOURCES.json b/research/unit-ring-dirty-fanout/SOURCES.json new file mode 100644 index 0000000000..9c5cb6155a --- /dev/null +++ b/research/unit-ring-dirty-fanout/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/dirty-anchor-edge-tariffs/PROOF.md", + "usage": "provenance", + "git_blob": "7643ababf0f003eaf699edb4910ce9693025b5cd", + "sha256": "1c73b56222dbd63a2230a23c00ce4b822eaa3aa7cdd4c5d6ba9975b98857b289" + }, + { + "path": "research/dirty-anchor-edge-tariffs/README.md", + "usage": "provenance", + "git_blob": "16aa73e36b791fd4c025011123b8101dd4a1c2d6", + "sha256": "dae5277016949f17bc55191e34a5f9470475b94ed679c843217973711ce2a341" + }, + { + "path": "research/dirty-fanout-cut-certificate/README.md", + "usage": "provenance", + "git_blob": "a8c115df2943da5fdb3da0604705524a9b8a0729", + "sha256": "67ff4fb86fd297162bb568097b02652097ec3a9ba3422f90c020fb213c36f094" + } + ] +} diff --git a/research/unit-ring-dirty-fanout/TASK.json b/research/unit-ring-dirty-fanout/TASK.json new file mode 100644 index 0000000000..45153d870a --- /dev/null +++ b/research/unit-ring-dirty-fanout/TASK.json @@ -0,0 +1,87 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. 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/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact stationary edge-priced dirty fanout over arbitrary nonzero unital rings, including noncommutative rings, with heterogeneous unit target coefficients.", + "scope_change_reason": "Extend the coefficient domain explicitly excluded by Ross Richardson PR3121. This is a scoped algebraic interface result rather than an R439 H2/K replacement.", + "bottleneck_link": "A side result: complete stationary fanout tariffs survive composite and noncommutative coefficients without extra source calls. No actual physical tariff matrix or changed recursive moment is supplied.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved ring extension with bounded exact corroboration. Do not pursue nonunit-demand optima or a physical supplier.", + "outcome": "completed", + "evidence": "Written free-module dirt-cut argument and ordered coefficient construction; exact finite words and unrestricted two-row residue-ring shortest paths.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "For nonunit target coefficients, what additional ideal or factorization constraints replace the unit-demand forest optimum?", + "why_it_matters": "The explicit Z/4 two-row example has true optimum 4 rather than the unit formula value 3.", + "first_step": "Classify every two-row demand over Z/4 at a declared stationary price matrix using exact affine-state shortest paths, then seek a structural formula.", + "blocked_by": "Nonunit coefficients cannot always be transported by a unit ratio; no all-ring classification is claimed." + }, + { + "question": "Can a named physical caller provide coefficient-independent complete tariffs for a profitable ring-valued fanout?", + "why_it_matters": "The theorem supplies an abstract tariff optimum, not a recursive supplier improvement.", + "first_step": "Choose one actual caller and charge coefficient application, source access, frames, target lifetimes and restoration before optimizing.", + "blocked_by": "No physical tariff matrix, chronological caller, storage/precision bill or compatible outer transfer is supplied." + } + ], + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134570", + "environment": { + "python": "CPython 3.12.15", + "platform": "macOS 27.0.1 arm64", + "dependencies": "standard library" + }, + "predecessors": [ + { + "pr": 3121, + "author": "Ross Richardson", + "head": "eea0861aff47df568be4bb4a4db43c2da390d351", + "role": "XOR directed-tariff theorem and subset dirt-cut method" + }, + { + "pr": 3130, + "author": "Tekalign", + "head": "d34c1142f914c477708d1bb03db11691b0341070", + "role": "Direct cut certificates and classical optimizer application; not executed here" + } + ] +} diff --git a/research/unit-ring-dirty-fanout/VERIFY.json b/research/unit-ring-dirty-fanout/VERIFY.json new file mode 100644 index 0000000000..d0c20872cb --- /dev/null +++ b/research/unit-ring-dirty-fanout/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All finite ring words, independent unrestricted modular shortest paths, boundary controls, and source-bound receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same mathematical predicates with Python assertions disabled." + } + ] +} diff --git a/research/unit-ring-dirty-fanout/verify.py b/research/unit-ring-dirty-fanout/verify.py new file mode 100644 index 0000000000..7b9fe3a0d5 --- /dev/null +++ b/research/unit-ring-dirty-fanout/verify.py @@ -0,0 +1,311 @@ +"""Exact finite evidence for unit-ring dirty fanout. + +Produced by Nick Petalas. Apache-2.0. +No predecessor executable is imported. Scientific checks survive -O. +""" + +from __future__ import annotations + +import argparse +import hashlib +import heapq +import itertools +import json +from dataclasses import dataclass +from pathlib import Path + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +@dataclass(frozen=True) +class Ring: + name: str + one: int + add: tuple[tuple[int, ...], ...] + mul: tuple[tuple[int, ...], ...] + neg: tuple[int, ...] + inv: tuple[int, ...] + + +def finish_ring(name: str, one: int, add: tuple, mul: tuple) -> Ring: + size = len(add) + neg = tuple(next(b for b in range(size) if add[a][b] == 0) for a in range(size)) + inv = tuple( + next((b for b in range(size) if mul[a][b] == one and mul[b][a] == one), -1) + for a in range(size) + ) + return Ring(name, one, add, mul, neg, inv) + + +def cyclic_ring(modulus: int) -> Ring: + require(2 <= modulus <= 6, "modulus outside fixed verification domain") + add = tuple( + tuple((a + b) % modulus for b in range(modulus)) for a in range(modulus) + ) + mul = tuple(tuple(a * b % modulus for b in range(modulus)) for a in range(modulus)) + return finish_ring(f"Z/{modulus}", 1, add, mul) + + +def matrix_ring() -> Ring: + """Encode a 2-by-2 binary matrix in row-major bit order.""" + add = tuple(tuple(a ^ b for b in range(16)) for a in range(16)) + rows = [] + for a in range(16): + row = [] + for b in range(16): + value = 0 + for i, j in itertools.product(range(2), repeat=2): + bit = 0 + for k in range(2): + bit ^= ((a >> (2 * i + k)) & 1) & ((b >> (2 * k + j)) & 1) + value |= bit << (2 * i + j) + row.append(value) + rows.append(tuple(row)) + return finish_ring("M2(F2)", 9, add, tuple(rows)) + + +def endpoint(ring: Ring, demand: tuple[int, ...]) -> tuple[int, ...]: + q = len(demand) + require(1 <= q <= 5, "row count outside verification domain") + return tuple( + ring.one if j == i else demand[i] if j == q else 0 + for i in range(q) + for j in range(q + 1) + ) + + +def apply_gate(ring: Ring, state: tuple, gate: tuple, q: int) -> tuple: + i, j, coefficient = gate + result = list(state) + if j == -1: + index = i * (q + 1) + q + result[index] = ring.add[result[index]][coefficient] + else: + for k in range(q + 1): + index = i * (q + 1) + k + value = ring.mul[coefficient][state[j * (q + 1) + k]] + result[index] = ring.add[result[index]][value] + return tuple(result) + + +def forest_depths(parents: tuple[int, ...]) -> tuple[int, ...] | None: + q = len(parents) + depths = [] + for start in range(q): + vertex = start + for depth in range(q): + if parents[vertex] == -1: + depths.append(depth) + break + vertex = parents[vertex] + else: + return None + return tuple(depths) + + +def forests(q: int) -> tuple[tuple[int, ...], ...]: + require(1 <= q <= 5, "forest bound exceeded") + choices = [tuple(j for j in range(-1, q) if j != i) for i in range(q)] + return tuple(p for p in itertools.product(*choices) if forest_depths(p) is not None) + + +def forest_word(ring: Ring, parents: tuple, demand: tuple) -> tuple: + require(len(parents) == len(demand), "inconsistent word dimensions") + require( + all(0 <= a < len(ring.inv) and ring.inv[a] >= 0 for a in demand), + "every target coefficient must be a unit", + ) + depths = forest_depths(parents) + require(depths is not None, "parent relation contains a cycle") + order = sorted(range(len(parents)), key=lambda i: (-depths[i], i)) + preparation = tuple( + (i, parents[i], ring.neg[ring.mul[demand[i]][ring.inv[demand[parents[i]]]]]) + for i in order + if parents[i] >= 0 + ) + calls = tuple((i, -1, demand[i]) for i in order if parents[i] == -1) + restoration = tuple((i, j, ring.neg[a]) for i, j, a in reversed(preparation)) + return preparation + calls + restoration + + +def execute(ring: Ring, q: int, word: tuple) -> tuple: + state = endpoint(ring, (0,) * q) + for gate in word: + state = apply_gate(ring, state, gate, q) + return state + + +def check_words(ring: Ring) -> dict: + units = tuple(a for a, inverse in enumerate(ring.inv) if inverse >= 0) + count = 0 + digest = hashlib.sha256() + for q in range(1, 6): + demands = { + tuple(units[(i + shift) % len(units)] for i in range(q)) + for shift in range(len(units)) + } + for parents, demand in itertools.product(forests(q), sorted(demands)): + word = forest_word(ring, parents, demand) + value = execute(ring, q, word) + require(value == endpoint(ring, demand), "arbitrary-dirt endpoint failed") + inverse = tuple((i, j, ring.neg[a]) for i, j, a in reversed(word)) + for gate in inverse: + value = apply_gate(ring, value, gate, q) + require(value == endpoint(ring, (0,) * q), "literal inverse failed") + digest.update(bytes(execute(ring, q, word))) + count += 1 + return {"ring": ring.name, "words": count, "endpoint_sha256": digest.hexdigest()} + + +def modular_distances(modulus: int, prices: tuple[int, ...]) -> dict: + """Independent full affine-state shortest paths, always exactly two rows.""" + start = (1, 0, 0, 0, 1, 0) + distances = {start: 0} + heap = [(0, start)] + gates = tuple( + (i, j, a, prices[k]) + for k, (i, j) in enumerate(((0, -1), (1, -1), (0, 1), (1, 0))) + for a in range(1, modulus) + ) + capacity = modulus**6 + for _ in range(capacity * len(gates) + 1): + if not heap: + return distances + cost, state = heapq.heappop(heap) + if distances[state] != cost: + continue + for i, j, a, price in gates: + changed = list(state) + if j == -1: + changed[3 * i + 2] = (changed[3 * i + 2] + a) % modulus + else: + for k in range(3): + changed[3 * i + k] = ( + state[3 * i + k] + a * state[3 * j + k] + ) % modulus + target = tuple(changed) + new_cost = cost + price + if new_cost < distances.get(target, 10**9): + distances[target] = new_cost + require(len(distances) <= capacity, "state-capacity bound violated") + heapq.heappush(heap, (new_cost, target)) + raise ValueError("bounded shortest-path queue failed to exhaust") + + +def check_shortest_paths() -> dict: + comparisons = 0 + states = 0 + histogram: dict[str, int] = {} + for modulus in (3, 4, 6): + ring = cyclic_ring(modulus) + units = tuple(a for a, inverse in enumerate(ring.inv) if inverse >= 0) + for prices in itertools.product((1, 4), repeat=4): + distances = modular_distances(modulus, prices) + states += len(distances) + mu0, mu1, c01, c10 = prices + expected = min(mu0 + mu1, mu0 + 2 * c10, mu1 + 2 * c01) + for a, b in itertools.product(units, repeat=2): + require( + distances[(1, 0, a, 0, 1, b)] == expected, + "unrestricted ring shortest path beats/misses forest price", + ) + comparisons += 1 + histogram[f"{modulus}:{','.join(map(str, prices))}"] = len(distances) + return { + "tariff_instances": len(histogram), + "unit_demand_comparisons": comparisons, + "affine_states_across_instances": states, + "state_counts": histogram, + } + + +def check_boundaries() -> dict: + ring = matrix_ring() + units = tuple(a for a, inverse in enumerate(ring.inv) if inverse >= 0) + order_witness = None + for parent, child in itertools.product(units, repeat=2): + right = ring.mul[child][ring.inv[parent]] + wrong = ring.mul[ring.inv[parent]][child] + if right != wrong: + order_witness = (parent, child, right, wrong) + break + require(order_witness is not None, "matrix-ring fixture must be noncommutative") + parent, child, right, wrong = order_witness + word = forest_word(ring, (-1, 0), (parent, child)) + mutant = tuple((i, j, wrong) if j >= 0 else (i, j, a) for i, j, a in word) + require( + execute(ring, 2, mutant) != endpoint(ring, (parent, child)), + "reversed coefficient-order control failed", + ) + require( + execute(ring, 2, word[:-1]) != endpoint(ring, (parent, child)), + "missing dirt-restoration control failed", + ) + z4 = cyclic_ring(4) + distances = modular_distances(4, (1, 9, 1, 1)) + nonunit_cost = distances[(1, 0, 2, 0, 1, 1)] + require(nonunit_cost == 4, "nonunit boundary must distinguish the formula value 3") + try: + forest_word(z4, (-1, 0), (2, 1)) + except ValueError as error: + require("unit" in str(error), "nonunit rejected for wrong reason") + else: + raise ValueError("nonunit demands were accepted") + require(forest_depths((1, 0)) is None, "cycle must not be a forest") + first = forest_word(z4, (-1, 0, 1), (3, 1, 3)) + require(execute(z4, 3, first) == endpoint(z4, (3, 1, 3)), "first fixture failed") + return { + "noncommuting_units": [parent, child], + "correct_ratio": right, + "incorrect_ratio": wrong, + "nonunit_Z4_cost": nonunit_cost, + "inapplicable_forest_value": 3, + "first_Z4_chain_gates": len(first), + "control_groups": 5, + } + + +def reconstruct() -> dict: + return { + "claim_type": "scoped proof with exact finite corroboration", + "new_kappa": False, + "words": [check_words(cyclic_ring(m)) for m in (3, 4, 6)] + + [check_words(matrix_ring())], + "shortest_paths": check_shortest_paths(), + "boundaries": check_boundaries(), + } + + +def bound_hashes() -> dict[str, str]: + base = Path(__file__).resolve().parent + names = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + return { + name: hashlib.sha256((base / name).read_bytes()).hexdigest() for name in names + } + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="create an absent external receipt") + args = parser.parse_args() + receipt = { + "schema_version": 1, + "file_sha256": bound_hashes(), + "result": reconstruct(), + } + encoded = json.dumps(receipt, indent=2, sort_keys=True) + "\n" + if args.output is not None: + with args.output.open("x", encoding="utf-8") as handle: + require(handle.write(encoded) == len(encoded), "short receipt write") + else: + stored = Path(__file__).with_name("RESULT.json").read_text(encoding="utf-8") + require(stored == encoded, "source-bound canonical receipt differs") + print("PASS_UNIT_RING_DIRTY_FANOUT") + print(json.dumps(receipt["result"], sort_keys=True)) + + +if __name__ == "__main__": + main()