diff --git a/research/projector-price-orbit-collapse/README.md b/research/projector-price-orbit-collapse/README.md new file mode 100644 index 0000000000..0848f5f16f --- /dev/null +++ b/research/projector-price-orbit-collapse/README.md @@ -0,0 +1,172 @@ +# Support-dependent projector prices collapse under free scalar mixing + +This contribution is produced by Nick Petalas. Apache-2.0. + +## Result and scope + +**Scoped proof, with finite executable corroboration.** This closes the literal +free-mixing version of Open next question 2 in ywz65's +[PR #2544](https://github.com/CrocSwap/integer-mult-bounds/pull/2544). +Allow the price of each paid label to depend arbitrarily on its displayed +rank-one projector. If every scalar change of basis is free between calls, +only the cheapest price for each label affects the exact optimum. + +For `R >= t >= 0` binary roles, write `c_a(N), c_b(N) >= 0` for these prices, +where N runs over every rank-one idempotent of `M_R(F2)`. For `R >= 1`, set + +```text +A = min_N c_a(N), B = min_N c_b(N). +minimum price of t coordinate SWAP targets = t (A + B + min(A,B)). +``` + +Every spectator starts arbitrarily and is restored individually. The minimum +for `R=t=0` is zero, without defining an empty projector minimum. Prices may +depend on R; take the two minima separately at that R. The fixed-price SWAP +theorem and its lower bound are inherited from #2544. The new step is the +exact compilation that eliminates dependence on projector support. + +This formal price result gives no native implementation, recursive invoice, +supplier admission, new kappa or complete multiplication theorem. Free changes +of basis are a hypothesis, not an assertion about physical costs. + +## Model + +Use precisely #2544's address group `G=GL_2(F2)` and paid labels + +```text +a = [[1,1],[0,1]], b = [[1,0],[1,1]], z = aba = bab. +D_N(g) = I_R + ([g]+[e]) N in M_R(F2[G]). +``` + +The endpoint is `diag([z] I_t, I_(R-t))`, coefficientwise in the full group +algebra. Scalar `GL_R(F2)` matrices may be interleaved for free and must be +included in that endpoint equality. The price `c_g(N)` is attached to the +projector displayed at the paid instruction. It is independent of the data, +earlier instructions, current gauge and eventual output. There are no free +address maps, erasures, clean allocations or state-dependent rebates. + +## Proof of price collapse + +The following compilation lemma applies more generally. Let H be any group of +free invertible scalar maps acting by conjugation on an allowed projector set +that is closed under H, with every orbit finite. For each projector orbit O +and paid label g, replace its prices by `m_g(O)=min_{P in O} c_g(P)`. +For every exact endpoint, the infimum over finite words is unchanged. + +For one direction, keep every word and reduce each of its paid prices to its +orbit minimum. Its new price cannot increase. For the reverse direction, take +any word at orbit-minimum prices. For each occurrence of `D_N(g)`, choose a +cheapest P in N's orbit and C in H with `N=C P C^(-1)`. Scalar entries commute +with address coefficients, so full coefficient equality gives + +```text +D_N(g) = C D_P(g) C^(-1). +``` + +Replace that occurrence by the three displayed factors. The two scalar maps +are free and the paid factor has price exactly `m_g(O)`. This preserves each +factor as a complete operator. Thus it preserves the entire endpoint, all dirty +inputs and every spectator, at exactly the orbit-minimum price. The two +inequalities give equality of infima. If one problem attains its infimum, the +same construction proves attainment for the other. This argument does not +assume that projectors in different calls commute, nor that gauges can be +discarded after normalization. + +For full `H=GL_R(F2)`, all rank-one idempotents lie in one orbit. This is standard +linear algebra: write `P=u v^T` with `v^T u=1`, and take a basis whose first +vector is u and remaining vectors form a basis of `ker(v^T)`. In that basis P +is `E_11`. Given bases `B_P,B_N` of this form, `C=B_N B_P^(-1)` maps P to N. +The verifier constructs these bases and checks the full formal replacement. + +Consequently the exact target cost equals the fixed-label-price optimum at +A and B. The cited #2544 theorem gives `t(A+B+min(A,B))`. Its coordinate `aba` +or `bab` attaining words can be compiled one factor at a time through cheapest +projectors. This proves the displayed all-role formula. No predecessor census +or proof is independently reverified here. + +## Why the free-mixing hypothesis matters + +Consider two roles and `P=[[1,0],[1,0]]`, with both labels free only at P and +priced one at every other projector. Let `N=E_11`. With free mixing, the target +`D_N(z)` has price zero by the compiler. If no scalar mixing is allowed, every +zero-price word belongs to the six-element subgroup `{D_P(g):g in G}`. Indeed +`D_P(g)D_P(h)=D_P(gh)` because `P^2=P`. This subgroup omits `D_N(z)` since its +nonidentity group coefficient is P rather than N. The verifier enumerates all +six states and checks closure and the omitted target. This does not claim the +exact positive optimum in the restricted-gauge model. + +Support tariffs can therefore matter with charged or restricted scalar maps. +Searching additional projector supports with unrestricted free scalar mixing +cannot change the optimum beyond the two minima above. + +## Reproduction and evidence + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/projector-price-orbit-collapse/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/projector-price-orbit-collapse +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/projector-price-orbit-collapse --check-source-history +``` + +The direct script checks every ordered projector pair at R=1,2,3 for each paid +label, and additional constructed pairs at R=4 through 8. It constructs full +group-algebra attaining endpoints for every t=0 through R at R=1,2,3 under four +price tables, including zero and nonconstant tariffs. It also checks the +restricted-gauge example and detects a missing inverse gauge. The printed +receipt is generated from those checks and binds its code, proof and source +manifest by SHA256. Default replay writes no files. The universal conclusion +rests on the written compilation proof and the cited fixed-price theorem, +rather than extrapolation from the finite checks. + +No Lean, Docker, predecessor replay or selected cold replay is required or run. +Independent human and formal proof-kernel review are unclaimed. + +## Sources and overlap + +The base is canonical main `624de9dc66858af0945e5f8a0942488d62280d43`, priority +revision 7. [SOURCES.json](SOURCES.json) pins the inherited #2544 theorem at its +retained main bytes. Credit ywz65 for the asymmetric SWAP tariff and explicit +support-price question; Ross Richardson #1989/#2415 for its inherited total-call +cut theorem; Aaron Wang's asymmetric-price handoff and their credited +register-model predecessors. Projector conjugacy itself is classical. + +The original `bit-new-register-model` card changes to a formal pricing side +question. This closes a stated loophole in the nonabelian model; it does not +provide a changed productive mechanism. Before claiming, live title/body and +Discussion searches, distinctive main README searches and merged PR searches +found no same-question result within their coverage. The overlap cache held +348 open PRs and 3,782 Discussion records. Sparse local notes, arbitrary code +diffs and unpublished work were not fully searched. The local question lock +was reserved before the public claim. These searches are not a novelty proof. +The pre-submission refresh at 21:17 UTC covered 352 open PRs and 3,793 Discussion +records, with complete remote pagination. Canonical main and the scoped source +remained unchanged. The refreshed terms matched this package, its own claim +and the explicit #2544 predecessor; broader group-algebra work is related +rather than checked. + +## Engineering bounds + +The verifier uses fixed dimensions at most eight, finite group size six and +bounded loops. The largest exhaustive projector-pair domain is 28 squared. +Functions fit within 60 lines, have direct call paths and use explicit checks +that remain active under optimized Python. It authenticates the sole inherited +input before computing. Managed Python allocation is a deviation from Power +of Ten rule 3: tuples, integer objects and convolution temporaries allocate at +runtime. Their dimensions and enumeration bounds are fixed above; no input can +expand them. Follow-up for a larger census would require an explicit capacity +limit before extending these constants. No compiler or static type checker is +required by this standard-library repository hook; direct development-mode +replay with warnings as errors provides its interpreted-code diagnostic check. + +## Open next questions + +1. Charge scalar mixing by an explicit native ADD or routing price. Does a + nonconstant support tariff then beat the best coordinate protocol after both + gauges are charged? First solve the two-role P/N example above with its + actual gauge costs. A physical gauge price and complete endpoint contract + are missing; the free-mixing theorem supplies neither. +2. Restrict free maps to a named subgroup H, such as coordinate permutations. + Which projector orbits determine the exact SWAP cost? First classify the + two-role orbits and solve one nonconstant orbit-price instance. The lemma + reduces each orbit internally but leaves interactions between orbits open. diff --git a/research/projector-price-orbit-collapse/SOURCES.json b/research/projector-price-orbit-collapse/SOURCES.json new file mode 100644 index 0000000000..438e5d8462 --- /dev/null +++ b/research/projector-price-orbit-collapse/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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/gl2-swap-weighted-tariff/README.md", + "usage": "input", + "git_blob": "e4647abcd7056dd205252f8d1e4d20368df66c9d", + "sha256": "bd9e1a3346adbb8b99a30eaa2819006760adff5258f629b2ffc628cc397e93c4" + } + ] +} diff --git a/research/projector-price-orbit-collapse/TASK.json b/research/projector-price-orbit-collapse/TASK.json new file mode 100644 index 0000000000..6307a7806a --- /dev/null +++ b/research/projector-price-orbit-collapse/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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 orbit-minimum compilation for displayed-projector prices under free scalar mixing; derive the exact support-dependent coordinate-SWAP tariff from PR2544.", + "scope_change_reason": "The chosen nonabelian-model card is changed to the explicit support-price open question in ywz65 PR2544. The fixed-label-price theorem is cited, not audited.", + "bottleneck_link": "Formal pricing side result: unrestricted free scalar gauges erase any support-price advantage beyond orbit minima. A productive native mechanism still needs paid gauge and hosting costs.", + "budget_minutes": 60, + "stop_rule": "Stop after the first exact price-collapse result and its bounded compiler controls; do not extend to charged or restricted gauges.", + "outcome": "completed", + "evidence": "Written compilation proof in README.md; direct verifier passes 1702 full-formal conjugation checks, 36 tariff endpoints and two boundary controls. The receipt is generated and bound to proof/code/source hashes.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact optimum when scalar mixing has a specified native price?", + "why_it_matters": "Free gauge compilation can conceal the full physical cost of changing supports.", + "first_step": "Price both gauges in the two-role P/N example and solve the complete exact endpoint.", + "blocked_by": "A native scalar-gauge price and endpoint contract are not supplied." + }, + { + "question": "What is sharp when only a proper subgroup of scalar maps is free?", + "why_it_matters": "Different projector orbits can retain different prices.", + "first_step": "Classify two-role coordinate-permutation orbits and solve one nonconstant orbit-price example.", + "blocked_by": "The orbit-collapse lemma does not solve interactions between distinct orbits." + } + ], + "claim_type": "scoped proof", + "predecessor": { + "pr": 2544, + "head": "9fb1552f12ca4777ca660461a8b602e709285f99", + "author": "ywz65", + "scope": "Inherit exact fixed-price SWAP theorem and support-price open question; do not independently audit predecessor." + }, + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132782", + "overlap_limitations": "348 cached open PRs and 3782 Discussion records; incomplete sparse local notes and no arbitrary code-diff or unpublished-work coverage.", + "submission_refresh": { + "canonical_main": "624de9dc66858af0945e5f8a0942488d62280d43", + "utc": "2026-10-22T21:17:37Z", + "open_prs": 352, + "discussion_records": 3793, + "remote_pagination_complete": true, + "limitations": "Sparse local notes and arbitrary diffs/unpublished work are incomplete." + } + } +} diff --git a/research/projector-price-orbit-collapse/VERIFY.json b/research/projector-price-orbit-collapse/VERIFY.json new file mode 100644 index 0000000000..9f64b38db0 --- /dev/null +++ b/research/projector-price-orbit-collapse/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/gl2-swap-weighted-tariff/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-X", + "dev", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "New conjugation compiler on all ordered rank-one projector pairs R<=3 and constructed pairs R<=8; full-formal price attainments; restricted-gauge and omitted-inverse controls; source hash." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the new compiler and its explicit rejection controls with assertions disabled." + } + ] +} diff --git a/research/projector-price-orbit-collapse/verify.py b/research/projector-price-orbit-collapse/verify.py new file mode 100644 index 0000000000..6e726ed31a --- /dev/null +++ b/research/projector-price-orbit-collapse/verify.py @@ -0,0 +1,224 @@ +#!/usr/bin/env python3 +"""Check the new conjugation compiler, not the inherited fixed-price theorem.""" + +import hashlib +import itertools +import json +from pathlib import Path + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def identity(r): + return tuple(1 << i for i in range(r)) + + +def add(a, b): + return tuple(x ^ y for x, y in zip(a, b, strict=True)) + + +def multiply(a, b): + return tuple(xor_rows(row, b) for row in a) + + +def xor_rows(mask, rows): + result = 0 + for i, row in enumerate(rows): + if mask >> i & 1: + result ^= row + return result + + +def inverse(a): + r = len(a) + rows = [a[i] | (1 << (r + i)) for i in range(r)] + for j in range(r): + pivots = [i for i in range(j, r) if rows[i] >> j & 1] + need(bool(pivots), "singular conjugator") + k = pivots[0] + rows[j], rows[k] = rows[k], rows[j] + for i in range(r): + if i != j and rows[i] >> j & 1: + rows[i] ^= rows[j] + result = tuple(row >> r for row in rows) + need(multiply(a, result) == identity(r), "inverse identity") + return result + + +def outer(u, v, r): + return tuple(v if u >> i & 1 else 0 for i in range(r)) + + +def projectors(r): + return tuple(outer(u, v, r) + for u in range(1, 1 << r) + for v in range(1, 1 << r) + if (u & v).bit_count() % 2) + + +def adapted_basis(p): + """Columns are an image generator followed by a basis of the kernel.""" + r = len(p) + columns = [sum(((p[i] >> j) & 1) << i for i in range(r)) + for j in range(r)] + u = next(column for column in columns if column) + j = next(i for i in range(r) if u >> i & 1) + v = p[j] + k = next(i for i in range(r) if v >> i & 1) + need((u & v).bit_count() % 2 == 1, "image/kernel complement") + basis = [u] + [(1 << i) ^ (((v >> i) & 1) << k) + for i in range(r) if i != k] + return tuple(sum(((column >> i) & 1) << j + for j, column in enumerate(basis)) for i in range(r)) + + +def conjugator(p, n): + c = multiply(adapted_basis(n), inverse(adapted_basis(p))) + need(multiply(c, p) == multiply(n, c), "conjugation equation") + return c + + +GROUP = tuple(itertools.permutations(range(3))) +E = GROUP.index((0, 1, 2)) +A = GROUP.index((1, 0, 2)) +B = GROUP.index((0, 2, 1)) +Z = GROUP.index((2, 1, 0)) +TABLE = tuple(tuple(GROUP.index(tuple(g[h[i]] for i in range(3))) + for h in GROUP) for g in GROUP) + + +def scalar(c): + zero = (0,) * len(c) + return tuple(c if g == E else zero for g in range(6)) + + +def paid(g, p): + result = list(scalar(identity(len(p)))) + result[E] = add(result[E], p) + result[g] = add(result[g], p) + return tuple(result) + + +def formal_multiply(x, y): + result = [(0,) * len(x[0]) for _ in range(6)] + for g in range(6): + for h in range(6): + k = TABLE[g][h] + result[k] = add(result[k], multiply(x[g], y[h])) + return tuple(result) + + +def compiled(g, n, cheapest): + c = conjugator(cheapest, n) + ci = inverse(c) + result = formal_multiply(scalar(c), paid(g, cheapest)) + result = formal_multiply(result, scalar(ci)) + need(result == paid(g, n), "full formal conjugation") + return result + + +def check_conjugations(): + pairs = 0 + for r in range(1, 4): + ps = projectors(r) + need(len(ps) == ((1 << r) - 1) * (1 << (r - 1)), + "rank-one projector population") + need(len(set(ps)) == len(ps), "duplicate projector") + for p in ps: + need(multiply(p, p) == p, "projector idempotence") + for n in ps: + for g in (A, B): + compiled(g, n, p) + pairs += 1 + for r in range(4, 9): + p = outer((1 << r) - 1, 1, r) + for i in range(r): + n = outer(1 << i, 1 << i, r) + for g in (A, B): + compiled(g, n, p) + pairs += 1 + return pairs + + +def price_table(ps, case): + """Fixed displayed-projector costs; gauges are separately free.""" + return {g: {p: (0 if case == 0 else 1 + (i + case * g) % 9) + for i, p in enumerate(ps)} for g in (A, B)} + + +def swap_target(r, t): + p = tuple(1 << i if i < t else 0 for i in range(r)) + return paid(Z, p) + + +def check_tariff_compilations(): + endpoints = 0 + for r in range(1, 4): + ps = projectors(r) + for case in range(4): + prices = price_table(ps, case) + cheapest = {g: min(ps, key=prices[g].__getitem__) for g in (A, B)} + minimum = {g: prices[g][cheapest[g]] for g in (A, B)} + first, second = sorted((A, B), key=minimum.__getitem__) + for t in range(r + 1): + result, cost = scalar(identity(r)), 0 + for i in range(t): + n = outer(1 << i, 1 << i, r) + for g in (first, second, first): + result = formal_multiply(result, compiled(g, n, cheapest[g])) + cost += prices[g][cheapest[g]] + need(result == swap_target(r, t), "whole dirty endpoint") + expected = t * (minimum[A] + minimum[B] + min(minimum.values())) + need(cost == expected, "collapsed tariff attainment") + endpoints += 1 + return endpoints + + +def check_boundaries(): + r = 2 + p = outer(3, 1, r) + n = outer(1, 1, r) + target = swap_target(r, 1) + need(p != n, "noncoordinate cheap projector") + result = scalar(identity(r)) + for g in (A, B, A): + result = formal_multiply(result, compiled(g, n, p)) + need(result == target, "zero-price compiled target") + # Without gauges, every zero-price word is in this six-state subgroup. + zero_states = {paid(g, p) for g in range(6)} + for state in zero_states: + for g in (A, B): + need(formal_multiply(state, paid(g, p)) in zero_states, + "zero-price state closure without gauges") + need(target not in zero_states, "restricted-gauge counterexample") + c = conjugator(p, n) + broken = formal_multiply(scalar(c), paid(A, p)) + need(broken != paid(A, n), "missing inverse-gauge rejection") + return {"no_gauge_zero_states": len(zero_states), "controls": 2} + + +def main(): + package = Path(__file__).resolve().parent + root = package.parent.parent + manifest = json.loads((package / "SOURCES.json").read_text()) + pins = [row for row in manifest["files"] if row["usage"] == "input"] + need(len(pins) == 1, "one inherited theorem input") + source = pins[0] + source_bytes = (root / source["path"]).read_bytes() + need(hashlib.sha256(source_bytes).hexdigest() == source["sha256"], + "inherited theorem source hash") + receipt = {"conjugation_checks": check_conjugations(), + "tariff_endpoints": check_tariff_compilations(), + **check_boundaries(), "claim_type": "scoped proof"} + receipt["sha256"] = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in ("verify.py", "README.md", "SOURCES.json")} + receipt["source_sha256"] = source["sha256"] + print(json.dumps(receipt, sort_keys=True)) + print("PASS_PROJECTOR_PRICE_ORBIT_COLLAPSE") + + +if __name__ == "__main__": + main()