Independent reconstruction of the UT3(F4) central-triple model: witnesses, controls, finite certificates and a bounded shorter-word search (no new kappa)

research/ut3-central-triple-independent/README.md

@@ -0,0 +1,120 @@
+# Independent check: the UT3(F4) central-triple register model
+
+**Result class: independent reproduction plus a bounded search failure.** No new
+kappa. The selected conditional result stays
+`kappa = 0.001672660197076918`.
+
+## What was checked, and how
+
+Two open results use one formal register model. In `F_2[UT_3(F_4)]` with
+`F_4 = F_2[w]/(w^2+w+1)`, a paid call is
+
+```text
+D_N(g) = I + ([g] + [1]) N,
+```
+
+with `g` one of the six axis involutions `X_1, X_w, X_{w^2}, Y_1, Y_w, Y_{w^2}`
+and `N` a rank-one idempotent in `M_r(F_2)`. The target on `r >= 3` registers is
+
+```text
+diag([Z_1], [Z_w], [Z_{w^2}], [1], ..., [1]),   Z_c = (0,0,c).
+```
+
+[PR #3774](https://github.com/CrocSwap/integer-mult-bounds/pull/3774) proves the
+four-label minimum 12; [PR #3788](https://github.com/CrocSwap/integer-mult-bounds/pull/3788)
+extends it to six labels. [PR #3784](https://github.com/CrocSwap/integer-mult-bounds/pull/3784),
+[#3785](https://github.com/CrocSwap/integer-mult-bounds/pull/3785),
+[#3786](https://github.com/CrocSwap/integer-mult-bounds/pull/3786) and
+[#3783](https://github.com/CrocSwap/integer-mult-bounds/pull/3783) record the
+same floor and its finite counts in a second, separately written form.
+
+This package rebuilds the model from the stated definition, using no code from
+those packages, and checks it. `model.py` carries two layers: the group algebra
+`F_2[H]` as 64-bit masks over an explicit product table, and the regular
+representation `rho tensor id`, which is injective, so matrix equality in
+`M_{6r}(F_2)` is equivalent to word equality in `F_2[H] tensor M_r(F_2)`.
+Everything below is measured on this implementation.
+
+| Check | Result |
+|---|---|
+| Group law: closure, full associativity, identity, inverses | order 64, all pass |
+| Six paid labels involutions; nine commutators | 6 and 3 distinct `Z` labels, all equal to `(0,0,alpha beta)` |
+| Rank-one matrices of `M_3(F_2)` (exhaustive over 512) | 49 rank-one, 28 rank-one idempotent, 21 trace-zero |
+| `u v^T` enumeration against exhaustive rank-one idempotents | identical 28-element set |
+| Mixed twelve-call word on `r = 3, 4, 5` | realizes the target; every extra register fixed |
+| Both-new twelve-call word on `r = 3, 4, 5` | realizes the target; every extra register fixed |
+| Single-deletion controls, both words | 24 of 24 deletions fail |
+| Block collapse versus the direct matrix product, 40 random words | 0 mismatches |
+| Block relation on the class sums, kernel dimension | rank 18 of 27, kernel 9 = the equal triples |
+| Stacked corner: block ranks, total rank | 2, 2, 2 and rank 6 |
+| Uniform random words, length 6-11, `r = 3` | 20000 trials, 0 realizing |
+| Class-sum-feasible words, shapes 4+4 to 6+5, `r = 3` | 18734 tested, 0 realizing |
+
+The class-sum-feasible family is the useful part of the search. Expanding the
+product of the calls gives `I + sum_k E(g_k) tensor N_k` plus the surviving
+second-order corners; the vanishing of the `(0,1)` and `(1,2)` blocks then
+forces the three per-letter-class idempotent sums on each side to agree, and
+that relation is checked here as a linear map: rank 18 on a 27-dimensional
+domain, so its kernel is exactly the nine-dimensional space of equal triples.
+The
+search samples that family shape by shape, with class multisets built from
+cancellation pairs plus one unpaired idempotent where the parity requires it.
+All eight call-count shapes from `4+4` to `6+5` were drawn at least 1150 times
+each (`4+4: 1249`, `4+5: 2541`, `4+6: 1273`, `5+4: 2519`, `5+5: 4928`,
+`5+6: 2596`, `6+4: 1150`, `6+5: 2478`). No word of length at most eleven
+realizes the target.
+
+## What this does not establish
+
+- **No machine-verified lower bound.** The step from the finite corner,
+  row-space and diagonal-lift inequalities to every `r >= 3` is a written
+  argument in the checked results. This package reproduces the finite pieces
+  and a witness half; it does not verify that step, so "minimum 12" remains
+  author-proved, not independently proved.
+- **A bounded search failure is not a lower bound.** The search covers one
+  subfamily exhaustively in shape but only by sampling, and it excludes even
+  call counts with a nonzero common value, which the cancellation-pair
+  construction does not reach.
+- **The `82160`-subset diagonal-lift census of PR #3788 was not reproduced.**
+- **No physical content.** Twelve calls are a formal per-call price in this
+  alphabet: no supplier, hosting, restoration or kappa claim is made, and none
+  of these calls is priced against the selected construction.
+- Two real defects were found in this package's own first draft by its own
+  checks (a trace parity test and the surviving-pair order); both are fixed in
+  the committed code and the checks that caught them are retained.
+
+## Reproduce
+
+```sh
+python3.12 -I -O -Werror -B research/ut3-central-triple-independent/verify.py
+```
+
+Expected: `PASS_UT3_CENTRAL_TRIPLE_INDEPENDENT order=64 involutions=6
+idempotents=28 trace_zero=21 witnesses=2 deletions=24 uniform_trials=20000
+class_sum_tested=18734 shorter_words=0`
+
+The run is deterministic (seeded `20261018`) and takes a few seconds. It writes
+`RESULT.json` with a SHA-256 receipt over its own sorted payload.
+
+## Open next questions
+
+1. **Can the all-`r` step be machine-verified instead of inspected?** It is the
+   only part a formal kernel could still reject. First step: encode the corner
+   and row-space inequalities as a finite linear-algebra statement with symbolic
+   `r`, or prove a residual bound by hand.
+2. **Is the minimum decided without the four-label split, on even call counts
+   with a nonzero class sum?** The sampled family does not reach those shapes.
+   First step: extend the class-sum-feasible construction with sums of three
+   idempotents that are not a cancellation pair.
+3. **Can one of the twelve formal calls be embedded in a pinned bit supplier
+   below the complete price of a rank-one factor?** Without an embedding the
+   count carries no physical saving. First step: price one legal physical
+   commutator pair including frames, hosting and restoration.
+
+## Credit
+
+Credit the authors and predecessors of PR #3774, PR #3788, PR #3784, PR #3785,
+PR #3786, PR #3783, and of the earlier UT3/D8 central-commutator line
+(#2261 and its lineage) for the model, the witnesses and the floor claims this
+package checks. Package produced by Nick Petalas with AI assistance. Independent
+human and formal proof-kernel review are unclaimed. Apache-2.0.

research/ut3-central-triple-independent/RESULT.json

@@ -0,0 +1,80 @@
+{
+ "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+ "block_relation": {
+  "domain_dim": 27,
+  "kernel_dim": 9,
+  "rank": 18
+ },
+ "collapse": {
+  "mismatches": 0,
+  "trials": 40
+ },
+ "corner": {
+  "corner_block_ranks": [
+   2,
+   2,
+   2
+  ],
+  "stacked_rank": 6
+ },
+ "group_law": {
+  "commutator_classes": 3,
+  "elements": 64,
+  "involutions": 6
+ },
+ "matrix_census_r3": {
+  "r": 3,
+  "rank_one": 49,
+  "rank_one_idempotents": 28,
+  "rank_one_trace_zero": 21
+ },
+ "not_checked": [
+  "all-r step of the lower-bound arguments (inspected, not machine-verified)",
+  "the 82160-subset diagonal-lift census of PR 3788",
+  "physical realisation, hosting or price of the twelve formal calls"
+ ],
+ "package": "research/ut3-central-triple-independent",
+ "receipt_sha256": "a5c3f2fc2b3ad05bc721752d9f149c0a150afc7de551aa782db93a526cbc9db7",
+ "schema_version": 1,
+ "search": {
+  "class_sum_feasible": {
+   "draws": 20000,
+   "hits": 0,
+   "r": 3,
+   "tested": 18734,
+   "tested_by_shape": {
+    "4+4": 1249,
+    "4+5": 2541,
+    "4+6": 1273,
+    "5+4": 2519,
+    "5+5": 4928,
+    "5+6": 2596,
+    "6+4": 1150,
+    "6+5": 2478
+   }
+  },
+  "uniform": {
+   "hits": 0,
+   "length_range": [
+    6,
+    11
+   ],
+   "r": 3,
+   "trials": 20000
+  }
+ },
+ "witnesses": {
+  "both_new": {
+   "deletion_failures": 12,
+   "length": 12,
+   "n_x": 6,
+   "n_y": 6
+  },
+  "mixed": {
+   "deletion_failures": 12,
+   "length": 12,
+   "n_x": 6,
+   "n_y": 6
+  }
+ }
+}

research/ut3-central-triple-independent/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "files": [
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    },
+    {
+      "path": "research/ut3-f4-central-pair-seedfcd785a2/README.md",
+      "usage": "provenance",
+      "git_blob": "c16c8394e0259c70a6e75e59fd173cf03d145202",
+      "sha256": "82b67c8b39e0290a86e5e2d54afc22f1a576af40b22fe2e3e71f60a0feaea060"
+    },
+    {
+      "path": "research/ut3-central-commutator-index/README.md",
+      "usage": "provenance",
+      "git_blob": "7a91b02231c5ff8445ec41cfd42c65c8e9e719fb",
+      "sha256": "c2df9a467945360e333fe475c2d0d9fa2961d2ab4fcb252a48faf7cb384dfb46"
+    },
+    {
+      "path": "research/ut3-two-targets-any-registers/README.md",
+      "usage": "provenance",
+      "git_blob": "3fc4f569a2e9bc81a1f61bc8343a276671a2d13f",
+      "sha256": "f879e3009b1fd5c625480ef92bdc454030ae62e7b378af7869e188df718e7399"
+    }
+  ]
+}

research/ut3-central-triple-independent/TASK.json

@@ -0,0 +1,88 @@
+{
+ "schema_version": 1,
+ "task_id": "bit-new-register-model",
+ "priority_revision": 6,
+ "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+ "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": "Independent verification of one specified nonabelian register model: the F_2[UT_3(F_4)] paid-call word problem with six paid involutions, rank-one idempotent calls and a three-register central-triple target, as stated in the open results PR #3774 and PR #3788. The package independently rebuilds the model, checks the two twelve-call witnesses, all single-deletion controls, the matrix-ring censuses recorded by #3785 and #3784, and the block collapse the lower-bound arguments use, then runs a bounded falsification search for a realizing word of length at most eleven.",
+ "scope_change_reason": "The card asks whether a larger or nonabelian register model can escape the scoped three-register obstruction, and names no single explicit alphabet. The UT3(F4) central-triple alphabet is one such explicit model and currently carries an unreviewed minimum-length claim in two open pull requests, so the same question is answered here for that one pinned model by independent reproduction and bounded search rather than by another mechanism search.",
+ "bottleneck_link": "The central-triple call count is a formal per-call price in this alphabet. A reproduced witness and a reproduced finite certificate decide whether the open minimum-12 claim can be relied on as a scoped input; they do not change the selected kappa, and the twelve calls are not a supplier or a physical price.",
+ "budget_minutes": 60,
+ "stop_rule": "Stop once the model, the witnesses, the deletion controls, the two matrix-ring censuses and the collapse identity are reproduced and the bounded search finishes. Do not claim a machine-verified all-r lower bound, do not attempt a physical realisation, and do not change any selected result.",
+ "outcome": "completed",
+ "evidence": "With an independently written model: the group has order 64 and is associative with the six paid labels involutions and the nine commutators equal to the three Z labels; the three-bit matrix ring has 49 rank-one matrices, 28 rank-one idempotents and 21 rank-one trace-zero matrices, matching the counts recorded in #3785; both published twelve-call words realize the target on three, four and five registers with every extra register fixed; all 24 single deletions fail; the block collapse equals the direct matrix product on 40 random words; the stacked corner has rank 6 with rank-two blocks. The bounded search tested 20000 uniform random words of length 6 to 11 and 18734 words drawn from the class-sum-feasible family that every realizing word must belong to (all eight feasible call-count shapes from 4+4 to 6+5, at least 1150 draws each) and found no word of length at most eleven that realizes the target.",
+ "author": "Nick Petalas",
+ "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+ "overlap": {
+  "checked_at": "2026-10-18",
+  "coverage": "Open pull requests and discussions were read through the repository API before starting; find_overlap was run for the register-model card and the two open UT3 central-triple pull requests were read directly. This is an overlap check, not a novelty certificate.",
+  "checked_paths": [
+   "PR #3774 research/ut3-f4-dependent-central-triple",
+   "PR #3788 research/ut3-f4-w2-lift-obstruction",
+   "PR #3784 research/central-triple-rank-floor",
+   "PR #3785 research/rank-one-idempotent-count",
+   "PR #3786 research/six-label-central-floor",
+   "PR #3783 research/twelve-call-central-triple"
+  ]
+ },
+ "open_questions": [
+  {
+   "question": "Can the all-r step of the two lower-bound arguments be machine-verified rather than inspected?",
+   "why_it_matters": "The finite certificates reproduce, but the passage from the corner, row-space and diagonal-lift inequalities to every r >= 3 is a written proof step in this package's evidence and the only part that a formal kernel could still reject.",
+   "first_step": "Encode the corner and row-space inequalities as a finite linear-algebra statement over symbolic r and check it with a proof assistant, or bound the residual by hand and record the bound in the package.",
+   "blocked_by": "No formal kernel run is part of this session; the statement is quantified over r, not over a finite domain."
+  },
+  {
+   "question": "Is the minimum-length question decided when w^2 is excluded and X_{w^2} alone is adjoined, i.e. does the four-label complementary split ever admit an eleven-call word?",
+   "why_it_matters": "The two open results use different arguments for the four-label and six-label cases; a word that needs only the weaker split would show the two hypotheses are not interchangeable.",
+   "first_step": "Extend the class-sum-feasible family here to the remaining even call counts with a nonzero common value, which the cancellation-pair construction does not reach.",
+   "blocked_by": "Even call counts with a nonzero class sum were not constructed in this session; the family sampled is a strict subfamily of the shapes the block equations allow."
+  },
+  {
+   "question": "Can any of the twelve formal calls be embedded in a pinned bit supplier below the complete price of a rank-one factor?",
+   "why_it_matters": "Without an embedding the twelve calls carry no physical saving and cannot move the selected kappa.",
+   "first_step": "Price one legal physical realisation of a single commutator pair including frames, hosting and restoration.",
+   "blocked_by": "No physical realisation, supplier admission or complete invoice is supplied here or in the checked results."
+  }
+ ]
+}

research/ut3-central-triple-independent/VERIFY.json

@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-Werror",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 600,
+      "checks": "Independent reconstruction of the F_2[UT_3(F_4)] paid-call model: group law over all 64 elements including associativity, the six involutions and the nine commutators; the rank-one and rank-one-idempotent census of the three-bit matrix ring by exhaustive enumeration (49 rank-one, 28 idempotent, 21 trace-zero); both twelve-call witnesses against the target on three, four and five registers with the spectator register checked fixed; all twenty-four single-deletion controls; the block collapse used by the lower-bound arguments against the direct matrix product on forty random words; the class-sum block relation and its kernel dimension; the stacked corner rank; and a bounded falsification search for a realizing word of length at most eleven. No new kappa."
+    }
+  ]
+}