diff --git a/research/mixed-sign-phase-spectrum/PROOF.md b/research/mixed-sign-phase-spectrum/PROOF.md new file mode 100644 index 0000000000..52457e2cdf --- /dev/null +++ b/research/mixed-sign-phase-spectrum/PROOF.md @@ -0,0 +1,165 @@ +# Mixed-sign orthogonal phase spectrum + +This contribution was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +## Contract and theorem + +Let V=F2^n for n>=1 with its ordinary dot product. All vector sums and matrix +operations below are binary unless a congruence or integer weight is written. +Fix a sign mask b in V and put + + q_b(x) = wt(x) + 2 b·x modulo 4. + +The dot product b·x in this formula is either 0 or 1. Its polarization is + + q_b(x+y) = q_b(x)+q_b(y)-2 x·y modulo 4. + +For S in O(n,2), define the row-convention phase defect d_b(S) by + + q_b(S^T x)-q_b(x) = 2 d_b(S)·x modulo 4. (1) + +The difference has zero polarization, hence is additive; its values are even +because S preserves x·x. Thus there is a unique binary d_b(S). + +**Theorem.** The exact attainable set is + + D_b = {e : q_b(e)=0} + = {e : wt(b+e) == wt(b) modulo 4}. (2) + +For every e in D_b, the symmetric orthogonal involution + + T_e = I + e e^T + +has d_b(T_e)=e. Every S has a unique factorization + + S = T_e H, e=d_b(S), d_b(H)=0. (3) + +Each fiber has size |O(n,2)|/N_(n,r), where + + r = wt(b) modulo 4, + N_(n,r) = sum_{0<=k<=n, k==r modulo 4} binomial(n,k). + +These are exact algebraic counts and a written scoped proof. They do not +price a physical chart change or establish supplier admission. + +The equal-sign case b=0, its transvection representative and orthogonal-group +order are Philipp / mightyOil's PR1300. Gareth Davidson's PR1255 supplies the +residual gate and row-defect conventions. The present addition is arbitrary +fixed mixed signs, their changed image and stabilizer, and the corresponding +literal signed-kernel contract. Classical quadratic-refinement and Gauss-sum +methods are not claimed as new mathematics independent of this application. + +## Necessity from an exact Gaussian sum + +The sum over all x of i^(q_b(x)) factors coordinatewise as + + G_b = (1+i)^(n-wt(b)) (1-i)^wt(b) + = (1+i)^n (-i)^wt(b). + +It is nonzero. Since S^T permutes V, equation (1) gives G_b=G_(b+e), for +e=d_b(S). Dividing their displayed nonzero expressions shows + + wt(b+e) == wt(b) modulo 4. + +No floating-point phase comparison or assumption on the weight of e alone +is involved. Writing h for the integer number of common 1-bits of b and e, + + wt(b+e)-wt(b) = wt(e)-2h == q_b(e) modulo 4, + +because 2h modulo 4 equals twice the binary dot product. This proves the +equality of the two descriptions in (2). In particular every admissible e +has even weight. + +## A representative for each admissible defect + +For even-weight e, e·e=0. Direct multiplication shows + + T_e^T=T_e, T_e^2=I, T_e^T T_e=I. + +Set a=e·x in {0,1}. Polarization gives + + q_b(T_e x)-q_b(x) = a (q_b(e)-2) modulo 4. + +If e is admissible, q_b(e)=0, so this difference is 2e·x. Equation (1) +therefore gives d_b(T_e)=e. This includes e=0 with T_0=I and proves +sufficiency for every n and every sign pattern. A nonzero admissible defect +is corrected by one algebraic rank-one transvection, and cannot be corrected +by zero such transvections. This counts algebraic factors only. + +The transported sign term can also be read directly from PR1300's defect: + + d_b(S) = d_0(S) + b + S b. (4) + +For even e it yields + + d_b(T_e) = (wt(e)/2 + 1 + b·e) e, + +where the coefficient is reduced modulo two. Dropping b+Sb incorrectly +reuses the equal-sign criterion. + +## Cocycle, normalization and exact fibers + +Apply (1) first to B^T A^T x, then to A^T x. The result is the twisted cocycle + + d_b(AB) = d_b(A) + A d_b(B). + +Let e=d_b(S). Since T_e e=e, the cocycle gives + + d_b(T_e S) = e + T_e e = 0. + +Thus H=T_e S proves (3). The e in (3) is prescribed by S, so H is unique. +The zero-defect maps form a subgroup. Conversely every such H satisfies + + d_b(T_e H)=e. + +Multiplication by T_e is therefore a bijection from this subgroup to the +e fiber. All fibers have equal size. Translation e -> b+e identifies the +image with all binary vectors of weight congruent to wt(b) modulo four, +which gives N_(n,r) and the claimed stabilizer count. + +For concrete counts use PR1300's credited recurrence + + O_1=1, O_n=(2^(n-1)-[n odd]) O_(n-1) for n>=2. + +At n=6 with one negative axis, N_(6,1)=binomial(6,1)+binomial(6,5)=12. +There are 23040/12=1920 exact preservers. The equal-sign case instead has +N_(6,0)=16 and 1440 preservers. These are counts of bases, not a cost saving. + +## Literal signed residual + +For orthonormal independent active directions u_1,...,u_n, take the product +of the commuting gates + + C_u^(s) = ((1+s i) I + (1-s i) X_u)/2, + X_u f(x)=f(x+u), s_j=(-1)^b_j. + +Independence makes every displacement Ux have one subset expansion. Hence +its exact convolution coefficient is + + K_(U,b)(Ux) = c_b (-i)^q_b(x), + c_b = ((1+i)/2)^n (-i)^wt(b). + +For V=US with S orthogonal, coordinates of Ux in V are S^T x. Equation (1) +then gives + + K_(US,b)(Ux) = (-1)^(d_b(S)·x) K_(U,b)(Ux). + +The fixed sign mask indexes the chart's columns on both sides. Permuting +signs with the axes is a different comparison. The all-nonzero coefficient +formula proves exact equality iff d_b(S)=0. The convolution commutes because +binary translations commute, without a native implementation assumption. + +At n=5, let b=e_1 and e=e_1+e_2. Then q_b(e)=0 and d_b(T_e)=e, although e +has weight two. The same transvection has d_0(T_e)=0. Thus the mixed-sign +boundary differs even for a coordinate swap. Conversely e=e_1+e_2+e_3+e_4 +has weight four but d_b(T_e)=0, so it is not its own mixed-sign defect. + +## Remaining obligations + +This proof treats an orthonormal active chart and fixed signed C gates. +It neither generalizes to every nonorthogonal chart nor prices native maps, +physical routes, source acquisition, dirty restoration, precision, stock, +fixed tapes or a complete recursive consumer. No selected-frontier change, +new kappa or complete multiplication theorem follows. The finite verifier +corroborates (1)-(4); the written argument supplies their universal quantifiers. diff --git a/research/mixed-sign-phase-spectrum/README.md b/research/mixed-sign-phase-spectrum/README.md new file mode 100644 index 0000000000..19a7b6b1c6 --- /dev/null +++ b/research/mixed-sign-phase-spectrum/README.md @@ -0,0 +1,105 @@ +# Exact phase defects for mixed-sign orthogonal charts + +For every binary sign mask b and every width n>=1, the attainable defects of +orthogonal chart changes are exactly + + D_b = {e : wt(b+e) == wt(b) modulo 4}. + +Each defect e has the explicit representative T_e=I+ee^T and the same number +of realizations. The exact-preserver subgroup has order + + |O(n,2)| / sum_{k==wt(b) modulo 4} binomial(n,k). + +This is a scoped written algebraic proof with exact finite corroboration. +See [PROOF.md](PROOF.md) for the full gate contract and argument. No new +kappa, physical supplier or selected-frontier change is claimed. + +The addition to Philipp / mightyOil's [PR1300](https://github.com/CrocSwap/integer-mult-bounds/pull/1300) +is an arbitrary fixed mixture of positive and negative residual gates. At +width five with one negative axis, a weight-two defect is attainable although +the equal-sign spectrum excludes it. At width six with one negative axis, +there are 12 defects and 1920 exact preservers, versus the credited equal-sign +values 16 and 1440. These exact counts are corroborated by the verifier's +explicit sign/defect enumeration and the inherited group-order recurrence. + +This changes the `bit-helper-contract` card to a phase-boundary side result. +It specifies the algebraic admission criterion for mixed signs before anyone +prices an actual changed chart. It does not claim a cheaper complete caller. +The first source discriminator is the width-five one-negative-axis fixture. +The selected metadata positive control was run separately; no predecessor +scientific suite was replayed as this contribution. + +## Reproduction + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/mixed-sign-phase-spectrum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/mixed-sign-phase-spectrum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/mixed-sign-phase-spectrum +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/mixed-sign-phase-spectrum --check-source-history +``` + +Substitute another CPython 3.12 path elsewhere. The verifier prints +`PASS_MIXED_SIGN_PHASE_SPECTRUM` inside a JSON receipt whose hashes bind every +package file. It reads no predecessor executable and writes no files. +`SOURCES.json` preserves predecessor proofs as historical provenance. + +The bounded replay enumerates every orthogonal matrix through width five, +every sign mask at those widths and every kernel coefficient. It also checks +the matrix census by independent full binary-matrix enumeration through width +four; constructs every admissible sign/defect pair through width nine; tests +every width-four twisted-cocycle pair for every sign mask; and includes ten +semantic controls. The generated receipt reports 777 orthogonal matrices, +23,866 matrix/sign pairs, 749,988 literal coefficients, 66,066 full binary +matrices, 349,524 sign/defect candidates, 87,892 attaining representatives +and 36,864 cocycle pairs. These are finite checks of the new mixed-sign +statement, not a predecessor audit. + +## Scope and provenance + +The scientific base is canonical main `ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c`, +priority revision 7. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19146049) +preceded implementation. The initial cache covered 340 open PRs and 4440 +Discussion records with complete remote pagination. The sparse local search +was incomplete; targeted `git grep origin/main` and merged-PR searches covered +the distinctive phase object separately. Search coverage is not novelty proof. + +Independent human and formal proof-kernel review are unclaimed. The all-width +claim rests on the written proof, not extrapolation from the finite checks. +Physical route/frame costs, native realization, source acquisition, restoration, +compiler, precision/tape, stock, complete supplier admission and the full +multiplication theorem remain outside scope. No Lean, Docker or selected +supplier cold replay was run. + +The verifier uses bounded Python allocation, a managed-runtime deviation from +Power of Ten's fixed-allocation rule. Widths are fixed at 1..5 for group/kernel +checks, 1..4 for the full-matrix cross-check, and 1..9 for representatives. The +prefix list is capped at 32768 entries, each matrix has at most nine columns, +and convolution arrays have at most 32 entries. There is no recursion, child +process, network access, dynamic code or external dependency. Explicit errors +preserve all checks under `-O`. Every function has fewer than 60 lines. Warning +strict normal/optimized replay is the available diagnostic check. A larger +registered domain must first update these bounds and its measured runtime. + +## Open next questions + +1. Can a named mixed-sign native helper use the larger exact-preserver subgroup + to reduce its complete physical bill? First bind its literal sign mask and + compare an explicit phase-preserving chart with all transport/restoration + costs. No priced caller is supplied here. +2. Which defects remain when the permitted orthogonal chart changes must fix + a specified set of literal axes? First derive the restricted orbit of q_b + on that stabilizer before proposing a synthesis search. The unrestricted + representative T_e need not fix those axes. + +## Credit + +This contribution was produced by Nick Petalas. Apache-2.0. +Philipp / mightyOil's PR1300 supplies the equal-sign defect spectrum, canonical +transvection and orthogonal-group order. Gareth Davidson's PR1255 supplies the +C-gate phase contract and row convention. yssite's PR1558 supplies the signed +Gauss-normalization context, following icekylinx's PR24. Credit Rohan Arun, +Jeremy Kothe, Hao Yan, Josie Elliston, Douglas Colkitt and the retained +Clifford/normalization lineage. Classical quadratic-refinement and Gauss-sum +facts retain their classical status. All predecessor notices stay unchanged. diff --git a/research/mixed-sign-phase-spectrum/SOURCES.json b/research/mixed-sign-phase-spectrum/SOURCES.json new file mode 100644 index 0000000000..ae33433565 --- /dev/null +++ b/research/mixed-sign-phase-spectrum/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/orthogonal-phase-defect-spectrum/README.md", + "usage": "provenance", + "git_blob": "8912dff64204efb160df1cda12e61b4eba666372", + "sha256": "1728301372b1027edeb28b4a88b8c47087d0f5af0b83ca692bed4c732635f532" + }, + { + "path": "research/selected1094-chart-phase/PROOF.md", + "usage": "provenance", + "git_blob": "6ba3890c6c9d919d096965a21d10141ee7cf05b2", + "sha256": "1c9010e7c716a9df0264da4749d727c690138509f3335340fb369785cca5e55a" + }, + { + "path": "research/signed-gauss-census/README.md", + "usage": "provenance", + "git_blob": "4d829cb5379ac1ef83c8afaa8c3bc4c7634df55f", + "sha256": "3cbf12962eb974302e1dd02232ca52350cf5c9115c0bc135b8c2684e07709913" + } + ] +} diff --git a/research/mixed-sign-phase-spectrum/TASK.json b/research/mixed-sign-phase-spectrum/TASK.json new file mode 100644 index 0000000000..0729752a87 --- /dev/null +++ b/research/mixed-sign-phase-spectrum/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 7, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "original_card": { + "id": "bit-helper-contract", + "question": "Can one precisely specified helper-mixing word satisfy a replacement for the inherited H2/K interface?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/r439-bsection-stars-seed01/README.md", + "research/r439-copy-path-sharing-barrier/README.md" + ], + "methods": [ + "Derive a replacement interface lemma and price its implementation.", + "Seek an exact dirty-input or chronological-cut counterexample to the proposed replacement." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. 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", + "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_status": "changed", + "actual_scope": "Classify every mixed-sign orthogonal binary chart phase defect, construct one-transvection representatives, and derive exact equal-fiber and stabilizer counts at every width.", + "scope_change_reason": "Extend Philipp / mightyOil PR1300 from equal signs to an arbitrary fixed signed C-gate pattern. This is an original phase-boundary side result, not an audit or a replacement H2/K implementation.", + "bottleneck_link": "Side result: gives the exact algebraic phase admission criterion for mixed-sign residual charts. No physical rebase or recursive saving follows without a priced actual caller.", + "budget_minutes": 60, + "stop_rule": "Stop at the first written scoped theorem with literal exact finite corroboration; package it without extending the construction family.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py exact Gaussian-integer convolution, full small matrix/sign census, constructive representatives, cocycle and ten semantic controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a named mixed-sign native helper use an exact-preserving chart with lower complete physical cost?", + "why_it_matters": "Algebraic phase freedom changes no recursive invoice until native and physical costs are charged.", + "first_step": "Bind the literal sign mask and price one explicit preserving chart including transport and restoration.", + "blocked_by": "No fully priced actual caller or native chart implementation is supplied." + }, + { + "question": "Which defects remain when allowed chart changes must fix specified literal axes?", + "why_it_matters": "Physical route contracts can forbid the unrestricted representative.", + "first_step": "Derive the orbit of q_b under the axis stabilizer before synthesis.", + "blocked_by": "The unrestricted T_e need not fix the required axes." + } + ], + "claim_type": "scoped-proof", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19146049", + "overlap_checked_utc": "2026-10-23T12:54:11Z" +} diff --git a/research/mixed-sign-phase-spectrum/VERIFY.json b/research/mixed-sign-phase-spectrum/VERIFY.json new file mode 100644 index 0000000000..e8b6dabbda --- /dev/null +++ b/research/mixed-sign-phase-spectrum/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": 180, + "checks": "Exact mixed-sign phase identity, literal signed C-gate convolution, complete small sign/matrix census and all candidate representatives through width nine." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Repeat the same exact checks with optimized Python; all invariants use explicit exceptions." + } + ] +} diff --git a/research/mixed-sign-phase-spectrum/verify.py b/research/mixed-sign-phase-spectrum/verify.py new file mode 100644 index 0000000000..4697a3b42c --- /dev/null +++ b/research/mixed-sign-phase-spectrum/verify.py @@ -0,0 +1,206 @@ +#!/usr/bin/env python3 +"""Exact mixed-sign phase checks. Standard library; no predecessor imports.""" +from collections import Counter +from hashlib import sha256 +from itertools import product +from math import comb +from pathlib import Path +import json + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def dot(x: int, y: int) -> int: + return (x & y).bit_count() & 1 + + +def apply(columns: tuple[int, ...], x: int) -> int: + value = 0 + for j, column in enumerate(columns): + if (x >> j) & 1: + value ^= column + return value + + +def transpose(columns: tuple[int, ...]) -> tuple[int, ...]: + n = len(columns) + return tuple(sum(((c >> i) & 1) << j for j, c in enumerate(columns)) + for i in range(n)) + + +def compose(a: tuple[int, ...], b: tuple[int, ...]) -> tuple[int, ...]: + return tuple(apply(a, column) for column in b) + + +def identity(n: int) -> tuple[int, ...]: + return tuple(1 << j for j in range(n)) + + +def orthogonal(columns: tuple[int, ...]) -> bool: + return all(dot(x, y) == int(i == j) + for i, x in enumerate(columns) for j, y in enumerate(columns)) + + +def q(b: int, x: int) -> int: + return (x.bit_count() + 2 * dot(b, x)) % 4 + + +def defect(columns: tuple[int, ...], b: int) -> int: + differences = tuple((q(b, row) - q(b, 1 << j)) % 4 + for j, row in enumerate(transpose(columns))) + require(all(d % 2 == 0 for d in differences), "nonbinary phase defect") + return sum((d // 2) << j for j, d in enumerate(differences)) + + +def representative(n: int, e: int) -> tuple[int, ...]: + return tuple((1 << j) ^ (e if (e >> j) & 1 else 0) for j in range(n)) + + +def admissible(b: int, e: int) -> bool: + return ((b ^ e).bit_count() - b.bit_count()) % 4 == 0 + + +def group_order(n: int) -> int: + value = 1 + for width in range(2, n + 1): + value *= (1 << (width - 1)) - (width & 1) + return value + + +def orbit_size(n: int, b: int) -> int: + return sum(comb(n, k) for k in range(b.bit_count() % 4, n + 1, 4)) + + +def enumerate_group(n: int) -> list[tuple[int, ...]]: + require(1 <= n <= 5, "enumeration width must lie in 1..5") + odd = tuple(x for x in range(1 << n) if x.bit_count() % 2) + partial = [()] + for _ in range(n): + partial = [prefix + (x,) for prefix in partial for x in odd + if all(dot(x, y) == 0 for y in prefix)] + require(len(partial) <= 32768, "orthogonal-prefix capacity exceeded") + require(len(set(partial)) == len(partial), "duplicate matrix") + return partial + + +def mul(z: tuple[int, int], w: tuple[int, int]) -> tuple[int, int]: + return z[0] * w[0] - z[1] * w[1], z[0] * w[1] + z[1] * w[0] + + +def literal_kernel(columns: tuple[int, ...], b: int) -> tuple[tuple[int, int], ...]: + """Convolve ((1+s*i)I+(1-s*i)X_u), with denominator 2^n.""" + values = [(1, 0)] + [(0, 0)] * ((1 << len(columns)) - 1) + for j, direction in enumerate(columns): + sign = -1 if (b >> j) & 1 else 1 + following = [] + for x in range(len(values)): + a = mul(values[x], (1, sign)) + c = mul(values[x ^ direction], (1, -sign)) + following.append((a[0] + c[0], a[1] + c[1])) + values = following + return tuple(values) + + +def enumerate_checks() -> dict[str, int]: + counts = Counter() + for n in range(1, 6): + matrices = enumerate_group(n) + require(len(matrices) == group_order(n), "group cardinality") + counts["orthogonal_matrices"] += len(matrices) + for b in range(1 << n): + histogram = Counter() + original = literal_kernel(identity(n), b) + for s in matrices: + require(orthogonal(s), "enumerator returned nonorthogonal map") + e = defect(s, b) + require(admissible(b, e), "mixed-sign spectrum necessity") + require(defect(compose(representative(n, e), s), b) == 0, + "canonical phase normalization") + st = transpose(s) + actual = literal_kernel(s, b) + for x in range(1 << n): + require(q(b, apply(st, x)) == (q(b, x) + 2 * dot(e, x)) % 4, + "quadratic phase identity") + sign = -1 if dot(e, x) else 1 + require(actual[x] == tuple(sign * v for v in original[x]), + "literal signed-gate coefficient") + counts["literal_coefficients"] += 1 + histogram[e] += 1 + counts["matrix_sign_pairs"] += 1 + expected = {e for e in range(1 << n) if admissible(b, e)} + require(set(histogram) == expected, "complete mixed-sign image") + require(len(expected) == orbit_size(n, b), "binomial orbit count") + require(set(histogram.values()) == {len(matrices) // len(expected)}, + "equal mixed-sign fiber counts") + return dict(counts) + + +def independent_and_constructive_checks() -> dict[str, int]: + counts = Counter() + for n in range(1, 5): + all_maps = product(range(1 << n), repeat=n) + direct = {s for s in all_maps if compose(transpose(s), s) == identity(n)} + require(direct == set(enumerate_group(n)), "independent full-matrix census") + counts["all_binary_matrices"] += 1 << (n * n) + for n in range(1, 10): + for b in range(1 << n): + found = 0 + for e in range(1 << n): + expected = admissible(b, e) + require(expected == (q(b, e) == 0), "isotropic-vector criterion") + counts["sign_defect_candidates"] += 1 + if expected: + t = representative(n, e) + require(orthogonal(t), "representative orthogonality") + require(compose(t, t) == identity(n), "representative involution") + require(defect(t, b) == e, "representative mixed-sign defect") + found += 1 + counts["constructive_representatives"] += 1 + require(found == orbit_size(n, b), "all-sign binomial count") + return dict(counts) + + +def cocycle_and_controls() -> dict[str, int]: + matrices = enumerate_group(4) + pairs = 0 + for b in range(16): + for a in matrices: + for c in matrices: + require(defect(compose(a, c), b) == + defect(a, b) ^ apply(a, defect(c, b)), "twisted cocycle") + pairs += 1 + t = representative(5, 3) + require(orthogonal(t) and defect(t, 1) == 3, "first mixed-sign fixture") + require(defect(t, 0) == 0, "same transvection equal-sign control") + require(not admissible(1, 15), "equal-sign criterion cannot be reused") + require(not orthogonal(representative(5, 1)), "odd vector is not orthogonal") + require(defect(representative(4, 15), 1) == 0, "weight-four need not be defect") + require(orbit_size(6, 1) == 12 and group_order(6) // 12 == 1920, + "six-axis mixed-sign stabilizer") + require(orbit_size(6, 0) == 16, "six-axis equal-sign distinction") + require(any(defect(compose(a, c), 1) != defect(a, 1) ^ defect(c, 1) + for a in matrices for c in matrices), "untwisted cocycle mutant") + require(any(defect(s, 1) != defect(transpose(s), 1) for s in matrices), + "transpose convention mutant") + require(any(defect(s, 1) != defect(s, 0) for s in matrices), + "omitted sign transport mutant") + return {"cocycle_pairs": pairs, "semantic_controls": 10} + + +def main() -> None: + result = {"status": "PASS_MIXED_SIGN_PHASE_SPECTRUM"} + result.update(enumerate_checks()) + result.update(independent_and_constructive_checks()) + result.update(cocycle_and_controls()) + package = Path(__file__).resolve().parent + files = sorted(p for p in package.iterdir() if p.is_file()) + require(len(files) <= 12, "package file capacity exceeded") + result["files_sha256"] = {p.name: sha256(p.read_bytes()).hexdigest() for p in files} + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()