diff --git a/research/nested-late-capacity-completion/PROOF.md b/research/nested-late-capacity-completion/PROOF.md new file mode 100644 index 0000000000..5416883d22 --- /dev/null +++ b/research/nested-late-capacity-completion/PROOF.md @@ -0,0 +1,143 @@ +# Shared-map completion with nested late capacities + +This proof and construction were produced by Nick Petalas. Apache-2.0. + +## Contract and theorem + +Let V and W have the same finite dimension n over any field F. A fixed +injective linear map h:U -> W has image U'. For i=1,...,k, let A_i be +arbitrary subspaces of V and let C_1 <= ... <= C_k be subspaces of W. +The requested map is an isomorphism g:V -> W extending h and satisfying +g(A_i) <= C_i for every i. Inclusions may be equal, sources may overlap, +and zero spaces, k=0 and n=0 are allowed. + +Put + +``` +S_i = A_1 + ... + A_i, +u = dim U, e_0 = 0, +e_i = dim(U+S_i) - u, +c_i = dim C_i, b_i = dim(C_i intersect U'). +``` + +Such a g exists if and only if, for every i, + +``` +h(U intersect S_i) <= C_i, (compatibility) +e_i <= c_i - b_i. (quotient capacity) +``` + +Over F_q, if these conditions hold, the exact number of requested maps is + +``` +product_(i=1..k) [q^(b_i (e_i-e_(i-1))) + product_(j=e_(i-1)..e_i-1) (q^(c_i-b_i)-q^j)] + * product_(j=u+e_k..n-1) (q^n-q^j). +``` + +For k=0, read e_k=0. Empty products equal one. If any condition fails, +the count is zero. The count covers distinct linear maps, without quotienting +by basis choices or charging any physical realization cost. + +## Reduction to cumulative sources + +If g(A_j) <= C_j for j<=i, nesting gives g(A_j) <= C_i, hence +g(S_i) <= C_i. Conversely A_i <= S_i, so the cumulative inclusions imply +the original ones. This equivalence permits arbitrary source intersections; +it requires nesting only on the target side. + +If g exists, its restriction to U intersect S_i is h and has image in C_i. +The induced injection from (U+S_i)/U into W/U' sends the e_i-dimensional +source into (C_i+U')/U', whose dimension is c_i-b_i. This proves necessity. + +## Compatible basis extension + +Choose a basis of U. Extend it successively to bases of U+S_i by choosing +e_i-e_(i-1) new vectors in S_i. Such choices are possible because the +cumulative sources form a flag. This ordered domain basis is fixed for +the remainder of the proof and counting argument. + +Suppose an injective extension has already been defined on U+S_(i-1), +and maps S_(i-1) into C_(i-1). Since S_(i-1) <= S_i, + +``` +(U+S_(i-1)) intersect S_i = (U intersect S_i) + S_(i-1). +``` + +The already prescribed image of this intersection lies in C_i, by +compatibility and nesting. Thus extending by any images in C_i for the +new independent domain vectors preserves the entire inclusion g(S_i)<=C_i. + +Work modulo U'. Images of the previous new basis vectors span an +e_(i-1)-dimensional subspace of (C_i+U')/U'. The latter space has dimension +c_i-b_i >= e_i. Extend these independent images to e_i independent vectors +in this quotient, and lift each new vector to C_i. The resulting map on +U+S_i is injective. This induction works over every field. Finally extend +the domain and image bases to bases of V and W. It yields the required g. + +The bounded reference implements this same constructive choice without +enumerating a field: an available member of a basis of C_i must lie outside +the current image span whenever another independent image is needed. + +## Counting every completion + +Over F_q, fix the domain basis chosen above. At stage i, after a total of +j new basis vectors have been assigned, where e_(i-1)<=j, h(x+y)=z, +A_1=, C_1=, +A_2=, C_2=. +``` + +The individual one-capacity contracts admit 4 and 12 isomorphisms, +respectively. The first sends x to x, then y to x+z, and has four choices +for the image of z outside their plane. The second has three nonzero +choices in C_2 for the image of y, then fixes the image of x through h, +and has four choices for the image of z. Yet no shared map exists: +U <= S_2 and h(U)= is not contained in C_2. This is a new joint-contract +example, rather than a re-evaluation of PR5020's one-capacity examples. + +The quotient condition also detects a different missed obstruction. Take +U=0, A_1=, A_2=, and C_1=C_2=. Both individual contracts are +feasible but S_2 has dimension two against a one-dimensional capacity. +The exact reference and the separate literal GL census check both examples. + +## Scope and attribution + +Brian / JoyboyBrian's PR5020 supplies the one-capacity prescribed-map +contract and asks for a second late capacity. The theorem above settles +its nested-target case, and includes any finite number of nested targets. +The proof is self-contained and does not invoke or recheck PR5020's theorem. +Basis extension, quotient dimensions and finite-field independent-vector +counts are classical; no general literature-priority claim is made. + +The unrestricted GL contract does not supply a symplectic native map, +an absolute phase, chronological contact realization, a changed emitted +word or a favorable complete paid/productive invoice. No helper credit, +physical saving, new kappa, selected-frontier change or complete +multiplication theorem follows. Nonnested targets require a different +compatibility argument; applying this theorem to a nonnested list is invalid. diff --git a/research/nested-late-capacity-completion/README.md b/research/nested-late-capacity-completion/README.md new file mode 100644 index 0000000000..9baf5b33e7 --- /dev/null +++ b/research/nested-late-capacity-completion/README.md @@ -0,0 +1,159 @@ +# Exact shared maps for nested late capacities + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped written proof with exact finite corroboration. This +settles the nested-target case of Brian / JoyboyBrian's +[PR5020](https://github.com/CrocSwap/integer-mult-bounds/pull/5020), +Open next question 2. It gives an exact feasibility criterion, construction +and finite-field count for one prescribed injective map extended to an +isomorphism meeting any finite list of nested late capacities. Sources +may overlap arbitrarily and need not be nested. No new kappa is claimed. + +## Result and first discriminating example + +For h:U -> W injective, dim V=dim W=n, arbitrary sources A_i and nested +capacities C_1 <= ... <= C_k, put + +``` +S_i = sum_(j<=i) A_j, U' = h(U), u = dim U, +e_i = dim(U+S_i)-u, c_i = dim C_i, b_i = dim(C_i intersect U'). + +An invertible g extending h with g(A_i)<=C_i exists exactly when +h(U intersect S_i)<=C_i and e_i<=c_i-b_i for every i. +``` + +[PROOF.md](PROOF.md) proves this over every field and counts every +completion over F_q. Its exact count is + +``` +product_i q^(b_i*(e_i-e_(i-1))) + product_(e_(i-1)<=j and y -> . Each request alone +admits a completion, with counts 4 and 12. Their shared contract admits +zero because h(U intersect (A_1+A_2)) lies outside the final capacity. +A second fixture has U=0 and two independent source lines directed into +one common target line; it fails the cumulative quotient condition. + +The new step is the simultaneous cumulative-source theorem and its count. +PR5020's one-capacity result, source-specific adapter and numbers are cited +context and are not replayed. The investigation stops at this scoped result. + +## Exact evidence + +The independent census constructs subspaces as literal finite vector sets, +enumerates invertible matrices by their complete vector permutations, and +groups every possible prescribed partial injection by its literal action. +For every source pair and nested target pair it compares the formula with +the exact number of satisfying GL matrices. It uses no reference row reducer. + +| Field and dimension | Partial injections | Source/target/map cases | +| --- | ---: | ---: | +| F_2^0 | 1 | 1 | +| F_2^1 | 2 | 24 | +| F_2^2 | 16 | 4,800 | +| F_3^2 | 81 | 43,740 | +| F_5^2 | 625 | 840,000 | +| F_2^3 | 512 | 8,650,752 | + +All 9,539,317 cases agree. Separately, 14,141 calls compare the bounded +row-reduction reference count with literal census values; 3,119 constructor +calls check existence, and every returned matrix is checked on complete +vector permutations and literal source/target membership. The constructor +also handles 112 attaining fixtures through dimension six, including empty, +repeated and eight-stage target flags. Fourteen malformed boundary cases +reject in both entry points. Checks use explicit exceptions under normal +and optimized Python. + +Every run generates a JSON receipt with all six domain digests, counts, +controls and SHA256 hashes of all seven package files. The verifier writes +nothing; redirect stdout outside the checkout to retain the receipt. + +## Reproduce + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/nested-late-capacity-completion/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/nested-late-capacity-completion/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/nested-late-capacity-completion +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/nested-late-capacity-completion --check-source-history +``` + +Any CPython 3.12 executable may replace the absolute path. Expected direct +marker: `PASS_NESTED_LATE_CAPACITY_COMPLETION`. Both registered commands +have 120-second limits. The direct verifier is self-contained in a Git-free +copy of these seven files. The source README, selected record and task card +are pinned historical provenance, not executable dependencies. + +## Scope, costs and credit + +The all-field conclusion rests on the written proof. The exhaustive +execution covers only the six stated prime-field domains. The reference +API accepts q in {2,3,5,7}, 0<=n<=6 and at most eight contacts; these are +software limits, not theorem hypotheses. It requires basis tuples and +rejects a noninjective prescribed map or nonnested targets. + +This is unrestricted linear-algebra completion. No actual selected-word +contact is changed. Symplectic/native realization, absolute phases, source +access, causal scheduling, arbitrary dirty restoration, basis preparation, +delivery, productive target debits and the complete paid invoice remain +open. Precision, stock, tape, compiler, outer admission and all five +selected assumptions remain. No native build, selected scientific replay, +Lean or Docker run was needed or performed. Independent human and formal +proof-kernel review are unclaimed. The selected frontier is unchanged. + +Credit Brian / JoyboyBrian for PR5020 and the explicit second-capacity +question; Cao Yifan / intqwq for PR4610's native-map caller; Nick Petalas +for PR4919's different three-subspace correspondence theorem; codyw912 +for PR4735; and Cinna Davis, Dugongue, zxv, Jacob Alan Sussman and the +retained native/compiler lineage. Basis extension and finite-field +independent-vector counts are classical. No general literature-priority +claim is made. Predecessor text and code are not copied or modified. + +The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363406) +records the scope. Canonical base is +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, selected +PR6030. [TASK.json](TASK.json) records the explicit change from the +coverage-law card to this shared-map feasibility side result. The selected +orientation passed its metadata-only positive control. Live open/account +PRs, recent claims, main README and merged/general-form searches were +checked. Sparse historical notes, arbitrary diffs and unpublished work +remain overlap-coverage limits. + +## Open next questions + +1. Extend the prescribed-map theorem to two nonnested target capacities. + Start with two intersecting binary planes and an oblique prescribed + subspace. Their coupled image choices are not decided by this flag proof. +2. Bind a nested-capacity instance to an actual shared native operator. + Export every same-operator source/image condition and determine whether + its capacities form a flag. Phase/native realization and a complete + signed invoice block any claimed helper or kappa gain. + +The structured questions in [TASK.json](TASK.json) give first steps and +blockers. No continuation or physical construction is reserved here. + +## Verifier bounds + +No function exceeds 60 physical lines and no call path recurses. The literal +census has at most 25 vectors, 16 subspaces, 480 GL matrices and 66 target +flags in a domain; it enumerates at most 625 candidate matrices. It retains +counts as a digest rather than storing the millions of case records. The +reference has at most six coordinates, twelve-column elimination matrices +and eight contacts. Each package file is limited to 128 KiB when hashed. +Warning-strict normal/optimized execution and in-memory syntax compilation +supply diagnostics. Input failures propagate as explicit errors. + +Python exact integers, dataclasses, iterators and bounded collections allocate +during execution. These are documented managed-runtime deviations from +Power of Ten static allocation and indirect-call restrictions, not a +constant-space physical implementation. There are no network, subprocess, +write or persistent shared-state paths in the scientific verifier. diff --git a/research/nested-late-capacity-completion/SOURCES.json b/research/nested-late-capacity-completion/SOURCES.json new file mode 100644 index 0000000000..7408405b71 --- /dev/null +++ b/research/nested-late-capacity-completion/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/multi-line-native-extension/README.md", + "usage": "provenance", + "git_blob": "655e6dba4e0850ad17d9947f075ad75a223884d7", + "sha256": "12074300d53cebd87ce4959f532c77af6a335a7f3101325e7e9f31d1473adc12" + } + ] +} diff --git a/research/nested-late-capacity-completion/TASK.json b/research/nested-late-capacity-completion/TASK.json new file mode 100644 index 0000000000..e471df4b26 --- /dev/null +++ b/research/nested-late-capacity-completion/TASK.json @@ -0,0 +1,88 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "coverage-law-change", + "question": "Can a completed call earn more independent productive target credit without an offsetting paid bill?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Use #5599 as a completed positive control, then choose one uncovered cut/module beyond an applicable frozen exclusion. Derive independence, saturation and chronological availability rather than counting rational rank alone. Price target credits and all new jobs together, then check compiler and actual caller compatibility. Stop on a nonphysical credit or an unfavorable complete relaxation.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "target credit", + "helper split", + "coverage law" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact shared prescribed-map extension for arbitrary overlapping late sources into nested target capacities: all-field proof, construction and finite-field count.", + "scope_change_reason": "The current coverage-law card is changed to a scoped algebraic compatibility prerequisite from PR5020 Open next question 2. No changed physical word, paid invoice or supplier credit is claimed.", + "bottleneck_link": "Several helper contacts sharing one native map require simultaneous image feasibility before any productive target credit can be counted. Separate one-capacity tests miss cumulative relations.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified nested-capacity theorem, exact count and constructor with bounded independent GL corroboration; leave nonnested targets and actual native realization open.", + "outcome": "completed", + "evidence": "PROOF.md; extension.py; verify.py generated hash-bound JSON receipt and exhaustive literal GL comparisons.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Extend the prescribed-map theorem to two nonnested late target capacities.", + "why_it_matters": "Arbitrary shared native contacts need not have a nested target family.", + "first_step": "Enumerate two intersecting binary planes with an oblique prescribed subspace and identify the coupled image obstruction.", + "blocked_by": "A sufficient compatibility criterion for coupled nonnested image choices." + }, + { + "question": "Bind one nested-capacity contract to an actual changed shared native operator.", + "why_it_matters": "An algebraic completion affects helper credit only with a legal realized caller and complete bill.", + "first_step": "Export all source/image conditions on one same-operator contact group and test whether target capacities form a flag.", + "blocked_by": "Actual emitted word, symplectic and absolute-phase realization, ownership, delivery, restoration and the complete signed invoice." + } + ], + "claim_type": "scoped proof with exact finite corroboration", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363406", + "predecessors": [ + { + "pr": 5020, + "author": "JoyboyBrian", + "role": "one-capacity interface and explicit second-capacity question" + } + ] +} diff --git a/research/nested-late-capacity-completion/VERIFY.json b/research/nested-late-capacity-completion/VERIFY.json new file mode 100644 index 0000000000..d11425adfe --- /dev/null +++ b/research/nested-late-capacity-completion/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 cumulative-source criterion and count versus complete small-field GL enumeration, reference constructor, longer flags and failure controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete scientific coverage under optimized Python; all acceptance checks remain active." + } + ] +} diff --git a/research/nested-late-capacity-completion/extension.py b/research/nested-late-capacity-completion/extension.py new file mode 100644 index 0000000000..ef2bf35693 --- /dev/null +++ b/research/nested-late-capacity-completion/extension.py @@ -0,0 +1,164 @@ +"""Bounded prime-field reference for the nested late-capacity theorem. + +Vectors act on the left; matrix rows are images of coordinate vectors. +The universal statement is in PROOF.md. This offline reference accepts +prime fields through seven, dimension at most six and at most eight contacts. +""" + +from dataclasses import dataclass + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def reduced(rows, q, width): + """Canonical row basis; callers have validated the finite dimensions.""" + work = [list(row) for row in rows] + pivot = 0 + for column in range(width): + found = next((i for i in range(pivot, len(work)) if work[i][column]), None) + if found is None: + continue + work[pivot], work[found] = work[found], work[pivot] + scale = pow(work[pivot][column], -1, q) + work[pivot] = [(x * scale) % q for x in work[pivot]] + for i in range(len(work)): + if i != pivot: + scale = work[i][column] + work[i] = [(x - scale * y) % q + for x, y in zip(work[i], work[pivot])] + pivot += 1 + if pivot == len(work): + break + return tuple(tuple(row) for row in work[:pivot]) + + +def combine(coefficients, rows, q, n): + return tuple(sum(a * row[j] for a, row in zip(coefficients, rows)) % q + for j in range(n)) + + +def kernel(rows, q, width): + basis = reduced(rows, q, width) + pivots = tuple(next(j for j, x in enumerate(row) if x) for row in basis) + result = [] + for free in range(width): + if free not in pivots: + vector = [0] * width + vector[free] = 1 + for pivot, row in zip(pivots, basis): + vector[pivot] = -row[free] % q + result.append(tuple(vector)) + return tuple(result) + + +def intersection_images(u, images, source, q, n): + """Images under h of a basis of U intersect source.""" + columns = u + tuple(tuple(-x % q for x in row) for row in source) + relations = kernel(tuple(zip(*columns)), q, len(columns)) + values = tuple(combine(row[:len(u)], images, q, n) for row in relations) + return reduced(values, q, n) + + +@dataclass(frozen=True) +class Problem: + q: int + n: int + u: tuple + images: tuple + sources: tuple + capacities: tuple + + def validate(self): + require(type(self.q) is int and self.q in (2, 3, 5, 7), "unsupported field") + require(type(self.n) is int and 0 <= self.n <= 6, "dimension outside 0..6") + require(type(self.u) is tuple and type(self.images) is tuple, + "partial-map bases must be tuples") + require(type(self.sources) is tuple and type(self.capacities) is tuple, + "contacts must be tuples") + require(len(self.sources) == len(self.capacities) <= 8, "contact count") + spaces = (self.u, self.images) + self.sources + self.capacities + for space in spaces: + require(type(space) is tuple and len(space) <= self.n, "basis shape") + for row in space: + require(type(row) is tuple and len(row) == self.n, "vector shape") + require(all(type(x) is int and 0 <= x < self.q for x in row), + "noncanonical coordinate") + require(len(reduced(space, self.q, self.n)) == len(space), + "dependent supplied basis") + require(len(self.u) == len(self.images), "partial map is not an injection") + previous = () + for capacity in self.capacities: + require(len(reduced(previous + capacity, self.q, self.n)) == len(capacity), + "target capacities are not nested") + previous = capacity + + +def stages(problem): + """Return cumulative source bases and their exact quotient invariants.""" + problem.validate() + q, n = problem.q, problem.n + cumulative = () + result = [] + for source, capacity in zip(problem.sources, problem.capacities): + cumulative = reduced(cumulative + source, q, n) + fixed = intersection_images(problem.u, problem.images, cumulative, q, n) + compatible = len(reduced(fixed + capacity, q, n)) == len(capacity) + e = len(reduced(problem.u + cumulative, q, n)) - len(problem.u) + c0 = len(capacity) + len(problem.images) - len( + reduced(capacity + problem.images, q, n)) + result.append((cumulative, compatible, e, len(capacity), c0)) + return tuple(result) + + +def count_extensions(problem): + count, previous = 1, 0 + for _, compatible, e, c, c0 in stages(problem): + if not compatible or e > c - c0: + return 0 + count *= problem.q ** (c0 * (e - previous)) + for j in range(previous, e): + count *= problem.q ** (c - c0) - problem.q ** j + previous = e + for j in range(len(problem.u) + previous, problem.n): + count *= problem.q ** problem.n - problem.q ** j + require(count > 0, "feasible count must be positive") + return count + + +def add_pair(vector, choices, domain, image, q, n): + """Append one independent vector and its independently chosen image.""" + if len(reduced(tuple(domain) + (vector,), q, n)) == len(domain): + return + chosen = next((w for w in choices if + len(reduced(tuple(image) + (w,), q, n)) > len(image)), None) + require(chosen is not None, "proved capacity unexpectedly exhausted") + domain.append(vector) + image.append(chosen) + + +def construct_extension(problem): + data = stages(problem) + if any(not compatible or e > c - c0 for _, compatible, e, c, c0 in data): + return None + q, n = problem.q, problem.n + domain, image = list(problem.u), list(problem.images) + for (source, _, _, _, _), capacity in zip(data, problem.capacities): + for vector in source: + add_pair(vector, capacity, domain, image, q, n) + standard = tuple(tuple(int(i == j) for j in range(n)) for i in range(n)) + for vector in standard: + add_pair(vector, standard, domain, image, q, n) + require(len(domain) == len(image) == n, "completion dimension") + augmented = tuple(left + right for left, right in zip(domain, image)) + answer = tuple(row[n:] for row in reduced(augmented, q, 2 * n)) + require(len(reduced(answer, q, n)) == n, "completion must be invertible") + for vector, expected in zip(problem.u, problem.images): + require(combine(vector, answer, q, n) == expected, "prescribed value") + for source, capacity in zip(problem.sources, problem.capacities): + actual = tuple(combine(v, answer, q, n) for v in source) + require(len(reduced(actual + capacity, q, n)) == len(capacity), + "late inclusion") + return answer diff --git a/research/nested-late-capacity-completion/verify.py b/research/nested-late-capacity-completion/verify.py new file mode 100644 index 0000000000..588715a8a4 --- /dev/null +++ b/research/nested-late-capacity-completion/verify.py @@ -0,0 +1,296 @@ +"""Independent bounded vector-set/GL corroboration of PROOF.md. + +The census uses literal vector permutations, not the reference eliminator. +It writes no files. Redirect its generated JSON receipt outside the checkout. +""" + +import hashlib +import importlib.util +import itertools +import json +from pathlib import Path +import sys + + +PACKAGE = Path(__file__).resolve().parent +SPEC = importlib.util.spec_from_file_location("nested_capacity_reference", + PACKAGE / "extension.py") +if SPEC is None or SPEC.loader is None: + raise RuntimeError("reference module unavailable") +REFERENCE = importlib.util.module_from_spec(SPEC) +sys.modules[SPEC.name] = REFERENCE +SPEC.loader.exec_module(REFERENCE) + + +def check(condition, message): + if not condition: + raise RuntimeError(message) + + +def indices(mask, size): + return tuple(i for i in range(size) if mask & (1 << i)) + + +def vector_sum(a, b, q): + return tuple((x + y) % q for x, y in zip(a, b)) + + +def literal_span(rows, vectors, lookup, q): + values = {vectors[0]} + for row in rows: + values = {vector_sum(v, tuple(t * x % q for x in row), q) + for v in values for t in range(q)} + return sum(1 << lookup[v] for v in values) + + +def geometry(q, n): + check((q, n) in ((2, 0), (2, 1), (2, 2), (3, 2), (5, 2), (2, 3)), + "unbudgeted literal census") + vectors = tuple(itertools.product(range(q), repeat=n)) + lookup = {v: i for i, v in enumerate(vectors)} + spaces = {1} + for _ in range(n): + additions = set() + for mask in spaces: + for vector in vectors: + rows = tuple(vectors[i] for i in indices(mask, len(vectors))) + # A space has at most eight vectors in the n=3 domain. + additions.add(literal_span(rows + (vector,), vectors, lookup, q)) + spaces |= additions + spaces = tuple(sorted(spaces, key=lambda x: (x.bit_count(), x))) + bases, dimensions = [], [] + for mask in spaces: + basis, current = [], 1 + for i in indices(mask, len(vectors)): + if not current & (1 << i): + basis.append(vectors[i]) + current = literal_span(tuple(basis), vectors, lookup, q) + check(current == mask and q ** len(basis) == mask.bit_count(), "space basis") + bases.append(tuple(basis)) + dimensions.append(len(basis)) + return vectors, lookup, spaces, tuple(bases), tuple(dimensions) + + +def literal_groups(q, n, vectors, lookup, spaces): + permutations, matrices = [], [] + for matrix in itertools.product(vectors, repeat=n): + permutation = tuple(lookup[tuple(sum(v[j] * matrix[j][i] for j in range(n)) % q + for i in range(n))] for v in vectors) + if len(set(permutation)) == len(vectors): + matrices.append(matrix) + permutations.append(permutation) + expected = 1 + for j in range(n): + expected *= q ** n - q ** j + check(len(matrices) == expected, "literal GL order") + space_lookup = {mask: i for i, mask in enumerate(spaces)} + images = tuple(tuple(space_lookup[sum(1 << permutation[i] + for i in indices(mask, len(vectors)))] + for mask in spaces) for permutation in permutations) + allowed = tuple(tuple(sum(1 << g for g in range(len(matrices)) + if spaces[images[g][a]] & ~spaces[c] == 0) + for c in range(len(spaces))) for a in range(len(spaces))) + return tuple(matrices), tuple(permutations), images, allowed + + +def tables(q, vectors, lookup, spaces, bases): + space_lookup = {mask: i for i, mask in enumerate(spaces)} + joins = tuple(tuple(space_lookup[literal_span(a + b, vectors, lookup, q)] + for b in bases) for a in bases) + intersections = tuple(tuple(space_lookup[a & b] for b in spaces) for a in spaces) + flags = tuple((c, d) for c in range(len(spaces)) for d in range(len(spaces)) + if spaces[c] & ~spaces[d] == 0) + return joins, intersections, flags + + +def stage_factors(q, u, g, images, spaces, dimensions, joins, intersections): + up = images[g][u] + es = tuple(dimensions[joins[u][s]] - dimensions[u] for s in range(len(spaces))) + factors = [] + for s, e in enumerate(es): + fixed_image = spaces[images[g][intersections[u][s]]] + capacities = [] + for c in range(len(spaces)): + b = dimensions[intersections[up][c]] + d = dimensions[c] - b + entries = [] + for previous in range(e + 1): + value = 0 + if fixed_image & ~spaces[c] == 0 and e <= d: + value = 1 + for j in range(previous, e): + value *= q ** dimensions[c] - q ** (b + j) + entries.append(value) + capacities.append(tuple(entries)) + factors.append(tuple(capacities)) + return es, tuple(factors) + + +def reference_check(q, n, u, g, a, b, c, d, bases, matrices, expected, construct): + values = tuple(tuple(sum(v[j] * matrices[g][j][i] for j in range(n)) % q + for i in range(n)) for v in bases[u]) + problem = REFERENCE.Problem(q, n, bases[u], values, + (bases[a], bases[b]), (bases[c], bases[d])) + check(REFERENCE.count_extensions(problem) == expected, "reference count") + if not construct: + return 0 + matrix = REFERENCE.construct_extension(problem) + check((matrix is None) == (expected == 0), "reference existence") + if matrix is not None: + # These complete permutations are independent of the reference's rank check. + vectors = tuple(itertools.product(range(q), repeat=n)) + outputs = {tuple(sum(v[j] * matrix[j][i] for j in range(n)) % q + for i in range(n)) for v in vectors} + check(len(outputs) == len(vectors), "constructed literal bijection") + lookup = {v: i for i, v in enumerate(vectors)} + for source, capacity in ((a, c), (b, d)): + source_mask = literal_span(bases[source], vectors, lookup, q) + capacity_mask = literal_span(bases[capacity], vectors, lookup, q) + for i in indices(source_mask, len(vectors)): + value = tuple(sum(vectors[i][j] * matrix[j][r] for j in range(n)) % q + for r in range(n)) + check(capacity_mask & (1 << lookup[value]), "constructed inclusion") + for v, value in zip(bases[u], values): + actual = tuple(sum(v[j] * matrix[j][i] for j in range(n)) % q + for i in range(n)) + check(actual == value, "constructed prescribed values") + return 1 + + +def census(q, n): + vectors, lookup, spaces, bases, dims = geometry(q, n) + matrices, permutations, images, allowed = literal_groups(q, n, vectors, lookup, spaces) + joins, intersections, flags = tables(q, vectors, lookup, spaces, bases) + total = positive = partials = references = constructions = 0 + digest = hashlib.sha256() + for u, mask in enumerate(spaces): + restrictions = {} + for g, permutation in enumerate(permutations): + key = tuple(permutation[i] for i in indices(mask, len(vectors))) + old_mask, representative = restrictions.get(key, (0, g)) + restrictions[key] = (old_mask | (1 << g), representative) + expected_partials = 1 + for j in range(dims[u]): + expected_partials *= q ** n - q ** j + check(len(restrictions) == expected_partials, "complete partial injections") + partials += len(restrictions) + for partial_mask, g in restrictions.values(): + es, factors = stage_factors(q, u, g, images, spaces, dims, joins, intersections) + tails = [] + for e in range(n - dims[u] + 1): + value = 1 + for j in range(dims[u] + e, n): + value *= q ** n - q ** j + tails.append(value) + for a in range(len(spaces)): + for b in range(len(spaces)): + s = joins[a][b] + for c, d in flags: + predicted = factors[a][c][0] * factors[s][d][es[a]] * tails[es[s]] + actual = (partial_mask & allowed[a][c] & allowed[b][d]).bit_count() + check(predicted == actual, "cumulative formula versus literal GL") + digest.update(actual.to_bytes(2, "little")) + if total % 1021 == 0 or (q, n) == (2, 2): + constructions += reference_check(q, n, u, g, a, b, c, d, + bases, matrices, actual, + total % 3063 == 0) + references += 1 + total += 1 + positive += int(actual > 0) + return {"q": q, "n": n, "spaces": len(spaces), "target_flags": len(flags), + "gl": len(matrices), "partial_injections": partials, "cases": total, + "positive": positive, "reference_counts": references, + "reference_constructions": constructions, "counts_sha256": digest.hexdigest()} + + +def fixtures(): + x, y, z = (1, 0, 0), (0, 1, 0), (0, 0, 1) + fixed = ((1, 1, 0),) + first = REFERENCE.Problem(2, 3, fixed, (z,), ((x,),), ((x,),)) + second = REFERENCE.Problem(2, 3, fixed, (z,), ((y,),), ((x, y),)) + joint = REFERENCE.Problem(2, 3, fixed, (z,), ((x,), (y,)), ((x,), (x, y))) + counts = tuple(REFERENCE.count_extensions(p) for p in (first, second, joint)) + check(counts == (4, 12, 0), "mixed prescribed relation fixture") + vectors = tuple(itertools.product(range(2), repeat=3)) + literal = [0, 0, 0] + for matrix in itertools.product(vectors, repeat=3): + outputs = tuple(tuple(sum(v[j] * matrix[j][i] for j in range(3)) % 2 + for i in range(3)) for v in vectors) + if len(set(outputs)) == 8 and outputs[6] == z: + a = matrix[0] in ((0, 0, 0), x) + b = matrix[1] in ((0, 0, 0), x, y, (1, 1, 0)) + for i, passed in enumerate((a, b, a and b)): + literal[i] += int(passed) + check(tuple(literal) == counts, "literal missed-compatibility counts") + dimension = REFERENCE.Problem(2, 3, (), (), ((x,), (y,)), ((x,), (x,))) + check(REFERENCE.count_extensions(dimension) == 0, "cumulative dimension fixture") + feasible = REFERENCE.Problem(2, 3, fixed, ((1, 1, 0),), + ((x,), (y,)), ((x,), (x, y))) + check(REFERENCE.count_extensions(feasible) == 4, "changed compatible image") + check(REFERENCE.construct_extension(feasible) is not None, "positive joint fixture") + return {"separate_and_joint_counts": counts, "compatible_joint_count": 4, + "dimension_obstruction": 0} + + +def malformed_controls(): + x, y = (1, 0), (0, 1) + good = dict(q=2, n=2, u=(), images=(), sources=((x,),), capacities=((x,),)) + mutations = ({"q": 4}, {"q": True}, {"n": 7}, {"n": True}, + {"sources": ((x,),) * 9, "capacities": ((x,),) * 9}, + {"sources": ()}, {"sources": [(x,)]}, {"u": []}, + {"u": (x,), "images": ()}, + {"u": (x, y), "images": (x, x)}, + {"sources": (((True, 0),),)}, {"sources": (((2, 0),),)}, + {"sources": (((1,),),)}, + {"sources": ((x,), (y,)), "capacities": ((x,), (y,))}) + for mutation in mutations: + arguments = good | mutation + for operation in (REFERENCE.count_extensions, REFERENCE.construct_extension): + try: + operation(REFERENCE.Problem(**arguments)) + except ValueError: + continue + raise RuntimeError("malformed boundary accepted") + return len(mutations) + + +def longer_flags(): + cases = 0 + for q in (2, 3, 5, 7): + for n in range(7): + standard = tuple(tuple(int(i == j) for j in range(n)) for i in range(n)) + matrix = tuple(tuple((int(i == j) + int(i + 1 == j)) % q + for j in range(n)) for i in range(n)) + u = standard[::2] + images = tuple(REFERENCE.combine(v, matrix, q, n) for v in u) + for k in (0, 1, 2, 8): + sources = tuple(standard[:min(n, i + 1)][::2 if i % 2 else 1] + for i in range(k)) + capacities = tuple(tuple(REFERENCE.combine(v, matrix, q, n) + for v in standard[:min(n, i + 1)]) + for i in range(k)) + problem = REFERENCE.Problem(q, n, u, images, sources, capacities) + check(REFERENCE.count_extensions(problem) > 0, "attained longer flag") + check(REFERENCE.construct_extension(problem) is not None, + "longer-flag constructor") + cases += 1 + return cases + + +def main(): + check(len(sys.argv) == 1, "no command-line options are supported") + domains = tuple(census(q, n) for q, n in + ((2, 0), (2, 1), (2, 2), (3, 2), (5, 2), (2, 3))) + receipt = {"status": "PASS_NESTED_LATE_CAPACITY_COMPLETION", "domains": domains, + "fixtures": fixtures(), "malformed_controls": malformed_controls(), + "longer_flag_cases": longer_flags()} + paths = tuple(sorted(path for path in PACKAGE.iterdir() if path.is_file())) + check(len(paths) == 7, "unexpected package file inventory") + check(all(path.stat().st_size <= 131072 for path in paths), "package file bound") + receipt["package_sha256"] = {path.name: hashlib.sha256(path.read_bytes()).hexdigest() + for path in paths} + print(json.dumps(receipt, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()