diff --git a/research/coherent-transvection-neighborhood/README.md b/research/coherent-transvection-neighborhood/README.md new file mode 100644 index 0000000000..6859d06bca --- /dev/null +++ b/research/coherent-transvection-neighborhood/README.md @@ -0,0 +1,238 @@ +# Exact cycle-constrained chart neighborhoods + +This contribution, produced by Nick Petalas, proves a scoped binary symplectic +geometry result. It extends David Ganz's single/pair transvection enumeration +in [PR4841](https://github.com/CrocSwap/integer-mult-bounds/pull/4841) to any +nonempty tuple of Lagrangian charts and a linear restriction on the allowed +axes. A graph-cycle kernel supplies one useful such restriction. + +The new result is an exact formula, an executable duplicate-free enumerator +and a written all-dimensional proof. The finite certificate corroborates that +proof. It is not a changed physical word, supplier admission, a complete +multiplication theorem or a new kappa. The selected frontier is unchanged. + +## The result + +Let V be a 2n-dimensional symplectic space over F2, with n>=1 and alternating +form omega. For a in V put T_a(x)=x+omega(x,a)a, including T_0=identity. +Let L_1,...,L_s be any nonempty finite tuple of Lagrangians. Let A be a linear +subspace of allowed axes. Define + +``` +I = intersection of all L_i +B = A intersect I +m = dim A, b = dim B, r = m-b +t = rank of the pairing A -> B*, a |-> omega(a, .)|B +``` + +Then 0<=t<=min(b,r). The exact number of distinct **changed** tuples +`(T_a L_1,...,T_a L_s)`, for a in A, is + +``` +N(A; L_1,...,L_s) = 2^(r+1) - 2^(r-t) - 1. +``` + +The unchanged tuple is excluded. All axes in B produce that one tuple. +For every a in A outside B, its exact fiber is + +``` +a + (B intersect a-perp). +``` + +In particular its size is 2^b if a is orthogonal to B and 2^(b-1) otherwise. +This characterizes every fiber, not only the number of outputs. + +Choose any vector-space complement C of B in A. For each nonzero c in C, +retain c. If omega(c,B) is nonzero, choose b_c in B with omega(c,b_c)=1 and +also retain c+b_c. These axes produce every changed tuple exactly once. +`neighborhood` in [verify.py](verify.py) implements this algorithm from bases, +using coefficient kernels rather than enumerating the ambient axis space. + +## Proof + +We use the one-chart equivalence stated and proved in David Ganz's +[complete-neighbors construction](https://github.com/CrocSwap/integer-mult-bounds/blob/6debdcdac8fe1c87958f8cd42ccb7db73c0a0eef/research/native-clifford-gauge-compiler/decoder/COMPLETE-PAIRED-NEIGHBORS.md), +at the exact predecessor head. For a Lagrangian L, T_a L=L exactly when a is +in L. For two nonfixed axes a,c, their changed charts agree exactly when +`c-a in L intersect a-perp`. This is an inherited lemma. No predecessor +verifier or supplier is imported or replayed here. + +**Tuple fibers.** Suppose a is outside I and a,c produce the same tuple. +At least one chart moves. On every moved chart, the inherited equivalence +puts c-a in that chart and in a-perp. On a fixed chart, both axes belong to +the chart, so their difference also belongs to it. Therefore c-a lies in +`I intersect a-perp`. Conversely this condition fixes every originally fixed +chart and gives equal images on every moved chart. Restricting a,c to A +changes I in this difference condition to B. Axes in B fix every chart; +axes outside B move at least one. This proves the full fiber statement. + +**Count and representatives.** B is isotropic because it is contained in +L_1. Hence the functional omega(a,.) on B is constant on every coset of B +in A. It defines a rank-t linear map from A/B to B*, so t<=r and t<=b. +Exactly 2^(r-t) cosets annihilate B. Each such coset is one fiber. Every +other coset has two fibers, because its nonzero functional on B has a +codimension-one kernel. Thus the number including the unchanged tuple is + +``` +2^(r-t) + 2 (2^r - 2^(r-t)) = 2^(r+1) - 2^(r-t). +``` + +Remove its zero coset. A complement selects one c from each remaining +coset. When there are two fibers, addition of b_c crosses between them. +Different cosets cannot give equal tuples by the fiber statement. This +proves the formula and the duplicate-free construction for all n,s,A. + +**Relation to the predecessor.** If A=V and k=dim I, then m=2n, b=t=k by +nondegeneracy, giving `2^(2n-k+1)-2^(2n-2k)-1`. For s=1 or s=2 this is +Ganz's existing result. That specialization is not claimed as new. The +new boundary permits any number of charts and restricted axes, where t +need not equal b and an ambient-space substitution can give the wrong count. + +## Exact transport through a graph + +Consider a finite connected contact graph. Each oriented internal edge e:u->v +has a specified symplectic map S_e. Choose a rooted spanning tree and let R_v +be its root-to-v transport, with R_root=identity. A coherent transvection +assignment has axes a_v=R_v a. The complete allowed root-axis space is + +``` +A = intersection over edges e:u->v of ker(R_v - S_e R_u). +``` + +Tree-edge equations vanish. Equivalently each remaining cycle fixes a under +its root holonomy `R_v^-1 S_e R_u`. The equations retain every edge, including +parallel edges and inconsistent cycles. + +Indeed `S T_a S^-1 = T_(S a)` for a symplectic S. Over F2 the axis map +`a |-> T_a` is injective, including zero. For nonzero a, the image of T_a-I +is the line spanned by a, whose only nonzero element is a. Consequently +`T_(a_v) S_e = S_e T_(a_u)` holds exactly when a_v=S_e a_u. +These are precisely the kernel equations above. The tree forces every coherent +assignment to have a_v=R_v a, so the kernel is also necessary. + +Apply the theorem to root-coordinate charts `K_v=R_v^-1 L_v` and this A. +Multiplying each output by R_v is invertible, so it preserves equality and +distinctness of chart tuples. The enumerator is therefore complete for the +stated coherent graph moves. Every internal contact rank is preserved, since + +``` +(T_(a_v) L_v) intersect (S_e T_(a_u) L_u) + = T_(a_v) (L_v intersect S_e L_u). +``` + +This is a sufficient restricted class. The theorem does not classify all +assignments that happen to preserve internal ranks. Boundary-edge costs, +absolute phases, ownership, endpoint restoration and all compiler/precision +costs must still be paid in an actual changed word. Their new full invoice is +unknown here. The family decision is to retain this local enumeration lemma +and stop before further physical construction or optimization. + +## Two sharp finite distinctions + +Write e_1,e_2,e_3,f_1,f_2,f_3 for the standard symplectic basis. Compare + +``` +U = (span(e1,e2,e3), span(e1,f2,f3), span(f1,e2,f3)) +W = (span(e1,e2,e3), span(e1,f2,f3), span(e1,e2+f2,e3+f3)). +``` + +Every pair in either triple intersects in dimension one. U has common +intersection zero and exactly 63 changed tuples. W has common intersection +span(e1) and exactly 47. Thus even all pairwise distances fail to determine +the coordinated triple neighborhood. + +For W, impose the single cycle holonomy T_e1. Its fixed-axis space is +A=e1-perp. Now `(m,b,t)=(5,1,0)` and exactly 15 changed tuples remain. +The unrestricted ambient formula gives 47 and would overcount this search. +The verifier enumerates each stated endpoint set literally. + +## Verification and reproduction + +Use CPython 3.12 and its standard library. From the repository root: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/coherent-transvection-neighborhood/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/coherent-transvection-neighborhood/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/coherent-transvection-neighborhood +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/coherent-transvection-neighborhood --check-source-history +``` + +Expected direct output is +`PASS_COHERENT_TRANSVECTION_NEIGHBORHOOD cases=226260 literal_graph_axes=4096`. +Checks use explicit exceptions and remain active with -O. + +For n=1,2 the replay enumerates every linear allowed-axis subspace and every +ordered triple of Lagrangians, including repeated charts. It compares the +actual transformed-subspace sets and exact axis fibers with the representatives +and the formula. The implementation caches identical `(A,B)` enumeration +problems, while testing the literal outputs for every triple/subspace case. +It also checks 256 three-vertex graphs with two independent cycle constraints, +using all 4,096 root-axis tests and literal matrix conjugation equations. +The two n=3 distinctions above are checked separately. Eleven invalid-input +controls and five named mathematical mutations reject. See the generated +[RESULT.json](RESULT.json) for the full enumerated histograms. + +`RESULT.json` binds the five package source/metadata files by SHA256. To +regenerate it, pass `--write-receipt /absolute/scratch/path/result.json` to +the same verifier, then compare that generated file. A changed receipt or +source file fails ordinary replay. No network, Git, solver or predecessor +module is needed for direct replay. The citation-only external source in +SOURCES.json is pinned by URL, commit, Git blob and SHA256; it is not a runtime +input or an implicit dependency on an unmerged commit. + +The original card's historical positive control was attempted and failed with +`KeyError: 'complex_profile'` in `complex-local-word-ceiling/verify.py` against +the current selected schema. No repair or audit of that old package is claimed. +The source-bound selected-baseline orientation passes. The changed scope and +reason are explicit in TASK.json. No historical/native/Lean/Docker suite or +formal proof-kernel review is part of this contribution. + +## Implementation bounds + +The theorem is all-dimensional. The public executable accepts 1<=n<=9, +1<=s<=64 charts and at most 128 graph edges. Bases have at most 18 vectors. +Chart intersection contributes at most 576 scalar equations; cycle equations +contribute at most 2,304. Enumeration visits at most 2^18 quotient elements +and retains at most 2^18-1 axes. The exhaustive verifier is separately capped +at ambient dimension four and fixed finite graph/fixture lists. Control flow +has no recursion. Functions stay below 60 lines and checked preconditions and +invariants use exceptions. The registered runs enable warning errors normally +and under -O. No shared runtime or selected source is changed. + +Power-of-Ten rule 3 has a managed-runtime deviation. Python allocates integers +and collections during elimination and enumeration. The scope is this bounded, +one-shot standard-library verifier and enumerator. Enforced dimension/chart/ +edge limits bound the live collections; exhaustive endpoint tests exercise +the algorithm rather than a persistent service. A fixed-capacity native port +would be required if steady-operation allocation must be prohibited. +Rule 9 has a bounded test-only dispatch deviation for the eleven explicit +invalid-input callables. Their targets are fixed in `rejection_controls`, and +all must raise ValueError. Production enumeration and transport use direct +calls. No general callback or registration mechanism is provided. + +## Open next questions + +- Does an actual complete source word have a cycle-coherent multi-chart move + with a strict full paid-moment gain? Start with a small connected contact + subgraph and enumerate its kernel-constrained representatives, repricing + every boundary edge. An exact source graph, phase-aware charts, ownership + and the complete paid inventory are required. +- Which rank-neutral coordinated moves lie outside edge conjugation? Start + with one small cycle and compare all endpoint-axis assignments with the + coherent kernel. A changed boundary contract and complete external-edge + accounting are required before using those moves in a supplier. + +The structured versions of these questions are in TASK.json. + +## Credit and scope of originality + +This contribution was produced by Nick Petalas. David Ganz / Dugongue, +PR4841 at `6debdcdac8fe1c87958f8cd42ccb7db73c0a0eef`, supplies the inherited +single/pair equivalence and coset representative idea. The new result is the +restricted-axis tuple formula and its complete cycle-coherent graph boundary, +with exact finite corroboration. No priority for classical symplectic geometry +or transvection conjugation is claimed. Cao Yifan / intqwq PR4610, Cinna Davis +PR4690/PR4672 and the retained native-caller contributors supply the contact +optimization setting through that predecessor. Their source credits remain +unchanged. Independent human and formal proof-kernel review are unclaimed. +Apache-2.0. diff --git a/research/coherent-transvection-neighborhood/RESULT.json b/research/coherent-transvection-neighborhood/RESULT.json new file mode 100644 index 0000000000..5a402c0d5d --- /dev/null +++ b/research/coherent-transvection-neighborhood/RESULT.json @@ -0,0 +1,199 @@ +{ + "claim_type": "scoped proof with finite exact corroboration", + "exhaustive": [ + { + "allowed_subspaces": 5, + "distinct_axis_problems": 11, + "lagrangians": 3, + "n": 1, + "parameter_histogram": [ + [ + 0, + 0, + 0, + 27 + ], + [ + 1, + 0, + 0, + 78 + ], + [ + 1, + 1, + 0, + 3 + ], + [ + 2, + 0, + 0, + 24 + ], + [ + 2, + 1, + 1, + 3 + ] + ], + "triple_subspace_cases": 135 + }, + { + "allowed_subspaces": 67, + "distinct_axis_problems": 382, + "lagrangians": 15, + "n": 2, + "parameter_histogram": [ + [ + 0, + 0, + 0, + 3375 + ], + [ + 1, + 0, + 0, + 50220 + ], + [ + 1, + 1, + 0, + 405 + ], + [ + 2, + 0, + 0, + 115320 + ], + [ + 2, + 1, + 0, + 1170 + ], + [ + 2, + 1, + 1, + 1620 + ], + [ + 2, + 2, + 0, + 15 + ], + [ + 3, + 0, + 0, + 47880 + ], + [ + 3, + 1, + 0, + 360 + ], + [ + 3, + 1, + 1, + 2340 + ], + [ + 3, + 2, + 1, + 45 + ], + [ + 4, + 0, + 0, + 3000 + ], + [ + 4, + 1, + 1, + 360 + ], + [ + 4, + 2, + 2, + 15 + ] + ], + "triple_subspace_cases": 226125 + } + ], + "graph": { + "allowed_dimension_histogram": [ + [ + 2, + 210 + ], + [ + 3, + 45 + ], + [ + 4, + 1 + ] + ], + "graphs": 256, + "literal_axis_tests": 4096 + }, + "mutation_controls": [ + "omit-second-representative", + "omit-axis-quotient", + "omit-pairing-rank", + "include-fixed-outcome", + "ignore-allowed-axis-space" + ], + "rejection_controls": 11, + "schema": "coherent-transvection-neighborhood/v1", + "sharp_fixtures": { + "one_cycle_constraint": { + "changed_tuples": 15, + "m_b_t": [ + 5, + 1, + 0 + ] + }, + "same_pairwise_distances": [ + { + "changed_tuples": 63, + "m_b_t": [ + 6, + 0, + 0 + ] + }, + { + "changed_tuples": 47, + "m_b_t": [ + 6, + 1, + 1 + ] + } + ] + }, + "source_sha256": { + "README.md": "927590f0144c4520febf6ccae3a0c31d4ab1f7cc77e5c9a27bc686e0d0609d9a", + "SOURCES.json": "7160419e21fa3bbd95886a0b1311d66e1dce752fc0e45b29bb929ff0272db836", + "TASK.json": "2a6b9ff15d4d46cebdc040b8439f1fc93511e8964312313fc42632bfb0390394", + "VERIFY.json": "21d6bf980f9c281beaf7ee608eda3e81d7b31e318d87b4000cf9aad985e30895", + "verify.py": "e129bc4fe57e1b4c3695de36c34628e7de5656a640435cfe9595a9a2dbb68593" + } +} diff --git a/research/coherent-transvection-neighborhood/SOURCES.json b/research/coherent-transvection-neighborhood/SOURCES.json new file mode 100644 index 0000000000..000a6081ff --- /dev/null +++ b/research/coherent-transvection-neighborhood/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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" + } + ], + "external_citations": [ + { + "author": "David Ganz / Dugongue", + "pr": 4841, + "commit": "6debdcdac8fe1c87958f8cd42ccb7db73c0a0eef", + "path": "research/native-clifford-gauge-compiler/decoder/COMPLETE-PAIRED-NEIGHBORS.md", + "git_blob": "3ca24bdfb03148d25f3da7c9f7a167223d70ef0b", + "sha256": "a41a68710aae94992c46aa42e48a327fd50a4e640ffc6d67ea3b48f9e16a4a24", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/6debdcdac8fe1c87958f8cd42ccb7db73c0a0eef/research/native-clifford-gauge-compiler/decoder/COMPLETE-PAIRED-NEIGHBORS.md", + "usage": "Citation-only predecessor; no imported or executed dependency. The proof and verifier are self-contained." + } + ] +} diff --git a/research/coherent-transvection-neighborhood/TASK.json b/research/coherent-transvection-neighborhood/TASK.json new file mode 100644 index 0000000000..fe199b1637 --- /dev/null +++ b/research/coherent-transvection-neighborhood/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. 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/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact duplicate-free binary transvection neighborhoods for any nonempty tuple of Lagrangian charts, restricted to a linear allowed-axis space, with cycle-coherent graph interpretation.", + "scope_change_reason": "Extend David Ganz PR4841 single/pair enumeration to coordinated tuples constrained by graph cycles. This is an original scoped geometry lemma, not the card's paid-profile construction or an audit of its predecessor.", + "bottleneck_link": "Coordinated chart changes must price all incident edges. The new quotient enumerates every changed tuple once while satisfying exact internal-edge transport constraints. No strict paid-moment gain or completed supplier is supplied.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified general formula and complete representative algorithm; do not run a source-word optimization campaign.", + "outcome": "completed", + "evidence": "README.md gives the all-dimensional proof; verify.py checks literal transformed subspaces, exact fibers, graph conjugation and named rejecting controls; RESULT.json is generated and bound to package source hashes.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does an actual complete source word have a cycle-coherent multi-chart move with a strict full paid-moment improvement?", + "why_it_matters": "A complete search neighborhood supplies no gain unless the fully charged changed word improves.", + "first_step": "Choose a small connected source contact subgraph, compute its cycle kernel and enumerate these representatives while repricing every boundary edge.", + "blocked_by": "An exact source graph, phase-aware physical charts, ownership and complete paid inventory." + }, + { + "question": "Which rank-neutral coordinated moves lie outside the edge-conjugation constraint?", + "why_it_matters": "The exact enumerator covers coherent transvection transport, a sufficient restricted class. Other moves may preserve internal ranks without preserving each edge map.", + "first_step": "Specify one small cycle and compare all endpoint axis assignments with the kernel-constrained assignments.", + "blocked_by": "A stated replacement contract and full external-edge accounting." + } + ] +} diff --git a/research/coherent-transvection-neighborhood/VERIFY.json b/research/coherent-transvection-neighborhood/VERIFY.json new file mode 100644 index 0000000000..1ab349e108 --- /dev/null +++ b/research/coherent-transvection-neighborhood/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": "Exact constrained triple neighborhoods, fibers, literal edge conjugations, mutation controls and source-bound generated receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same mathematical replay with assertions disabled; checks use explicit exceptions." + } + ] +} diff --git a/research/coherent-transvection-neighborhood/verify.py b/research/coherent-transvection-neighborhood/verify.py new file mode 100644 index 0000000000..dafbe2eb6d --- /dev/null +++ b/research/coherent-transvection-neighborhood/verify.py @@ -0,0 +1,387 @@ +#!/usr/bin/env python3 +"""Exact cycle-constrained binary chart neighborhoods. Standard library only.""" + +import argparse +from collections import Counter +import hashlib +from itertools import product +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def basis(vectors, width): + """Canonical reduced basis, with decreasing pivot positions.""" + rows = [0] * width + for vector in vectors: + value = vector + for pivot in range(width - 1, -1, -1): + if value >> pivot & 1 and rows[pivot]: + value ^= rows[pivot] + if value: + pivot = value.bit_length() - 1 + rows[pivot] = value + for other in range(width): + if other != pivot and rows[other] >> pivot & 1: + rows[other] ^= value + return tuple(row for row in reversed(rows) if row) + + +def span(rows): + values = [0] + for row in rows: + values += [value ^ row for value in values] + return frozenset(values) + + +def pairing(left, right, n): + mask = (1 << n) - 1 + return (((left & mask) & (right >> n)).bit_count() + + ((right & mask) & (left >> n)).bit_count()) & 1 + + +def transvect(value, axis, n): + return value ^ (axis if pairing(value, axis, n) else 0) + + +def kernel(equations, width): + reduced = basis(equations, width) + pivots = {row.bit_length() - 1 for row in reduced} + answer = [] + for free in range(width): + if free not in pivots: + value = 1 << free + for row in reduced: + if row >> free & 1: + value |= 1 << (row.bit_length() - 1) + answer.append(value) + return tuple(answer) + + +def combine(coefficients, rows): + value = 0 + for index, row in enumerate(rows): + if coefficients >> index & 1: + value ^= row + return value + + +def validate_basis(rows, width, expected=None): + require(isinstance(rows, tuple) and len(rows) <= width, "basis size/type") + require(all(type(x) is int and 0 < x < 1 << width for x in rows), + "basis vector range") + require(len(basis(rows, width)) == len(rows), "dependent basis") + require(expected is None or len(rows) == expected, "basis dimension") + + +def intersection_basis(n, charts, allowed): + """B=A intersect all charts, using L=L-perp and coefficient kernels.""" + equations = [] + for chart in charts: + for vector in chart: + equations.append(sum(pairing(axis, vector, n) << j + for j, axis in enumerate(allowed))) + return basis((combine(c, allowed) for c in kernel(equations, len(allowed))), + 2 * n) + + +def representatives(n, allowed, common): + """One or two axes per nonzero coset of B in A; no endpoint enumeration.""" + extended = basis(common, 2 * n) + complement = [] + for axis in allowed: + candidate = basis((*extended, axis), 2 * n) + if len(candidate) > len(extended): + complement.append(axis) + extended = candidate + answer = [] + for coefficients in range(1, 1 << len(complement)): + axis = combine(coefficients, complement) + answer.append(axis) + partner = next((b for b in common if pairing(axis, b, n)), None) + if partner is not None: + answer.append(axis ^ partner) + return tuple(answer) + + +def neighborhood(n, charts, allowed): + """Validated public enumerator, bounded to n<=9 and at most 64 charts.""" + require(type(n) is int and 1 <= n <= 9, "n must be in 1..9") + require(isinstance(charts, tuple) and 1 <= len(charts) <= 64, + "nonempty chart tuple of size at most 64 required") + validate_basis(allowed, 2 * n) + for chart in charts: + validate_basis(chart, 2 * n, n) + require(all(pairing(x, y, n) == 0 for x in chart for y in chart), + "nonisotropic chart") + common = intersection_basis(n, charts, allowed) + equations = [sum(pairing(a, b, n) << j for j, a in enumerate(allowed)) + for b in common] + t = len(basis(equations, len(allowed))) + r = len(allowed) - len(common) + require(0 <= t <= min(r, len(common)), "pairing rank invariant") + axes = representatives(n, allowed, common) + count = (1 << (r + 1)) - (1 << (r - t)) - 1 + require(len(axes) == count, "representative count invariant") + return axes, (len(allowed), len(common), t) + + +def all_subspaces(width): + require(0 <= width <= 4, "exhaustive subspace width cap") + layers = [{frozenset({0})}] + for dimension in range(width): + following = set() + for space in layers[dimension]: + for value in range(1, 1 << width): + if value not in space: + following.add(space | frozenset(x ^ value for x in space)) + layers.append(following) + return tuple(sorted((s for layer in layers for s in layer), + key=lambda s: (len(s), tuple(sorted(s))))) + + +def literal_image(space, axis, n): + return frozenset(transvect(x, axis, n) for x in space) + + +def exhaustive_triples(n): + """All ordered triples, all allowed subspaces, and every literal axis.""" + spaces = all_subspaces(2 * n) + lags = tuple(s for s in spaces if len(s) == 1 << n + and all(pairing(x, y, n) == 0 for x in s for y in s)) + images = {(i, a): literal_image(s, a, n) + for i, s in enumerate(lags) for a in range(1 << (2 * n))} + space_bases = {s: basis(s, 2 * n) for s in spaces} + cached = {} + cases = 0 + histogram = Counter() + for indices in product(range(len(lags)), repeat=3): + charts = tuple(lags[i] for i in indices) + original = tuple(charts) + common = charts[0] & charts[1] & charts[2] + rows = tuple(space_bases[s] for s in charts) + require(span(intersection_basis(n, rows, identity(n))) == common, + "coefficient-kernel intersection mismatch") + outcomes = {a: tuple(images[i, a] for i in indices) + for a in range(1 << (2 * n))} + for allowed in spaces: + bspace = allowed & common + key = (allowed, bspace) + if key not in cached: + reps, dimensions = neighborhood(n, rows, space_bases[allowed]) + literal_t = len({tuple(pairing(a, b, n) for b in bspace) + for a in allowed}).bit_length() - 1 + require(dimensions == (len(allowed).bit_length() - 1, + len(bspace).bit_length() - 1, literal_t), + "dimension or pairing rank mismatch") + fibers = {frozenset(bspace)} + for a in allowed - bspace: + fibers.add(frozenset(a ^ b for b in bspace + if pairing(a, b, n) == 0)) + cached[key] = (reps, dimensions, fibers) + reps, dimensions, fibers = cached[key] + actual = {} + for a in allowed: + actual.setdefault(outcomes[a], set()).add(a) + changed = set(actual) - {original} + delivered = [outcomes[a] for a in reps] + require(len(delivered) == len(set(delivered)), "duplicate output") + require(set(delivered) == changed, "incomplete neighborhood") + require({frozenset(f) for f in actual.values()} == fibers, + "incorrect exact fiber law") + m, b, t = dimensions + require(len(actual) == (1 << (m - b + 1)) - (1 << (m - b - t)), + "incorrect closed count") + cases += 1 + histogram[dimensions] += 1 + return {"n": n, "lagrangians": len(lags), "allowed_subspaces": len(spaces), + "triple_subspace_cases": cases, "distinct_axis_problems": len(cached), + "parameter_histogram": [[*k, v] for k, v in sorted(histogram.items())]} + + +def map_value(columns, value): + return combine(value, columns) + + +def identity(n): + return tuple(1 << j for j in range(2 * n)) + + +def map_word(n, word): + columns = identity(n) + for axis in word: + columns = tuple(transvect(x, axis, n) for x in columns) + return columns + + +def compose(left, right): + return tuple(map_value(left, x) for x in right) + + +def cycle_axes(n, transports, edges): + """Root axes satisfying R_v a = S_e R_u a on every declared edge.""" + require(type(n) is int and 1 <= n <= 9, "cycle n range") + require(isinstance(transports, tuple) and isinstance(edges, tuple) + and 1 <= len(transports) <= 64 and len(edges) <= 128, "graph size") + require(all(isinstance(edge, tuple) and len(edge) == 3 for edge in edges), + "edge shape") + require(transports[0] == identity(n), "root transport must be identity") + for columns in (*transports, *(edge[2] for edge in edges)): + validate_basis(columns, 2 * n, 2 * n) + require(all(pairing(columns[i], columns[j], n) + == pairing(1 << i, 1 << j, n) + for i in range(2 * n) for j in range(2 * n)), + "nonsymplectic transport") + equations = [] + for u, v, operator in edges: + require(type(u) is int and type(v) is int + and 0 <= u < len(transports) and 0 <= v < len(transports), + "edge vertex range") + other = compose(operator, transports[u]) + differences = tuple(x ^ y for x, y in zip(transports[v], other)) + for bit in range(2 * n): + equations.append(sum(((x >> bit) & 1) << j + for j, x in enumerate(differences))) + return kernel(equations, 2 * n) + + +def graph_controls(): + n = 2 + ident = identity(n) + root_maps = (ident, map_word(n, (1, 4)), map_word(n, (2, 8, 3))) + inverse_one = map_word(n, (4, 1)) + inverse_two = map_word(n, (3, 8, 2)) + total = 0 + dimensions = Counter() + for h1 in range(1 << (2 * n)): + for h2 in range(1 << (2 * n)): + chord = compose(root_maps[2], compose(map_word(n, (h1,)), inverse_one)) + back = compose(map_word(n, (h2,)), inverse_two) + edges = ((0, 1, root_maps[1]), (0, 2, root_maps[2]), + (1, 2, chord), (2, 0, back)) + allowed = span(cycle_axes(n, root_maps, edges)) + direct = set() + for a in range(1 << (2 * n)): + axes = tuple(map_value(r, a) for r in root_maps) + coherent = all(axes[v] == map_value(s, axes[u]) + for u, v, s in edges) + literal = all(compose(map_word(n, (axes[v],)), s) + == compose(s, map_word(n, (axes[u],))) + for u, v, s in edges) + require(coherent == literal, "literal conjugation mismatch") + if literal: + direct.add(a) + total += 1 + require(allowed == direct, "cycle kernel mismatch") + dimensions[len(basis(allowed, 2 * n))] += 1 + return {"graphs": 256, "literal_axis_tests": total, + "allowed_dimension_histogram": sorted(dimensions.items())} + + +def sharp_fixtures(): + n = 3 + disjoint = ((1, 2, 4), (1, 16, 32), (8, 2, 32)) + common = ((1, 2, 4), (1, 16, 32), (1, 2 ^ 16, 4 ^ 32)) + require(all(len(span(x) & span(y)) == 2 + for charts in (disjoint, common) + for i, x in enumerate(charts) for y in charts[i + 1:]), + "pairwise-distance fixture") + counts = [] + for charts in (disjoint, common): + reps, parameters = neighborhood(n, charts, identity(n)) + spaces = tuple(span(c) for c in charts) + actual = {tuple(literal_image(s, a, n) for s in spaces) + for a in range(1 << (2 * n))} - {spaces} + require(len(actual) == len(reps), "triple fixture literal count") + counts.append({"m_b_t": parameters, "changed_tuples": len(reps)}) + require([x["changed_tuples"] for x in counts] == [63, 47], + "pairwise data does not determine tuple count") + allowed = tuple(x for x in identity(n) if x != 8) + reps, parameters = neighborhood(n, common, allowed) + require(len(reps) == 15 and parameters == (5, 1, 0), "cycle restriction fixture") + return {"same_pairwise_distances": counts, + "one_cycle_constraint": {"m_b_t": parameters, "changed_tuples": len(reps)}} + + +def rejection_controls(): + good = ((1, 2), (4, 8), (1 ^ 4, 2 ^ 8)) + calls = ( + lambda: neighborhood(0, good, (1,)), + lambda: neighborhood(10, good, (1,)), + lambda: neighborhood(2, (), (1,)), + lambda: neighborhood(2, good, (1, 1)), + lambda: neighborhood(2, good, (16,)), + lambda: neighborhood(2, ((1, 4),), (1,)), + lambda: neighborhood(2, ((1,),), (1,)), + lambda: cycle_axes(2, (identity(2),), ((0, 1, identity(2)),)), + lambda: cycle_axes(2, (identity(2),), ((0, 0, (1, 2, 4, 9)),)), + lambda: cycle_axes(2, (identity(2),), ((0, 0),)), + lambda: cycle_axes(2, (identity(2),), ((0, 0, identity(2)),) * 129), + ) + for call in calls: + try: + call() + except ValueError: + continue + raise ValueError("invalid input accepted") + return len(calls) + + +def mutation_controls(): + n = 2 + chart = frozenset({0, 1, 2, 3}) + charts = ((1, 2),) * 3 + reps, parameters = neighborhood(n, charts, identity(n)) + target = {literal_image(chart, a, n) for a in range(16)} - {chart} + first_only = tuple(a for a in reps if a in (4, 8, 12)) + require({literal_image(chart, a, n) for a in first_only} != target, + "omitted second coset representative survived") + raw = [literal_image(chart, a, n) for a in range(16) if a not in chart] + require(len(raw) != len(set(raw)), "unquotiented axes survived") + require(parameters == (4, 2, 2) and len(reps) != (1 << 2) - 1, + "omitted pairing-rank correction survived") + require(chart in {literal_image(chart, a, n) for a in (*reps, 0)}, + "trivial outcome contamination survived") + restricted = ((1, 2, 4), (1, 16, 32), (1, 18, 36)) + axes, _ = neighborhood(3, restricted, (1, 2, 4, 16, 32)) + require(len(axes) == 15 and len(axes) != (1 << 6) - (1 << 4) - 1, + "unrestricted ambient formula survived") + return ["omit-second-representative", "omit-axis-quotient", "omit-pairing-rank", + "include-fixed-outcome", "ignore-allowed-axis-space"] + + +def receipt(): + package = Path(__file__).resolve().parent + files = ("verify.py", "README.md", "TASK.json", "SOURCES.json", "VERIFY.json") + return { + "schema": "coherent-transvection-neighborhood/v1", + "claim_type": "scoped proof with finite exact corroboration", + "source_sha256": {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in files}, + "exhaustive": [exhaustive_triples(n) for n in (1, 2)], + "graph": graph_controls(), "sharp_fixtures": sharp_fixtures(), + "rejection_controls": rejection_controls(), "mutation_controls": mutation_controls(), + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-receipt", type=Path) + args = parser.parse_args() + actual = json.loads(json.dumps(receipt(), sort_keys=True)) + if args.write_receipt is not None: + args.write_receipt.write_text(json.dumps(actual, indent=2, sort_keys=True) + "\n") + else: + expected = json.loads(Path(__file__).with_name("RESULT.json").read_text()) + require(actual == expected, "receipt or source hash mismatch") + count = sum(row["triple_subspace_cases"] for row in actual["exhaustive"]) + print(f"PASS_COHERENT_TRANSVECTION_NEIGHBORHOOD cases={count} " + f"literal_graph_axes={actual['graph']['literal_axis_tests']}") + + +if __name__ == "__main__": + main()