Research: UT3(F4) dependent central triple has exact minimum 12 (closes #2261 three-output question; no new kappa)

research/ut3-f4-dependent-central-triple/CERTIFICATE.json

@@ -0,0 +1,13 @@
+{
+  "schema_version": 1,
+  "minimum_calls": 12,
+  "predecessor_direct_calls": 14,
+  "n_X": 6,
+  "n_Y": 6,
+  "group_order": 64,
+  "labels": 4,
+  "idempotents_r3": 28,
+  "spectator_width": 4,
+  "kappa": "0.001672660197076918",
+  "no_new_kappa": true
+}

research/ut3-f4-dependent-central-triple/PROOF.md

@@ -0,0 +1,129 @@
+# Exact twelve-call minimum
+
+## Statement
+
+Let `H = UT_3(F_4)`, with `F_4 = F_2[w]/(w^2+w+1)` and
+
+```text
+(a,b,c)(a',b',c') = (a+a', b+b', c+c'+a b').
+```
+
+The group has order 64. The four paid labels
+
+```text
+X_1=(1,0,0), X_w=(w,0,0), Y_1=(0,1,0), Y_w=(0,w,0)
+```
+
+are involutions. Write `Z_1=[X_1,Y_1]=(0,0,1)`, `Z_w=[X_w,Y_1]=(0,0,w)`, and `Z_{w^2}=[X_w,Y_w]=(0,0,w^2)`. These central values satisfy `Z_{w^2}=Z_1 Z_w` and `1+w+w^2=0`.
+
+Work in the matrix ring over the group algebra `F_2[H]`. For `r >= 3` and a rank-one idempotent `N` in `M_r(F_2)`, a paid call is
+
+```text
+D_N(g) = I + ([g]+[1]) N,    g in {X_1, X_w, Y_1, Y_w}.
+```
+
+Each call costs one. There is no free clean role, copy, erase, or uncharged inverse. Scalar `GL_r(F_2)` mixing may be inserted, but it normalizes away: conjugation preserves rank-one idempotents, and augmentation sends every paid factor and the target to the identity, so the residual scalar map is the identity. It is enough to bound pure words in the paid factors.
+
+The target is the diagonal operator
+
+```text
+diag([Z_1], [Z_w], [Z_{w^2}], [1], ..., [1])
+```
+
+on arbitrary dirty register inputs. The exact minimum number of paid calls is **12**.
+
+## Attaining word and the previous schedule
+
+Apply, in time order, with `E_{tt}` the coordinate projector:
+
+```text
+E_00: X_1, Y_1, X_1, Y_1
+E_11: X_1, Y_w, X_1, Y_w
+E_22: X_w, Y_w, X_w, Y_w
+```
+
+Each block is four calls. Disjoint supports do not interact, and every spectator coordinate is fixed. Because each label is an involution, the address multiplier on coordinate `t` is the length-four commutator of that block:
+
+```text
+X_1 Y_1 X_1 Y_1 = Z_1,
+X_1 Y_w X_1 Y_w = Z_w,
+X_w Y_w X_w Y_w = Z_{w^2}.
+```
+
+The bill is 12 calls: six `X`-type and six `Y`-type. Letter counts are `n(X_1)=4`, `n(X_w)=2`, `n(Y_1)=2`, `n(Y_w)=4`.
+
+The schedule recorded with the two-register minimum used a six-call composite on the third output,
+
+```text
+X_1, X_w, Y_1, X_1, X_w, Y_1 = Z_{w^2},
+```
+
+together with four calls for `Z_1` and four calls for `Z_w` through `Y_1` only. That word is correct and costs **14**. It does not use `Y_w`. The twelve-call word replaces that composite by the primitive commutator `[X_w,Y_w]`.
+
+## Nilpotent expansion
+
+Realize `H` by its defining matrices over `F_4` and expand scalars through the regular representation `F_4 -> M_2(F_2)`. Each group element becomes a `6×6` binary matrix. For a paid label `g`, the nilpotent `E(g)=ρ(g)+I` has a single off-diagonal block:
+
+- `X_1` and `X_w` occupy the `A` block (rows `0..1`, columns `2..3`) with `F_4` coefficients `1` and `w`;
+- `Y_1` and `Y_w` occupy the `B` block (rows `2..3`, columns `4..5`) with coefficients `1` and `w`.
+
+Direct multiplication of these four nilpotents gives:
+
+- `E(X)E(Y)` is the pure corner `α(X)β(Y)` in rows `0..1`, columns `4..5`;
+- `E(Y)E(X)`, `E(X)E(X)`, and `E(Y)E(Y)` are zero;
+- every product of three nilpotents is zero.
+
+Therefore, for calls applied in time order `g_1,...,g_n` with matrices `N_1,...,N_n`,
+
+```text
+T = D(g_n) ... D(g_1)
+  = I + sum_k E(g_k)⊗N_k
+      + sum_{i<j} E(g_j)E(g_i)⊗(N_j N_i).
+```
+
+The length-two sum is supported only on pairs where call `i` is `Y`-type, call `j` is later and `X`-type, and the corner coefficient is `α(g_j)β(g_i)`.
+
+The image of the target under `ρ` has vanishing `A` and `B` blocks and corner
+
+```text
+I_2⊗(E_00+E_22) + M_w⊗(E_11+E_22),
+```
+
+where `M_w` is multiplication by `w` and the displayed diagonal matrices are the `r×r` projectors onto the first three coordinates (zeros on spectators). Write `P=E_00+E_22` and `Q=E_11+E_22`. Any word whose full group-algebra endpoint is the target must realize this corner and must have zero linear blocks, because `ρ` is a group homomorphism. The corner identities are necessary; the twelve-call upper bound is checked separately in the full group algebra, not in this `6×6` quotient.
+
+## Rank bound
+
+Zero linear `A` and `B` blocks mean
+
+```text
+sum_{X-calls} α_s N_s = 0,    sum_{Y-calls} β_t N_t = 0
+```
+
+in `M_r(F_4)`. Factor `N_s=u_s v_s^T` with `v_s^T u_s=1`. For the `X` calls let `α_s in {1,w}` have `F_2` coordinates `(α_{s0},α_{s1})`, and view `α_s u_s` as the column `(α_{s0} u_s, α_{s1} u_s)` in `F_2^{2r}`. If `U` has those columns and `V` has rows `v_s^T`, then `UV=0`, so
+
+```text
+n_X >= rank(U) + rank(V).
+```
+
+Here `rank(V)=dim span{v_s}`. Because `1` and `w` land in complementary summands,
+
+```text
+rank(U) = dim span{u: label X_1} + dim span{u: label X_w}
+        >= dim span{u: all X calls}.
+```
+
+The same identities hold for the `Y` calls.
+
+Columns of each corner component lie in `span{u: X calls}`, and rows lie in `span{v: Y calls}`, because a contributing term has the shape `u_X (v_X·u_Y) v_Y^T` after the later/earlier assignment above. Thus
+
+```text
+span{e_0,e_1,e_2} ⊆ span{u_X} ∩ span{v_Y}.
+```
+
+The contragredient representation `(ρ(g)^{-1})^T` reverses the corner order: the same target corner is produced by later `Y` calls after earlier `X` calls, with columns in `span{u_Y}` and rows in `span{v_X}`. Hence all four spans have dimension at least 3, `rank(U)>=3`, and `rank(V)>=3`. Therefore `n_X>=6` and `n_Y>=6`, so every realizing word costs at least `12`.
+
+The twelve-call word meets both inequalities with equality of the summed ranks. The minimum is exactly 12 for every finite `r>=3`, including arbitrary restored dirty spectators.
+
+## What is not claimed
+
+The alphabet is only the four involutions above. Labels `X_{w^2}` and `Y_{w^2}` are outside the argument, because a coefficient `w^2=(1,1)` no longer sits in a single complementary summand. The result is not a bit-supplier embedding, a hosting or precision bill, or a change of `κ`. The selected decimal remains `0.001672660197076918`.

research/ut3-f4-dependent-central-triple/README.md

@@ -0,0 +1,69 @@
+# Twelve calls suffice and are necessary for one UT3(F4) central triple
+
+**Scoped formal minimum; no new kappa.** In `F_2[UT_3(F_4)]`, every word in the four involutory labels `X_1,X_w,Y_1,Y_w` with rank-one idempotent calls that realizes
+
+```text
+diag([Z_1], [Z_w], [Z_{w^2}])
+```
+
+on three registers, and the identity on every extra dirty register, has length at least **12**. The disjoint commutator schedule
+
+```text
+[X_1,Y_1], [X_1,Y_w], [X_w,Y_w]
+```
+
+attains 12. The six-call composite previously used for `Z_{w^2}` attains the same endpoint in **14** calls and is not minimal. The selected decimal stays `0.001672660197076918`.
+
+The proof is the nilpotent corner expansion of the defining `6×6` representation together with a rank-nullity count on each letter class: `n_X>=6` and `n_Y>=6`. Full group-algebra evaluation checks the twelve-call word, the fourteen-call composite, a restored spectator, and every one-call deletion. Details are in [PROOF.md](PROOF.md).
+
+This is a side result about one finite address alphabet. It does not change a supplier profile, a hosting bill, or `κ`. The operative donor priority revision is 6. The pinned catalogue object in this checkout is historical revision 3; the selected decimal above is the one revision 6 still binds.
+
+## Costs
+
+| Schedule | Calls | Letter split |
+|---|---:|---|
+| Disjoint commutators `[X_1,Y_1]`, `[X_1,Y_w]`, `[X_w,Y_w]` | 12 | `n_X=6`, `n_Y=6` |
+| Previous composite on the third output | 14 | four + four + six |
+| Rank-nullity floor | 12 | `6+6` |
+
+At a positive per-call price `α` the sharp bill is `12α`. The two-call improvement over the composite is only an invocation saving inside this formal alphabet.
+
+## Reproduce
+
+From the repository root, standard-library Python 3.12:
+
+```sh
+python3 -I -B research/ut3-f4-dependent-central-triple/verify.py
+python3 -I -O -Werror -B research/ut3-f4-dependent-central-triple/verify.py
+python3 -I -B research/ut3-f4-dependent-central-triple/independent.py
+python3 -I -B research/ut3-f4-dependent-central-triple/test_package.py
+python3 -B scripts/research_package.py --package research/ut3-f4-dependent-central-triple
+```
+
+Expected verifier line:
+
+```text
+PASS_UT3_F4_DEPENDENT_TRIPLE minimum=12 predecessor_direct=14 nX=6 nY=6 group_order=64 idempotents=28 spectator=1 omission_controls=12 no_new_kappa
+```
+
+`verify.py` is read-only. It rejects a corrupted temporary copy of [CERTIFICATE.json](CERTIFICATE.json) and rejects duplicate JSON keys. Checks remain active under `-O`.
+
+## Scope
+
+The predecessor two-register minimum is eight calls for `diag([Z_1],[Z_w])`, proved by a radius-three search plus an even-length parity cut, and it left the dependent three-output word open. The block family tested there used only `Y_1`. This note keeps that alphabet and role model, replaces the unsearched length bound by an exact minimum, and does not reopen the two-register census.
+
+Nearby bipartite commutator tariffs count independent central edges in a larger Heisenberg group. The center of `UT_3(F_4)` is the two-dimensional quotient of that four-dimensional center, so those edge multiplicities do not apply verbatim. The argument here is the quotient corner, not a citation of the cover bound.
+
+Not claimed: a shorter word after adding `X_{w^2}` or `Y_{w^2}`; a physical bit-supplier realization; any selected-profile or `κ` change. The result is disjoint from Q8 negative-target minima, odd-kernel tariffs, flag-0 tail hosts, gate-operand parity, C5 charging, present-head side corrections, rank-7 width audits, and stock-leaf packaging.
+
+## Open next questions
+
+Can the involutions `X_{w^2}=(w^2,0,0)` and `Y_{w^2}=(0,w^2,0)` reduce this triple below 12 calls? Extend the complementary-summand rank identity, which uses coefficients in `{1,w}` only, to the coefficient `w^2=(1,1)`, and test whether a length-10 word appears. The blocker is that `w^2` mixes the two `F_2` summands, so the present `n_X>=6` split does not apply.
+
+Can one of these twelve formal calls be embedded in a pinned bit supplier below the complete price of a rank-one factor? Charge frame changes, hosting, restoration, and dispatch for the `w=3,k=1` boundary of this word. The blocker is the absence of a legal physical realization; the formal count does not supply one.
+
+## Credit
+
+The two-register minimum, the fourteen-call composite, and the open three-output question are Cinna Davis's UT3(F4) central-pair note. The rank-one idempotent register model follows the eumemic / woklerx address-call lineage used there. The rank-nullity shape is the same style as the UT3(F2) central arguments; the corner identities and the twelve-call schedule are specific to this `F_4` quotient.
+
+Prepared by Wentao Li with substantial AI assistance. No independent human or proof-assistant review is claimed. Apache-2.0.

research/ut3-f4-dependent-central-triple/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1",
+      "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075"
+    }
+  ]
+}

research/ut3-f4-dependent-central-triple/TASK.json

@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 3,
+  "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?",
+    "starting_points": [
+      "certificates/selected-result.json",
+      "research/hyperplane-end-lean/PROOF.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove the exact paid-call minimum for diag([Z_1],[Z_w],[Z_w^2]) in F2[UT3(F4)] on the four involutory labels with rank-one idempotents and arbitrary dirty spectators.",
+  "scope_change_reason": "The catalogue card asks for a selected-interface formal lemma. The operative gap is the dependent three-output word left open by the UT3(F4) central-pair minimum. This package proves that finite address minimum. It is a side result: no selected-supplier interface is discharged and kappa is unchanged. Donor priority revision 6 binds the same selected decimal; the pinned catalogue object is historical revision 3.",
+  "bottleneck_link": "Side result. The complex supplier remains binding. A sharp formal call count removes an under-priced 14-call schedule for this alphabet without changing kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the twelve-call word and the matching n_X,n_Y rank bound are checked in the full group algebra, including the spectator and one-call deletions. Do not search enlarged alphabets or physical embeddings in this package.",
+  "outcome": "completed",
+  "evidence": "PASS_UT3_F4_DEPENDENT_TRIPLE minimum=12 predecessor_direct=14 nX=6 nY=6; independent frozenset replay; omission and duplicate-key controls.",
+  "author": "Wentao Li",
+  "ai_assistance": "Substantial AI assistance for the rank-nullity argument, independent replay, and write-up.",
+  "open_questions": [
+    {
+      "question": "Do the extra involutions X_{w^2} and Y_{w^2} reduce the dependent triple below 12 calls?",
+      "why_it_matters": "A shorter word would replace the sharp bill for this endpoint inside a mildly larger alphabet.",
+      "first_step": "Extend the complementary-summand identity from coefficients {1,w} to w^2=(1,1) and test length 10.",
+      "blocked_by": "w^2 mixes the two F2 summands, so the present n_X>=6 split does not apply."
+    },
+    {
+      "question": "Can one of the twelve formal calls be realized in a pinned bit supplier below one rank-one complete price?",
+      "why_it_matters": "Only then does the invocation count change a physical bill.",
+      "first_step": "Charge frame changes, hosting, restoration, and dispatch for this twelve-call boundary.",
+      "blocked_by": "No legal physical realization is supplied; the formal count does not provide one."
+    }
+  ]
+}

research/ut3-f4-dependent-central-triple/VERIFY.json

@@ -0,0 +1,51 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Full group law, nilpotent corner table, twelve-call and fourteen-call endpoints, spectator, twelve omissions, rank counts, read-only receipt, duplicate-key rejection."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-Werror",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Same checks with assertions removed by -O; need() still enforces every gate."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/independent.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Separate frozenset convolution of both schedules, commutators, and span counts."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/test_package.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Replays verify under -O -Werror, independent, and a duplicate-key control."
+    }
+  ]
+}