From 4a940386c07eab4dd4aebcb6ed65462abeb1bda7 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 22:50:57 +0100 Subject: [PATCH] feat(research): prove exact monotone UT3 rank tariffs --- research/ut3-monotone-rank-tariff/README.md | 234 ++++++++++++++++ .../ut3-monotone-rank-tariff/SOURCES.json | 30 +++ research/ut3-monotone-rank-tariff/TASK.json | 70 +++++ research/ut3-monotone-rank-tariff/VERIFY.json | 34 +++ research/ut3-monotone-rank-tariff/verify.py | 249 ++++++++++++++++++ 5 files changed, 617 insertions(+) create mode 100644 research/ut3-monotone-rank-tariff/README.md create mode 100644 research/ut3-monotone-rank-tariff/SOURCES.json create mode 100644 research/ut3-monotone-rank-tariff/TASK.json create mode 100644 research/ut3-monotone-rank-tariff/VERIFY.json create mode 100644 research/ut3-monotone-rank-tariff/verify.py diff --git a/research/ut3-monotone-rank-tariff/README.md b/research/ut3-monotone-rank-tariff/README.md new file mode 100644 index 0000000000..ac6dd3ff8e --- /dev/null +++ b/research/ut3-monotone-rank-tariff/README.md @@ -0,0 +1,234 @@ +# Exact monotone rank tariffs for central UT3 block calls + +This scoped proof removes the concavity requirement from the common-price +version of the UT3 block-call tariff. Every nonnegative nondecreasing rank +price has an exact finite integer-partition optimum, attained on the target +roles alone. Arbitrarily many restored dirty roles cannot lower that optimum. +There is no new kappa or physical supplier claim. + +The first nonconcave fixture has five central targets, rank cap four, and +complete call price `tau(d)=5+d^2` for either letter. Its exact bill is **90**, +attained by ten rank-two calls. The earlier six-call constructions cost 98 +and 102 under this same hypothetical price. This comparison changes the +abstract price, not an admitted supplier's recursive profile. + +This contribution is produced by Nick Petalas. New work is Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +## Model and exact theorem + +Keep Arham Tahir's [PR1919](https://github.com/CrocSwap/integer-mult-bounds/pull/1919) +alphabet. In `G=UT3(F2)`, write + +``` +(u,v,z)(U,V,Z) = (u+U,v+V,z+Z+uV), +a=(1,0,0), b=(0,1,0), c=abab=(0,0,1). +``` + +For arbitrary finite integers `r>=w>=1` and `k>=1`, paid calls in +`M_r(F2[G])` are `D_N(g)=I+([g]+1)N`, with `g` equal to `a` or `b` and +`1<=rank_F2(N)<=k`. The binary matrix `N` need not be idempotent. Every +factor is an involution because `([g]+1)^2=0`. The full required endpoint is +`diag([c] repeated w, 1 repeated r-w)`. All inputs, including spectators, +are arbitrary. All off-diagonal coefficients must vanish, and every +spectator must return. There are no clean ancillas, central-letter calls, +free address maps, erasures or uncharged inverse calls. + +Scalar invertible binary maps are free in this formal model. Conjugation +pushes them to one endpoint while preserving ranks. Augmentation forces +the remaining scalar map to be identity, as in PR1919. This is not a +statement that scalar mixing is free in a physical implementation. + +Let `tau:{0,...,k}->[0,infinity)` be any nondecreasing real function with +`tau(0)=0`. Each nonzero call of either letter costs `tau(rank N)`. +Invocation overhead can be included in positive-rank entries of `tau`. +Concavity, convexity and strict positivity are unnecessary. + +Set `K=min(k,w)`. Define a finite recurrence + +``` +F(0)=0, +F(s)=min_{1<=d<=min(K,s)} (tau(d)+F(s-d)), 1<=s<=2w. +``` + +**Theorem.** The exact minimum complete formal bill is `2 F(2w)`. +Every minimizing partition of `2w` into parts at most `K` gives an +attaining diagonal-projector word, with that rank list for each letter. +No extra roles are needed. The recurrence has `2w` states after its initial +state and at most `2w*K` candidate transitions. + +PR1919 proves rank-volume and affine pricing. Nick Petalas's +[PR2129](https://github.com/CrocSwap/integer-mult-bounds/pull/2129) proves the +concave special case and its loopless-incidence attainment. The new step +here is a monotone truncation lemma that reduces every feasible, possibly +rank-wasteful word to an exact-mass partition without a concavity assumption. +The finite recurrence then gives an attainable optimum, including convex +and nonconvex monotone tables. No predecessor executable is imported or +replayed. + +## Proof + +Use the inherited PR1919 coefficient-span lemma. For either letter in any +valid word, let its positive scalar ranks be `d_1,...,d_m` and `S=sum d_i`. +That lemma gives `S>=2w`. Its zero degree-one coefficient also gives +`sum N_i=0`, so + +``` +d_i = rank(sum_{j!=i} N_j) <= sum_{j!=i} d_j, +thus 2 max(d_i) <= S. +``` + +These are necessary conditions for the original full dirty boundary, for +every finite number of roles and arbitrary noncommuting scalar matrices. +They are cited predecessor results, not new claims here. + +**Monotone truncation lemma.** Suppose a positive integer list has +`S>=2w` and `2 max d_i<=S`. Then it has a coordinatewise smaller list of +nonnegative integers `e_i<=min(d_i,w)` with `sum e_i=2w`. + +To prove this, first clip every entry at `w`. If no entry exceeds `w`, the +sum remains at least `2w`. If at least two exceed `w`, those two clipped +entries alone sum to `2w`. If exactly one entry `d_j` exceeds `w`, all +other entries remain unchanged and sum to at least `d_j>w`, by the rank +triangle inequality. Together with the clipped entry `w`, they still sum +to at least `2w`. Finally remove individual units until the sum is exactly +`2w`. This only decreases entries. The original cap also gives `e_i<=k`. + +Monotonicity and nonnegativity imply +`sum tau(d_i)>=sum tau(e_i)>=F(2w)`, dropping zero entries. Apply this +independently to the two letters. Every valid word therefore costs at +least `2 F(2w)`. This is a relaxation of its rank lists, not an assertion +that one may truncate the original word's matrices and preserve its endpoint. + +For attainment, take any minimizing partition `e_1,...,e_m`. It has total +degree `2w` and maximum at most `w`. The loopless-multigraph construction +credited to PR2129 realizes it as the degrees of a multigraph with `w` +edges. One explicit construction repeatedly joins the two largest positive +remaining degrees, then decrements both. With `h` edges remaining, the +degree sum is `2h` and maximum at most `h`. After this operation, every +unchosen degree is at most `h-1`, since three degrees of size `h` would +exceed `2h`. The two chosen degrees also become at most `h-1`. Induction +finishes the construction in exactly `w` steps. + +Assign one target coordinate to each edge. For each vertex `i`, let `P_i` +be the diagonal projector onto its incident edges, extended by zero on all +spectators. Execute an `a` call and then a `b` call on each `P_i`. Every +target belongs to exactly two distinct vertices, so sees `a,b,a,b`, whose +endpoint is `c`. Every spectator sees identity. All factors are diagonal, +so there are no off-diagonal couplings. Each letter has the chosen rank +list and costs `F(2w)`. This proves the full formal endpoint and equality +in the bound for every finite `r,w,k`. + +## First improvement and stopping point + +At `w=5,k=4,tau(d)=5+d^2`, the minimizing per-letter ranks are +`(2,2,2,2,2)` and the complete bill is `2*5*9=90`. +The old balanced list `(4,3,3)` costs `2*(21+14+14)=98`; the old +concentrated list `(4,4,2)` costs `2*(21+21+9)=102`. +For a short exact lower certificate, each of the four allowed ranks obeys +`5+d^2 >= (9/2)d`, with equality at rank two. The inherited rank mass of +at least ten per letter therefore forces the complete price to be at least 90. +These are the displayed lists from PR1919 and PR2129, priced here, rather +than independent reconstructions of their receipts. The finite recurrence +enumerates every allowable exact-mass partition, including longer words. +The written theorem excludes cheaper words with excess rank mass as well. + +This is the first verified extension. Stop here. Neither the abstract price +table nor the saving of eight establishes a physical or recursive gain. + +## Evidence and reproduction + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/ut3-monotone-rank-tariff +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/ut3-monotone-rank-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/ut3-monotone-rank-tariff/verify.py +``` + +Both direct modes print `PASS_UT3_MONOTONE_RANK_TARIFF no_new_kappa` and a +generated receipt binding every package file by SHA256. They write nothing. +The exact evidence is: + +- 736 formal construction fixtures, `w=1..16`, `k=1..w+3`, and four rational + price families, with two restored dirty roles per fixture. +- 6,368 complete basis columns in an independently coded faithful regular + action, forward and inverse, for the subdomain `w<=6,k<=w+2`. +- 766 nondecreasing integer price tables with values in `{0,1,2,3}`, + `w=1..5,k=1..w+2`. An independent exhaustive partition iterator agrees + with the dynamic program for every table. +- 2,010 rank lists in that domain with total mass `2w..2w+4` satisfying + the rank triangle. Their clipped lists and prices satisfy the new lemma + for every enumerated table for that `w,k`. +- 18 rejection controls, including each of the ten omitted calls in the + new fixture, dirty leakage, negative/decreasing prices, invalid degree + data, missing zero-sum constraints and domain/capacity errors. + +The finite fixtures corroborate the written arbitrary-size proof. They are +not a census of all formal words, a proof-kernel certificate or a full +multiplication theorem. The standalone checker needs no Git or predecessor +files; metadata authenticates historical provenance separately. + +## Scope, cost ledger and implementation bounds + +The boundary, formal prices and complete rank-call bill above are proved. +Native realization, scalar mixing costs, frames, routing, hosting, physical +storage, precision/tape, recursive child-rank identification and a complete +consumer are unknown here. Unknown costs are not zero. No physical +implementation campaign, selected cold replay, Lean or Docker run is part +of this package. The selected conditional kappa remains `0.00302015`. + +The task changes `bit-new-register-model` from mechanism exploration to a +formal nonlinear-pricing side result. PR1974's GL3 census and PR2027's UT4 +tariff use different groups and hypotheses; this package does not claim to +escape either result or provide a native operation alphabet. The current +selected source-binding control passed; the card's historical baseline +command is replaced by `scripts/research_selected_baseline.py` as current +guidance requires. No scientific predecessor replay was used as a deliverable. + +`verify.py` uses finite domains: at most 32 targets and cap 35 in the +optimizer, at most 16 targets in fixtures, and total at most 16 in partition +probes. All functions are below 60 lines. Checks use exceptions and remain +active under `-O`; no recursion, subprocess, network or file writes occur. +File reads only hash package sources. Python-managed integer, +tuple and list allocation is a Power-of-Ten rule-3 deviation, confined to +these fixed small domains, with no hard real-time allocation claim. Rule 9 +has a bounded synchronous exception-control callback set. Warning-strict +normal and optimized runs are the available recurring Python diagnostics; +no separate linter is installed. Larger domains would require a fresh +capacity/diagnostic review rather than removal of these limits. + +## Open next questions + +- Can different nonproportional monotone prices for `a` and `b` attain both + independent partition optima simultaneously? The separate lower bounds + follow, but the construction here uses one shared degree list. First find + a pair of tables with incompatible minimizing degree lists and write a + complete alternating-incidence word or an obstruction. Attainability is + the unresolved step. +- Can an actual native interface realize the ten-call rank-two fixture + more cheaply than its six-call comparator? First price both whole + boundaries with scalar work, frames, setup, restoration, hosting and + precision. A native realization and the connection between scalar rank + and recursive child rank are missing; the abstract saving cannot supply + them. + +## Sources, overlap and credit + +Scientific base is canonical main +`624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7. +`SOURCES.json` pins the retained PR1919 and PR2129 READMEs as provenance. +Credit Arham Tahir for PR1919's rank cap, affine bill and nonlinear-pricing +gap; steph4n-gh/PR1573, Arham Tahir/PR1589, Hanson Sun/PR1607 and Josie +Elliston/PR1792 for the coefficient/rank and model lineage; and Nick +Petalas/PR2129 for the concave tariff and loopless-incidence attainment. +Their credit and source files are unchanged. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133304) +records the new question. Entry overlap covered 365 open PRs and 3,817 +Discussion records, paginated at 21:44 UTC on 2026-10-22. Local notes were +sparse, so distinctive searches also read all matching main-branch READMEs +through Git and live merged-PR searches. The last-hour handoff posts from +this account and all UT3 candidate PR titles/bodies were checked. Closed +diffs, arbitrary nested files and unpublished work remain outside this +coverage. No novelty guarantee follows from a lack of matches. diff --git a/research/ut3-monotone-rank-tariff/SOURCES.json b/research/ut3-monotone-rank-tariff/SOURCES.json new file mode 100644 index 0000000000..6bbd70d95c --- /dev/null +++ b/research/ut3-monotone-rank-tariff/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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/ut3-rank-bounded-block-calls/README.md", + "usage": "provenance", + "git_blob": "dc0d1bac91fcebecc9fed4e8c3d26a11acca3ef5", + "sha256": "822574c7040b5571d729960951425a1ad9742ae8541a2af2882733f952975b5d" + }, + { + "path": "research/ut3-concave-rank-tariff/README.md", + "usage": "provenance", + "git_blob": "28526ec86ed833f345247c67718fa151fe2a039f", + "sha256": "33244a1263261475f549c57e5714921e97eba29fc3c7ab0eaaccacb18cc16fa1" + } + ] +} diff --git a/research/ut3-monotone-rank-tariff/TASK.json b/research/ut3-monotone-rank-tariff/TASK.json new file mode 100644 index 0000000000..65bbf96bd7 --- /dev/null +++ b/research/ut3-monotone-rank-tariff/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact common nonnegative monotone rank tariff for central UT3 block calls with arbitrary restored dirty workspace.", + "scope_change_reason": "The selected card explores new alphabets. This answers the nonlinear-pricing gap in Arham Tahir PR1919, beyond the concave special case PR2129, as a formal pricing side result rather than a native mechanism.", + "bottleneck_link": "An exact paid-call optimizer screens proposed nonlinear interfaces. Scalar coupling rank is not an admitted recursive child rank; no selected moment gain follows.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified extension and one nonconcave fixture; do not expand into a native implementation or further tariff families.", + "outcome": "completed", + "evidence": "Written arbitrary-size monotone truncation theorem; verify.py enumerates 766 price tables, 2010 relaxed rank lists, 736 constructions, 6368 faithful regular basis columns and 18 rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can nonproportional letter-specific monotone tariffs attain both independent partition minima?", + "why_it_matters": "It would price asymmetric complete interfaces.", + "first_step": "Choose two tables with incompatible minimizing rank partitions, then construct an alternating-incidence word or prove an obstruction.", + "blocked_by": "The current attaining construction uses one common rank partition." + }, + { + "question": "Can a native complete interface realize a gain for the ten-call rank-two fixture?", + "why_it_matters": "Only a physical cost comparison could affect a recursive supplier.", + "first_step": "Price both whole dirty boundaries including scalar work, frames, setup, restoration, hosting and precision.", + "blocked_by": "No native realization or recursive-child interpretation is provided." + } + ] +} diff --git a/research/ut3-monotone-rank-tariff/VERIFY.json b/research/ut3-monotone-rank-tariff/VERIFY.json new file mode 100644 index 0000000000..411ac00a45 --- /dev/null +++ b/research/ut3-monotone-rank-tariff/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": "Exact partition optimum, monotone truncation, full dirty formal/faithful endpoints and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete checks with interpreter assertions disabled." + } + ] +} diff --git a/research/ut3-monotone-rank-tariff/verify.py b/research/ut3-monotone-rank-tariff/verify.py new file mode 100644 index 0000000000..49bce8289c --- /dev/null +++ b/research/ut3-monotone-rank-tariff/verify.py @@ -0,0 +1,249 @@ +"""Exact monotone UT3 pricing and full dirty-input construction controls.""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations_with_replacement +import json +from pathlib import Path + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def optimum(w, k, prices): + """Return the exact per-letter price and an attaining rank partition.""" + need(type(w) is int and 1 <= w <= 32, "target bound") + need(type(k) is int and 1 <= k <= 35, "rank-cap bound") + need(len(prices) == k + 1 and prices[0] == 0, "price domain") + need(all(0 <= prices[d - 1] <= prices[d] for d in range(1, k + 1)), + "nonnegative monotone prices required") + cap = min(w, k) + best = [(Fraction(0), ())] + for mass in range(1, 2 * w + 1): + choices = [] + for d in range(1, min(mass, cap) + 1): + cost, parts = best[mass - d] + choices.append((cost + prices[d], tuple(sorted(parts + (d,))))) + best.append(min(choices)) + cost, parts = best[-1] + need(sum(parts) == 2 * w and max(parts) <= cap, "partition contract") + return cost, parts + + +def partitions(total, cap): + """Enumerate every nonincreasing partition in a bounded probe domain.""" + need(1 <= total <= 16 and 1 <= cap <= 9, "partition probe bound") + stack = [((), total, cap)] + for _ in range(1 << total): + if not stack: + return + prefix, remaining, largest = stack.pop() + if remaining == 0: + yield prefix + else: + for d in range(1, min(remaining, largest) + 1): + stack.append((prefix + (d,), remaining - d, d)) + need(not stack, "partition work budget exhausted") + + +def truncate(parts, w): + """The new lower-bound reduction, applied to a feasible rank list.""" + total = sum(parts) + need(parts and min(parts) >= 1 and total >= 2 * w, "rank mass") + need(2 * max(parts) <= total, "zero-sum rank triangle") + clipped = [min(d, w) for d in parts] + need(sum(clipped) >= 2 * w, "clipping lemma") + excess = sum(clipped) - 2 * w + for i, d in enumerate(clipped): + removed = min(d, excess) + clipped[i] -= removed + excess -= removed + answer = tuple(d for d in clipped if d) + need(excess == 0 and sum(answer) == 2 * w, "exact truncation mass") + return answer + + +def supports(parts, w): + """The credited loopless-incidence construction, with explicit invariants.""" + need(parts and sum(parts) == 2 * w and max(parts) <= w, "graph degrees") + remaining = list(parts) + rows = [0] * len(parts) + for coordinate in range(w): + order = sorted(range(len(parts)), key=lambda i: (-remaining[i], i)) + left, right = order[:2] + need(remaining[right] > 0, "two distinct incident vertices") + for vertex in (left, right): + remaining[vertex] -= 1 + rows[vertex] |= 1 << coordinate + edges_left = w - coordinate - 1 + need(sum(remaining) == 2 * edges_left, "remaining graph degree mass") + need(max(remaining) <= edges_left, "remaining graph degree maximum") + need(tuple(row.bit_count() for row in rows) == parts, "support ranks") + return tuple(rows) + + +def group_product(left, right): + """Triple UT3 law, used only by the formal endpoint engine.""" + u, v, z = left + a, b, c = right + return u ^ a, v ^ b, z ^ c ^ (u & b) + + +def formal_endpoint(rows, roles): + endpoint = [(0, 0, 0)] * roles + for support in rows: + for label in ((1, 0, 0), (0, 1, 0)): + for role in range(roles): + if support >> role & 1: + endpoint[role] = group_product(label, endpoint[role]) + return tuple(endpoint) + + +def literal_call(state, support, letter): + """Independent faithful regular action on every address of every role. + + Encode a unitriangular 3 by 3 matrix by address = 4*u + 2*v + z. + Left a changes u and z by 1 and v; left b changes v. The triple-law + helper is deliberately not used in this endpoint oracle. + """ + output = [0] * len(state) + for role in range(len(state) // 8): + for address in range(8): + destination = address + if support >> role & 1: + if letter == "a": + destination = address ^ 4 ^ ((address >> 1) & 1) + else: + need(letter == "b", "letter domain") + destination = address ^ 2 + output[8 * role + destination] ^= state[8 * role + address] + return tuple(output) + + +def regular_check(rows, w, roles, omitted=None, leak=False): + calls = [(row, letter) for row in rows for letter in ("a", "b")] + if omitted is not None: + calls = calls[:omitted] + calls[omitted + 1:] + if leak: + calls.append((1 << w, "a")) + columns = 0 + for source in range(8 * roles): + basis = tuple(int(i == source) for i in range(8 * roles)) + state = basis + for row, letter in calls: + state = literal_call(state, row, letter) + role, address = divmod(source, 8) + target = 8 * role + (address ^ int(role < w)) + need(state == tuple(int(i == target) for i in range(8 * roles)), + "full dirty endpoint") + for row, letter in reversed(calls): + state = literal_call(state, row, letter) + need(state == basis, "inverse dirty endpoint") + columns += 1 + return columns + + +def price_families(k): + return ( + tuple(Fraction(0) if d == 0 else Fraction(5 + d * d) + for d in range(k + 1)), + tuple(Fraction(d, d + 1) for d in range(k + 1)), + tuple(Fraction(0) if d == 0 else Fraction(2 + (d + 2) // 3) + for d in range(k + 1)), + tuple(Fraction(d) + Fraction(d >= 3, 2) + Fraction(d >= 5, 3) + for d in range(k + 1)), + ) + + +def construction_checks(): + fixtures = columns = 0 + digest = sha256() + for w in range(1, 17): + for k in range(1, w + 4): + for prices in price_families(k): + cost, parts = optimum(w, k, prices) + rows = supports(parts, w) + expected = ((0, 0, 1),) * w + ((0, 0, 0),) * 2 + need(formal_endpoint(rows, w + 2) == expected, "formal endpoint") + need(sum(prices[row.bit_count()] for row in rows) == cost, + "literal rank price") + digest.update(repr((w, k, cost, parts, rows)).encode()) + fixtures += 1 + if w <= 6 and k <= w + 2: + columns += regular_check(rows, w, w + 2) + return {"formal_fixtures": fixtures, "regular_basis_columns": columns, + "construction_digest": digest.hexdigest()} + + +def partition_checks(): + cases = lists = 0 + for w in range(1, 6): + for k in range(1, w + 3): + exact = tuple(partitions(2 * w, min(w, k))) + relaxed = tuple(parts for mass in range(2 * w, 2 * w + 5) + for parts in partitions(mass, k) + if 2 * max(parts) <= mass) + lists += len(relaxed) + for values in combinations_with_replacement(range(4), k): + prices = (0,) + values + cost, _ = optimum(w, k, prices) + need(cost == min(sum(prices[d] for d in p) for p in exact), + "independent exhaustive integer-partition optimum") + for parts in relaxed: + smaller = truncate(parts, w) + old_price = sum(prices[d] for d in parts) + new_price = sum(prices[d] for d in smaller) + need(cost <= new_price <= old_price, "tariff reduction") + cases += 1 + return {"monotone_price_tables": cases, "relaxed_rank_lists": lists} + + +def rejects(action, message): + try: + action() + except ValueError: + return + raise ValueError("control did not reject: " + message) + + +def controls(): + prices = tuple(0 if d == 0 else 5 + d * d for d in range(5)) + cost, parts = optimum(5, 4, prices) + need(cost == 45 and parts == (2, 2, 2, 2, 2), "first new fixture") + need(sum(prices[d] for d in (4, 3, 3)) == 49, "balanced comparison") + need(sum(prices[d] for d in (4, 4, 2)) == 51, "concentrated comparison") + rows = supports(parts, 5) + rejected = 0 + for call in range(2 * len(rows)): + rejects(lambda: regular_check(rows, 5, 7, omitted=call), "omitted call") + rejected += 1 + rejects(lambda: regular_check(rows, 5, 7, leak=True), "dirty leakage") + rejects(lambda: optimum(2, 3, (0, 2, 1, 3)), "decreasing tariff") + rejects(lambda: optimum(2, 2, (0, -1, 2)), "negative tariff") + rejects(lambda: supports((3, 1), 2), "non-graphical rank list") + rejects(lambda: truncate((4,), 2), "missing zero-sum triangle") + rejects(lambda: optimum(33, 1, (0, 1)), "target capacity") + rejects(lambda: optimum(2, 0, (0,)), "rank capacity") + rejects(lambda: optimum(2, 2, (1, 2, 3)), "charged identity entry") + return {"complete_price": str(2 * cost), "ranks_per_letter": parts, + "balanced_price": 98, "concentrated_price": 102, + "rejection_controls": rejected + 8} + + +def main(): + result = {"claim_type": "scoped proof with exact finite corroboration", + "construction": construction_checks(), + "partition": partition_checks(), "first_fixture": controls()} + package = Path(__file__).resolve().parent + result["source_sha256"] = { + path.name: sha256(path.read_bytes()).hexdigest() + for path in sorted(package.iterdir()) if path.is_file() + } + print(json.dumps(result, indent=2, sort_keys=True)) + print("PASS_UT3_MONOTONE_RANK_TARIFF no_new_kappa") + + +if __name__ == "__main__": + main()