diff --git a/research/exact-factor-workspace/PROOF.md b/research/exact-factor-workspace/PROOF.md new file mode 100644 index 0000000000..555b248dde --- /dev/null +++ b/research/exact-factor-workspace/PROOF.md @@ -0,0 +1,145 @@ +# Exact workspace under a single spectator basis change + +This contribution is produced by Nick Petalas. Apache-2.0. +This is a written scoped proof, with finite exact controls. + +## 1. Boundary and theorem + +Let F be any field and let R=A⊕S be a finite dimensional scalar role space. +The original active coordinates A are fixed. Write n=dim S. Consider a fixed +list of nonzero rank-one scalar couplings x_i y_i, with x_i∈R and y_i∈R*. +Its paid factors may be I+λ_i x_i y_i over any unital F-algebra, with scalar +coefficients central and λ_i nonzero. No commutativity between λ_i is needed. +Idempotent couplings additionally satisfy y_i(x_i)=1. + +A permitted restriction chooses S=K⊕N, changes only the spectator basis, +and discards the identity block N. Every original factor must be block +diagonal on (A⊕K)⊕N, with its N block equal to identity. Thus the operation +retains the actual couplings through a single invertible change of coordinates. +It does not replace them by new couplings with the same contractions. + +Let u_i be the S component of x_i and v_i=y_i|_S. Set + + U=span{u_i}, V=span{v_i}, + u=dim U, v=dim V, t=rank(V×U→F), + d=u+v-t, k=n-d. + +**Theorem.** The smallest possible dim K is exactly d. All optimal discarded +spaces N are precisely the complements of U∩ann(V) inside ann(V). For each +such N, all complements K to N in S containing U are optimal and permitted. + +If F has q elements, the numbers of distinct optimal discarded subspaces +and ordered optimal retained/discarded decompositions are respectively + + q^((u-t)k), q^(k(u+v-2t)). (1) + +These count subspaces and ordered pairs of subspaces, not choices of bases. +The theorem includes zero dimensional spaces, empty lists, arbitrary finite +word lengths and dirty inputs. It requires no endpoint assumption. + +## 2. Factor support and the lower bound + +A nonzero rank-one outer product is supported on A⊕K precisely when its column +lies in A⊕K and its functional vanishes on N. One direction follows by taking +the outer product. For the other, any nonzero functional value exposes the +column as the image of an input, and a nonzero column exposes every nonzero +functional value. Multiplication by a nonzero scalar in F is injective even +when the ambient F-algebra has zero divisors. A nonzero λ_i therefore does not +hide a nonzero scalar coefficient of an off-diagonal block or N-block update. + +Consequently a split is permitted exactly when + + U⊂K, N⊂F_0:=ann(V). (2) + +Now dim F_0=n-v and W:=U∩F_0 has dimension u-t, by rank-nullity applied to +U→V*. Since K∩N=0 and U⊂K, any permitted N is disjoint from W. Hence + + dim N ≤ dim F_0-dim W = n-v-u+t = k. + +Since dim K=n-dim N, this proves dim K≥d. In particular d≤n once a permitted +split is constructed. The full split K=S,N=0 also shows existence directly. + +## 3. Attainment and exact classification + +Choose any complement N of W in F_0. It has dimension k and is disjoint from +U because N∩U=N∩W=0. Extend a basis of U together with a basis of N to a +basis of S. Assign the added vectors to K along with U. This gives S=K⊕N, +with dim K=n-k=d, and (2) makes every original factor legal after restriction. + +Conversely, an optimal split has dim N=k. Its inclusion in F_0 and trivial +intersection with W imply F_0=W⊕N by dimensions. Thus these are all optimal +discarded spaces. For each such N, exactly the complements K containing U +satisfy the factor-support condition. This proves the stated classification. + +For F of size q, complements N to W in F_0 are graphs of arbitrary linear +maps from one fixed k-dimensional complement to W. There are q^(k(u-t)). +Fix N. The complements K to N in S are sections of S→S/N. The condition +U⊂K fixes the section on the u-dimensional image of U. The remaining d-u +directions can be lifted independently by any vector of N. There are +q^(k(d-u))=q^(k(v-t)) choices. Multiply the two counts to obtain (1). +The usual graph-of-a-linear-map complement count is standard linear algebra. + +## 4. Full words, endpoint restoration and the two contracts + +Choose any bases of an optimal K and N and prepend the unchanged basis of A. +This is one scalar spectator-only basis change B. Each factor has the form + + B^(-1) G_i B = G_i' ⊕ I_N. + +Therefore the same identity holds for every chronological partial product and +the complete word, with the same ordered coefficient list. Self-contractions, +nonzero rank-one status and idempotence are unchanged. If the original full +endpoint is Q_A⊕I_S, the restricted endpoint is Q_A⊕I_K. This includes all +dirty inputs and both off-diagonal endpoint blocks. Label-only prices and +call counts are unchanged. B is a coordinate witness, not a priced physical +conversion or an additional operation executed by the word. + +Brian's PR4783 proves that a normalized simple-label S4 word with m calls and +ordered-pair crossing rank L admits such a restriction with dim K≤m-L. +That theorem is a cited premise, not replayed here. The new exact answer d +therefore satisfies d≤m-L on that domain. Computing d uses only the scalar +couplings, and gives the exact dimension for this same restriction boundary. +This proof itself also applies to other labels and fields. It does not +extend Brian's inversion-slack inequality to those other alphabets. + +Gareth Davidson's PR2323 preserves active components and all contractions +while replacing couplings. Its optimum is t, already proved there. It need +not arise by a single invertible spectator basis change. The difference is + + d-t=(u-t)+(v-t). + +Thus the new result counts the two pairing radicals that the stricter +coordinate restriction must keep. It does not improve PR2323's resynthesis. + +The difference can be arbitrarily large even for restored words. For s≥1, +take one active role e_0 and 2s dirty roles. For j=1,...,s use the idempotent + + P_j=(e_0+e_j)(e_0*+e_(s+j)*). + +Over F2[S3], for two adjacent transpositions a,b, the formal factors +G_a(P)=I+([a]+1)P and G_b(P)=I+([b]+1)P satisfy +(G_a(P)G_b(P))^3=I. Concatenate these six-call relators for all P_j. +Every dirty input is restored. Here u=v=s,t=0, so a single basis restriction +requires 2s dirty roles, while contraction-preserving resynthesis needs zero. +The endpoint itself is identity and has an empty word. This is a separation +of preservation contracts, never an endpoint-workspace or paid-call lower bound. + +## 5. Verification and limits + +The finite verifier enumerates every scalar subspace pair in the declared +small prime-field domains. A separate exhaustive oracle tries every ordered +direct-sum decomposition and independently finds its minimum and both counts. +It does not use the predicted minimum to prune candidates. Pairing rank is +computed from the literal evaluation image rather than Gaussian elimination. + +Full-word controls use the faithful six-dimensional regular representation +of S3, with every regular input column in every role. They check each original +factor under an explicit invertible spectator basis, the discarded identity +block, and both complete restored endpoints. The regular representation is +faithful on the group algebra, so these are full formal equalities for those +fixtures. General quantifiers follow from the proof above, not the census. + +Native address implementation, restricted scalar mixing, physical conversions, +precision, tape costs, ownership, geometry, supplier admission and multiplication +transfer remain separate obligations. No new κ or selected-frontier update is +claimed. The result does not optimize workspace when factors can change. diff --git a/research/exact-factor-workspace/README.md b/research/exact-factor-workspace/README.md new file mode 100644 index 0000000000..344e4a0913 --- /dev/null +++ b/research/exact-factor-workspace/README.md @@ -0,0 +1,108 @@ +# Exact fixed-factor dirty workspace + +For a fixed rank-one word, one spectator-only basis change needs exactly + + d = dim(U) + dim(V) - rank(V|U) + +retained dirty roles. Here U is the span of dirty column components and V +the span of dirty row components. This is a scoped proof, with an exact finite +certificate. It preserves the original active coordinates and every paid +factor. It supplies no new κ or cheaper endpoint word. + +The result replaces an upper bound by the exact answer for the single-basis +restriction used in [Brian's PR4783](https://github.com/CrocSwap/integer-mult-bounds/pull/4783). +That predecessor gives d≤m-L for normalized simple-label S4 words. Its proof +and executable are cited, not audited or replayed here. Our theorem works over +any field and any unital algebra with central scalar coefficients. The S4 +inversion-slack inequality retains its predecessor's narrower hypotheses. + +[PROOF.md](PROOF.md) classifies every optimal retained/discarded splitting. +Writing u=dim U, v=dim V, t=rank(V|U) and k=n-u-v+t, over a field of size q +there are exactly q^((u-t)k) optimal discarded subspaces and +q^(k(u+v-2t)) ordered optimal splittings. These count subspaces, not bases. + +[Gareth Davidson's PR2323](https://github.com/CrocSwap/integer-mult-bounds/pull/2323) +already gives the smaller optimum t when one can replace the factors while +preserving their contractions. Our stricter preservation boundary keeps both +pairing radicals. The difference can be arbitrarily large even for words that +restore every dirty input. It is not a contradiction or an improvement of +that resynthesis theorem. No literature-priority claim is made for elementary +subspace and complement arguments. + +## Evidence and reproduction + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/exact-factor-workspace +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/exact-factor-workspace/verify.py +``` + +`verify.py` enumerates all subspace pairs over F2 in dimensions 0 through 4, +F3 in dimensions 0 through 3 and F5 in dimensions 0 through 2. Its independent +minimum oracle enumerates every ordered direct-sum decomposition without +formula-based pruning. It checks the exact dimension and both optimal counts. +Seven restored S3 word fixtures check all formal factors and endpoints through +the faithful regular representation, including one-sided, paired, orthogonal +and dense dirty couplings. All 5,669 subspace pairs agree with the minimum +and both counts. Exact coverage and transcript hashes are generated +in [RESULT.json](RESULT.json). Every package source file is hash-bound. + +Both registered commands are read-only. To regenerate the receipt, use +`verify.py --write-result /an/unoccupied/path.json` and compare the generated +file with RESULT.json. The direct verifier works from a Git-free package copy. +Receipt generation refuses an occupied output path. Verification remains +active when Python assertions are disabled. + +## Scope and family decision + +This changes the bit-new-register-model card to a formal workspace-interface +classification. It avoids an unbounded workspace search for a supplied word, +while retaining the exact coordinate-preservation boundary. It is a local +module, not a new native mechanism or complete supplier. Stop after this +classification. Physical scalar conversion, restricted gauges, native access, +ownership, precision/tape costs and admission remain unknown, not zero. + +The current selected source-binding positive control passed. The card's older +`scripts/research_baseline.py` fails with `KeyError: 'bit_lower'` on the current +selected certificate. That unrelated script is unchanged. No historical +construction replay, C++, Lean or Docker check is needed for this theorem. + +The verifier follows structured, nonrecursive control flow with fixed census +domains. Its largest universe has 27 vectors and its largest subspace family +has 67 members. Functions are below 60 lines. A managed-runtime allocation +deviation applies to Python tuples, sets and arbitrary-precision integers; +the fixed domains bound their live sizes. There is no steady service loop or +unbounded search. The warning-strict registered normal and optimized runs +check the complete declared domain. Reassess these bounds before widening it. + +## Open next questions + +- Can the exact coordinate restriction be computed efficiently for a large + supplied word with additional support constraints? Start with one actual + native layout and characterize the legal spectator basis changes. The full + GL model here does not pay or preserve those physical restrictions. +- Which target needs less workspace after changing its factors? Specify an + endpoint and paid budget, then use the existing contraction-preserving + theorem where its alphabet is closed. This package gives no endpoint optimum. + +## Sources and credit + +This contribution is produced by Nick Petalas. Apache-2.0. + +Credit Brian/JoyboyBrian PR4783 and PR4765 for the single-basis spectator +restriction and inversion-slack context; Gareth Davidson/bitplane PR2323 for +the exact contraction-preserving pairing compression; Cinna Davis/1337isnot1337 +PR1541 for image-span restriction; ToikY PR1662/1680 for the UT4 span and +orientation reductions; and the register-model and cut predecessors credited +by those packages. None of their mathematics or counts is a new deliverable +here. [SOURCES.json](SOURCES.json) pins provenance, including the pending +PR4783 citation, without importing predecessor executables. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133318) +records canonical main 624de9dc66858af0945e5f8a0942488d62280d43 and priority +revision 7. Entry overlap checked live open PRs, recent claims, merged searches +and distinctive all-main README/proof terms. The cache covered 365 open PRs +and 3,819 Discussion records. Sparse local notes, nested source differences +and unpublished work are incompletely covered. No novelty certificate, +independent human review or formal proof-kernel acceptance is claimed. diff --git a/research/exact-factor-workspace/RESULT.json b/research/exact-factor-workspace/RESULT.json new file mode 100644 index 0000000000..fdb5192fbe --- /dev/null +++ b/research/exact-factor-workspace/RESULT.json @@ -0,0 +1,205 @@ +{ + "census": [ + { + "direct_sum_decompositions": 1, + "n": 0, + "pairs": 1, + "q": 2, + "sha256": "5e5f01766a2d71df915f11041d6b8d85b16ef6550c2eddf4a2aa01c1382fa4be", + "spaces": 1 + }, + { + "direct_sum_decompositions": 2, + "n": 1, + "pairs": 4, + "q": 2, + "sha256": "76c6e2af33d6fd46dae5f769c6eaa906df82cd06d9f5d3bc085db21aa567d6be", + "spaces": 2 + }, + { + "direct_sum_decompositions": 8, + "n": 2, + "pairs": 25, + "q": 2, + "sha256": "6829016eb7de76ffe9f13621b47c312bd7331190dae13f9888c2395d41763774", + "spaces": 5 + }, + { + "direct_sum_decompositions": 58, + "n": 3, + "pairs": 256, + "q": 2, + "sha256": "aaa37c705bb64f7bf75c2fc79c70ba10fe278e039dd75fac840bbf9c9e844f13", + "spaces": 16 + }, + { + "direct_sum_decompositions": 802, + "n": 4, + "pairs": 4489, + "q": 2, + "sha256": "73830ba529ba729660f0428579b1186d99376e9d1b2f0d625d084a88c05332f8", + "spaces": 67 + }, + { + "direct_sum_decompositions": 1, + "n": 0, + "pairs": 1, + "q": 3, + "sha256": "5e5f01766a2d71df915f11041d6b8d85b16ef6550c2eddf4a2aa01c1382fa4be", + "spaces": 1 + }, + { + "direct_sum_decompositions": 2, + "n": 1, + "pairs": 4, + "q": 3, + "sha256": "193489df1f69cbf7738ba6505f5ca44a9cf89157e1fffd43dc0edc3383c75abb", + "spaces": 2 + }, + { + "direct_sum_decompositions": 14, + "n": 2, + "pairs": 36, + "q": 3, + "sha256": "dce4b3286d34e7d059ea5cff0519578f7f165ee93bfef3fc15e35d8578b61b1c", + "spaces": 6 + }, + { + "direct_sum_decompositions": 236, + "n": 3, + "pairs": 784, + "q": 3, + "sha256": "2ab79a05c014ae849b809883898d4ffce253d151df87be35794b577973caf6e0", + "spaces": 28 + }, + { + "direct_sum_decompositions": 1, + "n": 0, + "pairs": 1, + "q": 5, + "sha256": "5e5f01766a2d71df915f11041d6b8d85b16ef6550c2eddf4a2aa01c1382fa4be", + "spaces": 1 + }, + { + "direct_sum_decompositions": 2, + "n": 1, + "pairs": 4, + "q": 5, + "sha256": "02e6d55a6fc52ba6f05512d0f9e7e6e329e50a4a64be62aacf0405e91eb08b37", + "spaces": 2 + }, + { + "direct_sum_decompositions": 32, + "n": 2, + "pairs": 64, + "q": 5, + "sha256": "98edfd7bf2c174c544430f104065e53f328ac4d2d83317d4eea24772a0ed5b3f", + "spaces": 8 + } + ], + "claim_type": "scoped proof with finite controls", + "formal_word_fixtures": [ + { + "basis": [ + 1 + ], + "factors": 1, + "minimum": 0, + "n": 0, + "regular_input_columns_per_factor": 6, + "u": 0, + "v": 0 + }, + { + "basis": [ + 1, + 2, + 6 + ], + "factors": 7, + "minimum": 1, + "n": 2, + "regular_input_columns_per_factor": 18, + "u": 1, + "v": 0 + }, + { + "basis": [ + 1, + 6, + 2 + ], + "factors": 7, + "minimum": 1, + "n": 2, + "regular_input_columns_per_factor": 18, + "u": 0, + "v": 1 + }, + { + "basis": [ + 1, + 2, + 4 + ], + "factors": 13, + "minimum": 1, + "n": 2, + "regular_input_columns_per_factor": 18, + "u": 1, + "v": 1 + }, + { + "basis": [ + 1, + 2, + 4 + ], + "factors": 13, + "minimum": 2, + "n": 2, + "regular_input_columns_per_factor": 18, + "u": 1, + "v": 1 + }, + { + "basis": [ + 1, + 2, + 4, + 8, + 16 + ], + "factors": 25, + "minimum": 4, + "n": 4, + "regular_input_columns_per_factor": 30, + "u": 2, + "v": 2 + }, + { + "basis": [ + 1, + 2, + 4, + 8 + ], + "factors": 25, + "minimum": 3, + "n": 3, + "regular_input_columns_per_factor": 24, + "u": 2, + "v": 2 + } + ], + "schema_version": 1, + "source_sha256": { + "PROOF.md": "cbcb971bcc29f0d1935306899ac6d89622e852976ac162e82db1b906df7f3aa1", + "README.md": "ed63696a241b5056c7a391888dfecc2bdb7a563cf576c6ea892c7bf6ea16a248", + "SOURCES.json": "ed3e9b82e7260812000d80fa12cf39d0cb75726303d585332a9fdf3182c3046d", + "TASK.json": "d66f5d080c7c25db7d61829869839fd71f9185e92926deda0749f8a19c78e856", + "VERIFY.json": "c2c822265c795643e3cd8b703ba6fbb83a6b28d5ba3e66d71cfe56ae4ca4d562", + "verify.py": "057828d0ae7f95402757bac66ea58e0e948354bc43532e12c86a751877a37cab" + }, + "subspace_pairs": 5669 +} diff --git a/research/exact-factor-workspace/SOURCES.json b/research/exact-factor-workspace/SOURCES.json new file mode 100644 index 0000000000..19651a82e8 --- /dev/null +++ b/research/exact-factor-workspace/SOURCES.json @@ -0,0 +1,44 @@ +{ + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "external_citations": [ + { + "author": "Brian / JoyboyBrian", + "role": "Motivates the exact single-basis boundary. Its S4 slack bound is cited only as a corollary premise, not replayed. No source import or runtime dependency.", + "source_commit": "c46cf15df53f3dad2ce59faec9cdc54184e643e5", + "source_path": "research/s4-slack-workspace-bound/PROOF.md", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4783" + }, + { + "author": "Gareth Davidson / bitplane", + "role": "Main-pinned proof above supplies attribution and the different resynthesis contract. No executable dependency.", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2323" + } + ], + "files": [ + { + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "path": "docs/research/agent-task-catalog.json", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72", + "usage": "provenance" + }, + { + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "path": "certificates/selected-result.json", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375", + "usage": "provenance" + }, + { + "git_blob": "f91d23a43002ac69e884af6d3fe485d0868d5b34", + "path": "research/register-pairing-compression/PROOF.md", + "sha256": "f9c3c3f1363787ed0c92a65abba065d5debcb1e526a439cd3c82ad48d24f27bd", + "usage": "provenance" + }, + { + "git_blob": "8db05b993afe33649afd549f779c613a141806dc", + "path": "research/s4-tight-word-spectator-elimination/README.md", + "sha256": "74f218e5cb2a28986b5db53ede7da419df5d719cd7c3bca0c955a354a24d92c4", + "usage": "provenance" + } + ], + "schema_version": 1 +} diff --git a/research/exact-factor-workspace/TASK.json b/research/exact-factor-workspace/TASK.json new file mode 100644 index 0000000000..cdf45c27f7 --- /dev/null +++ b/research/exact-factor-workspace/TASK.json @@ -0,0 +1,73 @@ +{ + "actual_scope": "Determine the exact dirty dimension and classify/count optimal spectator-only single-basis restrictions of a fixed rank-one word over any field.", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "author": "Nick Petalas", + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "baseline": "Current research_selected_baseline.py passes metadata bindings; the card historical research_baseline.py fails with KeyError bit_lower and is unchanged.", + "bottleneck_link": "An exact fixed-word role bound removes unnecessary spectator enumeration; native conversions and complete supplier costs remain separate.", + "budget_minutes": 60, + "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133318", + "evidence": "Written all-field lower bound and attaining split, exact finite-field split counts, exhaustive small-domain decomposition oracle and full formal S3 word controls. Coverage is generated in RESULT.json.", + "family_decision": "Finish this scoped classification. No larger word search or native implementation campaign is implied.", + "open_questions": [ + { + "blocked_by": "No physical conversion or restricted-gauge theorem is supplied.", + "first_step": "Specify one actual layout and its legal spectator basis subgroup.", + "question": "Can the exact coordinate restriction be computed under native support constraints?", + "why_it_matters": "An arbitrary scalar basis need not preserve a paid physical layout." + }, + { + "blocked_by": "This theorem fixes factors and supplies no endpoint optimum.", + "first_step": "Specify an endpoint and paid budget, then apply the existing contraction-preserving theorem only in a closed alphabet.", + "question": "Which target admits less workspace after its factors change?", + "why_it_matters": "The preserved-factor optimum need not be the endpoint optimum." + } + ], + "original_card": { + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "id": "bit-new-register-model", + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ], + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ] + }, + "outcome": "completed", + "priority_revision": 7, + "schema_version": 1, + "scope_change_reason": "Replace construction search by an exact coordinate-preserving workspace boundary motivated by Brian PR4783. This differs from Gareth Davidson PR2323, which replaces factors while preserving contractions.", + "scope_status": "changed", + "stop_rule": "Ship the first verified exact dimension/classification with bounded subspace and formal-word controls; do not optimize endpoints or expand the mechanism.", + "task_id": "bit-new-register-model" +} diff --git a/research/exact-factor-workspace/VERIFY.json b/research/exact-factor-workspace/VERIFY.json new file mode 100644 index 0000000000..bd6a07f742 --- /dev/null +++ b/research/exact-factor-workspace/VERIFY.json @@ -0,0 +1,34 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "checks": "Exact subspace-pair census against all direct-sum decompositions, optimal split counts, faithful full-formal S3 factors/endpoints and source-bound receipt.", + "timeout_seconds": 120 + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "checks": "The same mathematical controls and receipt checks with Python assertions disabled.", + "timeout_seconds": 120 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/exact-factor-workspace/verify.py b/research/exact-factor-workspace/verify.py new file mode 100644 index 0000000000..d2696e57d8 --- /dev/null +++ b/research/exact-factor-workspace/verify.py @@ -0,0 +1,228 @@ +"""Exact finite controls for fixed-factor spectator basis restriction.""" + +import argparse +import hashlib +import itertools +import json +from pathlib import Path + + +ROOT = Path(__file__).resolve().parent +DOMAINS = ((2, 4), (3, 3), (5, 2)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dot(x, y, q): + return sum(a * b for a, b in zip(x, y, strict=True)) % q + + +def subspaces(q, n): + """Enumerate unique RREF bases and their literal vector-set masks.""" + require(any(q == prime and 0 <= n <= cap for prime, cap in DOMAINS), + 'outside the registered finite domain') + universe = tuple(itertools.product(range(q), repeat=n)) + indices = {v: i for i, v in enumerate(universe)} + spaces = [] + for size in range(n + 1): + for pivots in itertools.combinations(range(n), size): + free = [(i, j) for i, p in enumerate(pivots) + for j in range(p + 1, n) if j not in pivots] + for values in itertools.product(range(q), repeat=len(free)): + rows = [[int(j == p) for j in range(n)] for p in pivots] + for (i, j), value in zip(free, values, strict=True): + rows[i][j] = value + basis = tuple(tuple(row) for row in rows) + mask = 0 + for coefficients in itertools.product(range(q), repeat=size): + v = tuple(sum(c * row[j] for c, row in + zip(coefficients, basis, strict=True)) % q + for j in range(n)) + mask |= 1 << indices[v] + require(mask.bit_count() == q ** size, 'RREF span size') + spaces.append((basis, mask)) + require(len({mask for _, mask in spaces}) == len(spaces), 'duplicate space') + return universe, spaces + + +def parameters(q, n, ubasis, vbasis, universe): + """Find pairing rank from its entire evaluation image, without elimination.""" + images = set() + for coefficients in itertools.product(range(q), repeat=len(ubasis)): + u = tuple(sum(c * row[j] for c, row in + zip(coefficients, ubasis, strict=True)) % q + for j in range(n)) + images.add(tuple(dot(v, u, q) for v in vbasis)) + ranks = [t for t in range(n + 1) if q ** t == len(images)] + require(len(ranks) == 1, 'evaluation image is not a vector space') + t = ranks[0] + u, v = len(ubasis), len(vbasis) + d = u + v - t + k = n - d + require(0 <= t <= min(u, v) and 0 <= d <= n, 'dimension bounds') + ann = sum(1 << i for i, x in enumerate(universe) + if all(dot(row, x, q) == 0 for row in vbasis)) + return d, q ** ((u - t) * k), q ** (k * (u + v - 2 * t)), ann + + +def census(q, n): + universe, spaces = subspaces(q, n) + # The oracle enumerates every ordered direct-sum decomposition, with no + # use of the predicted dimension or the counting formulas. + splits = [(i, j) for i, (a, amask) in enumerate(spaces) + for j, (b, bmask) in enumerate(spaces) + if len(a) + len(b) == n and amask & bmask == 1] + digest = hashlib.sha256() + records = 0 + for ubasis, umask in spaces: + for vbasis, _ in spaces: + d, n_count, pair_count, ann = parameters(q, n, ubasis, vbasis, universe) + legal = [(i, j) for i, j in splits + if umask & ~spaces[i][1] == 0 and spaces[j][1] & ~ann == 0] + require(bool(legal), 'missing decomposition') + best = min(len(spaces[i][0]) for i, _ in legal) + optimal = [(i, j) for i, j in legal if len(spaces[i][0]) == best] + observed = (best, len({j for _, j in optimal}), len(optimal)) + require(observed == (d, n_count, pair_count), 'formula mismatch') + digest.update(json.dumps([umask, list(vbasis), observed], + separators=(',', ':')).encode('ascii')) + records += 1 + return {'q': q, 'n': n, 'spaces': len(spaces), 'pairs': records, + 'direct_sum_decompositions': len(splits), 'sha256': digest.hexdigest()} + + +def apply(columns, vector): + require(0 <= vector < 1 << len(columns), 'column input range') + value = 0 + for i, column in enumerate(columns): + if vector >> i & 1: + value ^= column + return value + + +def compose(left, right): + return tuple(apply(left, column) for column in right) + + +def scalar_lift(columns, output_roles): + require(all(0 <= c < 1 << output_roles for c in columns), 'role range') + return tuple(sum(((c >> i) & 1) << (6 * i + g) + for i in range(output_roles)) + for c in columns for g in range(6)) + + +def factor(roles, u, v, label): + """Faithful left regular S3 action on every role, including all dirt.""" + require(1 <= roles <= 5 and 0 < u < 1 << roles and + 0 < v < 1 << roles and (u & v).bit_count() % 2 == 1, + 'nonzero rank-one idempotent required') + group = tuple(itertools.permutations(range(3))) + indices = {p: i for i, p in enumerate(group)} + require(label in ((1, 0, 2), (0, 2, 1)), 'illegal S3 label') + result = [] + for j in range(roles): + for g, p in enumerate(group): + column = 1 << (6 * j + g) + if v >> j & 1: + moved = indices[tuple(label[p[i]] for i in range(3))] + for i in range(roles): + if u >> i & 1: + column ^= (1 << (6 * i + g)) ^ (1 << (6 * i + moved)) + result.append(column) + return tuple(result) + + +def fixture(n, ubasis, vbasis): + require(0 <= n <= 4, 'fixture size') + universe, spaces = subspaces(2, n) + predicted, _, _, ann = parameters(2, n, ubasis, vbasis, universe) + umask = 0 + for cs in itertools.product(range(2), repeat=len(ubasis)): + u = tuple(sum(c * row[j] for c, row in zip(cs, ubasis, strict=True)) % 2 + for j in range(n)) + umask |= 1 << universe.index(u) + choices = [(a, b) for a, am in spaces for b, bm in spaces + if len(a) == predicted and len(a) + len(b) == n and + am & bm == 1 and umask & ~am == 0 and bm & ~ann == 0] + require(bool(choices), 'fixture has no optimal split') + kept, discarded = choices[0] + basis = (1,) + tuple(sum(x << (j + 1) for j, x in enumerate(row)) + for row in kept + discarded) + lookup = {apply(basis, x): x for x in range(1 << (n + 1))} + require(len(lookup) == 1 << (n + 1), 'basis not invertible') + inverse = tuple(lookup[1 << i] for i in range(n + 1)) + return check_word(n, ubasis, vbasis, predicted, basis, inverse) + + +def check_word(n, ubasis, vbasis, d, basis, inverse): + a, b = (1, 0, 2), (0, 2, 1) + word = [(1, 1, a)] + projectors = [(1 | sum(x << (j + 1) for j, x in enumerate(row)), 1) + for row in ubasis] + projectors += [(1, 1 | sum(x << (j + 1) for j, x in enumerate(row))) + for row in vbasis] + for u, v in projectors: + word.extend((u, v, label) for label in (a, b, a, b, a, b)) + full = tuple(1 << i for i in range(6 * (n + 1))) + reduced = tuple(1 << i for i in range(6 * (d + 1))) + lifted = scalar_lift(basis, n + 1) + ilifted = scalar_lift(inverse, n + 1) + identity_dirt = tuple(1 << i for i in range(6 * (n + 1))) + for u, v, label in word: + gate = factor(n + 1, u, v, label) + up = apply(inverse, u) + vp = sum(((v & column).bit_count() % 2) << j + for j, column in enumerate(basis)) + require(up < 1 << (d + 1) and vp < 1 << (d + 1), 'discarded support') + small = factor(d + 1, up, vp, label) + target = small + identity_dirt[6 * (d + 1):] + require(compose(ilifted, compose(gate, lifted)) == target, + 'full factor intertwiner') + full = compose(gate, full) + reduced = compose(small, reduced) + require(full == factor(n + 1, 1, 1, a), 'original dirty endpoint') + require(reduced == factor(d + 1, 1, 1, a), 'reduced dirty endpoint') + return {'n': n, 'u': len(ubasis), 'v': len(vbasis), 'minimum': d, + 'factors': len(word), 'basis': list(basis), + 'regular_input_columns_per_factor': 6 * (n + 1)} + + +def report(): + rows = [census(q, n) for q, cap in DOMAINS for n in range(cap + 1)] + e1, e2 = (1, 0), (0, 1) + fixtures = [fixture(0, (), ()), fixture(2, (e1,), ()), + fixture(2, (), (e2,)), fixture(2, (e1,), (e1,)), + fixture(2, (e1,), (e2,)), + fixture(4, ((1, 0, 0, 0), (0, 1, 0, 0)), + ((0, 0, 1, 0), (0, 0, 0, 1))), + fixture(3, ((1, 1, 0), (0, 1, 1)), + ((1, 0, 1), (1, 1, 1)))] + return {'schema_version': 1, 'claim_type': 'scoped proof with finite controls', + 'census': rows, 'subspace_pairs': sum(r['pairs'] for r in rows), + 'formal_word_fixtures': fixtures, + 'source_sha256': {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(ROOT.iterdir()) + if p.is_file() and p.name != 'RESULT.json'}} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write-result', type=Path) + args = parser.parse_args() + measured = report() + if args.write_result: + with args.write_result.open('x', encoding='utf-8') as handle: + payload = json.dumps(measured, indent=2, sort_keys=True) + '\n' + require(handle.write(payload) == len(payload), 'short receipt write') + else: + expected = json.loads((ROOT / 'RESULT.json').read_text(encoding='utf-8')) + require(measured == expected, 'receipt or source mismatch') + print('PASS_EXACT_FACTOR_WORKSPACE', measured['subspace_pairs'], + 'subspace pairs;', len(measured['formal_word_fixtures']), 'formal words') + + +if __name__ == '__main__': + main()