From 1678bc607c369b90ac573e6c7188fb254ef03c05 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 10:08:38 +0000 Subject: [PATCH] feat(research): classify phase defects fixing a binary subspace --- .../fixed-subspace-phase-defects/PROOF.md | 125 ++++++++++ .../fixed-subspace-phase-defects/README.md | 128 ++++++++++ .../fixed-subspace-phase-defects/SOURCES.json | 30 +++ .../fixed-subspace-phase-defects/TASK.json | 93 ++++++++ .../fixed-subspace-phase-defects/VERIFY.json | 34 +++ .../fixed-subspace-phase-defects/verify.py | 222 ++++++++++++++++++ 6 files changed, 632 insertions(+) create mode 100644 research/fixed-subspace-phase-defects/PROOF.md create mode 100644 research/fixed-subspace-phase-defects/README.md create mode 100644 research/fixed-subspace-phase-defects/SOURCES.json create mode 100644 research/fixed-subspace-phase-defects/TASK.json create mode 100644 research/fixed-subspace-phase-defects/VERIFY.json create mode 100644 research/fixed-subspace-phase-defects/verify.py diff --git a/research/fixed-subspace-phase-defects/PROOF.md b/research/fixed-subspace-phase-defects/PROOF.md new file mode 100644 index 0000000000..9331643ad3 --- /dev/null +++ b/research/fixed-subspace-phase-defects/PROOF.md @@ -0,0 +1,125 @@ +# Phase defects with a pointwise fixed subspace + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement + +Let V=F_2^n, n>=1, with its ordinary nondegenerate dot product. Fix b in V, +a subspace W of V, and the quadratic refinement + + q_b(x) = wt(x) + 2(b dot x) modulo 4. + +The dot product in this expression takes values zero and one. Write + + G_W = {S in O(n,2): Sw=w for every w in W}. + +Use the row convention of Gareth Davidson #1255 and Nick Petalas #5225: + + q_b(S^T x) - q_b(x) = 2 d_b(S) dot x modulo 4. + +The unrestricted mixed-sign theorem of #5225 is a cited premise. It says +that every defect satisfies q_b(d_b(S))=0, that T_e=I+ee^T has defect e +whenever q_b(e)=0, and that d_b(AB)=d_b(A)+A d_b(B). No predecessor +verification or physical implementation is assumed here. + +**Restricted image theorem.** The exact defect image of G_W is + + D_(b,W) = {e in W-perpendicular: q_b(e)=0}. (1) + +Every e in this set has the representative T_e inside G_W. Put + + H_(b,W) = {S in G_W: d_b(S)=0}. + +Every S in G_W has the unique factorization + + S = T_e H, e=d_b(S), H in H_(b,W). (2) + +Each defect fiber has exactly |H_(b,W)| elements. Consequently + + |H_(b,W)| = |G_W| / |D_(b,W)|. (3) + +This statement permits degenerate W, including totally isotropic subspaces. +No nondegeneracy assumption or choice of a complement to W is needed. + +## Proof of the restriction and its converse + +If S fixes W pointwise, its inverse fixes W pointwise too. Orthogonality gives +S^T=S^-1. For w in W the defining defect identity therefore gives + + 2 d_b(S) dot w = q_b(w)-q_b(w) = 0 modulo 4. + +Thus d_b(S) belongs to W-perpendicular. The cited unrestricted theorem gives +q_b(d_b(S))=0, proving necessity in (1). + +Conversely, let e belong to the set in (1). Since q_b(e)=0, e has even +weight, so e dot e=0. The cited transvection identity gives T_e in O(n,2), +T_e^2=I and d_b(T_e)=e. For every w in W, + + T_e w = w + e(e dot w) = w. + +Hence T_e belongs to G_W. This proves sufficiency and the promised attaining +representative. It also shows that a nonzero defect requires exactly one +such algebraic rank-one transvection when correcting a chart in G_W. +This is a factor count, not a paid physical cost. + +## Factorization and fibers + +For S in G_W, put e=d_b(S) and H=T_e S. Both factors fix W, and the cited +cocycle gives + + d_b(H) = e + T_e e = e+e = 0. + +Here T_e e=e follows from e dot e=0. Thus H belongs to H_(b,W) and S=T_e H. +The defect e is forced by S, after which H=T_e S is forced, proving +uniqueness. The cocycle also shows that zero-defect maps form a subgroup +and that d_b(T_e H)=e for every H in that subgroup. Left multiplication by +T_e is therefore a bijection onto the e fiber. This proves (2) and (3). + +## Literal axes and nested restrictions + +Suppose W is spanned by k distinct coordinate vectors. Orthogonality forces +S to be the identity on those axes and an arbitrary orthogonal map on the +remaining m=n-k coordinates. Defects vanish on the fixed coordinates. +Let b_free be b restricted to the free coordinates. Translation +z -> b_free+z in (1) gives the closed count + + N = sum_{0<=j<=m, j == wt(b_free) modulo 4} binomial(m,j), + |H_(b,W)| = |O(m,2)| / N. (4) + +Use |O(0,2)|=1. The all-fixed case has N=1. In particular, signs on fixed +axes do not affect this count. This answers the literal-axis question left +open by #5225. + +For arbitrary W_1 contained in W_2, equation (1) gives + + D_(b,W_2) = D_(b,W_1) intersect W_2-perpendicular. (5) + +The actual fixed subspace matters, not only its dimension. At n=4, b=0, +fixing e_1 leaves only defect zero. Fixing the isotropic vector e_1+e_2 +allows defects zero and (1,1,1,1). Both constraints have dimension one. +The latter nonzero defect is attained by T_(1,1,1,1), which fixes e_1+e_2 +but moves each of e_1 and e_2. Replacing a required fixed sum by separately +fixed axes would impose a stronger contract. + +## Scope and credit + +This is a scoped algebraic proof. The only change from #5225 is the exact +pointwise-fixed-subspace contract and its consequences above. The sign mask +remains attached to the chart's columns. Setwise stabilization, unequal input +and output restrictions and nonorthogonal charts are separate questions. +The finite verifier corroborates the new restricted statement; it does not +supply its all-width quantifiers or audit predecessor results. + +Credit Nick Petalas #5225 for the unrestricted mixed-sign image, representatives, +cocycle and explicit literal-axis handoff; Philipp / mightyOil #1300 for the +equal-sign phase model; Gareth Davidson #1255 for the residual C-gate phase +and row conventions; and yssite #1558 following icekylinx #24 for the retained +signed Gauss-normalization context. All existing notices remain unchanged. +No external literature priority is claimed for quadratic refinements, +transvections, subgroup fibers or their elementary restriction argument. + +No native producer, chart circuit, physical route, data acquisition, dirty-state +restoration, stock, precision, fixed-tape implementation, compiler or complete +consumer bill is constructed. Those costs remain unknown. No new kappa, +supplier admission, selected-frontier change or complete multiplication theorem +follows. Independent human and formal proof-kernel review are unclaimed. diff --git a/research/fixed-subspace-phase-defects/README.md b/research/fixed-subspace-phase-defects/README.md new file mode 100644 index 0000000000..0d8c026faa --- /dev/null +++ b/research/fixed-subspace-phase-defects/README.md @@ -0,0 +1,128 @@ +# Exact phase defects under fixed-subspace chart constraints + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped algebraic proof with exact finite corroboration. This answers +the literal-axis restriction question left open by merged +[#5225](https://github.com/CrocSwap/integer-mult-bounds/pull/5225), and permits +an arbitrary specified binary subspace W, including degenerate W. + +For V=F2^n, fixed sign mask b, and q_b(x)=wt(x)+2(b dot x) modulo four, let +G_W be the orthogonal chart changes fixing W pointwise. The result is + +```text +{d_b(S): S in G_W} = {e in W-perpendicular: q_b(e)=0}. +T_e = I + e e^T lies in G_W and attains each such e. +S = T_(d_b(S)) H, with H fixing W and preserving the phase exactly. +``` + +All defect fibers have equal size. For k fixed literal axes and m=n-k free +axes, their number is + +```text +N = sum_{0<=j<=m, j == wt(b_free) mod 4} binomial(m,j). +``` + +The exact phase-preserver subgroup has order |O(m,2)|/N. Signs on fixed axes +do not affect this count. The all-fixed case has N=1. + +The actual fixed subspace matters. At n=4 with all positive signs, fixing e1 +permits only defect zero, while fixing e1+e2 permits zero and (1,1,1,1). +These are constraints of the same dimension. [PROOF.md](PROOF.md) gives the +all-width argument, attaining representatives, subgroup fibers and these +specializations. This is a local algebraic result, with no new kappa. + +## Evidence and reproduction + +The standalone verifier enumerates every orthogonal matrix, subspace and +sign mask through width five. It checks the restricted images, equal fibers, +attaining representatives and full factorization for each admissible matrix. +Its generated counts are: + +- 464 subspaces and 13,192 subspace/sign contexts; +- 30,232 attaining representatives and 168,200 restricted factorizations; +- 1,364 literal-axis formula contexts; +- 777 orthogonal matrices and 749,988 literal phase comparisons. + +Eight controls distinguish unrestricted charts, fixed sums versus separately +fixed axes, even weight versus phase zero, transported signs, pointwise versus +setwise stabilization, zero versus nonzero correction, and capacity rejection. +These finite checks corroborate the new restriction theorem. The universal +claim rests on the proof and cited unrestricted theorem, not extrapolation. +No predecessor executable is imported or replayed. + +From the repository root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/fixed-subspace-phase-defects/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/fixed-subspace-phase-defects/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/fixed-subspace-phase-defects +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/fixed-subspace-phase-defects --check-source-history +``` + +Any CPython 3.12 installation can replace the local interpreter path. The +verifier prints `PASS_FIXED_SUBSPACE_PHASE_DEFECTS` and a generated JSON receipt +binding all six package files by SHA256. It writes nothing. The publication +preflight requires Git history; the direct verifier supports a Git-free export. + +## Scope, sources and implementation limits + +The base is canonical main de5ec2e7a6074068452f45b1a191b5c72832df4a, priority +revision 8. [TASK.json](TASK.json) changes the `bit-helper-contract` card to +this algebraic side result, because #5225 explicitly leaves this route constraint +open. The card's current selected-binding first step passed. It is metadata +orientation, not a selected supplier replay. [SOURCES.json](SOURCES.json) pins +the predecessor proof and README as provenance, alongside the selected record +and catalogue. They are not runtime inputs to the new verifier. + +The advance [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19214412) +followed live open/account PR and Discussion checks, local reservation and +distinctive main/merged searches. The overlap cache completely paginated 416 +open PRs and 5,307 Discussion records. Sparse local coverage searched 185 of +7,845 tracked notes; targeted all-main README and merged-PR searches supplemented +it. Unpublished work and arbitrary historical diffs remain outside that coverage. +No search establishes external mathematical priority. + +The new verifier is bounded at widths 1..5, at most 720 complete matrices, +374 subspaces and 32 vectors in one width. It has no recursion, subprocesses, +network, dynamic code or shared mutable state. All functions stay below 60 +physical lines. Explicit exceptions retain the checks under optimized Python; +both registered commands treat warnings as errors. No additional static analyzer +is configured or claimed. The only file reads are the six local receipt inputs. + +Power of Ten rule 3 deviation: CPython allocates integers and containers during +finite enumeration. The enforced width bound limits each subspace to 32 vectors, +the subspace inventory to 374 entries, the group inventory to 720 entries and +the sign/defect table to 32 by 720 integers. No fixed-allocation claim is made. +Normal and optimized complete finite replays exercise this domain. Any executable +width expansion requires a fresh capacity review; the written theorem has no +such finite-width restriction. + +The contract fixes W pointwise and retains orthogonal charts and a fixed sign +mask. Setwise stabilization and nonorthogonal charts are outside scope. No native +producer, chart circuit, physical route, acquisition, dirty restoration, stock, +precision, tape implementation, compiler or complete consumer bill is supplied. +Those costs remain unknown. No supplier admission, selected-frontier change or +complete multiplication theorem follows. Lean, Docker and selected scientific +cold replay were not run. Independent human and formal proof-kernel review are +unclaimed. + +## Open next questions + +Can a named native helper exploit one nonzero admissible defect while preserving +its required literal directions? Start with its actual fixed subspace W and +sign mask b, and price the T_e chart change with all acquisition, transport and +restoration costs. Algebraic attainability supplies none of those prices. This +question is unclaimed here; no further construction expansion is justified by +this package alone. + +## Credit + +Nick Petalas #5225 supplies the unrestricted mixed-sign theorem and explicit +fixed-axis question. Philipp / mightyOil #1300 supplies the equal-sign phase +model, Gareth Davidson #1255 the residual C-gate contract and row convention, +and yssite #1558 following icekylinx #24 the signed Gauss-normalization context. +Credit Rohan Arun, Jeremy Kothe, Hao Yan, Josie Elliston, Douglas Colkitt and the +retained Clifford/normalization lineage. Classical quadratic refinements, +transvections and subgroup-fiber arguments retain their classical status. +All predecessor notices remain unchanged. diff --git a/research/fixed-subspace-phase-defects/SOURCES.json b/research/fixed-subspace-phase-defects/SOURCES.json new file mode 100644 index 0000000000..ecbda286cc --- /dev/null +++ b/research/fixed-subspace-phase-defects/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/mixed-sign-phase-spectrum/PROOF.md", + "usage": "provenance", + "git_blob": "52457e2cdf873ad649dde6142542840a1e7f2776", + "sha256": "cdfc423adaf8623cb9e2d61a9d18aca97e75604d2ab1e9360bdc4e15433a57f9" + }, + { + "path": "research/mixed-sign-phase-spectrum/README.md", + "usage": "provenance", + "git_blob": "19a7b6b1c6b235f12e46f8b1f327d57c7dfe7f2b", + "sha256": "2ef5f8bd5d543a2910a3e2cff022add0283a869ff625ddf8c4ecd7b42f8f4472" + } + ] +} diff --git a/research/fixed-subspace-phase-defects/TASK.json b/research/fixed-subspace-phase-defects/TASK.json new file mode 100644 index 0000000000..efa6b5ebcd --- /dev/null +++ b/research/fixed-subspace-phase-defects/TASK.json @@ -0,0 +1,93 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "bit-helper-contract", + "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/g20-helper-split/README.md", + "research/g20-conjugation-admission/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "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", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "G20", + "helper split", + "5679", + "5708", + "independent target" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact mixed-sign orthogonal phase-defect image for chart changes fixing an arbitrary binary subspace pointwise, with attaining transvections, equal fibers and the literal-axis closed count.", + "scope_change_reason": "Merged PR5225 explicitly leaves fixed literal axes open. This proves that missing route-constraint lemma, generalized to arbitrary specified subspaces, rather than auditing the unrestricted theorem or constructing a BIT supplier.", + "bottleneck_link": "A constrained signed chart can preserve required directions exactly when its defect lies in the proved restricted image. This is an algebraic interface side result; physical synthesis, transport, restoration and complete supplier costs remain unknown.", + "budget_minutes": 60, + "stop_rule": "Stop after the first verified restricted-image theorem and its literal-axis specialization; do not extend to physical synthesis or new parameter searches.", + "outcome": "completed", + "evidence": "PROOF.md proves the all-width restricted image and equal fibers. The standalone verifier covers every subspace/sign context through width five, with 13192 contexts, 30232 attaining representatives, 168200 factorizations and eight controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a named native helper exploit an admissible constrained defect at a lower complete physical cost?", + "why_it_matters": "An algebraically legal chart change may still cost more than its benefit.", + "first_step": "Bind its exact fixed subspace and signs, then price one explicit T_e chart including acquisition, transport and restoration.", + "blocked_by": "No physical chart program, native consumer or complete cost ledger is supplied." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19214412", + "checked_main": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "priority_revision": 8, + "overlap_open_prs": 416, + "overlap_discussion_records": 5307, + "complete_remote_pagination": true, + "sparse_local_notes": 185, + "tracked_notes": 7845, + "limits": "Targeted main README and merged searches supplement incomplete sparse local coverage. Unpublished work and arbitrary historical diffs are not covered." + }, + "predecessor": { + "pr": 5225, + "head": "350b7408b11161aa153b5ab74c51fb1881909389", + "usage": "Cited unrestricted theorem and explicit open question; no executable imports or audit." + } +} diff --git a/research/fixed-subspace-phase-defects/VERIFY.json b/research/fixed-subspace-phase-defects/VERIFY.json new file mode 100644 index 0000000000..bc7a52b368 --- /dev/null +++ b/research/fixed-subspace-phase-defects/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": 120, + "checks": "Complete width-one-through-five fixed-subspace/sign census, attaining representatives, equal fibers, literal-axis formula, factorizations, literal phases and eight controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete width-one-through-five fixed-subspace/sign census, attaining representatives, equal fibers, literal-axis formula, factorizations, literal phases and eight controls." + } + ] +} diff --git a/research/fixed-subspace-phase-defects/verify.py b/research/fixed-subspace-phase-defects/verify.py new file mode 100644 index 0000000000..a16f8f2e0a --- /dev/null +++ b/research/fixed-subspace-phase-defects/verify.py @@ -0,0 +1,222 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the pointwise-fixed-subspace phase theorem. + +Produced by Nick Petalas. Apache-2.0. Standard library only; writes no files. +""" +from collections import Counter +from hashlib import sha256 +import json +from math import comb +from pathlib import Path + + +MAX_WIDTH = 5 +MAX_STATES = 4096 +PACKAGE_FILES = ( + "PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py" +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dot(x, y): + return (x & y).bit_count() & 1 + + +def phase(b, x): + return (x.bit_count() + 2 * dot(b, x)) % 4 + + +def apply(columns, x): + result = 0 + for i, column in enumerate(columns): + if x & (1 << i): + result ^= column + return result + + +def transpose(columns): + n = len(columns) + return tuple(sum(((columns[j] >> i) & 1) << j for j in range(n)) + for i in range(n)) + + +def compose(left, right): + return tuple(apply(left, column) for column in right) + + +def transvection(n, e): + return tuple((1 << i) ^ (e if e & (1 << i) else 0) for i in range(n)) + + +def defect(columns, b): + result = 0 + for i, row in enumerate(transpose(columns)): + difference = (phase(b, row) - phase(b, 1 << i)) % 4 + require(difference in (0, 2), "orthogonal defect must be even") + result |= (difference // 2) << i + return result + + +def orthogonal_group(n): + require(1 <= n <= MAX_WIDTH, "orthogonal enumeration capacity") + states = [()] + candidates = tuple(v for v in range(1 << n) if dot(v, v)) + for _ in range(n): + states = [prefix + (v,) for prefix in states for v in candidates + if all(dot(v, w) == 0 for w in prefix)] + require(len(states) <= MAX_STATES, "partial group capacity") + require(len(states) == len(set(states)), "duplicate group element") + return tuple(states) + + +def all_subspaces(n): + require(1 <= n <= MAX_WIDTH, "subspace enumeration capacity") + level = {(0,)} + spaces = [(0,)] + for _ in range(n): + next_level = set() + for space in level: + for v in range(1 << n): + if v not in space: + extension = tuple(sorted((*space, *(x ^ v for x in space)))) + next_level.add(extension) + require(len(next_level) <= MAX_STATES, "subspace level capacity") + spaces.extend(sorted(next_level)) + level = next_level + require(len(spaces) == len(set(spaces)), "duplicate subspace") + return tuple(spaces) + + +def basis(space, n): + generated = {0} + result = [] + for v in space: + if v not in generated: + result.append(v) + generated.update(tuple(x ^ v for x in generated)) + require(len(result) <= n and generated == set(space), "basis span mismatch") + return tuple(result) + + +def phase_table(group, n, counts): + tables = [] + for b in range(1 << n): + values = [] + for matrix in group: + e = defect(matrix, b) + values.append(e) + rows = transpose(matrix) + for x in range(1 << n): + actual = (phase(b, apply(rows, x)) - phase(b, x)) % 4 + require(actual == 2 * dot(e, x), "literal phase defect mismatch") + counts["literal_phase_values"] += 1 + tables.append(tuple(values)) + return tuple(tables) + + +def axis_count(n, w_basis, b): + if any(w.bit_count() != 1 for w in w_basis): + return None + fixed = sum(w_basis) + free = ((1 << n) - 1) ^ fixed + m = n - len(w_basis) + residue = (b & free).bit_count() % 4 + return sum(comb(m, j) for j in range(m + 1) if j % 4 == residue) + + +def check_context(n, w_basis, b, group, indices, table, allowed, counts): + predicted = {e for e in range(1 << n) + if phase(b, e) == 0 and all(dot(e, w) == 0 for w in w_basis)} + observed = Counter(table[i] for i in allowed) + require(set(observed) == predicted, "restricted image mismatch") + require(len(set(observed.values())) == 1, "unequal restricted fibers") + require(sum(observed.values()) == len(allowed), "lost group elements") + counts["subspace_sign_contexts"] += 1 + counts["attainable_defects"] += len(predicted) + for e in predicted: + representative = transvection(n, e) + require(representative in indices, "representative not orthogonal") + require(all(apply(representative, w) == w for w in w_basis), + "representative moves required vector") + require(table[indices[representative]] == e, "representative defect") + counts["attaining_representatives"] += 1 + for i in allowed: + representative = transvection(n, table[i]) + h = compose(representative, group[i]) + require(h in indices and table[indices[h]] == 0, "factor not phase exact") + require(all(apply(h, w) == w for w in w_basis), "factor moves W") + require(compose(representative, h) == group[i], "factorization mismatch") + counts["restricted_factorizations"] += 1 + closed = axis_count(n, w_basis, b) + if closed is not None: + require(closed == len(predicted), "literal-axis binomial count") + counts["coordinate_axis_contexts"] += 1 + + +def run_census(): + counts = Counter() + for n in range(1, MAX_WIDTH + 1): + group = orthogonal_group(n) + spaces = all_subspaces(n) + require(len(group) == (1, 2, 6, 48, 720)[n - 1], "group census size") + require(len(spaces) == (2, 5, 16, 67, 374)[n - 1], "subspace census size") + indices = {matrix: i for i, matrix in enumerate(group)} + tables = phase_table(group, n, counts) + counts["orthogonal_matrices"] += len(group) + counts["subspaces"] += len(spaces) + for space in spaces: + w_basis = basis(space, n) + allowed = tuple(i for i, matrix in enumerate(group) + if all(apply(matrix, w) == w for w in w_basis)) + require(allowed, "identity missing from pointwise stabilizer") + for b in range(1 << n): + check_context(n, w_basis, b, group, indices, tables[b], allowed, counts) + return dict(sorted(counts.items())) + + +def controls(): + n = 4 + identity = tuple(1 << i for i in range(n)) + e = 15 + t = transvection(n, e) + require(phase(0, e) == 0 and apply(t, 1) != 1, + "unrestricted representative must violate a fixed-axis fixture") + require(apply(t, 3) == 3 and apply(t, 1) != 1 and apply(t, 2) != 2, + "fixing a sum is weaker than fixing its summands") + require(phase(0, 3) == 2, "even weight alone is insufficient") + require(phase(1, 3) == 0 and defect(transvection(n, 3), 1) == 3, + "dropping the transported signs must change the fixture") + swap = (2, 1, 4, 8) + require(defect(swap, 1) == 3 and apply(swap, 1) != 1, + "setwise stabilization is not pointwise stabilization") + require(defect(identity, 15) == 0 and defect(t, 0) == 15, + "identity and nonzero correction controls") + try: + orthogonal_group(6) + except ValueError: + pass + else: + raise ValueError("group capacity must reject") + try: + all_subspaces(0) + except ValueError: + pass + else: + raise ValueError("subspace capacity must reject") + return 8 + + +def receipt(): + root = Path(__file__).resolve().parent + hashes = {name: sha256((root / name).read_bytes()).hexdigest() + for name in PACKAGE_FILES} + return {"status": "PASS_FIXED_SUBSPACE_PHASE_DEFECTS", + "evidence": run_census(), "controls": controls(), "sha256": hashes} + + +if __name__ == "__main__": + print(json.dumps(receipt(), sort_keys=True))