diff --git a/research/low-use-source-gauges/PROOF.md b/research/low-use-source-gauges/PROOF.md new file mode 100644 index 0000000000..59ab3fe1cd --- /dev/null +++ b/research/low-use-source-gauges/PROOF.md @@ -0,0 +1,126 @@ +# Restored gauges have a sharp source-use threshold + +This is a scoped scalar-cost theorem. It answers the low-use part of the +coupled source/target question in Dugongue's PR #4518. Its native word and +its target-only interval theorem are predecessor work, not replay targets. + +## Model + +Let X be a finite collection of sources and Y a disjoint collection of +targets. Every field starts with arbitrary data. Fix a list of nonzero +dyadic contributions, indexed by e, + + Y_t(e) <- Y_t(e) + q_e X_s(e), q_e = o_e 2^v_e, + +where o_e is a signed odd integer and v_e is an integer. Parallel list +entries count separately. Each listed contribution executes exactly once, +in any order. No other ADDs, role mixing, scratch, or factorizations are +allowed. Sources never receive contributions. Targets never supply them. + +Each role may undergo any finite sequence of positive power-of-two SCALEs. +Its integer gauge starts and ends at zero. With current source and target +gauges a_s and b_t, the physical ADD coefficient must be + + q_e 2^(b_t-a_s). + +SCALE by 2^h costs 2|h|. The retained #4518 tariff for a nonzero ADD is + + c(o) + 2|v|, c(o) = 2(2 + bit_length(|o|) + popcount(|o|)). + +Thus the charged cost of a schedule is + + C + 2 sum_roles TV(g_role) + + 2 sum_e |v_e + b_t(e) - a_s(e)|, (1) + +where C=sum_e c(o_e). Gauge paths have zero endpoints, and TV includes both +entry and return. Nothing is assumed zero initially. The representation +invariant is X_stored=2^a X_initial and +Y_stored=2^b(Y_initial + sum of completed logical contributions). +It proves exactness of every schedule in this model and full dirty return. + +## Theorem 1: remove every source used at most twice + +For any schedule, erase all SCALEs of a source s used d_s<=2 times, leave +every other gauge path and the ADD order unchanged, and adjust its ADD +coefficients to the displayed representation invariant. The new schedule +has the same exact endpoint and costs no more. + +Proof. Let M=max|a_s| over that source's complete path. Its zero endpoints +imply TV(a_s)>=2M. Erasing its SCALEs saves at least 4M. For each use, + + |v+b| - |v+b-a_s| <= |a_s| <= M. + +Consequently its ADD cost grows by at most 2 d_s M <= 4M. Odd parts are +unchanged. The representation invariant proves the endpoint, including the +restored arbitrary source. This argument does not modify any target gauge +or rely on the timing of another source. Apply it to each such source. QED. + +The same argument removes a target used at most twice. Interchanging the +two gauge variables only changes a sign inside the absolute value. This +observation is used below for the sharpness family. + +## Corollary: an exact optimum with no coupled-source search + +If every source has at most two list entries, the minimum over all coupled +source/target paths equals the target-only minimum + + C + sum_t min_(L<=0<=H) + [4(H-L) + 2 sum_(e:t(e)=t) dist(-v_e,[L,H])]. (2) + +Each endpoint can be chosen among zero and the -v_e incident to that target. +The new implication is Theorem 1. The target-only interval formula and its +attaining walk 0 -> L -> H -> 0 are #4518 Theorem 2, used as a cited premise. +Targets are independent when sources are fixed. Serve them consecutively to +attain the sum, with no extra fields and every entry/return SCALE charged. +Formula (2) covers arbitrary finite graph size, odd parts, valuation sizes, +ADD orders and finite integer gauge paths under the model above. + +## Theorem 2: three uses are the first possible strict gain + +Consider one source and d distinct targets, with every coefficient o 2^v. +For d>=1, the exact coupled optimum is + + d c(o) + 2 min(d,2)|v|. (3) + +The target-only optimum is d c(o)+2d|v|. Hence for d>=3 and v!=0 the exact +gain is 2(d-2)|v|, and the source-use threshold in Theorem 1 is sharp. + +Proof. Remove all target gauges by the symmetric low-use argument. Let M +be the largest absolute source gauge visited. Return costs at least 4M, +and the d ADDs cost at least d c(o)+2d max(|v|-M,0). For M<=|v| the variable +part is 2d|v|+(4-2d)M; for M>=|v| it is at least 4|v|. Minimizing these two +pieces gives (3). With d<=2, use no SCALEs. With d>=2, scale the source to +gauge v, execute all ADDs with coefficient o, and restore it to zero. +These constructions attain the bound. Without source gauges each target +has one contribution, and its return costs cannot improve that direct ADD. + +At d=3, o=1, v=-1, the direct/target-only optimum is 30. Scaling the dirty +source by 1/2, executing three coefficient-one ADDs and scaling it by 2 +costs 2+3*8+2=28. Every source and target retains its required arbitrary-input +endpoint. This is a scalar allowance gain for this star, not an invoice gain +for a complete supplier. QED. + +## Both dual interfaces + +Elementwise inverse-transpose dualization in the same execution order sends +ADD(t,s,q) to ADD(s,t,-q) and SCALE(r,2^h) to SCALE(r,2^-h). It gives the +inverse transpose of the full product and preserves every tariff. This is +the classical Levi homomorphism, used in #4518 Theorem 3. The star's dual +is one target receiving -o 2^v from d distinct sources. Both interfaces +restore every gauge and have the same optimum and dirty-state contract. +The finite checker independently multiplies both physical words. + +## Scope + +This supplies a new source-elimination theorem and an attaining sharpness +family for the declared ADD-once bipartite class. It is not optimality over +general scalar circuits. Repeated use count, source writes, target reads, +borrowing, non-diagonal changes, unreturned gauges, and alternative tariffs +can change the conclusion. The minimum includes a fixed list of ADDs; +coalescing or deleting that list is a separate optimization. + +Ali Romman's PR #5824/#5830 already provide optimal signed representations +on different fixed P104 gauge graphs, using exact cuts and flow certificates. +No global gauge-optimization invention is claimed here. No existing native +word, recursive paid/target histogram, physical precision/tape bill or selected +frontier is changed. All five selected framework assumptions remain. diff --git a/research/low-use-source-gauges/README.md b/research/low-use-source-gauges/README.md new file mode 100644 index 0000000000..8634e0b6fa --- /dev/null +++ b/research/low-use-source-gauges/README.md @@ -0,0 +1,145 @@ +# Source gauges cannot help before the third use + +**Claim type: scoped proof with exact finite corroboration. No new κ.** +This contribution was produced by Nick Petalas. + +In the restored dyadic ADD-once bipartite model of [PROOF.md](PROOF.md), +temporarily scaling sources cannot reduce the optimum if every source is +used at most twice. This holds with arbitrary simultaneous target gauges, +ADD order, integer gauge excursions and arbitrary dirty initial fields. +The optimum reduces to Dugongue's target-only interval formula from +[PR #4518](https://github.com/CrocSwap/integer-mult-bounds/pull/4518). + +Three uses are the first possible strict gain. For one source feeding d +distinct targets with coefficient o 2^v, o signed odd, the exact optimum is + +```text +d c(o) + 2 min(d,2)|v|, +c(o) = 2(2 + bit_length(|o|) + popcount(|o|)). +``` + +The target-only optimum is d c(o)+2d|v|. At d=3, o=1, v=-1, a restored +source scaling gives cost 28, versus the exact target-only minimum 30. +The inverse-dual word has the same cost and full dirty-state correctness. +The star construction is elementary shared-factor extraction. The new +contribution is the elimination theorem, its exact coupled optimum and +sharp source-use threshold under this schedule contract. + +The proof erases a source's gauges, saving at least four times its maximum +absolute gauge. Each incident ADD can lose at most twice that maximum. +At two uses the saving covers the entire possible loss. This supplies a +pruning rule for the coupled source/target question in #4518 Open next +question 2. A single row with distinct sources is an immediate special case. + +## Reproduce + +CPython 3.12, standard library only, from the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -X dev -I -B research/low-use-source-gauges/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -X dev -I -O -B research/low-use-source-gauges/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/low-use-source-gauges +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/low-use-source-gauges --check-source-history +``` + +Another CPython 3.12 path may replace the one shown. Direct replay prints +`PASS_LOW_USE_SOURCE_GAUGES no_new_kappa` and a freshly generated stdout +receipt binding the package files by SHA256. It writes no files. Registered +replay runs both normal and optimized modes with warnings treated as errors. + +The exact finite checks enumerate: + +- All 256 two-source/two-target lists with each of four pairs absent or + carrying valuation -1, 0 or 1, and fixed alternating odd parts 1 and -3. + A separate Dijkstra oracle searches every ADD order and gauge state in + {-1,0,1}. Coupled and source-fixed minima equal the interval formula. +- 81 prescribed gauge-path fixtures at levels -2, 0, 2, comparing each + original and source-erased program on all arbitrary-input coefficients. +- 18 star shortest-path problems and their 18 reversed-incidence versions, + with one to three leaves, valuations -1, 0, 1 and odd parts -3 or 1; + 51 additional degree-three witnesses with valuations -8 through 8 and + odd parts -3, 1, 5. Reversed stars exercise profitable target gauges while + all sources remain low-use. +- Full physical and inverse-transpose endpoints and tariff equality for + every checked word. Six invalid contracts are rejected. Two further + controls detect wrong coefficient compensation and failure of the + low-use premise at degree three. + +The finite gauge box corroborates the new theorem; it does not prove the +unbounded optimum by enumeration. The written proof carries that quantifier. +The predecessor's native program, counts and scientific suite are not replayed. + +## Scope and sources + +Base `721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision 8. +[SOURCES.json](SOURCES.json) pins the retained #4518 model, tariff, interval +theorem and dualization statement at head +`2b71c89a7ca0ad41f12149d7971e73f16f320e81`. The catalogue and selected +record are historical provenance. Both predecessor files are authenticated +before direct replay. Its mathematical results are cited inputs. + +The scope requires disjoint source/target roles, each listed contribution +once, only positive power-of-two gauge scales, and every gauge returned to +zero. Repeated entries count as repeated uses. Role mixing, factoring the +ADD list, borrowing, source writes, target reads, different prices and +unreturned gauges are outside the result. No actual P104 word is changed. +No paid recursive gain, physical implementation, precision/tape saving, +supplier admission or complete multiplication theorem is claimed. All five +selected framework assumptions remain. Selected cold replay, Lean, Docker, +independent human review and proof-kernel review are unrun. + +Before reservation, live open PRs, recent account PRs, handoff comments, +active Discussions, local locks and main/merged-work searches were checked. +The overlap helper reported complete pagination of 379 open PRs and 5,780 +Discussion records, but only 60 of 8,348 local notes. Searches of main's +README objects and relevant merged PRs supplemented that sparse cache. +These searches do not establish global literature priority. + +Ali Romman's [#5824](https://github.com/CrocSwap/integer-mult-bounds/pull/5824) +and [#5830](https://github.com/CrocSwap/integer-mult-bounds/pull/5830) already +optimize different fixed P104 representation graphs with exact flow duals; +[#5783](https://github.com/CrocSwap/integer-mult-bounds/pull/5783) supplies +related exact binary-cut tooling. Richard Hoekstra's +[#1235](https://github.com/CrocSwap/integer-mult-bounds/pull/1235) normalizes +endpoint gauge tours in a different rank-priced phase model. None is an +audit target or an executable dependency here. No new general gauge, +shared-factor, shortest-path or flow algorithm is claimed. + +## Open next questions + +Which sources with at least three uses in a named complete native window +admit a profitable restored gauge after all surrounding interfaces are +charged? Start by extracting one ADD-once bipartite window and its existing +target-only optimum, then remove low-use source variables with this theorem. +The remaining emitted-window, caller, native and precision/tape contracts +block physical adoption. The present package stops at the sharp threshold. + +## Verification design + +The verifier is a separate standard-library implementation and imports no +predecessor code. Its finite domain enforces at most four roles, four ADDs, +valuation magnitude eight and 1,000 events. The oracle has at most 1,296 +states and 15,553 heap pops, with parent reconstruction bounded by the state +count. Other enumerations have literal finite products. Functions have +fewer than 60 lines. Explicit exception-based invariants remain active under +`-O`; all arithmetic is exact. No recursion, runtime code generation or +external solver is used. + +Power-of-Ten rule 3 has a managed-runtime deviation in `verify.py`: CPython, +Fraction and heap/dictionary operations allocate during execution. The +enforced capacities bound live state and rational sizes; no retained +external resources or output files exist. Static input sizes and the finite +loop bounds compensate for the lack of allocation-free Python operation. +A fixed-storage implementation would be needed for an allocation-free +runtime; that is outside this scientific check. Warning-strict normal and +optimized runs are the available local diagnostics. + +## Credit + +Credit David Ganz / Dugongue for #4518's native dyadic tariff, target-only +interval theorem, emitted interfaces and coupled-path question. Its +PR #4502/#4505 borrowed-adapter and native lineage retain their attribution. +The Levi inverse-transpose identity is classical and used as in #4518. +Credit Ali Romman and Richard Hoekstra for the related gauge work above. +New work is Apache-2.0. Independent human and formal proof-kernel review +are unclaimed. diff --git a/research/low-use-source-gauges/SOURCES.json b/research/low-use-source-gauges/SOURCES.json new file mode 100644 index 0000000000..8fbf8bb5b7 --- /dev/null +++ b/research/low-use-source-gauges/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/levi-adaptive-gauges/PROOF.md", + "usage": "input", + "git_blob": "78ce6bc0a8797934bc6906336bf1d5a9fb37f99a", + "sha256": "4bd623c249866389837591edb3972a6456570e83aa82354d1905914de3b74d4c" + }, + { + "path": "research/levi-adaptive-gauges/README.md", + "usage": "input", + "git_blob": "577b69b92b9d71330c7d80e5ee56faaa55e04318", + "sha256": "b3ed2bffa4b3c6d9d530c45b9f8516820edc02663ca5723089040bb9006552d7" + } + ] +} diff --git a/research/low-use-source-gauges/TASK.json b/research/low-use-source-gauges/TASK.json new file mode 100644 index 0000000000..3cab03249d --- /dev/null +++ b/research/low-use-source-gauges/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a changed helper inventory earn productive credit that survives completion, compilation and the actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Specify all arbitrary inputs, owned fields, restored outputs and a physically legal consumer. Compare complete P and T, including target debits and precision/stock costs. #5599 is a positive control for target refinement, not permission to split every helper for free. #5614 is a hypothetical compiler budget, not an emitted 145-split word. Stop at the first unpaid boundary or a failing optimistic full bill.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "productive helper", + "target refinement", + "5599", + "5614" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove elimination of fully restored source gauges at at most two uses in ADD-once bipartite dyadic shears, and the sharp degree-three threshold with an exact star cost.", + "scope_change_reason": "Takes Open next question 2 of PR4518 about coupled source/target paths. This is a scalar schedule-class obstruction and sharpness result, not a new helper supplier or paid-profile improvement.", + "bottleneck_link": "Removes an infinite coupled-source gauge search for low-use shear sources. A three-use star proves the pruning threshold is sharp; native integration and the complete recursive bill remain separate.", + "budget_minutes": 60, + "stop_rule": "Package the source-elimination theorem and first sharpness witness, then stop. Do not extend the native word or search higher-degree networks.", + "outcome": "completed", + "evidence": "PROOF.md; direct and registered verify.py print PASS_LOW_USE_SOURCE_GAUGES with enumerated finite controls and a SHA256-bound stdout receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which sources with at least three uses in a named complete native window admit a profitable restored gauge after all surrounding interfaces are charged?", + "why_it_matters": "The theorem excludes low-use sources but does not decide the remaining coupled-source optimization or a full supplier invoice.", + "first_step": "Extract one bipartite ADD-once window and its existing target-only optimum, prune sources of degree at most two by this theorem, and price one remaining source path including entry and return.", + "blocked_by": "A complete emitted-window contract, caller compatibility, both orientations, native and precision/tape bills are needed for adoption." + } + ] +} diff --git a/research/low-use-source-gauges/VERIFY.json b/research/low-use-source-gauges/VERIFY.json new file mode 100644 index 0000000000..f14aba90ed --- /dev/null +++ b/research/low-use-source-gauges/VERIFY.json @@ -0,0 +1,41 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/levi-adaptive-gauges/PROOF.md", + "research/levi-adaptive-gauges/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-X", + "dev", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "New coupled-gauge source-elimination theorem: exact bounded shortest paths, full arbitrary-input matrix and inverse-dual endpoints, sharp star witnesses, invalid-contract and changed-premise controls; source authentication." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-X", + "dev", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "New coupled-gauge source-elimination theorem: exact bounded shortest paths, full arbitrary-input matrix and inverse-dual endpoints, sharp star witnesses, invalid-contract and changed-premise controls; source authentication." + } + ] +} diff --git a/research/low-use-source-gauges/verify.py b/research/low-use-source-gauges/verify.py new file mode 100644 index 0000000000..aa94cd08d3 --- /dev/null +++ b/research/low-use-source-gauges/verify.py @@ -0,0 +1,294 @@ +"""Exact finite controls for the low-use source-gauge theorem; no writes.""" + +from __future__ import annotations + +import hashlib +import heapq +import itertools +import json +import platform +from fractions import Fraction +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +MAX_ROLES = 4 +MAX_EDGES = 4 + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def power(exponent: int) -> Fraction: + require(type(exponent) is int and abs(exponent) <= 32, "bad exponent") + return Fraction(2**exponent) if exponent >= 0 else Fraction(1, 2**-exponent) + + +def tariff(value: Fraction) -> int: + require(value != 0 and value.denominator.bit_count() == 1, "not dyadic") + numerator = abs(value.numerator) + trailing = (numerator & -numerator).bit_length() - 1 + odd = numerator >> trailing + valuation = trailing - (value.denominator.bit_length() - 1) + return 2 * (2 + odd.bit_length() + odd.bit_count() + abs(valuation)) + + +def validate(edges: tuple, sources: int, roles: int) -> None: + require(1 <= sources < roles <= MAX_ROLES, "bad role counts") + require(len(edges) <= MAX_EDGES, "too many edges") + for source, target, odd, valuation in edges: + require(0 <= source < sources <= target < roles, "not bipartite") + require(type(odd) is int and odd != 0 and odd % 2 != 0, "bad odd part") + require(type(valuation) is int and abs(valuation) <= 8, "bad valuation") + + +def identity(size: int) -> list[list[Fraction]]: + return [[Fraction(i == j) for j in range(size)] for i in range(size)] + + +def compile_word(edges: tuple, events: list, sources: int, roles: int) -> tuple: + validate(edges, sources, roles) + require(len(events) <= 1000, "event capacity") + gauges = [0] * roles + used = [0] * len(edges) + physical = [] + cost = 0 + for kind, index, delta in events: + if kind == "S": + require(0 <= index < roles, "scale role") + coefficient = power(delta) + gauges[index] += delta + physical.append(("S", index, index, coefficient)) + cost += 2 * abs(delta) + else: + require(kind == "A" and 0 <= index < len(edges), "unknown event") + source, target, odd, valuation = edges[index] + coefficient = odd * power(valuation + gauges[target] - gauges[source]) + physical.append(("A", target, source, coefficient)) + used[index] += 1 + cost += tariff(coefficient) + require(gauges == [0] * roles, "gauge not restored") + require(used == [1] * len(edges), "contribution multiplicity") + return physical, cost + + +def replay(physical: list, roles: int) -> list: + matrix = identity(roles) + require(len(physical) <= 1000, "physical word capacity") + for kind, target, source, coefficient in physical: + if kind == "S": + matrix[target] = [coefficient * x for x in matrix[target]] + else: + matrix[target] = [x + coefficient * y + for x, y in zip(matrix[target], matrix[source])] + return matrix + + +def check_endpoint(edges: tuple, events: list, sources: int, roles: int) -> int: + physical, cost = compile_word(edges, events, sources, roles) + expected = identity(roles) + inverse_transpose = identity(roles) + for source, target, odd, valuation in edges: + coefficient = odd * power(valuation) + expected[target][source] += coefficient + inverse_transpose[source][target] -= coefficient + require(replay(physical, roles) == expected, "wrong full endpoint") + dual = [(kind, source if kind == "A" else target, + target if kind == "A" else source, + -q if kind == "A" else 1 / q) + for kind, target, source, q in physical] + require(replay(dual, roles) == inverse_transpose, "wrong dual endpoint") + dual_cost = sum(tariff(q) if kind == "A" else 2 * abs( + q.numerator.bit_length() - q.denominator.bit_length()) + for kind, _, _, q in dual) + require(dual_cost == cost, "dual tariff differs") + return cost + + +def interval_cost(edges: tuple, roles: int) -> int: + total = sum(tariff(odd * power(v)) - 2 * abs(v) + for _, _, odd, v in edges) + for target in range(roles): + values = [-v for _, t, _, v in edges if t == target] + points = sorted({0, *values}) + candidates = [4 * (high - low) + 2 * sum( + max(low - s, 0, s - high) for s in values) + for low in points for high in points if low <= 0 <= high] + total += min(candidates) + return total + + +def relax(state: tuple, value: int, event: tuple, previous: tuple, + distances: dict, parents: dict, heap: list) -> None: + if value < distances.get(state, 10**9): + distances[state] = value + parents[state] = (previous, event) + heapq.heappush(heap, (value, state)) + + +def shortest(edges: tuple, sources: int, roles: int, coupled: bool) -> tuple: + """Independent bounded gauge-state oracle, gauges in {-1,0,1}.""" + validate(edges, sources, roles) + require(all(abs(edge[3]) <= 1 for edge in edges), "oracle valuation") + start = (0, (0,) * roles) + goal = ((1 << len(edges)) - 1, start[1]) + distances, parents, heap = {start: 0}, {}, [(0, start)] + capacity = (1 << len(edges)) * 3**roles + pop_limit = 1 + capacity * (2 * roles + len(edges)) + for _ in range(pop_limit): + require(bool(heap), "oracle exhausted") + value, state = heapq.heappop(heap) + if value != distances[state]: + continue + if state == goal: + return value, reconstruct(parents, start, goal, capacity) + mask, gauges = state + for role in range(0 if coupled else sources, roles): + for delta in (-1, 1): + if abs(gauges[role] + delta) <= 1: + changed = list(gauges) + changed[role] += delta + relax((mask, tuple(changed)), value + 2, + ("S", role, delta), state, distances, parents, heap) + for index, (source, target, odd, valuation) in enumerate(edges): + if not (mask >> index) & 1: + cost = tariff(odd * power(valuation + gauges[target] - gauges[source])) + relax((mask | (1 << index), gauges), value + cost, + ("A", index, 0), state, distances, parents, heap) + raise ValueError("oracle pop bound") + + +def reconstruct(parents: dict, start: tuple, goal: tuple, capacity: int) -> list: + events = [] + state = goal + for _ in range(capacity): + if state == start: + return list(reversed(events)) + state, event = parents[state] + events.append(event) + raise ValueError("parent path bound") + + +def matrix_census() -> dict: + count = 0 + pairs = tuple(itertools.product(range(2), range(2, 4))) + for options in itertools.product((None, -1, 0, 1), repeat=4): + edges = tuple((source, target, (-3 if i % 2 else 1), v) + for i, ((source, target), v) in enumerate(zip(pairs, options)) + if v is not None) + coupled, events = shortest(edges, 2, 4, True) + fixed, _ = shortest(edges, 2, 4, False) + expected = interval_cost(edges, 4) + require(coupled == fixed == expected, "low-use optimum differs") + require(check_endpoint(edges, events, 2, 4) == coupled, "cost mismatch") + normalized = [e for e in events if e[0] != "S" or e[1] >= 2] + require(check_endpoint(edges, normalized, 2, 4) <= coupled, + "source erasure increased cost") + count += 1 + return {"matrix_instances": count} + + +def path_controls() -> int: + edges = ((0, 2, 1, -1), (1, 2, -3, 1), (0, 3, 3, 1), (1, 3, 1, -1)) + count = 0 + for gauges in itertools.product((-2, 0, 2), repeat=4): + events = [("S", r, g) for r, g in enumerate(gauges) if g] + events += [("A", index, 0) for index in (3, 0, 2, 1)] + events += [("S", r, -g) for r, g in enumerate(gauges) if g] + cost = check_endpoint(edges, events, 2, 4) + reduced = [e for e in events if e[0] != "S" or e[1] >= 2] + require(check_endpoint(edges, reduced, 2, 4) <= cost, "path removal") + count += 1 + return count + + +def star_controls() -> dict: + oracle_count = 0 + witnesses = 0 + sharp = {} + for degree, valuation, odd in itertools.product(range(1, 4), range(-1, 2), (-3, 1)): + edges = tuple((0, target, odd, valuation) for target in range(1, degree + 1)) + base = degree * tariff(Fraction(odd)) + expected = base + 2 * min(degree, 2) * abs(valuation) + coupled, events = shortest(edges, 1, degree + 1, True) + fixed, _ = shortest(edges, 1, degree + 1, False) + require(coupled == expected, "star coupled optimum") + require(fixed == base + 2 * degree * abs(valuation), "star fixed optimum") + require(check_endpoint(edges, events, 1, degree + 1) == expected, "star word") + if degree == 3 and valuation == -1 and odd == 1: + sharp = {"sharp_star_target_only_cost": fixed, "sharp_star_coupled_cost": coupled} + reverse = tuple((source, degree, odd, valuation) for source in range(degree)) + reverse_coupled, reverse_events = shortest(reverse, degree, degree + 1, True) + reverse_fixed, _ = shortest(reverse, degree, degree + 1, False) + require(reverse_coupled == reverse_fixed == interval_cost(reverse, degree + 1) + == expected, "reversed star source elimination") + require(check_endpoint(reverse, reverse_events, degree, degree + 1) == expected, + "reversed star endpoint") + oracle_count += 1 + for valuation, odd in itertools.product(range(-8, 9), (-3, 1, 5)): + edges = tuple((0, target, odd, valuation) for target in range(1, 4)) + events = [("S", 0, valuation)] + [("A", i, 0) for i in range(3)] + events += [("S", 0, -valuation)] + cost = check_endpoint(edges, events, 1, 4) + require(cost == 3 * tariff(Fraction(odd)) + 4 * abs(valuation), "star family") + witnesses += 1 + require(bool(sharp), "missing sharpness fixture") + return {"star_oracle_instances": oracle_count, "reversed_star_oracle_instances": oracle_count, + "star_witnesses": witnesses, **sharp} + + +def rejection_controls() -> int: + failures = 0 + invalid_edges = [((0, 0, 1, 0),), ((0, 1, 2, 0),), ((0, 1, 1, 9),)] + for edges in invalid_edges: + try: + validate(edges, 1, 2) + except ValueError: + failures += 1 + try: + tariff(Fraction(1, 3)) + except ValueError: + failures += 1 + for events in ([], [("A", 0, 0), ("S", 0, 1)]): + try: + compile_word(((0, 1, 1, 0),), events, 1, 2) + except ValueError: + failures += 1 + require(failures == 6, "invalid contract accepted") + edges = tuple((0, target, 1, -1) for target in range(1, 4)) + events = [("S", 0, -1)] + [("A", i, 0) for i in range(3)] + [("S", 0, 1)] + normalized = [e for e in events if e[0] != "S"] + require(check_endpoint(edges, normalized, 1, 4) > check_endpoint(edges, events, 1, 4), + "degree-three premise control") + physical, _ = compile_word(edges, events, 1, 4) + broken = [(kind, t, s, q / 2 if kind == "A" else q) + for kind, t, s, q in physical] + require(replay(broken, 4) != replay(physical, 4), "wrong compensation survived") + return failures + 2 + + +def authenticate_sources() -> None: + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + for row in manifest["files"]: + if row["usage"] == "input": + data = (PACKAGE.parent.parent / row["path"]).read_bytes() + require(hashlib.sha256(data).hexdigest() == row["sha256"], "source drift") + + +def main() -> None: + authenticate_sources() + result = matrix_census() + result["gauge_path_fixtures"] = path_controls() + result.update(star_controls()) + result["rejection_controls"] = rejection_controls() + result["python"] = platform.python_version() + result["package_sha256"] = { + path.name: hashlib.sha256(path.read_bytes()).hexdigest() + for path in sorted(PACKAGE.iterdir()) if path.is_file()} + print(json.dumps(result, sort_keys=True, indent=2)) + print("PASS_LOW_USE_SOURCE_GAUGES no_new_kappa") + + +if __name__ == "__main__": + main()