From 9d6117918025cee6a0c5b7ef30ff8d936ca0621f Mon Sep 17 00:00:00 2001 From: Hanson Sun <182361798+bbMisk@users.noreply.github.com> Date: Tue, 13 Oct 2026 23:54:50 -0400 Subject: [PATCH] Prove exact tariffs for mixed UT3 register targets --- .../ut3-mixed-target-tariffs/CERTIFICATE.json | 49 ++ research/ut3-mixed-target-tariffs/README.md | 265 +++++++++++ .../ut3-mixed-target-tariffs/SOURCES.json | 62 +++ research/ut3-mixed-target-tariffs/TASK.json | 149 +++++++ research/ut3-mixed-target-tariffs/VERIFY.json | 25 ++ .../ut3-mixed-target-tariffs/independent.py | 155 +++++++ research/ut3-mixed-target-tariffs/verify.py | 419 ++++++++++++++++++ 7 files changed, 1124 insertions(+) create mode 100644 research/ut3-mixed-target-tariffs/CERTIFICATE.json create mode 100644 research/ut3-mixed-target-tariffs/README.md create mode 100644 research/ut3-mixed-target-tariffs/SOURCES.json create mode 100644 research/ut3-mixed-target-tariffs/TASK.json create mode 100644 research/ut3-mixed-target-tariffs/VERIFY.json create mode 100644 research/ut3-mixed-target-tariffs/independent.py create mode 100644 research/ut3-mixed-target-tariffs/verify.py diff --git a/research/ut3-mixed-target-tariffs/CERTIFICATE.json b/research/ut3-mixed-target-tariffs/CERTIFICATE.json new file mode 100644 index 0000000000..1394300a4f --- /dev/null +++ b/research/ut3-mixed-target-tariffs/CERTIFICATE.json @@ -0,0 +1,49 @@ +{ + "all_eight_labels_bill": [ + 8, + 8 + ], + "boundary_mutation_controls": 3925, + "diagonal_endpoint_words": 7435, + "exact_tariff_endpoints": 32, + "expanded_r2_alphabet": 18, + "faithful_columns": 62848, + "group_products": 64, + "independent": { + "expanded_involutions": 566, + "faithful_columns": 62848, + "kernel_dirty_columns_detected": 8, + "nilpotent_involutions": 258, + "two_factor_digest": "c36a1fa70144f60549eeea5f61fb5799097bba7a9af2d20c0c609c96c4853c58", + "two_factor_products": 324, + "witness_digest": "69789e8017dde99a172de85b1cb5dbd5db5867374ba9bfc2eac14012ee988753", + "witness_fixtures": 2336 + }, + "model_controls": [ + "nonfaithful_quotient_kernel", + "formal_kernel_rejection", + "faithful_kernel_rejection", + "clean_extra_blind_spot", + "nonzero_first_order_correction", + "missing_xy_correction", + "central_label_restriction", + "nonzero_factor_restriction", + "unit_priced_rank_two_escape", + "nilpotent_reversibility" + ], + "nonfaithful_kernel_support": [ + 0, + 1, + 4, + 5 + ], + "quotient_associativity_triples": 32768, + "schema_version": 1, + "scope": "Finite evidence for the written all-register mixed UT3 tariff theorem; no new kappa.", + "sylvester_nonzero_products": 3735, + "sylvester_pairs": 4369, + "two_factor_digest": "c36a1fa70144f60549eeea5f61fb5799097bba7a9af2d20c0c609c96c4853c58", + "witness_digest": "69789e8017dde99a172de85b1cb5dbd5db5867374ba9bfc2eac14012ee988753", + "witness_fixtures": 2336, + "words_through_length_four": 111151 +} diff --git a/research/ut3-mixed-target-tariffs/README.md b/research/ut3-mixed-target-tariffs/README.md new file mode 100644 index 0000000000..1778bfdb77 --- /dev/null +++ b/research/ut3-mixed-target-tariffs/README.md @@ -0,0 +1,265 @@ +# Exact tariffs for every mixture of UT3 targets + +**Scoped negative theorem; no new kappa.** In the formal two-letter +`F2[UT_3(F2)]` register model, arbitrary mixtures of the eight address labels +cost exactly the sum of their separate direct bills. Free scalar mixing and +any finite number of restored dirty registers cannot lower either generator +count. The result permits all nonzero binary rank-one scalar couplings, +including nilpotents. + +For a target `g_i=(x_i,y_i,z_i)`, with each coordinate in `{0,1}`, define + +``` +A_min = sum_i (x_i + 2(1-x_i)z_i) +B_min = sum_i (y_i + 2(1-y_i)z_i). +``` + +Every legal word uses at least `A_min` calls of `a` and `B_min` calls of `b`. +One direct word attains both bounds simultaneously. Thus fixed positive +per-letter prices `alpha,beta` give exactly `alpha*A_min + beta*B_min`. +The displayed counts use ordinary integer arithmetic, not arithmetic mod 2. + +This extends steph4n-gh's [PR1573](https://github.com/CrocSwap/integer-mult-bounds/pull/1573) +and Arham Tahir's [PR1589](https://github.com/CrocSwap/integer-mult-bounds/pull/1589). +They prove the repeated central-target bill `4k`, first for idempotents and +then for arbitrary rank-one couplings. Their quotient and rank methods are +retained and credited. The new step handles **nonzero first-order endpoint +coefficients**, yielding separate sharp tariffs for every heterogeneous +endpoint, rather than only repeated central targets. For example, the mixture +`(a,b,c,aba,bab,ab,ba)` costs exactly eight a-calls and eight b-calls. No +predecessor executable or unproved predecessor conclusion is assumed. + +## Model and complete abstract bill + +Let `G=UT_3(F2)`, where `(x,y,z)` specifies entries `01,12,02` of an upper +unitriangular binary 3-by-3 matrix. Its multiplication is + +`(x,y,z)(X,Y,Z)=(x+X,y+Y,z+Z+xY)`. + +Here and throughout the proof, additions and products of matrix entries are +over `F2`. Put `a=(1,0,0)`, `b=(0,1,0)`, and `c=abab=(0,0,1)`. +For any finite `r >= w >= 1`, require the full formal endpoint + +`T = diag([g_1],...,[g_w],1,...,1)` in `Mat_r(F2[G])`. + +Every role has arbitrary input. In particular, the last `r-w` roles must be +restored as operators, not merely tested from zero. An allowed paid call is + +`D_N(g) = I_r + ([g]+1)N`, where `g` is only `a` or `b`, +`N=u v^T`, and `u,v` are nonzero binary r-vectors. + +Both `v^T u=1` (idempotent) and `v^T u=0` (nilpotent) are allowed, at one +optimistic unit each. Since `g^2=1`, `([g]+1)^2=0`; hence every such call is +an involution regardless of `N^2`. Arbitrary scalar `GL_r(F2)` maps are free. +There are no other free address operations, clean allocation, COPY, ERASE, +unpaid inverses, or higher-rank paid factors. This is the expanded abstract +screening alphabet of PR1589, not an implementation claim for the supplier. + +Interleaved scalar maps can be collected at one end by conjugating the +rank-one couplings. Augmentation `[g] -> 1` sends every paid call and the +endpoint to `I_r`, so the remaining scalar map is `I_r`. Conjugation preserves +rank and stays inside the declared alphabet. It is therefore enough to bound +a product of paid factors. The conclusion also holds for a common scalar +conjugate of the whole endpoint. + +The following coordinate words attain the two bounds. Apply each word to the +coordinate projector `E_ii`, and concatenate across target roles. + +| `(x,y,z)` | Address word | a-calls | b-calls | +|---|---|---:|---:| +| `(0,0,0)` | empty | 0 | 0 | +| `(1,0,0)` | `a` | 1 | 0 | +| `(0,1,0)` | `b` | 0 | 1 | +| `(1,1,0)` | `ba` | 1 | 1 | +| `(0,0,1)` | `abab` | 2 | 2 | +| `(1,0,1)` | `bab` | 1 | 2 | +| `(0,1,1)` | `aba` | 2 | 1 | +| `(1,1,1)` | `ab` | 1 | 1 | + +These are full formal identities: a coordinate factor acts by `[g]` on its +role and by identity on every other role. The bill uses `w` target roles, +zero extra workspace, the displayed paid calls, and no additional preparation +or restoration. Appending untouched roles gives any `r >= w`. The theorem +also applies to the idempotent-only alphabet, since the lower bound allows +more calls and the attaining words use idempotents. + +## Proof: coefficient spans with nonzero first-order terms + +Use the five-dimensional algebra + +`Q = F2 / (X^2, Y^2, all monomials of degree at least three)`. + +The map on group elements is + +`[x,y,z] -> 1 + xX + yY + zXY + (z+xy)YX`. + +Substitution in the group law proves multiplicativity: the `XY` cross term +is `xY` and the `YX` cross term is `yX`. Extending linearly gives an algebra +homomorphism `F2[G] -> Q`. This is exactly PR1589's quotient, equivalently +PR1573's two small representations. It is used only for necessary conditions. +It is not faithful and cannot certify a formal endpoint. + +Write a normalized word's quotient as + +`I + AX + BY + CXY + DYX`, + +where `A,B,C,D` are binary r-by-r matrices. Matrix factors keep their original +order. Collect all a-call column factors into `U` and row factors into `V`, +so `U` is r-by-`n_a`, `V` is `n_a`-by-r, and + +`A = UV = sum_{a calls} N_i`. + +Every `XY` term chooses an a-call followed by a b-call. Its matrix is +`N_i N_j`, whose image lies in the image of `U`. Thus + +`rank [A C] <= rank U`. + +Every `YX` term chooses a b-call followed by an a-call, so its row space +lies in the row space of `V`. Thus + +`rank [A; D] <= rank V`. + +Here `[A C]` denotes horizontal concatenation and `[A; D]` vertical stacking. +No commutation of the scalar matrices is used. Rank-nullity, or Sylvester's +inequality for the product `UV`, gives + +`rank U + rank V <= n_a + rank(UV) = n_a + rank A`. + +For completeness, restrict `U` to `im V`: its image has dimension `rank(UV)` +and its kernel has dimension at most `dim ker U = n_a-rank U`. This proves +the displayed inequality without a zero-product assumption. Consequently + +`n_a >= rank [A C] + rank [A; D] - rank A`. (1) + +Exchanging a and b gives + +`n_b >= rank [B D] + rank [B; C] - rank B`. (2) + +These two inequalities hold for any endpoint of a legal word, even one that +is not diagonal. They are the useful coefficient-span relaxation. + +For the required diagonal endpoint, include the restored roles as triples +`(0,0,0)`. Then + +`A=diag(x_i), B=diag(y_i), C=diag(z_i), D=diag(z_i+x_i*y_i)`. + +The rank of `[A C]` is the number of indices with `x_i=1` or `z_i=1`. +The same is true of `[A; D]`: if `x_i=0`, the i-th entry of D is `z_i`; +if `x_i=1`, A already contributes that index. Substituting into (1), each +index contributes + +`2 * 1_{x_i=1 or z_i=1} - x_i = x_i + 2(1-x_i)z_i`. + +The analogous substitution in (2) gives `y_i+2(1-y_i)z_i`. These are the +two claimed lower bounds. The direct table attains both, completing the +proof for every target count, every finite dirty workspace, and every word +length. Positive uniform per-letter tariffs follow by weighting the two +inequalities. Prices depending on roles, chronology, or implementation +costs are outside that corollary. + +The subtraction of `rank A` or `rank B` is essential. For a single target +`a`, there is one a-call and `rank A=1`; reusing the central-only zero-sum +inequality would falsely demand two calls. When all targets are `c`, both +first-order matrices vanish and (1)-(2) recover the predecessors' `2k+2k` +central bill. That special case is credited to the predecessors. + +## Reproduction and finite evidence + +Python 3.12 or later, standard library only, from the repository root: + +```sh +python3 -I -O -B research/ut3-mixed-target-tariffs/verify.py +python3.12 scripts/research_package.py --package research/ut3-mixed-target-tariffs +``` + +Expected: `PASS_UT3_MIXED_TARGET_TARIFFS` and, for the registered command, +`PASS_REGISTERED_RESEARCH_PACKAGE`. Default replay is read-only. `--emit` +prints a fresh deterministic receipt; acceptance compares every field and +value type against [CERTIFICATE.json](CERTIFICATE.json). + +The written argument above proves the unbounded statement. The finite checks +corroborate its definitions, inequalities and attaining words: + +- All 64 group products verify the quotient homomorphism; all 32,768 triples + of quotient elements verify associativity. Exact shortest paths independently + check all eight address tariffs at four positive rational price pairs. +- All 4,369 pairs of binary matrices of shapes `2-by-n` and `n-by-2`, + `0 <= n <= 3`, check Sylvester's inequality, including 3,735 nonzero products. +- All 111,151 words of length zero through four on two registers are checked + in the expanded 18-factor alphabet. Both coefficient-span bounds hold; + all 7,435 diagonal endpoint words satisfy the proposed separate tariffs. +- All 584 ordered one-, two-, and three-target mixtures have full formal + witnesses with zero or one extra dirty role, both in the coordinate basis + and after scalar conjugation: 2,336 fixtures and 62,848 basis columns. + A ten-register fixture also checks all eight labels together, costing 8+8. +- [independent.py](independent.py) imports no local implementation. It uses + literal binary 3-by-3 address matrices and the faithful 8r-dimensional + regular action. Both implementations agree on complete witness operators + and all 324 ordered two-factor products, using canonical SHA256 digests. + It also checks 566 full paid involutions at r=2,3,4, including 258 nilpotent + ones. Both implementations were authored in this session; this is not + independent human review. +- Deleted calls and un-restored dirty roles give 3,925 rejected boundary + mutations. Model controls exercise the nonzero first-order correction, + noncommuting order, alphabet/rank restrictions and the nonfaithful quotient. + In particular, a nonzero four-term off-diagonal perturbation has zero + quotient image, is invisible on clean-extra inputs, and changes all eight + dirty-extra basis columns in the faithful check. + +Local validation passed on CPython 3.12.13 (registered replay, about 2.5 +seconds) and CPython 3.14.6 (optimized, read-only standalone relocation). +A deliberately corrupted certificate was rejected under optimization; the +source package and read-only export stayed byte-identical during those checks. +Exact tested code hashes and validation scope are in TASK.json. Hosted CI is +separate from these local results. + +This is a written scoped theorem with exact executable evidence, not a Lean +proof. Full selected-supplier cold replay, physical/compiler/common-label +realization, hosting, precision/tape and outer analytic transfer were not +checked. No selected record, frozen predecessor, or upstream source is changed. + +## Provenance, overlap, and credit + +The starting main commit is `ebedc0895eb4c06725af020bc1af165722b0a3ce`. +The catalogue chose `bit-new-register-model` in the bit-mechanisms track, +nonce `4aba18fcd52cd4290d0badf705c2dfc3`, priority revision 2. The selected +PR1094 baseline binding check passed; its conditional kappa is unchanged. +[TASK.json](TASK.json) contains the refined scope, stopping rule and overlap +coverage. [SOURCES.json](SOURCES.json) pins the base inputs and contextual +predecessor texts. The contextual remote files are not runtime dependencies. +Coordination: [Discussion1599](https://github.com/CrocSwap/integer-mult-bounds/discussions/1599). + +The nearest predecessors are PR1573 at +`0b8c5a69297c794f2de22c04494c83e41300ae36` and PR1589 at +`010ec8c01c0edbbb08b541be236ab78d096f2ca1`; both explicitly restrict their +conclusions to central targets. Hanson's PR1567 treats mixed GL3 targets +with six coordinate letters on exactly two registers by finite enumeration; +it is a different alphabet and method, not a dependency. The all-target UT3 +conclusion here follows analytically and permits arbitrary finite workspace. +The final refresh covered 733 open PRs and 244 discussion records with +complete pagination and no warnings, at 2026-10-14 03:52 UTC. Before submission, +the branch was rebased onto main `81e81af67714bdc8d1693b0bf5c29468b92f62ff`; +priority revision 3 leaves this bit task and the selected record unchanged. +Search coverage is not a claim of literature priority. + +Credit steph4n-gh (PR1573) and Arham Tahir (PR1589) for the central all-register +bounds, quotient and rank methods; @juper997 (PR1478) and @woklerx (PR1443) for +the finite UT3/D8 predecessors; Gareth Davidson / @bitplane (PR1333) for the +nonabelian register direction and scalar normalization; and the retained +@eumemic, Ali Romman, David Govea and @commdata2338 register-model lineage. +No novelty is claimed for Sylvester's inequality or the quotient itself. + +Prepared for **Hanson Sun (@bbMisk)** with substantial **OpenAI Codex +assistance** in proof, implementation, validation and writing. No subagents or +independent human proof review. Apache-2.0. + +## Open next questions + +Can a different, fully priced nonabelian address alphabet escape these bills? +The mixed-target and workspace-only routes in the stated UT3 alphabet are +settled by the theorem. A feasible first step is to specify one additional +physically realizable address primitive, compute its first- and second-degree +coefficient matrices, and charge its rank, frames and restoration. The blocker +is the actual supplier interface: declaring another label to cost one does not +establish a usable improvement. This package does not claim a stronger +obstruction for that changed alphabet. diff --git a/research/ut3-mixed-target-tariffs/SOURCES.json b/research/ut3-mixed-target-tariffs/SOURCES.json new file mode 100644 index 0000000000..03d9f1c4b3 --- /dev/null +++ b/research/ut3-mixed-target-tariffs/SOURCES.json @@ -0,0 +1,62 @@ +{ + "schema_version": 1, + "base_commit": "ebedc0895eb4c06725af020bc1af165722b0a3ce", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "input", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/bit-three-register-lower-bound/README.md", + "usage": "input", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "input", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + } + ], + "contextual_predecessors": [ + { + "pr": 1573, + "head": "0b8c5a69297c794f2de22c04494c83e41300ae36", + "author": "steph4n-gh", + "path": "research/ut3-commutator-all-registers/README.md", + "git_blob": "4a6a4ee9d995818348b3b853a95500dcce81228d", + "sha256": "fdd5405da1c0535a407013f2a4628a07dae4957fd9fb776cd14f05315d1aa26b", + "usage": "Contextual proof and scope attribution only; no executable import or unproved premise." + }, + { + "pr": 1589, + "head": "010ec8c01c0edbbb08b541be236ab78d096f2ca1", + "author": "Arham Tahir", + "path": "research/ut3-two-targets-any-registers/README.md", + "git_blob": "3fc4f569a2e9bc81a1f61bc8343a276671a2d13f", + "sha256": "f879e3009b1fd5c625480ef92bdc454030ae62e7b378af7869e188df718e7399", + "usage": "Contextual proof and scope attribution only; no executable import or unproved premise." + } + ] +} diff --git a/research/ut3-mixed-target-tariffs/TASK.json b/research/ut3-mixed-target-tariffs/TASK.json new file mode 100644 index 0000000000..90f55bbdd8 --- /dev/null +++ b/research/ut3-mixed-target-tariffs/TASK.json @@ -0,0 +1,149 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 2, + "base_commit": "ebedc0895eb4c06725af020bc1af165722b0a3ce", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write a complete operation alphabet outside one named premise and price a baseline before searching identities.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "refined", + "actual_scope": "Exact separate a/b call minima for every diagonal mixture of UT_3(F2) targets, with arbitrary finite restored dirty workspace and every nonzero binary rank-one scalar coupling.", + "scope_change_reason": "The catalogue permits a specified nonabelian family. Extend the central-only target scopes of PR1573 and PR1589 to all eight UT3 labels; retain their two-letter paid alphabet and explicitly expanded rank-one coupling model.", + "bottleneck_link": "Scoped negative result for a concrete nonabelian register interface: decide whether heterogeneous targets or workspace lower the fully charged abstract call bill. This is not a selected-supplier construction or a kappa improvement.", + "budget_minutes": 60, + "stop_rule": "One 60-minute session; stop the proposed formula on the first exact counterexample. Reserve the final quarter for replay, review, and handoff.", + "outcome": "negative-result", + "evidence": "README.md proves the all-register mixed-target tariff; CERTIFICATE.json records exact formal and separately implemented faithful-regular checks, all 111151 expanded two-register words through length four, and boundary/model controls.", + "author": "Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in proof, implementation, checking, and writing; no subagents or independent human proof review.", + "open_questions": [ + { + "question": "Does the sharp mixed-target rank bill survive a different, fully priced nonabelian address alphabet?", + "why_it_matters": "The two-letter UT3 mixture and workspace routes are closed by the proposed theorem, so a useful escape must change an explicit hypothesis.", + "first_step": "Specify one additional physically realizable address primitive and compute both mixed coefficient matrices and its complete rank/restoration cost.", + "blocked_by": "The abstract added label must be connected to the actual supplier interface and charged; an arbitrary unit-cost declaration is insufficient." + } + ], + "selection": { + "nonce": "4aba18fcd52cd4290d0badf705c2dfc3", + "track": "bit-mechanisms", + "scope_key": "7084092dd726e7ba1f2f", + "method": "Derive a target-specific relaxation bound for that same explicit alphabet.", + "other_suggestion": "bit-helper-contract; immediate helper-star admission and restoration questions already had active PRs and discussion claims." + }, + "proposed_scope_key": "UT3F2/all-eight-diagonal-target-mixtures/all-finite-registers/all-rank-one-couplings/separate-label-Sylvester-bound", + "optimistic_full_cost_budget": "Each g=(x,y,z) costs x+2(1-x)z calls of a and y+2(1-y)z calls of b. Sum over targets; arbitrary dirty extras are restored; all inverse calls charged. Improvement would violate at least one proposed lower bound.", + "overlap": { + "snapshot": "2026-10-14T03:36:06.654610+00:00", + "open_prs": 727, + "discussion_records": 233, + "complete_pagination": true, + "nearest": [ + { + "pr": 1573, + "head": "0b8c5a69297c794f2de22c04494c83e41300ae36", + "scope": "Central targets only; rank-one idempotents. Supplies the two-representation zero-sum rank argument." + }, + { + "pr": 1589, + "head": "010ec8c01c0edbbb08b541be236ab78d096f2ca1", + "scope": "Central targets only; includes nilpotent rank-one couplings. Supplies the degree-two quotient formulation." + }, + { + "pr": 1567, + "head": "fd7f1a434da543e3fb4e1efbb6056dbdc3a292af", + "scope": "Different six-label GL3 alphabet; exactly two registers; finite mixed-target census." + } + ], + "coverage_limits": "PR titles/bodies and discussion posts plus local notes/ledger; not all diffs, closed remote PRs, or literature. No novelty assertion." + }, + "coordination": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1599", + "claim_expires": "2026-10-14T05:46:00Z" + }, + "submission_base_commit": "81e81af67714bdc8d1693b0bf5c29468b92f62ff", + "priority_refresh": "Main advanced to priority revision 3 during the session. The bit-mechanisms track, task card, selected record, and replay driver are unchanged. The original revision-2 assignment and exact provenance remain recorded; no reroll.", + "final_overlap": { + "searched_at": "2026-10-14T03:52:08.193282+00:00", + "terms": [ + "UT3", + "UT_3", + "mixed target", + "heterogeneous target" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-14T03:51:42.501989+00:00", + "complete_pagination": true, + "records": 733 + }, + "discussions": { + "fetched_at": "2026-10-14T03:52:08.147981+00:00", + "complete_pagination": true, + "records": 244 + } + }, + "warnings": [], + "assessment": "Only this claim addresses all eight UT3 diagonal targets with arbitrary register count. PR1573/1589 remain central-only; PR1567 uses the larger GL3 six-letter alphabet on exactly two registers. Search coverage is not a novelty proof." + }, + "validation": { + "python_versions": { + "python3": "Python 3.14.6", + "python3.12": "Python 3.12.13" + }, + "platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O", + "registered_replay": "python3.12 scripts/research_package.py --package research/ut3-mixed-target-tariffs", + "registered_exit_code": 0, + "registered_elapsed_seconds": 2.493, + "readonly_optimized_relocated_replay_exit_code": 0, + "corrupted_receipt_replay_exit_code": 1, + "corruption": "Changed integer group_products to boolean true; optimized replay rejected the committed certificate mismatch.", + "source_package_unchanged_during_checks": true, + "tested_files": { + "verify.py": "247e1039ba2a153b0b65e69983dc936a8932c04d14b1ce71b07773b4bf699416", + "independent.py": "ffe303e3e0a9b21d2527c6f54f6f514182231e0415ec16f0543b440fc18fd121", + "CERTIFICATE.json": "0a7729c64d7c9fc3cf7d344c7aa74f6bc509287ba28999cfa8e86a8f27fcc37e" + }, + "unrun": [ + "Full selected supplier cold replay", + "Physical/compiler/common-label/hosting/precision/tape interfaces", + "Outer analytic transfer", + "Lean formalization", + "Independent human proof review", + "Hosted CI at local validation time" + ] + } +} diff --git a/research/ut3-mixed-target-tariffs/VERIFY.json b/research/ut3-mixed-target-tariffs/VERIFY.json new file mode 100644 index 0000000000..716e3fc36b --- /dev/null +++ b/research/ut3-mixed-target-tariffs/VERIFY.json @@ -0,0 +1,25 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "docs/research/community-batch1099-review.md", + "research/bit-three-register-lower-bound/README.md", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/community-frontier1094-audit/SELECTED-SOURCE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact coefficient-span inequalities, full formal mixed-target witnesses, separate faithful-regular agreement, and boundary/model failure controls." + } + ] +} diff --git a/research/ut3-mixed-target-tariffs/independent.py b/research/ut3-mixed-target-tariffs/independent.py new file mode 100644 index 0000000000..b26c9ef82a --- /dev/null +++ b/research/ut3-mixed-target-tariffs/independent.py @@ -0,0 +1,155 @@ +#!/usr/bin/env python3 +"""Separate faithful-regular witness implementation; imports no local code. + +Address multiplication uses literal binary 3x3 matrices. Register actions use +8r-dimensional row-bit matrices, not formal group-algebra coefficients. +Hanson Sun, with substantial OpenAI Codex assistance. Apache-2.0. +""" + +import hashlib +from itertools import product +import json + + +def demand(condition, message): + if not condition: + raise ValueError(message) + + +def address_product(a, b): + return tuple(sum(a[3 * i + k] * b[3 * k + j] for k in range(3)) % 2 for i in range(3) for j in range(3)) + + +ELEMENTS = tuple((1, n & 1, n >> 2, 0, 1, (n >> 1) & 1, 0, 0, 1) for n in range(8)) +INDEX = {value: i for i, value in enumerate(ELEMENTS)} +PERM = tuple(tuple(INDEX[address_product(g, h)] for h in ELEMENTS) for g in ELEMENTS) +DIRECT = ((), (1,), (2,), (2, 1), (1, 2, 1, 2), (2, 1, 2), (1, 2, 1), (1, 2)) + + +def identity(n): + return [1 << i for i in range(n)] + + +def multiply(a, b): + out = [] + for row in a: + value = 0 + while row: + low = row & -row + value ^= b[low.bit_length() - 1] + row ^= low + out.append(value) + return out + + +def paid(r, label, u, v): + rows = identity(8 * r) + for i in range(r): + for j in range(r): + if u >> i & 1 and v >> j & 1: + for h in range(8): + rows[8 * i + h] ^= 1 << (8 * j + h) + rows[8 * i + PERM[label][h]] ^= 1 << (8 * j + h) + return rows + + +def endpoint(labels, r): + rows = [0] * (8 * r) + for i in range(r): + label = labels[i] if i < len(labels) else 0 + for h in range(8): + rows[8 * i + PERM[label][h]] = 1 << (8 * i + h) + return rows + + +def lift(scalar): + r = len(scalar) + rows = [0] * (8 * r) + for i, row in enumerate(scalar): + for j in range(r): + if row >> j & 1: + for h in range(8): + rows[8 * i + h] |= 1 << (8 * j + h) + return rows + + +def basis(r): + changes = [] + for i in range(r - 1): + change = identity(r) + change[i] |= 1 << (i + 1) + changes.append(change) + forward = identity(r) + backward = identity(r) + for change in changes: + forward = multiply(forward, change) + for change in reversed(changes): + backward = multiply(backward, change) + demand(multiply(forward, backward) == identity(r), "independent basis inversion") + return lift(forward), lift(backward) + + +def digest_rows(digest, rows): + digest.update(json.dumps(rows, separators=(",", ":")).encode() + b"\n") + + +def run(): + for label, word in enumerate(DIRECT): + g = ELEMENTS[0] + for letter in word: + g = address_product(g, ELEMENTS[letter]) + demand(g == ELEMENTS[label], "direct literal address word") + witness_digest = hashlib.sha256() + fixtures = columns = 0 + for size in range(1, 4): + for labels in product(range(8), repeat=size): + for extra in (0, 1): + r = size + extra + gates = [paid(r, letter, 1 << i, 1 << i) for i, label in enumerate(labels) for letter in DIRECT[label]] + for conjugated in (False, True): + f, inv = basis(r) + out = identity(8 * r) + for gate in gates: + op = multiply(multiply(f, gate), inv) if conjugated else gate + out = multiply(out, op) + expected = endpoint(labels, r) + if conjugated: + expected = multiply(multiply(f, expected), inv) + demand(out == expected, "faithful full arbitrary-input boundary") + digest_rows(witness_digest, out) + fixtures += 1 + columns += 8 * r + pair_digest = hashlib.sha256() + alphabet = [paid(2, label, u, v) for label in (1, 2) for u in range(1, 4) for v in range(1, 4)] + for left, right in product(alphabet, repeat=2): + digest_rows(pair_digest, multiply(left, right)) + involutions = nilpotents = 0 + for r in (2, 3, 4): + for u, v in product(range(1, 1 << r), repeat=2): + for label in (1, 2): + gate = paid(r, label, u, v) + demand(multiply(gate, gate) == identity(8 * r), "full expanded factor involution") + involutions += 1 + nilpotents += (u & v).bit_count() % 2 == 0 + # A four-term off-diagonal algebra element invisible to both small images + # must still change the faithful action on a restored dirty role. + good = endpoint((4,), 2) + bad = list(good) + for label in (0, 1, 4, 5): + for h in range(8): + bad[PERM[label][h]] ^= 1 << (8 + h) + differences = [a ^ b for a, b in zip(good, bad)] + demand(any(differences), "faithful kernel mutation must reject") + demand(all(d & 255 == 0 for d in differences), "clean-input-only blind spot") + dirty_changed = sum(any(d >> j & 1 for d in differences) for j in range(8, 16)) + demand(dirty_changed == 8, "all eight dirty basis inputs detect kernel mutation") + # Reversing the noncommuting direct word distinguishes ab from ba. + demand(multiply(paid(1, 1, 1, 1), paid(1, 2, 1, 1)) != endpoint((3,), 1), "noncommuting order control") + return {"witness_fixtures": fixtures, "faithful_columns": columns, + "witness_digest": witness_digest.hexdigest(), "two_factor_digest": pair_digest.hexdigest(), + "two_factor_products": 324, "expanded_involutions": involutions, + "nilpotent_involutions": nilpotents, "kernel_dirty_columns_detected": dirty_changed} + + +if __name__ == "__main__": + print(json.dumps(run(), sort_keys=True)) diff --git a/research/ut3-mixed-target-tariffs/verify.py b/research/ut3-mixed-target-tariffs/verify.py new file mode 100644 index 0000000000..256e34a01f --- /dev/null +++ b/research/ut3-mixed-target-tariffs/verify.py @@ -0,0 +1,419 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the mixed UT3 target theorem in README.md. + +Hanson Sun, with substantial OpenAI Codex assistance. Apache-2.0. +No predecessor implementation is imported. The unbounded theorem is written, +not inferred from the finite fixtures below. Default operation is read-only. +""" + +import argparse +from collections import deque +from fractions import Fraction +import hashlib +from itertools import product +import json +from pathlib import Path +import subprocess +import sys + +HERE = Path(__file__).resolve().parent +A, B, C = 1, 2, 4 # x + 2*y + 4*z + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def group_mul(g, h): + x, y, z = g & 1, (g >> 1) & 1, g >> 2 + X, Y, Z = h & 1, (h >> 1) & 1, h >> 2 + return (x ^ X) | ((y ^ Y) << 1) | ((z ^ Z ^ (x & Y)) << 2) + + +TABLE = tuple(tuple(group_mul(g, h) for h in range(8)) for g in range(8)) + + +def algebra_mul(a, b): + out = 0 + for g in range(8): + if a >> g & 1: + for h in range(8): + if b >> h & 1: + out ^= 1 << TABLE[g][h] + return out + + +def quotient(a): + # Coefficients in 1, X, Y, XY, YX, packed into five bits. + out = 0 + for g in range(8): + if a >> g & 1: + x, y, z = g & 1, (g >> 1) & 1, g >> 2 + out ^= 1 | (x << 1) | (y << 2) | (z << 3) | ((z ^ (x & y)) << 4) + return out + + +def quotient_mul(a, b): + out = 0 + for i in range(5): + for j in range(5): + if not (a >> i & 1 and b >> j & 1): + continue + k = j if i == 0 else i if j == 0 else 3 if (i, j) == (1, 2) else 4 if (i, j) == (2, 1) else None + if k is not None: + out ^= 1 << k + return out + + +def rank(rows): + pivots = {} + for row in rows: + while row: + bit = row.bit_length() - 1 + if bit in pivots: + row ^= pivots[bit] + else: + pivots[bit] = row + break + return len(pivots) + + +def bmul(left, right): + out = [] + for row in left: + value = 0 + for j, rr in enumerate(right): + if row >> j & 1: + value ^= rr + out.append(value) + return tuple(out) + + +def outer(u, v, r): + return tuple(v if u >> i & 1 else 0 for i in range(r)) + + +def ident(r): + return tuple(1 << i for i in range(r)) + + +def formal_identity(r): + return tuple(tuple(int(i == j) for j in range(r)) for i in range(r)) + + +def append_paid(state, gate): + # Right multiplication by I + ([g]+1) u v^T. + g, u, v = gate + r = len(state) + out = [] + for row in state: + col = 0 + for j in range(r): + if u >> j & 1: + col ^= row[j] + delta = algebra_mul(col, 1 ^ (1 << g)) + out.append(tuple(row[j] ^ (delta if v >> j & 1 else 0) for j in range(r))) + return tuple(out) + + +def legal(gate, r): + g, u, v = gate + return g in (A, B) and 0 < u < 1 << r and 0 < v < 1 << r + + +def replay(r, word): + state = formal_identity(r) + for gate in word: + require(legal(gate, r), "illegal paid factor") + state = append_paid(state, gate) + return state + + +def target(labels, r): + return tuple(tuple((1 << (labels[i] if i < len(labels) else 0)) if i == j else 0 for j in range(r)) for i in range(r)) + + +def direct_words(): + words = {0: ()} + queue = deque([0]) + while queue: + g = queue.popleft() + for letter in (A, B): + h = TABLE[g][letter] + if h not in words: + words[h] = words[g] + (letter,) + queue.append(h) + require(len(words) == 8, "address alphabet coverage") + return words + + +WORDS = direct_words() + + +def counts(labels): + a = b = 0 + for g in labels: + x, y, z = g & 1, (g >> 1) & 1, g >> 2 + a += x + 2 * (1 - x) * z + b += y + 2 * (1 - y) * z + return a, b + + +def witness(labels): + return tuple((g, 1 << i, 1 << i) for i, label in enumerate(labels) for g in WORDS[label]) + + +def coefficients(state): + r = len(state) + return tuple(tuple(sum(((quotient(state[i][j]) >> k) & 1) << j for j in range(r)) for i in range(r)) for k in (1, 2, 3, 4)) + + +def concatenate_rank(left, right): + r = len(left) + return rank(tuple(x | (y << r) for x, y in zip(left, right))) + + +def lower_bounds(state): + a, b, ab, ba = coefficients(state) + # Sylvester, without assuming a or b vanishes. + return (concatenate_rank(a, ab) + rank(a + ba) - rank(a), + concatenate_rank(b, ba) + rank(b + ab) - rank(b)) + + +def scalar_conjugate(state, f, inv): + r = len(state) + left = [] + for row in f: + dst = [0] * r + for i in range(r): + if row >> i & 1: + dst = [x ^ y for x, y in zip(dst, state[i])] + left.append(dst) + return tuple(tuple(xor_values(row[k] for k in range(r) if inv[k] >> j & 1) for j in range(r)) for row in left) + + +def xor_values(values): + out = 0 + for v in values: + out ^= v + return out + + +def scalar_basis(r): + f = ident(r) + ops = [] + for i in range(r - 1): + gate = list(ident(r)) + gate[i] ^= 1 << (i + 1) + f = bmul(f, tuple(gate)) + ops.append(tuple(gate)) + inv = ident(r) + for gate in reversed(ops): + inv = bmul(inv, gate) + require(bmul(f, inv) == ident(r), "scalar basis inverse") + return f, inv + + +def conjugate_word(word, f, inv): + r = len(f) + out = [] + for g, u, v in word: + uu = sum(((row & u).bit_count() & 1) << i for i, row in enumerate(f)) + vv = bmul((v,), inv)[0] + require(rank(bmul(bmul(f, outer(u, v, r)), inv)) == 1, "conjugated factor rank") + out.append((g, uu, vv)) + return tuple(out) + + +def regular_rows(state): + # Expand formal coefficients in the left regular representation. + r = len(state) + rows = [0] * (8 * r) + for i in range(r): + for j in range(r): + for g in range(8): + if state[i][j] >> g & 1: + for h in range(8): + rows[8 * i + TABLE[g][h]] ^= 1 << (8 * j + h) + return rows + + +def update_digest(digest, rows): + digest.update(json.dumps(rows, separators=(",", ":")).encode() + b"\n") + + +def check_algebra(): + for g, h in product(range(8), repeat=2): + require(quotient(1 << TABLE[g][h]) == quotient_mul(quotient(1 << g), quotient(1 << h)), "quotient homomorphism") + for a, b, c in product(range(32), repeat=3): + require(quotient_mul(quotient_mul(a, b), c) == quotient_mul(a, quotient_mul(b, c)), "quotient associativity") + for g in range(8): + require(counts((g,)) == (WORDS[g].count(A), WORDS[g].count(B)), "direct word fails separate minima") + # Exact shortest paths independently reprice the eight address endpoints. + tariffs = ((1, 1), (1, 7), (7, 1), (Fraction(2, 3), Fraction(5, 7))) + for alpha, beta in tariffs: + dist = {0: Fraction(0)} + done = set() + while len(done) < 8: + g = min((x for x in dist if x not in done), key=dist.get) + done.add(g) + for label, price in ((A, alpha), (B, beta)): + h = TABLE[g][label] + cost = dist[g] + price + if h not in dist or cost < dist[h]: + dist[h] = cost + for g in range(8): + p, q = counts((g,)) + require(dist[g] == alpha * p + beta * q, "weighted address bound") + return {"group_products": 64, "quotient_associativity_triples": 32768, "exact_tariff_endpoints": 32} + + +def check_sylvester(): + checked = nonzero = 0 + for n in range(4): + for x in product(range(1 << n), repeat=2): + for y in product(range(4), repeat=n): + z = bmul(x, y) + require(rank(x) + rank(y) - rank(z) <= n, "Sylvester bound") + checked += 1 + nonzero += bool(rank(z)) + return {"sylvester_pairs": checked, "sylvester_nonzero_products": nonzero} + + +def check_witnesses(): + digest = hashlib.sha256() + fixtures = columns = controls = 0 + for t in range(1, 4): + for labels in product(range(8), repeat=t): + for extra in (0, 1): + r = t + extra + word = witness(labels) + expected = target(labels, r) + state = replay(r, word) + require(state == expected, "full formal dirty boundary") + require(lower_bounds(state) == counts(labels), "mixed endpoint rank formula") + for conjugated in (False, True): + if conjugated: + f, inv = scalar_basis(r) + state = replay(r, conjugate_word(word, f, inv)) + require(state == scalar_conjugate(expected, f, inv), "scalar-conjugated dirty boundary") + require(lower_bounds(state) == counts(labels), "basis-invariant lower bound") + update_digest(digest, regular_rows(state)) + fixtures += 1 + columns += 8 * r + if extra and word: + bad = word + ((A, 1 << t, 1 << t),) + require(replay(r, bad) != expected, "unrestored dirty role must reject") + controls += 1 + if any(labels): + word = witness(labels) + for i in range(len(word)): + require(replay(t, word[:i] + word[i + 1:]) != target(labels, t), "deleted paid call must reject") + controls += 1 + # All eight labels together, including two arbitrary restored dirty roles. + labels = tuple(range(8)) + word = witness(labels) + require(replay(10, word) == target(labels, 10), "all-label boundary") + require(lower_bounds(target(labels, 10)) == (8, 8), "all-label cost") + return {"witness_fixtures": fixtures, "faithful_columns": columns, "witness_digest": digest.hexdigest(), "all_eight_labels_bill": [8, 8], "boundary_mutation_controls": controls} + + +def check_all_short_words(): + # Every r=2 expanded-alphabet word of length <=4, including nilpotents. + alphabet = tuple((g, u, v) for g in (A, B) for u in range(1, 4) for v in range(1, 4)) + identity = formal_identity(2) + checked = endpoints = 0 + pair_digest = hashlib.sha256() + + def visit(state, depth, na, nb): + nonlocal checked, endpoints + bound_a, bound_b = lower_bounds(state) + require(bound_a <= na and bound_b <= nb, "short-word coefficient-rank inequality") + checked += 1 + if state[0][1] == state[1][0] == 0 and all(v > 0 and v & (v - 1) == 0 for v in (state[0][0], state[1][1])): + labels = (state[0][0].bit_length() - 1, state[1][1].bit_length() - 1) + need_a, need_b = counts(labels) + require(need_a <= na and need_b <= nb, "short formal endpoint violates proposed tariff") + endpoints += 1 + if depth == 2: + update_digest(pair_digest, regular_rows(state)) + if depth == 4: + return + for gate in alphabet: + visit(append_paid(state, gate), depth + 1, na + (gate[0] == A), nb + (gate[0] == B)) + + visit(identity, 0, 0, 0) + return {"expanded_r2_alphabet": len(alphabet), "words_through_length_four": checked, "diagonal_endpoint_words": endpoints, "two_factor_digest": pair_digest.hexdigest()} + + +def check_controls(): + # The quotient is deliberately not a formal endpoint acceptance test. + kernel = algebra_mul(1 ^ (1 << A), 1 ^ (1 << C)) + require(kernel != 0 and quotient(kernel) == 0, "nonfaithful quotient control") + good = target((C,), 2) + bad = ((good[0][0], kernel), good[1]) + require(coefficients(bad) == coefficients(good), "kernel perturbation invisible to rank proof") + require(bad != good and regular_rows(bad) != regular_rows(good), "formal and faithful controls reject kernel") + # It is invisible on all clean-extra inputs but changes a dirty-extra column. + differences = [x ^ y for x, y in zip(regular_rows(bad), regular_rows(good))] + require(all(d & 255 == 0 for d in differences) and any(d >> 8 for d in differences), "clean-only false acceptance control") + # The central-only proof cannot be copied verbatim for a noncentral target. + state = replay(1, ((A, 1, 1),)) + require(lower_bounds(state) == (1, 0), "rank(A) correction is essential") + require(2 * rank(coefficients(state)[0]) > 1, "zero-sum shortcut would be false") + # Simply exchanging x and y misses the xy term in the quotient. + wrong = lambda g: ((g >> 1) & 1) | ((g & 1) << 1) | (g & 4) + require(wrong(TABLE[A][B]) != TABLE[wrong(A)][wrong(B)], "missing xy correction must fail") + require(not legal((C, 1, 1), 1), "central address primitive outside alphabet") + require(not legal((A, 0, 1), 1), "zero scalar factor outside alphabet") + # Four full-rank coordinatewise macros attain two central targets. Each + # macro is rank two, so charging it once would change the legal alphabet. + require(rank(ident(2)) == 2, "higher-rank control") + state = formal_identity(2) + for label in WORDS[C]: + state = tuple(tuple(algebra_mul(entry, 1 << label) for entry in row) for row in state) + require(state == target((C, C), 2), "rank-two macro witness") + require(len(WORDS[C]) < sum(lower_bounds(state)), "unit-priced rank-two macros violate the intended bill") + nilpotent = (A, 1, 2) + require(replay(2, (nilpotent, nilpotent)) == formal_identity(2), "nilpotent paid factor remains reversible") + return {"model_controls": ["nonfaithful_quotient_kernel", "formal_kernel_rejection", + "faithful_kernel_rejection", "clean_extra_blind_spot", "nonzero_first_order_correction", + "missing_xy_correction", "central_label_restriction", "nonzero_factor_restriction", + "unit_priced_rank_two_escape", "nilpotent_reversibility"], + "nonfaithful_kernel_support": [g for g in range(8) if kernel >> g & 1]} + + +def run(): + result = {"schema_version": 1, "scope": "Finite evidence for the written all-register mixed UT3 tariff theorem; no new kappa."} + for check in (check_algebra, check_sylvester, check_witnesses, check_all_short_words, check_controls): + result.update(check()) + independent = json.loads(subprocess.check_output([sys.executable, "-I", "-B", str(HERE / "independent.py")], text=True, timeout=120)) + for field in ("witness_fixtures", "faithful_columns", "witness_digest", "two_factor_digest"): + require(independent[field] == result[field], "separate regular implementation disagrees: " + field) + result["independent"] = independent + return result + + +def canonical(data): + return json.dumps(data, sort_keys=True, separators=(",", ":")) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", help="print freshly computed finite evidence without modifying files") + args = parser.parse_args() + try: + result = run() + if args.emit: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + expected = json.loads((HERE / "CERTIFICATE.json").read_text()) + require(canonical(result) == canonical(expected), "committed certificate differs from exact replay") + print("PASS_UT3_MIXED_TARGET_TARIFFS words=" + str(result["words_through_length_four"]) + " witnesses=" + str(result["witness_fixtures"]) + " no_new_kappa") + except (OSError, ValueError, KeyError, subprocess.SubprocessError) as exc: + parser.exit(1, "FAIL_UT3_MIXED_TARGET_TARIFFS: " + str(exc) + "\n") + + +if __name__ == "__main__": + main()