Noncommuting controller stages work for every p: proof of the descending-support invariant (completes #4534 Q2 with #4540; no new κ)

research/descending-invariant-allp/README.md

@@ -0,0 +1,93 @@
+# Noncommuting stages work for every controller size: the descending-support invariant
+
+**Claim type:** a written proof with a mechanized check. **No new κ.** Together with the reduction lemma of
+my #4540, this answers open question 2 of Dugongue's
+[#4534](https://github.com/CrocSwap/integer-mult-bounds/pull/4534) ("an all-p inductive free-algebra
+identity").
+
+## Theorem
+
+Take #4440's complex p-controller for any `p ≥ 1`, any keep mask, and either the full stage set or the
+thick-stage thinning that #4440 and #4470 use. Every word occurring in its operator matrix
+`W ∈ Mat_{2p}(ℚ⟨d_s⟩[q, q^{−1}])` is a strictly descending sequence of distinct stage letters.
+
+**Corollary.** Abelianization is injective on the support of `W`. By #4540's lemma, any scalar commutative
+factorization `L W_ab R = diag(q^ε d^α)`, for example the one #4440's `factor()` computes, is also a
+factorization in the free algebra, with `D_s` noncommuting among themselves and commuting with `Q`. #4534
+proved this only for the fixed p16 word.
+
+## Proof
+
+Lines start as empty words, and later operators are prepended on the left. Only two kinds of event add
+letters:
+
+- `LOCAL(s, pair, ·)` first shears one line of the pair into the other, which merges words, and then
+  prepends `d_s` to both lines.
+- `IDLE(pair, S)` prepends the block `d_{max S}⋯d_{min S}` to both lines.
+
+`ADD` merges word sets, and `SWAP`/`SIGNED_SWAP` move them; neither creates letters. So it suffices that
+**every prepended letter is larger than every letter already on its target lines.** Follow
+`complex_controller_factor.controller`:
+
+1. **Stage order.** Locals run in the order `0, 1, 2, …, 2p`. `LOCAL(2j+1, j)` and `LOCAL(2j+2, j)` act on
+   pair `j`. Until its own locals run, pair `j` holds only letters `≤ 2j`, and only from its own middle idle
+   and its initial block.
+2. **Initial idle**, after stage `2j+1`, on pair `j+1` with `S = {0, …, 2j+1}`. Pair `j+1` is still
+   untouched: bridges so far only mixed pairs `≤ j`. So its words are empty, and the block lands on empty
+   words.
+3. **The bridge `(j, j+1)`** merges words with letters `≤ 2j+1`. Then `LOCAL(2j+2, j)` prepends `2j+2`,
+   which exceeds every letter present.
+4. **Middle idle**, after stage `2j+2`, on pair `j+1` with `S = {2j+2}`. Pair `j+1` carries letters
+   `≤ 2j+1`.
+5. **Terminal idles**, after stage `2p` and before the final bridges, on pair `j` with
+   `S = {2j+3, …, 2p}`. After iteration `j`, pair `j` is never touched again until this point, and it
+   carries letters `≤ 2j+2 < 2j+3`.
+6. **Thinning and keep masks.** Thinning deletes letters from prepends. A keep-mask bit `0` deletes a whole
+   idle. Deleting letters preserves "new letters exceed old ones".
+
+So every word is strictly descending with distinct letters. ∎
+
+## Mechanized check (`verify.py`)
+
+The actual constructor emits its event stream, with its polynomial arithmetic stubbed out, since the event
+sequence does not depend on it. The verifier tracks the largest letter on each line and checks the
+strict-increase condition at every prepend. It covers every `p` from 2 to 60, with keep masks all-ones,
+all-zeros and three random masks, both with and without thick-stage thinning: **590 cases, all passing**.
+A control in which an old stage is prepended again is rejected. `evidence/` records the same check up to
+`p = 200` (440 cases). My #4540 already confirmed the full free-algebra identity directly for `p ≤ 14`.
+
+## The BIT controller
+
+#4440's binary controller, `bit.physical_controller` over `F₂[(ℤ/2)^{2p+2}]`, runs the identical stage and
+idle schedule. The verifier checks the same invariant on its event stream, with idle bitmasks decoded to
+stage lists: **590 more cases**, `p ≤ 60`, five keep masks, with and without thinning. All pass.
+
+Because no letter repeats within a word, the group-ring relation `d² = 1` never acts on the support.
+Abelianization is therefore again injective, and the same corollary applies on the BIT side.
+
+## Not covered
+
+- Existence of the commutative factorization for every `p`. This is #4440's constructor claim.
+- The physical realization of noncommuting `D_s`. That is #4534's open question 1.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/descending-invariant-allp --check-only
+python3.12 -B scripts/research_package.py --package research/descending-invariant-allp
+```
+
+The verifier prints `PASS_DESCENDING_INVARIANT_ALLP` in about a minute, using only the standard library.
+
+## Open next questions
+
+1. **A physically priced noncommuting stage family.** This is #4534's open question 1; the algebra
+   now permits any `p`.
+
+## Credit
+
+- The controller is Cinna Davis's (1337isnot1337, #4440).
+- The question and the p16 theorem are Dugongue's (#4534).
+
+Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
+Apache-2.0.

research/descending-invariant-allp/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40",
+      "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/kappa-rebuild/bit/complex_controller_factor.py",
+      "usage": "input",
+      "git_blob": "cb0cff7c8be5f38f2ee52201d9d0907f9dfd7947",
+      "sha256": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497"
+    },
+    {
+      "path": "research/query-thinned-controllers/controller.py",
+      "usage": "input",
+      "git_blob": "d4557e08cfb9fe57cc1ae4024705a72dc95f3583",
+      "sha256": "8b462d660487b1be4940357c4c7522967b1bfaede3c02b1c66109b85acae0fd2"
+    },
+    {
+      "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py",
+      "usage": "input",
+      "git_blob": "8b40135a84e7f0f0cd44bed69655801310b916a7",
+      "sha256": "8a0de761642d21919e969475c3f13e5d01a4bae7343c1e1f37c586d94b676a85"
+    },
+    {
+      "path": "research/kappa-rebuild/bit/mixed_productive_bit.py",
+      "usage": "input",
+      "git_blob": "9c7a8bd5d3ae4c19952648c815031858d6627b96",
+      "sha256": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e"
+    }
+  ]
+}

research/descending-invariant-allp/TASK.json

@@ -0,0 +1,100 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "original_card": {
+    "id": "independent-moment",
+    "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/staged544-mixed-fourth-entry/README.md",
+      "research/staged-fourth-mixture-ceiling/README.md",
+      "research/r437-two-window-carrier/README.md"
+    ],
+    "methods": [
+      "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.",
+      "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls."
+    ],
+    "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.",
+    "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.",
+    "allowed_variations": [
+      "Reconstruct either a source ledger or a numeric enclosure with a different method."
+    ],
+    "scope_change_triggers": [
+      "Importing the primary function and calling its output independent verification.",
+      "Calling an aggregate histogram or source archive an independently accepted physical supplier."
+    ],
+    "overlap_terms": [
+      "independent moment",
+      "rank histogram",
+      "exact enclosure",
+      "2979",
+      "rank7 joint endframes",
+      "paired extraction",
+      "joint lowering",
+      "4088",
+      "4091",
+      "4067",
+      "staged544-mixed-fourth-entry",
+      "staged-fourth-mixture-ceiling",
+      "r437-two-window-carrier"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.",
+        "evidence": "research/staged544-mixed-fourth-entry/README.md",
+        "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.",
+        "status": "author-checked",
+        "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.",
+        "evidence": "research/staged-fourth-mixture-ceiling/README.md",
+        "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.",
+        "status": "author-checked",
+        "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.",
+        "evidence": "research/r437-two-window-carrier/README.md",
+        "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.",
+        "status": "author-checked",
+        "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "All-p descending-support invariant for the p-controller; completes #4534 Q2 with #4540's lemma.",
+  "scope_change_reason": "Follow-up to #4540.",
+  "bottleneck_link": "Extends native-construction freedom (noncommuting stages) to every controller size.",
+  "budget_minutes": 40,
+  "stop_rule": "Stop at the invariant; physical realization out of scope.",
+  "outcome": "completed",
+  "evidence": "Written proof from the constructor schedule; mechanized check over 590 cases (p<=60) and 440 recorded cases (p<=200). BIT controller: same invariant, 590 cases (p<=60).",
+  "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance",
+  "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.",
+  "open_questions": [
+    {
+      "question": "A physically priced noncommuting stage family (#4534 Q1).",
+      "why_it_matters": "The algebra now permits any p.",
+      "first_step": "One pair of stage embeddings with exact symplectic matrix and central-Q commutation.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/descending-invariant-allp/VERIFY.json

@@ -0,0 +1,25 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/selected-result.json",
+    "docs/research/agent-task-catalog.json",
+    "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py",
+    "research/kappa-rebuild/bit/complex_controller_factor.py",
+    "research/kappa-rebuild/bit/mixed_productive_bit.py",
+    "research/query-thinned-controllers/controller.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 400,
+      "checks": "Descending-support invariant on #4440's constructor event stream for p=2..60, five keep masks, with and without thinning (590 cases); rejection control; recorded sweep to p=200. Also #4440's BIT controller (590 cases)."
+    }
+  ]
+}

research/descending-invariant-allp/evidence/INVARIANT-P2-200.txt

@@ -0,0 +1,4 @@
+Command: python3.12 -B invariant sweep (scratch script equivalent to verify.py invariant(); p = 2..40, 60, 80, 120, 160, 200;
+keep masks all-ones, all-zeros, three random (seed 4540); with and without thick-stage thinning)
+Output:
+invariant holds: 440 cases

research/descending-invariant-allp/verify.py

@@ -0,0 +1,110 @@
+#!/usr/bin/env python3
+"""The descending-support invariant of #4440's complex p-controller, for every p and keep mask.
+
+Invariant (README, written proof): along the constructor's emitted event stream, every stage letter prepended to a
+line (by LOCAL on a thick stage, or as an IDLE block d_(s_k)...d_(s_1)) is larger than every stage letter already on
+that line; ADD only merges lines and SWAP/SIGNED_SWAP only move them. Hence every word in W is strictly descending
+with distinct letters, abelianization is injective on W's support, and by the reduction lemma of
+research/free-identity-allp any scalar commutative factorization L W_ab R = diag is also a noncommuting one.
+
+Mechanized check: the constructor (research/kappa-rebuild/bit/complex_controller_factor.py via
+research/query-thinned-controllers/controller.py) emits its event stream with its polynomial arithmetic stubbed out;
+this verifier tracks, per line, the largest letter present, and checks the strict-increase condition at every
+prepend, for p = 2..60, keep masks all-ones, all-zeros and three random masks, with and without thick-stage thinning.
+The same is checked for #4440's BIT controller (bit.physical_controller; IDLE bitmasks decoded to stage lists).
+evidence/ records the complex check up to p = 200.
+Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0.
+"""
+import hashlib
+import importlib.util
+import json
+from pathlib import Path
+import random
+import sys
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parents[1]
+
+
+def need(condition, message):
+    if not condition:
+        raise AssertionError(message)
+
+
+def load_constructor():
+    sys.path.insert(0, str(ROOT / "research/query-thinned-controllers"))
+    spec = importlib.util.spec_from_file_location("qtc_controller", ROOT / "research/query-thinned-controllers/controller.py")
+    C = importlib.util.module_from_spec(spec)
+    spec.loader.exec_module(C)
+    B, M = C.engines()
+    M.plus = lambda a, b, c=1: a              # the event stream does not depend on the polynomial values
+    M.monomial_times = lambda poly, exp, c=1: poly
+    B.add = lambda a, b: a                    # same for the binary group-ring controller
+    B.shift = lambda a, m: a
+    B.polynomial_coefficients = lambda m: {}
+    return M, B
+
+
+def invariant(events, p, thick=None):
+    mx = [-1] * (2 * p)                       # largest letter on each line; -1 = no letter
+    for ev in events:
+        op = ev[0]
+        if op == "LOCAL":
+            _, stage, pair, rev = ev
+            x, y = (2 * pair + 1, 2 * pair) if rev else (2 * pair, 2 * pair + 1)
+            mx[y] = max(mx[y], mx[x])         # the shear merges x into y before the stage letter
+            if thick is not None and stage not in thick:
+                continue                      # thin stage: query shear only, no letter
+            for r in (x, y):
+                if not stage > mx[r]:
+                    return False
+                mx[r] = stage
+        elif op == "IDLE":
+            _, pair, sel = ev
+            sel = [s for s in sel if thick is None or s in thick]
+            if not sel:
+                continue
+            for r in (2 * pair, 2 * pair + 1):
+                if not min(sel) > mx[r]:
+                    return False
+                mx[r] = max(sel)
+        elif op == "ADD":
+            _, d, s, *c = ev
+            mx[d] = max(mx[d], mx[s])
+        elif op in ("SWAP", "SIGNED_SWAP"):
+            _, x, y = ev
+            mx[x], mx[y] = mx[y], mx[x]
+        else:
+            raise AssertionError("unknown event " + op)
+    return True
+
+
+def main():
+    for row in json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8"))["files"]:
+        need(hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() == row["sha256"], row["path"])
+    M, B = load_constructor()
+    rng = random.Random(4540)
+    cases = bit_cases = 0
+    for p in range(2, 61):
+        thick = {0, 2 * p, *range(1, 2 * p, 2)}
+        for keep in [(1 << (8 * p)) - 1, 0] + [rng.getrandbits(8 * p) for _ in range(3)]:
+            _, events, _ = M.controller(p, keep)
+            for th in (None, thick):
+                need(invariant(events, p, th), f"p={p}: descending invariant")
+                cases += 1
+            _, bev, _ = B.physical_controller(p, keep)
+            bev = [["IDLE", e[1], [s for s in range(2 * p + 1) if e[2] >> (s + 1) & 1]] if e[0] == "IDLE" else e for e in bev]
+            for th in (None, thick):
+                need(invariant(bev, p, th), f"p={p}: BIT descending invariant")
+                bit_cases += 1
+    # control: a schedule that prepends an old stage again must fail
+    bad = [["LOCAL", 1, 0, False], ["LOCAL", 0, 0, False]]
+    need(not invariant(bad, 1), "non-increasing prepend rejected")
+    ev = (HERE / "evidence/INVARIANT-P2-200.txt").read_text(encoding="utf-8")
+    need("invariant holds:" in ev and "FAIL" not in ev, "recorded sweep to p = 200")
+    print(json.dumps({"status": "PASS_DESCENDING_INVARIANT_ALLP", "cases_checked_here": cases, "bit_cases_checked_here": bit_cases, "p_range": [2, 60],
+                      "new_kappa_claimed": False}, indent=1))
+
+
+if __name__ == "__main__":
+    sys.exit(main())