diff --git a/research/ut3-rank-bounded-block-calls/CERTIFICATE.json b/research/ut3-rank-bounded-block-calls/CERTIFICATE.json new file mode 100644 index 0000000000..46566c69eb --- /dev/null +++ b/research/ut3-rank-bounded-block-calls/CERTIFICATE.json @@ -0,0 +1,75 @@ +{ + "all_binary_couplings_rank_counts": { + "1": [ + 1, + 1 + ], + "2": [ + 1, + 9, + 6 + ], + "3": [ + 1, + 49, + 294, + 168 + ] + }, + "arbitrary_two_factor_formal_regular_comparisons": 900, + "exact_rational_tariff_checks": 306, + "formula": "t=max(2,ceil(2w/k)); counts=(t,t); rank_mass=(2w,2w)", + "forward_inverse_regular_basis_columns": 16160, + "full_formal_and_regular_fixtures": 102, + "omitted_call_controls": 62, + "other_model_controls": 10, + "pilot": { + "invoice": { + "counts": [ + 3, + 3 + ], + "rank_mass": [ + 6, + 6 + ] + }, + "k": 2, + "r": 5, + "supports": [ + [ + 0, + 1 + ], + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 0, + 2 + ], + [ + 1, + 2 + ], + [ + 1, + 2 + ] + ], + "w": 3 + }, + "profiles_sha256": "3250f60623b54a2f4da0409a2e7ed5d6431e281e3c6f58bb3086c5ef175b3e21", + "quotient_associativity_triples": 32768, + "quotient_products": 64, + "result": "sharp rank-cap invocation count; no new kappa", + "same_label_rank_decompositions": 1060, + "scalar_gauged_fixtures": 1, + "schema_version": 1, + "short_words": 27931 +} diff --git a/research/ut3-rank-bounded-block-calls/README.md b/research/ut3-rank-bounded-block-calls/README.md new file mode 100644 index 0000000000..dc0d1bac91 --- /dev/null +++ b/research/ut3-rank-bounded-block-calls/README.md @@ -0,0 +1,234 @@ +# Sharp invocation count for rank-bounded UT3 block calls + +**Scoped alphabet extension; no new kappa.** For `w` central UT3 targets, +arbitrary restored dirty workspace, and paid a/b calls of scalar rank at most +`k`, the exact minimum number of calls is + +`2t`, where `t = max(2, ceil(2w/k))`. + +Search aliases: D8 (the dihedral group of order eight), UT3(F2), UT_3(F2), +Heisenberg group mod 2, central commutator, rank cap, higher-rank block calls. + +Every word has at least `2w` charged rank units of **each** letter. One +construction simultaneously attains the minimum invocation count and both +rank bounds. Under nonnegative per-letter complete prices +`alpha_g + beta_g rank(N)`, the sharp abstract tariff is therefore + +`t(alpha_a + alpha_b) + 2w(beta_a + beta_b)`. + +The smallest batching improvement is `w=3,k=2`: six rank-two calls, rather +than twelve rank-one calls or eight calls from disjoint blocks of sizes two +and one. All three constructions charge twelve total rank units. At uniform +price `alpha + beta rank`, their bills are respectively `6alpha+12beta`, +`12alpha+12beta`, and `8alpha+12beta`. This improves an invocation overhead +only when the hypothetical block call really has that complete price. +It is not a recursive-moment or physical supplier improvement. + +## Exact model and predecessor boundary + +Let `G=UT_3(F2)`, with triples `(u,v,z)` and group product + +`(u,v,z)(U,V,Z)=(u+U,v+V,z+Z+uV)`. + +Set `a=(1,0,0)`, `b=(0,1,0)`, `c=abab=(0,0,1)`. Work in the **full formal** +group algebra `R=F2[G]` on any finite `r>=w>=1` scalar registers. For an integer +`k>=1`, the expanded paid alphabet is + +`D_N(g)=I+([g]+1)N`, `g in {a,b}`, `1<=rank_F2(N)<=k`. + +`N` is any binary `r-by-r` matrix; it need not be idempotent. This is one +optimistically priced **block primitive**, not a claim that its implementation +costs one rank-one call. Each factor is reversible with inverse itself: +`([g]+1)^2=0` gives `D_N(g)^2=I` even when `N^2` is neither zero nor `N`. +The endpoint is `diag([c] repeated w, 1 repeated r-w)` on arbitrary inputs. +All restored roles, every invocation and its full scalar rank are counted. +There are no free address maps, central-letter calls, clean ancillas, COPY, +ERASE, or uncharged inverse calls. + +Scalar `GL_r(F2)` mixing is free **only in this abstract screening model**. +Conjugate it through paid factors, retaining scalar rank. Augmentation sends +every paid factor and the target to identity, so the residual free scalar +map must be identity. The expanded alphabet contains all these conjugates. +Consequently the normalized paid-word model covers arbitrary free scalar +mixing with the declared complete dirty boundary. + +steph4n-gh's [PR1573](https://github.com/CrocSwap/integer-mult-bounds/pull/1573) +already proves `4w` for rank-one idempotents with arbitrary workspace. +Arham Tahir's [PR1589](https://github.com/CrocSwap/integer-mult-bounds/pull/1589) +extends that bound to all rank-one matrices; Hanson Sun's +[PR1607](https://github.com/CrocSwap/integer-mult-bounds/pull/1607) treats mixed +rank-one targets. Their zero-sum/coefficient-span proof supplies the method +below. The new part is the sharp rank-cap invocation count, cyclic block +construction and simultaneously optimal rank/invocation tariff. At `k=1` it specializes +to their central-only result. woklerx's +[PR1841](https://github.com/CrocSwap/integer-mult-bounds/pull/1841) adds a paid +central label while keeping scalar rank one, a different changed premise. +Josie Elliston's [PR1792](https://github.com/CrocSwap/integer-mult-bounds/pull/1792) +already observes that a rank-s coupling splits into s same-label rank-one +calls, preserving the rank-linear bill. That fact and the `4w` rank-volume +floor are credited consequences of predecessor work, not new savings here. +Exact heads are recorded in [SOURCES.json](SOURCES.json). No predecessor code +or source archive is imported. + +## Uniform lower bound + +The predecessor floor can also be obtained by splitting each rank-d `N` +as a sum of d rank-one matrices. Since `([g]+1)^2=0`, their same-label factors +multiply to `D_N(g)`. The rank-one lower bound therefore applies to total +rank mass. The self-contained coefficient argument below records that +inherited implication without requiring a pending executable or theorem. + +Use the predecessor quotient + +`A=F2/(X^2,Y^2, all monomials of length >=3)`. + +Its basis is `1,X,Y,XY,YX`; the map + +`(u,v,z) -> 1+uX+vY+zXY+(z+uv)YX` + +preserves the displayed group law. Thus `a->1+X`, `b->1+Y`, +`c->1+XY+YX`. This is only a necessary-condition quotient; acceptance of +the upper words uses the full formal algebra. Put `Q=diag(I_w,0)`, rank `w`. +The target's degree-one coefficients vanish and its two mixed coefficients +both equal `Q`. + +For the a factors write `N_i=U_i V_i`, where `d_i=rank(N_i)`, +`U_i` has `d_i` columns and `V_i` has `d_i` rows. Concatenate them into +`U=(U_1 ... U_p)` and `V=(V_1^T ... V_p^T)^T`, with inner dimension +`s_a=sum_i d_i`. The `X` coefficient gives `UV=sum_i N_i=0`. + +The `XY` coefficient is a sum of `N_i` times later b factors, so its column +space is contained in `col(U)`. The `YX` coefficient is a sum of earlier b +factors times `N_i`, so its row space is contained in `row(V)`. Since both +are `Q`, `rank(U)>=w` and `rank(V)>=w`. But `UV=0` implies +`image(V) subset kernel(U)` inside `F2^{s_a}`, hence + +`s_a >= rank(U)+rank(V) >= 2w`. + +Exchanging a,b proves `s_b>=2w`. No scalar commutation, idempotence, +determinant parity, register bound, or finite-search assumption is used. +Since every rank is at most `k`, `p,q >= ceil(2w/k)`. Each letter must occur +at least twice: zero occurrences cannot give the mixed coefficient `Q`, +and one occurrence would require its nonzero `N` to equal zero in the +degree-one coefficient. Therefore `p,q>=t`. + +For nonnegative tariff coefficients the complete bill is at least +`t(alpha_a+alpha_b)+2w(beta_a+beta_b)`. Negative prices are outside the model. + +## Uniform attaining construction + +Let `t=max(2,ceil(2w/k))`. Assign target coordinate `i=0,...,w-1` to two +block indices + +`2i mod t` and `(2i+1) mod t`. + +These indices differ because `t>=2`. For each block `j`, let `P_j` be the +diagonal projector onto its assigned target coordinates, zero on all dirt. +The `2w` consecutive residues distribute across `t` indices with loads +`floor(2w/t)` or `ceil(2w/t)`. Since `t<=2w` and `t>=2w/k`, every block is +nonempty and has rank at most `k`. Execute, in increasing block order, + +`D_{P_j}(a) D_{P_j}(b)`. + +Each target belongs to exactly two blocks. Its complete formal word is +`abab=c`; all other factors act identically there. Every extra dirty +coordinate sees only identity. Thus the word has the required full endpoint, +`t` calls of each letter, and rank mass `sum_j rank(P_j)=2w` per letter. +There is no preparation or extra workspace requirement. Adding any number +of identity roles preserves the construction. This proves the sharp count +and tariff for every finite `r>=w` and integer `k>=1`, including `k>w`. + +For `w=3,k=2`, the supports are `{0,1}`, `{0,2}`, `{1,2}`. Apply a then b +on each support. Overlapping these blocks removes two invocations relative +to disjoint batching; it does not remove any charged rank. + +## Exact evidence and reproduction + +The written proofs establish the arbitrary-size statement. +[verify.py](verify.py) supplies bounded exact corroboration: + +- All 64 group products check the quotient homomorphism; all 32,768 quotient + triples check associativity. +- All 530 binary scalar matrices at `r=1,2,3`, including zero as an algebra + control, check two rank implementations, rank factorizations, all 1,060 + same-label decompositions and full formal + and faithful regular involutions for both letters. The `r=3` rank counts + are `1,49,294,168` at ranks `0,1,2,3`. +- All 27,931 two-register words through three calls, over both letters and + all fifteen nonzero scalar matrices, check ordered coefficients against + both a separate dynamic recurrence and full-formal quotient projection. + Actual carrier spans and zero-sum rank bounds are checked. All 900 ordered + two-factor products additionally compare formal and faithful regular maps. +- 102 attaining fixtures cover `w=1..12`, `k=1..w+2`, each with two dirty + roles. Both engines check complete forward and inverse operators, including + 16,160 regular basis columns and exact counts/rank invoices. +- A scalar-conjugated pilot mixes dirty input into a target and restores the + complete boundary with the two permitted free scalar maps. Omitting those + maps fails in both engines. Sixty-two single-call omissions and ten model, + rank-invoice, label and dirty-boundary controls reject. A nonzero formal + off-diagonal perturbation in the quotient kernel is rejected by the faithful + engine even though the lower-bound quotient cannot see it. 306 exact rational + tariff fixtures include zero overhead, pure overhead and unequal prices. + +The formal engine uses triple convolution. The regular engine uses literal +binary 3-by-3 address matrices and their faithful eight-element action, with +different enumeration and multiplication. They share scalar bit-matrix +arithmetic and were written in one session; this is not independent human +review. [CERTIFICATE.json](CERTIFICATE.json) stores the deterministic receipt +and construction-profile digest. `--emit` prints a fresh receipt without +changing the package. Checks remain active under `-O`. + +From the repository root, standard-library Python 3.12: + +```sh +python -I -O -B research/ut3-rank-bounded-block-calls/verify.py +python -I -B research/ut3-rank-bounded-block-calls/test_verify.py +python scripts/research_package.py --package research/ut3-rank-bounded-block-calls --check-only +python scripts/research_package.py --package research/ut3-rank-bounded-block-calls +``` + +The registered command covers normal/optimized checking, read-only source +export, regenerated receipt equality, and certificate-corruption rejection. +The source exports need only verifier and certificate; generic provenance +checks additionally require Git history. Task selection, scope, exact main, +overlap and validation environment are in [TASK.json](TASK.json). + +## Limits + +The rank units above are **scalar coupling ranks in this formal alphabet**, +not an admitted supplier's recursive child ranks. Rank-linear pricing gives +the same `4w` rank bill at every cap. A nonlinear recursive tariff requires +its own analysis; this result does not optimize it. The expanded block +primitive, free scalar maps and fixed invocation overhead have no supplied +physical realization, rational-frame translation or H1-H5 admission. +Selected-source orientation passed; the selected cold replay, compiler, +common-label realization, hosting/ownership, precision/tape, outer analytic +transfer, Lean proof and independent human review were not performed. +No new multiplication exponent or maintainer acceptance is claimed. + +## Open next questions + +Can a physical bit interface realize one rank-k block call below the sum of +its rank-one complete prices? That determines whether the invocation savings +matter. Start with this `w=3,k=2` six-call boundary and charge frame changes, +scalar preparation, hosting, precision, restoration and dispatch against all +twelve rank-one calls. The blocker is a legal physical realization; neither +formal rank nor fewer invocations provides it. Structured scope and this +handoff are in [TASK.json](TASK.json). + +## Credit and license + +Credit steph4n-gh/PR1573 for the all-register rank-one central bound and +zero-sum rank argument; Arham Tahir/PR1589 for the nilpotent rank-one extension +and two-coefficient quotient; Hanson Sun (@bbMisk)/PR1607 for mixed-target +coefficient tariffs; woklerx/PR1841 for the distinct priced-central alphabet. +Credit Josie Elliston/PR1792 for the family index, D8/UT3 alias warning and +explicit rank-s decomposition/rank-linear pricing observation. +Retain juper997/PR1478 and woklerx/PR1443's finite UT3/D8 predecessors, +Gareth Davidson (@bitplane)/PR1333's scalar-normalization context and the +eumemic/PR288, Ali Romman/PR468 and David Govea/PR720 register-model lineage. +No literature-priority claim is made for rank-nullity or cyclic load balancing. + +Prepared by **Arham Tahir with substantial OpenAI Codex assistance** in proof, +implementation, verification and writing. No subagents or independent human +proof review. New work is Apache-2.0; frozen inputs and notices are unchanged. diff --git a/research/ut3-rank-bounded-block-calls/SOURCES.json b/research/ut3-rank-bounded-block-calls/SOURCES.json new file mode 100644 index 0000000000..c5e9293496 --- /dev/null +++ b/research/ut3-rank-bounded-block-calls/SOURCES.json @@ -0,0 +1,65 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + } + ], + "contextual_references": [ + { + "pr": 1573, + "head": "0b8c5a69297c794f2de22c04494c83e41300ae36", + "path": "research/ut3-commutator-all-registers/README.md", + "git_blob": "4a6a4ee9d995818348b3b853a95500dcce81228d", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/0b8c5a69297c794f2de22c04494c83e41300ae36/research/ut3-commutator-all-registers/README.md", + "sha256": "fdd5405da1c0535a407013f2a4628a07dae4957fd9fb776cd14f05315d1aa26b", + "usage": "Inspected reference prose at exact head, not vendored or needed for executable replay; pending work is not maintainer acceptance." + }, + { + "pr": 1589, + "head": "010ec8c01c0edbbb08b541be236ab78d096f2ca1", + "path": "research/ut3-two-targets-any-registers/README.md", + "git_blob": "3fc4f569a2e9bc81a1f61bc8343a276671a2d13f", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/010ec8c01c0edbbb08b541be236ab78d096f2ca1/research/ut3-two-targets-any-registers/README.md", + "sha256": "f879e3009b1fd5c625480ef92bdc454030ae62e7b378af7869e188df718e7399", + "usage": "Inspected reference prose at exact head, not vendored or needed for executable replay; pending work is not maintainer acceptance." + }, + { + "pr": 1607, + "head": "9d6117918025cee6a0c5b7ef30ff8d936ca0621f", + "path": "research/ut3-mixed-target-tariffs/README.md", + "git_blob": "1778bfdb77e3c02eaa628da3a85b32fd37939a9a", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/9d6117918025cee6a0c5b7ef30ff8d936ca0621f/research/ut3-mixed-target-tariffs/README.md", + "sha256": "7c27f4cb1f97f65778c6b9e7a0025fdfdcb7cd1f0cf6ab34c14ece7db1b88124", + "usage": "Inspected reference prose at exact head, not vendored or needed for executable replay; pending work is not maintainer acceptance." + }, + { + "pr": 1841, + "head": "0c305488a4e27cd96edd61460bb5429ed5e8abf0", + "path": "research/ut3-priced-central-calls/README.md", + "git_blob": "da8daef118849ba53b31d619bc28edabafe77bc7", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/0c305488a4e27cd96edd61460bb5429ed5e8abf0/research/ut3-priced-central-calls/README.md", + "sha256": "d6f51fee5fdef526460f4d7d04e7ddc0e44806a0eae0f7d8cbe32a831cc6f81b", + "usage": "Inspected reference prose at exact head, not vendored or needed for executable replay; pending work is not maintainer acceptance." + }, + { + "pr": 1792, + "head": "cc3a4adbae23fb07687803d1361bb7a1bcd449b0", + "path": "research/ut3-central-commutator-index/README.md", + "git_blob": "7a91b02231c5ff8445ec41cfd42c65c8e9e719fb", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/cc3a4adbae23fb07687803d1361bb7a1bcd449b0/research/ut3-central-commutator-index/README.md", + "sha256": "c2df9a467945360e333fe475c2d0d9fa2961d2ab4fcb252a48faf7cb384dfb46", + "usage": "Inspected reference prose at exact head, not vendored or needed for executable replay; pending work is not maintainer acceptance." + } + ] +} diff --git a/research/ut3-rank-bounded-block-calls/TASK.json b/research/ut3-rank-bounded-block-calls/TASK.json new file mode 100644 index 0000000000..081d4379cf --- /dev/null +++ b/research/ut3-rank-bounded-block-calls/TASK.json @@ -0,0 +1,170 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "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": "Sharp call count and affine rank tariff for w central UT3 targets, arbitrary finite restored dirty workspace, paid a/b calls with any nonzero binary scalar matrix of rank at most k.", + "scope_change_reason": "Use the allowed specified nonabelian alphabet variation: enlarge the rank-one UT3 alphabet to paid rank-bounded couplings. Existing PR1573/1589 settle the rank-one case, so a new rank-cap construction and matching rank-volume bound are needed.", + "bottleneck_link": "Tests whether larger-rank interface calls reduce complete invocation overhead; separates fewer calls from unchanged charged rank mass. This is an abstract bit-interface screening result, not a hosted supplier.", + "budget_minutes": 60, + "stop_rule": "One approximately 60-minute session: prove or falsify the uniform rank-cap construction, replay full formal and faithful regular dirty endpoints, test boundaries and mutations, then package one result. No larger heuristic search.", + "outcome": "completed", + "evidence": "README uniform rank-volume proof and cyclic-incidence construction; deterministic full receipt: 102 full formal/faithful regular forward/inverse dirty fixtures, 27931 short words, 900 arbitrary two-factor comparisons, 62 omission and 10 model controls, 306 exact tariffs. No supplier admission.", + "author": "Arham Tahir with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in proof, code, verification and writing. No subagents and no independent human proof review.", + "open_questions": [ + { + "question": "Can one physical bit interface realize a rank-k block call below the sum of k rank-one complete call prices?", + "why_it_matters": "The abstract gain is entirely reduced invocation overhead; rank-linear pricing gives no rank saving.", + "first_step": "Implement the w=3,k=2 six-call boundary and price scalar preparation, frame changes, hosting, precision, restoration and dispatch against twelve rank-one calls.", + "blocked_by": "The formal nonabelian operator model has no supplied rational-frame/physical realization or supplier admission." + } + ], + "chooser_nonce": "c79b0a54a0d8afe483e69e03ae03fa5b", + "scope_key": "UT3F2/a-b-only/central-targets/rank-cap-k/affine-rank-tariff/cyclic-pair-incidence", + "selected_method": "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "optimistic_budget": { + "pilot": { + "w": 3, + "rank_cap": 2, + "calls": 6, + "total_paid_rank": 12 + }, + "tariff": "alpha_g + beta_g rank(N) per complete call, all coefficients nonnegative; physical implementation not established", + "required_observable_improvement": "Beat twelve rank-one invocations and eight naive rank-two block invocations at unchanged twelve total rank units when invocation overhead is positive." + }, + "predecessors": [ + { + "pr": 1573, + "head": "0b8c5a69297c794f2de22c04494c83e41300ae36", + "credit": "steph4n-gh: all-register rank-one idempotent 4w bound and zero-sum rank argument" + }, + { + "pr": 1589, + "head": "010ec8c01c0edbbb08b541be236ab78d096f2ca1", + "credit": "Arham Tahir: nilpotent rank-one extension and two-mixed-coefficient quotient" + }, + { + "pr": 1607, + "head": "9d6117918025cee6a0c5b7ef30ff8d936ca0621f", + "credit": "Hanson Sun/bbMisk: mixed-target rank-one tariffs" + }, + { + "pr": 1841, + "head": "0c305488a4e27cd96edd61460bb5429ed5e8abf0", + "credit": "woklerx: priced central-label extension, explicitly retains rank-one couplings" + }, + { + "pr": 1792, + "head": "cc3a4adbae23fb07687803d1361bb7a1bcd449b0", + "credit": "Josie Elliston: family/alias index and explicit rank-s decomposition; rank-linear floor is corroboration, not a new savings claim." + } + ], + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1890", + "validation_environment": { + "python": "3.12.10", + "implementation": "CPython", + "platform": "Windows-11-10.0.26200-SP0", + "dependencies": "standard library only" + }, + "overlap_entry": { + "open_prs_including_drafts": 542, + "discussion_body_comment_reply_records": 528, + "prs_fetched_at": "2026-10-14T13:22:59.338711+00:00", + "discussions_fetched_at": "2026-10-14T13:24:01.750347+00:00", + "complete_pagination": true, + "limits": "PR title/body, Discussion body/comment/reply and local top-level README/TASK/ledger; no all-diff search or novelty guarantee. Repository helper searched an independently refreshed authenticated API cache offline." + }, + "overlap_final": { + "open_prs": { + "fetched_at": "2026-10-14T13:41:23.310345+00:00", + "complete_pagination": true, + "records": 556 + }, + "discussions": { + "fetched_at": "2026-10-14T13:42:26.477973+00:00", + "complete_pagination": true, + "records": 536 + }, + "local_records": 873, + "terms": [ + "UT3", + "rank-bounded", + "rank cap", + "block calls", + "D8", + "dihedral", + "rank-s" + ], + "report_sha256": "a39943f590dc5369261295711df581731deea9c246f8fb19eb29f70afec494bc", + "nearest_heads": { + "1857": "dd070f72856c6ba0a2e8b4b7b15a38cb24441daa", + "1841": "0c305488a4e27cd96edd61460bb5429ed5e8abf0", + "1836": "0a62e3f1c0ea493ddb83f25b91c5548c87978bcc", + "1792": "cc3a4adbae23fb07687803d1361bb7a1bcd449b0", + "1764": "811a8e715b6b888c94f0d9da810541a4639c1ff9", + "1607": "9d6117918025cee6a0c5b7ef30ff8d936ca0621f", + "1589": "010ec8c01c0edbbb08b541be236ab78d096f2ca1", + "1573": "0b8c5a69297c794f2de22c04494c83e41300ae36" + }, + "assessment": "No matching rank-cap invocation theorem found; inspected PR1792 rank-linear observation and credited it. PR1841 adds the central letter at rank one; PR1764/1836/1857 concern complex interfaces or planning ranks. All predecessor heads remain unchanged.", + "limitations": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission. Offline helper queried a separately authenticated fresh fully paginated snapshot. D8/dihedral aliases were also queried; exact-word matching removes incidental hexadecimal D8 matches. No novelty guarantee." + }, + "validation": { + "status": "passed", + "commands": [ + "python -B scripts/research_baseline.py", + "python -I -B research/ut3-rank-bounded-block-calls/verify.py --emit", + "python -B scripts/research_package.py --package research/ut3-rank-bounded-block-calls --check-only", + "UT3_TEST_TMPDIR= python -B scripts/research_package.py --package research/ut3-rank-bounded-block-calls" + ], + "registered_result": "PASS_REGISTERED_RESEARCH_PACKAGE; optimized full replay and two CLI/evidence-integrity test groups pass, including normal/optimized export and four certificate mutations.", + "test_elapsed_seconds": "27.080 for final two test groups; no performance claim", + "resolved_local_failures": "Windows sandbox default temp denied file writes; explicit workspace scratch directory passed. A test initially misplaced --emit before the script path; corrected and all final controls rerun.", + "unrun": "Full selected cold replay, physical/compiler/common-label realization, hosting, precision/tape, nonlinear recursive tariff, outer transfer, Lean and independent human review.", + "artifacts": { + "verify.py": "0f7c53be71f4cbe9c7bbb6b0a1172c2b68bf5974308031e6b76a6c0cf876e542", + "test_verify.py": "237a3532bf9099e018f747b08c22c1c8838d1750640d0e82a54b457dd27fa6ee", + "README.md": "822574c7040b5571d729960951425a1ad9742ae8541a2af2882733f952975b5d", + "CERTIFICATE.json": "451fab7e802276c159988333b5a681101902df60199b368e3b0fb892ad6547b9", + "SOURCES.json": "95b2121ea7f86d7d6bce5f734d2beca6254c85db60e490c8ae9dca3011f692d5" + } + } +} diff --git a/research/ut3-rank-bounded-block-calls/VERIFY.json b/research/ut3-rank-bounded-block-calls/VERIFY.json new file mode 100644 index 0000000000..ca6a5685f0 --- /dev/null +++ b/research/ut3-rank-bounded-block-calls/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Full formal and faithful regular endpoints/inverses, rank volumes and tariffs, quotient/rank controls and exact certificate equality under optimized Python." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Normal/optimized read-only CLI replay, minimal source-export replay, deterministic receipt regeneration, four certificate-corruption controls including duplicate keys and Boolean counts." + } + ] +} diff --git a/research/ut3-rank-bounded-block-calls/test_verify.py b/research/ut3-rank-bounded-block-calls/test_verify.py new file mode 100644 index 0000000000..b3ddad373e --- /dev/null +++ b/research/ut3-rank-bounded-block-calls/test_verify.py @@ -0,0 +1,66 @@ +"""CLI and evidence-integrity controls. Apache-2.0; AI-assisted by OpenAI Codex.""" +import json +import os +from pathlib import Path +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent + + +class EvidenceTests(unittest.TestCase): + def command(self, package, *options): + interpreter_options = [option for option in options if option == '-O'] + script_options = [option for option in options if option != '-O'] + return subprocess.run([sys.executable, '-I', *interpreter_options, '-B', str(package / 'verify.py'), *script_options], + capture_output=True, text=True, timeout=60, + env=dict(os.environ, PYTHONDONTWRITEBYTECODE='1')) + + def test_normal_and_optimized_read_only_replay(self): + before = {p.name: p.read_bytes() for p in HERE.iterdir() if p.is_file()} + for options in ((), ('-O',)): + answer = self.command(HERE, *options) + self.assertEqual(answer.returncode, 0, answer.stderr) + self.assertIn('PASS_UT3_RANK_CAP', answer.stdout) + self.assertEqual(before, {p.name: p.read_bytes() for p in HERE.iterdir() if p.is_file()}) + + def test_source_export_and_evidence_corruption(self): + # No Git, parent scripts, writable package or network required by the verifier. + scratch = os.environ.get('UT3_TEST_TMPDIR') + with tempfile.TemporaryDirectory(prefix='ut3-rank-cap-', dir=scratch) as temporary: + package = Path(temporary) + if scratch: + self.assertEqual(package.resolve().parent, Path(scratch).resolve()) + for name in ('verify.py', 'CERTIFICATE.json'): + (package / name).write_bytes((HERE / name).read_bytes()) + for options in ((), ('-O',)): + good = self.command(package, *options) + self.assertEqual(good.returncode, 0, good.stderr) + fresh = self.command(package, '--emit') + self.assertEqual(fresh.returncode, 0, fresh.stderr) + certificate = json.loads((package / 'CERTIFICATE.json').read_text()) + self.assertEqual(json.loads(fresh.stdout), certificate) + mutants = [] + changed = json.loads(json.dumps(certificate)) + changed['pilot']['invoice']['rank_mass'][1] = 5 + mutants.append(json.dumps(changed)) + changed = json.loads(json.dumps(certificate)) + changed['profiles_sha256'] = '0' * 64 + mutants.append(json.dumps(changed)) + changed = json.loads(json.dumps(certificate)) + changed['scalar_gauged_fixtures'] = True # bool must not pass as integer one. + mutants.append(json.dumps(changed)) + mutants.append('{"schema_version":1,' + json.dumps(certificate)[1:]) + for text in mutants: + (package / 'CERTIFICATE.json').write_text(text) + for options in ((), ('-O',)): + bad = self.command(package, *options) + self.assertNotEqual(bad.returncode, 0) + self.assertTrue('certificate mismatch' in bad.stderr or 'duplicate JSON key' in bad.stderr, + bad.stderr) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/ut3-rank-bounded-block-calls/verify.py b/research/ut3-rank-bounded-block-calls/verify.py new file mode 100644 index 0000000000..0cebc0294f --- /dev/null +++ b/research/ut3-rank-bounded-block-calls/verify.py @@ -0,0 +1,486 @@ +#!/usr/bin/env python3 +"""Exact corroboration of the written rank-cap theorem; no supplier claim. +Arham Tahir with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from fractions import Fraction +import hashlib +from itertools import product +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def rank(rows): + pivots = {} + for value in rows: + while value: + bit = value.bit_length() - 1 + if bit in pivots: + value ^= pivots[bit] + else: + pivots[bit] = value + break + return len(pivots) + + +def dense_rank(rows, width): + """Separate Boolean-array Gaussian elimination.""" + matrix = [[bool(row & (1 << j)) for j in range(width)] for row in rows] + pivot = 0 + for j in range(width): + candidate = next((i for i in range(pivot, len(matrix)) if matrix[i][j]), None) + if candidate is None: + continue + matrix[pivot], matrix[candidate] = matrix[candidate], matrix[pivot] + for i in range(pivot + 1, len(matrix)): + if matrix[i][j]: + matrix[i] = [x != y for x, y in zip(matrix[i], matrix[pivot])] + pivot += 1 + return pivot + + +def identity(n): + return tuple(1 << i for i in range(n)) + + +def binary_mul(left, right): + answer = [] + for row in left: + value = 0 + while row: + bit = (row & -row).bit_length() - 1 + value ^= right[bit] + row &= row - 1 + answer.append(value) + return tuple(answer) + + +def group_mul(g, h): + u, v, z = g & 1, (g >> 1) & 1, (g >> 2) & 1 + U, V, Z = h & 1, (h >> 1) & 1, (h >> 2) & 1 + return (u ^ U) | ((v ^ V) << 1) | ((z ^ Z ^ (u & V)) << 2) + + +GM = tuple(tuple(group_mul(g, h) for h in range(8)) for g in range(8)) + + +def ring_mul(left, right): + value = 0 + for g in range(8): + if left & (1 << g): + for h in range(8): + if right & (1 << h): + value ^= 1 << GM[g][h] + return value + + +def formal_identity(n): + return tuple(tuple(int(i == j) for j in range(n)) for i in range(n)) + + +def formal_mul(left, right): + n = len(left) + answer = [[0] * n for _ in range(n)] + for i in range(n): + for k in range(n): + if left[i][k]: + for j in range(n): + if right[k][j]: + answer[i][j] ^= ring_mul(left[i][k], right[k][j]) + return tuple(map(tuple, answer)) + + +def factor(g, rows): + n = len(rows) + return tuple(tuple(int(i == j) ^ ((1 ^ (1 << g)) if rows[i] & (1 << j) else 0) + for j in range(n)) for i in range(n)) + + +def scalar(rows): + return tuple(tuple(int(bool(row & (1 << j))) for j in range(len(rows))) for row in rows) + + +def target(r, w): + return tuple(tuple((1 << 4 if i < w else 1) if i == j else 0 for j in range(r)) + for i in range(r)) + + +def count_per_label(w, k): + require(type(w) is int and type(k) is int and w >= 1 and k >= 1, 'positive integer w,k') + return max(2, (2 * w + k - 1) // k) + + +def construction(r, w, k): + require(type(r) is int and r >= w, 'workspace r must be at least w') + t = count_per_label(w, k) + supports = [set() for _ in range(t)] + for i in range(w): + supports[(2 * i) % t].add(i) + supports[(2 * i + 1) % t].add(i) + word = [] + for support in supports: + rows = tuple(1 << i if i in support else 0 for i in range(r)) + require(1 <= rank(rows) <= k, 'empty or oversized block') + word.extend(((1, rows), (2, rows))) + return tuple(word) + + +def invoice(word, k): + counts, masses = [0, 0], [0, 0] + for g, rows in word: + require(g in (1, 2), 'only paid labels a,b are allowed') + d = rank(rows) + require(1 <= d <= k, 'rank cap violated') + counts[g - 1] += 1 + masses[g - 1] += d + return {'counts': counts, 'rank_mass': masses} + + +def replay(word, r): + answer = formal_identity(r) + for g, rows in word: + answer = formal_mul(answer, factor(g, rows)) + return answer + + +def check_word(word, r, w, k, claimed_invoice): + for _, rows in word: + require(len(rows) == r and all(type(row) is int and 0 <= row < 1 << r for row in rows), + 'invalid scalar coupling dimensions') + require(invoice(word, k) == claimed_invoice, 'undercharged invoice') + require(replay(word, r) == target(r, w), 'incorrect complete dirty boundary') + + +# Basis 1,X,Y,XY,YX; this algebra multiplication does not use GM. +QM = ((0, 1, 2, 3, 4), (1, None, 3, None, None), + (2, 4, None, None, None), (3, None, None, None, None), + (4, None, None, None, None)) + + +def quotient_mul(left, right): + value = 0 + for i in range(5): + for j in range(5): + if left & (1 << i) and right & (1 << j) and QM[i][j] is not None: + value ^= 1 << QM[i][j] + return value + + +def quotient(g): + u, v, z = g & 1, (g >> 1) & 1, (g >> 2) & 1 + return 1 | (u << 1) | (v << 2) | (z << 3) | ((z ^ (u & v)) << 4) + + +def formal_quotient(matrix): + out = {i: [] for i in range(1, 5)} + for row in matrix: + values = [0] * 5 + for j, entry in enumerate(row): + q = 0 + for g in range(8): + if entry & (1 << g): + q ^= quotient(g) + for i in range(1, 5): + if q & (1 << i): + values[i] |= 1 << j + for i in out: + out[i].append(values[i]) + return {i: tuple(rows) for i, rows in out.items()} + + +def coefficients(word, r): + """Ordered one/two-subsequence expansion, with matrix factors in order.""" + zero = tuple(0 for _ in range(r)) + out = {1: zero, 2: zero, 3: zero, 4: zero} + for j, (g, rows) in enumerate(word): + out[g] = tuple(a ^ b for a, b in zip(out[g], rows)) + for h, previous in word[:j]: + if h != g: + key = 3 if h == 1 else 4 + contribution = binary_mul(previous, rows) + out[key] = tuple(a ^ b for a, b in zip(out[key], contribution)) + return out + + +def quotient_replay(word, r): + """Separate dynamic recurrence, with no subsequence list.""" + zero = tuple(0 for _ in range(r)) + X, Y, XY, YX = zero, zero, zero, zero + for g, rows in word: + if g == 1: + YX = tuple(a ^ b for a, b in zip(YX, binary_mul(Y, rows))) + X = tuple(a ^ b for a, b in zip(X, rows)) + else: + XY = tuple(a ^ b for a, b in zip(XY, binary_mul(X, rows))) + Y = tuple(a ^ b for a, b in zip(Y, rows)) + return {1: X, 2: Y, 3: XY, 4: YX} + + +def rank_factorization(rows): + """A=UV, U full column rank and V full row rank, over F2.""" + r = len(rows) + basis, coordinates = [], [] + columns = [sum(((rows[i] >> j) & 1) << i for i in range(r)) for j in range(r)] + for column in columns: + lookup = {0: 0} + for j, value in enumerate(basis): + lookup.update({x ^ value: c | (1 << j) for x, c in list(lookup.items())}) + if column not in lookup: + basis.append(column) + coordinates.append(1 << (len(basis) - 1)) + else: + coordinates.append(lookup[column]) + U = tuple(sum(((col >> i) & 1) << j for j, col in enumerate(basis)) for i in range(r)) + V = tuple(sum(((coordinates[j] >> i) & 1) << j for j in range(r)) for i in range(len(basis))) + require(binary_mul(U, V) == rows, 'rank factorization') + return U, V + + +def span_check(word, r): + """Check actual zero-sum, carrier spans and mixed coefficients.""" + coeff = coefficients(word, r) + for g in (1, 2): + left_columns, right_rows = [], [] + for h, rows in word: + if h == g: + U, V = rank_factorization(rows) + for j in range(len(V)): + left_columns.append(sum(((U[i] >> j) & 1) << i for i in range(r))) + right_rows.extend(V) + U = tuple(sum(((col >> i) & 1) << j for j, col in enumerate(left_columns)) for i in range(r)) + require(binary_mul(U, tuple(right_rows)) == coeff[g], 'degree-one sum') + col_mixed, row_mixed = coeff[3 if g == 1 else 4], coeff[4 if g == 1 else 3] + columns = [sum(((col_mixed[i] >> j) & 1) << i for i in range(r)) for j in range(r)] + require(rank(left_columns + columns) == rank(left_columns), 'mixed column containment') + require(rank(right_rows + list(row_mixed)) == rank(right_rows), 'mixed row containment') + if not any(coeff[g]): + require(rank(U) + rank(right_rows) <= len(right_rows), 'zero-product rank inequality') + require(rank(col_mixed) + rank(row_mixed) <= len(right_rows), 'rank-volume lower bound') + + +# Faithful regular engine: literal 3x3 address matrices, independent group +# enumeration and multiplication. It never calls GM or ring_mul. +ADDRESS = tuple(tuple((int(i == j) ^ (u if (i, j) == (0, 1) else 0) + ^ (v if (i, j) == (1, 2) else 0) + ^ (z if (i, j) == (0, 2) else 0)) + for i in range(3) for j in range(3)) + for u, v, z in product((0, 1), repeat=3)) + + +def address_mul(a, b): + return tuple(sum(a[3 * i + t] * b[3 * t + j] for t in range(3)) % 2 + for i in range(3) for j in range(3)) + + +def regular_address(address): + rows = [0] * 8 + for j, h in enumerate(ADDRESS): + rows[ADDRESS.index(address_mul(address, h))] |= 1 << j + return tuple(rows) + + +RA, RB, RC = (regular_address(ADDRESS[i]) for i in (4, 2, 1)) + + +def regular_from_formal(matrix): + """Bridge only for comparison; the regular replay never calls this.""" + r = len(matrix) + out = [0] * (8 * r) + for i, row in enumerate(matrix): + for j, entry in enumerate(row): + for g in range(8): + if entry & (1 << g): + index = 4 * (g & 1) + 2 * ((g >> 1) & 1) + ((g >> 2) & 1) + action = regular_address(ADDRESS[index]) + for s in range(8): + out[8 * i + s] ^= action[s] << (8 * j) + return tuple(out) + + +def regular_factor(g, rows): + r = len(rows) + transport = RA if g == 1 else RB + output = list(identity(8 * r)) + for i, row in enumerate(rows): + for j in range(r): + if row & (1 << j): + for s in range(8): + output[8 * i + s] ^= (transport[s] ^ (1 << s)) << (8 * j) + return tuple(output) + + +def regular_scalar(rows): + return tuple(sum((1 << (8 * j + s)) for j in range(len(rows)) if row & (1 << j)) + for row in rows for s in range(8)) + + +def regular_target(r, w): + return tuple((RC[s] if i < w else 1 << s) << (8 * i) for i in range(r) for s in range(8)) + + +def regular_replay(word, r): + result = identity(8 * r) + for g, rows in word: + result = binary_mul(result, regular_factor(g, rows)) + return result + + +def expect_rejection(action): + try: + action() + except ValueError: + return + raise ValueError('negative control was accepted') + + +def run(): + for g, h in product(range(8), repeat=2): + require(quotient(GM[g][h]) == quotient_mul(quotient(g), quotient(h)), 'quotient homomorphism') + for x, y, z in product(range(32), repeat=3): + require(quotient_mul(quotient_mul(x, y), z) == quotient_mul(x, quotient_mul(y, z)), 'quotient associativity') + require(quotient(4) == 1 ^ 8 ^ 16, 'both mixed coefficients required') + coupling_counts = {} + for r in (1, 2, 3): + counts = [0] * (r + 1) + for rows in product(range(1 << r), repeat=r): + d = rank(rows) + require(d == dense_rank(rows, r), 'independent rank mismatch') + U, V = rank_factorization(rows) + counts[d] += 1 + for g in (1, 2): + F = factor(g, rows) + split = formal_identity(r) + for j, v in enumerate(V): + component = tuple(v if U[i] & (1 << j) else 0 for i in range(r)) + require(rank(component) == 1, 'nonzero rank-one decomposition component') + split = formal_mul(split, factor(g, component)) + require(split == F, 'same-label rank decomposition') + require(formal_mul(F, F) == formal_identity(r), 'arbitrary-rank call inverse') + D = regular_factor(g, rows) + require(binary_mul(D, D) == identity(8 * r), 'regular call inverse') + coupling_counts[str(r)] = counts + matrices = [rows for rows in product(range(4), repeat=2) if any(rows)] + alphabet = [(g, rows) for g in (1, 2) for rows in matrices] + short_words = 0 + for length in range(4): + for word in product(alphabet, repeat=length): + require(coefficients(word, 2) == quotient_replay(word, 2), 'ordered coefficient mismatch') + require(coefficients(word, 2) == formal_quotient(replay(word, 2)), 'formal quotient mismatch') + span_check(word, 2) + short_words += 1 + for first, second in product(alphabet, repeat=2): + require(regular_from_formal(replay((first, second), 2)) == regular_replay((first, second), 2), + 'formal/regular arbitrary two-factor mismatch') + fixtures, omissions, basis_columns, profiles = 0, 0, 0, [] + for w in range(1, 13): + for k in range(1, w + 3): + r = w + 2 + word = construction(r, w, k) + bill = invoice(word, k) + t = count_per_label(w, k) + require(bill == {'counts': [t, t], 'rank_mass': [2 * w, 2 * w]}, 'sharp invoice') + require(replay(word, r) == target(r, w), 'full formal dirty endpoint') + require(replay(tuple(reversed(word)), r) == target(r, w), 'formal inverse endpoint') + require(regular_replay(word, r) == regular_target(r, w), 'faithful regular dirty endpoint') + require(regular_replay(tuple(reversed(word)), r) == regular_target(r, w), 'regular inverse endpoint') + span_check(word, r) + profiles.append([w, k, t, [rank(rows) for _, rows in word]]) + fixtures += 1 + basis_columns += 2 * 8 * r + if w <= 3: + for j in range(len(word)): + bad = word[:j] + word[j + 1:] + require(replay(bad, r) != target(r, w), 'omitted-call formal control') + require(regular_replay(bad, r) != regular_target(r, w), 'omitted-call regular control') + omissions += 1 + r, w, k = 5, 3, 2 + pilot = construction(r, w, k) + S = list(identity(r)) + S[0] ^= 1 << 4 + S[1] ^= 1 << 2 + S = tuple(S) + require(binary_mul(S, S) == identity(r), 'scalar gauge inverse') + gauged = tuple((g, binary_mul(binary_mul(S, rows), S)) for g, rows in pilot) + F, D = replay(gauged, r), regular_replay(gauged, r) + require(formal_mul(formal_mul(scalar(S), F), scalar(S)) == target(r, w), 'full gauged dirty boundary') + require(binary_mul(binary_mul(regular_scalar(S), D), regular_scalar(S)) == regular_target(r, w), 'regular gauged boundary') + require(F != target(r, w) and D != regular_target(r, w), 'missing scalar boundary control') + span_check(gauged, r) + expect_rejection(lambda: invoice(pilot, 1)) + expect_rejection(lambda: invoice(((4, identity(r)),), r)) + expect_rejection(lambda: construction(2, 3, 2)) + expect_rejection(lambda: construction(3, 3, 0)) + expect_rejection(lambda: check_word(pilot, r, w, k, {'counts': [3, 3], 'rank_mass': [6, 5]})) + wrong = ((2, pilot[0][1]),) + pilot[1:] + require(replay(wrong, r) != target(r, w), 'wrong paid label control') + require(regular_replay(wrong, r) != regular_target(r, w), 'wrong paid label regular control') + dirty = list(pilot[0][1]) + dirty[0] ^= 1 << 3 + leaked = ((1, tuple(dirty)),) + pilot[1:] + require(replay(leaked, r) != target(r, w), 'dirty-source contamination formal control') + require(regular_replay(leaked, r) != regular_target(r, w), 'dirty-source contamination regular control') + extra = tuple(1 << 3 if i == 3 else 0 for i in range(r)) + unrestored = pilot + ((1, extra),) + require(replay(unrestored, r) != target(r, w), 'unrestored workspace formal control') + require(regular_replay(unrestored, r) != regular_target(r, w), 'unrestored workspace regular control') + perturbed = [list(row) for row in target(r, w)] + perturbed[0][r - 1] ^= ring_mul(1 ^ (1 << 1), 1 ^ (1 << 4)) + perturbed = tuple(map(tuple, perturbed)) + require(perturbed != target(r, w), 'nonzero quotient-kernel control') + require(formal_quotient(perturbed) == formal_quotient(target(r, w)), 'kernel perturbation must be invisible to quotient') + require(regular_from_formal(perturbed) != regular_target(r, w), 'faithful kernel rejection') + tariff_checks = 0 + for w in range(1, 13): + for k in range(1, w + 3): + bill = invoice(construction(w, w, k), k) + t = count_per_label(w, k) + for aa, ab, ba, bb in ((1, 1, 0, 0), (0, 0, 1, 1), + (Fraction(3, 2), Fraction(5, 7), Fraction(2, 3), Fraction(7, 11))): + paid = aa * bill['counts'][0] + ab * bill['counts'][1] + ba * bill['rank_mass'][0] + bb * bill['rank_mass'][1] + require(paid == t * (aa + ab) + 2 * w * (ba + bb), 'exact affine tariff') + tariff_checks += 1 + return {'schema_version': 1, 'result': 'sharp rank-cap invocation count; no new kappa', + 'formula': 't=max(2,ceil(2w/k)); counts=(t,t); rank_mass=(2w,2w)', + 'quotient_products': 64, 'quotient_associativity_triples': 32768, + 'all_binary_couplings_rank_counts': coupling_counts, + 'same_label_rank_decompositions': 1060, + 'short_words': short_words, 'full_formal_and_regular_fixtures': fixtures, + 'arbitrary_two_factor_formal_regular_comparisons': len(alphabet) ** 2, + 'forward_inverse_regular_basis_columns': basis_columns, + 'omitted_call_controls': omissions, 'other_model_controls': 10, + 'scalar_gauged_fixtures': 1, 'exact_rational_tariff_checks': tariff_checks, + 'profiles_sha256': hashlib.sha256(json.dumps(profiles, separators=(',', ':')).encode()).hexdigest(), + 'pilot': {'w': 3, 'k': 2, 'r': 5, 'invoice': invoice(pilot, k), + 'supports': [[i for i in range(r) if rows[i]] for _, rows in pilot]}} + + +def unique_object(pairs): + result = {} + for key, value in pairs: + require(key not in result, 'duplicate JSON key') + result[key] = value + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--emit', action='store_true', help='print fresh receipt; never write package files') + args = parser.parse_args() + receipt = run() + if args.emit: + print(json.dumps(receipt, sort_keys=True, indent=2)) + else: + expected = json.loads((HERE / 'CERTIFICATE.json').read_text(), object_pairs_hook=unique_object) + require(json.dumps(receipt, sort_keys=True) == json.dumps(expected, sort_keys=True), 'certificate mismatch') + print('PASS_UT3_RANK_CAP calls=2*max(2,ceil(2w/k)) rank_mass=4w pilot_calls=6 no_new_kappa') + + +if __name__ == '__main__': + main()