From 93a05b2221fb68c9e134d45b70e289bd7b7bc289 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 23:24:54 +0100 Subject: [PATCH] feat(research): bound permutation workspace by inversion slack --- research/permutation-slack-workspace/PROOF.md | 182 ++++++++ .../permutation-slack-workspace/README.md | 185 +++++++++ .../permutation-slack-workspace/SOURCES.json | 30 ++ .../permutation-slack-workspace/TASK.json | 101 +++++ .../permutation-slack-workspace/VERIFY.json | 59 +++ .../permutation-slack-workspace/oracle.py | 74 ++++ .../permutation-slack-workspace/verify.py | 393 ++++++++++++++++++ 7 files changed, 1024 insertions(+) create mode 100644 research/permutation-slack-workspace/PROOF.md create mode 100644 research/permutation-slack-workspace/README.md create mode 100644 research/permutation-slack-workspace/SOURCES.json create mode 100644 research/permutation-slack-workspace/TASK.json create mode 100644 research/permutation-slack-workspace/VERIFY.json create mode 100644 research/permutation-slack-workspace/oracle.py create mode 100644 research/permutation-slack-workspace/verify.py diff --git a/research/permutation-slack-workspace/PROOF.md b/research/permutation-slack-workspace/PROOF.md new file mode 100644 index 0000000000..6c26a08010 --- /dev/null +++ b/research/permutation-slack-workspace/PROOF.md @@ -0,0 +1,182 @@ +# Inversion-weighted spectator reduction + +This contribution is produced by Nick Petalas. Apache-2.0. + +This is a scoped algebraic proof. Its finite controls are corroboration, +not a proof of the universal quantifiers or a complete multiplication theorem. + +## Statement + +Let F be any field, n>=2, and R=A direct-sum S a finite-dimensional scalar +role space, with dim A=w. Work in M_R(F[S_n]). For a nonidentity permutation g +and scalar column u and row v with vu=1, define + + G_g(u,v) = I + ([g]-[e])uv. + +The inverse is G_(g^-1)(u,v). Consider a nonempty normalized written word + + T = G_(g_1)(u_1,v_1) ... G_(g_m)(u_m,v_m) = Q_A direct-sum I_S. + +The endpoint equality is coefficientwise in the full group algebra. It +includes arbitrary dirty inputs, every off-diagonal coefficient, and complete +spectator restoration. No restriction to diagonal active endpoints is made. +Put d_i=inv(g_i)>0 and d_*=min_i d_i. Let permutations act on ordered distinct +pairs, let H be the increasing-pair subspace tensored with R, and K the +decreasing-pair subspace. For the represented endpoint set + + L = rank(projection_K T restricted_to H). + +**Theorem.** A single spectator-only scalar basis change, fixing the original +active coordinates, puts every original paid factor on at most + + w + floor((sum_i d_i - L)/d_*) + +total roles. Restricting those same factors preserves their labels, order, +rank-one idempotents and full formal endpoint. The retained extra roles remain +arbitrary dirty inputs and are restored. In particular sum_i d_i>=L. + +When all labels have inversion count d, the bound is +w+m-ceil(L/d). At d=1 this recovers Brian/JoyboyBrian's #4783 simple-label +bound. The new statement admits non-simple and non-involutive labels, varying +inversion counts, arbitrary symmetric groups, and every scalar field. + +The empty word needs no dirty roles and is treated separately. Identity +labels can be deleted before defining d_*. This theorem does not price a label +as inv(g) physical calls; d_i is a geometric quantity used to bound workspace. + +## The crossing decomposition + +Write U_+ for the span of increasing pairs and U_- for decreasing pairs. +For any permutation h let C be the coordinate intersection U_+ intersect hU_+, +let X be the coordinate complement of C in U_+, and Y the negative coordinate +part of hU_+. Thus + + U_+ = C direct-sum X, hU_+ = C direct-sum Y, + dim X = dim Y = inv(h) = d. + +This holds because the ordered-pair action is a permutation action. An inversion +is precisely an increasing pair sent to a decreasing one. No involution +assumption is used. Since R=ker(v) direct-sum span(u), the represented gate is +identity on ker(v) and h on span(u). Consequently + + G_h H = (R tensor C) direct-sum (ker(v) tensor X) + direct-sum (span(u) tensor Y). (1) + +In particular d(H,G_h H)=d, where d(B,C)=dim B-dim(B intersect C) is the +Grassmann distance for subspaces of the same dimension. Also + + H intersect G_h H = ker(ell), + +where ell:H -> F^d applies v to each X-coordinate. Its quotient in G_h H +has dimension d. Formula (1) is the new replacement for the predecessor's +one-crossing decomposition. + +## The local charge + +Suppose the current residual P has full formal form P_A0 direct-sum I_S0. +Define phi(P)=rank(projection_K P restricted_to H). Equivalently +phi(P)=d(H,P^-1 H). Put Z=P^-1 H and D=H intersect Z. + +Peel a rightmost factor G_g by multiplying P on the right by its inverse. +Set h=g^-1 and Y0=G_(g^-1) H. Invariance of Grassmann distance gives + + phi(P G_g^-1) - phi(P) + = dim D - dim(Y0 intersect Z). (2) + +Indeed phi(PG_g^-1)=d(H,G_g P^-1 H)=d(G_g^-1 H,P^-1 H). +In (1) use h=g^-1 throughout this local step. Both h and g have +inversion count d. + +Write a for the S0 component of u, b for the restriction of v to S0, and +eta=1[a!=0]+1[b!=0]. Then + + d eta <= d + phi(P G_g^-1) - phi(P). (3) + +To prove this, note that Z contains S0 tensor U_+ and has no negative +spectator component. If b!=0, ell restricted to D has rank exactly d, +because D contains S0 tensor X and b is a nonzero functional there. +Thus dim(D intersect ker ell)=dim D-d. + +If a!=0, any nonzero Y-coordinate in (1) has a nonzero negative spectator +component, so cannot lie in Z. Therefore +Y0 intersect Z=D intersect ker ell. If both a,b are nonzero, (2) is exactly +d, proving (3) with eta=2. If a!=0 and b=0, (2) is nonnegative, proving +(3) with eta=1. + +If a=0 and b!=0, the quotient of Y0 intersect Z by D intersect ker ell +injects into Y0/(Y0 intersect H), a space of dimension d. Hence its dimension +is at most dim D, so (2) is nonnegative and again eta=1 is charged. +If a=b=0, the distance triangle gives (2)>=-d, completing the four cases. + +The nonnegative local slack s=d+phi(PG_g^-1)-phi(P) therefore pays +eta<=s/d<=s/d_* dirty directions. This step is valid for arbitrary invertible +active represented maps. It does not use faithfulness to admit an endpoint. + +## Nested splits and the global word + +For a vector a in S0 and functional b on S0, choose S0=V direct-sum S1, +with a in V and b annihilating S1. Such a V has dimension at most eta. +If a=b=0 take V=0. If just one is nonzero, retain its vector or a vector +t with b(t)=1, respectively. If both are nonzero and b(a)!=0, take V=span(a) +and S1=ker b. If both are nonzero and b(a)=0, choose b(t)=1 and take +V=span(a,t), with S1 a complement to span(a) in ker b. These constructions +work over every field. + +Enlarge A0 to A1=A0 direct-sum V. The peeled factor has u in A1 and v +annihilates S1. Both the old residual and its peeled successor preserve A1 +and are identity on S1 in the full formal algebra. Repeat, starting at T +and peeling factors from right to left. The final residual is identity. +All retained V spaces lie inside the original spectator space. Telescoping +the local nonnegative slacks gives + + retained_dirty <= sum_i s_i/d_* + = (sum_i d_i + phi(I) - phi(T))/d_* + = (sum_i d_i - L)/d_*. + +The retained dimension is an integer, giving the floor in the theorem. +The distance triangle also directly gives sum_i d_i>=L. + +Take a basis of the retained V spaces in peeling order, followed by a basis +of the final discarded spectator space. This is one scalar basis of S, with +the original active basis fixed. Let J include the retained role space and +E project onto it along the discarded space. Every original factor satisfies +u_i=J u_i' and v_i=v_i' E, with EJ=I. Thus + + v_i' u_i'=1, G_i J=J G_i', E G_i=G_i' E, + G_i = G_i' direct-sum I_discarded. + +These identities hold coefficientwise in F[S_n], not just in the ordered-pair +representation. Multiplication gives the original complete endpoint on the +retained roles. Labels, order and every label-dependent tariff are preserved. + +## Sharpness and scope + +For any nonidentity g with d inversions, take one active axis e0 and two dirty +axes e1,e2. Let u=e0+e1 and v=e0*+e2*, so vu=1. The written word + + G_g(e0,e0*) G_g(u,v) G_(g^-1)(u,v) + +has endpoint diag([g],1,1), total inversion mass 3d, L=d and d_*=d. +The theorem retains at most two dirty roles. Both are necessary if the actual +factors must survive one spectator-only basis change: their nonzero dirty +image and dirty functional have zero pairing. On a one-dimensional space, +a nonzero vector and functional have nonzero pairing. This proves sharpness +of the coefficient for this reduction, over every field, including a genuinely +non-involutive 3-cycle. The canceling pair makes no endpoint-optimal-workspace +or shortest-word claim. + +The result answers #4783's non-simple-label charge question. Brian's nested +splits, positive-slack framework and preserved-factor sharpness mechanism +remain predecessor credit. Ross Richardson #1989 supplies the ordered-pair +inversion cut, following Adam Gall #1941 and Ross Richardson #1966. Credit +Sagar Thakrar #3888, Arham Tahir #2998 and Nick Petalas #2583/#3408 for the +retained weighted-register context. The proof is self-contained and imports +no pending executable or finite-exclusion receipt. + +This is a fixed-word algebraic workspace reduction. It gives no physical +basis-conversion algorithm or native tariff, and permits neither nilpotent +couplings, unreturned spectators nor free address operations. Scalar mixing +is normalized into the given rank-one idempotents; augmentation forces any +remaining free scalar endpoint to be identity. Precision, tape, ownership, +hosting, complete supplier admission and all-size multiplication transfer +remain separate obligations. No new kappa is claimed. diff --git a/research/permutation-slack-workspace/README.md b/research/permutation-slack-workspace/README.md new file mode 100644 index 0000000000..496fcf8a85 --- /dev/null +++ b/research/permutation-slack-workspace/README.md @@ -0,0 +1,185 @@ +# Dirty workspace from inversion-weighted permutation slack + +A fixed formal word with arbitrary nonidentity permutation labels can be +restricted to at most + +```text +active roles + floor((sum label inversions - endpoint crossing rank) + / smallest label inversion count). +``` + +This is a scoped all-field algebraic proof with exact finite corroboration. +The restriction preserves every original rank-one idempotent, paid label, +written order and full arbitrary-dirty-input endpoint. When every label has +the same inversion count d, the bound is `w+m-ceil(L/d)` total roles. +There is no new kappa or complete multiplication theorem. + +This answers the first Open next question in Brian/JoyboyBrian's +[PR #4783](https://github.com/CrocSwap/integer-mult-bounds/pull/4783), read at +`c46cf15df53f3dad2ce59faec9cdc54184e643e5`. That predecessor proves the +simple adjacent S4 case and leaves non-simple labels open. Its local-charge +method, nested spectator splits and fixed-word sharpness mechanism retain +predecessor credit. The new step replaces one crossing by the complete +inversion-sized coordinate crossing space. Non-involutive labels use their +literal inverse when peeling. The theorem covers all symmetric groups and +all scalar fields. + +## Exact boundary and result + +Let F be any field, `R=A direct-sum S` a finite scalar role space, `dim A=w`, +and `n>=2`. A paid factor in `M_R(F[S_n])` is + +```text +G_g(u,v) = I + ([g]-[e])uv, vu=1, g != e. +``` + +A nonempty normalized word has full formal endpoint `Q_A direct-sum I_S`. +The active block may be non-diagonal. Every spectator input is arbitrary +and must be restored; every off-diagonal formal coefficient is constrained. +Define `d_i=inv(g_i)`, `d_*=min d_i`, and `L` as the endpoint's crossing rank +in the ordered-distinct-pair representation, increasing pairs to decreasing +pairs. Then one spectator-only scalar basis change fixing A supports every +original factor on at most `w+floor((sum d_i-L)/d_*)` roles. + +The [proof](PROOF.md) gives the exact crossing decomposition and four-case +local inequality + +```text +d_i * (1[dirty image != 0] + 1[dirty functional != 0]) + <= d_i + phi(peeled residual) - phi(current residual). +``` + +Each right-hand side is nonnegative. Explicit nested splits and telescoping +prove the bound; full group-algebra intertwiners prove the retained endpoint. +The ordered-pair representation supplies a necessary geometric charge and +is never used as a full endpoint oracle. + +The coefficient is sharp for preserving the given factors. A nonidentity +coordinate call followed by a canceling non-simple gate/inverse pair has +inversion slack `2d` and needs two dirty directions under the stated basis +restriction. Their nonzero image and functional have zero pairing, which +cannot happen on a one-dimensional retained dirty space. This says nothing +about the endpoint's minimum workspace after resynthesis: the pair cancels. + +Identity labels can be removed first. The empty word needs no extra roles. +The inversion count is a geometric weight, not an asserted native-call tariff. + +## Evidence and reproduction + +Python 3.12 and the standard library suffice. From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/permutation-slack-workspace +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/permutation-slack-workspace/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/permutation-slack-workspace/oracle.py +``` + +On another machine substitute its CPython 3.12 path. Normal replay writes +nothing. `verify.py --emit /absolute/new/path.json` explicitly generates a +receipt with every package source hash and the recomputed transcript. It +refuses an occupied output path. `--receipt /absolute/path.json` recomputes +and compares every receipt field. Default replay checks the mathematical +invariants directly; no generated output stays in the checkout. The source +hashes authenticate bytes, not mathematical truth or independent authorship. + +The primary check covers 5,625 local peels. Every permutation label and +rank-one projector is enumerated within these six finite domains; active +maps are a declared deterministic sample of invertible maps on one active +role's ordered-pair space, not an exhaustive GL census. + +| Permutations | Field | Total roles | Active maps per label/projector | Peels | +| --- | --- | ---: | ---: | ---: | +| S2 | F2 | 3 | 4 | 112 | +| S3 | F2 | 3 | 4 | 560 | +| S4 | F2 | 3 | 3 | 1,932 | +| S3 | F3 | 3 | 3 | 1,755 | +| S4 | F3 | 2 | 2 | 552 | +| S5 | F2 | 2 | 1 | 714 | + +It also checks 576 literal crossing-space decompositions, four sharpness +words in the full formal algebra, 300 complete regular-action dirty-input +basis columns, and two constructive nested mixed-label compressions over +F2 and F3. The nested words reduce six roles to four by one computed scalar +basis, preserving every factor. Seven controls cover malformed permutations, +nilpotent couplings, unsupported fields, unreturned dirt, forward-for-inverse +substitution, unit crossing undercharge and the one-dimensional sharpness +boundary. + +`oracle.py` imports no primary code. It enumerates actual 512-element binary +subspace sets and computes intersection dimensions from their cardinalities. +All 840 cases cover every S3 active permutation, every nonidentity paid S3 +label and every rank-one idempotent on three scalar roles. All crossing +lengths 1,2,3 and dirty-component counts 0,1,2 occur. This checks the local +charge without matrix Gaussian elimination or the predicted decomposition. +Both registered normal and optimized modes use explicit runtime checks. + +The written proof establishes the quantified theorem. These finite domains +do not establish an arbitrary-word exclusion or audit a predecessor result. + +## Scope, sources and credit + +Scientific base `624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7. +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133755). +The original card was `formal-interface-lemma`; this is a declared scope +change to an elementary quantified proof of an explicitly open interface +question. The selected source-binding positive control passed. The historical +card command `research_baseline.py` raises `KeyError: 'bit_lower'` against the +current selected certificate schema; neither command is a scientific replay. + +`SOURCES.json` pins the catalogue, selected record and merged predecessor +notes as Git provenance. The pending #4783 is an exact external citation, +not an imported executable or a source-history dependency. The proof is +self-contained. No predecessor checker or finite receipt was replayed. + +The live overlap helper at 22:17-22:18 UTC on October 22 covered 380 open PRs +and 3,860 Discussion records with complete pagination. Its local sparse scan +covered 69 of 6,319 main notes. Distinctive `git grep origin/main` searches +separately searched main README objects, and live merged/open PR searches +and this account's last-hour claims were checked. No matching non-simple +slack theorem was found in that coverage. Arbitrary diffs, unretained closed +work and unpublished investigations remain outside coverage. This is not a +novelty certificate. + +Related open work is #4783, the simple-label slack theorem; #4847, the exact +scalar minimum for a supplied factor list under the same basis restriction; +and #4851, shortest S3 word rigidity. This contribution proves a geometric +slack inequality for a changed label alphabet. It does not extend the scalar +classification or shortest-word result and compares no predecessor numbers. + +Credit Brian/JoyboyBrian #4783/#4765, Ross Richardson #1989/#1966, +Adam Gall #1941, Sagar Thakrar #3888, Arham Tahir #2998, +Nick Petalas #2583/#3408 and their retained register-model predecessors. +The elementary Grassmann distance and linear complement arguments are +standard; no literature-priority claim is made. + +This contribution is produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +## Limits + +This is a fixed-word formal reduction. Native realization, physical scalar +basis conversion, gauge restrictions, source access, ownership, hosting, +precision, tape and complete supplier/outer admission remain unknown here. +They are not zero-cost assumptions. No selected frontier changes. + +## Open next questions + +- Does a specified changed permutation-label target and paid budget make + this finite-role bound materially reduce a necessary search? First give + its full alphabet and endpoint crossing rank. A candidate with an actual + physical allowance is missing; this package does not justify a large census. +- Can higher-rank scalar idempotents support a corresponding workspace + charge? First derive their exact crossing subspace and split requirement. + The rank-one image/functional argument does not establish that extension. + +## Implementation bounds + +Both Python files use explicit finite domains. Control flow is +nonrecursive, functions are below 60 lines, and all domains are explicitly +bounded: n<=5, at most six roles, prime fields 2,3,5 and at most 120 group +labels. The largest regular-action fixture is 120 by 120. The nested split +enumerates at most 3^5 scalar candidates; the independent oracle holds +512-element sets in an 18-dimensional binary space. Python and standard-library +allocations are bounded by these finite domains. There is no dynamic code +generation or external process. Registered normal and optimized replays +treat warnings as errors. diff --git a/research/permutation-slack-workspace/SOURCES.json b/research/permutation-slack-workspace/SOURCES.json new file mode 100644 index 0000000000..b4ba1bdbb1 --- /dev/null +++ b/research/permutation-slack-workspace/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/s4-tight-word-spectator-elimination/README.md", + "usage": "provenance", + "git_blob": "8db05b993afe33649afd549f779c613a141806dc", + "sha256": "74f218e5cb2a28986b5db53ede7da419df5d719cd7c3bca0c955a354a24d92c4" + }, + { + "path": "research/symmetric-adjacent-cut-bound/README.md", + "usage": "provenance", + "git_blob": "cdb3f431acc07b4a75abdd3998093fd68d9a498f", + "sha256": "4fb453c83d7cd15a93fc7c65b82f2f67cb609a31285ac9ebd1f44b675777d154" + } + ] +} diff --git a/research/permutation-slack-workspace/TASK.json b/research/permutation-slack-workspace/TASK.json new file mode 100644 index 0000000000..619ae51d36 --- /dev/null +++ b/research/permutation-slack-workspace/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "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": "All-field inversion-weighted spectator reduction for arbitrary nonidentity permutation labels, preserving the original factors and full dirty endpoint.", + "scope_change_reason": "Answer the non-simple-label Open next question in Brian/JoyboyBrian #4783 by a self-contained elementary proof rather than proof-assistant binding.", + "bottleneck_link": "A finite role bound can close unbounded dirty-workspace obligations for a changed permutation alphabet; physical supplier pricing remains separate.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved extension with exact local and full formal controls; do not expand to a new word search.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py and independent subspace-set oracle.py; optional generated hash-bound receipt is emitted outside the checkout.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which specified changed permutation-label target and paid budget benefits from the finite role bound?", + "why_it_matters": "Could replace an unbounded dirty-workspace search by a justified finite question.", + "first_step": "Specify the full alphabet, complete endpoint and crossing rank before a census.", + "blocked_by": "No concrete physically funded candidate is supplied." + }, + { + "question": "Can higher-rank scalar idempotents support an analogous charge?", + "why_it_matters": "Would extend the algebraic operation boundary.", + "first_step": "Derive the exact crossing subspace and spectator split requirement for one rank-two idempotent.", + "blocked_by": "The rank-one split proof does not cover that case." + } + ] +} diff --git a/research/permutation-slack-workspace/VERIFY.json b/research/permutation-slack-workspace/VERIFY.json new file mode 100644 index 0000000000..ef70287ee2 --- /dev/null +++ b/research/permutation-slack-workspace/VERIFY.json @@ -0,0 +1,59 @@ +{ + "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 new permutation-slack proof controls, verify.py, normal" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact new permutation-slack proof controls, verify.py, optimized" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/oracle.py" + ], + "timeout_seconds": 120, + "checks": "Exact new permutation-slack proof controls, oracle.py, normal" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/oracle.py" + ], + "timeout_seconds": 120, + "checks": "Exact new permutation-slack proof controls, oracle.py, optimized" + } + ] +} diff --git a/research/permutation-slack-workspace/oracle.py b/research/permutation-slack-workspace/oracle.py new file mode 100644 index 0000000000..62c9e4a63d --- /dev/null +++ b/research/permutation-slack-workspace/oracle.py @@ -0,0 +1,74 @@ +#!/usr/bin/env python3 +"""Enumerate actual binary subspace sets, without the primary rank engine. + +Nick Petalas. Apache-2.0. +""" +from itertools import permutations + + +def check(ok, message): + if not ok: + raise ValueError(message) + + +def send(value, permutation, addresses): + out = 0 + for i, (a, b) in enumerate(addresses): + if value >> i & 1: + target = addresses.index((permutation[a], permutation[b])) + out ^= 1 << target + return out + + +def controlled(value, g, u, v, addresses): + width = len(addresses) + mask = (1 << width)-1 + read = 0 + for role in range(3): + if v >> role & 1: + read ^= (value >> (role*width)) & mask + delta = read ^ send(read, g, addresses) + out = value + for role in range(3): + if u >> role & 1: + out ^= delta << (role*width) + return out + + +def dimension(size): + check(size > 0 and size & (size-1) == 0, "not a binary subspace size") + return size.bit_length()-1 + + +def main(): + address = [(i, j) for i in range(3) for j in range(3) if i != j] + positive = [r*6+i for r in range(3) for i, (a, b) in enumerate(address) if a < b] + h = {sum(((bits >> j) & 1) << i for j, i in enumerate(positive)) + for bits in range(1 << 9)} + total, kinds = 0, set() + for active in permutations(range(3)): + pi = tuple(active.index(i) for i in range(3)) + z = {(value & ~63) | send(value & 63, pi, address) for value in h} + before = 9-dimension(len(h & z)) + for g in permutations(range(3)): + d = sum(g[i] > g[j] for i in range(3) for j in range(i+1, 3)) + if d == 0: + continue + gi = tuple(g.index(i) for i in range(3)) + for u in range(1, 8): + for v in range(1, 8): + if (u & v).bit_count() % 2 != 1: + continue + y = {controlled(value, gi, u, v, address) for value in h} + after = 9-dimension(len(y & z)) + eta = int(u >> 1 != 0)+int(v >> 1 != 0) + check(d*eta <= d+after-before, "enumerated subspace charge failed") + kinds.add((d, eta)) + total += 1 + check(total == 840, "incomplete finite domain") + check(kinds == {(d, eta) for d in (1, 2, 3) for eta in (0, 1, 2)}, "missing boundary case") + print("PASS_SUBSPACE_SET_ORACLE", total, "literal subspace intersections") + + +if __name__ == "__main__": + main() diff --git a/research/permutation-slack-workspace/verify.py b/research/permutation-slack-workspace/verify.py new file mode 100644 index 0000000000..0cb517e451 --- /dev/null +++ b/research/permutation-slack-workspace/verify.py @@ -0,0 +1,393 @@ +#!/usr/bin/env python3 +"""Exact finite controls for the permutation spectator-slack proof. + +Nick Petalas. Apache-2.0. +""" +import argparse +from hashlib import sha256 +from itertools import permutations, product +import json +from math import factorial +from pathlib import Path +import random + +HERE = Path(__file__).resolve().parent + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def rank(rows, q): + if not rows: + return 0 + a, r = [list(row) for row in rows], 0 + for col in range(len(a[0])): + pivot = next((i for i in range(r, len(a)) if a[i][col] % q), None) + if pivot is None: + continue + a[r], a[pivot] = a[pivot], a[r] + z = pow(a[r][col] % q, -1, q) + a[r] = [(z * x) % q for x in a[r]] + for i in range(r + 1, len(a)): + if a[i][col] % q: + z = a[i][col] % q + a[i] = [(x - z * y) % q for x, y in zip(a[i], a[r])] + r += 1 + if r == len(a): + break + return r + + +def eye(n): + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def mul(a, b, q): + out = [[0] * len(b[0]) for _ in a] + for i, row in enumerate(a): + for k, z in enumerate(row): + if z: + out[i] = [(x + z * y) % q for x, y in zip(out[i], b[k])] + return out + + +def inv(a, q): + n = len(a) + b = [list(row) + tail for row, tail in zip(a, eye(n))] + for j in range(n): + pivot = next((i for i in range(j, n) if b[i][j] % q), None) + require(pivot is not None, "singular scalar basis") + b[j], b[pivot] = b[pivot], b[j] + z = pow(b[j][j] % q, -1, q) + b[j] = [(z*x) % q for x in b[j]] + for i in range(n): + if i != j: + z = b[i][j] + b[i] = [(x-z*y) % q for x, y in zip(b[i], b[j])] + return [row[n:] for row in b] + + +def matvec(a, u, q): + return tuple(sum(x*y for x, y in zip(row, u)) % q for row in a) + + +def inverse_perm(g): + return tuple(g.index(i) for i in range(len(g))) + + +def compose(g, h): + return tuple(g[h[i]] for i in range(len(g))) + + +def inversions(g): + return sum(g[i] > g[j] for i in range(len(g)) for j in range(i + 1, len(g))) + + +def projectors(r, q): + out = [] + for u in product(range(q), repeat=r): + if not any(u) or next(x for x in u if x) != 1: + continue + for v in product(range(q), repeat=r): + if sum(x * y for x, y in zip(u, v)) % q == 1: + out.append((u, v)) + return out + + +def pairs(n): + return [(i, j) for i in range(n) for j in range(n) if i != j] + + +def gate(g, u, v, q, regular=False): + n, r = len(g), len(u) + require(2 <= n <= 5 and 1 <= r <= 6 and len(v) == r, "gate dimensions") + require(q in (2, 3, 5), "unsupported finite field") + require(sorted(g) == list(range(n)), "illegal permutation") + require(sum(x * y for x, y in zip(u, v)) % q == 1, "not an idempotent") + domain = list(permutations(range(n))) if regular else pairs(n) + index, d = {a: i for i, a in enumerate(domain)}, len(domain) + a = eye(r * d) + for j in range(r): + for k, address in enumerate(domain): + target = compose(g, address) if regular else (g[address[0]], g[address[1]]) + t = index[target] + for i in range(r): + z = u[i] * v[j] + a[i*d+t][j*d+k] = (a[i*d+t][j*d+k] + z) % q + a[i*d+k][j*d+k] = (a[i*d+k][j*d+k] - z) % q + return a + + +def crossing(a, n, r, q): + domain = pairs(n) + h = [i for i, (x, y) in enumerate(domain) if x < y] + k = [i for i, (x, y) in enumerate(domain) if x > y] + d = len(domain) + return rank([[a[i*d+x][j*d+y] for j in range(r) for y in h] + for i in range(r) for x in k], q) + + +def active_map(d, seed, q): + a, rng = eye(d), random.Random(seed) + for _ in range(3 * d): + i, j = rng.sample(range(d), 2) + a[i] = [(x + y) % q for x, y in zip(a[i], a[j])] + require(rank(a, q) == d, "active map must be invertible") + return a + + +def local_controls(): + counts, hist = {}, {} + domains = [(2, 3, 2, 4), (3, 3, 2, 4), (4, 3, 2, 3), + (3, 3, 3, 3), (4, 2, 3, 2), (5, 2, 2, 1)] + for n, r, q, samples in domains: + d, total = n * (n - 1), 0 + active = [active_map(d, 100*n+s, q) for s in range(samples)] + for g in permutations(range(n)): + length = inversions(g) + if not length: + continue + for u, v in projectors(r, q): + peel = gate(inverse_perm(g), u, v, q) + for a in active: + p = eye(r * d) + for i in range(d): + p[i][:d] = a[i] + before, after = crossing(p, n, r, q), crossing(mul(p, peel, q), n, r, q) + eta = int(any(u[1:])) + int(any(v[1:])) + require(length * eta <= length + after - before, "local charge") + key = f"d={length},eta={eta},delta={after-before}" + hist[key] = hist.get(key, 0) + 1 + total += 1 + require(total == (factorial(n)-1)*((q**r-1)//(q-1))*q**(r-1)*samples, + "local domain coverage") + counts[f"S{n}/F{q}/roles{r}"] = total + return {"domains": counts, "peels": sum(counts.values()), "histogram": hist} + + +def decomposition(g, u, v, q): + n, r = len(g), len(u) + domain, h = pairs(n), [(i, j) for i in range(n) for j in range(i+1, n)] + index, d = {x: i for i, x in enumerate(domain)}, len(domain) + image = {(g[x], g[y]) for x, y in h} + common, cross_h, cross_k = sorted(set(h) & image), sorted(set(h)-image), sorted(image-set(h)) + require(len(cross_h) == len(cross_k) == inversions(g), "crossing sets") + a = gate(g, u, v, q) + actual = [[a[i][j*d+index[x]] for i in range(r*d)] for j in range(r) for x in h] + expected = [[int(i == j*d+index[x]) for i in range(r*d)] + for j in range(r) for x in common] + pivot = next(i for i in range(r) if v[i]) + for j in range(r): + if j == pivot: + continue + z = (-v[j] * pow(v[pivot], -1, q)) % q + for x in cross_h: + expected.append([(int(i == j*d+index[x]) + z*int(i == pivot*d+index[x])) % q + for i in range(r*d)]) + for x in cross_k: + expected.append([u[i//d] * int(i % d == index[x]) for i in range(r*d)]) + target = r * len(h) + require(rank(expected, q) == target, "decomposition dimension") + require(rank(actual + expected, q) == target, "literal GH decomposition") + + +def subspace_controls(): + count = 0 + for n, r, q in [(3, 3, 2), (4, 2, 3), (5, 1, 5)]: + for g in permutations(range(n)): + for u, v in projectors(r, q): + decomposition(g, u, v, q) + count += 1 + return count + + +def formal_product(word, n, r, q): + result = {tuple(range(n)): eye(r)} + for g, u, v in word: + nxt = {} + for h, a in result.items(): + au = [sum(a[i][j] * u[j] for j in range(r)) % q for i in range(r)] + for label, sign in ((h, -1), (compose(h, g), 1)): + out = nxt.setdefault(label, [[0] * r for _ in range(r)]) + for i in range(r): + for j in range(r): + out[i][j] = (out[i][j] + sign * au[i] * v[j]) % q + out = nxt.setdefault(h, [[0] * r for _ in range(r)]) + for i in range(r): + for j in range(r): + out[i][j] = (out[i][j] + a[i][j]) % q + result = {g: a for g, a in nxt.items() if any(any(row) for row in a)} + return result + + +def split_basis(a, b, q): + s, kept = len(a), [] + if any(a): + kept.append(a) + if any(b) and (not any(a) or sum(x*y for x, y in zip(a, b)) % q == 0): + j = next(i for i in range(s) if b[i]) + kept.append(tuple(int(i == j) for i in range(s))) + columns = list(kept) + for x in product(range(q), repeat=s): + if sum(z*y for z, y in zip(x, b)) % q == 0 and rank(columns+[x], q) > len(columns): + columns.append(x) + require(len(columns) == s, "spectator split spans") + return [list(row) for row in zip(*columns)], len(kept) + + +def transform(word, basis, q): + bi = inv(basis, q) + return [(g, matvec(bi, u, q), matvec(list(zip(*basis)), v, q)) for g, u, v in word] + + +def represented_word(word, n, r, q): + result = eye(r*n*(n-1)) + for g, u, v in word: + result = mul(result, gate(g, u, v, q), q) + return result + + +def compress(word, n, w, q): + r, original_w = len(word[0][1]), w + basis, work, charges = eye(r), word, [] + endpoint_rank = crossing(represented_word(word, n, r, q), n, r, q) + for end in range(len(word), 0, -1): + g, u, v = work[end-1] + residual = formal_product(work[:end], n, r, q) + for h, matrix in residual.items(): + for i in range(r): + for j in range(r): + if i >= w or j >= w: + require(matrix[i][j] == int(h == tuple(range(n)) and i == j), + "residual must restore every current spectator") + before = crossing(represented_word(work[:end], n, r, q), n, r, q) + after = crossing(represented_word(work[:end-1], n, r, q), n, r, q) + eta, d = int(any(u[w:]))+int(any(v[w:])), inversions(g) + require(d*eta <= d+after-before, "global peel charge") + change, added = split_basis(u[w:], v[w:], q) + full = eye(r) + for i in range(r-w): + full[w+i][w:] = change[i] + basis = mul(basis, full, q) + work = transform(work, full, q) + charges.append({"d": d, "delta": after-before, "eta": eta, "added": added}) + w += added + slack = sum(inversions(g) for g, _, _ in word)-endpoint_rank + bound = slack // min(inversions(g) for g, _, _ in word) + require(w-original_w <= bound, "global inversion-slack bound") + for (g, u, v), (h, x, y) in zip(word, work): + require(g == h and not any(x[w:]) and not any(y[w:]), "discarded factor support") + require(matvec(basis, x, q) == u, "column intertwiner") + require(matvec(list(zip(*basis)), v, q) == y, "row intertwiner") + reduced = [(g, u[:w], v[:w]) for g, u, v in work] + small = formal_product(reduced, n, w, q) + full = formal_product(work, n, r, q) + require(small == {g: [row[:w] for row in a[:w]] for g, a in full.items()}, "reduced endpoint") + return {"retained": w, "bound_dirty": bound, "endpoint_rank": endpoint_rank, + "charges": charges, "basis": basis} + + +def nested_controls(): + records = [] + for q in (2, 3): + e = (1, 0, 0, 0, 0, 0) + u, v = (1, 1, 1, 0, 0, 0), (1, 0, 0, 1, 1, 0) + x, y = (1, 0, 1, 1, 0, 0), (1, 1, 0, 0, 1, 0) + a, b, c = (3, 2, 1, 0), (1, 2, 0, 3), (2, 1, 0, 3) + word = [(a, e, e), (b, u, v), (c, x, y), + (inverse_perm(c), x, y), (inverse_perm(b), u, v)] + spectator_basis = eye(6) + spectator_basis[2][1] = spectator_basis[3][2] = spectator_basis[4][3] = 1 + spectator_basis[5][4] = 1 + mixed = transform(word, spectator_basis, q) + record = compress(mixed, 4, 1, q) + record["q"] = q + records.append(record) + return records + + +def word_controls(): + records = [] + for n, q, g in [(3, 2, (1, 2, 0)), (3, 3, (2, 1, 0)), + (4, 2, (3, 2, 1, 0)), (4, 3, (1, 3, 0, 2))]: + r, axis = 5, (1, 0, 0, 0, 0) + u, v = (1, 1, 0, 0, 0), (1, 0, 1, 0, 0) + word = [(g, axis, axis), (g, u, v), (inverse_perm(g), u, v)] + formal = formal_product(word, n, r, q) + target = {tuple(range(n)): [[int(i == j and i > 0) for j in range(r)] for i in range(r)], + g: [[int(i == j == 0) for j in range(r)] for i in range(r)]} + require(formal == target, "full formal dirty endpoint") + represented, basis = eye(r*n*(n-1)), list(permutations(range(n))) + regular = eye(r * len(basis)) + for label, x, y in word: + represented = mul(represented, gate(label, x, y, q), q) + regular = mul(regular, gate(label, x, y, q, True), q) + length = inversions(g) + require(crossing(represented, n, r, q) == length, "endpoint crossing rank") + small = formal_product([(h, x[:3], y[:3]) for h, x, y in word], n, 3, q) + require(small == {h: [row[:3] for row in a[:3]] for h, a in target.items()}, + "restricted full endpoint") + for j in range(len(regular)): + role, addr = divmod(j, len(basis)) + address = basis.index(compose(g, basis[addr])) if role == 0 else addr + expected = role * len(basis) + address + require(all(regular[i][j] == int(i == expected) for i in range(len(regular))), + "literal regular-action dirty basis column") + records.append({"n": n, "q": q, "label": list(g), "d": length, + "weighted_slack": 2*length, "bound_dirty": 2, + "required_dirty": 2, "regular_basis_columns": len(regular), + "formal_sha256": sha256(json.dumps(sorted(formal.items())).encode()).hexdigest()}) + return records + + +def negative_controls(): + count = 0 + for g, u, v, q in [((0, 0, 2), (1,), (1,), 2), + ((1, 0), (1, 0), (0, 1), 2), ((1, 0), (1,), (1,), 4)]: + try: + gate(g, u, v, q) + except ValueError: + count += 1 + else: + raise ValueError("illegal gate accepted") + g, u, v = (1, 2, 0), (1, 1, 0), (1, 0, 1) + require(formal_product([(g, u, v)], 3, 3, 2) != + formal_product([(g, (1, 0, 0), (1, 0, 0))], 3, 3, 2), "dirty leak control") + require(formal_product([(g, u, v), (g, u, v)], 3, 3, 2) != + {tuple(range(3)): eye(3)}, "forward-for-inverse control") + require(inversions((2, 1, 0)) == 3 and inversions(g) == 2, "unit undercharge") + require(all(a*b % q != 0 for q in (2, 3, 5) for a in range(1, q) + for b in range(1, q)), "sharpness pairing") + return count + 4 + + +def compute(): + return {"claim_type": "scoped proof with finite corroboration", "local": local_controls(), + "decompositions": subspace_controls(), "words": word_controls(), + "nested_compressions": nested_controls(), + "negative_controls": negative_controls()} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + mode = parser.add_mutually_exclusive_group() + mode.add_argument("--emit", type=Path) + mode.add_argument("--receipt", type=Path) + args = parser.parse_args() + hashes = {p.name: sha256(p.read_bytes()).hexdigest() for p in sorted(HERE.iterdir()) + if p.is_file()} + result = {"sources": hashes, "result": compute()} + if args.emit: + with args.emit.open("x", encoding="utf-8") as handle: + handle.write(json.dumps(result, indent=2, sort_keys=True) + "\n") + elif args.receipt: + require(result == json.loads(args.receipt.read_text()), "receipt differs") + print("PASS_PERMUTATION_SLACK_WORKSPACE", result["result"]["local"]["peels"], + "peels;", result["result"]["decompositions"], "decompositions;", + len(result["result"]["words"]), "formal words") + + +if __name__ == "__main__": + main()