diff --git a/research/diagonal-pair-five-call-collisions/PROOF.md b/research/diagonal-pair-five-call-collisions/PROOF.md new file mode 100644 index 0000000000..75a4586f3a --- /dev/null +++ b/research/diagonal-pair-five-call-collisions/PROOF.md @@ -0,0 +1,151 @@ +# A cancellation certificate for the five-call diagonal-pair obstruction + +## Statement and scope + +Let G be any group, L any set of group labels, and a,b distinct elements, +neither expressible as a product of zero, one or two labels from L. Over +F2[G], let D_N(g) = (I-N) + [g]N, where N is a rank-one idempotent 2 by 2 +matrix over F2 and g belongs to L. Then **no product of at most five calls is +diag([a],[b])**. + +This is a computer-assisted theorem: the written argument below proves that +an actual realization survives the finite collision relaxation; the registered +exact verifier exhausts and rejects that relaxation. It is not a handwritten +classification of all projector tuples, a proof-kernel result, a finite-group +sample, or a theorem for other fields or widths. + +In particular, when a=xyx and b=yxy satisfy the stated shortest-word and +distinctness hypotheses for L={x,y}, the minimum is exactly six. The upper +bound is D_E00(x) D_E00(y) D_E00(x) D_E11(y) D_E11(x) D_E11(y). +This is the formal register model of Wentao Li (#4089), as used by Nick +Petalas (#6038) and Josie Elliston (#6048). No native tariff, supplier or +multiplication bound is inferred. + +## Free scalar changes of basis + +The stated product form also covers arbitrary invertible scalar basis changes +between paid calls. Write such a circuit as + + S0 D_N1(g1) S1 ... D_Nk(gk) Sk, + Si in GL_2(F2). + +Let Ci=S0 ... S_(i-1). The identity S D_N(g) S^-1 = D_(S N S^-1)(g) +moves each scalar factor to the right, giving + + D_(C1 N1 C1^-1)(g1) ... D_(Ck Nk Ck^-1)(gk) S, + S=S0 ... Sk. + +Conjugation preserves rank-one idempotence, so every resulting projector is +in the six-element inventory. The group-algebra augmentation [g] -> 1 sends +every paid factor to I and sends diag([a],[b]) to I. Thus any successful +circuit has S=I. Free scalar changes of basis therefore add no missing +terminal factor or extra cases. This normalization does not admit free +address-dependent maps, clean auxiliary registers, COPY or ERASE. + +## The missing group implication + +Write the chronological labels of a k-call candidate as g_1,...,g_k. They +are positional symbols, not presumed distinct. For a subset U of positions, +let w_U be its increasing sequence and g_U its group product. If two such +sequences have a common prefix p, then + + g_(pu) = g_(pv) if and only if g_u = g_v. + +The same equivalence holds for a common suffix. These are cancellation and +multiplication in G; they hold in every group, including groups with torsion +and arbitrary relations. In particular inserting one nonidentity letter +between a fixed prefix and suffix cannot preserve the group element. +The certificate uses both implications, only when all sequences involved +are chronological subsets of the candidate. It does not presume that these +rules decide the word problem. + +A concrete five-call tuple has projectors, in row-major bit encoding, + + (1,5,5,3,10) = (E00, [[1,0],[1,0]], [[1,0],[1,0]], + [[1,1],[0,0]], [[0,1],[0,1]]). + +Its matrix coefficients are + + T00 = [g1 g2 g3 g4] + T01 = [g1 g2 g3 g4] + [g1 g2 g3 g5] + T10 = [g4] + [g2 g3 g4] + T11 = [g4] + [g2 g3 g5] + [g2 g3 g4]. + +The required zero T10 forces g4=g2 g3 g4, hence g2 g3=e. Consequently +T00=[g1 g4], so a has a two-label expression, contrary to the hypothesis. +Separate choices of cancellation classes for different coefficients miss +this shared implication. The finite certificate propagates it jointly. + +## Why the finite relaxation contains every realization + +Drop identity-labelled calls first. Therefore all remaining g_i are +nonidentity and k is still at most five. Expand the product exactly as + + product_i D_Ni(gi) = sum_U [g_U] P_U, + P_U = product_i (N_i if i in U else I-N_i), + +with every product in increasing position order. Each of the four matrix +entries gives an equation over F2[G]. Move [a] into the 00 equation and [b] +into the 11 equation. Every equation must now be zero. + +The solver has one node for each subset U and two extra nodes A,B for a,b. +A partition stores only equalities forced or chosen so far. Initially all +nodes are separate. A genuine realization supplies a coarser partition by +actual group value. Every solver step preserves at least one branch +compatible with that realization: + +1. **Cancellation closure.** For every common-prefix or common-suffix rule, + if its premise nodes have been equated, equate its conclusion nodes. + The group equivalences above justify this. The reverse rules are valid + multiplication by the common prefix or suffix. +2. **Forbidden equalities.** Reject if the empty subset equals a singleton, + if A=B, or if A or B equals a subset of size at most two. These contradict + respectively g_i != e, a != b, or the shortest-label hypothesis. +3. **Parity equations.** Replace each equation node by its current partition + class, retaining precisely classes with odd multiplicity. An actual + group-value class must occur evenly because the elements [g] form a + basis of F2[G]. If exactly two classes remain, their equality is forced. + If an odd number remain, no partition into even multiplicities exists. +4. **Exhaustive partner branching.** Otherwise choose the first class in a + shortest nonempty residual equation. In any actual completion its + group-value class has even multiplicity, so at least one of the other + remaining classes has that same value. Branch over every such partner + and equate them. At least one branch retains the actual realization. + +Every branch strictly merges two classes; closure also only merges classes. +Thus the search terminates. It may accept partitions unrealizable by groups, +because it omits many group implications, but this only weakens a rejection. +If every branch rejects, no actual realization of that projector tuple +exists. The node cap fails the verifier rather than declaring a rejection. + +## Finite coverage + +A nonzero rank-one idempotent over F2 is u v^T with v^T u=1. The six 2 by 2 +possibilities have row-major bit encodings 1,3,5,8,10,12. The verifier obtains +them by idempotence and trace one, then independently checks the outer-product +inventory. It evaluates all 6^k tuples for each k=0,...,5, without identifying +or omitting symmetry classes. There are 9,331 tuples in total. + +Every label sequence, in every group and every label set, is covered by the +positional-symbol argument for its projector tuple. No assignment of x,y, +no finite group, and no determinant/degree invariant is enumerated. The +computed zero survivors, together with the sound relaxation argument, +establish the scoped theorem. + +## Controls and remaining proof obligations + +The six-call direct construction is checked by exact free-word coefficients. +Removing cancellation reopens the four-call tuple (1,5,1,10), demonstrating +that support and coefficient parity alone do not prove the result. Relaxing +the target length hypothesis reopens the two-call tuple (E00,E11). The +explicit five-call example above is checked by the same refutation engine. +The verifier independently authenticates every generated cancellation rule as a +single common-context law, checks the displayed coefficient expansion, and +accepts the actual four- and six-call constructions in the collision solver. +It uses explicit checks, which remain active under Python -O. + +The proof still depends on the correctness and successful completion of the +small Python certificate. Independent human or proof-assistant review has +not been claimed. The six-projector inventory and characteristic-two parity +are essential scope restrictions; extension to other fields or widths +requires new reasoning. diff --git a/research/diagonal-pair-five-call-collisions/README.md b/research/diagonal-pair-five-call-collisions/README.md new file mode 100644 index 0000000000..cebd2e061c --- /dev/null +++ b/research/diagonal-pair-five-call-collisions/README.md @@ -0,0 +1,69 @@ +# Five-call diagonal-pair collision obstruction + +**All-group computer-assisted obstruction, restricted to width two over F2. +No new kappa.** In the formal rank-one-idempotent call model, a diagonal pair +of distinct targets, each requiring at least three labels, needs at least six +calls. For (xyx,yxy) satisfying these hypotheses, the direct six-call word +meets the bound. + +[PROOF.md](PROOF.md) gives the exact scope, a symbolic five-call cancellation +example, and the soundness argument for the exhaustive finite refutation. +[verify.py](verify.py) checks every one of the 9,331 projector tuples of +length zero through five. It propagates common-prefix/suffix cancellation +jointly through the four group-algebra coefficient equations. Free invertible scalar basis changes are normalized by conjugation and +augmentation in the proof. The groups and label alphabets remain arbitrary; this is not evidence extrapolated +from a finite group census. + +This resolves the width-two/F2 portion of Josie Elliston's #6048 open +question 1. That package's support-only relaxation admitted 20 four-call +and 938 five-call projector tuples. Its arbitrary subset-class assignment +omitted joint group-word consistency. This successor adds cancellation and +all coefficient equations, rather than repeating the free-group degree +control. Nick Petalas's #6038 established the earlier four-call xy/yx result. + +## Reproduce + +Standard-library Python 3.12; approximately two seconds per direct run: + +```sh +python3 -B research/diagonal-pair-five-call-collisions/verify.py +python3 -O -B research/diagonal-pair-five-call-collisions/verify.py +python3 -B scripts/research_package.py --package research/diagonal-pair-five-call-collisions +``` + +Expected marker: `PASS_DIAGONAL_PAIR_FIVE_CALL_COLLISIONS`, with zero survivors +at every length. Registered controls include the six-call exact endpoint, +a reopened four-call support-only instance when cancellation is removed, +and a reopened two-call instance when short targets are allowed. Independent +controls authenticate every generated context rule and require the collision +solver itself to accept the known four- and six-call constructions. + +The package has no runtime source dependencies. Exact predecessor proof and +README pins are provenance in SOURCES.json; their bytes are not imported or +modified. The verifier also runs directly in a Git-free source export. + +## Open next questions + +1. Does the six-call floor hold at larger widths over F2? It would remove the + two-register restriction. First inspect whether the parity refutation can + be replaced by a rank/corner argument; the six-projector inventory does + not cover larger matrices. +2. Does it hold in odd characteristic or F4? It would address the remaining + field scope of #6048's question. First derive coefficient-class constraints + with nonbinary weights; even pairing is specific to F2 and is not valid + unchanged over those fields. + +Neither question authorizes another construction round or certifies a native +implementation. Conversion, restoration, tariffs, whole callers and the +selected multiplication frontier are outside this result. + +## Credit + +Prepared by JoyboyBrian with substantial OpenAI Codex assistance, Apache-2.0. +Josie Elliston (#6048, substantial Claude assistance) supplied the longer-pair +question, support-only counterexamples and group-free proof approach; Nick +Petalas (#6038) supplied the preceding all-group xy/yx theorem and corner +method; Wentao Li (#4089/#4093) supplied the rank-one-idempotent group-algebra +model, following Cinna Davis's A5 target (#2246). Their broader results are +not re-audited here. Source heads are pinned, and no frozen predecessor is +changed. diff --git a/research/diagonal-pair-five-call-collisions/SOURCES.json b/research/diagonal-pair-five-call-collisions/SOURCES.json new file mode 100644 index 0000000000..c2b6406a81 --- /dev/null +++ b/research/diagonal-pair-five-call-collisions/SOURCES.json @@ -0,0 +1,46 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/conjugate-pair-group-free-audit/README.md", + "usage": "provenance", + "pin": "head:518cd2a7880f94b80c9c93aad304a7f041def647:research/conjugate-pair-group-free-audit/README.md", + "git_blob": "c0ae47bf6c566c69466e150661641d61fd9ff636", + "sha256": "3adf65a79d27ea7a60ec8978fa6b45f75d65c07c3aed019080b64431078f28f3" + }, + { + "path": "research/conjugate-pair-group-free-audit/PROOF.md", + "usage": "provenance", + "pin": "head:518cd2a7880f94b80c9c93aad304a7f041def647:research/conjugate-pair-group-free-audit/PROOF.md", + "git_blob": "a92cbe6f25408cd5ff1e4f820963d44cabc9f362", + "sha256": "a37a1bc0bd306a94c148c703c43e41ee4f8d90fcf009cfeb7cee8b2a31fa600a" + }, + { + "path": "research/conjugate-pair-every-group/README.md", + "usage": "provenance", + "pin": "head:0cee0e104b68ce6f06bf84af03f46ac30680e64c:research/conjugate-pair-every-group/README.md", + "git_blob": "47bb74c1399e2bed48afd5be200e53223bb7e4c0", + "sha256": "9ddac65a112890de4d098a5387209927d753cbdb68fa3a5d064d6dfe717b9a1a" + }, + { + "path": "research/conjugate-pair-every-group/PROOF.md", + "usage": "provenance", + "pin": "head:0cee0e104b68ce6f06bf84af03f46ac30680e64c:research/conjugate-pair-every-group/PROOF.md", + "git_blob": "46d33fc3b993a53435bf8c450421a5310e20a8a0", + "sha256": "414b5f88f7fd24d7066b03efa371bdf7a28fbed22a8c36fd78a1073b469aafd2" + } + ] +} diff --git a/research/diagonal-pair-five-call-collisions/TASK.json b/research/diagonal-pair-five-call-collisions/TASK.json new file mode 100644 index 0000000000..da30f03b65 --- /dev/null +++ b/research/diagonal-pair-five-call-collisions/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove or refute the five-call diagonal-pair obstruction using genuine group-word collisions, initially width two over F2.", + "scope_change_reason": "Explicit preclaimed handoff #6048 open question 1 replaces the generic register-model task; formal group-algebra obstruction only, no native implementation.", + "bottleneck_link": "A scoped lower bound on sharing longer noncommutative diagonal targets; no primitive saving or complete BIT supplier is claimed.", + "budget_minutes": 30, + "stop_rule": "One written collision lemma or exact counterexample; bounded exhaustive projector certificate only, no finite-group inference.", + "outcome": "completed", + "evidence": "PROOF.md and registered verify.py: all 9331 tuples at lengths 0 through 5 rejected; exact six-call endpoint and weakened-hypothesis controls.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance.", + "open_questions": [ + { + "question": "Does the six-call floor extend to larger widths over F2?", + "why_it_matters": "Removes the two-register restriction.", + "first_step": "Replace the six-projector case split by a rank/corner argument.", + "blocked_by": "Finite projector inventory only covers width two." + }, + { + "question": "Does the six-call floor extend to odd characteristic or F4?", + "why_it_matters": "Addresses remaining field scope of predecessor question.", + "first_step": "Derive weighted coefficient-class constraints.", + "blocked_by": "Even pairing is specific to F2." + } + ] +} diff --git a/research/diagonal-pair-five-call-collisions/VERIFY.json b/research/diagonal-pair-five-call-collisions/VERIFY.json new file mode 100644 index 0000000000..35e9a200ff --- /dev/null +++ b/research/diagonal-pair-five-call-collisions/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "All 9331 projector tuples, common-prefix/suffix collision closure, exact six-call endpoint, missing-cancellation and short-target controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "All 9331 projector tuples, common-prefix/suffix collision closure, exact six-call endpoint, missing-cancellation and short-target controls." + } + ] +} diff --git a/research/diagonal-pair-five-call-collisions/verify.py b/research/diagonal-pair-five-call-collisions/verify.py new file mode 100644 index 0000000000..8710e77059 --- /dev/null +++ b/research/diagonal-pair-five-call-collisions/verify.py @@ -0,0 +1,185 @@ +#!/usr/bin/env python3 +"""Exact all-group collision refutation; standard library, no group sampling.""" +import itertools +import json + +IDENTITY = 9 + + +def require(condition, message): + if not condition: + raise SystemExit('FAIL ' + message) + + +def multiply(a, b): + return sum((sum(((a >> (2*i+t)) & 1) * ((b >> (2*t+j)) & 1) + for t in range(2)) % 2) << (2*i+j) + for i in range(2) for j in range(2)) + + +PROJECTORS = tuple(n for n in range(16) + if multiply(n, n) == n and ((n & 1) ^ ((n >> 3) & 1))) + + +def expand(projectors): + terms = {0: IDENTITY} + for position, n in enumerate(projectors): + terms = {mask: product for old, coefficient in terms.items() + for mask, product in ((old, multiply(coefficient, IDENTITY ^ n)), + (old | (1 << position), multiply(coefficient, n)))} + return terms + + +def cancellation_rules(k): + words = [tuple(i for i in range(k) if mask >> i & 1) for mask in range(1 << k)] + index = {word: mask for mask, word in enumerate(words)} + rules = set() + for a, u in enumerate(words): + for b, v in enumerate(words[:a]): + prefix = suffix = 0 + while prefix < min(len(u), len(v)) and u[prefix] == v[prefix]: + prefix += 1 + while suffix < min(len(u), len(v)) and u[-1-suffix] == v[-1-suffix]: + suffix += 1 + for left, right in ((u[prefix:], v[prefix:]), + (u[:-suffix], v[:-suffix]) if suffix else (u, v)): + c, d = index[left], index[right] + if (a, b) != (c, d): + rules.add((a, b, c, d)) + rules.add((c, d, a, b)) + return tuple(sorted(rules)) + + +class CollisionProblem: + def __init__(self, k, cancellation=True, minimum=3): + self.k = k + self.target_a = 1 << k + self.target_b = self.target_a + 1 + self.rules = cancellation_rules(k) if cancellation else () + self.short = tuple(mask for mask in range(1 << k) if mask.bit_count() < minimum) + self.nodes = 0 + + def solve(self, projectors): + require(len(projectors) == self.k, 'wrong word length') + terms = expand(projectors) + equations = tuple(tuple(mask for mask, value in terms.items() if value >> entry & 1) + + ((self.target_a,) if entry == 0 else + (self.target_b,) if entry == 3 else ()) for entry in range(4)) + return self.search(equations, list(range((1 << self.k) + 2))) + + def search(self, equations, partition): + self.nodes += 1 + require(self.nodes <= 200000, 'explicit search-node cap exceeded') + parent = partition[:] + + def root(a): + while parent[a] != a: + a = parent[a] + return a + + def union(a, b): + a, b = root(a), root(b) + if a == b: + return False + parent[max(a, b)] = min(a, b) + return True + + while True: + changed = False + for a, b, c, d in self.rules: + if root(a) == root(b): + changed = union(c, d) or changed + if any(root(0) == root(1 << i) for i in range(self.k)): + return None + if root(self.target_a) == root(self.target_b): + return None + if any(root(target) == root(mask) for target in (self.target_a, self.target_b) + for mask in self.short): + return None + residual = [] + for equation in equations: + odd = set() + for node in equation: + node = root(node) + odd.symmetric_difference_update((node,)) + if len(odd) % 2: + return None + if len(odd) == 2: + changed = union(*odd) or changed + elif odd: + residual.append(tuple(sorted(odd))) + if not changed: + break + if not residual: + return parent + equation = min(residual, key=lambda item: (len(item), item)) + first = equation[0] + # Every true equality class has even parity, so first has a partner. + for partner in equation[1:]: + branch = parent[:] + a, b = root(first), root(partner) + branch[max(a, b)] = min(a, b) + witness = self.search(equations, branch) + if witness is not None: + return witness + return None + + +def exact_endpoint(pattern, projectors): + coefficients = {} + for mask, coefficient in expand(projectors).items(): + word = ''.join(label for i, label in enumerate(pattern) if mask >> i & 1) + coefficients[word] = coefficients.get(word, 0) ^ coefficient + return {word: value for word, value in coefficients.items() if value} + + +def main(): + require(PROJECTORS == (1, 3, 5, 8, 10, 12), 'rank-one projector inventory') + # Independent outer-product characterization, not a second trace filter. + outer = {sum(((u >> i) & 1)*((v >> j) & 1) << (2*i+j) + for i in range(2) for j in range(2)) + for u in (1, 2, 3) for v in (1, 2, 3) if (u & v).bit_count() % 2} + require(set(PROJECTORS) == outer, 'outer-product inventory mismatch') + require(multiply(3, 5) != multiply(5, 3), 'matrix order control') + # Independently authenticate every generated rule as a single context law. + for k in range(7): + words = [tuple(i for i in range(k) if mask >> i & 1) for mask in range(1 << k)] + for a, b, c, d in cancellation_rules(k): + valid = False + for u, v, s, t in ((words[a], words[b], words[c], words[d]), + (words[c], words[d], words[a], words[b])): + for split in range(len(u) + 1): + context = u[:split] + valid |= u == context + s and v == context + t + context = u[split:] + valid |= u == s + context and v == t + context + require(valid, 'invalid cancellation rule') + require(CollisionProblem(6).solve((1, 1, 1, 8, 8, 8)) is not None, + 'solver rejected six-call true endpoint') + require(CollisionProblem(4, minimum=2).solve((1, 1, 8, 8)) is not None, + 'solver rejected preceding four-call true endpoint') + require({m: v for m, v in expand((1, 5, 5, 3, 10)).items() if v} + == {8: 12, 14: 12, 15: 3, 22: 8, 23: 2}, + 'written collision example coefficients') + require(exact_endpoint('xyxyxy', (1, 1, 1, 8, 8, 8)) == {'xyx': 1, 'yxy': 8}, + 'six-call positive endpoint') + relaxed = CollisionProblem(4, cancellation=False) + require(relaxed.solve((1, 5, 1, 10)) is not None, 'missing-cancellation control did not reopen') + shortened = CollisionProblem(2, minimum=1) + require(shortened.solve((1, 8)) is not None, 'short-target control did not reopen') + require(CollisionProblem(5).solve((1, 5, 5, 3, 10)) is None, + 'written five-call collision example') + results = [] + for k in range(6): + problem = CollisionProblem(k) + tested = 0 + for projectors in itertools.product(PROJECTORS, repeat=k): + require(problem.solve(projectors) is None, 'surviving collision relaxation ' + str(projectors)) + tested += 1 + require(tested == 6**k, 'incomplete projector enumeration') + results.append({'calls': k, 'tuples': tested, 'nodes': problem.nodes, 'survivors': 0}) + print('PASS_DIAGONAL_PAIR_FIVE_CALL_COLLISIONS ' + json.dumps(results, sort_keys=True)) + + +if __name__ == '__main__': + main()