diff --git a/research/mixed-gl2-block-tariff/README.md b/research/mixed-gl2-block-tariff/README.md new file mode 100644 index 0000000000..0e70d9afe3 --- /dev/null +++ b/research/mixed-gl2-block-tariff/README.md @@ -0,0 +1,185 @@ +# Exact mixed GL2-block tariffs in larger address spaces + +**Scoped formal-model theorem; no new kappa.** Fix disjoint pairs of address +coordinates. A diagonal register target can use any of the six `GL_2(F2)` +operators on each pair, with different choices on different registers. +Its exact cost is the sum of the block tariffs + +```text +label: e a b ab ba s=aba +cost: 0 1 1 2 2 3. +``` + +This remains true in every ambient `GL_n(F2)` that contains the pairs, even +when the circuit uses arbitrary coordinate CNOTs between pairs or with +address spectators. Free scalar register mixing and any finite number of +restored dirty registers are allowed. + +The dimension-two mixed tariff is already a corollary of Ross Richardson's +[PR #1989](https://github.com/CrocSwap/integer-mult-bounds/pull/1989), through +the `GL_2(F2)=S_3` bridge in +[PR #2415](https://github.com/CrocSwap/integer-mult-bounds/pull/2415). +This contribution extends the averaged row-order method of +[PR #4950](https://github.com/CrocSwap/integer-mult-bounds/pull/4950) from +identical swaps to all six block labels and sums over disjoint pairs. +It does not claim a new dimension-two lower bound. The selected kappa remains +`60403/20000000`; no physical supplier is supplied. + +## Model and theorem + +Let `n>=2` and let `B_j=(p_j,q_j)` be fixed pairs with disjoint coordinate +sets in `{0,...,n-1}`. For each target register `r` and block `j`, select +`g_(r,j)` from `GL_2(F2)`. Its embedding acts on the two coordinates of `B_j` +and fixes all other coordinates. The register target `g_r` is the product +of these embeddings. They commute because the pairs are disjoint. +Other register targets and all unused address coordinates are identity. + +Work in the formal group algebra `M_R(F2[GL_n(F2)])`. Every register input +is arbitrary. The endpoint is `diag([g_1],...,[g_t],1,...,1)`, with every +extra register restored and no off-diagonal residue. Paid units are + +```text +I_R + ([c]+1)N, +``` + +where `c` is any coordinate CNOT in the ambient address space, and `N` is +any binary scalar rank-one idempotent. Each unit costs one. Free scalar +`GL_R(F2)` maps may occur anywhere. There are no other free address maps, +clean allocations or uncharged restoration calls. + +**Theorem.** For every finite `R>=t`, the exact paid-call minimum is +`sum_(r,j) ell(g_(r,j))`, with `ell` given by the table above. +The empty target uses the empty word. The statement covers arbitrary +intermediate scalar projectors and cross-pair address calls; only the +required final target has the block form. + +## Proof + +Use the left regular representation of `G=GL_n(F2)`. For each total order +`<` on the nonzero binary vectors and pair `(p,q)`, let + +```text +A_(p,q) = {x in G : row_p(x) < row_q(x)}. +``` + +On all `R` registers, take the crossing rank from this address cut to its +complement. Block multiplication gives `q(MN)<=q(M)+q(N)`. A free scalar +map has crossing rank zero. A paid call has crossing block +`P_c[A^c,A] tensor N`, so its crossing rank is `out_A(c)`, since `rank(N)=1`. +A diagonal target has the sum of its register crossing ranks. These facts +hold in the formal algebra and do not assume commuting projectors. + +Average each cut over all total orders. Write `u=|G|/6`. +A CNOT writing neither coordinate of a pair changes neither selected row, +so its charge in that cut is zero. If it writes the first row, denote the +old rows by `x,y` and the new row by `z`. The three vectors are distinct: +rows of an invertible matrix are independent, and a sum of two rows is +neither zero nor any original row. The event that the cut is left is +`x0`, this proves +the lower bound for arbitrary dirty workspace and ambient dimension. + +For the upper bound, use the direct two-generator word for each block on +its own register with coordinate projector `E_rr`. Its length is `ell(g)`. +The factors remain diagonal formal monomials, so the group identity is +also a coefficientwise identity in the full formal algebra. Concatenate +the words for all blocks and registers. This attains the lower bound and +restores every unused register and coordinate. No unpaid cleanup is needed. + +## Consequences and boundary + +The heterogeneous target `diag([a],[b],[aba])` costs exactly five for all +`n>=2` and any `R>=3`. The fixed-three-register search in +[the retained heterogeneous-target note](../bit-mixed-transposition-triple/README.md) +already found five at `n=2`. Its extra-register question is covered there by +the inherited dimension-two cut theorem; the ambient-address extension here +also rules out using other address coordinates to reduce that cost. + +The coordinate pairs must be disjoint. On one register, the product of the +three swaps on `(01),(12),(02)` equals the swap on `(12)`. Its separate +nine-call implementation can therefore be replaced by three calls. The +verifier checks this literal counterexample and rejects overlapping pairs +as input to the additive tariff. This is a one-register product; it is not +the three-register mixed-swap target of the component-cut theorem. + +The theorem also retains the rank-one tariff, arbitrary-input endpoint and +absence of free address transformations. It does not cover unequal or +projector-dependent prices, a rank-two call charged as one, a restricted +clean-input endpoint, or arbitrary overlapping block products. + +## Evidence and reproduction + +Use CPython 3.12 and the standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/mixed-gl2-block-tariff +python3.12 -I -W error -O -B research/mixed-gl2-block-tariff/verify.py +``` + +Expected markers: `PASS_REGISTERED_RESEARCH_PACKAGE` and +`PASS_MIXED_GL2_BLOCK_TARIFF costs=0,1,1,2,2,3 no_new_kappa`. +Normal replay recomputes [RESULT.json](RESULT.json), writes no files and +needs no Git or network. `--emit-receipt` emits JSON for explicit regeneration. +The receipt binds all five source files by SHA-256. + +The checker compares the six crossing counts with independently computed +`GL2` word lengths. It checks 80 actual coordinate-CNOT/basis cases over +31,992 relative orders, including cross-pair reads and spectator writes. +It exhausts all three-register single-block label triples and all two-register +two-block label quadruples in the declared finite dimension/register grids: +7,128 complete diagonal formal endpoints and 39,852 single-call omissions. +Nine controls cover invalid contracts, empty targets, the five-call example +and the overlapping-block counterexample. + +These particular upper words remain diagonal monomials. Their group labels +are therefore sufficient to verify their full formal endpoints. This does +not assert that natural matrices certify arbitrary group-algebra programs. +The lower bound for all programs is the written regular-representation proof. +No predecessor executable is imported. + +## Open next questions + +What is possible for overlapping target blocks? First specify the actual +one-register product or multi-register endpoint; the example above shows +that a list of local block prices need not add. No general cost law for +that changed boundary is supplied here. Native realization, full supplier +accounting and proof-kernel review remain separate obligations. + +## Credit and source pins + +Prepared for Ali Romman with substantial OpenAI Codex assistance. New work +is Apache-2.0. Ross Richardson supplied the general inversion-sum theorem +and the GL2 bridge; James Reed supplied the averaged spectator cut; Cinna +Davis supplied the fixed-register heterogeneous question. Their retained +notes credit Mihir Srivastava, commdata2338, Gareth Davidson and earlier +register-model/cut contributors. All notices remain unchanged. +The four source documents are provenance only, pinned in +[SOURCES.json](SOURCES.json). Base: +`f259dabc7d70e0db8d6d36bfda888f008bbfecc1`, priority revision 7. +No independent human review, native/compiler admission, selected cold replay, +full multiplier theorem or kappa improvement is claimed. diff --git a/research/mixed-gl2-block-tariff/RESULT.json b/research/mixed-gl2-block-tariff/RESULT.json new file mode 100644 index 0000000000..8189c78d84 --- /dev/null +++ b/research/mixed-gl2-block-tariff/RESULT.json @@ -0,0 +1,77 @@ +{ + "ambient_paid": { + "cases": 80, + "relative_orders": 31992 + }, + "boundary_controls": 9, + "formal_diagonal_words": { + "endpoints": 7128, + "omissions": 39852, + "paid_calls": 39852 + }, + "no_new_kappa": true, + "schema": "mixed-gl2-block-tariff/v1", + "source_sha256": { + "README.md": "c261a4d289c61e31dc495303f22d994b506c87b2f03de308ed94435bd7a1a4e0", + "SOURCES.json": "0bf3f591df2bd72806d5087a421a7fdd4c248ae9bd356dbc92b8569da750fb32", + "TASK.json": "aea608cafc4e5ec31d8af1fa52c6615125cf909ae26e0d6e222378b00e777b4b", + "VERIFY.json": "491b483ee1214d957f4ded739810898d6e4978ff031337538ca2c966c880763b", + "verify.py": "b99269d958510a9f9cfde49a28b239d3e56d21ddba8a7e39a37b590cb44b1775" + }, + "tariffs": { + "a": { + "cost": 1, + "leaving_orders": 1, + "orders": 6, + "rows": [ + 3, + 2 + ] + }, + "ab": { + "cost": 2, + "leaving_orders": 2, + "orders": 6, + "rows": [ + 2, + 3 + ] + }, + "b": { + "cost": 1, + "leaving_orders": 1, + "orders": 6, + "rows": [ + 1, + 3 + ] + }, + "ba": { + "cost": 2, + "leaving_orders": 2, + "orders": 6, + "rows": [ + 3, + 1 + ] + }, + "e": { + "cost": 0, + "leaving_orders": 0, + "orders": 6, + "rows": [ + 1, + 2 + ] + }, + "s": { + "cost": 3, + "leaving_orders": 3, + "orders": 6, + "rows": [ + 2, + 1 + ] + } + } +} diff --git a/research/mixed-gl2-block-tariff/SOURCES.json b/research/mixed-gl2-block-tariff/SOURCES.json new file mode 100644 index 0000000000..e7aa7edb99 --- /dev/null +++ b/research/mixed-gl2-block-tariff/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1", + "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/bit-mixed-transposition-triple/README.md", + "usage": "provenance", + "git_blob": "44c449f37495b75cfda01a3293eca1e7e29633e9", + "sha256": "d394690ebf1905f3940e3a17662e1169bed68fe02304e2ed863f79c4ad093d5f" + }, + { + "path": "research/gl2-swap-cut-corollary/README.md", + "usage": "provenance", + "git_blob": "c34c1460063ee4690c934d3c3fb3d81896f8931c", + "sha256": "3650918994be00323ccb61b75cdd81ecae47104a6e0765e319196618737949d9" + }, + { + "path": "research/swap-row-order-cut/README.md", + "usage": "provenance", + "git_blob": "941c1eb4f2301023757c45bbe1bb767962065cd1", + "sha256": "a5e9661f5ffa504cafee1c9481f0a1072b98341f98a031a2b4d18bb8c4a9ef7c" + }, + { + "path": "research/symmetric-adjacent-cut-bound/PROOF.md", + "usage": "provenance", + "git_blob": "30dad3856246c9cef3b8014ee967dd545f3a092d", + "sha256": "008be68867a8e85f4e18455d206e03f20aebfc28e9f08efba576180e7e1edc50" + } + ] +} diff --git a/research/mixed-gl2-block-tariff/TASK.json b/research/mixed-gl2-block-tariff/TASK.json new file mode 100644 index 0000000000..107f605cba --- /dev/null +++ b/research/mixed-gl2-block-tariff/TASK.json @@ -0,0 +1,87 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "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" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "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.", + "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." + }, + "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.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "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." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the exact mixed GL2-block sum tariff for arbitrary ambient coordinate CNOTs, free scalar mixing and restored dirty registers.", + "scope_change_reason": "The dimension-two mixed tariff follows from PR1989. Extend PR4950 averaged row-order cuts to all six block operators and sums over disjoint coordinate pairs; do not repeat an old fixed-register search.", + "bottleneck_link": "Arbitrary address spectators and cross-pair reads/writes cannot reduce this complete formal paid-call bill. Native costs and supplier admission remain separate.", + "budget_minutes": 60, + "stop_rule": "Stop at the uniform tariff proof, bounded exact checks and changed-premise control. No general formal-word census or native search.", + "outcome": "completed", + "evidence": "Six exact crossing tariffs and independent group word lengths; actual coordinate-CNOT order counts; exhaustive bounded diagonal upper words, call omissions and an overlapping-block counterexample.", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance for proof, implementation, verification and publication. No independent human or proof-kernel review.", + "open_questions": [ + { + "question": "What cost is possible for target blocks whose coordinate sets overlap?", + "why_it_matters": "The disjoint-write accounting no longer applies, and an explicit one-register product can cancel from nine to three calls.", + "first_step": "Specify one overlapping target product and compare its actual endpoint with the formal cut charges.", + "blocked_by": "No general additive law is claimed for overlapping blocks." + } + ], + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-19139741", + "selection": { + "mode": "handoff-first", + "source_pr": 4950, + "source_head": "78dc9c12f46967df0d85594875a32a62b5639670", + "related_question": "research/bit-mixed-transposition-triple/README.md" + }, + "overlap": { + "searched_at": "2026-10-23T06:47:45.225966+00:00", + "open_prs": { + "fetched_at": "2026-10-23T06:46:43.014855+00:00", + "complete_pagination": true, + "records": 318 + }, + "discussions": { + "fetched_at": "2026-10-23T06:47:45.121400+00:00", + "complete_pagination": true, + "records": 4130 + }, + "local_notes": 83, + "total_local_notes": 6710, + "limits": "Sparse omitted notes, arbitrary diffs and unpublished work. Related local proofs were read directly." + } +} diff --git a/research/mixed-gl2-block-tariff/VERIFY.json b/research/mixed-gl2-block-tariff/VERIFY.json new file mode 100644 index 0000000000..cb5df1af86 --- /dev/null +++ b/research/mixed-gl2-block-tariff/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": 30, + "checks": "Exact crossing tariffs, ambient-coordinate paid counts, formal diagonal words and boundaries." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "The same checks with Python assertions disabled." + } + ] +} diff --git a/research/mixed-gl2-block-tariff/verify.py b/research/mixed-gl2-block-tariff/verify.py new file mode 100644 index 0000000000..f9ab2261d7 --- /dev/null +++ b/research/mixed-gl2-block-tariff/verify.py @@ -0,0 +1,191 @@ +#!/usr/bin/env python3 +"""Check the mixed GL2-block tariff. Ali Romman with Codex assistance. + +Apache-2.0. Formal diagonal words stay single group basis elements. +""" +from collections import deque +from itertools import permutations, product +from pathlib import Path +import hashlib +import json +import math +import sys + +ELEMENTS = {'e': (1,2), 'a': (3,2), 'b': (1,3), + 'ab': (2,3), 'ba': (3,1), 's': (2,1)} +WORDS = {'e': (), 'a': ((0,1),), 'b': ((1,0),), + 'ab': ((1,0),(0,1)), 'ba': ((0,1),(1,0)), + 's': ((0,1),(1,0),(0,1))} +COSTS = {'e':0, 'a':1, 'b':1, 'ab':2, 'ba':2, 's':3} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def tariffs(): + distance = {(1,2):0} + queue = deque([(1,2)]) + while queue: + state = queue.popleft() + for i,j in ((0,1),(1,0)): + nxt = list(state) + nxt[i] ^= nxt[j] + nxt = tuple(nxt) + if nxt not in distance: + distance[nxt] = distance[state]+1 + queue.append(nxt) + require(set(distance) == set(ELEMENTS.values()), 'GL2 inventory differs') + rows = {} + for name, matrix in ELEMENTS.items(): + leave = 0 + for order in permutations((1,2,3)): + positions = {q:i for i,q in enumerate(order)} + leave += positions[1] < positions[2] and positions[matrix[0]] > positions[matrix[1]] + require(leave == COSTS[name] == distance[matrix] == len(WORDS[name]), 'tariff differs') + rows[name] = {'rows':matrix, 'leaving_orders':leave, 'orders':6, 'cost':COSTS[name]} + return rows + + +def validate(labels, pairs, n, registers): + require(type(n) is int and n >= 2 and type(registers) is int and registers >= max(1,len(labels)), + 'invalid dimension or register count') + require(all(len(pair)==2 and all(type(i) is int and 0<=i position[after[b]]) + orders_checked += 1 + unit = math.factorial(n+1)//6 + expected = [unit if write in pair else 0 for pair in pairs] + require(counts == expected and sum(counts) <= unit, 'ambient paid capacity differs') + cases += 1 + return {'cases':cases, 'relative_orders':orders_checked} + + +def upper_words(): + cases = omissions = total_calls = 0 + + def check(labels,pairs,n,registers): + nonlocal cases,omissions,total_calls + price = bill(labels,pairs,n,registers) + word = program(labels,pairs) + wanted = target(labels,pairs,n,registers) + require(len(word) == price and execute(word,n,registers) == wanted, 'formal endpoint differs') + for omit in range(len(word)): + require(execute(word,n,registers,omit) != wanted, 'omitted call accepted') + omissions += 1 + cases += 1 + total_calls += len(word) + + for values in product(ELEMENTS,repeat=3): + labels = [[v] for v in values] + for n in (2,3,5): + for registers in (3,4,5): + check(labels,[(0,n-1)],n,registers) + for values in product(ELEMENTS,repeat=4): + labels = [list(values[:2]),list(values[2:])] + for n,pairs in ((4,[(0,1),(2,3)]),(5,[(0,3),(1,4)])): + for registers in (2,3): + check(labels,pairs,n,registers) + require((cases,omissions,total_calls)==(7128,39852,39852), 'word coverage differs') + return {'endpoints':cases, 'omissions':omissions, 'paid_calls':total_calls} + + +def controls(): + invalid = [([['s','s']],[(0,1),(1,2)],3,1), ([['s']],[(0,0)],2,1), + ([['s']],[(0,2)],2,1), ([['s'],['a']],[(0,1)],2,1), + ([['unknown']],[(0,1)],2,1), ([[]],[(0,1)],2,1)] + for args in invalid: + try: + bill(*args) + except ValueError: + continue + raise ValueError('invalid contract accepted') + require(bill([],[(0,1)],2,1)==0, 'empty target bill') + require(bill([['a'],['b'],['s']],[(0,1)],5,5)==5, 'heterogeneous target bill') + # Three different overlapping pairs on one register can cancel. + long = [(0,i,j) for a,b in ((0,1),(1,2),(0,2)) + for i,j in ((a,b),(b,a),(a,b))] + short = [(0,1,2),(0,2,1),(0,1,2)] + require(len(long)==9 and len(short)==3 and execute(long,3,1)==execute(short,3,1), + 'overlapping-block boundary differs') + return len(invalid)+3 + + +def evidence(): + here = Path(__file__).resolve().parent + result = {'schema':'mixed-gl2-block-tariff/v1', 'tariffs':tariffs(), + 'ambient_paid':ambient_paid_checks(), 'formal_diagonal_words':upper_words(), + 'boundary_controls':controls(), 'no_new_kappa':True} + result['source_sha256'] = {name:hashlib.sha256((here/name).read_bytes()).hexdigest() + for name in ('README.md','verify.py','TASK.json','VERIFY.json','SOURCES.json')} + return result + + +def main(): + encoded = json.dumps(evidence(),sort_keys=True,indent=2)+'\n' + if sys.argv[1:] == ['--emit-receipt']: + print(encoded,end='') + else: + require(not sys.argv[1:], 'unexpected argument') + require(Path(__file__).with_name('RESULT.json').read_text(encoding='utf-8')==encoded, 'receipt differs') + print('PASS_MIXED_GL2_BLOCK_TARIFF costs=0,1,1,2,2,3 no_new_kappa') + + +if __name__=='__main__': + main()