Research: six-label UT3(F4) triple still costs 12 after adjoining w^2 (answers #3774; no new kappa)

research/ut3-f4-w2-lift-obstruction/CERTIFICATE.json

@@ -0,0 +1,16 @@
+{
+  "schema_version": 1,
+  "alphabet_labels": 6,
+  "six_label_minimum": 12,
+  "mixed_word_calls": 12,
+  "both_new_labels_calls": 12,
+  "n_X": 6,
+  "n_Y": 6,
+  "blind_separated_span": 2,
+  "mixed_lift_rank": 3,
+  "shadow_subsets_r3": 82160,
+  "group_order": 64,
+  "idempotents_r3": 28,
+  "kappa": "0.001672660197076918",
+  "no_new_kappa": true
+}

research/ut3-f4-w2-lift-obstruction/PROOF.md

@@ -0,0 +1,150 @@
+# Six-label diagonal lift
+
+## 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 six paid labels
+
+```text
+X_1=(1,0,0), X_w=(w,0,0), X_{w^2}=(w^2,0,0),
+Y_1=(0,1,0), Y_w=(0,w,0), Y_{w^2}=(0,w^2,0)
+```
+
+are involutions. Their commutators are `[X_a,Y_b]=(0,0,a b)`. In particular
+
+```text
+Z_1=[X_1,Y_1]=(0,0,1),
+Z_w=[X_w,Y_1]=(0,0,w),
+Z_{w^2}=[X_w,Y_w]=(0,0,w^2).
+```
+
+Also `[X_{w^2},Y_{w^2}]=(0,0,w)=Z_w`, because `w^2 w^2=w`.
+
+Work in the matrix ring over `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,
+```
+
+with `g` one of the six labels. Each call costs one. There is no free clean role, copy, erase, or uncharged inverse. A scalar factor from `GL_r(F_2)` may be inserted without charge. Conjugation preserves the set of rank-one idempotents. Augmentation `F_2[H] -> F_2` kills every paid factor, since `[g]+[1]` has even weight, and it kills the target below, so the residual scalar on a realizing word is the identity. It is enough to bound pure words in the paid factors.
+
+The target is
+
+```text
+diag([Z_1], [Z_w], [Z_{w^2}], [1], ..., [1])
+```
+
+on `r` registers. Every realizing word has length at least **12**. Two explicit words attain 12. One of them uses both `X_{w^2}` and `Y_{w^2}`.
+
+The four-label count on `{X_1,X_w,Y_1,Y_w}` is a different hypothesis. Its complementary-summand split uses coefficients in `{1,w}` only. The coefficient `w^2=(1,1)` meets both `F_2` coordinates, so that split does not prove the six-label statement. The argument below replaces it.
+
+## Two attaining words
+
+Coordinate projectors `E_{tt}` commute across `t`. On a single coordinate the address multiplier is the left product of the labels in time order. Both schedules below are four calls per register.
+
+Mixed word, using `X_{w^2}` and only `Y_1`:
+
+```text
+E_00: X_1, Y_1, X_1, Y_1          = Z_1
+E_11: X_w, Y_1, X_w, Y_1          = Z_w
+E_22: X_{w^2}, Y_1, X_{w^2}, Y_1  = Z_{w^2}
+```
+
+The third block is `[X_{w^2},Y_1]=(0,0,w^2)`.
+
+Both-new word, using `X_{w^2}` and `Y_{w^2}`:
+
+```text
+E_00: X_1, Y_1, X_1, Y_1                = Z_1
+E_11: X_{w^2}, Y_{w^2}, X_{w^2}, Y_{w^2} = Z_w
+E_22: X_w, Y_w, X_w, Y_w                = Z_{w^2}
+```
+
+Each word has `n_X=6` and `n_Y=6`. Spectators stay at the identity because their projector rows are zero.
+
+## Nilpotent shape
+
+Realize `H` by its defining matrices and expand `F_4` through the regular representation `F_4 -> M_2(F_2)`. Multiplication by `1`, `w`, and `w^2` becomes
+
+```text
+I_2,  [[0,1],[1,1]],  [[1,1],[1,0]].
+```
+
+All three matrices are symmetric, and the last one equals `I_2+M_w`. Each group element becomes a `6×6` binary matrix. For an axis label the nilpotent `E(g)=ρ(g)+I` has a single off-diagonal block: an `X`-label occupies rows `0..1`, columns `2..3`; a `Y`-label occupies rows `2..3`, columns `4..5`. Consequently, for every pair among the six labels,
+
+- `E(X)E(Y)` is the pure corner `m_α m_β` in rows `0..1`, columns `4..5`;
+- every other length-two product is zero;
+- every product of three nilpotents is zero.
+
+The same block arithmetic, transposed, holds for `σ(g)=ρ(g^{-1})^T=ρ(g)^T`. The only nonzero length-two products are `E^σ(Y)E^σ(X)`, and they sit in rows `4..5`, columns `0..1`.
+
+For calls in time order `g_1,...,g_n` with idempotents `N_k`,
+
+```text
+ρ_*(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 quadratic sum is supported on pairs where call `i` is `Y`-type and later call `j` is `X`-type. A term `N_j N_i=u_j(v_j·u_i)v_i^T` has image in `span{u_X}` and row space in `span{v_Y}`. The contragredient expansion swaps the roles: image in `span{u_Y}` and row space in `span{v_X}`.
+
+The target corner is `m_1` on register 0, `m_w` on register 1, and `m_{w^2}` on register 2. In the basis `{m_1,m_w}` that is `P=E_{00}+E_{22}` and `Q=E_{11}+E_{22}`. Both images, and both row spaces, equal `span{e_0,e_1,e_2}`. Therefore every realizing word satisfies
+
+```text
+dim span{u_X} >= 3,  dim span{v_Y} >= 3,
+dim span{u_Y} >= 3,  dim span{v_X} >= 3.
+```
+
+The linear blocks must vanish. With `S_α` the sum of the `X`-call idempotents of coefficient `α`, the regular representation gives the two independent equations `S_1+S_{w^2}=0` and `S_w+S_{w^2}=0`. The same holds for `Y`.
+
+## Diagonal-lift lemma
+
+Write `α=α_0·1+α_1·w` in `F_2`. Form the `2r×n` matrix `U` whose columns are `(α_0 u, α_1 u)`, and the `n×r` matrix `V` whose rows are `v^T`. The linear equations are exactly `UV=0`, so
+
+```text
+n >= rank(U) + rank(V).
+```
+
+`rank(V)` is `dim span{v}`. The new point is that `w^2` does not let `dim span{u}` exceed `rank(U)`.
+
+Let `L` be the column space of `U` inside `F_2^r ⊕ F_2^r`. Define `φ(x,y)=x+y` and let `Δ={(u,u)}`. Then `Δ` sits inside `ker φ`. Every type-`1` or type-`w` column `c` satisfies `φ(c)=u`, and every type-`w^2` column is `(u,u)`. Hence
+
+```text
+span{u} ⊆ φ(L) + π_0(L ∩ Δ),
+```
+
+where `π_0` reads the first summand. Dimension counting gives
+
+```text
+dim φ(L) + dim(L ∩ Δ)
+  = dim L - dim(L ∩ ker φ) + dim(L ∩ Δ)
+  <= dim L,
+```
+
+because `L ∩ Δ ⊆ L ∩ ker φ`. Therefore
+
+```text
+dim span{u} <= rank(U).
+```
+
+Adding the two rank inequalities,
+
+```text
+n_X >= dim span{u_X} + dim span{v_X} >= 6,
+n_Y >= dim span{u_Y} + dim span{v_Y} >= 6.
+```
+
+Every realizing word costs at least 12, for every finite `r>=3`, with arbitrary restored spectators. Both words meet the bound.
+
+The separated `{1,w}` span is not this count. On the mixed word the `X_1` and `X_w` shadows span only `span{e_0,e_1}`, dimension 2. The third direction is the `w^2` column `(e_2,e_2)`. It is invisible to a split that discards `w^2`, and it still costs one dimension of `L`. A direct sum of the three pure-type subspaces of `L` can overcount: `span{(e_0,0),(0,e_0)}` has dimension 2 while the three axis spaces each contribute dimension 1. That overcount is not used.
+
+The same packing cannot hide three independent shadows in a rank-2 lift. In `r=3` every shadow has dimension at most 3, so a violating family would contain three pure columns with independent shadows and lift rank at most 2. All `C(21,3)=1330` triples, and all `82160` subsets of size at most 6, satisfy `dim span{u} <= rank(U)`.
+
+## What is not claimed
+
+This does not reprove the four-label minimum, and it does not use the fourteen-call composite. It does not allow non-idempotent factors, non-axis letters, or a bit-supplier embedding. `12α` is a formal per-call price in this alphabet. The selected decimal remains `0.001672660197076918`.

research/ut3-f4-w2-lift-obstruction/README.md

@@ -0,0 +1,67 @@
+# Six axis labels still take twelve calls for one UT3(F4) triple
+
+**Scoped formal minimum; no new kappa.** In `F_2[UT_3(F_4)]`, every word in the six involutions
+
+```text
+X_1, X_w, X_{w^2}, Y_1, Y_w, Y_{w^2}
+```
+
+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 coefficient `w^2=(1,1)` mixes the two `F_2` summands, so the four-label complementary split does not apply. The diagonal-lift lemma replaces it: the output shadows of `{1,w,w^2}` still satisfy `dim span{u} <= rank(U)`, and both letter classes need six calls. Two twelve-call words attain the endpoint. One uses `X_{w^2}` with `Y_1` only. The other uses both `X_{w^2}` and `Y_{w^2}`. The selected decimal stays `0.001672660197076918`.
+
+On the mixed word the `{1,w}` shadows span only two coordinates. That is the sense in which the older split is blind. The `w^2` column supplies the third direction and still consumes one lift dimension. 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 | What is new |
+|---|---:|---|
+| Mixed word `[X_1,Y_1]`, `[X_w,Y_1]`, `[X_{w^2},Y_1]` | 12 | uses `X_{w^2}` |
+| Both-new word `[X_1,Y_1]`, `[X_{w^2},Y_{w^2}]`, `[X_w,Y_w]` | 12 | uses both new labels |
+| Diagonal-lift floor on six labels | 12 | `dim span{u} <= rank(U)` |
+
+At a positive per-call price `α` the sharp bill is `12α`. Adjoining the two `w^2` labels does not improve it.
+
+## Reproduce
+
+From the repository root, standard-library Python 3.12:
+
+```sh
+python3 -I -B research/ut3-f4-w2-lift-obstruction/verify.py
+python3 -I -O -Werror -B research/ut3-f4-w2-lift-obstruction/verify.py
+python3 -I -B research/ut3-f4-w2-lift-obstruction/independent.py
+python3 -I -B research/ut3-f4-w2-lift-obstruction/test_package.py
+python3 -B scripts/research_package.py --package research/ut3-f4-w2-lift-obstruction
+```
+
+Expected verifier line:
+
+```text
+PASS_UT3_F4_W2_LIFT six_label_minimum=12 labels=6 mixed_word=12 both_new_labels=12 nX=6 nY=6 blind_span=2 lift_rank=3 shadow_subsets=82160 spectator=1 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 four-label exact minimum, including its disjoint commutator schedule and its `n_X>=6` split, is a prior result on a smaller alphabet. This note answers the question that result left open: the mixed summand does not produce a shorter legal word. The separated span on the mixed witness is 2, which is why that earlier split cannot be cited for this alphabet.
+
+Not claimed: a reprint of the four-label theorem; a fourteen-call composite; a non-idempotent shortening; 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 rank-one calls that are not idempotent reduce this six-label triple below 12? Keep the six axis labels, drop `N^2=N`, and test whether a nilpotent factor can feed a three-dimensional corner. The blocker is that `v·u=0` kills every quadratic scalar `v_X·u_Y`, so the present normal form does not admit those factors.
+
+Can one of these twelve formal calls be realized in a pinned bit supplier below one rank-one complete price? Charge frame changes, hosting, restoration, and dispatch for either twelve-call word. The blocker is the absence of a legal physical realization.
+
+## Credit
+
+The two-register minimum and the open three-output question are Cinna Davis's UT3(F4) central-pair note. The four-label exact minimum that posed the `w^2` question is the dependent-central-triple note. The rank-one idempotent register model follows the eumemic / woklerx address-call lineage used there.
+
+Prepared by Wentao Li with substantial AI assistance. No independent human or proof-assistant review is claimed. Apache-2.0.

research/ut3-f4-w2-lift-obstruction/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "input",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    }
+  ]
+}

research/ut3-f4-w2-lift-obstruction/TASK.json

@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 3,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "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 that adjoining the axis involutions X_{w^2} and Y_{w^2} does not reduce the paid-call length of diag([Z_1],[Z_w],[Z_{w^2}]) below 12 in F2[UT3(F4)].",
+  "scope_change_reason": "The catalogue card asks for a selected-interface formal lemma. The operative gap is the six-label question left by the four-label UT3(F4) triple: w^2=(1,1) mixes the two F2 summands, so that split no longer applies. This package proves the diagonal-lift obstruction on the enlarged alphabet. It is a side result 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. The enlarged formal alphabet does not undercut the twelve-call bill, and kappa is unchanged.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the diagonal-lift inequality, both twelve-call words, and the r=3 pure-column census are checked. Do not search non-idempotent factors or physical embeddings.",
+  "outcome": "completed",
+  "evidence": "PASS_UT3_F4_W2_LIFT six_label_minimum=12 labels=6 mixed_word=12 both_new_labels=12 blind_span=2 lift_rank=3 shadow_subsets=82160.",
+  "author": "Wentao Li",
+  "ai_assistance": "Substantial AI assistance for the diagonal-lift argument, independent replay, and write-up.",
+  "open_questions": [
+    {
+      "question": "Can rank-one calls that are not idempotent reduce this six-label triple below 12?",
+      "why_it_matters": "The lift inequality uses v·u=1 only to stay inside the paid idempotent model. A nilpotent rank-one factor is a different alphabet.",
+      "first_step": "Keep the six axis labels and replace N^2=N by rank(N)=1 with N^2=0, then test whether the corner image can meet dimension 3 with fewer than six calls on one side.",
+      "blocked_by": "The expansion scalar v_X·u_Y vanishes on every purely nilpotent pair, so a new normal form is required before any shorter word is legal."
+    },
+    {
+      "question": "Does one of these twelve formal calls embed in a pinned bit supplier below one rank-one complete price?",
+      "why_it_matters": "Only a legal physical realization can move a supplier bill. The six-label count is still formal.",
+      "first_step": "Charge frame changes, hosting, restoration, and dispatch for either twelve-call word at the w=3,k=1 boundary.",
+      "blocked_by": "No legal physical realization is supplied. The lift inequality does not provide one."
+    }
+  ]
+}

research/ut3-f4-w2-lift-obstruction/VERIFY.json

@@ -0,0 +1,53 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/selected-result.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Six-label group law, nilpotent and contragredient tables, both twelve-call words, spectator and omissions, diagonal-lift census, read-only receipt, duplicate JSON keys."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-Werror",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Same gates under -O -Werror. need() is not stripped."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/independent.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Separate frozenset convolution of both mixed words, the blind span, and the phi-diagonal lift inequality."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/test_package.py"
+      ],
+      "timeout_seconds": 240,
+      "checks": "Replays verify under -O -Werror, independent, and a duplicate-key rejection."
+    }
+  ]
+}