diff --git a/research/odd-dihedral-joint-tariff/OVERLAP.json b/research/odd-dihedral-joint-tariff/OVERLAP.json new file mode 100644 index 0000000000..b872b7aede --- /dev/null +++ b/research/odd-dihedral-joint-tariff/OVERLAP.json @@ -0,0 +1,171 @@ +{ + "status": "POSSIBLE_OVERLAP_NOT_A_NOVELTY_CERTIFICATE", + "searched_at": "2026-10-14T15:18:21.577400+00:00", + "terms": [ + "odd period", + "odd dihedral", + "antipodal", + "finite-dihedral" + ], + "entry_coverage": { + "open_prs": { + "fetched_at": "2026-10-14T14:59:01.036857+00:00", + "complete_pagination": true, + "records": 601 + }, + "discussions": { + "fetched_at": "2026-10-14T15:00:56.703857+00:00", + "complete_pagination": true, + "records": 578 + } + }, + "final_coverage": { + "open_prs": { + "fetched_at": "2026-10-14T15:16:16.140418+00:00", + "complete_pagination": true, + "records": 535 + }, + "discussions": { + "fetched_at": "2026-10-14T15:18:21.498074+00:00", + "complete_pagination": true, + "records": 592 + } + }, + "warnings": [], + "limits": "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.", + "matches_total": 12, + "relevant_matches": [ + { + "kind": "pr", + "number": 1941, + "title": "Research: sharp even finite-dihedral tariffs with dirty workspace", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1941", + "head": "5938ce3e91bbb8b5c2227af7976d444b2fbac7d4", + "updated_at": "2026-10-14T14:33:00Z", + "draft": false, + "state": "open", + "matched_terms": [ + "odd period", + "finite-dihedral" + ], + "score": 4, + "excerpt": "at is new\n\nThis closes the explicitly open **finite-torsion** question in #1911 (`712593f8`): its infinite-dihedral Laurent invariant does not descend through `r^n=1`. The new finite cut invariant does. In particular #1821's D16 central pair retains its 16-call minimum with arbitrarily many dirty roles, and the theorem covers all even periods and heterogeneous endpoints.\n\nThe all-register **D8 central-target** special case was already proved by steph4n-gh in #1573; it is credited, not claimed an" + }, + { + "number": 1955, + "title": "CLAIM: sharp odd finite-dihedral joint tariffs with dirty workspace", + "kind": "discussion", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1955", + "updated_at": "2026-10-14T15:03:43Z", + "matched_terms": [ + "finite-dihedral" + ], + "score": 3, + "excerpt": "CLAIM \u2014 odd finite-dihedral joint tariffs; bit-mechanisms / bit-new-register-model, scope refined. OS nonce 721bc4f2e2d9f3c304d6dab0f34c1803; priority revision 3; exact base 0b1cccf86e2f5132ed286a26ef0a681a495740ea; selected-record SHA256 10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32.\n\nQuestion: for every odd rotation period n=2m+1>=3, arbitrary heterogeneous diagonal targets r^k_i x^e_i in formal F2[D_{2n}], and any finite restored dirty workspace, do reflection-only rank-one" + }, + { + "kind": "pr", + "number": 1911, + "title": "Research: sharp infinite-dihedral reflection bills with arbitrary dirty registers", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1911", + "head": "712593f82739203639d0a169b88c6bcac6f0590c", + "updated_at": "2026-10-14T13:44:11Z", + "draft": false, + "state": "open", + "matched_terms": [ + "finite-dihedral" + ], + "score": 3, + "excerpt": "e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`.\n- Source byte/blob pins: `research/infinite-dihedral-register-bound/SOURCES.json`.\n- Coordination: https://github.com/CrocSwap/integer-mult-bounds/discussions/1884\n\nClosest inspected predecessors are #1573 (already proves all-register finite D8 central targets), #1478 (D8, two/three registers), #1821 (D16, two registers), #1733 (four-register rational two-relation ansatz), and #1822 (Q8). Exact heads are recorded in README and were r" + }, + { + "number": 1167, + "title": "Larger \u03ba: proposals that change the current cost structure", + "kind": "discussion-comment", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18926680", + "updated_at": "2026-10-14T15:01:20Z", + "matched_terms": [ + "odd period", + "finite-dihedral" + ], + "score": 2, + "excerpt": "pen PRs and 575 Discussions, complete pagination and no warnings. It surfaced PR #1941, whose sharp finite-dihedral tariff covers every even rotation order and explicitly excludes odd periods. This package is the odd order-five `D10` inverse-rotation slice. No exact D10/order-five target claim appeared. The D-infinity and D8/D16/S3 precedents are distinguished in the package.\n\n**Remaining obligations:** registered Python 3.12 replay and hosted CI; no native supplier/compiler, physical interface " + }, + { + "number": 1884, + "title": "Ten-instance independent research session: interface and verifier audits", + "kind": "discussion", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1884", + "updated_at": "2026-10-14T14:18:49Z", + "matched_terms": [ + "finite-dihedral" + ], + "score": 1, + "excerpt": "-writer domain (`6b222d01fee072bcd3a680e6a96ae7d22e13bcac`).\n- **bit-new-register-model:** formal infinite-dihedral F2 group algebra, paid reflections only, arbitrary finite dirty-workspace register count; investigate a sharp per-reflection lower bound for diagonal translation powers. Distinct from finite D8/D16/Q8 cases (#1573/#1821/#1822).\n- **complex-rank-shape-decoder:** P112 rank-one terms with at least one actual support confined to a canonical tetrad block, arbitrary opposite support/term" + }, + { + "number": 1929, + "title": "Round 2: ten independently seeded parallel research instances", + "kind": "discussion-comment", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1929#discussioncomment-18925900", + "updated_at": "2026-10-14T14:17:48Z", + "matched_terms": [ + "finite-dihedral" + ], + "score": 1, + "excerpt": "us endpoints with arbitrary workspace, not another finite-domain search. Expected artifact research/finite-dihedral-cut-bound with written theorem, independently implemented verifier, source pins, complete paid formal budget and controls. Claim expires 2026-10-14T16:30:00Z. Prepared for Adam Gall with substantial OpenAI Codex assistance." + }, + { + "number": 1929, + "title": "Round 2: ten independently seeded parallel research instances", + "kind": "discussion-comment", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1929#discussioncomment-18926159", + "updated_at": "2026-10-14T14:33:31Z", + "matched_terms": [ + "finite-dihedral" + ], + "score": 1, + "excerpt": "929#discussioncomment-18925900 (seed63537661f5ee8acaa486b70f82726911).\n\nEstablished: for every even finite-dihedral period n and every finite dirty-register count, arbitrary heterogeneous targets r^k x^e have sharp simultaneous reflection tariffs sum dist_n(k+e) x calls and sum dist_n(k) y calls. Two shifted finite permutation representations and balanced address-cut rank prove the all-length result; full formal coordinate words attain it. This resolves the finite-torsion next question of PR1911" + }, + { + "number": 1929, + "title": "Round 2: ten independently seeded parallel research instances", + "kind": "discussion-comment", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1929#discussioncomment-18926555", + "updated_at": "2026-10-14T14:55:04Z", + "matched_terms": [ + "finite-dihedral" + ], + "score": 1, + "excerpt": "ttps://github.com/CrocSwap/integer-mult-bounds/pull/1941) | Sharp per-letter tariffs for every even finite-dihedral period and heterogeneous targets with arbitrary restored dirty workspace. |\n| 03 | `4e1451a884a6979cb599a332ccc7ad40` | [#1940](https://github.com/CrocSwap/integer-mult-bounds/pull/1940) | Chronological P104 schedule attains PR1125's known32-path bound:416reads and24additional arrays, with conditional tail invoice. |\n| 04 | `3cc9f4c8f3719f13f4ae6bf28c9ba982` | [#1936](https://githu" + }, + { + "number": 1884, + "title": "Ten-instance independent research session: interface and verifier audits", + "kind": "discussion-comment", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1884#discussioncomment-18925359", + "updated_at": "2026-10-14T13:48:38Z", + "matched_terms": [ + "finite-dihedral" + ], + "score": 1, + "excerpt": " tetrad-local masked decoder COPY112 floor.\n- #1910: selected k8 omission observability.\n- #1911: infinite-dihedral reflection bills with dirty workspace.\n- #1912: selected generated-identity field-coverage audit (no defect found).\n- #1913: fixed-frame two-writer helper absorption obstruction.\n- #1915: generic dirty-connector rigidity under paid frames.\n- #1917: cross-fed handoff versus strengthened closed-call baseline.\n- #1918: exact composed scalar centre-source rank for one selected pair.\n\nE" + }, + { + "kind": "pr", + "number": 1953, + "title": "Research: D10 inverse rotations retain four-call minimum", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1953", + "head": "4f3bdf7c3bdd7033180c9d8c41245023cc402bc6", + "updated_at": "2026-10-14T14:59:43Z", + "draft": false, + "state": "open", + "matched_terms": [ + "odd period" + ], + "score": 1, + "excerpt": "iscussion #1929\ncomment 18925900, proves tariffs for every even rotation order and expressly\nleaves odd periods out. This package treats odd rotation order five and the\ninverse-rotation pair. The final overlap refresh at 2026-10-14 14:56:57 UTC\ncovered 601 open PRs and 575 Discussions with complete pagination and no\nwarnings; no D10 target claim was found. Prepared with\nsubstantial OpenAI Codex assistance. No independent human review is claimed.\n" + } + ], + "scope_delta": "Odd rather than even period; all heterogeneous formal endpoints and any finite dirty workspace. New regular-action cut supplies the missing joint charge. PR1953 is a credited finite special case, not an unclaimed instance." +} diff --git a/research/odd-dihedral-joint-tariff/PROOF.md b/research/odd-dihedral-joint-tariff/PROOF.md new file mode 100644 index 0000000000..cde698569a --- /dev/null +++ b/research/odd-dihedral-joint-tariff/PROOF.md @@ -0,0 +1,357 @@ +# Odd finite dihedral groups: separate cuts and a sharp joint tariff + +This is an all-parameter written proof for the formal operation model below. +Finite executable checks corroborate its implementation; they do not replace +the proof, and no formal-kernel verification is asserted. This result supplies +no physical BIT supplier, recursive child profile, precision estimate, or new +multiplication exponent. + +## Statement and exact operation model + +Let `n=2m+1`, where `m>=1`, and let + +``` +G = D_(2n) = , +y = r^-1 x, so that xy=r. +``` + +The coefficient ring is the full, generally noncommutative group algebra +`F2[G]`. There are any finite number `R>=W` of scalar register roles. A paid +unit call has the form + +``` +D_N(g) = I_R + ([g]+1) N, +g in {x,y}, +N = u v^T over F2, with v^T u = 1. +``` + +Thus `N` is any binary rank-one idempotent, including non-coordinate ones. +Arbitrary scalar `GL_R(F2)` maps are free and may be interleaved anywhere. +They act on roles, not on group addresses. There are no additional free +address operations, clean inputs, resets, erasures, or COPY operations. +All inputs, including all spectator inputs, are arbitrary. The required +complete formal endpoint is + +``` +T = diag([r^k_1 x^e_1], ... , [r^k_W x^e_W], 1, ... , 1), +e_i in {0,1}. +``` + +In particular, every spectator is restored and every off-diagonal role +coupling vanishes. Every paid call used for preparation or restoration is +included in the bill. + +Define, for integers `k`, + +``` +d_n(k) = min(k mod n, n-(k mod n)), +A = sum_i d_n(k_i+e_i), +B = sum_i d_n(k_i), +t = #{i : e_i=1 and k_i=m mod n}. +``` + +The unique exceptional group element is the longest reflection `r^m x`. +If a circuit has `X` paid x calls and `Y` paid y calls, then + +``` +X >= A, +Y >= B, +X+Y >= A+B+t. (1) +``` + +For every integer `j` with `0<=j<=t`, the pair + +``` +(X,Y) = (A+j, B+t-j) (2) +``` + +is attained by a literal coordinate-projector circuit with no extra roles +and no scalar basis changes. Every feasible count pair componentwise +dominates at least one pair in (2). These statements do not characterize +every feasible pair away from that boundary. + +Consequently, for arbitrary nonnegative real prices `alpha,beta`, the exact +minimum weighted cost is + +``` +alpha*A + beta*B + t*min(alpha,beta). (3) +``` + +This includes zero prices. The exact minimum unweighted number of calls is +`A+B+t`. The bounds hold uniformly over all finite `R`, all word lengths, all +allowed rank-one idempotents, and all interleavings with free scalar maps. + +## The common cut-rank argument + +Given a permutation action of `G` on a finite address set `Omega`, extend it +linearly to `F2[G]` and entrywise to register matrices. Choose a partition +`Omega=H disjoint_union K`, and include every scalar role in each side. For +an operator `M` on the represented space define + +``` +q_H(M) = rank_F2 M[K,H]. +``` + +Here the block takes inputs supported on `H` to outputs supported on `K`. +Block multiplication gives + +``` +(UV)[K,H] = U[K,H] V[H,H] + U[K,K] V[K,H], +q_H(UV) <= q_H(U) + q_H(V). (4) +``` + +No invertibility is needed for this inequality. A free scalar map is +`S tensor I_Omega` and has crossing rank zero. For a paid call the crossing +block is + +``` +N tensor rho(g)[K,H], +``` + +so its rank is `rank(N)*q_H(rho(g))=q_H(rho(g))`. +For a permutation `g`, the crossing block is a partial permutation matrix, +and its rank is the number of elements of `H` mapped into `K`. + +The endpoint is diagonal in roles, so its crossing blocks are direct sums +of the target crossing blocks. Their ranks add; identity spectators +contribute zero. Formal equality of circuits implies equality under every +representation used here. The proof never takes represented equality as a +sufficient certificate of formal equality. + +This directly handles interleaved free scalar operations. Equivalently, +one can normalize them by + +``` +S D_N(g) S^-1 = D_(SNS^-1)(g). +``` + +Conjugation preserves binary rank-one idempotence. Applying augmentation +`[g] -> 1` to the full formal endpoint shows that the product of all free +scalar factors must be `I_R`. Thus normalization leaves no unpriced scalar +endpoint. This observation is consistent with, but not needed for, (4). + +## The two separate-letter cuts + +The finite permutation representations and separate-letter cut idea are +inherited from Adam Gall's even-period result in +[PR1941](https://github.com/CrocSwap/integer-mult-bounds/pull/1941), pinned at +`5938ce3e91bbb8b5c2227af7976d444b2fbac7d4`. The argument is checked here for +the changed odd period and its unequal sides. + +On addresses `a in Z/nZ`, for any integer `c`, put + +``` +rho_c(r)(a) = a+1, +rho_c(x)(a) = c-a, +rho_c(y)(a) = c-1-a. +``` + +These permutations satisfy the displayed presentation of the actual finite +group. Use `H={0,...,m-1}` of size `m`; its complement has size `m+1`. +For any interval of length `m` or `m+1` on the `(2m+1)`-cycle, translation +by `k` sends exactly `d_n(k)` of its points outside the interval. To see +this, it suffices to take `0<=k<=m`, for which precisely `k` points leave; +negative translations give the same count and exhaust the other residues. + +For `c=m`, the letter y preserves H while x sends H to `H+1`. The per-call +crossing ranks are therefore `(1,0)` for `(x,y)`. For `c=m-1`, x preserves +H while y sends it to `H-1`, giving `(0,1)`. A rotation translates H by k. +A reflection `r^k x` sends H to + +``` +H + (k+c-m+1). +``` + +The endpoint crossing ranks are therefore + +``` +c=m: sum_i d_n(k_i+e_i) = A, +c=m-1: sum_i d_n(k_i) = B. +``` + +Applying (4) proves the first two inequalities in (1). These unequal cuts +alone miss one call for each longest reflection: its two ranks are `(m,m)`. +The next cut supplies the joint constraint without a parity relaxation. + +## A regular-action cut gives the full alternating-word length + +Use the faithful left regular action on the `2n` addresses + +``` +(a,e) <-> r^a x^e, a in Z/nZ, e in {0,1}. +``` + +In these coordinates, + +``` +r(a,e) = (a+1,e), +x(a,e) = (-a,1-e), +y(a,e) = (-a-1,1-e), +(r^k x)(a,e) = (k-a,1-e). +``` + +Let `I={-m,...,0}` and `J={0,...,m-1}`, interpreted modulo n. Choose the +balanced regular-address cut + +``` +H = (I x {0}) union (J x {1}), +K = (G-addresses) minus H. +``` + +Both sides have size `n`. Write `q(g)` for the crossing rank of the left +regular permutation of g at this cut. + +For a rotation, each layer is simply translated. The two intervals have +lengths `m+1` and `m`, respectively, so the interval calculation above yields + +``` +q(r^k) = 2 d_n(k). (5) +``` + +A reflection interchanges the layers, and + +``` +(r^k x) H = ((k-J) x {0}) union ((k-I) x {1}). +``` + +The two intersection sizes `|I intersect (k-J)|` and +`|J intersect (k-I)|` are equal under `a -> k-a`. Since H has n points, + +``` +q(r^k x) = n - 2 |I intersect (k-J)|. (6) +``` + +Choose the unique representative `k' in {-m,...,m}`. For `0<=k'<=m`, the +intersection in (6) has `m-k'` points: it is the part of +`{k'-m+1,...,k'}` lying in `{-m,...,0}`. No additional modular intersection +occurs because the positive endpoints are at most m. For `k'=-j` with +`1<=j<=m`, the intersection is `{-m,...,-j}`, of size `m-j+1`. The part +below `-m` wraps to positive residues at most m and adds no points of I. +It follows that + +``` +q(r^k x) = 2k'+1, if 0<=k'<=m, + -2k'-1, if -m<=k'<=-1. (7) +``` + +In particular, `q(x)=1` and `q(y)=1`. At the longest reflection `k'=m`, +the rank is `2m+1=n`: it interchanges H and K completely. For every other +reflection it is `d_n(k+1)+d_n(k)`. Equations (5)--(7) can thus be written +uniformly as + +``` +q(r^k x^e) = d_n(k+e)+d_n(k) + + 1_{e=1 and k=m mod n}. (8) +``` + +The quantities in (5)--(7) also equal the lengths of the shortest +alternating x/y words. This equality does not need an independent word +metric theorem: subadditivity and `q(x)=q(y)=1` give a lower bound on any +literal word, and the attaining words below have exactly these lengths. + +By additivity over roles, the endpoint has regular-cut crossing rank +`A+B+t`. Each paid call has crossing rank one at this cut, and each free +scalar operation has rank zero. Equation (4) proves + +``` +X+Y >= A+B+t, +``` + +the remaining inequality in (1). It applies to arbitrarily many longest +reflections simultaneously, without limiting the number of restored dirty +spectators. + +## Attaining formal circuit and complete invoice + +Let `E_i` be the coordinate projector onto role i. In the full formal group +algebra, directly multiplying the two factors gives + +``` +D_(E_i)(g) D_(E_i)(h) = D_(E_i)(gh). (9) +``` + +Indeed `E_i^2=E_i`, and in characteristic two the coefficient of `E_i` +reduces to `[gh]+1`. No permutation representation is used to certify (9). +Calls on distinct coordinate roles commute. + +For rotations, take the representative `k' in {-m,...,m}` and the literal +word `(xy)^k'`, interpreting negative powers as repetitions of `yx`. Its +counts are `(d_n(k),d_n(k))`. + +For a reflection other than `r^m x`, choose `k' in {-m,...,m-1}` and freely +reduce `(xy)^k' x`. If `k'>=0`, its counts are `(k'+1,k')`; if `k'=-j<0`, +they are `(j-1,j)`. In either case the counts are exactly +`(d_n(k+1),d_n(k))`. + +The longest reflection has the two formal words + +``` +(xy)^m x = r^m x, +(yx)^m y = r^(-m-1) x = r^m x, +``` + +with counts `(m+1,m)` and `(m,m+1)`. Choose the first word on exactly j of +the t longest-reflection roles and the second on the remainder. Equations +(9) and the group relation `r^n=1` prove the complete formal endpoint with +the counts in (2). With column-vector conventions, the rightmost displayed +factor acts first, so each displayed product is executed right to left. + +For any feasible counts write `X=A+u`, `Y=B+v`. By (1), the integers u,v +are nonnegative and `u+v>=t`. There is an integer + +``` +max(0,t-v) <= j <= min(t,u), +``` + +so `(X,Y)` componentwise dominates `(A+j,B+t-j)`. Nonnegative weights +therefore have minimum (3), attained by selecting the cheaper extra letter +on each longest-reflection role. Equal weights permit every choice of j. + +| Resource | Complete attaining implementation | +| --- | --- | +| Arbitrary-input target roles | W | +| Extra roles required | Zero; any added spectators remain untouched | +| Paid x/y calls | `(A+j,B+t-j)` for chosen `0<=j<=t` | +| Scalar changes of basis | Zero | +| Clean inputs, COPYs, resets, erasures | None | +| Extra preparation or inverse restoration | None hidden or deferred | +| Endpoint verification | Equality in the full formal group algebra | +| Physical supplier or recursive adoption | Not supplied | + +The lower-bound argument also applies to arbitrary-rank binary idempotent +calls if each call is charged its scalar rank: (1) then bounds x rank mass, +y rank mass, and their sum. This is not an invocation-count optimum for +batched calls and does not price recursive children by their rank. + +## Scope, predecessor credit, and remaining obligations + +The separate-letter construction and the explicit odd-period gap come from +Adam Gall's [PR1941](https://github.com/CrocSwap/integer-mult-bounds/pull/1941), +at the pinned head above. Adam Gall's +[PR1911](https://github.com/CrocSwap/integer-mult-bounds/pull/1911), head +`712593f82739203639d0a169b88c6bcac6f0590c`, supplies the infinite-dihedral +predecessor and its finite-torsion question. The new mathematical step here +is the regular-action cut (6)--(8) that closes the joint odd-period tariff; +the general subadditive cut-rank principle is not claimed as new. + +Relevant overlapping evidence also includes the coordinate/CNOT setting of +[PR1414](https://github.com/CrocSwap/integer-mult-bounds/pull/1414) and +Cinna Davis's [PR1953](https://github.com/CrocSwap/integer-mult-bounds/pull/1953), +head `4f3bdf7c3bdd7033180c9d8c41245023cc402bc6`, with its finite D10 +inverse-rotation special case. Those special cases are credited, not claimed +as previously unsettled instances. This proof allows every binary rank-one +idempotent, arbitrary free scalar mixing, and any finite number of restored +dirty spectators. Overlap review and publication status belong to the package +metadata; this mathematical proof is not a novelty certificate. + +The covered domain is odd `n>=3`, any finite `R>=W`, and complete diagonal +formal endpoints of the displayed kind. The proof uses no integer lift, +analytic approximation, or precision assumption: the historical scalar +mixing permission is an optimistic formal relaxation. Moving to a physical +supplier would require independently admitting and pricing the native group +actions, all frame/compiler and hosting work, precision/tape behavior, and +the full recursive profile. None of those obligations follows from the +formal tariff. Other free address maps, other paid labels, partial endpoint +contracts, clean ancillas, or nonlinear operations are outside this theorem. + +Prepared with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/odd-dihedral-joint-tariff/README.md b/research/odd-dihedral-joint-tariff/README.md new file mode 100644 index 0000000000..05f26becee --- /dev/null +++ b/research/odd-dihedral-joint-tariff/README.md @@ -0,0 +1,165 @@ +# Odd dihedral groups: exact joint reflection tariffs with dirty workspace + +**Scoped all-parameter theorem; no new kappa.** For every odd rotation +period `n=2m+1>=3`, arbitrary heterogeneous diagonal targets in formal +`F2[D_(2n)]` cannot share paid reflection calls below their direct bill, +even with arbitrary free scalar register mixing and any finite restored +dirty workspace. The missing joint charge is one call for **each** longest +reflection, not merely the parity of their number. + +This closes the odd-period question explicitly left by Adam Gall's +[PR1941](https://github.com/CrocSwap/integer-mult-bounds/pull/1941), pinned at +`5938ce3e91bbb8b5c2227af7976d444b2fbac7d4`. Its two separate cut bounds are +credited and extended to unequal halves. The new step uses a cut in the +faithful regular action to obtain the full joint charge. The proof is in +[PROOF.md](PROOF.md); finite checks support that proof rather than imply it. + +## Model and sharp result + +Let `r=xy`, `x^2=y^2=1`, `r^n=1`. A paid unit is +`I+([g]+1)N`, where `g` is **only x or y**, and `N=uv^T` is any binary +rank-one idempotent (`v^T u=1`). Scalar `GL_R(F2)` operations are free in +this optimistic model. No other free address maps, COPYs, erasures or clean +allocations are permitted; every preparation/restoration call is counted. + +For the complete endpoint +`diag([r^k_1 x^e_1],...,[r^k_W x^e_W],1,...,1)`, with every input arbitrary, +define + +``` +A = sum_i d_n(k_i+e_i), B = sum_i d_n(k_i), +t = number of i with e_i=1 and k_i=m mod n, +d_n(k) = min(k mod n, n-(k mod n)). +``` + +Every circuit has `X>=A`, `Y>=B`, and **`X+Y>=A+B+t`**. Every pair +`(A+j,B+t-j)`, `0<=j<=t`, is attained by coordinate-role words. Thus the +exact optimum for arbitrary nonnegative real prices is + +``` +alpha*A + beta*B + t*min(alpha,beta). +``` + +The attaining circuits require zero extra roles or scalar changes of basis, +and no uncharged cleanup. These are sharp formal tariffs, not physical +supplier costs or recursive moments. + +For example, two longest reflections at `n=5` have `A=B=4`, `t=2`. +The separate bounds and parity alone permit an eight-call bill. The new +regular cut forces ten calls; the sharp pairs are `(4,6),(5,5),(6,4)`. +At `n=3`, the result covers any number of coordinate-SWAP targets and any +number of restored dirty spectators. Previously established special cases +retain their credit; the contribution is the uniform odd-period argument. + +## Why the new cut works + +Represent the group by left multiplication on its own `2n` elements, +written `(a,e)=r^a x^e`. Use + +``` +H = {(-m,0),..., (0,0)} union {(0,1),..., (m-1,1)}. +``` + +Both x and y have one crossing from H to its complement. The crossing +rank of a target is its shortest alternating-word length: +`d_n(k+e)+d_n(k)+1_(e=1,k=m)`. Crossing rank is subadditive under operator +composition and additive on the required diagonal endpoint. A scalar map +does not cross addresses, and an arbitrary rank-one scalar projector +multiplies a generator's crossing rank by one. These facts give the bound +with no limit on role count or word length. Literal formal words attain it. + +## Exact evidence and reproduction + +Python 3.12+, standard library only: + +```sh +python3.12 -I -B scripts/research_package.py --package research/odd-dihedral-joint-tariff +python3.12 -I -O -B research/odd-dihedral-joint-tariff/verify.py +``` + +`verify.py` compares full formal coefficient matrices with a separately +specified faithful regular-action interpreter. The latter builds the group +from literal permutations, then applies every call to all basis columns; +it does not use the formal multiplication or update routines. Both receive +the same declared `(label,u,v)` factors. Binary elimination computes actual +crossing ranks. Neither proof-representation equality nor hashes alone +certify an endpoint. + +The fixed [RECEIPT.json](RECEIPT.json) records: + +| Covered finite domain | Checks | +| --- | ---: | +| Every group element, odd `n=3..31` | 510 targets, 525 attaining words | +| Every group-element pair, odd `n=3..15` | 2,716 independent multiplication comparisons | +| Every rank-one projector through four roles, `n=3,5,7,9,11` | 1,550 factor checks | +| Every paid word of lengths 0–3 on two roles, `n=3,5` | 3,770 full operator comparisons | +| All ordered target pairs, `n=3,5,7`, with one dirty spectator | 392 forward and 392 inverse words | +| Mixed tuples with 0–5 longest reflections, up to eight roles | 84 words, every surplus-letter split | +| All scalar invertible maps through three roles | 4,741 projector conjugations; 350 zero-cut checks | +| Nonnegative rational prices, including zero | 8,300 comparisons | + +All 2,478 single-call omission controls reject. Additional controls cover +missing joint charges, each separate-letter underbill, dirty leakage, +unrestored spectators, wrong noncommuting order, illegal labels/projectors, +and even-period misuse. An invertible dirty shear by +`sum_(g in G)[g]` is invisible in both small proof representations but is +rejected by the full formal endpoint and detected by the faithful action. +A non-coordinate cancelling presentation is accepted. + +The package tests remove the actual x, y, joint, and endpoint detectors +in disposable in-memory variants; the associated negative-control harness +then fails. They also reject a missing/duplicate/corrupted receipt and +changed source bytes, compare explicit regeneration byte for byte, and run +an isolated optimized replay from a minimal read-only relocation. Normal +verification never regenerates missing evidence. `--emit` prints a fresh +receipt only when explicitly requested. + +A separate specialist wrote [independent_check.py](independent_check.py) without +importing this package. It checks all 5,200 single targets over odd periods +3–101 using set images and literal-word Pareto search through length n, plus 216 +full-matrix scalar conjugations. It requires assertions and explicitly refuses +optimized execution; the main checker supports `-O`. + +These are finite software checks. The universal statement comes from the +written proof; no Lean, independent human proof review, native admission, +selected cold replay, or hosted CI success is inferred from them. Actual +local commands and environment are in [VALIDATION.json](VALIDATION.json). + +## Provenance, overlap, and credit + +Base `0b1cccf86e2f5132ed286a26ef0a681a495740ea`; one OS chooser draw +`721bc4f2e2d9f3c304d6dab0f34c1803`, bit-mechanisms / bit-new-register-model, +target-specific relaxation method, priority revision 3. [TASK.json](TASK.json) +records the refinement, bounds, stop rule and next question. The initial +[claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1955) +precedes the package computation. [SOURCES.json](SOURCES.json) binds the +context and selected-record provenance; predecessor code is not imported. +[OVERLAP.json](OVERLAP.json) records coverage and its limits. + +Credit Adam Gall's PR1941 even-period cut construction and explicit open +question, and PR1911 infinite-dihedral theorem; commdata2338's PR1414 +coordinate-CNOT proof; Cinna Davis's PR1541 arbitrary-workspace three-swap +theorem and PR1870 +two-role S3 census and PR1953 three-role D10 inverse-rotation result; +Ross Richardson's PR1766 full-occupancy four-swap theorem and its explicit +dirty-workspace gap; Aaron Wang's PR1763 finite rotation-target census; and +eumemic PR288, Ali Romman PR468, Gareth Davidson PR1333 and the retained +register-model lineage. The relevant live heads are pinned in SOURCES. +Known finite or all-register special cases are not claimed as newly open. +No literature-priority claim is made for rank subadditivity. + +Prepared for Ross Richardson with substantial OpenAI Codex assistance in +proof, implementation, testing and writing. A bit-supplier specialist wrote +the proof; a separate exact-verification specialist reviewed it and the +code. This is AI-assisted checking, not independent human review. +Apache-2.0. Frozen inputs and the selected frontier are unchanged. + +## Open next questions + +The two-reflection model now has no formal sharing headroom. A useful next +step must change a material hypothesis: specify one physically justified +new native operation and price its full entrance/exit map, child histogram, +restoration, frames and hosting. Compare its cut ranks to the complete bill +before attempting construction. A source-bound compiler/hosting/precision/ +tape bridge and a replacement complete recursive profile are still missing; +the current result supplies neither. See the structured question in TASK. diff --git a/research/odd-dihedral-joint-tariff/RECEIPT.json b/research/odd-dihedral-joint-tariff/RECEIPT.json new file mode 100644 index 0000000000..368227b236 --- /dev/null +++ b/research/odd-dihedral-joint-tariff/RECEIPT.json @@ -0,0 +1,128 @@ +{ + "counts": { + "all_projector_factor_checks": 1550, + "complete_group_pairs": 2716, + "complete_pair_attaining_words": 392, + "complete_short_words": 3770, + "complete_single_targets": 510, + "factor_regular_basis_columns": 80780, + "free_scalar_cut_checks": 350, + "larger_mixed_tuple_words": 84, + "larger_tuple_regular_basis_columns": 8512, + "pair_inverse_words": 392, + "pair_regular_basis_columns": 13872, + "rational_price_checks": 8300, + "scalar_projector_conjugations": 4741, + "short_word_regular_basis_columns": 60320, + "single_attaining_words": 525, + "single_call_omissions": 2478 + }, + "domains": { + "all_group_pairs_periods": [ + 3, + 5, + 7, + 9, + 11, + 13, + 15 + ], + "all_ordered_target_pairs": { + "periods": [ + 3, + 5, + 7 + ], + "roles": 3 + }, + "all_projectors_periods": [ + 3, + 5, + 7, + 9, + 11 + ], + "all_projectors_roles": [ + 1, + 2, + 3, + 4 + ], + "all_scalar_GL_roles": [ + 1, + 2, + 3 + ], + "complete_short_words": { + "lengths": [ + 0, + 1, + 2, + 3 + ], + "periods": [ + 3, + 5 + ], + "roles": 2 + }, + "larger_mixed_tuples": { + "dirty_spectators": 1, + "exceptional_counts": [ + 0, + 1, + 2, + 3, + 4, + 5 + ], + "ordinary_targets": [ + "x", + "r^-1" + ], + "periods": [ + 3, + 5, + 9, + 15 + ] + }, + "odd_periods_all_targets": [ + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31 + ] + }, + "mathematical_digest_sha256": "13c455a200fdf09562cb9d7e2751b947d6be855c040042c0f8b9ac5e00aa8622", + "schema_version": 1, + "scope": "finite corroboration; universal theorem is PROOF.md; no_new_kappa", + "semantic_controls": [ + "even-period misuse", + "negative tariff", + "illegal rotation label", + "non-idempotent scalar factor", + "foreign scalar role", + "joint deficit n=3", + "wrong noncommuting order n=3", + "joint deficit n=5", + "wrong noncommuting order n=5", + "x bill hidden by large y bill", + "y bill hidden by large x bill", + "dirty spectator leaks into target", + "spectator not restored", + "proof-representation false endpoint", + "positive noncoordinate cancelling presentation" + ] +} diff --git a/research/odd-dihedral-joint-tariff/SELECTION.json b/research/odd-dihedral-joint-tariff/SELECTION.json new file mode 100644 index 0000000000..a1b4f7d96b --- /dev/null +++ b/research/odd-dihedral-joint-tariff/SELECTION.json @@ -0,0 +1,90 @@ +{ + "seed": "721bc4f2e2d9f3c304d6dab0f34c1803", + "track": "bit-mechanisms", + "suggestions": [ + { + "task_id": "bit-new-register-model", + "scope_key": "7084092dd726e7ba1f2f", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "method": "Derive a target-specific relaxation bound for that same explicit alphabet.", + "starting_points": [ + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json" + ], + "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_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + }, + { + "task_id": "bit-helper-contract", + "scope_key": "3475f46c8358c6a9211b", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "method": "Derive a replacement interface lemma and price its implementation.", + "starting_points": [ + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "research/r439-bsection-stars-seed01/verify.py" + ], + "expected": "PASS_R439_BSECTION_STARS", + "inspect": "Compare the two false H2/K flags with the unchanged paid profile in its README.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write one replacement H2/K implication for a single helper-star operation, then try to falsify it on dirty inputs.", + "bottleneck_link": "A legitimate replacement could admit a cheaper bit circuit; scalar savings alone do not alter the selected moment.", + "allowed_variations": [ + "Choose one helper-star or quartet instance; narrow to one boundary implication." + ], + "scope_change_triggers": [ + "Changing only source count or scalar addition count without an interface argument." + ], + "overlap_terms": [ + "H2_D_frame0_targets_from_helpers", + "K_equals_D", + "helper-star" + ], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + } + ], + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "catalog_assessed_on": "2026-10-13", + "priority_revision": 3, + "priority_log": "docs/research/research-priority-log.md", + "catalog_sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "selected": { + "kappa": "836330098538459/500000000000000000", + "review": "docs/research/community-batch1099-review.md", + "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "reproduce": "make frontier1094-verify" + }, + "status": "SUGGESTIONS_ONLY_NOT_RESERVED", + "next_step": "Check live overlap, refine one question's object and domain, and record a bounded task card. A different seed or scope key is not evidence of novelty." +} diff --git a/research/odd-dihedral-joint-tariff/SOURCES.json b/research/odd-dihedral-joint-tariff/SOURCES.json new file mode 100644 index 0000000000..a916ccc33f --- /dev/null +++ b/research/odd-dihedral-joint-tariff/SOURCES.json @@ -0,0 +1,79 @@ +{ + "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" + }, + { + "path": "research/bit-three-register-lower-bound/README.md", + "usage": "input", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + }, + { + "path": "research/coordinate-cnot-register-bound/README.md", + "usage": "input", + "git_blob": "cdcc5a9e7f11ab3dbf7745a175ddcca208c68211", + "sha256": "e1666512fb71cf34c427c69ffb61a18b61e897a7f8f91f87820edf744e85a9fe" + } + ], + "context_predecessors": [ + { + "pr": 1941, + "author": "Adam Gall", + "head": "5938ce3e91bbb8b5c2227af7976d444b2fbac7d4", + "path": "research/finite-dihedral-cut-bound/README.md", + "git_blob": "7ef17c9f10e4c32292f6cb92ea6e19628b1638f1", + "sha256": "d8a94457ecb8e79caa22bd66d34b873556c365d2b5847d936b3ab531cc79c04a", + "usage": "context only; proof read at this head; no predecessor code imported" + }, + { + "pr": 1911, + "author": "Adam Gall", + "head": "712593f82739203639d0a169b88c6bcac6f0590c" + }, + { + "pr": 1953, + "author": "Cinna Davis", + "head": "4f3bdf7c3bdd7033180c9d8c41245023cc402bc6" + }, + { + "pr": 1870, + "author": "Cinna Davis", + "head": "538d194e69420a6a773612e0b5ad0c94575f8aaa" + }, + { + "pr": 1414, + "author": "commdata2338", + "retained_path": "research/coordinate-cnot-register-bound/README.md" + }, + { + "pr": 1541, + "author": "1337isnot1337", + "head": "194724d87505ec2517fdca1c1884da12398f4c33", + "usage": "context and special-case attribution; not imported" + }, + { + "pr": 1766, + "author": "RossRichardson", + "head": "ff68746efa11b491734362d82ac7ff359aa1b48b", + "usage": "context and special-case attribution; not imported" + }, + { + "pr": 1763, + "author": "navinor", + "head": "07910c7bee862dadbb3b3d30ea5dfcdbbbe23fda", + "usage": "context and special-case attribution; not imported" + } + ] +} diff --git a/research/odd-dihedral-joint-tariff/TASK.json b/research/odd-dihedral-joint-tariff/TASK.json new file mode 100644 index 0000000000..9a081f0ba9 --- /dev/null +++ b/research/odd-dihedral-joint-tariff/TASK.json @@ -0,0 +1,64 @@ +{ + "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": "Every odd finite dihedral period n>=3, every heterogeneous formal diagonal target and every finite arbitrary dirty scalar workspace: sharp joint x/y tariffs with rank-one idempotent paid calls.", + "scope_change_reason": "Choose a specified nonabelian family outside the rational abelian starting model; change PR1941 even period to odd and resolve its missing longest-reflection joint charge using a faithful regular-action cut.", + "bottleneck_link": "Mechanism-screening side result: this optimistic reflection-only model cannot save its direct formal call bill. The selected bit primitive is nonbinding; no selected moment or kappa change.", + "budget_minutes": 60, + "stop_rule": "Stop construction effort on proving the direct bill sharp, or stop the theorem if a cut formula fails; reserve final quarter of ~60min for checking/publication/cleanup.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py; RECEIPT.json; exact source pins and documented limitations.", + "author": "Ross Richardson, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in proof, code, tests and writing; bounded bit-supplier and exact-verification specialist review. No independent human or Lean proof review.", + "open_questions": [ + { + "question": "Can a physically justified paid alphabet outside the two reflections provide a complete supplier saving?", + "why_it_matters": "The sharp formal tariff eliminates sharing as a source of headroom in this exact alphabet, but does not constrain a genuinely different primitive or recursive bill.", + "first_step": "Specify one new native operation, its complete entrance/exit map and charged child histogram; compare its representation cut ranks with its full cost before constructing a network.", + "blocked_by": "No source-bound physical/compiler/hosting/precision/tape bridge or replacement complete recursive profile is supplied here." + } + ], + "scope_key": "7084092dd726e7ba1f2f/odd-dihedral/all-periods/all-roles/joint-tariff", + "seed": "721bc4f2e2d9f3c304d6dab0f34c1803", + "method": "Target-specific rank relaxation, uniform proof, independently specified exact formal and regular-action checks.", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1955" +} diff --git a/research/odd-dihedral-joint-tariff/TASK.md b/research/odd-dihedral-joint-tariff/TASK.md new file mode 100644 index 0000000000..13788d03c1 --- /dev/null +++ b/research/odd-dihedral-joint-tariff/TASK.md @@ -0,0 +1,13 @@ +CLAIM — odd finite-dihedral joint tariffs; bit-mechanisms / bit-new-register-model, scope refined. OS nonce 721bc4f2e2d9f3c304d6dab0f34c1803; priority revision 3; exact base 0b1cccf86e2f5132ed286a26ef0a681a495740ea; selected-record SHA256 10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32. + +Question: for every odd rotation period n=2m+1>=3, arbitrary heterogeneous diagonal targets r^k_i x^e_i in formal F2[D_{2n}], and any finite restored dirty workspace, do reflection-only rank-one-idempotent calls have sharp tariff alpha*A + beta*B + t*min(alpha,beta)? Here r=xy, A=sum d_n(k_i+e_i), B=sum d_n(k_i), and t counts the longest reflection r^m x. Scalar GL_R(F2) mixing is free only in this stated optimistic model; all x/y preparation/restoration calls count, no other address gates/COPY/clean state. + +Changed premise: PR1941 (Adam Gall, exact head 5938ce3e91bbb8b5c2227af7976d444b2fbac7d4) proves even periods and explicitly leaves the missing odd-period joint constraint open. We reuse and credit its two cut bounds, then test a new n-address half of the faithful 2n-address regular action whose crossing rank should equal each target's shortest word length. This would imply #x+#y>=A+B+t, rather than parity alone, and direct coordinate words should attain all minimal count pairs (A+j,B+t-j), 0<=j<=t. + +Method/domain: all-parameter written proof plus exact finite corroboration over complete small odd groups, all rank-one projectors through four roles, full formal coefficient and independent regular-action endpoint checks with dirty states and meaningful failure controls. Target budget is the complete direct formal bill; stop if any cut or endpoint formula fails. No physical supplier or kappa gain is proposed. + +Overlap: complete entry snapshot covers 601 open PRs and 578 Discussion records at 14:59–15:00 UTC; targeted odd-period search finds PR1941 and Cinna Davis PR1953 (head 4f3bdf7c3bdd7033180c9d8c41245023cc402bc6), the r=3 D10 inverse-rotation special case. PR1870 and the coordinate-CNOT line cover S3 finite cases; these will be credited, not reclaimed. PR1911 is the infinite-dihedral predecessor. No novelty guarantee is inferred from text searches. + +Expected artifact: research/odd-dihedral-joint-tariff, written proof, standard-library exact checker, source pins, controls and narrow reproduction. Claim expiry 2026-10-14 17:15 UTC. Prepared for Ross Richardson with substantial OpenAI Codex assistance; Apache-2.0. + +Worktree owner: integer-multiplication-research-sprint. Path /Users/ross/git/math/donated-20261014-1457. Branch research/donated-20261014-1457. All specialists share this checkout with disjoint file ownership. diff --git a/research/odd-dihedral-joint-tariff/VALIDATION.json b/research/odd-dihedral-joint-tariff/VALIDATION.json new file mode 100644 index 0000000000..c53a10355d --- /dev/null +++ b/research/odd-dihedral-joint-tariff/VALIDATION.json @@ -0,0 +1,56 @@ +{ + "recorded_at_utc": "2026-10-14T15:19:56.741957+00:00", + "base": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "main_at_submission_check": "ecc75c79c22d909fd42aa68437eb77c4c1361835", + "main_advance_effect": "Selected record, guidance, task catalogue, both pinned inputs and replay runner were byte-identical; original research base retained.", + "environment": { + "system": "macOS-26.5.2-arm64-arm-64bit-Mach-O", + "registered_python": "Python 3.12.12", + "second_python": "3.14.6" + }, + "checks": [ + { + "command": "python3.12 -I -B scripts/research_package.py --package research/odd-dihedral-joint-tariff", + "result": "PASS_REGISTERED_RESEARCH_PACKAGE outcome=completed; optimized mathematical verifier, separate independent checker and all six package tests passed." + }, + { + "command": "python3 -I -O -B research/odd-dihedral-joint-tariff/verify.py", + "result": "PASS; same fixed receipt under CPython 3.14.6." + }, + { + "command": "python3 -I -B research/odd-dihedral-joint-tariff/independent_check.py", + "result": "PASS; 5200 single targets and 216 full matrix conjugations." + }, + { + "command": "make selected-record-check", + "result": "PASS; integrity only, not a cold replay." + }, + { + "command": "git diff --check", + "result": "PASS" + } + ], + "independent_review": { + "role": "math-exact-circuit-verification", + "verdict": "No blocking mathematical or code defect; final optimized verifier, separate checker and six tests passed in separate agent run.", + "reviewed_sha256": { + "PROOF.md": "bf56bbf426ca30030ad3868d0df9582b3077d21782460bddb3d2e6ae952b01a3", + "verify.py": "74c360fcacc08e7344afa2a4e1e7245a7f51439c0223afc3eaabf816d1cee7dc", + "independent_check.py": "ab76c1b9e29afe3e76198a44a98b80559afa1d819307d52b7f9d12c130899e77", + "test_package.py": "be667f4e5248211fbefdafe354b06bbbebbcaa88ed94fc96bc291d2ff5872b2c" + }, + "finding_resolved": "Crossing block orientation aligned to proof; joint-deficit control tests actual operator ranks.", + "nature": "Separate Codex specialist; AI-assisted, not human or formal-kernel review." + }, + "limits": [ + "No Lean proof or independent human review.", + "No selected-supplier cold/native replay, physical compiler/hosting/frame/precision/tape or recursive analytic transfer.", + "No new supplier, selected moment, multiplication runtime or kappa claim.", + "Hosted CI status is separate from local verification." + ], + "source_integrity": { + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "predecessor1941_head_readback": "5938ce3e91bbb8b5c2227af7976d444b2fbac7d4", + "predecessor1953_head_readback": "4f3bdf7c3bdd7033180c9d8c41245023cc402bc6" + } +} diff --git a/research/odd-dihedral-joint-tariff/VERIFY.json b/research/odd-dihedral-joint-tariff/VERIFY.json new file mode 100644 index 0000000000..5935c573c9 --- /dev/null +++ b/research/odd-dihedral-joint-tariff/VERIFY.json @@ -0,0 +1,43 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-three-register-lower-bound/README.md", + "research/coordinate-cnot-register-bound/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All finite operator/cut/call-count domains and fixed receipt; deliberate endpoint and invoice controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent_check.py" + ], + "timeout_seconds": 120, + "checks": "Separate specialist set-action and literal-word Pareto census for all odd periods 3..101; GL2 conjugations." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 120, + "checks": "Receipt and source corruption; actual detector-removal sensitivity; no-regeneration and optimized read-only relocation." + } + ] +} diff --git a/research/odd-dihedral-joint-tariff/independent_check.py b/research/odd-dihedral-joint-tariff/independent_check.py new file mode 100644 index 0000000000..72ee752716 --- /dev/null +++ b/research/odd-dihedral-joint-tariff/independent_check.py @@ -0,0 +1,119 @@ +#!/usr/bin/env python3 +"""Separate Codex exact-verification specialist check; Apache-2.0. + +No package imports. Original independent script SHA256: +5ebb07e7b470229874676ae57917b3c22ba8164da3bf0bc91e8621c99fedf206. +Parent added this header, optimized-mode refusal and expected receipt comparison. +Finite corroboration only; the universal proof is PROOF.md. +""" +if not __debug__: + raise RuntimeError("independent checker requires assertions; do not use -O") + +from collections import Counter +from itertools import product +import hashlib,json + +# Independent plain-set address action. No import of package functions. +# A word tuple gives displayed factors; evaluation acts rightmost first. +def action(word,a,e,n): + for letter in reversed(word): + a = (-a - (letter=='y')) % n + e = 1-e + return a,e + +def normal_action(k,s,a,e,n): + return (k + (-a if s else a)) % n, e^s + +def rank(rows): + work=list(rows); result=0 + while any(work): + p=max(work); bit=p.bit_length()-1 + work=[q^p if q>>bit&1 else q for q in work] + result+=1 + return result + +def times(A,B): + return tuple(_xor(B[j] for j in range(len(B)) if a>>j&1) for a in A) +def _xor(xs): + out=0 + for x in xs:out^=x + return out + +def eye(d): return tuple(1<>j&1) + for i in range(len(S)) for a in range(L)) +def gate(n,letter,u,v): + L=2*n; rows=list(eye(2*L)) + for out_role in range(2): + if not u>>out_role&1:continue + for a,e in product(range(n),range(2)): + b,f=action((letter,),a,e,n) + for in_role in range(2): + if v>>in_role&1: + rows[out_role*L+2*a+e]^=(1<<(in_role*L+2*a+e))^(1<<(in_role*L+2*b+f)) + return tuple(rows) +def cross(rows,H,L): + # Proof convention: outputs K, inputs H. + mask=sum(1<<(i*L+a) for i in range(2) for a in H) + return rank(rows[i*L+a]&mask for i in range(2) for a in range(L) if a not in H) +counts=Counter(); digest=hashlib.sha256() +for n in range(3,102,2): + m=n//2 + H={(a%n,0) for a in range(-m,1)}|{(b,1) for b in range(m)} + assert len(H)==n + # BFS generated directly from action on identity; records all count-Pareto points + # up to maximum shortest length n, independent of closed-form target words. + states={(0,0):{(0,0)}} + frontier={(0,0,0,0)} + for depth in range(n): + nxt=set() + for k,e,nx,ny in frontier: + for letter in ('x','y'): + h,f=action((letter,),k,e,n) + pair=(nx+(letter=='x'),ny+(letter=='y')) + old=states.get((h,f),set()) + if any(x<=pair[0] and y<=pair[1] for x,y in old):continue + old={p for p in old if not(pair[0]<=p[0] and pair[1]<=p[1])} + old.add(pair); states[h,f]=old + nxt.add((h,f,*pair)) + frontier=nxt + for k,e in product(range(n),range(2)): + distance=lambda z:min(z%n,n-z%n) + A=distance(k+e);B=distance(k);t=int(e==1 and k==m) + target={(normal_action(k,e,a,f,n)) for a,f in H} + q=len(target-H) + assert q==A+B+t + predicted={(A+j,B+t-j) for j in range(t+1)} + assert states[k,e]==predicted,(n,k,e,states[k,e],predicted) + for c,want in ((m,A),(m-1,B)): + I=set(range(m)); image={(k+(c-a if e else a))%n for a in I} + assert len(image-I)==want + digest.update(json.dumps((n,k,e,q,sorted(states[k,e]))).encode()) + counts['single_targets_odd_3_through_101']+=1 + counts['periods']+=1 +# Exhaust every two-role free invertible scalar map, every projector, and both letters. +GL=[(a,b) for a,b in product(range(4),repeat=2) if rank((a,b))==2] +projectors=[(u,v) for u,v in product(range(1,4),repeat=2) if (u&v).bit_count()%2] +for n in (3,5,7): + m=n//2;L=2*n;H={2*(a%n) for a in range(-m,1)}|{2*b+1 for b in range(m)} + for S in GL: + Sinv=next(T for T in GL if times(S,T)==eye(2)) + s,si=lift(S,L),lift(Sinv,L) + assert cross(s,H,L)==cross(si,H,L)==0 + for u,v in projectors: + # outer(u,v) gives N; conjugation independently as binary row matrices + N=tuple(v if u>>i&1 else 0 for i in range(2)) + C=times(times(S,N),Sinv) + up,vp=next((a,b) for a,b in projectors if tuple(b if a>>i&1 else 0 for i in range(2))==C) + for letter in ('x','y'): + original=gate(n,letter,u,v) + conj=times(times(s,original),si) + assert conj==gate(n,letter,up,vp) + assert cross(conj,H,L)==1 + counts['all_GL2_projector_conjugations']+=1 +result = {'counts':dict(counts),'sha256':digest.hexdigest(),'status':'PASS_INDEPENDENT_ODD_DIHEDRAL_REVIEW'} +expected = {'counts':{'all_GL2_projector_conjugations':216, 'periods':50, 'single_targets_odd_3_through_101':5200}, 'sha256':'52e3d7c91a93c51fe5e115ebfcdd7e2730308fafb83bc9a8e14739128d0b2724', 'status':'PASS_INDEPENDENT_ODD_DIHEDRAL_REVIEW'} +if result != expected: + raise ValueError('independent mathematical receipt mismatch') +print(json.dumps(result,sort_keys=True)) diff --git a/research/odd-dihedral-joint-tariff/test_package.py b/research/odd-dihedral-joint-tariff/test_package.py new file mode 100644 index 0000000000..87f05f692c --- /dev/null +++ b/research/odd-dihedral-joint-tariff/test_package.py @@ -0,0 +1,130 @@ +#!/usr/bin/env python3 +"""Fail-closed package and detector-sensitivity checks. Apache-2.0.""" +from copy import deepcopy +import importlib.util +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("odd_dihedral_verifier", HERE / "verify.py") +v = importlib.util.module_from_spec(spec) +spec.loader.exec_module(v) + + +class PackageChecks(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.actual = v.compute() + cls.expected = v.strict_json(HERE / "RECEIPT.json") + + def test_complete_receipt_and_semantic_controls(self): + self.assertEqual(v.canonical(self.actual), v.canonical(self.expected)) + self.assertIn("joint deficit n=3", self.actual["semantic_controls"]) + self.assertIn("dirty spectator leaks into target", self.actual["semantic_controls"]) + + def test_scientific_receipt_corruptions(self): + mutants = [] + d = deepcopy(self.expected); d["counts"]["complete_single_targets"] -= 1; mutants.append(d) + d = deepcopy(self.expected); d["counts"]["complete_short_words"] = True; mutants.append(d) + d = deepcopy(self.expected); d["domains"]["odd_periods_all_targets"].append(33); mutants.append(d) + d = deepcopy(self.expected); d["semantic_controls"].remove("joint deficit n=3"); mutants.append(d) + d = deepcopy(self.expected); d["mathematical_digest_sha256"] = "0" * 64; mutants.append(d) + d = deepcopy(self.expected); del d["counts"]["single_call_omissions"]; mutants.append(d) + for mutant in mutants: + with self.assertRaisesRegex(ValueError, "receipt differs"): + v.verify_receipt(self.actual, mutant) + + def test_detector_removal_is_observed(self): + source = (HERE / "verify.py").read_text() + controls = [ + (' require(nx + ny >= qjoint, "joint cut invoice")', ' pass # removed joint invoice'), + (' require(nx >= qx, "x cut invoice")', ' pass # removed x invoice'), + (' require(ny >= qy, "y cut invoice")', ' pass # removed y invoice'), + (' require(state == target_matrix(targets, roles), "formal endpoint mismatch")', + ' pass # removed full endpoint'), + ] + for old, new in controls: + self.assertEqual(source.count(old), 1) + namespace = {"__file__": str(HERE / "verify.py"), "__name__": "mutated_verifier"} + exec(compile(source.replace(old, new), "detector_removed.py", "exec"), namespace) + with self.assertRaisesRegex(ValueError, "negative control accepted"): + namespace["semantic_controls"]() + + def test_wrong_joint_formula_is_observed(self): + source = (HERE / "verify.py").read_text() + old = 'sum((k, e) == (m, 1) for k, e in pairs))' + self.assertEqual(source.count(old), 1) + namespace = {"__file__": str(HERE / "verify.py"), "__name__": "mutated_verifier"} + exec(compile(source.replace(old, '0)'), "joint_formula_removed.py", "exec"), namespace) + with self.assertRaisesRegex(ValueError, "joint cut / shortest distance"): + namespace["compute"]() + + def test_independent_checker_refuses_disabled_assertions(self): + result = subprocess.run([sys.executable, "-I", "-O", "-B", str(HERE / "independent_check.py")], + text=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE, timeout=30) + self.assertNotEqual(result.returncode, 0) + self.assertIn("independent checker requires assertions", result.stderr) + + def test_receipt_source_and_relocated_cli(self): + with tempfile.TemporaryDirectory(prefix="odd-dihedral-package-") as directory: + root = Path(directory) + package = root / "research" / HERE.name + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns("__pycache__")) + for item in v.strict_json(HERE / "SOURCES.json")["files"]: + if item["usage"] == "input": + dest = root / item["path"] + dest.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(HERE.parents[1] / item["path"], dest) + def run(*args): + return subprocess.run([sys.executable, "-I", "-O", "-B", str(package / "verify.py"), *args], + cwd=root, text=True, stdout=subprocess.PIPE, stderr=subprocess.PIPE, + timeout=60) + def failure(message): + result = run() + self.assertNotEqual(result.returncode, 0, result.stdout) + self.assertIn(message, result.stderr) + receipt = package / "RECEIPT.json" + original = receipt.read_bytes() + receipt.unlink() + failure("RECEIPT.json") + self.assertFalse(receipt.exists(), "missing evidence must not be regenerated") + receipt.write_text('{"x":0,"x":1}') + failure("duplicate JSON key") + receipt.write_text('{}') + failure("receipt differs from exact recomputation") + receipt.write_bytes(original) + item = next(x for x in v.strict_json(HERE / "SOURCES.json")["files"] if x["usage"] == "input") + source = root / item["path"] + saved = source.read_bytes() + source.write_bytes(saved + b"\nsource drift\n") + failure("source hash mismatch") + source.write_bytes(saved) + regenerated = run("--emit") + self.assertEqual(regenerated.returncode, 0, regenerated.stderr) + self.assertEqual(regenerated.stdout.encode(), original) + files = [p for p in root.rglob("*") if p.is_file()] + before = {str(p.relative_to(root)): p.read_bytes() for p in files} + for p in files: + p.chmod(0o444) + directories = [root] + [p for p in root.rglob("*") if p.is_dir()] + for p in directories: + p.chmod(0o555) + try: + passed = run() + self.assertEqual(passed.returncode, 0, passed.stderr) + self.assertIn("PASS_ODD_DIHEDRAL_JOINT_TARIFF", passed.stdout) + after = {str(p.relative_to(root)): p.read_bytes() for p in root.rglob("*") if p.is_file()} + self.assertEqual(before, after) + finally: + for p in directories: + p.chmod(0o755) + for p in files: + p.chmod(0o644) + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/odd-dihedral-joint-tariff/verify.py b/research/odd-dihedral-joint-tariff/verify.py new file mode 100644 index 0000000000..1bc244e674 --- /dev/null +++ b/research/odd-dihedral-joint-tariff/verify.py @@ -0,0 +1,516 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of PROOF.md; standard library, Apache-2.0. + +Prepared for Ross Richardson with substantial OpenAI Codex assistance. +No predecessor implementation is imported. Verification never generates evidence. +""" +from __future__ import annotations + +import argparse +from collections import Counter, deque +from fractions import Fraction +import hashlib +import itertools +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def reject(fn, message): + try: + fn() + except ValueError: + return + raise ValueError("negative control accepted: " + message) + + +def strict_json(path): + def pairs(items): + out = {} + for key, value in items: + require(key not in out, "duplicate JSON key: " + key) + out[key] = value + return out + return json.loads(path.read_text(), object_pairs_hook=pairs) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")) + + +def verify_receipt(actual, expected): + require(canonical(actual) == canonical(expected), "receipt differs from exact recomputation") + + +def mul(a, b, n): + k, e = divmod(a, 2) + l, f = divmod(b, 2) + return 2 * ((k + (-l if e else l)) % n) + (e ^ f) + + +def cmul(a, b, n): + out = 0 + while a: + low = a & -a + x = low.bit_length() - 1 + a ^= low + q = b + while q: + low = q & -q + y = low.bit_length() - 1 + q ^= low + out ^= 1 << mul(x, y, n) + return out + + +def identity(roles): + return tuple(1 if i == j else 0 for i in range(roles) for j in range(roles)) + + +def projectors(roles): + return [(u, v) for u in range(1, 1 << roles) + for v in range(1, 1 << roles) if (u & v).bit_count() % 2] + + +def validate_factor(factor, n, roles): + g, u, v = factor + require(g in (1, 2 * (n - 1) + 1), "illegal paid label") + require(type(u) is int and type(v) is int and 0 < u < 1 << roles + and 0 < v < 1 << roles and (u & v).bit_count() % 2 == 1, + "not a legal rank-one idempotent") + + +def append_factor(state, factor, n, roles): + """Right multiply the full formal matrix by I + ([g]+1) u v^T.""" + validate_factor(factor, n, roles) + g, u, v = factor + out = list(state) + for a in range(roles): + aggregate = 0 + for s in range(roles): + if u >> s & 1: + aggregate ^= state[a * roles + s] + delta = aggregate ^ cmul(aggregate, 1 << g, n) + for b in range(roles): + if v >> b & 1: + out[a * roles + b] ^= delta + return tuple(out) + + +def formal(word, n, roles): + state = identity(roles) + for f in word: + state = append_factor(state, f, n, roles) + return state + + +def target_matrix(targets, roles): + require(len(targets) <= roles, "too many targets") + t = tuple(targets) + (0,) * (roles - len(targets)) + return tuple(1 << t[i] if i == j else 0 + for i in range(roles) for j in range(roles)) + + +def endpoint(state, targets, roles): + require(state == target_matrix(targets, roles), "formal endpoint mismatch") + + +def distance(t, n): + t %= n + return min(t, n - t) + + +def budget(targets, n): + require(type(n) is int and n >= 3 and n % 2 == 1, "odd period >=3 required") + m = n // 2 + pairs = [divmod(g, 2) for g in targets] + require(all(0 <= k < n and e in (0, 1) for k, e in pairs), "invalid target") + return (sum(distance(k + e, n) for k, e in pairs), + sum(distance(k, n) for k, e in pairs), + sum((k, e) == (m, 1) for k, e in pairs)) + + +def tariff(targets, n, alpha, beta): + require(alpha >= 0 and beta >= 0, "negative price") + a, b, t = budget(targets, n) + return alpha * a + beta * b + t * min(alpha, beta) + + +def letters(g, n, extra_x=True): + """An attaining alternating word; group products are displayed left to right.""" + k, e = divmod(g, 2) + m = n // 2 + if k > m or (k == m and e and not extra_x): + k -= n + x, y = 1, 2 * (n - 1) + 1 + word = [x, y] * k if k >= 0 else [y, x] * (-k) + if e: + word.append(x) + reduced = [] + for h in word: + if reduced and reduced[-1] == h: + reduced.pop() + else: + reduced.append(h) + return reduced + + +def direct_word(targets, n, j=0): + """j of the exceptional roles receive the extra x; the rest an extra y.""" + _, _, t = budget(targets, n) + require(type(j) is int and 0 <= j <= t, "invalid exceptional split") + seen = 0 + word = [] + for role, g in enumerate(targets): + exceptional = g == n # index 2m+1 of (m,1) + extra_x = not exceptional or seen < j + seen += exceptional + word.extend((h, 1 << role, 1 << role) for h in letters(g, n, extra_x)) + return word + + +def compose(p, q): + return tuple(p[q[a]] for a in range(len(p))) + + +class RegularOracle: + """Independent group construction from literal permutations on n vertices. + + Matrices are binary rows; calls execute on all 2n group-basis addresses. + This uses neither mul/cmul nor append_factor to build the operator. + """ + def __init__(self, n): + self.n = n + one = tuple(range(n)) + x = tuple((-a) % n for a in range(n)) + y = tuple((-a - 1) % n for a in range(n)) + found = {one} + queue = deque([one]) + self.bfs_distance = {one: 0} + while queue: + p = queue.popleft() + for q in (x, y): + r = compose(q, p) + if r not in found: + found.add(r) + queue.append(r) + self.bfs_distance[r] = self.bfs_distance[p] + 1 + self.perms = sorted(found) + require(len(self.perms) == 2 * n, "wrong group order") + index = {p: i for i, p in enumerate(self.perms)} + self.normal = [index[tuple((k + (-a if e else a)) % n for a in range(n))] + for k in range(n) for e in range(2)] + self.actions = [[index[compose(p, q)] for q in self.perms] for p in self.perms] + + def matrix(self, word, roles): + width = 2 * self.n + rows = [1 << i for i in range(width * roles)] + for label, u, v in reversed(word): + action = self.actions[self.normal[label]] + old = rows[:] + for address in range(width): + delta = 0 + for role in range(roles): + if v >> role & 1: + delta ^= old[role * width + address] ^ old[role * width + action[address]] + for role in range(roles): + if u >> role & 1: + rows[role * width + address] ^= delta + return rows + + def from_formal(self, state, roles): + width = 2 * self.n + rows = [0] * (width * roles) + for i in range(roles): + for j in range(roles): + coeffs = state[i * roles + j] + for normal in range(width): + if coeffs >> normal & 1: + for source, dest in enumerate(self.actions[self.normal[normal]]): + rows[i * width + dest] ^= 1 << (j * width + source) + return rows + + +def rank(rows): + pivots = {} + for x in rows: + while x: + p = x.bit_length() - 1 + if p in pivots: + x ^= pivots[p] + else: + pivots[p] = x + break + return len(pivots) + + +def crossing(rows, half, width, roles): + """Rank of the output-K/input-H block, matching PROOF.md.""" + k = [i * width + a for i in range(roles) for a in range(width) if a not in half] + mask = sum(1 << (i * width + a) for i in range(roles) for a in half) + return rank([rows[i] & mask for i in k]) + + +def regular_half(oracle): + n = oracle.n + m = n // 2 + return {oracle.normal[2 * (a % n)] for a in range(-m, 1)} | { + oracle.normal[2 * b + 1] for b in range(m)} + + +def small_action(g, n, c): + k, e = divmod(g, 2) + return tuple((k + (c - a if e else a)) % n for a in range(n)) + + +def represented(state, n, roles, c): + rows = [0] * (n * roles) + for i in range(roles): + for j in range(roles): + for g in range(2 * n): + if state[i * roles + j] >> g & 1: + for a, b in enumerate(small_action(g, n, c)): + rows[i * n + b] ^= 1 << (j * n + a) + return rows + + +def count_bound(targets, n, roles, nx, ny): + """Reject bills below actual operator cut ranks, not a substituted formula. + + Passing this necessary-condition test is not endpoint/circuit certification. + """ + require(type(nx) is int and type(ny) is int and nx >= 0 and ny >= 0, "invalid bill") + budget(targets, n) + state = target_matrix(targets, roles) + m = n // 2 + qx = crossing(represented(state, n, roles, m), set(range(m)), n, roles) + qy = crossing(represented(state, n, roles, m-1), set(range(m)), n, roles) + oracle = RegularOracle(n) + qjoint = crossing(oracle.from_formal(state, roles), regular_half(oracle), 2*n, roles) + require(nx >= qx, "x cut invoice") + require(ny >= qy, "y cut invoice") + require(nx + ny >= qjoint, "joint cut invoice") + return qx, qy, qjoint + + +def verify_sources(): + source = strict_json(HERE / "SOURCES.json") + root = HERE.parents[1] + for item in source["files"]: + if item["usage"] == "input": + require(hashlib.sha256((root / item["path"]).read_bytes()).hexdigest() + == item["sha256"], "source hash mismatch: " + item["path"]) + + +def compute(): + counts = Counter() + digest = hashlib.sha256() + for n in range(3, 32, 2): + oracle = RegularOracle(n) + half = regular_half(oracle) + require(len(half) == n, "regular half size") + m = n // 2 + for g in range(2 * n): + a, b, t = budget([g], n) + rows = oracle.from_formal((1 << g,), 1) + q = crossing(rows, half, 2 * n, 1) + shortest = oracle.bfs_distance[oracle.perms[oracle.normal[g]]] + require(q == shortest == a + b + t, "joint cut / shortest distance") + require(crossing(represented((1 << g,), n, 1, m), set(range(m)), n, 1) == a, + "x cut formula") + require(crossing(represented((1 << g,), n, 1, m - 1), set(range(m)), n, 1) == b, + "y cut formula") + for j in range(t + 1): + word = direct_word([g], n, j) + endpoint(formal(word, n, 1), [g], 1) + require(oracle.matrix(word, 1) == rows, "single formal/regular disagreement") + counts["single_attaining_words"] += 1 + digest.update(canonical([n, g, a, b, t, q]).encode()) + counts["complete_single_targets"] += 1 + if n <= 15: + for g, h in itertools.product(range(2 * n), repeat=2): + product = mul(g, h, n) + require(oracle.normal[product] == oracle.actions[oracle.normal[g]][oracle.normal[h]], + "independent group multiplication") + for c in (m, m - 1): + require(small_action(product, n, c) == compose(small_action(g, n, c), + small_action(h, n, c)), "representation law") + counts["complete_group_pairs"] += 1 + if n <= 11: + for roles in range(1, 5): + ps = projectors(roles) + require(len(ps) == (1 << (roles - 1)) * ((1 << roles) - 1), "projector count") + for u, v in ps: + for letter, label in enumerate((1, 2 * (n - 1) + 1)): + state = formal([(label, u, v)], n, roles) + rows = oracle.matrix([(label, u, v)], roles) + require(rows == oracle.from_formal(state, roles), "factor oracle") + cuts = (crossing(represented(state, n, roles, m), set(range(m)), n, roles), + crossing(represented(state, n, roles, m - 1), set(range(m)), n, roles), + crossing(rows, half, 2 * n, roles)) + require(cuts == ((1, 0, 1) if letter == 0 else (0, 1, 1)), "rank-one cut charges") + counts["all_projector_factor_checks"] += 1 + counts["factor_regular_basis_columns"] += 2 * n * roles + for n in (3, 5): + oracle = RegularOracle(n) + half = regular_half(oracle) + alphabet = [(g, u, v) for g in (1, 2 * (n - 1) + 1) for u, v in projectors(2)] + for length in range(4): + for word in itertools.product(alphabet, repeat=length): + state = formal(word, n, 2) + rows = oracle.matrix(word, 2) + require(rows == oracle.from_formal(state, 2), "mixed full operator disagreement") + nx = sum(g == 1 for g, _, _ in word) + qx = crossing(represented(state, n, 2, n // 2), set(range(n // 2)), n, 2) + qy = crossing(represented(state, n, 2, n // 2 - 1), set(range(n // 2)), n, 2) + qr = crossing(rows, half, 2 * n, 2) + require(qx <= nx and qy <= length - nx and qr <= length, "mixed cut subadditivity") + counts["complete_short_words"] += 1 + counts["short_word_regular_basis_columns"] += 4 * n + digest.update(canonical([n, list(word), state]).encode()) + prices = (Fraction(0), Fraction(1, 3), Fraction(1), Fraction(2), Fraction(7)) + for n in (3, 5, 7): + oracle = RegularOracle(n) + for targets in itertools.product(range(2 * n), repeat=2): + a, b, t = budget(targets, n) + costs = [] + for j in range(t + 1): + word = direct_word(targets, n, j) + state = formal(word, n, 3) + endpoint(state, targets, 3) + regular = oracle.matrix(word, 3) + require(regular == oracle.from_formal(target_matrix(targets, 3), 3), "dirty regular boundary") + nx = sum(g == 1 for g, _, _ in word) + require((nx, len(word) - nx) == (a + j, b + t - j), "joint count split") + costs.append((nx, len(word) - nx)) + inverse_targets = [2*(-(g//2) % n) if g % 2 == 0 else g for g in targets] + inverse = formal(list(reversed(word)), n, 3) + endpoint(inverse, inverse_targets, 3) + require(oracle.matrix(list(reversed(word)), 3) == oracle.from_formal(inverse, 3), + "inverse regular boundary") + counts["pair_inverse_words"] += 1 + for cut in range(len(word)): + reject(lambda cut=cut: endpoint(formal(word[:cut] + word[cut+1:], n, 3), targets, 3), + "single-call omission") + counts["single_call_omissions"] += 1 + counts["complete_pair_attaining_words"] += 1 + counts["pair_regular_basis_columns"] += 6 * n + digest.update(canonical([n, targets, j, state]).encode()) + for alpha, beta in itertools.product(prices, repeat=2): + require(min(alpha*x + beta*y for x, y in costs) == tariff(targets, n, alpha, beta), + "nonnegative rational tariff") + counts["rational_price_checks"] += 1 + # Beyond pair endpoints: every exceptional split, with varied ordinary targets + # and one arbitrary spectator, for t=0..5 (up to eight scalar roles). + for n in (3, 5, 9, 15): + oracle = RegularOracle(n) + for t in range(6): + targets = [n] * t + [1, 2*n-2] + roles = len(targets) + 1 + a, b, actual_t = budget(targets, n) + require(actual_t == t, "larger tuple setup") + for j in range(t+1): + word = direct_word(targets, n, j) + state = formal(word, n, roles) + endpoint(state, targets, roles) + require(oracle.matrix(word, roles) == oracle.from_formal(state, roles), "larger tuple regular boundary") + require(count_bound(targets, n, roles, a+j, b+t-j) == (a,b,a+b+t), "joint operator bill") + counts["larger_mixed_tuple_words"] += 1 + counts["larger_tuple_regular_basis_columns"] += roles * 2*n + # All scalar invertible maps through three roles have zero crossing rank, + # and conjugation permutes the full rank-one-idempotent alphabet. + for roles in range(1,4): + ps = projectors(roles) + for scalar in itertools.product(range(1 << roles), repeat=roles): + if rank(scalar) != roles: + continue + images = [sum(((row & v).bit_count() % 2) << i for i, row in enumerate(scalar)) + for v in range(1 << roles)] + inverse = {image: v for v, image in enumerate(images)} + for u, v in ps: + covector = sum(((v & inverse[1 << i]).bit_count() % 2) << i for i in range(roles)) + require((images[u], covector) in ps, "scalar conjugation closure") + counts["scalar_projector_conjugations"] += 1 + for n in (3,5): + rows = [sum(1 << (j*2*n+a) for j in range(roles) if scalar[i] >> j & 1) + for i in range(roles) for a in range(2*n)] + oracle = RegularOracle(n) + require(crossing(rows, regular_half(oracle), 2*n, roles) == 0, "free scalar charge") + counts["free_scalar_cut_checks"] += 1 + controls = semantic_controls() + return {"schema_version": 1, "scope": "finite corroboration; universal theorem is PROOF.md; no_new_kappa", + "domains": {"odd_periods_all_targets": list(range(3, 32, 2)), + "all_group_pairs_periods": list(range(3, 16, 2)), + "all_projectors_roles": [1, 2, 3, 4], "all_projectors_periods": [3, 5, 7, 9, 11], + "complete_short_words": {"periods": [3, 5], "roles": 2, "lengths": [0, 1, 2, 3]}, + "all_ordered_target_pairs": {"periods": [3, 5, 7], "roles": 3}, + "larger_mixed_tuples": {"periods": [3,5,9,15], "exceptional_counts": list(range(6)), + "ordinary_targets": ["x", "r^-1"], "dirty_spectators": 1}, + "all_scalar_GL_roles": [1,2,3]}, + "counts": dict(sorted(counts.items())), "semantic_controls": controls, + "mathematical_digest_sha256": digest.hexdigest()} + + +def semantic_controls(): + names = [] + def bad(name, fn): + reject(fn, name) + names.append(name) + bad("even-period misuse", lambda: budget([0], 4)) + bad("negative tariff", lambda: tariff([1], 3, Fraction(-1), Fraction(1))) + bad("illegal rotation label", lambda: formal([(2, 1, 1)], 3, 2)) + bad("non-idempotent scalar factor", lambda: formal([(1, 1, 2)], 3, 2)) + bad("foreign scalar role", lambda: formal([(1, 4, 4)], 3, 2)) + for n in (3, 5): + a, b, t = budget([n, n], n) + require((a+b) % 2 == 0 and t == 2, "joint-gap fixture setup") + bad(f"joint deficit n={n}", lambda n=n, a=a, b=b: count_bound([n,n], n, 3, a, b)) + bad(f"wrong noncommuting order n={n}", lambda n=n: endpoint(formal([(1,1,1),(2*n-1,1,1)], n, 1), [2*n-2], 1)) + require(len(direct_word([n], n, 0)) == n, "longest reflection length") + n, roles = 5, 3 + bad("x bill hidden by large y bill", lambda: count_bound([1], 5, 2, 0, 100)) + bad("y bill hidden by large x bill", lambda: count_bound([9], 5, 2, 100, 0)) + word = direct_word([n, 2], n, 1) + baseline = formal(word, n, roles) + dirty = list(baseline) + dirty[2] ^= 1 + require(dirty[0] == baseline[0] and dirty[1] == baseline[1], "clean control setup") + bad("dirty spectator leaks into target", lambda: endpoint(tuple(dirty), [n,2], roles)) + dirty = list(baseline) + dirty[8] = 1 << 1 + bad("spectator not restored", lambda: endpoint(tuple(dirty), [n,2], roles)) + hidden = list(identity(2)); hidden[1] = (1 << (2*n)) - 1 + for c in (n//2, n//2-1): + require(represented(tuple(hidden), n, 2, c) == represented(identity(2), n, 2, c), "common kernel setup") + bad("proof-representation false endpoint", lambda: endpoint(tuple(hidden), [], 2)) + oracle = RegularOracle(n) + require(oracle.from_formal(tuple(hidden), 2) != oracle.from_formal(identity(2), 2), "faithful kernel detector") + extra = [(1, 3, 1), (1, 3, 1)] + require(formal(extra, n, 2) == identity(2), "equivalent cancelling presentation") + require(oracle.matrix(extra, 2) == oracle.from_formal(identity(2), 2), "oracle equivalent presentation") + names.append("positive noncoordinate cancelling presentation") + return names + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", help="print recomputation without writing evidence") + args = parser.parse_args() + verify_sources() + actual = compute() + if args.emit: + print(json.dumps(actual, indent=2, sort_keys=True)) + return + expected = strict_json(HERE / "RECEIPT.json") + verify_receipt(actual, expected) + print("PASS_ODD_DIHEDRAL_JOINT_TARIFF " + canonical(actual["counts"]) + " no_new_kappa") + + +if __name__ == "__main__": + main()