diff --git a/research/shortest-chart-axis-words/README.md b/research/shortest-chart-axis-words/README.md new file mode 100644 index 0000000000..0d6804260d --- /dev/null +++ b/research/shortest-chart-axis-words/README.md @@ -0,0 +1,180 @@ +# Exact shortest chart paths and literal axis words + +This contribution is produced by Nick Petalas. New work is Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +This is a scoped algebraic proof with exact finite corroboration. For two binary +Lagrangian charts at distance r, the shortest chart-path count is + + P(r) = product_(j=1)^r (2^j - 1). + +For charts in a 2n-dimensional ambient space, the number of shortest literal +nonzero-axis words is + + W(n,r) = 2^(r(n-1)) P(r). + +Empty products are one. The minimum length is r. The new executable result is +an exact lexicographic rank/unrank bijection for these words, so a uniform +integer in [0,W(n,r)) gives a uniform shortest literal word. The implementation +accepts 1 <= n <= 6; the written theorem covers every n >= 1. + +The contribution counts syntactically different axis sequences, and separately +counts chart paths. It does not count distinct full symplectic products or +phase-exact Clifford lifts. No native paid-profile improvement, supplier +admission, new kappa or complete multiplication theorem is claimed. + +## Model and predecessors + +Let E be a 2n-dimensional symplectic space over F2 with alternating form omega. +A chart is an n-dimensional isotropic subspace. For nonzero a in E, let +T_a(x) = x + omega(x,a)a. A literal word is an ordered tuple of nonzero axes, +applied from left to right to the current chart. Its endpoint requirement is +T_(a_r) ... T_(a_1) U = V; no action on other charts is prescribed. + +Distance is d(U,V) = n - dim(U intersect V). Chart paths identify axes whenever +they produce the same next chart. Fixed steps and repeated axes are allowed in +the general word alphabet, but cannot occur in a minimum-length word unless +they decrease the remaining distance. + +Dugongue's [PR #4841](https://github.com/CrocSwap/integer-mult-bounds/pull/4841), +head `6debdcdac8fe1c87958f8cd42ccb7db73c0a0eef`, supplies complete single and +paired transvection neighborhoods and the corrected one-step distance test in +`research/native-clifford-gauge-compiler/decoder/CROSS-REVIEW-DYNAMIC.md`. +Cinna Davis's [PR #4690](https://github.com/CrocSwap/integer-mult-bounds/pull/4690) +supplies the Gaussian contact-search setting. Cao Yifan's #4610 supplies its +round-three supplier context; Yiyang's #4710 and the retained native caller +#4713/#4630/#4635 supply the physical and phase obligations. Their constructions +and predecessor notices retain credit. No predecessor executable is imported or +replayed here. The underlying finite symplectic and dual-polar geometry is +classical; no literature-priority claim is intended. The repository contribution +is the explicit shortest-word multiplicity and its exact indexing algorithm. + +## Proof + +Put I = U intersect V and r = n - dim I. + +First, one transvection changes distance to V by at most one. If a belongs to U, +it fixes U. Otherwise H = U intersect a-perp is a hyperplane fixed pointwise by +T_a, so U and T_a U share H. Intersecting this common hyperplane with V shows +that the two intersection dimensions with V differ by at most one. Thus every +word from U to V has length at least r. + +We count distance-decreasing axes directly. If a is outside U+V = I-perp, then +I intersect a-perp has codimension one in I, and no new intersection vector can +appear: T_a x in V with omega(x,a)=1 would imply a = x + T_a x in U+V. Such an +axis increases the distance. For a in U+V, write a=u+v with u in U and v in V. +All of I is fixed. A vector x in U can produce a new intersection vector only +when omega(x,a)=1. Then x+a belongs to V exactly when x belongs to u+I, and on +that coset omega(x,a)=omega(u,v). Consequently a decreases the distance exactly +when omega(u,v)=1. The decomposition is unique up to adding an element of I to +both u and v; this value is independent of that choice. + +The quotient I-perp/I is a symplectic space of dimension 2r. Its subspaces U/I +and V/I are complementary Lagrangians, with a nondegenerate pairing between +them. For each nonzero u-bar in U/I there are exactly 2^(r-1) choices of v-bar +with pairing one. Each quotient axis has 2^(n-r) lifts in I-perp. Therefore for +r > 0 the exact number of distance-decreasing literal axes is + + A(n,r) = (2^r-1) 2^(r-1) 2^(n-r) + = 2^(n-1) (2^r-1). + +This is positive, so repeatedly taking a decreasing axis constructs a word of +length r. Every word of length r reaching V must decrease the remaining distance +at every step. At remaining distance j, there are A(n,j) choices, each followed +by the same number of completions, since that number depends only on n and j-1. +Induction gives + + W(n,r) = product_(j=1)^r A(n,j) = 2^(r(n-1)) P(r). + +For completeness, every changed chart edge U -> U' has exactly 2^(n-1) literal +axis lifts. Let H = U intersect U', of dimension n-1. An axis inducing U' fixes +H pointwise and belongs to H-perp. In the symplectic plane H-perp/H, the two +charts give distinct lines. Of the three nonzero vectors in this binary plane, +exactly the third line's vector induces their interchange; the other two fix +one of the lines. All 2^(n-1) lifts of that vector induce U', and there are no +other axes. Dividing each path's literal lifts by 2^(r(n-1)) gives P(r). + +Finally, sort the decreasing axes by their packed integer labels. Every first +axis has exactly W(n,r-1) completions. Euclidean division of an index by that +block size chooses its first axis and the residual suffix index. Repeat r +times. Conversely, rank adds each chosen axis's position times its suffix block +size. This proves the lexicographic bijection and the uniform-integer sampling +contract. The code supplies the bijection, not a random-number source. + +## Exact evidence and reproduction + +The independent checker generates all isotropic RREF subspaces for n=1,2,3. +It builds chart adjacency by intersection cardinality, without using +transvections, then computes distances and shortest-path counts by breadth-first +dynamic programming. It covers 3, 15 and 135 charts, and all 9, 225 and 18,225 +ordered pairs. Literal first-letter counts are separately enumerated for those +pairs. These finite checks corroborate the theorem; the proof is not an +extrapolation from them. + +For n=1,2 the checker exhausts all 28,386 axis tuples at the minimum lengths and +finds 1,644 successful words. Every successful word is checked against its exact +lexicographic rank and unrank. There are 58 additional round trips through n=6 +and eleven rejection controls. Counts come from the executable enumeration. +For example, transverse n=3 charts have 21 shortest chart paths and 1,344 +shortest literal words; these are included in the all-pairs count certificate. + +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/shortest-chart-axis-words +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/shortest-chart-axis-words/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/shortest-chart-axis-words/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/shortest-chart-axis-words --check-source-history +``` + +Expected verifier status is `PASS_SHORTEST_CHART_AXIS_WORDS`. Each run prints a +machine-generated receipt including all package-file SHA256 hashes. Receipts and +logs should be redirected outside the checkout. No receipt is handwritten or +committed. Python 3.12 and its standard library suffice; the exact local path +above can be replaced by a clean Python 3.12 interpreter. + +The inherited card's historical first command fails at `KeyError: +'complex_profile'` against the current selected schema. The current +`research_selected_baseline.py` source-binding control passes. That failure is +orientation evidence only and is unrelated to this self-contained theorem. + +## Scope, implementation bounds and remaining obligations + +`TASK.json` records a changed scope from larger-rank supplier synthesis to an +exact chart-word counting and indexing result. Efficient exploration can use +these multiplicities to avoid biasing chart-path sampling toward a particular +axis encoding. A profitable supplier would still require a new complete word, +all other incident edge costs, literal phase lifts, dirty restoration, ownership, +compiler, precision and outer admission. Those obligations are unrun here. + +The executable reference implementation intentionally enumerates at most 4^6-1 +axes per step and at most six steps. Charts contain at most 64 vectors. Input +closure/isotropy validation uses at most 4^6 pairs. A choices list retains at most +4^6-1 charts of 64 vectors, so the Python allocation deviation is explicitly +bounded; fixed allocation is not claimed. Functions fit within 60 physical lines; +there is no recursion, dynamic evaluation, network or subprocess execution in +the verifier. Its eleven fixed rejection callbacks are the only varying call +targets. Warning-strict normal and optimized runs retain explicit exception-based +invariants. No external static analyzer or proof-kernel check is claimed. + +Overlap searches included live open PR bodies, recent account publications, +recent handoffs, merged-title searches and distinctive all-main README terms. +Sparse local notes, arbitrary source diffs and unpublished work are outside +complete coverage. The separately reserved cycle-coherent coordinated-neighborhood +question is excluded. This package does not recheck or extend a recent result +from the same account as its target. + +## Open next questions + +1. Can exact indexing avoid scanning all ambient axes at each step? This would + make the sampler usable in the actual nine-bit search. First construct the + pairing-one quotient axes directly with a canonical basis and prove the same + lexicographic or a newly declared ordering. The current implementation is a + bounded reference, and arbitrary-chart basis selection remains to implement. +2. How many distinct full symplectic products occur among minimum chart words? + This separates chart-path freedom from physical-map freedom. First enumerate + the complete matrices for transverse n=2 charts and classify product fibers. + The present endpoint contract does not identify products or their phase lifts. + +These questions are recorded with relevance, first steps and blockers in +[TASK.json](TASK.json). They are not part of the delivered result. diff --git a/research/shortest-chart-axis-words/SOURCES.json b/research/shortest-chart-axis-words/SOURCES.json new file mode 100644 index 0000000000..80f74a60e2 --- /dev/null +++ b/research/shortest-chart-axis-words/SOURCES.json @@ -0,0 +1,18 @@ +{ + "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" + } + ] +} diff --git a/research/shortest-chart-axis-words/TASK.json b/research/shortest-chart-axis-words/TASK.json new file mode 100644 index 0000000000..0d320c1c16 --- /dev/null +++ b/research/shortest-chart-axis-words/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact shortest binary Lagrangian chart-path and literal-axis-word counts, with a lexicographic rank/unrank bijection.", + "scope_change_reason": "Replace larger-rank supplier synthesis by a self-contained exact contact-geometry compiler result, building on Dugongue PR4841 rather than auditing it.", + "bottleneck_link": "Exact word multiplicity and indexing support unbiased exploration of physical chart transitions; complete supplier admission and any paid-profile benefit remain open.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved original counting/indexing result and bounded exact certificate.", + "outcome": "completed", + "evidence": "README.md proof; verify.py independent graph and exhaustive literal-word certificate; words.py bijection.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can shortest-word indexing avoid scanning all ambient axes?", + "why_it_matters": "Would permit practical use at the actual nine-bit contact-search boundary.", + "first_step": "Construct pairing-one quotient axes directly in a canonical basis and declare an exact word order.", + "blocked_by": "Arbitrary-chart basis selection and a proved efficient indexing algorithm are not implemented." + }, + { + "question": "How many distinct full symplectic products occur among minimum chart words?", + "why_it_matters": "Chart equivalence need not preserve physical symplectic maps or phase lifts.", + "first_step": "Enumerate full matrices for transverse n=2 chart endpoints and classify product fibers.", + "blocked_by": "The current contract identifies endpoints and axis words, not product equivalence or phases." + } + ] +} diff --git a/research/shortest-chart-axis-words/VERIFY.json b/research/shortest-chart-axis-words/VERIFY.json new file mode 100644 index 0000000000..492b44316c --- /dev/null +++ b/research/shortest-chart-axis-words/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": "Independent all-pairs shortest chart-path counts through n=3, exhaustive shortest literal words through n=2, exact rank/unrank controls through n=6; source-bound generated receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Independent all-pairs shortest chart-path counts through n=3, exhaustive shortest literal words through n=2, exact rank/unrank controls through n=6; source-bound generated receipt." + } + ] +} diff --git a/research/shortest-chart-axis-words/verify.py b/research/shortest-chart-axis-words/verify.py new file mode 100644 index 0000000000..73dab99c5e --- /dev/null +++ b/research/shortest-chart-axis-words/verify.py @@ -0,0 +1,147 @@ +"""Independent graph counts and literal shortest-word certificate.""" + +import hashlib +import itertools +import json +import sys +from collections import deque +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import words + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ArithmeticError(message) + + +def span(rows: tuple[int, ...]) -> frozenset[int]: + result = {0} + for row in rows: + result |= {x ^ row for x in result} + return frozenset(result) + + +def lagrangians(n: int) -> list[frozenset[int]]: + """Enumerate RREF spaces, independently of the transvection graph.""" + require(1 <= n <= 3, "certificate enumeration bound") + spaces = [] + for pivots in itertools.combinations(range(2 * n), n): + cells = [(i, j) for i, p in enumerate(pivots) + for j in range(p + 1, 2 * n) if j not in pivots] + for bits in range(1 << len(cells)): + rows = [1 << p for p in pivots] + for k, (i, j) in enumerate(cells): + rows[i] |= ((bits >> k) & 1) << j + isotropic = all(sum(((a >> j) & 1) * ((b >> (j + n)) & 1) + + ((b >> j) & 1) * ((a >> (j + n)) & 1) + for j in range(n)) % 2 == 0 + for a in rows for b in rows) + if isotropic: + spaces.append(span(tuple(rows))) + require(len(set(spaces)) == len(spaces), "duplicate RREF chart") + return spaces + + +def graph_certificate(n: int) -> dict[str, int]: + charts = lagrangians(n) + edges = [[j for j, b in enumerate(charts) if len(a & b) == 1 << (n - 1)] + for a in charts] + pair_checks = 0 + for target in range(len(charts)): + depths = [-1] * len(charts) + paths = [0] * len(charts) + depths[target], paths[target] = 0, 1 + queue = deque([target]) + for _ in range(len(charts)): + require(bool(queue), "disconnected chart graph") + node = queue.popleft() + for neighbor in edges[node]: + if depths[neighbor] == -1: + depths[neighbor] = depths[node] + 1 + queue.append(neighbor) + if depths[neighbor] == depths[node] + 1: + paths[neighbor] += paths[node] + require(not queue, "graph traversal bound exceeded") + for start, chart in enumerate(charts): + r = n - ((len(chart & charts[target])).bit_length() - 1) + require(depths[start] == r, "minimum-length formula") + require(paths[start] == words.count(n, r, literal=False), "chart path count") + actual = sum(words.distance(words.move(chart, a, n), charts[target], n) == r - 1 + for a in range(1, 1 << (2 * n))) if r else 0 + expected = (1 << (n - 1)) * ((1 << r) - 1) + require(actual == expected, "shortest-word first-letter count") + require(words.count(n, r) == paths[start] * (1 << (r * (n - 1))), + "literal-word multiplicity") + pair_checks += 1 + return {"n": n, "charts": len(charts), "ordered_pairs": pair_checks} + + +def literal_certificate() -> dict[str, int]: + executions = 0 + roundtrips = 0 + for n in (1, 2): + charts = lagrangians(n) + for left in charts: + for right in charts: + r = words.distance(left, right, n) + actual = [] + for word in itertools.product(range(1, 1 << (2 * n)), repeat=r): + current = left + for axis in word: + current = words.move(current, axis, n) + if current == right: + actual.append(word) + executions += 1 + require(len(actual) == words.count(n, r), "literal exhaustive count") + for index, word in enumerate(actual): + require(words.unrank(left, right, n, index) == word, "lexicographic unrank") + require(words.rank(left, right, n, word) == index, "lexicographic rank") + roundtrips += 1 + return {"enumerated_axis_words": executions, "all_small_word_roundtrips": roundtrips} + + +def larger_and_controls() -> dict[str, int]: + samples = 0 + for n in range(3, 7): + left = span(tuple(1 << i for i in range(n))) + for r in range(n + 1): + right = span(tuple(1 << (i + n if i < r else i) for i in range(n))) + total = words.count(n, r) + for index in sorted({0, total // 2, total - 1}): + word = words.unrank(left, right, n, index) + require(words.rank(left, right, n, word) == index, "larger roundtrip") + samples += 1 + good = frozenset({0, 1, 2, 3}) + target = frozenset({0, 4, 8, 12}) + controls = [lambda: words.count(0, 0), lambda: words.count(2, 3), + lambda: words.count(True, 0), lambda: words.validate(good, 7), + lambda: words.validate(frozenset({0, 1, 2, 4}), 2), + lambda: words.validate(frozenset({0, 1, 4, 5}), 2), + lambda: words.unrank(good, target, 2, -1), + lambda: words.unrank(good, target, 2, 12), + lambda: words.rank(good, target, 2, (1,)), + lambda: words.rank(good, target, 2, (0, 4)), + lambda: words.rank(good, target, 2, (1, 4))] + for check in controls: + try: + check() + except ValueError: + continue + raise ArithmeticError("rejection control unexpectedly accepted") + return {"larger_roundtrips": samples, "rejection_controls": len(controls)} + + +def main() -> None: + result = {"status": "PASS_SHORTEST_CHART_AXIS_WORDS", + "graph_certificates": [graph_certificate(n) for n in (1, 2, 3)], + **literal_certificate(), **larger_and_controls()} + package = Path(__file__).resolve().parent + result["source_sha256"] = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(package.iterdir()) if p.is_file()} + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/shortest-chart-axis-words/words.py b/research/shortest-chart-axis-words/words.py new file mode 100644 index 0000000000..3b63786e2e --- /dev/null +++ b/research/shortest-chart-axis-words/words.py @@ -0,0 +1,95 @@ +"""Exact ranking of shortest binary symplectic chart words, for 1 <= n <= 6.""" + +from math import prod + +Chart = frozenset[int] +MAX_N = 6 + + +def pairing(x: int, y: int, n: int) -> int: + mask = (1 << n) - 1 + return (((x & mask) & (y >> n)).bit_count() + + ((y & mask) & (x >> n)).bit_count()) & 1 + + +def validate(chart: Chart, n: int) -> None: + if type(n) is not int or not 1 <= n <= MAX_N: + raise ValueError("dimension must be an integer from 1 through 6") + if not isinstance(chart, frozenset) or len(chart) != 1 << n or 0 not in chart: + raise ValueError("a chart must contain exactly 2^n vectors, including zero") + if any(type(x) is not int or not 0 <= x < 1 << (2 * n) for x in chart): + raise ValueError("vector outside the ambient space") + for x in chart: + for y in chart: + if x ^ y not in chart or pairing(x, y, n): + raise ValueError("chart must be an isotropic subspace") + + +def distance(left: Chart, right: Chart, n: int) -> int: + return n - ((len(left & right)).bit_length() - 1) + + +def move(chart: Chart, axis: int, n: int) -> Chart: + return frozenset(x ^ (axis if pairing(x, axis, n) else 0) for x in chart) + + +def count(n: int, r: int, *, literal: bool = True) -> int: + if type(n) is not int or type(r) is not int or not 1 <= n <= MAX_N or not 0 <= r <= n: + raise ValueError("require 1 <= n <= 6 and 0 <= distance <= n") + paths = prod((1 << j) - 1 for j in range(1, r + 1)) + return paths << (r * (n - 1)) if literal else paths + + +def choices(current: Chart, target: Chart, n: int) -> list[tuple[int, Chart]]: + r = distance(current, target, n) + if r == 0: + return [] + result = [] + for axis in range(1, 1 << (2 * n)): + changed = move(current, axis, n) + if distance(changed, target, n) == r - 1: + result.append((axis, changed)) + if len(result) != (1 << (n - 1)) * ((1 << r) - 1): + raise ArithmeticError("distance-decreasing axis multiplicity failed") + return result + + +def unrank(left: Chart, right: Chart, n: int, index: int) -> tuple[int, ...]: + """Lexicographic bijection from [0,count(n,r)) to shortest literal words.""" + validate(left, n) + validate(right, n) + r = distance(left, right, n) + if type(index) is not int or not 0 <= index < count(n, r): + raise ValueError("word index outside the exact range") + current = left + word = [] + for remaining in range(r, 0, -1): + block = count(n, remaining - 1) + digit, index = divmod(index, block) + axis, current = choices(current, right, n)[digit] + word.append(axis) + if current != right or index != 0: + raise ArithmeticError("unranking did not reach the target") + return tuple(word) + + +def rank(left: Chart, right: Chart, n: int, word: tuple[int, ...]) -> int: + validate(left, n) + validate(right, n) + r = distance(left, right, n) + if not isinstance(word, tuple) or len(word) != r: + raise ValueError("word must be a tuple with the minimum length") + current = left + index = 0 + for step, axis in enumerate(word): + if type(axis) is not int or not 0 < axis < 1 << (2 * n): + raise ValueError("invalid nonzero axis") + options = choices(current, right, n) + position = next((i for i, item in enumerate(options) if item[0] == axis), None) + if position is None: + raise ValueError("word is not distance-decreasing") + index += position * count(n, r - step - 1) + current = options[position][1] + if current != right: + raise ArithmeticError("ranked word did not reach the target") + return index