Noncommuting controller identity for all p ≤ 14 (91 cases) via a support-injectivity reduction (answers #4534 Q2 empirically; no new κ)

research/free-identity-allp/README.md

@@ -0,0 +1,72 @@
+# The noncommuting controller identity at every tested size, and why it holds
+
+**Claim type:** a reduction lemma plus exact finite evidence. **No new κ.** It addresses open question 2 of
+Dugongue's [#4534](https://github.com/CrocSwap/integer-mult-bounds/pull/4534), "an all-p inductive
+free-algebra identity". #4534 proves the noncommuting-stage identity only for #4470's fixed p16 word. My
+#4539 replayed that case.
+
+## Reduction lemma
+
+Let `W ∈ Mat_{2p}(ℚ⟨d_s⟩[q, q^{−1}])` be the controller word, with `q` central and the `d_s` free, and let
+`L` and `R` be scalar matrices. Suppose the abelianization map, which forgets letter order, is **injective on
+the set of monomials that occur in `W`**. Then the commutative identity `L W_ab R = diag(…)` implies the free
+identity `L W R = diag(…)`.
+
+**Proof.** Every entry of `L W R` is a scalar combination of `W`'s monomials. Under the injectivity
+hypothesis, its coefficients are exactly those of the corresponding commutative entry. ∎
+
+A strictly descending word with distinct letters is determined by its letter set. So it suffices that every
+monomial of `W` is strictly descending.
+
+## Evidence
+
+The controllers are emitted by #4440's constructor on main (`research/query-thinned-controllers/controller.py`)
+for each size `p` and prefix length `a`, together with their **commutative** boundaries `L` and `R`. A
+separately written free-algebra replay then shows:
+
+| range | cases | result |
+| --- | ---: | --- |
+| `p = 2…10`, all `a = 0…p−2` (in `verify.py`) | 45 | `L W R` is diagonal in the free algebra, with single monomials that abelianize to the commutative diagonal. `W` has exactly **2p** monomials, all strictly descending. |
+| `p = 2…14`, all `a` (in `evidence/`) | 91 | the same |
+| #4470's actual p16 `CONTROLLER.json` | 1 | 32 monomials, all strictly descending |
+
+So for every tested size, the **commutative boundaries already work for noncommuting stages**, as the lemma
+predicts. The support of `W` is tiny: exactly the 2p diagonal monomials, each a descending chain of thick
+stages.
+
+## Why descending (observed structure)
+
+Stage letters enter in chronological order: `LOCAL` events run in increasing stage order, and each `IDLE`
+prepends the block `d_{s_k}⋯d_{s_1}` of earlier stages. Every observed word is strictly descending, which
+suggests a general invariant: whenever a letter is prepended to a line, it exceeds every letter already on
+that line. A proof for all `p` needs the constructor's pair and idle schedule and is **not** given here.
+
+## Not covered
+
+- An all-`p` proof of the descending-support invariant.
+- `p > 14`, except for #4470's p16 support.
+- The physical realization of noncommuting `D_s`.
+
+## Reproduce
+
+```sh
+python3.12 -B scripts/research_package.py --package research/free-identity-allp --check-only
+python3.12 -B scripts/research_package.py --package research/free-identity-allp
+```
+
+The verifier prints `PASS_FREE_IDENTITY_ALLP` in about a minute, using only the standard library.
+
+## Open next questions
+
+1. **Prove the descending-support invariant from #4440's constructor schedule for all `p` and `a`.**
+   - *Why it matters:* it would give #4534's all-`p` theorem through the lemma above.
+   - *First step:* show that each `IDLE` targets a pair whose lines carry no stage letter above the idle's
+     smallest stage.
+
+## Credit
+
+- The question and the p16 theorem are Dugongue's (#4534).
+- The constructor is Cinna Davis's (1337isnot1337, #4440 and #4470).
+
+Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.
+Apache-2.0.

research/free-identity-allp/SOURCES.json

@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc",
+  "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/joint-helper-lattice/CONTROLLER.json",
+      "usage": "input",
+      "git_blob": "49a2f0675819f9deeea27ed77be2c2b6ff2e87e5",
+      "sha256": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f"
+    },
+    {
+      "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"
+    },
+    {
+      "path": "research/kappa-rebuild/bit/complex_controller_factor.py",
+      "usage": "input",
+      "git_blob": "cb0cff7c8be5f38f2ee52201d9d0907f9dfd7947",
+      "sha256": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497"
+    }
+  ]
+}

research/free-identity-allp/TASK.json

@@ -0,0 +1,100 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc",
+  "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": "Reduction lemma and finite evidence for #4534's all-p noncommuting controller identity.",
+  "scope_change_reason": "Open question 2 of #4534.",
+  "bottleneck_link": "Extends the algebraic interface for native construction changes on the kappa ~0.00302 line.",
+  "budget_minutes": 40,
+  "stop_rule": "Stop at the lemma and p<=14 evidence.",
+  "outcome": "completed",
+  "evidence": "Commutative boundaries diagonalize W in the free algebra for all 91 (p,a) with p<=14; W has exactly 2p strictly descending monomials, so abelianization is injective on its support.",
+  "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": "Prove the descending-support invariant for all p and a.",
+      "why_it_matters": "Gives #4534's all-p theorem via the lemma.",
+      "first_step": "Show each IDLE targets lines with no stage letter above its smallest stage.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/free-identity-allp/VERIFY.json

@@ -0,0 +1,26 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/selected-result.json",
+    "docs/research/agent-task-catalog.json",
+    "research/joint-helper-lattice/CONTROLLER.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": "Free-algebra controller identity for p=2..10, all prefix lengths (45 cases): commutative boundaries diagonalize in the free algebra, W has 2p strictly descending monomials; p16 #4470 support; recorded p<=14 sweep (91 cases)."
+    }
+  ]
+}

research/free-identity-allp/evidence/FREE-P2-14.txt

@@ -0,0 +1,16 @@
+p 2 done; cases 1 fails [] constructor errors 0
+p 3 done; cases 3 fails [] constructor errors 0
+p 4 done; cases 6 fails [] constructor errors 0
+p 5 done; cases 10 fails [] constructor errors 0
+p 6 done; cases 15 fails [] constructor errors 0
+p 7 done; cases 21 fails [] constructor errors 0
+p 8 done; cases 28 fails [] constructor errors 0
+p 9 done; cases 36 fails [] constructor errors 0
+p 10 done; cases 45 fails [] constructor errors 0
+p 11 done; cases 55 fails [] constructor errors 0
+p 12 done; cases 66 fails [] constructor errors 0
+p 13 done; cases 78 fails [] constructor errors 0
+p 14 done; cases 91 fails [] constructor errors 0
+TOTAL 91 fails [] constructor errors []
+
+[exited with code 0]

research/free-identity-allp/evidence/SUPPORT-P2-14.txt

@@ -0,0 +1,16 @@
+2 [] max support 4
+3 [] max support 6
+4 [] max support 8
+5 [] max support 10
+6 [] max support 12
+7 [] max support 14
+8 [] max support 16
+9 [] max support 18
+10 [] max support 20
+11 [] max support 22
+12 [] max support 24
+13 [] max support 26
+14 [] max support 28
+ALL DESCENDING: True 91
+
+[exited with code 0]