diff --git a/research/ut3-f4-w2-lift-obstruction/CERTIFICATE.json b/research/ut3-f4-w2-lift-obstruction/CERTIFICATE.json new file mode 100644 index 0000000000..6e82b0855b --- /dev/null +++ b/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 +} diff --git a/research/ut3-f4-w2-lift-obstruction/PROOF.md b/research/ut3-f4-w2-lift-obstruction/PROOF.md new file mode 100644 index 0000000000..6c65514ce5 --- /dev/null +++ b/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= 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`. diff --git a/research/ut3-f4-w2-lift-obstruction/README.md b/research/ut3-f4-w2-lift-obstruction/README.md new file mode 100644 index 0000000000..dd34206ebd --- /dev/null +++ b/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. diff --git a/research/ut3-f4-w2-lift-obstruction/SOURCES.json b/research/ut3-f4-w2-lift-obstruction/SOURCES.json new file mode 100644 index 0000000000..8c69ff75e8 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/ut3-f4-w2-lift-obstruction/TASK.json b/research/ut3-f4-w2-lift-obstruction/TASK.json new file mode 100644 index 0000000000..8894e669ea --- /dev/null +++ b/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." + } + ] +} diff --git a/research/ut3-f4-w2-lift-obstruction/VERIFY.json b/research/ut3-f4-w2-lift-obstruction/VERIFY.json new file mode 100644 index 0000000000..4c7304a6d9 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/ut3-f4-w2-lift-obstruction/independent.py b/research/ut3-f4-w2-lift-obstruction/independent.py new file mode 100644 index 0000000000..5b65aec614 --- /dev/null +++ b/research/ut3-f4-w2-lift-obstruction/independent.py @@ -0,0 +1,229 @@ +#!/usr/bin/env python3 +"""Independent frozenset replay of the six-label diagonal lift. + +Does not import verify.py. Recomputes commutators, both mixed words, the +blind {1,w} span, and the phi-diagonal inequality on those witnesses. +""" +from __future__ import annotations + +import itertools + +X1 = (1, 0, 0) +XW = (2, 0, 0) +XW2 = (3, 0, 0) +Y1 = (0, 1, 0) +YW = (0, 2, 0) +YW2 = (0, 3, 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): + 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 bit_rank(masks, width): + rows = list(masks) + rank = 0 + for col in range(width): + shift = width - 1 - col + pivot = None + for i, row in enumerate(rows): + if (row >> shift) & 1: + pivot = i + break + if pivot is None: + continue + rank += 1 + pivot_row = rows[pivot] + for i in range(len(rows)): + if (rows[i] >> shift) & 1: + rows[i] ^= pivot_row + return rank + + +def span_vectors(masks, width): + basis = [] + rows = list(masks) + for col in range(width): + shift = width - 1 - col + pivot = None + for i, row in enumerate(rows): + if (row >> shift) & 1: + pivot = i + break + if pivot is None: + continue + pivot_row = rows[pivot] + basis.append(pivot_row) + for i in range(len(rows)): + if (rows[i] >> shift) & 1: + rows[i] ^= pivot_row + vectors = [0] + for vector in basis: + vectors.extend([item ^ vector for item in vectors]) + return vectors + + +def phi_delta_bound(vectors, width): + low_mask = (1 << width) - 1 + phi = [] + diagonal = [] + for vector in vectors: + low = vector & low_mask + high = vector >> width + phi.append(low ^ high) + if low == high: + diagonal.append(low) + return bit_rank(phi, width) + bit_rank(diagonal, width) + + +def main(): + for a in range(4): + for b in range(4): + for c in range(4): + element = (a, b, c) + inverse = (a, b, f4_add(c, f4_mul(a, b))) + need(mul(element, inverse) == IDENTITY, "inverse") + need(mul(element, IDENTITY) == element, "identity") + need(f4_mul(3, 3) == 2, "w^2 square") + for a in (1, 2, 3): + for b in (1, 2, 3): + acc = IDENTITY + for label in ((a, 0, 0), (0, b, 0), (a, 0, 0), (0, b, 0)): + acc = mul(label, acc) + need(acc == (0, 0, f4_mul(a, b)), "commutator") + mixed = ( + (0, (X1, Y1, X1, Y1)), + (1, (XW, Y1, XW, Y1)), + (2, (XW2, Y1, XW2, Y1)), + ) + both = ( + (0, (X1, Y1, X1, Y1)), + (1, (XW2, YW2, XW2, YW2)), + (2, (XW, YW, XW, YW)), + ) + targets = (Z1, ZW, ZW2) + need(run_schedule(mixed, 3, targets), "mixed frozenset endpoint") + need(run_schedule(both, 3, targets), "both-new frozenset endpoint") + need(run_schedule(both, 4, targets + (IDENTITY,)), "spectator") + # Drop the last Y_w. The third register must miss Z_{w^2}. + broken = ( + (0, (X1, Y1, X1, Y1)), + (1, (XW2, YW2, XW2, YW2)), + (2, (XW, YW, XW)), + ) + need(not run_schedule(broken, 3, targets), "shortened both-new word matched") + # X shadows of the mixed word, ignoring w^2: e0 twice from X1, e1 twice from Xw. + blind = bit_rank([0b100, 0b100, 0b010, 0b010], 3) + need(blind == 2, "blind span") + # Lifts: X1 -> (e0, 0), Xw -> (0, e1), Xw2 -> (e2, e2). Low bits are the 1-coordinate. + e0, e1, e2 = 0b001, 0b010, 0b100 + lifts = [e0, e1 << 3, e2 | (e2 << 3)] + shadows = [e0, e1, e2] + need(bit_rank(lifts, 6) == 3, "lift rank") + need(bit_rank(shadows, 3) == 3, "shadow rank") + bound = phi_delta_bound(span_vectors(lifts, 6), 3) + need(bound <= 3 and bit_rank(shadows, 3) <= bound, "phi-delta on the mixed lifts") + # Overcount trap: axis dimensions 1+1+1 on a rank-2 lift. Not used as a bound. + trap = span_vectors([e0, e0 << 3], 6) + low_mask = 0b111 + dims = [] + for selector in ( + lambda low, high: high == 0, + lambda low, high: low == 0, + lambda low, high: low == high, + ): + picked = [] + for vector in trap: + low = vector & low_mask + high = vector >> 3 + if selector(low, high): + picked.append(low if high == 0 or low == high else high) + dims.append(bit_rank(picked, 3)) + need(sum(dims) == 3 and bit_rank([e0, e0 << 3], 6) == 2, "axis overcount") + need(phi_delta_bound(trap, 3) <= 2, "phi-delta repairs the overcount") + # Every triple of pure columns in r=3 obeys the shadow bound. A violation + # with shadow dimension 3 would appear as one of these triples. + pure = [] + for shadow in range(1, 8): + pure.append((shadow, shadow)) + pure.append((shadow, shadow << 3)) + pure.append((shadow, shadow | (shadow << 3))) + need(len(pure) == 21, "pure columns") + for triple in itertools.combinations(pure, 3): + shadow_rank = bit_rank([item[0] for item in triple], 3) + lift_rank = bit_rank([item[1] for item in triple], 6) + need(shadow_rank <= lift_rank, "triple outgrew its lift") + print( + "PASS_UT3_F4_W2_LIFT_INDEPENDENT minimum=12 labels=6 mixed=12 " + "both_new=12 blind_span=2 lift_rank=3 no_new_kappa" + ) + + +if __name__ == "__main__": + main() diff --git a/research/ut3-f4-w2-lift-obstruction/test_package.py b/research/ut3-f4-w2-lift-obstruction/test_package.py new file mode 100644 index 0000000000..a490bc59f8 --- /dev/null +++ b/research/ut3-f4-w2-lift-obstruction/test_package.py @@ -0,0 +1,66 @@ +#!/usr/bin/env python3 +"""Package controls for the six-label diagonal lift.""" +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_W2_LIFT " in out, out) + code, out, err = run([sys.executable, "-I", "-O", "-Werror", "-B", str(PACKAGE / "verify.py")]) + need(code == 0, err or out) + need("six_label_minimum=12" in out, out) + need("blind_span=2" 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_W2_LIFT_INDEPENDENT " in out, out) + certificate = json.loads((PACKAGE / "CERTIFICATE.json").read_text(encoding="utf-8")) + need(certificate["alphabet_labels"] == 6, "certificate labels") + need(certificate["six_label_minimum"] == 12, "certificate minimum") + need(certificate["blind_separated_span"] == 2, "certificate blind span") + 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" + " 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_W2_LIFT_PACKAGE_TESTS groups=3") + + +if __name__ == "__main__": + main() diff --git a/research/ut3-f4-w2-lift-obstruction/verify.py b/research/ut3-f4-w2-lift-obstruction/verify.py new file mode 100644 index 0000000000..98523a3180 --- /dev/null +++ b/research/ut3-f4-w2-lift-obstruction/verify.py @@ -0,0 +1,652 @@ +#!/usr/bin/env python3 +"""Six-label diagonal-lift obstruction for the UT3(F4) central triple. + +Read-only. Gates use need() so they stay live under python -O. No new kappa. +""" +from __future__ import annotations + +import hashlib +import itertools +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) +XW2 = (3, 0, 0) +Y1 = (0, 1, 0) +YW = (0, 2, 0) +YW2 = (0, 3, 0) +Z1 = (0, 0, 1) +ZW = (0, 0, 2) +ZW2 = (0, 0, 3) +LABELS = (X1, XW, XW2, Y1, YW, YW2) +X_LABELS = (X1, XW, XW2) +Y_LABELS = (Y1, YW, YW2) +ADD = ( + (0, 1, 2, 3), + (1, 0, 3, 2), + (2, 3, 0, 1), + (3, 2, 1, 0), +) +MUL = ( + (0, 0, 0, 0), + (0, 1, 2, 3), + (0, 2, 3, 1), + (0, 3, 1, 2), +) + + +def need(ok, message): + if not ok: + raise SystemExit("FAIL: " + message) + + +def f4_add(a, b): + return ADD[a][b] + + +def f4_mul(a, b): + return MUL[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) + + +def inverse_element(element): + a, b, c = element + return (a, b, f4_add(c, f4_mul(a, b))) + + +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 coeff_bits(label): + value = label[0] or label[1] + return {1: (1, 0), 2: (0, 1), 3: (1, 1)}[value] + + +def mat_mul(left, right): + size = len(left) + 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 = len(left) + 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 zeros(size): + return [[0] * size for _ in range(size)] + + +def transpose(matrix): + size = len(matrix) + return [[matrix[j][i] for j in range(size)] for i in range(size)] + + +def embed_scalar(value): + companion = [[0, 1], [1, 1]] + ident = eye(2) + b0, b1 = {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(b0, ident), scale(b1, companion)) + + +def rho6(element): + a, b, c = element + blocks = { + (0, 0): eye(2), (0, 1): embed_scalar(a), (0, 2): embed_scalar(c), + (1, 0): zeros(2), (1, 1): eye(2), (1, 2): embed_scalar(b), + (2, 0): zeros(2), (2, 1): zeros(2), (2, 2): eye(2), + } + out = zeros(6) + for bi in range(3): + for bj in range(3): + block = blocks[(bi, bj)] + for i in range(2): + for j in range(2): + out[2 * bi + i][2 * bj + j] = block[i][j] + return out + + +def nilpotent(element): + return mat_add(rho6(element), eye(6)) + + +def contragredient(element): + return transpose(rho6(inverse_element(element))) + + +def bit_rank(masks, width): + rows = list(masks) + rank = 0 + for col in range(width): + shift = width - 1 - col + pivot = None + for i, row in enumerate(rows): + if (row >> shift) & 1: + pivot = i + break + if pivot is None: + continue + rank += 1 + pivot_row = rows[pivot] + for i in range(len(rows)): + if (rows[i] >> shift) & 1: + rows[i] ^= pivot_row + return rank + + +def vector_mask(bits): + acc = 0 + for bit in bits: + acc = (acc << 1) | bit + return acc + + +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 + + +IDEMPOTENTS_R3 = idempotents(3) + + +def projector(index, width): + rows = [[0] * width for _ in range(width)] + rows[index][index] = 1 + return rows + + +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 apply_word(calls, width, bitset_inputs): + 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 schedule_calls(schedule, width): + calls = [] + for register, labels in schedule: + rows = projector(register, width) + for label in labels: + calls.append((label, rows)) + return calls + + +def mixed_schedule(): + return ( + (0, (X1, Y1, X1, Y1)), + (1, (XW, Y1, XW, Y1)), + (2, (XW2, Y1, XW2, Y1)), + ) + + +def both_new_schedule(): + return ( + (0, (X1, Y1, X1, Y1)), + (1, (XW2, YW2, XW2, YW2)), + (2, (XW, YW, XW, YW)), + ) + + +def factor_call(label, rows): + width = len(rows) + bank = IDEMPOTENTS_R3 if width == 3 else idempotents(width) + for u, v, matrix in bank: + if matrix == tuple(tuple(row) for row in rows): + return u, v + need(False, "call matrix is not a rank-one idempotent") + return [], [] + + +def lifts_of(side): + shadows = [] + columns = [] + rows = [] + width = len(side[0][1]) + for label, u, v in side: + b0, b1 = coeff_bits(label) + shadow = vector_mask(u) + # Low width bits are the first F2 coordinate (coefficient of 1). + column = (b0 * shadow) | ((b1 * shadow) << width) + shadows.append(shadow) + columns.append(column) + rows.append(vector_mask(v)) + return shadows, columns, rows, width + + +def split_sides(calls): + x_side = [] + y_side = [] + for label, rows in calls: + u, v = factor_call(label, rows) + if label in X_LABELS: + x_side.append((label, u, v)) + elif label in Y_LABELS: + y_side.append((label, u, v)) + else: + need(False, "label outside the six-involution alphabet") + return x_side, y_side + + +def pure_columns(width): + columns = [] + for shadow in range(1, 1 << width): + columns.append((shadow, shadow)) + columns.append((shadow, shadow << width)) + columns.append((shadow, shadow | (shadow << width))) + return columns + + +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: + need(group_mul(label, label) == (0, 0, 0), "paid label is not an involution") + # [g]+[1] is two distinct basis elements, so the F2 augmentation is 0. + support = {group_index(label), 0} + need(len(support) == 2 and (len(support) & 1) == 0, "paid factor augments nontrivially") + for a in (1, 2, 3): + for b in (1, 2, 3): + acc = (0, 0, 0) + for label in ((a, 0, 0), (0, b, 0), (a, 0, 0), (0, b, 0)): + acc = group_mul(label, acc) + need(acc == (0, 0, f4_mul(a, b)), "axis commutator mismatch") + need(f4_mul(3, 3) == 2, "w^2 * w^2 is not w") + + +def check_nilpotent_calculus(): + nil = {label: nilpotent(label) for label in LABELS} + x_set = set(X_LABELS) + y_set = set(Y_LABELS) + for left in LABELS: + for right in LABELS: + product = mat_mul(nil[left], nil[right]) + nonzero = any(bit for row in product for bit in row) + expect = left in x_set and right in y_set + need(nonzero == expect, "length-two nilpotent support") + if expect: + corner = [[product[i][4 + j] for j in range(2)] for i in range(2)] + need(corner == mat_mul(embed_scalar(left[0]), embed_scalar(right[1])), "pair corner") + 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: + for third in LABELS: + triple = mat_mul(nil[first], mat_mul(nil[second], nil[third])) + need(not any(bit for row in triple for bit in row), "nilpotent triple is nonzero") + for value in (1, 2, 3): + block = embed_scalar(value) + need(transpose(block) == block, "regular representation is not symmetric") + vee = {label: mat_add(contragredient(label), eye(6)) for label in LABELS} + for left in LABELS: + for right in LABELS: + product = mat_mul(vee[left], vee[right]) + nonzero = any(bit for row in product for bit in row) + expect = left in y_set and right in x_set + need(nonzero == expect, "contragredient length-two support") + if expect: + corner = [[product[4 + i][j] for j in range(2)] for i in range(2)] + need( + corner == mat_mul(embed_scalar(left[1]), embed_scalar(right[0])), + "contragredient corner", + ) + 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") + direct = rho6(target) + upper = [[direct[i][4 + j] for j in range(2)] for i in range(2)] + need(upper == embed_scalar(scalar), "direct target corner") + + +def check_idempotents_and_scalars(): + need(len(IDEMPOTENTS_R3) == 28, "M3(F2) rank-one idempotent count") + bank = {matrix for _, _, matrix in IDEMPOTENTS_R3} + invertible = [] + for bits in range(1 << 9): + matrix = [[(bits >> (3 * i + j)) & 1 for j in range(3)] for i in range(3)] + if bit_rank([vector_mask(row) for row in matrix], 3) == 3: + invertible.append(matrix) + need(len(invertible) == 168, "GL3(F2) order") + checked = 0 + for matrix in invertible: + inverse = invert3(matrix) + for _, _, rows in IDEMPOTENTS_R3: + body = [list(row) for row in rows] + conjugated = mat_mul(inverse, mat_mul(body, matrix)) + key = tuple(tuple(row) for row in conjugated) + need(key in bank, "conjugation left the idempotent set") + checked += 1 + need(checked == 168 * 28, "conjugation census") + + +def invert3(matrix): + size = 3 + work = [row[:] + [1 if i == j else 0 for j in range(size)] for i, row in enumerate(matrix)] + for col in range(size): + pivot = None + for row in range(col, size): + if work[row][col]: + pivot = row + break + need(pivot is not None, "singular matrix in GL3") + work[col], work[pivot] = work[pivot], work[col] + for row in range(size): + if row != col and work[row][col]: + work[row] = [(work[row][k] + work[col][k]) & 1 for k in range(2 * size)] + return [row[size:] for row in work] + + +def check_words(): + targets3 = [Z1, ZW, ZW2] + targets4 = [Z1, ZW, ZW2, (0, 0, 0)] + mixed = schedule_calls(mixed_schedule(), 3) + both = schedule_calls(both_new_schedule(), 3) + need(len(mixed) == 12 and len(both) == 12, "attaining length") + need(word_matches(mixed, targets3, 3), "mixed word endpoint") + need(word_matches(both, targets3, 3), "both-new word endpoint") + need(word_matches(schedule_calls(mixed_schedule(), 4), targets4, 4), "mixed spectator") + need(word_matches(schedule_calls(both_new_schedule(), 4), targets4, 4), "both-new spectator") + for calls in (mixed, both): + for omit in range(12): + broken = calls[:omit] + calls[omit + 1 :] + need(not word_matches(broken, targets3, 3), "omitted call still matched") + need(not word_matches(mixed, [Z1, ZW, Z1], 3), "wrong third target matched") + labels_used = {label for label, _ in both} + need(XW2 in labels_used and YW2 in labels_used, "both-new word missed a w^2 label") + mixed_labels = {label for label, _ in mixed} + need(XW2 in mixed_labels and YW2 not in mixed_labels, "mixed word label set") + + +def separated_span(calls): + shadows = [] + for label, rows in calls: + if label not in (X1, XW): + continue + u, _ = factor_call(label, rows) + shadows.append(vector_mask(u)) + return bit_rank(shadows, len(calls[0][1])) + + +def side_stats(side): + shadows, columns, rows, width = lifts_of(side) + return { + "count": len(side), + "shadow": bit_rank(shadows, width), + "lift": bit_rank(columns, 2 * width), + "v": bit_rank(rows, width), + } + + +def check_lift_on_words(): + mixed = schedule_calls(mixed_schedule(), 3) + both = schedule_calls(both_new_schedule(), 3) + need(separated_span(mixed) == 2, "separated span should be blind to w^2") + for calls in (mixed, both): + x_side, y_side = split_sides(calls) + for side in (x_side, y_side): + stats = side_stats(side) + need(stats["count"] == 6, "letter total") + need(stats["shadow"] == 3 and stats["v"] == 3, "witness spans") + need(stats["lift"] >= stats["shadow"], "lift lost a shadow") + need(stats["count"] >= stats["lift"] + stats["v"], "nullity inequality") + x_stats = side_stats(x_side) + need(x_stats["lift"] == 3, "mixed or both-new lift rank") + # The naive sum of the three pure-type subspace dimensions can exceed rank(L). + # span{(e0,0),(0,e0)} has lift rank 2 and axis dimensions 1+1+1. + e0 = 1 + columns = [e0, e0 << 3] + need(bit_rank(columns, 6) == 2, "overcount example rank") + span = span_vectors(columns, 6) + axis = axis_dims(span, 3) + need(sum(axis) == 3 and sum(axis) > bit_rank(columns, 6), "axis sum should overcount") + phi_bound = phi_delta_bound(span, 3) + need(phi_bound <= 2, "phi-delta bound failed on the overcount example") + + +def span_vectors(masks, width): + basis = [] + rows = list(masks) + for col in range(width): + shift = width - 1 - col + pivot = None + for i, row in enumerate(rows): + if (row >> shift) & 1: + pivot = i + break + if pivot is None: + continue + pivot_row = rows[pivot] + basis.append(pivot_row) + for i in range(len(rows)): + if (rows[i] >> shift) & 1: + rows[i] ^= pivot_row + vectors = [0] + for vector in basis: + vectors.extend([item ^ vector for item in vectors]) + return vectors + + +def axis_dims(vectors, width): + low_mask = (1 << width) - 1 + a_set = [] + b_set = [] + d_set = [] + for vector in vectors: + low = vector & low_mask + high = vector >> width + if high == 0: + a_set.append(low) + if low == 0: + b_set.append(high) + if low == high: + d_set.append(low) + return (bit_rank(a_set, width), bit_rank(b_set, width), bit_rank(d_set, width)) + + +def phi_delta_bound(vectors, width): + low_mask = (1 << width) - 1 + phi = [] + diagonal = [] + kernel = [] + for vector in vectors: + low = vector & low_mask + high = vector >> width + phi.append(low ^ high) + if low == high: + diagonal.append(low) + if low ^ high == 0: + kernel.append(vector) + # dim phi(L) + dim(L∩Δ) = dim L - dim(L∩ker) + dim(L∩Δ) <= dim L. + return bit_rank(phi, width) + bit_rank(diagonal, width) + + +def check_shadow_census(): + columns = pure_columns(3) + need(len(columns) == 21, "pure column count") + checked = 0 + violating_triples = 0 + for size in range(0, 7): + for subset in itertools.combinations(columns, size): + checked += 1 + shadows = [item[0] for item in subset] + lifts = [item[1] for item in subset] + shadow_rank = bit_rank(shadows, 3) if shadows else 0 + lift_rank = bit_rank(lifts, 6) if lifts else 0 + if shadow_rank > lift_rank: + violating_triples += 1 + if size <= 4 and lifts: + vectors = span_vectors(lifts, 6) + need(phi_delta_bound(vectors, 3) <= lift_rank, "phi-delta census") + need(shadow_rank <= phi_delta_bound(vectors, 3), "shadow outside phi+delta") + need(checked == 82160, "subset census size") + need(violating_triples == 0, "a pure family outgrew its lift") + # Three aligned output directions are independent as lifts, so no rank-2 + # space contains all of them. + witness = [1, 2 << 3, 4 | (4 << 3)] + need(bit_rank(witness, 6) == 3, "three output directions are dependent") + for pair in itertools.combinations(witness, 2): + need(bit_rank(pair, 6) == 2, "pair of output directions collapsed") + + +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, + "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": 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('"six_label_minimum": 12', '"six_label_minimum": 10'), 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_and_scalars() + check_words() + check_lift_on_words() + check_shadow_census() + check_kappa_and_receipt() + check_read_only(before) + print( + "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" + ) + + +if __name__ == "__main__": + main()