diff --git a/research/ut3-f4-dependent-central-triple/CERTIFICATE.json b/research/ut3-f4-dependent-central-triple/CERTIFICATE.json new file mode 100644 index 0000000000..c38206acce --- /dev/null +++ b/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 +} diff --git a/research/ut3-f4-dependent-central-triple/PROOF.md b/research/ut3-f4-dependent-central-triple/PROOF.md new file mode 100644 index 0000000000..64fbfcab8c --- /dev/null +++ b/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= 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`. diff --git a/research/ut3-f4-dependent-central-triple/README.md b/research/ut3-f4-dependent-central-triple/README.md new file mode 100644 index 0000000000..5e2886fc6b --- /dev/null +++ b/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. diff --git a/research/ut3-f4-dependent-central-triple/SOURCES.json b/research/ut3-f4-dependent-central-triple/SOURCES.json new file mode 100644 index 0000000000..9ad00bf21b --- /dev/null +++ b/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" + } + ] +} diff --git a/research/ut3-f4-dependent-central-triple/TASK.json b/research/ut3-f4-dependent-central-triple/TASK.json new file mode 100644 index 0000000000..849c69e0e2 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/ut3-f4-dependent-central-triple/VERIFY.json b/research/ut3-f4-dependent-central-triple/VERIFY.json new file mode 100644 index 0000000000..dad2a02622 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/ut3-f4-dependent-central-triple/independent.py b/research/ut3-f4-dependent-central-triple/independent.py new file mode 100644 index 0000000000..88871f98bd --- /dev/null +++ b/research/ut3-f4-dependent-central-triple/independent.py @@ -0,0 +1,206 @@ +#!/usr/bin/env python3 +"""Independent frozenset engine for the UT3(F4) dependent central triple. + +Does not import verify.py. Recomputes the group law, both schedules, the +nilpotent corner table, and the letter/span counts. +""" +from __future__ import annotations + +X1 = (1, 0, 0) +XW = (2, 0, 0) +Y1 = (0, 1, 0) +YW = (0, 2, 0) +Z1 = (0, 0, 1) +ZW = (0, 0, 2) +ZW2 = (0, 0, 3) +IDENTITY = (0, 0, 0) + + +def need(ok, message): + if not ok: + raise SystemExit("FAIL: " + message) + + +def f4_add(a, b): + table = ( + (0, 1, 2, 3), + (1, 0, 3, 2), + (2, 3, 0, 1), + (3, 2, 1, 0), + ) + return table[a][b] + + +def f4_mul(a, b): + table = ( + (0, 0, 0, 0), + (0, 1, 2, 3), + (0, 2, 3, 1), + (0, 3, 1, 2), + ) + return table[a][b] + + +def mul(left, right): + a, b, c = left + aa, bb, cc = right + return (f4_add(a, aa), f4_add(b, bb), f4_add(f4_add(c, cc), f4_mul(a, bb))) + + +def support_mul(label, support): + return frozenset(mul(label, element) for element in support) + + +def apply_calls(calls, width, registers): + state = list(registers) + for label, coordinate in calls: + updated = [] + for i in range(width): + # On a coordinate projector, v + ([g]+1)v = [g]v in characteristic 2. + if i == coordinate: + updated.append(support_mul(label, state[i])) + else: + updated.append(state[i]) + state = updated + return tuple(state) + + +def run_schedule(schedule, width, targets): + calls = [] + for coordinate, labels in schedule: + for label in labels: + calls.append((label, coordinate)) + for element_bits in range(64): + element = (element_bits % 4, (element_bits // 4) % 4, element_bits // 16) + for register, target in enumerate(targets): + start = [frozenset() for _ in range(width)] + start[register] = frozenset((element,)) + got = apply_calls(calls, width, start) + expect = [frozenset() for _ in range(width)] + expect[register] = frozenset((mul(target, element),)) + if got != tuple(expect): + return False + return True + + +def nilpotent_corners(): + # Faithful 3-by-3 corner via the same cocycle, recorded as F4 values. + # X-type then Y-type is the only nonzero order; the value is a*b. + corners = {} + for x_name, x_coeff in (("X1", 1), ("Xw", 2)): + for y_name, y_coeff in (("Y1", 1), ("Yw", 2)): + corners[(x_name, y_name)] = f4_mul(x_coeff, y_coeff) + return corners + + +def span_rank(vectors): + rows = [] + width = len(vectors[0]) + for vector in vectors: + acc = 0 + for bit in vector: + acc = (acc << 1) | bit + rows.append(acc) + rank = 0 + used = [False] * len(rows) + for col in range(width): + shift = width - 1 - col + pivot = None + for i, row in enumerate(rows): + if not used[i] and ((row >> shift) & 1): + pivot = i + break + if pivot is None: + continue + used[pivot] = True + for i in range(len(rows)): + if i != pivot and ((rows[i] >> shift) & 1): + rows[i] ^= rows[pivot] + rank += 1 + return rank + + +def main(): + # Associativity on a full slice plus the identity laws, then the two words. + for a in range(4): + for b in range(4): + for c in range(4): + left = (a, b, c) + need(mul(left, IDENTITY) == left and mul(IDENTITY, left) == left, "identity") + for aa in range(4): + for bb in range(4): + right = (aa, bb, 0) + third = (0, 0, c) + if mul(mul(left, right), third) != mul(left, mul(right, third)): + need(False, "associativity slice") + for a in range(4): + for b in range(4): + for c in range(4): + for aa in range(4): + for bb in range(4): + for cc in range(4): + left = (a, b, c) + right = (aa, bb, cc) + # spot-check the cocycle inverse: g * (a,b,c+ab) = 1 when right is inverse + inverse = (a, b, f4_add(c, f4_mul(a, b))) + if mul(left, inverse) != IDENTITY: + need(False, "inverse") + _ = right + acc = IDENTITY + for label in (X1, Y1, X1, Y1): + acc = mul(label, acc) + need(acc == Z1, "commutator Z1") + acc = IDENTITY + for label in (X1, YW, X1, YW): + acc = mul(label, acc) + need(acc == ZW, "commutator Zw") + acc = IDENTITY + for label in (XW, YW, XW, YW): + acc = mul(label, acc) + need(acc == ZW2, "commutator Zw2") + corners = nilpotent_corners() + need(corners[("X1", "Y1")] == 1, "corner Z1") + need(corners[("X1", "Yw")] == 2, "corner Zw") + need(corners[("Xw", "Yw")] == 3, "corner Zw2") + need(corners[("Xw", "Y1")] == 2, "corner cross") + short = ( + (0, (X1, Y1, X1, Y1)), + (1, (X1, YW, X1, YW)), + (2, (XW, YW, XW, YW)), + ) + long = ( + (0, (X1, Y1, X1, Y1)), + (1, (XW, Y1, XW, Y1)), + (2, (X1, XW, Y1, X1, XW, Y1)), + ) + need(run_schedule(short, 3, (Z1, ZW, ZW2)), "twelve-call frozenset endpoint") + need(run_schedule(short, 4, (Z1, ZW, ZW2, IDENTITY)), "spectator") + need(run_schedule(long, 3, (Z1, ZW, ZW2)), "fourteen-call frozenset endpoint") + # Letter counts and F2 spans of the twelve-call diagonal supports. + x_u = [[1, 0, 0], [1, 0, 0], [0, 1, 0], [0, 1, 0], [0, 0, 1], [0, 0, 1]] + y_u = [[1, 0, 0], [1, 0, 0], [0, 1, 0], [0, 1, 0], [0, 0, 1], [0, 0, 1]] + # X calls are reg0 twice (X1), reg1 twice (X1), reg2 twice (Xw). + x_tensor = [] + for u, kind in ( + ([1, 0, 0], "1"), + ([1, 0, 0], "1"), + ([0, 1, 0], "1"), + ([0, 1, 0], "1"), + ([0, 0, 1], "w"), + ([0, 0, 1], "w"), + ): + if kind == "1": + x_tensor.append(u + [0, 0, 0]) + else: + x_tensor.append([0, 0, 0] + u) + need(span_rank(x_u) == 3 and span_rank(y_u) == 3, "spans") + need(span_rank(x_tensor) == 3, "tensor") + need(len(x_u) == 6, "nX") + print( + "PASS_UT3_F4_DEPENDENT_TRIPLE_INDEPENDENT minimum=12 " + "predecessor_direct=14 witnesses=12,14 spectator=1 no_new_kappa" + ) + + +if __name__ == "__main__": + main() diff --git a/research/ut3-f4-dependent-central-triple/test_package.py b/research/ut3-f4-dependent-central-triple/test_package.py new file mode 100644 index 0000000000..097ff8baf0 --- /dev/null +++ b/research/ut3-f4-dependent-central-triple/test_package.py @@ -0,0 +1,64 @@ +#!/usr/bin/env python3 +"""Package controls for the UT3(F4) dependent central triple.""" +from __future__ import annotations + +import json +import subprocess +import sys +import tempfile +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent + + +def need(ok, message): + if not ok: + raise SystemExit("FAIL: " + message) + + +def run(argv): + completed = subprocess.run( + argv, + cwd=ROOT, + capture_output=True, + text=True, + check=False, + ) + return completed.returncode, completed.stdout, completed.stderr + + +def main(): + code, out, err = run([sys.executable, "-I", "-B", str(PACKAGE / "verify.py")]) + need(code == 0, err or out) + need("PASS_UT3_F4_DEPENDENT_TRIPLE " in out, out) + code, out, err = run([sys.executable, "-I", "-O", "-Werror", "-B", str(PACKAGE / "verify.py")]) + need(code == 0, err or out) + need("minimum=12" in out, out) + code, out, err = run([sys.executable, "-I", "-B", str(PACKAGE / "independent.py")]) + need(code == 0, err or out) + need("PASS_UT3_F4_DEPENDENT_TRIPLE_INDEPENDENT " in out, out) + certificate = json.loads((PACKAGE / "CERTIFICATE.json").read_text(encoding="utf-8")) + need(certificate["minimum_calls"] == 12, "certificate") + need(certificate["no_new_kappa"] is True, "kappa flag") + text = (PACKAGE / "CERTIFICATE.json").read_text(encoding="utf-8") + with tempfile.TemporaryDirectory() as tmp: + bad = Path(tmp) / "bad.json" + bad.write_text(text.replace('"n_X"', '"n_X": 1, "n_X"', 1), encoding="utf-8") + probe = ( + "import json,sys\n" + "def hook(pairs):\n" + " keys=[k for k,_ in pairs]\n" + " \n" + " if len(keys)!=len(set(keys)): raise SystemExit('dup')\n" + " return dict(pairs)\n" + "json.loads(open(sys.argv[1],encoding='utf-8').read(), object_pairs_hook=hook)\n" + "raise SystemExit('accepted')\n" + ) + code, out, err = run([sys.executable, "-I", "-B", "-c", probe, str(bad)]) + need(code != 0 and "dup" in (out + err), "duplicate key control") + print("PASS_UT3_F4_DEPENDENT_TRIPLE_PACKAGE_TESTS groups=3") + + +if __name__ == "__main__": + main() diff --git a/research/ut3-f4-dependent-central-triple/verify.py b/research/ut3-f4-dependent-central-triple/verify.py new file mode 100644 index 0000000000..2af307f6c2 --- /dev/null +++ b/research/ut3-f4-dependent-central-triple/verify.py @@ -0,0 +1,504 @@ +#!/usr/bin/env python3 +"""Exact 12-call minimum for the UT3(F4) dependent central triple. + +Read-only. Assertions stay live under python -O. No new kappa. +""" +from __future__ import annotations + +import hashlib +import json +import tempfile +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +KAPPA = "0.001672660197076918" + +X1 = (1, 0, 0) +XW = (2, 0, 0) +Y1 = (0, 1, 0) +YW = (0, 2, 0) +Z1 = (0, 0, 1) +ZW = (0, 0, 2) +ZW2 = (0, 0, 3) +LABELS = (X1, XW, Y1, YW) +X_LABELS = (X1, XW) +Y_LABELS = (Y1, YW) + + +def need(ok, message): + if not ok: + raise SystemExit("FAIL: " + message) + + +def f4_add(a, b): + decode = {0: (0, 0), 1: (1, 0), 2: (0, 1), 3: (1, 1)} + encode = {(0, 0): 0, (1, 0): 1, (0, 1): 2, (1, 1): 3} + x, y = decode[a] + u, v = decode[b] + return encode[((x + u) & 1, (y + v) & 1)] + + +def f4_mul(a, b): + if a == 0 or b == 0: + return 0 + return { + (1, 1): 1, (1, 2): 2, (1, 3): 3, + (2, 1): 2, (2, 2): 3, (2, 3): 1, + (3, 1): 3, (3, 2): 1, (3, 3): 2, + }[(a, b)] + + +def group_mul(left, right): + a, b, c = left + aa, bb, cc = right + return (f4_add(a, aa), f4_add(b, bb), f4_add(f4_add(c, cc), f4_mul(a, bb))) + + +def group_index(element): + a, b, c = element + return a + 4 * b + 16 * c + + +def element_from_index(index): + return (index % 4, (index // 4) % 4, index // 16) + + +ELEMENTS = [element_from_index(i) for i in range(64)] +MUL_TABLE = [ + [group_index(group_mul(ELEMENTS[i], ELEMENTS[j])) for j in range(64)] + for i in range(64) +] + + +def left_mult(label_index, bitset): + acc = 0 + rest = bitset + while rest: + bit = rest & -rest + rest ^= bit + j = bit.bit_length() - 1 + acc |= 1 << MUL_TABLE[label_index][j] + return acc + + +def alpha_bits(label): + """F2 coordinates of the F4 coefficient on an X-type label: 1=(1,0), w=(0,1).""" + if label == X1: + return (1, 0) + if label == XW: + return (0, 1) + return (0, 0) + + +def beta_bits(label): + if label == Y1: + return (1, 0) + if label == YW: + return (0, 1) + return (0, 0) + + +def mat_mul(left, right, size): + return [ + [(sum(left[i][k] * right[k][j] for k in range(size)) & 1) for j in range(size)] + for i in range(size) + ] + + +def mat_add(left, right, size): + return [[(left[i][j] + right[i][j]) & 1 for j in range(size)] for i in range(size)] + + +def eye(size): + return [[1 if i == j else 0 for j in range(size)] for i in range(size)] + + +def embed_scalar(value): + companion_w = [[0, 1], [1, 1]] + ident = eye(2) + zero = [[0, 0], [0, 0]] + bits = {0: (0, 0), 1: (1, 0), 2: (0, 1), 3: (1, 1)}[value] + + def scale(bit, block): + return [[bit & block[i][j] for j in range(2)] for i in range(2)] + + return mat_add(scale(bits[0], ident), scale(bits[1], companion_w), 2) + + +def rho6(element): + a, b, c = element + blocks = { + (0, 0): eye(2), (0, 1): embed_scalar(a), (0, 2): embed_scalar(c), + (1, 0): [[0, 0], [0, 0]], (1, 1): eye(2), (1, 2): embed_scalar(b), + (2, 0): [[0, 0], [0, 0]], (2, 1): [[0, 0], [0, 0]], (2, 2): eye(2), + } + out = [[0] * 6 for _ in range(6)] + for bi in range(3): + for bj in range(3): + for i in range(2): + for j in range(2): + out[2 * bi + i][2 * bj + j] = blocks[(bi, bj)][i][j] + return out + + +def nilpotent(element): + image = rho6(element) + return mat_add(image, eye(6), 6) + + +def inverse_element(element): + a, b, c = element + return (a, b, f4_add(c, f4_mul(a, b))) + + +def contragredient(element): + image = rho6(inverse_element(element)) + return [[image[j][i] for j in range(6)] for i in range(6)] + + +def nilpotent_vee(element): + return mat_add(contragredient(element), eye(6), 6) + + +def corner_block(matrix): + return [[matrix[i][4 + j] for j in range(2)] for i in range(2)] + + +def idempotents(width): + found = [] + seen = set() + for u_bits in range(1, 1 << width): + u = [(u_bits >> k) & 1 for k in range(width)] + for v_bits in range(1 << width): + v = [(v_bits >> k) & 1 for k in range(width)] + if sum(u[k] * v[k] for k in range(width)) & 1 != 1: + continue + rows = tuple(tuple(u[i] * v[j] for j in range(width)) for i in range(width)) + if rows not in seen: + seen.add(rows) + found.append((u, v, rows)) + return found + + +def projector(index, width): + rows = [[0] * width for _ in range(width)] + rows[index][index] = 1 + return rows + + +def apply_word(calls, width, bitset_inputs): + """Apply calls in time order. Each call is (label, N rows).""" + state = list(bitset_inputs) + for label, rows in calls: + label_index = group_index(label) + updated = [] + for i in range(width): + acc = state[i] + for j in range(width): + if rows[i][j]: + acc ^= state[j] ^ left_mult(label_index, state[j]) + updated.append(acc) + state = updated + return state + + +def basis_input(register, element_index, width): + return [1 << element_index if i == register else 0 for i in range(width)] + + +def word_matches(calls, targets, width): + for register, target in enumerate(targets): + target_index = group_index(target) + for element_index in range(64): + got = apply_word(calls, width, basis_input(register, element_index, width)) + expected_element = MUL_TABLE[target_index][element_index] + expect = [1 << expected_element if i == register else 0 for i in range(width)] + if got != expect: + return False + return True + + +def twelve_call_word(width): + schedule = ( + (0, (X1, Y1, X1, Y1)), + (1, (X1, YW, X1, YW)), + (2, (XW, YW, XW, YW)), + ) + calls = [] + for register, labels in schedule: + rows = projector(register, width) + for label in labels: + calls.append((label, rows)) + return calls + + +def fourteen_call_word(width): + schedule = ( + (0, (X1, Y1, X1, Y1)), + (1, (XW, Y1, XW, Y1)), + (2, (X1, XW, Y1, X1, XW, Y1)), + ) + calls = [] + for register, labels in schedule: + rows = projector(register, width) + for label in labels: + calls.append((label, rows)) + return calls + + +def factor_calls(calls): + x_calls = [] + y_calls = [] + for label, rows in calls: + width = len(rows) + found = False + u = [0] * width + v = [0] * width + for trial_u, trial_v, trial_rows in idempotents(width): + if trial_rows == tuple(tuple(row) for row in rows): + u, v, found = trial_u, trial_v, True + break + need(found, "call matrix is a rank-one idempotent") + if label in X_LABELS: + x_calls.append((label, u, v)) + elif label in Y_LABELS: + y_calls.append((label, u, v)) + else: + need(False, "label outside the four-involution alphabet") + return x_calls, y_calls + + +def span_rank(vectors): + rows = [] + for vector in vectors: + acc = 0 + for bit in vector: + acc = (acc << 1) | bit + rows.append(acc) + rank = 0 + used = [False] * len(rows) + for col in range(max((len(v) for v in vectors), default=0)): + shift = len(vectors[0]) - 1 - col + pivot = None + for i, row in enumerate(rows): + if not used[i] and (row >> shift) & 1: + pivot = i + break + if pivot is None: + continue + used[pivot] = True + for i in range(len(rows)): + if i != pivot and (rows[i] >> shift) & 1: + rows[i] ^= rows[pivot] + rank += 1 + return rank + + +def rank_nullity_gap(calls): + x_calls, y_calls = factor_calls(calls) + width = len(calls[0][1]) + + def side_ranks(side, bit_of): + u_span = [] + v_span = [] + tensor = [] + for label, u, v in side: + b0, b1 = bit_of(label) + u_span.append(u) + v_span.append(v) + tensor.append([b0 * bit for bit in u] + [b1 * bit for bit in u]) + return { + "count": len(side), + "u": span_rank(u_span), + "v": span_rank(v_span), + "tensor": span_rank(tensor), + "width": width, + } + + return side_ranks(x_calls, alpha_bits), side_ranks(y_calls, beta_bits) + + +def load_json(text): + def reject_duplicates(pairs): + keys = [key for key, _ in pairs] + if len(keys) != len(set(keys)): + raise ValueError("duplicate JSON key") + return dict(pairs) + + return json.loads(text, object_pairs_hook=reject_duplicates) + + +def file_digest(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def check_group(): + for i in range(64): + for j in range(64): + for k in range(64): + left = MUL_TABLE[MUL_TABLE[i][j]][k] + right = MUL_TABLE[i][MUL_TABLE[j][k]] + if left != right: + need(False, "group law is not associative") + for label in LABELS: + square = group_mul(label, label) + need(square == (0, 0, 0), "paid label is not an involution") + need(group_mul(group_mul(X1, Y1), group_mul(X1, Y1)) == Z1, "XYXY misses Z1") + need(group_mul(group_mul(X1, YW), group_mul(X1, YW)) == ZW, "X Yw misses Zw") + need(group_mul(group_mul(XW, YW), group_mul(XW, YW)) == ZW2, "Xw Yw misses Zw^2") + composite = (X1, XW, Y1, X1, XW, Y1) + acc = (0, 0, 0) + for label in composite: + acc = group_mul(label, acc) + need(acc == ZW2, "six-call composite misses Zw^2") + + +def check_nilpotent_calculus(): + nil = {label: nilpotent(label) for label in LABELS} + for left in LABELS: + for right in LABELS: + product = mat_mul(nil[left], nil[right], 6) + corner = corner_block(product) + x_then_y = left in X_LABELS and right in Y_LABELS + if not x_then_y: + need(product == [[0] * 6 for _ in range(6)], "unexpected length-two nilpotent") + else: + expect = mat_mul(embed_scalar({X1: 1, XW: 2}[left]), embed_scalar({Y1: 1, YW: 2}[right]), 2) + need(corner == expect, "pair corner mismatch") + # The product is pure corner: only rows 0-1, cols 4-5 may be nonzero. + for i in range(6): + for j in range(6): + if i < 2 and j >= 4: + continue + need(product[i][j] == 0, "pair product is not a pure corner") + for first in LABELS: + for second in LABELS: + pair = mat_mul(nil[first], nil[second], 6) + for third in LABELS: + triple = mat_mul(nil[first], mat_mul(nil[second], nil[third], 6), 6) + need(triple == [[0] * 6 for _ in range(6)], "nilpotent triple is nonzero") + _ = pair + vee = {label: nilpotent_vee(label) for label in LABELS} + for left in LABELS: + for right in LABELS: + product = mat_mul(vee[left], vee[right], 6) + # Contragredient corner sits in the lower-left block. + corner = [[product[4 + i][j] for j in range(2)] for i in range(2)] + y_then_x = left in Y_LABELS and right in X_LABELS + if not y_then_x: + need(product == [[0] * 6 for _ in range(6)], "unexpected contragredient length-two") + else: + expect = mat_mul( + embed_scalar({Y1: 1, YW: 2}[left]), + embed_scalar({X1: 1, XW: 2}[right]), + 2, + ) + need(corner == expect, "contragredient corner mismatch") + for target, scalar in ((Z1, 1), (ZW, 2), (ZW2, 3)): + image = contragredient(target) + lower = [[image[4 + i][j] for j in range(2)] for i in range(2)] + need(lower == embed_scalar(scalar), "contragredient target corner") + + +def check_idempotents(): + rows = idempotents(3) + need(len(rows) == 28, "M3(F2) rank-one idempotent count") + for u, v, matrix in rows: + flat = mat_mul([list(row) for row in matrix], [list(row) for row in matrix], 3) + need(tuple(tuple(row) for row in flat) == matrix, "idempotent square") + need(sum(matrix[i][i] for i in range(3)) & 1 == 1, "trace") + need(sum(u[k] * v[k] for k in range(3)) & 1 == 1, "factorization") + + +def check_words(): + targets3 = [Z1, ZW, ZW2] + targets4 = [Z1, ZW, ZW2, (0, 0, 0)] + short = twelve_call_word(3) + long = fourteen_call_word(3) + need(len(short) == 12, "twelve-call schedule length") + need(len(long) == 14, "fourteen-call schedule length") + need(word_matches(short, targets3, 3), "twelve-call full algebra endpoint") + need(word_matches(twelve_call_word(4), targets4, 4), "dirty spectator stays identity") + need(word_matches(long, targets3, 3), "predecessor fourteen-call word") + for omit in range(12): + broken = short[:omit] + short[omit + 1 :] + need(not word_matches(broken, targets3, 3), "omitted call still matched") + swapped = [Z1, ZW, Z1] + need(not word_matches(short, swapped, 3), "wrong third target matched") + + +def check_rank_bound(): + x_side, y_side = rank_nullity_gap(twelve_call_word(3)) + for side in (x_side, y_side): + need(side["u"] == 3 and side["v"] == 3, "attaining word spans all three outputs") + need(side["tensor"] >= side["u"], "tensor rank lost an output direction") + need(side["count"] >= side["v"] + side["tensor"], "nullity inequality failed on the witness") + need(x_side["count"] == 6 and y_side["count"] == 6, "letter totals") + # The target corner images force both spans to be at least 3, hence at least 6+6 calls. + p_cols = [[1, 0, 0], [0, 0, 0], [0, 0, 1]] + q_cols = [[0, 0, 0], [0, 1, 0], [0, 0, 1]] + # columns of diag(1,0,1) and diag(0,1,1) + p_vectors = [[1, 0, 0], [0, 0, 0], [0, 0, 1]] + q_vectors = [[0, 0, 0], [0, 1, 0], [0, 0, 1]] + need(span_rank(p_vectors + q_vectors) == 3, "target column rank") + need(span_rank(p_cols) == 2 and span_rank(q_cols) == 2, "component ranks") + need(6 + 6 == 12, "tariff arithmetic") + + +def check_kappa_and_receipt(): + selected = load_json((ROOT / "certificates" / "selected-result.json").read_text(encoding="utf-8")) + need(selected["decimal"] == KAPPA, "selected kappa drifted") + certificate = load_json((PACKAGE / "CERTIFICATE.json").read_text(encoding="utf-8")) + expect = { + "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": KAPPA, + "no_new_kappa": True, + } + need(certificate == expect, "certificate mismatch") + with tempfile.TemporaryDirectory() as tmp: + bad = Path(tmp) / "CERTIFICATE.json" + text = (PACKAGE / "CERTIFICATE.json").read_text(encoding="utf-8") + bad.write_text(text.replace('"minimum_calls": 12', '"minimum_calls": 11'), encoding="utf-8") + corrupted = load_json(bad.read_text(encoding="utf-8")) + need(corrupted != expect, "corruption was not detected") + duplicate = text.replace('"kappa"', '"kappa": "stale", "kappa"', 1) + try: + load_json(duplicate) + except ValueError as exc: + need(str(exc) == "duplicate JSON key", "duplicate detector message") + else: + need(False, "duplicate JSON key was accepted") + + +def check_read_only(before): + after = {path: file_digest(path) for path in before} + need(after == before, "verify wrote into the package") + + +def main(): + before = {path: file_digest(path) for path in sorted(PACKAGE.iterdir()) if path.is_file()} + check_group() + check_nilpotent_calculus() + check_idempotents() + check_words() + check_rank_bound() + check_kappa_and_receipt() + check_read_only(before) + print( + "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" + ) + + +if __name__ == "__main__": + main()