From fe77116fcf5012533e6de748ab6089790f43ac37 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 09:05:17 +0000 Subject: [PATCH] feat(research): attain five A2 targets with rank-three calls --- research/a2-five-target-cap-three/PROOF.md | 111 +++++++++ research/a2-five-target-cap-three/README.md | 151 ++++++++++++ .../a2-five-target-cap-three/SOURCES.json | 42 ++++ research/a2-five-target-cap-three/TASK.json | 71 ++++++ research/a2-five-target-cap-three/VERIFY.json | 34 +++ research/a2-five-target-cap-three/verify.py | 230 ++++++++++++++++++ 6 files changed, 639 insertions(+) create mode 100644 research/a2-five-target-cap-three/PROOF.md create mode 100644 research/a2-five-target-cap-three/README.md create mode 100644 research/a2-five-target-cap-three/SOURCES.json create mode 100644 research/a2-five-target-cap-three/TASK.json create mode 100644 research/a2-five-target-cap-three/VERIFY.json create mode 100644 research/a2-five-target-cap-three/verify.py diff --git a/research/a2-five-target-cap-three/PROOF.md b/research/a2-five-target-cap-three/PROOF.md new file mode 100644 index 0000000000..3830d0e7dd --- /dev/null +++ b/research/a2-five-target-cap-three/PROOF.md @@ -0,0 +1,111 @@ +# Five rank-three calls for five A2 longest-element targets + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement and model + +Let K be any field and W=S3 have simple involutions s,t with sts=tst. +Write w0=sts. Fix any finite r>=5. Work coefficientwise in M_r(K[W]); +every role has arbitrary initial data. The required complete endpoint is + + T = diag([w0],[w0],[w0],[w0],[w0],1,...,1). + +A paid call is F_u(A)=I+([u]-[e])A, where u is s or t and +1<=rank_K(A)<=3. Scalar GL_r(K) maps may be interleaved for free. +Couplings A need not be projectors or invertible. There are no other free +address operations, clean allocations, resets or discarded outputs. +Every spectator and every off-diagonal formal coefficient must be restored. + +Let f on {0,1,2,3} be nonnegative, nondecreasing and discretely concave, +with f(0)=0. The cost of a paid call is f(rank A), the same for both labels. +Then the exact formal tariff is + + optimum = 5 f(3). + +In particular, the minimum number of paid invocations is five, by taking +f(k)=1 for k>0. This is a formal call price, not a native or recursive bill. + +## Attaining support schedule + +Number productive roles 0 through 4, and let E_B be the diagonal projector +on B. Execute the following calls chronologically: + +| Call | Label | Support B | Rank | +| --- | --- | --- | ---: | +| 1 | s | {0,1,2} | 3 | +| 2 | t | {0,1,4} | 3 | +| 3 | s | {0,3,4} | 3 | +| 4 | t | {2,3,4} | 3 | +| 5 | s | {1,2,3} | 3 | + +On roles 0,1,2,3 the chronological subsequence is s,t,s. On role 4 it is +t,s,t. Both are palindromes equal to w0, so the rightmost-first convention +for multiplying column-vector operators gives the same endpoint. A call +acts as its group label on its support and as identity everywhere else. +All role matrices are diagonal. Thus the full group-algebra product is T, +including every zero off-diagonal and the identity on every spectator. +This is valid over every field, including characteristic two. It uses no +scalar mixing, dirty helper, preparation, restoration or extra call. +All five calls have rank three and cost 5 f(3). + +## Matching lower bound + +Use the all-field root-cut rank bound in zhaobenny's +[PR6817, proof section 2](../coxeter-capped-concave-tariff/PROOF.md), +building on David Arias's [PR2738](../coxeter-root-tariff/PROOF.md). +Its hypotheses are exactly the formal factors, scalar maps and complete +dirty endpoint above. The A2 simple roots form one root orbit, and w0 +has three inversions. Five targets therefore force + + sum_j rank_K(A_j) >= 15. + +This inequality is an inherited theorem, not re-proved or replayed here. +Its allowance of arbitrary scalar couplings and arbitrarily many restored +dirty spectators is needed for the lower bound, even though the attaining +word uses diagonal projectors and no spectators. + +Concavity and f(0)=0 give f(k)>=k f(3)/3 for k=1,2,3. Consequently every +legal finite circuit has cost at least + + sum_j f(rank A_j) >= f(3)/3 sum_j rank A_j >= 5 f(3). + +The support schedule attains this bound. No classification of circuits, +finite-field extrapolation or numerical root calculation is required. +For unit invocation prices, the same rank bound rules out four calls, +since four rank-three calls supply at most twelve rank units. + +## Improvement and relation to prior work + +The direct fixed partition into a three-role block and a two-role block +applies the three-letter word separately, costing 3 f(3)+3 f(2). +The displayed schedule saves exactly 3 f(2)-2 f(3), which is nonnegative +by concavity and positive for every strictly concave f. At f(k)=k/(k+1), +the exact price is 15/4 instead of 17/4, saving 1/2. This comparator is an +explicit construction, not a claimed optimum of any enlarged model. + +Nick Petalas's [PR5083](../rank2-swap-batching/README.md) already gives +three longest-element targets at rank cap two using changing supports. +That idea and schedule are credited, not claimed again. The present new +instance has five targets, cap three and five full-rank calls. PR6817's +divisible theorem does not cover 3 not dividing 5, and its cap-two st +correction has a different target. ToikY's +[PR6821](../a2-st-all-cap-tariff/README.md) settles repeated st at every +cap; it does not settle repeated w0. We answer one instance of PR6817's +explicit nondivisible-target question. No claim of literature priority +for support scheduling, concavity or the root-cut method is made. + +## Evidence and limits + +The standalone verifier multiplies full signed coefficients in K[S3]. +It also checks the full left regular action using a separate GL2(F2) +address representation. Finite gauges mix productive and dirty roles, +with explicit entrance and exit scalar maps. These are corroborating +examples; the displayed word and cited lower bound give the universal proof. +The verifier does not run any predecessor's scientific program. + +Scalar coupling rank is not recursive child rank. Native realization, +the price of scalar maps, routing, storage, ownership, precision, stock, +hosting, compilation and the complete supplier invoice remain unknown. +No new kappa, supplier admission, selected-frontier change, independent +human review, formal-kernel acceptance or complete multiplication theorem +is claimed. The five selected framework assumptions remain. diff --git a/research/a2-five-target-cap-three/README.md b/research/a2-five-target-cap-three/README.md new file mode 100644 index 0000000000..ce8738b5e9 --- /dev/null +++ b/research/a2-five-target-cap-three/README.md @@ -0,0 +1,151 @@ +# Five A2 longest-element targets need five rank-three calls + +This contribution was produced by Nick Petalas. Apache-2.0. + +Scoped written proof with exact finite corroboration. Five identical +longest-element targets w0=sts=tst in S3 have exact formal tariff **5 f(3)** +when paid scalar rank is capped at three and the common rank price f is +nonnegative, nondecreasing and discretely concave, with f(0)=0. The result +holds over every field, with free scalar GL mixing and any finite number +of restored dirty spectators. In particular, five unit-priced invocations +are necessary and sufficient. + +The new diagonal support schedule has five rank-three calls, compared with +six calls of ranks (3,3,3,2,2,2) from fixed disjoint batching. It costs +5 f(3) instead of 3 f(3)+3 f(2), saving 3 f(2)-2 f(3). At f(k)=k/(k+1), +the exact bill is 15/4 instead of 17/4. The matching 15-unit rank lower +bound is a cited predecessor theorem, not a new result here. + +[PROOF.md](PROOF.md) gives the complete endpoint, five support sets and +all-field argument. This answers one nondivisible-target instance explicitly +left open by zhaobenny's [PR6817](https://github.com/CrocSwap/integer-mult-bounds/pull/6817). +Its divisible theorem does not cover five targets at cap three. Nick Petalas's +[PR5083](https://github.com/CrocSwap/integer-mult-bounds/pull/5083) already +supplies the changing-support idea and the distinct three-target/cap-two +word; those are credited. ToikY's +[PR6821](https://github.com/CrocSwap/integer-mult-bounds/pull/6821) treats +repeated st, a different endpoint. The new contribution is this five-target +support schedule and its sharp cap-three tariff, not a new root-cut or +concavity principle. + +## Evidence and reproduction + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/a2-five-target-cap-three/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/a2-five-target-cap-three/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/a2-five-target-cap-three +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/a2-five-target-cap-three --check-source-history --check-modes +``` + +Other installations can substitute their CPython 3.12 path. The direct +commands print `PASS_A2_FIVE_TARGET_CAP_THREE` in a newly computed JSON +receipt bound to the SHA256 of all six package files. They write no files, +import no predecessor program and require no Git, network or external input. +`SOURCES.json` pins cited prose and the historical task context as provenance; +the package validator authenticates those Git pins separately. + +The finite checks cover exactly: + +- 24 complete signed group-algebra endpoints over Q, F2, F3 and F5, using + five, six and eight roles and two scalar gauges. All 120 paid couplings + have rank three and are idempotent; 78 genuinely couple productive and + dirty roles. Entrance and exit scalar maps restore the target endpoint. +- 912 basis columns of the complete left regular action, using a separate + GL2(F2) address representation rather than the S3 permutation product. +- 120 omitted-call and 120 label-flip mutants, each rejected by its complete + formal endpoint. These controls concern the new word only. +- 36 exact rational price schedules, including all 35 nonincreasing + nonnegative integer slope triples with slopes at most four, plus + f(k)=k/(k+1). Each is compared against all 90 nonnegative rank-count + profiles with total rank 15 through 17, for 3,240 comparisons. + Exactly 31 of the 36 schedules give strict savings over fixed batching. + +The price-profile enumeration suffices for this finite relaxation: from +any list of ranks 1..3 with total at least 15, retain a prefix through its +first crossing of 15. Its total lies in 15..17 and its cost cannot increase. +The universal circuit lower bound is the written cited theorem, not an +extrapolation from this finite price test or from the tested fields. + +Local validation uses CPython 3.12.15 on macOS arm64. Normal, optimized +and registered replay are the required checks; exact timings and the +publication commit are recorded in the PR body. Hosted CI status is separate. +No local mathematical check is deferred solely to CI. Independent human +and formal proof-kernel review are unclaimed. + +## Scope and overlap + +The formal paid operation is I+([u]-[e])A, u in {s,t}, with arbitrary +scalar A of positive rank at most three. The endpoint is diagonal with +five [w0] entries and identity on every other role. Arbitrary couplings, +free scalar maps and restored dirty spectators are allowed for the lower +bound. The attaining schedule needs only coordinate projectors and no +spectators. It does not classify other target counts, caps or prices. + +This is a changed-scope side result for `bit-new-register-model`. It does +not fulfill that card's native-conversion or complete-supplier gate. +Scalar coupling rank is not recursive child rank. The actual physical +price, ownership, routing, storage, precision, stock, compilation, hosting +and complete supplier invoice remain unknown. No new kappa, supplier +admission or selected-frontier change is claimed; all five selected +framework assumptions remain. Lean, Docker, the selected cold replay +and predecessor scientific suites were not run. + +The scientific base is canonical main +`e54523517d0f03e58352e647c403a5af3e525a57`, with the selected #7000 record +and priority revision 8 pinned separately in `SOURCES.json`. The +[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19538441) +states the same five-target/cap-three scope. + +Entry overlap included live open PRs, account PR history, recent handoffs, +active discussions, relevant PR bodies, and distinctive whole-main README +searches for the specific and general batching formulas. The cached scan +covered 477 open PRs and 7,121 Discussion records with complete remote +pagination, but only 169 materialized notes against 10,178 HEAD note paths. +Whole-main Git searches supplemented that sparse coverage. A separate +source-reference scan covered 477 open and 6,175 closed PR bodies and found +no account PR created since November 4 citing #6817. These snapshots are +non-atomic; arbitrary diffs, unmaterialized nested code and unpublished +work are outside coverage. A lack of matches is not a novelty certificate. + +## Credit + +zhaobenny / Benny Zhao's #6817 supplies the all-field rank-cap model, +nondivisible-target question and root-cut/concave-price lower bound. +David Arias's #2738 supplies its Coxeter predecessor. Nick Petalas's +#5083 supplies the older cap-two changing-support construction. ToikY's +#6821 settles the distinct repeated-st question. Credit also Adam Gall, +Ross Richardson, ywz65, eumemic, Ali Romman and Gareth Davidson for the +retained cut and register-model lineage. All predecessor notices remain +unchanged. No literature-priority claim is made for support scheduling, +concavity, matrix rank or regular representations. + +## Open next questions + +Can a native implementation supply a rank-three call with a complete +subadditive price? First specify the actual data/address layout and +arbitrary-input entry/exit contract, then charge scalar maps, movement, +ownership, precision and restoration. No such physical contract or map +from scalar rank to recursive child rank is supplied here. + +Which other nondivisible longest-element batches attain the packed floor? +Start with a support-incidence feasibility problem at one declared target +count and cap. This result gives no general scheduling theorem or chronology +obstruction. No broader construction or follow-on scope is reserved. + +## Verifier bounds + +The verifier has no recursion, subprocess, solver, external mutable state +or unbounded CLI input. Dimensions are at most eight, each formal matrix +has at most 6*8*8=384 coefficient positions, and words have five calls. +Price loops use 36 schedules and 972 candidate rank-count tuples before +filtering. All functions are shorter than sixty physical lines. Explicit +exceptions preserve invariants under optimized Python. + +Python's managed tuples, dictionaries and arbitrary-size integers allocate +during calculation. This is a deviation from fixed allocation, confined to +the bounded finite verifier. Fixed dimensions, domains and support-capacity +checks bound live collections. Warning-strict normal and optimized replay +check the same result. A future larger or native verifier must reassess +allocation rather than inherit a real-time or native-memory guarantee. diff --git a/research/a2-five-target-cap-three/SOURCES.json b/research/a2-five-target-cap-three/SOURCES.json new file mode 100644 index 0000000000..0f27df3351 --- /dev/null +++ b/research/a2-five-target-cap-three/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/a2-st-all-cap-tariff/README.md", + "usage": "provenance", + "git_blob": "65b290f04027f819b6d4295f9c6a921e2c6a1d0d", + "sha256": "83f19d188e3ec529ffbe5bc27013137227743b01654053a18249c8a4551c82a3" + }, + { + "path": "research/coxeter-capped-concave-tariff/PROOF.md", + "usage": "provenance", + "git_blob": "00c633badd2f1848ec34b9893553161012e7a8f3", + "sha256": "1ef4cb87aee9ca82b9fe42a114b152e1241b7454d68dd49ea8d260fb91e28353" + }, + { + "path": "research/coxeter-capped-concave-tariff/README.md", + "usage": "provenance", + "git_blob": "a9098b3da041be510c0853c5330f74d9e3521219", + "sha256": "75fec6903abe17ebeee06627b5cbf7b38d9b00ef5f233774d64539755c339120" + }, + { + "path": "research/rank2-swap-batching/README.md", + "usage": "provenance", + "git_blob": "431363d53d9d5b6f1832698cc7332244e0e4efd0", + "sha256": "2eded51bc7d80e360ff3937f3cc9feddb79e35b3f3d5ee3d69ac5b232b0d8054" + } + ] +} diff --git a/research/a2-five-target-cap-three/TASK.json b/research/a2-five-target-cap-three/TASK.json new file mode 100644 index 0000000000..3844eb3790 --- /dev/null +++ b/research/a2-five-target-cap-three/TASK.json @@ -0,0 +1,71 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "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. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "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.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact common concave formal tariff 5 f(3) for five identical A2 longest-element targets at paid scalar rank cap three, over every field and with arbitrary finite restored dirty workspace.", + "scope_change_reason": "The contextual picker suggested complex mechanisms. The live-question search instead identified PR6817's nondivisible Coxeter batching question. This changes the native-register card to a formal tariff side result, without native conversion or the original complete-supplier gate.", + "bottleneck_link": "Changing supports can lower a capped concave formal invoice. Scalar coupling rank is not recursive child rank; a native realization and full physical invoice are still required before a supplier gain can follow.", + "budget_minutes": 60, + "stop_rule": "Stop after the first verified five-target/cap-three support schedule and exact tariff. Do not generalize it or search a larger group.", + "outcome": "completed", + "evidence": "PROOF.md and the standalone warning-strict normal/optimized verifier, which prints a freshly generated hash-bound receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a native implementation realize one of these rank-three calls at a complete subadditive price?", + "why_it_matters": "The formal five-call saving cannot be identified with a recursive saving without this map.", + "first_step": "Specify the actual data/address layout and arbitrary-input endpoint, then charge scalar maps, ownership, routing, precision and restoration.", + "blocked_by": "No physical call contract or conversion from scalar rank to recursive child rank is supplied." + }, + { + "question": "Which other nondivisible longest-element batches attain the packed bound?", + "why_it_matters": "The explicit five-target schedule answers one case, while general remainder attainability remains undecided here.", + "first_step": "Derive a bounded support-incidence feasibility problem at one different declared target count and cap before considering arbitrary scalar couplings.", + "blocked_by": "No general support-scheduling theorem or chronology obstruction is proved by this package." + } + ], + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19538441" +} diff --git a/research/a2-five-target-cap-three/VERIFY.json b/research/a2-five-target-cap-three/VERIFY.json new file mode 100644 index 0000000000..b2f625c38b --- /dev/null +++ b/research/a2-five-target-cap-three/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Full formal endpoint, independent regular-action endpoint, rank-three and dirty coupling checks, omitted-call/label controls, and exact concave-price profiles." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same complete finite verification with Python assertions disabled; explicit exceptions remain active." + } + ] +} diff --git a/research/a2-five-target-cap-three/verify.py b/research/a2-five-target-cap-three/verify.py new file mode 100644 index 0000000000..5c54014255 --- /dev/null +++ b/research/a2-five-target-cap-three/verify.py @@ -0,0 +1,230 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration, produced by Nick Petalas. Apache-2.0. + +Writes no files. The universal lower bound is cited in PROOF.md. +""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations_with_replacement, product +from pathlib import Path +import json + + +SUPPORTS = ((0, 1, 2), (0, 1, 4), (0, 3, 4), (2, 3, 4), (1, 2, 3)) +LABELS = (1, 2, 1, 2, 1) +IDENTITY = (0, 1, 2) +SIMPLE = (IDENTITY, (1, 0, 2), (0, 2, 1)) +FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def reduced(value, prime): + return value % prime if prime else value + + +def identity(size): + require(1 <= size <= 8, "matrix size") + return tuple(tuple(int(i == j) for j in range(size)) for i in range(size)) + + +def multiply(left, right, prime): + size = len(left) + require(size == len(right) and 1 <= size <= 8, "matrix size") + return tuple(tuple(reduced(sum(left[i][k] * right[k][j] for k in range(size)), prime) + for j in range(size)) for i in range(size)) + + +def rank(matrix, prime): + size = len(matrix) + require(1 <= size <= 8, "matrix size") + rows = [[Fraction(v) if not prime else v % prime for v in row] for row in matrix] + count = 0 + for column in range(size): + pivot = next((j for j in range(count, size) if rows[j][column]), None) + if pivot is None: + continue + rows[count], rows[pivot] = rows[pivot], rows[count] + inverse = 1 / rows[count][column] if not prime else pow(rows[count][column], -1, prime) + rows[count] = [reduced(v * inverse, prime) for v in rows[count]] + for j in range(size): + if j != count: + multiple = rows[j][column] + rows[j] = [reduced(a - multiple * b, prime) + for a, b in zip(rows[j], rows[count])] + count += 1 + return count + + +def gauge(size, variant, prime): + matrix = identity(size) + inverse = matrix + edges = [(0, size - 1), (size - 1, 1)] + edges += [(j, j + 1) for j in range(size - 1)] + for index, (i, j) in enumerate(edges): + value = 1 + variant * (index % 2) + forward = [list(row) for row in identity(size)] + backward = [list(row) for row in identity(size)] + forward[i][j] = value + backward[i][j] = -value + matrix = multiply(forward, matrix, prime) + inverse = multiply(inverse, backward, prime) + require(multiply(matrix, inverse, prime) == identity(size), "gauge inverse") + return matrix, inverse + + +def couplings(size, matrix, inverse, prime): + result = [] + for support in SUPPORTS: + projector = tuple(tuple(int(i == j and i in support) for j in range(size)) + for i in range(size)) + coupling = multiply(multiply(matrix, projector, prime), inverse, prime) + require(rank(coupling, prime) == 3, "rank cap or rank loss") + require(multiply(coupling, coupling, prime) == coupling, "projector") + result.append(coupling) + return tuple(result) + + +def compose(left, right): + return tuple(left[right[j]] for j in range(3)) + + +def formal_scalar(matrix): + size = len(matrix) + return {(i, j, IDENTITY): matrix[i][j] for i in range(size) for j in range(size) + if matrix[i][j]} + + +def formal_gate(label, coupling, prime): + size = len(coupling) + result = {(i, i, IDENTITY): 1 for i in range(size)} + for i, j in product(range(size), repeat=2): + value = coupling[i][j] + for group, sign in ((SIMPLE[label], 1), (IDENTITY, -1)): + key = (i, j, group) + result[key] = reduced(result.get(key, 0) + sign * value, prime) + return {key: value for key, value in result.items() if value} + + +def formal_product(left, right, prime): + require(len(left) <= 384 and len(right) <= 384, "formal support capacity") + result = {} + for (i, k, g), a in left.items(): + for (other, j, h), b in right.items(): + if other == k: + key = (i, j, compose(g, h)) + result[key] = reduced(result.get(key, 0) + a * b, prime) + return {key: value for key, value in result.items() if value} + + +def formal_endpoint(size, matrix, inverse, gates, prime, omit=-1, flip=-1): + result = formal_scalar(matrix) + for index in range(5): + if index != omit: + label = 3 - LABELS[index] if index == flip else LABELS[index] + result = formal_product(formal_gate(label, gates[index], prime), result, prime) + return formal_product(formal_scalar(inverse), result, prime) + + +def target(size): + longest = compose(compose(SIMPLE[1], SIMPLE[2]), SIMPLE[1]) + return {(i, i, longest if i < 5 else IDENTITY): 1 for i in range(size)} + + +def binary_product(left, right): + a, b, c, d = left + e, f, g, h = right + return ((a * e + b * g) % 2, (a * f + b * h) % 2, + (c * e + d * g) % 2, (c * f + d * h) % 2) + + +def regular_scalar(matrix, vector, prime): + size = len(matrix) + return [[reduced(sum(matrix[i][j] * vector[j][g] for j in range(size)), prime) + for g in range(6)] for i in range(size)] + + +def regular_check(size, matrix, inverse, gates, prime): + # Separate GL2(F2) address realization, not the permutation table. + group = tuple(x for x in product(range(2), repeat=4) if (x[0] * x[3] - x[1] * x[2]) % 2) + generators = ((1, 0, 0, 1), (1, 1, 0, 1), (1, 0, 1, 1)) + swap = (0, 1, 1, 0) + require(len(group) == 6, "regular group order") + for role, address in product(range(size), range(6)): + initial = [[int(i == role and g == address) for g in range(6)] for i in range(size)] + state = regular_scalar(matrix, initial, prime) + for label, coupling in zip(LABELS, gates): + coupled = regular_scalar(coupling, state, prime) + next_state = [row.copy() for row in state] + for i, g in product(range(size), range(6)): + moved = group.index(binary_product(generators[label], group[g])) + next_state[i][g] -= coupled[i][g] + next_state[i][moved] += coupled[i][g] + state = [[reduced(v, prime) for v in row] for row in next_state] + state = regular_scalar(inverse, state, prime) + expected = [row.copy() for row in initial] + if role < 5: + expected[role][address] = 0 + expected[role][group.index(binary_product(swap, group[address]))] = 1 + require(state == expected, "regular full endpoint") + return size * 6 + + +def price_checks(): + prices = [] + for slopes in combinations_with_replacement(range(5), 3): + a, b, c = reversed(slopes) + prices.append((Fraction(a), Fraction(a + b), Fraction(a + b + c))) + prices.append((Fraction(1, 2), Fraction(2, 3), Fraction(3, 4))) + profiles = tuple(q for q in product(range(18), range(9), range(6)) + if 15 <= q[0] + 2 * q[1] + 3 * q[2] <= 17) + strict = 0 + for c1, c2, c3 in prices: + optimum = min(q1 * c1 + q2 * c2 + q3 * c3 for q1, q2, q3 in profiles) + require(optimum == 5 * c3, "packed tariff") + require(3 * c2 - 2 * c3 >= 0, "batch saving") + strict += int(3 * c2 > 2 * c3) + require(5 * prices[-1][2] == Fraction(15, 4), "rational optimum") + require(3 * prices[-1][1] + 3 * prices[-1][2] == Fraction(17, 4), "rational baseline") + return {"prices": len(prices), "rank_profiles": len(profiles), + "profile_comparisons": len(prices) * len(profiles), "strict_savings": strict} + + +def verify(): + endpoints = columns = omissions = flips = dirty_coupled = 0 + for prime, size, variant in product((0, 2, 3, 5), (5, 6, 8), range(2)): + matrix, inverse = gauge(size, variant, prime) + gates = couplings(size, matrix, inverse, prime) + require(formal_endpoint(size, matrix, inverse, gates, prime) == target(size), "formal endpoint") + columns += regular_check(size, matrix, inverse, gates, prime) + endpoints += 1 + for gate in gates: + dirty_coupled += int(any(gate[i][j] for i, j in product(range(size), repeat=2) + if (i < 5) != (j < 5))) + for index in range(5): + require(formal_endpoint(size, matrix, inverse, gates, prime, omit=index) != target(size), + "omitted-call control") + require(formal_endpoint(size, matrix, inverse, gates, prime, flip=index) != target(size), + "label-flip control") + omissions += 1 + flips += 1 + require(dirty_coupled > 0, "dirty coupling coverage") + words = tuple(tuple(LABELS[j] for j in range(5) if i in SUPPORTS[j]) for i in range(5)) + require(words == ((1, 2, 1),) * 4 + ((2, 1, 2),), "literal role words") + result = {"formal_endpoints": endpoints, "paid_calls": 5 * endpoints, + "regular_basis_columns": columns, "dirty_coupled_calls": dirty_coupled, + "omission_rejections": omissions, "label_flip_rejections": flips, + "prices": price_checks(), "rank_profile": [3] * 5, + "formal_optimum": "5 f(3)", "claim_type": "scoped proof with finite corroboration"} + package = Path(__file__).resolve().parent + result["source_sha256"] = {name: sha256((package / name).read_bytes()).hexdigest() for name in FILES} + result["status"] = "PASS_A2_FIVE_TARGET_CAP_THREE" + return result + + +if __name__ == "__main__": + print(json.dumps(verify(), sort_keys=True, indent=2))