diff --git a/research/two-capacity-direct-unranking/PROOF.md b/research/two-capacity-direct-unranking/PROOF.md new file mode 100644 index 0000000000..3402fc3c4a --- /dev/null +++ b/research/two-capacity-direct-unranking/PROOF.md @@ -0,0 +1,174 @@ +# Direct unranking for two capacities without a prescribed injection + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement and premises + +Let V and W have dimension n over F_q. Fix arbitrary subspaces A,B of V +and C,D of W. Define + +`G = {g:V->W invertible : g(A) contained in C, g(B) contained in D}`. + +There is a deterministic bijection from the integers 0 through |G|-1 to G +using O(1+n^5) field operations and O(1+n^4) exact integer arithmetic +operations on O(1+n^2 log q)-bit integers. Live working storage is O(1+n^2) +field elements and O(1+n^3 log q) bits. Fixed input and output matrices have +the same field-element bound. An empty G is detected before decoding. + +This is the U=0 specialization of Ali Romman's PR6539 contract. Its count +and quotient/lift decomposition are cited premises. The new result makes +that decomposition an explicit direct unranking algorithm, with polynomial +resource bounds. The predecessor count, ToikY's PR6535 feasibility theorem, +and classical Gaussian, graph-map and basis-extension formulas are not new +claims. Nick Petalas's PR6607 already gives a general prescribed-injection +sampler through exponentially many candidate images. That self-reduction is +not used here. This proof leaves nonzero prescribed U open. + +The field-operation bound assumes an exact finite-field arithmetic interface +and a fixed ordering of its elements. Bit cost of a chosen field representation +is additional. The executable supports prime orders at most 31 and F4, with +n at most 12. The proof has no such fixed dimension or field-order limit. + +## Fixed decompositions and cardinality + +All complements below are deterministic once the inputs are fixed. Extend +an ordered independent list by scanning a fixed basis of its containing +space, retaining exactly those vectors which increase rank. + +Write J=A intersect B and T=C intersect D, of dimensions j and tau. Fix + +`V = J direct-sum A0 direct-sum B0 direct-sum R`, +`C = T direct-sum C0`, `D = T direct-sum D0`, + +where A=J direct-sum A0 and B=J direct-sum B0. Put +alpha=dim A0, beta=dim B0, c=dim C, d=dim D and s=j+alpha+beta. +The complement R concerns the whole domain V, not A+B alone. + +Write Inj(m,k)=product_{r=0}^{k-1}(q^m-q^r), zero outside 0<=k<=m, +and use Gaussian coefficients with their usual zero convention. If j>tau +then G is empty. Otherwise set H=tau-j and + +```text +w_i = [H choose i]_q [c-tau choose alpha-i]_q + q^((H-i)(alpha-i)) Inj(alpha,alpha) + Inj(d-j-i,beta) q^(i beta), + +max(0,alpha-c+tau) <= i <= min(alpha,H), +S = sum_i w_i, +N = Inj(tau,j) S q^(j(alpha+beta)) + product_{r=s}^{n-1}(q^n-q^r). +``` + +PR6539 supplies N=|G| in this specialization. Zero weights are omitted. +An empty sum means N=0. No negative-dimensional injection is decoded. + +## Polynomial elementary decoders + +An ordered injection from F_q^k into F_q^m is decoded one image at a time. +After r images, extend their ordered basis to a full deterministic basis. +Every vector outside their span has unique coordinates (a,b), where +a is arbitrary in F_q^r and b is nonzero in F_q^(m-r). Index a in base q +and b by the nonzero integers 1,...,q^(m-r)-1. This is a bijection of +q^m-q^r indices with the possible next images. Mixed radices decode the +complete injection. No ambient vector list or rejection trial is needed. + +A k-subspace of F_q^m has a unique reduced row-echelon basis. Divide its +first-column cases into a zero column and a pivot column. The first has +[m-1 choose k]_q possibilities. In the second, the remaining rows form a +(k-1)-subspace of F_q^(m-1), and the first row has m-k free coordinates +in the nonpivot columns. Its count is q^(m-k)[m-1 choose k-1]_q. +This gives a weighted first-column decoder. Iterating at most m times records +the pivots and their free coordinates, and then fills their unique RREF. +The executable uses iteration rather than recursion. + +Both decoders have explicit inverse descriptions. Read the unique coordinates +or RREF, recover each mixed-radix digit, and reverse the branch decomposition. + +## Decode a completion + +1. Decode an arbitrary injection J->T, with Inj(tau,j) possibilities. Call + its ordered image L. Choose the deterministic complement H0 of L in T. + Thus H0 represents T/L and has dimension H. +2. Select i by its interval of length w_i within S. A subsequent local + index ranges over exactly w_i choices. Choose an i-subspace I of H0, + and an (alpha-i)-subspace K of C0, with the two Grassmann decoders. + Choose every entry of a graph map K->H0/I in base q. The complement of + I in H0 supplies fixed quotient representatives. The resulting subspace + P of H0+C0 has dimension alpha and satisfies P intersect H0=I. +3. Decode an arbitrary ordered alpha-basis of P, by an element of GL_alpha. + These are the images of the fixed basis of A0, modulo L. +4. In D/L=H0+D0, quotient by I. Decode an injection of the beta-dimensional + B0 into the fixed representative space of dimension d-j-i. Lift each + image through I by i arbitrary field entries. Its image Q is disjoint + from P: the intersection of P with D/L is exactly I, and Q projects + injectively modulo I. This accounts for Inj(d-j-i,beta)q^(i beta). +5. Independently lift every A0 and B0 basis image through L. These + j(alpha+beta) free entries give the displayed global q-power. +6. Extend the resulting ordered s-dimensional image basis to an image of + the fixed remaining domain basis R. Decode each next image outside the + previous span with the elementary decoder. Finally change from the + adapted domain basis back to the standard basis. + +Steps 2 through 4 consume precisely the factors in w_i. Steps 1, 5 and 6 +consume the other global factors of N. Integer division with remainder +therefore splits each index in [0,N) into one such sequence of choices. + +## Bijection and uniformity + +Every decoded image list is independent. The first j images lie in T. +The next alpha lie in C and the next beta in D; their quotient images +have zero intersection by step 4. Lifting through L preserves quotient +independence. The last images are independent by construction. The map +is thus in G, including all arbitrary input vectors by linearity. + +Conversely, fix g in G. Its values on the fixed J basis determine the +injection and L. Project its A0 images modulo L. Their span is the unique P +in step 2, hence determines i, I, K and the graph. The ordered values +determine the GL_alpha choice in step 3. Projecting the B0 values modulo +L and then I determines the injection and lifts in step 4. The L-components +determine step 5. The values on R determine the outside-span digits in +step 6. All fixed complements are functions of earlier recovered choices. +Thus this inverse is unique, so the decoder is bijective. + +A uniform integer index gives exactly the uniform distribution on G. +Put b=ceil(log2 N), with b=0 at N=1. Independent uniform b-bit integers, +accepted exactly when below N, give a uniform index at the first success. +With R attempts the exact exhaustion probability is +`(1-N/2^b)^R`; conditional on success, every map has probability 1/N. +The executable accepts at most 64 pre-supplied entropy blocks, validates +them all, and charges Rb provisioned bits. It returns the acceptance position +in bits separately. It has no hidden random source and no unbounded loop. +The abstract online version, generating blocks only until acceptance, +uses expected b*2^b/N<2b bits for N>1. This latter expectation is not a +measured cost of the pre-supplied-list API. At N=1 zero bits suffice. + +## Resource bound + +Row reduction of O(n) rows of length O(n) costs O(1+n^3) field operations. +A deterministic complement scans at most n vectors and performs at most n +such reductions, costing O(1+n^4). The injection and final extension +decoders make O(1+n) complement calls in total. All other operations are +linear combinations, a fixed number of complements, or the final n +coordinate solves. This proves O(1+n^5) field operations. + +Gaussian products use O(1+n) factors each. The weighted branch sum and +the first-column decoders use polynomially many such products; including +integer powers by repeated squaring, O(1+n^4) arithmetic operations is a +conservative bound. All intermediate integers have O(1+n^2 log q) bits. +Rank comparisons and index arithmetic are included; no q^n candidate loop +is hidden. Space is bounded by a fixed number of O(n)-vector bases, O(n) +stored branch weights of O(1+n^2 log q) bits, and integer counters. +Zero-dimensional spaces use empty bases +and empty products, with one empty invertible map. + +## Limits and next obligations + +This supplies unrestricted linear completions. A nonzero prescribed +injection introduces the compatible quotient discrepancy of PR6539 and +is deliberately outside this proof. An actual native shared contact still +requires its signed or symplectic constraints, physical basis changes, +randomness generation, causal access, dirty restoration, precision, stock, +tapes, compiler and complete outer costs. No selected assumption is +discharged and no kappa is changed. The proof is written mathematics with +finite executable corroboration; independent human and proof-kernel +acceptance are unclaimed. diff --git a/research/two-capacity-direct-unranking/README.md b/research/two-capacity-direct-unranking/README.md new file mode 100644 index 0000000000..0015285b7b --- /dev/null +++ b/research/two-capacity-direct-unranking/README.md @@ -0,0 +1,129 @@ +# Polynomial direct generation of two-capacity completions + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped constructive proof with exact finite corroboration. +For arbitrary subspaces A,B,C,D in n-dimensional finite-field spaces, the +package constructs every invertible map g satisfying g(A) contained in C +and g(B) contained in D exactly once from an integer index. It decodes +one index with O(1+n^5) field operations and O(1+n^4) integer arithmetic +operations. Uniform indices therefore give exactly uniform completions. +No injection is prescribed. Nonzero prescribed images remain open here. + +The construction makes the quotient factors in +[Ali Romman's PR6539](https://github.com/CrocSwap/integer-mult-bounds/pull/6539) +directly executable for this subclass. Its count theorem is a cited input, +not a result re-audited by this package. The older +[PR6607](https://github.com/CrocSwap/integer-mult-bounds/pull/6607) samples +the more general prescribed-injection contract through an exponential +candidate-image scan. Its self-reduction and code are not used here. +Classical subspace, graph-map and basis-extension methods retain credit; +no general literature-priority claim is made. + +[PROOF.md](PROOF.md) proves the bijection, uniformity and resource bounds. +[unrank.py](unrank.py) implements the direct decoder and a bounded entropy +interface. [linear.py](linear.py) supplies exact row reduction and canonical +complements. The executable accepts n<=12, prime q<=31, and F4 represented +by F2[t]/(t^2+t+1). The written construction applies to every finite field +with an exact arithmetic interface and a fixed element ordering. + +For N>0 completions, set b=ceil(log2 N). A batch of R independent uniform +b-bit blocks has exact exhaustion probability (1-N/2^b)^R. Conditional on +success, each completion has probability 1/N. The finite API accepts R<=64, +validates the whole batch and provisions Rb bits. It reports the acceptance +position separately. There is no hidden random source. The corresponding +online method uses fewer than 2b expected fair bits when N>1. At N=1, no +random bits are needed. Empty sets are rejected for sampling. + +## Evidence and reproduction + +The verifier compares complete decoded endpoint sets and collision counts +with literal matrix enumeration. It covers every ordered quadruple of +subspaces over F2 at n=0,1,2, and over F3/F4 at n=1. Further selected +fixtures cover F3/F4/F5 at n=2 and F2 at n=3, including a two-branch +crossed-plane contract. Component checks enumerate all Grassmann and +ordered-injection indices through dimension three over F2/F3/F4. +Sixteen selected indices in dimensions 8,10,12 satisfy their full endpoints. +These are selected large examples, not large exhaustive censuses. + +For GL2(F2), all 64 pairs of three-bit blocks produce ten occurrences of +each of six matrices and four exhausted pairs. Singleton and zero-attempt +cases are checked. Invalid field orders, dimensions, vectors, indices, +empty sampling and entropy limits are rejected. Checks use ordinary +exceptions and remain enabled under optimized Python. + +From the worktree 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/two-capacity-direct-unranking +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/two-capacity-direct-unranking --check-source-history +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/two-capacity-direct-unranking/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/two-capacity-direct-unranking/verify.py +``` + +Another CPython 3.12 installation may replace the absolute interpreter path. +Expected marker: `PASS_TWO_CAPACITY_DIRECT_UNRANKING`. Each registered +command has a 240-second timeout. Default execution writes only stdout. +Optional `--receipt /absolute/scratch/result.json` writes a generated +receipt outside the checkout, bound to package and predecessor-input hashes. +No receipt is handwritten or committed. + +For an API example, put this package on the Python import path: + +```python +from unrank import Contract + +contract = Contract(2, 2, (), (), (), ()) +matrix = contract.decode(4) +sample, acceptance_position_bits = contract.sample((7, 4)) +assert sample == matrix and acceptance_position_bits == 6 +``` + +Maps are tuples of their standard-domain column vectors. Inputs are ordered +lists of canonical coordinate vectors; redundant rows are reduced. The API +normalizes input subspaces and fixes all later complements deterministically. + +## Sources and limits + +The immediate mathematical predecessor is Ali Romman's PR6539 and its +quotient/lift count. Its proof at canonical base +e54523517d0f03e58352e647c403a5af3e525a57 is a hash-bound declared input in +[SOURCES.json](SOURCES.json). It is read for attribution and hypotheses; +no predecessor scientific executable is imported or replayed. Credit ToikY +PR6535 for coupled quotient feasibility; Ali Romman PR6533 for general +capacity rank counts; Nick Petalas PR6489/4919 and PR6607 for the prior +nested/general sampling work; Brian/JoyboyBrian PR5020, Cao Yifan/intqwq +PR4610, codyw912 PR4735, and the retained Cinna Davis, Dugongue, zxv and +Jacob Alan Sussman lineage. Existing predecessor notices remain unchanged. + +The code has no recursion and no function longer than 60 lines. +All production loops are bounded by the enforced dimensions or 64 entropy +blocks. Python managed allocation and bigint/field arithmetic are explicit +deviations from fixed-allocation low-level rules. Production working memory +is O(1+n^2) field elements plus O(1+n^3 log q) bits, including stored branch +weights. The verifier separately enumerates finite endpoint sets and retains +them for collision checks. Its largest component class has 181,440 members. +Ordinary Python method dispatch has the fixed visible targets in these three +files. Warning-strict ordinary and optimized execution are the diagnostics. + +This is unrestricted GL generation. There is no actual native contact, +symplectic or signed-phase constraint, physical randomness source, legal +access schedule, dirty restoration, precision, stock, tape, compiler or +outer invoice. The five selected framework assumptions remain. No new +kappa, supplier admission or complete multiplication theorem follows. +Independent human and formal proof-kernel review are unclaimed. + +The formal-interface-lemma card changes scope to this finite-field +construction. Selected #7000 and its kappa are unchanged. The current +selected-baseline binding check passed; no selected scientific cold replay, +Lean, Docker or predecessor verification suite ran. + +## Open next questions + +1. Can the direct polynomial decoder handle a nonzero prescribed injection? + Start with the common lift subject to the quotient discrepancy in PR6539. + Compatible affine representatives and their unique inverse decomposition + are the missing step. The exponential general sampler remains available. +2. Can one actual shared native contact use these samples with a favorable + complete bill? Extract its two capacities and chronological bases first. + Signed/symplectic realization and physical costs remain blockers. diff --git a/research/two-capacity-direct-unranking/SOURCES.json b/research/two-capacity-direct-unranking/SOURCES.json new file mode 100644 index 0000000000..8d6df76f34 --- /dev/null +++ b/research/two-capacity-direct-unranking/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/two-capacity-completion-count/PROOF.md", + "usage": "input", + "git_blob": "0a835ca8de78befc93e61b72d18a471a1e1df344", + "sha256": "66ab99f0c3b13999325523378ae3f9ade8c0341cd194cc8ad5580916bc9144c4" + } + ] +} diff --git a/research/two-capacity-direct-unranking/TASK.json b/research/two-capacity-direct-unranking/TASK.json new file mode 100644 index 0000000000..f6f1681dd7 --- /dev/null +++ b/research/two-capacity-direct-unranking/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Polynomial direct unranking and exact uniform generation of invertible maps with two arbitrary capacity constraints and no prescribed injection.", + "scope_change_reason": "Take the U=0 sampling opening of Ali Romman PR6539. This is a constructive finite-field prerequisite, not a formal selected-caller proof.", + "bottleneck_link": "Makes two shared-capacity GL search samples available without scanning q^n candidate images; physical/native realization remains separate.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved U=0 direct construction and its exact endpoint checks. Leave prescribed injections and native binding open.", + "outcome": "completed", + "evidence": "PROOF.md, unrank.py, linear.py, verify.py; generated source-bound receipts go outside the checkout.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the direct polynomial decoder handle a nonzero prescribed injection?", + "why_it_matters": "The general shared-contact contract fixes source images.", + "first_step": "Decode a common injection subject to PR6539\u2019s quotient discrepancy, then compatible affine lifts.", + "blocked_by": "Uniform compatible representatives and their inverse decomposition are not implemented." + }, + { + "question": "Can an actual native contact use these samples within a favorable complete bill?", + "why_it_matters": "Unrestricted GL samples alone do not supply a supplier.", + "first_step": "Extract one actual caller and its two capacities.", + "blocked_by": "Signed/symplectic realization, legal access and physical costs remain." + } + ] +} diff --git a/research/two-capacity-direct-unranking/VERIFY.json b/research/two-capacity-direct-unranking/VERIFY.json new file mode 100644 index 0000000000..68dd3a36b1 --- /dev/null +++ b/research/two-capacity-direct-unranking/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/two-capacity-completion-count/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Exact new decoder endpoint sets and collisions; Grassmann/injection components; F4; finite entropy distribution; large selected indices; invalid inputs." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Exact new decoder endpoint sets and collisions; Grassmann/injection components; F4; finite entropy distribution; large selected indices; invalid inputs." + } + ] +} diff --git a/research/two-capacity-direct-unranking/linear.py b/research/two-capacity-direct-unranking/linear.py new file mode 100644 index 0000000000..d3d56fd50c --- /dev/null +++ b/research/two-capacity-direct-unranking/linear.py @@ -0,0 +1,117 @@ +"""Small exact field and subspace operations. Produced by Nick Petalas.""" +from math import isqrt + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +class Field: + """Prime fields through 31, plus F4 = F2[t]/(t^2+t+1).""" + + def __init__(self, q): + need(type(q) is int and 2 <= q <= 31, "field order limit") + need(q == 4 or all(q % d for d in range(2, isqrt(q) + 1)), "field order") + self.q = q + + def add(self, x, y): + return x ^ y if self.q == 4 else (x + y) % self.q + + def neg(self, x): + return x if self.q == 4 else -x % self.q + + def mul(self, x, y): + if self.q != 4: + return x * y % self.q + z = (x & 1) * (y & 1) + z ^= ((x >> 1) * (y & 1) ^ (x & 1) * (y >> 1)) << 1 + z ^= ((x >> 1) * (y >> 1)) * 3 + return z + + def inv(self, x): + need(0 < x < self.q, "nonzero inverse") + return self.mul(x, x) if self.q == 4 else pow(x, -1, self.q) + + +def unit(n, j): + return tuple(int(i == j) for i in range(n)) + + +def standard(n): + return tuple(unit(n, j) for j in range(n)) + + +def combine(coefficients, rows, n, field): + need(len(coefficients) == len(rows), "combination dimensions") + out = [0] * n + for a, row in zip(coefficients, rows): + for j in range(n): + out[j] = field.add(out[j], field.mul(a, row[j])) + return tuple(out) + + +def add_vectors(x, y, field): + need(len(x) == len(y), "vector dimensions") + return tuple(field.add(a, b) for a, b in zip(x, y)) + + +def reduce_rows(rows, n, field): + work = [list(row) for row in rows] + pivots = [] + for col in range(n): + at = next((i for i in range(len(pivots), len(work)) if work[i][col]), None) + if at is None: + continue + pos = len(pivots) + work[pos], work[at] = work[at], work[pos] + scale = field.inv(work[pos][col]) + work[pos] = [field.mul(x, scale) for x in work[pos]] + for i in range(len(work)): + if i != pos and work[i][col]: + scale = field.neg(work[i][col]) + work[i] = [field.add(x, field.mul(scale, y)) + for x, y in zip(work[i], work[pos])] + pivots.append(col) + return tuple(tuple(row) for row in work[:len(pivots)]), tuple(pivots) + + +def basis(rows, n, field): + return reduce_rows(rows, n, field)[0] + + +def annihilator(rows, n, field): + reduced, pivots = reduce_rows(rows, n, field) + out = [] + for j in range(n): + if j not in pivots: + v = list(unit(n, j)) + for row, col in zip(reduced, pivots): + v[col] = field.neg(row[j]) + out.append(tuple(v)) + return tuple(out) + + +def meet(left, right, n, field): + return annihilator(annihilator(left, n, field) + + annihilator(right, n, field), n, field) + + +def complement(initial, container, n, field): + current = list(initial) + need(len(basis(current, n, field)) == len(current), "independent initial basis") + added = [] + for v in container: + if len(basis(tuple(current) + (v,), n, field)) > len(current): + current.append(v) + added.append(v) + return tuple(added) + + +def coordinates(rows, vector, n, field): + """Unique coordinates in an independent ordered row basis.""" + k = len(rows) + equations = [tuple(row[j] for row in rows) + (vector[j],) for j in range(n)] + reduced, pivots = reduce_rows(equations, k + 1, field) + need(pivots == tuple(range(k)), "vector outside independent span") + return tuple(row[-1] for row in reduced) diff --git a/research/two-capacity-direct-unranking/unrank.py b/research/two-capacity-direct-unranking/unrank.py new file mode 100644 index 0000000000..0db03cb2b7 --- /dev/null +++ b/research/two-capacity-direct-unranking/unrank.py @@ -0,0 +1,197 @@ +"""Direct two-capacity unranking with no prescribed injection. + +Produced by Nick Petalas. Apache-2.0. +Uses Ali Romman's PR6539 quotient factors and classical Grassmann counts. +""" +from math import prod + +from linear import (Field, add_vectors, basis, combine, complement, coordinates, + meet, need, standard) + + +def gaussian(m, k, q): + if not 0 <= k <= m: + return 0 + k = min(k, m - k) + top = prod(q ** (m - j) - 1 for j in range(k)) + bottom = prod(q ** (k - j) - 1 for j in range(k)) + quotient, remainder = divmod(top, bottom) + need(remainder == 0, "integral Gaussian coefficient") + return quotient + + +def injections(m, k, q): + return prod(q ** m - q ** j for j in range(k)) if 0 <= k <= m else 0 + + +class Index: + def __init__(self, value): + need(type(value) is int and value >= 0, "nonnegative integer index") + self.value = value + + def take(self, radix): + need(radix > 0, "positive radix") + self.value, digit = divmod(self.value, radix) + return digit + + def finish(self): + need(self.value == 0, "index fully consumed") + + +def digits(value, length, q): + need(0 <= value < q ** length, "field digit range") + cursor = Index(value) + result = tuple(cursor.take(q) for _ in range(length)) + cursor.finish() + return result + + +def subspace(m, k, value, field): + """Unrank a Grassmannian by first-column RREF decomposition, iteratively.""" + need(0 <= value < gaussian(m, k, field.q), "subspace index") + pending, left = [], k + for col in range(m): + remaining = m - col + skip = gaussian(remaining - 1, left, field.q) + if value < skip: + continue + value -= skip + value, free = divmod(value, field.q ** (remaining - left)) + pending.append((col, digits(free, remaining - left, field.q))) + left -= 1 + need(left == value == 0, "Grassmann index consumed") + pivots = tuple(col for col, _ in pending) + rows = [] + for col, free in pending: + row = [int(j == col) for j in range(m)] + slots = tuple(j for j in range(col + 1, m) if j not in pivots) + need(len(slots) == len(free), "RREF free slots") + for j, digit in zip(slots, free): + row[j] = digit + rows.append(tuple(row)) + return tuple(rows) + + +def outside(rows, n, value, field): + """Unrank a vector outside span(rows) without scanning ambient vectors.""" + k = len(rows) + need(0 <= value < field.q ** n - field.q ** k, "outside-span index") + tail = complement(rows, standard(n), n, field) + free, old = divmod(value, field.q ** k) + coefficients = digits(old, k, field.q) + digits(free + 1, n - k, field.q) + return combine(coefficients, rows + tail, n, field) + + +def injection(m, k, value, field): + need(0 <= value < injections(m, k, field.q), "injection index") + cursor, rows = Index(value), () + for j in range(k): + row = outside(rows, m, cursor.take(field.q ** m - field.q ** j), field) + rows += (row,) + cursor.finish() + return rows + + +def branch_weights(c, d, tau, j, alpha, beta, q): + h = tau - j + return tuple((i, gaussian(h, i, q) * gaussian(c - tau, alpha - i, q) + * q ** ((h - i) * (alpha - i)) * injections(alpha, alpha, q) + * injections(d - j - i, beta, q) * q ** (i * beta)) + for i in range(max(0, alpha - c + tau), min(alpha, h) + 1)) + + +class Contract: + """Canonical finite input; maps are returned as standard-domain columns.""" + + def __init__(self, n, q, a, b, c, d): + need(type(n) is int and 0 <= n <= 12, "dimension limit") + self.n, self.field = n, Field(q) + spaces = [] + for rows in (a, b, c, d): + need(len(rows) <= n, "input basis length") + need(all(len(v) == n and all(type(x) is int and 0 <= x < q for x in v) + for v in rows), "canonical vectors") + spaces.append(basis(rows, n, self.field)) + self.a, self.b, self.c, self.d = spaces + self.j = meet(self.a, self.b, n, self.field) + self.t = meet(self.c, self.d, n, self.field) + self.aa = complement(self.j, self.a, n, self.field) + self.bb = complement(self.j, self.b, n, self.field) + self.cc = complement(self.t, self.c, n, self.field) + self.dd = complement(self.t, self.d, n, self.field) + self.source = self.j + self.aa + self.bb + self.source += complement(self.source, standard(n), n, self.field) + self.weights = () + if len(self.j) <= len(self.t): + self.weights = branch_weights(len(self.c), len(self.d), len(self.t), + len(self.j), len(self.aa), len(self.bb), q) + self.total = (injections(len(self.t), len(self.j), q) + * sum(w for _, w in self.weights) + * q ** (len(self.j) * (len(self.aa) + len(self.bb))) + * prod(q ** n - q ** k + for k in range(len(self.j + self.aa + self.bb), n))) + + def decode(self, value): + need(type(value) is int and 0 <= value < self.total, "completion index") + f, n, q = self.field, self.n, self.field.q + j, alpha, beta = len(self.j), len(self.aa), len(self.bb) + cursor = Index(value) + common = injection(len(self.t), j, + cursor.take(injections(len(self.t), j, q)), f) + images = tuple(combine(v, self.t, n, f) for v in common) + h = complement(images, self.t, n, f) + branch = cursor.take(sum(w for _, w in self.weights)) + selected = None + for i, weight in self.weights: + if branch < weight: + selected = i + break + branch -= weight + need(selected is not None, "nonempty intersection branch") + left, right = self._quotient(images, h, selected, Index(branch)) + for v in left + right: + coeff = digits(cursor.take(q ** j), j, q) + images += (add_vectors(v, combine(coeff, images[:j], n, f), f),) + for k in range(len(images), n): + images += (outside(images, n, cursor.take(q ** n - q ** k), f),) + cursor.finish() + need(len(images) == n, "complete image basis") + return tuple(combine(coordinates(self.source, v, n, f), images, n, f) + for v in standard(n)) + + def sample(self, blocks): + """Supplied independent uniform b-bit blocks; report bounded exhaustion.""" + need(self.total > 0, "nonempty sampling contract") + width = (self.total - 1).bit_length() + need(len(blocks) <= 64, "sampling attempt limit") + need(all(type(x) is int and 0 <= x < 2 ** width for x in blocks), + "canonical entropy blocks") + for attempt, value in enumerate(blocks): + if value < self.total: + return self.decode(value), (attempt + 1) * width + return None, len(blocks) * width + + def _quotient(self, common, h, i, cursor): + f, n, q = self.field, self.n, self.field.q + alpha, beta = len(self.aa), len(self.bb) + ib = subspace(len(h), i, cursor.take(gaussian(len(h), i, q)), f) + intersection = tuple(combine(v, h, n, f) for v in ib) + hc = complement(intersection, h, n, f) + kb = subspace(len(self.cc), alpha - i, + cursor.take(gaussian(len(self.cc), alpha - i, q)), f) + graph = tuple(combine(v, self.cc, n, f) for v in kb) + graph = tuple(add_vectors(v, combine(digits(cursor.take(q ** len(hc)), + len(hc), q), hc, n, f), f) + for v in graph) + p = intersection + graph + gl = injection(alpha, alpha, cursor.take(injections(alpha, alpha, q)), f) + left = tuple(combine(v, p, n, f) for v in gl) + target = hc + self.dd + inj = injection(len(target), beta, + cursor.take(injections(len(target), beta, q)), f) + right = tuple(combine(v, target, n, f) for v in inj) + right = tuple(add_vectors(v, combine(digits(cursor.take(q ** i), i, q), + intersection, n, f), f) for v in right) + cursor.finish() + need(len(common) + len(h) == len(self.t), "common quotient dimensions") + return left, right diff --git a/research/two-capacity-direct-unranking/verify.py b/research/two-capacity-direct-unranking/verify.py new file mode 100644 index 0000000000..153e8dfede --- /dev/null +++ b/research/two-capacity-direct-unranking/verify.py @@ -0,0 +1,228 @@ +"""Verify the new unranking endpoint sets, not predecessor executables. + +Produced by Nick Petalas. Apache-2.0. Default execution writes only stdout. +""" +import argparse +import hashlib +import itertools +import json +from pathlib import Path +import sys + +ROOT = Path(__file__).resolve().parent +sys.path.insert(0, str(ROOT)) +from linear import Field, add_vectors, basis, combine, need, standard +from unrank import Contract, gaussian, injection, injections, subspace + + +def span(rows, n, field): + return frozenset(combine(v, rows, n, field) + for v in itertools.product(range(field.q), repeat=len(rows))) + + +def all_subspaces(n, field): + """Independent vector-set closure, only used for n<=2.""" + need(n <= 2, "literal subspace limit") + zero = (0,) * n + spaces = {frozenset((zero,))} + vectors = tuple(itertools.product(range(field.q), repeat=n)) + for _ in range(n): + next_spaces = set(spaces) + for old in spaces: + for v in vectors: + extended = frozenset(add_vectors(w, combine((t,), (v,), n, field), field) + for w in old for t in range(field.q)) + next_spaces.add(extended) + spaces = next_spaces + return tuple(sorted(spaces, key=lambda x: (len(x), sorted(x)))) + + +def literal_gl(n, field): + need(n <= 3 and field.q ** (n * n) <= 200000, "literal matrix limit") + vectors = tuple(itertools.product(range(field.q), repeat=n)) + return tuple(columns for columns in itertools.product(vectors, repeat=n) + if len(span(columns, n, field)) == field.q ** n) + + +def admissible(matrix, spaces, n, field): + a, b, c, d = spaces + return (all(combine(v, matrix, n, field) in c for v in a) + and all(combine(v, matrix, n, field) in d for v in b)) + + +def compare_contract(n, field, spaces, ambient): + inputs = tuple(basis(tuple(s), n, field) for s in spaces) + contract = Contract(n, field.q, *inputs) + expected = frozenset(m for m in ambient if admissible(m, spaces, n, field)) + actual = tuple(contract.decode(i) for i in range(contract.total)) + need(len(actual) == len(set(actual)), "unranking collision") + need(frozenset(actual) == expected, "decoded endpoint set") + return len(actual) + + +def small_census(): + records = [] + for n, q in ((0, 2), (1, 2), (1, 3), (1, 4), (2, 2)): + field = Field(q) + spaces, ambient = all_subspaces(n, field), literal_gl(n, field) + contracts = endpoints = positive = 0 + for quadruple in itertools.product(spaces, repeat=4): + count = compare_contract(n, field, quadruple, ambient) + contracts += 1 + endpoints += count + positive += int(count > 0) + records.append(dict(n=n, q=q, contracts=contracts, + endpoints=endpoints, nonempty=positive)) + return records + + +def selected_census(): + records = [] + for n, q in ((2, 3), (2, 4), (2, 5), (3, 2)): + field = Field(q) + ambient = literal_gl(n, field) + e = standard(n) + line = (add_vectors(e[0], e[1], field),) + candidates = ((), (e[0],), (e[1],), line, e[:2], e) + fixtures = [] + for i in range(12): + quadruple = tuple(candidates[(i * (2 * j + 1) + j) % len(candidates)] + for j in range(4)) + fixtures.append(tuple(span(x, n, field) for x in quadruple)) + fixtures.extend(tuple(span(x, n, field) for x in quad) for quad in ( + (e[:1], e[:1], e[:2], e[:2]), + (e[:1], e[1:2], e[:2], e[:2]), + (e[:1], e[1:2], e[:1], e[1:2]), + (e[:2], e[:2], e[:1], e[:2]), + ((), (), (), ()), + )) + if n == 3: + fixtures.append(tuple(span(x, n, field) for x in + (e[:1], e[1:2], e[:2], e[1:]))) + counts = [compare_contract(n, field, quad, ambient) for quad in fixtures] + records.append(dict(n=n, q=q, contracts=len(fixtures), endpoints=sum(counts), + nonempty=sum(x > 0 for x in counts))) + return records + + +def component_census(): + grassmann = ordered = 0 + for q in (2, 3, 4): + f = Field(q) + for m in range(4): + for k in range(m + 1): + rows = tuple(subspace(m, k, i, f) for i in range(gaussian(m, k, q))) + need(len(set(rows)) == len(rows), "Grassmann collision") + need(all(basis(r, m, f) == r for r in rows), "Grassmann RREF") + grassmann += len(rows) + images = tuple(injection(m, k, i, f) + for i in range(injections(m, k, q))) + need(len(set(images)) == len(images), "injection collision") + need(all(len(basis(r, m, f)) == k for r in images), "injection rank") + ordered += len(images) + return dict(grassmann_endpoints=grassmann, injection_endpoints=ordered) + + +def large_examples(): + records = [] + for n, q in ((8, 2), (10, 3), (12, 4), (12, 31)): + f, e = Field(q), standard(n) + contract = Contract(n, q, e[:n // 2], e[n // 3:2 * n // 3], + e[:n - 1], e[1:]) + need(contract.total > 0, "large nonempty contract") + indices = tuple(sorted({0, 1, contract.total // 2, contract.total - 1})) + spaces = (contract.a, contract.b, contract.c, contract.d) + for index in indices: + matrix = contract.decode(index) + need(len(basis(matrix, n, f)) == n, "large invertibility") + for source, target in ((spaces[0], spaces[2]), (spaces[1], spaces[3])): + for v in source: + image = combine(v, matrix, n, f) + need(len(basis(target + (image,), n, f)) == len(target), + "large capacity endpoint") + records.append(dict(n=n, q=q, selected_indices=len(indices), + cardinality_bits=contract.total.bit_length())) + return records + + +def rejections(): + tests = ( + lambda: Contract(13, 2, (), (), (), ()), + lambda: Contract(-1, 2, (), (), (), ()), + lambda: Contract(2, 6, (), (), (), ()), + lambda: Contract(2, 32, (), (), (), ()), + lambda: Contract(True, 2, (), (), (), ()), + lambda: Contract(2, 2, ((2, 0),), (), (), ()), + lambda: Contract(2, 2, ((0,),), (), (), ()), + lambda: Contract(1, 2, ((0,), (1,)), (), (), ()), + lambda: Contract(1, 2, (), (), (), ()).decode(-1), + lambda: Contract(1, 2, (), (), (), ()).decode(1), + lambda: Contract(1, 2, (), (), (), ()).decode(True), + lambda: Contract(1, 2, ((1,),), (), (), ()).decode(0), + lambda: Contract(1, 2, ((1,),), (), (), ()).sample(()), + lambda: Contract(1, 2, (), (), (), ()).sample((1,)), + lambda: Contract(1, 2, (), (), (), ()).sample((0,) * 65), + ) + for operation in tests: + try: + operation() + except ValueError: + continue + raise ValueError("invalid input accepted") + return len(tests) + + +def sampling_law(): + contract = Contract(2, 2, (), (), (), ()) + need(contract.total == 6, "literal GL2 contract") + counts, failures = {}, 0 + for blocks in itertools.product(range(8), repeat=2): + matrix, used = contract.sample(blocks) + need(used in (3, 6), "charged entropy width") + if matrix is None: + failures += 1 + else: + counts[matrix] = counts.get(matrix, 0) + 1 + need(len(counts) == 6 and set(counts.values()) == {10} and failures == 4, + "exact finite entropy distribution") + singleton = Contract(0, 2, (), (), (), ()) + need(singleton.sample((0,)) == ((), 0), "zero-bit singleton") + need(contract.sample(()) == (None, 0), "zero-attempt exhaustion") + return dict(two_block_inputs=64, occurrences_per_matrix=10, exhausted=4) + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + report = dict(status="PASS_TWO_CAPACITY_DIRECT_UNRANKING", + source_sha256=source_bindings(), + complete=small_census(), selected=selected_census(), + components=component_census(), large=large_examples(), + sampling=sampling_law(), + invalid_inputs_rejected=rejections()) + report["package_sha256"] = { + p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(ROOT.iterdir()) if p.is_file()} + text = json.dumps(report, indent=2, sort_keys=True) + "\n" + if args.receipt: + need(not args.receipt.resolve().is_relative_to(ROOT.parent.parent), + "receipt must be outside checkout") + args.receipt.write_text(text) + print(text, end="") + + +def source_bindings(): + manifest = json.loads((ROOT / "SOURCES.json").read_text()) + checked = {} + for row in manifest["files"]: + if row["usage"] == "input": + path = ROOT.parent.parent / row["path"] + digest = hashlib.sha256(path.read_bytes()).hexdigest() + need(digest == row["sha256"], "predecessor input bytes") + checked[row["path"]] = digest + return checked + + +if __name__ == "__main__": + main()