diff --git a/research/p104-a2-packing-maximum/PACKING.json b/research/p104-a2-packing-maximum/PACKING.json new file mode 100644 index 0000000000..8d46b95d4e --- /dev/null +++ b/research/p104-a2-packing-maximum/PACKING.json @@ -0,0 +1,177 @@ +{ + "schema_version": 1, + "triangles": [ + [ + 0, + 45, + 67 + ], + [ + 1, + 2, + 95 + ], + [ + 3, + 40, + 65 + ], + [ + 4, + 33, + 73 + ], + [ + 5, + 37, + 62 + ], + [ + 6, + 16, + 88 + ], + [ + 7, + 29, + 66 + ], + [ + 8, + 28, + 69 + ], + [ + 9, + 31, + 59 + ], + [ + 10, + 50, + 75 + ], + [ + 11, + 57, + 77 + ], + [ + 14, + 15, + 99 + ], + [ + 17, + 55, + 72 + ], + [ + 18, + 47, + 71 + ], + [ + 19, + 35, + 39 + ], + [ + 20, + 23, + 56 + ], + [ + 21, + 38, + 70 + ], + [ + 22, + 27, + 94 + ], + [ + 24, + 46, + 82 + ], + [ + 25, + 34, + 86 + ], + [ + 26, + 41, + 79 + ], + [ + 30, + 32, + 90 + ], + [ + 36, + 49, + 78 + ], + [ + 42, + 48, + 91 + ], + [ + 43, + 44, + 102 + ], + [ + 51, + 60, + 85 + ], + [ + 52, + 61, + 92 + ], + [ + 53, + 64, + 93 + ], + [ + 63, + 68, + 96 + ], + [ + 74, + 76, + 100 + ], + [ + 80, + 83, + 97 + ], + [ + 81, + 84, + 101 + ], + [ + 87, + 89, + 103 + ] + ], + "uncovered": [ + 12, + 13, + 54, + 58, + 98 + ] +} diff --git a/research/p104-a2-packing-maximum/README.md b/research/p104-a2-packing-maximum/README.md new file mode 100644 index 0000000000..91f0183c65 --- /dev/null +++ b/research/p104-a2-packing-maximum/README.md @@ -0,0 +1,145 @@ +# The P104 A2-triangle packing maximum is 33 + +A packing of pairwise disjoint A2 triangles in the pinned 104-port set has at +most **33 triangles**. The explicit [packing](PACKING.json) attains this bound, +covering 99 ports and leaving five. Thus at least five partners require another +scheme in the disjoint-triangle routing architecture of +[Matarener's PR6217](https://github.com/CrocSwap/integer-mult-bounds/pull/6217). +This is a scoped proof with a finite attainment certificate. It supplies no +routing word, supplier admission, new kappa or complete multiplication theorem. + +PR6217 reports a 33-triangle packing and explicitly leaves its maximality open. +The new contribution is the parity obstruction to 34, which settles that +question. The witness here was found separately; no predecessor packing or +routing theorem was audited. This contribution was produced by Nick Petalas. + +## Proof + +Write `u = 511`, the all-ones vector in `F_2^9`, and identify an integer port +label with its nine bits. Use the source's A8-coordinate root `r(q)`. For a +weight-three port, `x(q) = 3r(q)` has coordinate 2 on its support and -1 +off it. For a weight-seven port with zero positions `a < b`, it is +`x(q) = 3(e_a-e_b)`. Both cases give the same coordinatewise identity: + +```text +x(q) mod 2 = u XOR q. +``` + +For an A2 triangle, choose signs so that one of its roots is a signed sum of +the other two. This also follows directly from its norm-two Gram matrix. If +`A = `, `B = `, `C = ` are signs with `ABC = -1`, +then + +```text +||r_c - C r_a - B r_b||^2 = 2 + 2ABC = 0. +``` + +Reduce the resulting integer relation among the three `x` vectors modulo +two. Signs disappear, and the displayed coordinate identity gives + +```text +q_a XOR q_b XOR q_c = u for every A2 triangle. +``` + +The XOR of the 104 distinct labels in the pinned port list is zero. This is +one finite input calculation, authenticated and performed by `verify.py`. +Suppose 34 disjoint triangles existed. They would cover 102 ports, whose XOR +would be the XOR of 34 copies of `u`, hence zero. The two remaining labels +would consequently XOR to zero. They would be equal, contradicting their +distinctness. The counting bound already excludes 35 triangles, so the +maximum is at most 33. + +The certificate lists 33 triangles by zero-based index in the pinned port +list. The checker verifies disjointness and every signed root identity over +the integers. It also checks the nonconflicting binary labels and the A2 +Gram signs. It leaves precisely indices `12, 13, 54, 58, 98`, whose labels +are `73, 265, 152, 200, 239`. This proves attainment and finishes the proof. +The upper bound covers every possible A2 triangle, by the argument above; +it does not rely on an enumeration or a solver's infeasibility verdict. + +The underlying parity argument is classical: if `6m+2` distinct binary +labels have total XOR zero, disjoint triples with one common XOR cannot +cover all but two labels. A putative `2m` triples would have total XOR zero, +forcing the remaining pair to coincide. The contribution here applies +this argument through the root/port parity identity to resolve the stated +P104 packing question. + +## Evidence and reproduction + +Only the port list is a live external input. Its path, Git blob and SHA256 +are in [SOURCES.json](SOURCES.json), pinned at canonical main +`a5bff3bf133e482541c09eba4e773884bdb2b1b7`. The verifier imports no predecessor +code and requires only the Python standard library. It does not enumerate +or recount PR6217's triangle catalogue or replay its routing claims. + +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/p104-a2-packing-maximum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/research_package.py --package research/p104-a2-packing-maximum +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/check_research_commit.py --package research/p104-a2-packing-maximum --check-source-history +``` + +Elsewhere, replace the absolute interpreter path with CPython 3.12. Both +normal and optimized modes are registered in [VERIFY.json](VERIFY.json). +The final marker is `PASS_P104_A2_PACKING_MAXIMUM`. Each direct run prints a +generated receipt with SHA256 hashes of the package and live input. No +receipt is handwritten or stored in the package. + +The checks cover all 104 root/label parity identities, the 33 attaining +triangles, all 487,200 ordered pairs of disjoint triples in the zero-XOR +eight-subsets of four-bit labels, and fifteen rejecting controls. The small +label enumeration corroborates the general parity argument independently of +the P104 geometry. It is not its universal proof. The rejecting controls +include overlapping triangles, a nontriangle, bad indices and types, a false +two-port leave, a missing triangle, duplicate ports and failed parity premises. +All mathematical checks remain enabled under `-O`. + +## Scope and engineering decisions + +The upper bound is for disjoint A2 triples in this exact port set. It does +not exclude overlapping routing schemes, different port sets, added helpers, +multistage relays or a different boundary contract. Maximality of a geometric +packing does not prove legal data delivery, dirty restoration or a favorable +complete signed invoice. The selected frontier and its five framework +assumptions are unchanged. Independent human and formal proof-kernel review +are unclaimed. No selected scientific replay, Lean or Docker build was run. + +The verifier has no recursion or subprocesses. All geometry uses nine +coordinates, 104 ports and 33 triples. The small-label loop is bounded by +`C(16,8) * C(8,3) * C(5,3) = 7,207,200` candidate iterations before filtering. +JSON inputs are limited to 64 KiB. Functions stay below 60 lines and use +explicit runtime contracts instead of removable assertions. + +Power-of-ten deviations apply to rules 3 and 9 in `verify.py`. Python's +managed runtime allocates integers and containers during checks; input sizes +and the fixed finite loops bound live state. The negative-control helper +uses only the explicitly named validator functions as call targets. Its +lifetime is one synchronous call, and every control must raise `ValueError`. +Normal and optimized warning-strict replay exercise these bounds and targets. +A fixed-storage native implementation or removal of the control helper would +be needed if hard real-time allocation or static dispatch became a requirement. + +## Open next questions + +- Can a legal wire-plus-helper program for one A2 triangle beat the complete + swarm invoice? Start with one certified triangle, arbitrary initial public + data and every physical entry, exit, sign correction and restoration charge. + A constructive program and its full bill remain missing. +- Can the five exceptional partners be handled more cheaply by an overlapping + or multistage scheme? Start with the five listed labels and name the changed + contract. This packing result supplies no implementation or cost allowance. + +Structured questions and the recorded scope change are in [TASK.json](TASK.json). +No follow-on search is part of this contribution. + +## Credit + +Matarener retains PR6217's routing question, reported 33-triangle construction +and routing lemmas, at head `6aa982f08190fb3f2bff8f4dee3eeaf0ba0412d9`. +Matarener's merged PR6166, `p104-carrier-code-uniqueness`, supplies the pinned +ports and A8-coordinate root interpretation. Ali Romman and DreamingOfClouds +retain the P104 word lineage, including PR5827, PR5907 and PR6030; the native, +caller, compiler and BIT contributions retain their existing attribution. +Root-system facts and binary parity are classical. The new maximality result, +attainment certificate and checker were produced by Nick Petalas. Apache-2.0. diff --git a/research/p104-a2-packing-maximum/SOURCES.json b/research/p104-a2-packing-maximum/SOURCES.json new file mode 100644 index 0000000000..5cdd62e1c4 --- /dev/null +++ b/research/p104-a2-packing-maximum/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "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/p104-carrier-code-uniqueness/e8/ports.json", + "usage": "input", + "git_blob": "b964c3ae2ea54d3763d74639d691ea9f5b02920e", + "sha256": "ba6a0b9cf76b7cccc1ce8b3d1aa78a4aa329b34d45aded694648f0cf43fc9fce" + }, + { + "path": "research/p104-carrier-code-uniqueness/e8/E8-PROOF.md", + "usage": "provenance", + "git_blob": "91ef08f375a93d48a852fb0d595cfe5b4cea5cd2", + "sha256": "a2ce265ea2eafc03ad1ffcfd68bc0059bbeba6370776b12a8a121c78c0840697" + } + ] +} diff --git a/research/p104-a2-packing-maximum/TASK.json b/research/p104-a2-packing-maximum/TASK.json new file mode 100644 index 0000000000..50ff760a66 --- /dev/null +++ b/research/p104-a2-packing-maximum/TASK.json @@ -0,0 +1,144 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 8, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "original_card": { + "id": "p104-side-correction", + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "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/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/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": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. 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": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "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": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "existing_checks": [ + { + "scope": "PR #4133: literal-slot defect", + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4136: uniform commutation gap", + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4140: uniform encoding gap", + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4154: fiber-tag seam mismatch", + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "status": "author-checked", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "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": "Prove that the pinned 104 P104 ports have maximum disjoint A2-triangle packing size 33, settling the maximality question in PR6217.", + "scope_change_reason": "Follow the explicit open packing question in PR6217 rather than repeat a helper split or audit. This is a geometric prerequisite for its proposed disjoint-triangle routing architecture, not a complete supplier improvement.", + "bottleneck_link": "The complex supplier binds. The proposed routing architecture needs exceptions outside disjoint A2 triangles; this result proves at least five exceptions instead of the counting lower bound of two. Physical delivery, restoration and complete signed accounting remain open.", + "budget_minutes": 60, + "stop_rule": "Ship the first exact new obstruction and a matching certificate; do not extend into routing construction.", + "outcome": "completed", + "evidence": "README.md parity proof; PACKING.json explicit 33-triangle attainment; verify.py exact standard-library checks, 487200 small-label triple-pair cases and fifteen rejecting controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can wires plus one helper per partner implement one A2 triangle more cheaply than the complete swarm invoice?", + "why_it_matters": "A packing is not a physical complex-supplier improvement.", + "first_step": "Use one certified triangle and write an arbitrary-input program with every entry, exit, sign correction and restoration charge.", + "blocked_by": "A legal program and complete paid/productive invoice are missing." + }, + { + "question": "Can an overlapping or multistage scheme handle the five exceptional partners cheaply?", + "why_it_matters": "The disjoint-triangle parity obstruction forces at least five exceptions.", + "first_step": "Start with the listed five labels and specify a changed routing boundary and optimistic complete bill.", + "blocked_by": "No physical construction or cost allowance is supplied." + } + ], + "claim_type": "scoped proof with finite attainment certificate", + "source_question": { + "pr": 6217, + "author": "Matarener", + "head": "6aa982f08190fb3f2bff8f4dee3eeaf0ba0412d9", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6217", + "question": "The best packing found has 33 A2 triangles; is it maximal?", + "dependency": "Question and root interpretation only; no pending code or routing theorem is imported." + }, + "environment": { + "python": "3.12.15", + "implementation": "CPython", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "requirements": [] + }, + "freshness": { + "upstream_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "priority_revision": 8, + "checked_utc": "2026-10-29T22:05:00Z", + "overlap": "Main README key-term and general-form searches, live open/merged PR searches, last 30 handoffs and active Discussions, 200 recent account PRs plus targeted seven-day account triangle searches. Cached helper covers 8623 main notes and 337 open PRs; its Discussion refresh timed out, so live GraphQL reads supplied separate bounded coverage. Unpublished work is outside coverage." + } +} diff --git a/research/p104-a2-packing-maximum/VERIFY.json b/research/p104-a2-packing-maximum/VERIFY.json new file mode 100644 index 0000000000..1db13d5675 --- /dev/null +++ b/research/p104-a2-packing-maximum/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-carrier-code-uniqueness/e8/ports.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Exact source hash, root/port parity, 33 disjoint A2 triangles, written-bound premises, complete four-bit local controls and fifteen rejection controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "The same certificate and rejecting controls with removable assertions disabled." + } + ] +} diff --git a/research/p104-a2-packing-maximum/verify.py b/research/p104-a2-packing-maximum/verify.py new file mode 100644 index 0000000000..1abe35278d --- /dev/null +++ b/research/p104-a2-packing-maximum/verify.py @@ -0,0 +1,184 @@ +#!/usr/bin/env python3 +"""Exact certificate checks for the P104 A2 packing maximum. Apache-2.0.""" + +import copy +import hashlib +import itertools +import json +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +PORT_PATH = "research/p104-carrier-code-uniqueness/e8/ports.json" +PORT_SHA = "ba6a0b9cf76b7cccc1ce8b3d1aa78a4aa329b34d45aded694648f0cf43fc9fce" +MASK = 511 +MAX_BYTES = 65536 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def load_json(path): + require(path.stat().st_size <= MAX_BYTES, "oversized JSON input") + raw = path.read_bytes() + require(len(raw) <= MAX_BYTES, "JSON input grew while reading") + return json.loads(raw), raw + + +def xor_sum(values): + result = 0 + for value in values: + result ^= value + return result + + +def root3(q): + """Three times the A8-coordinate root attached to the odd port q.""" + require(type(q) is int and 0 < q <= MASK, "port outside nine bits") + require(q.bit_count() in (3, 7), "port has unsupported weight") + if q.bit_count() == 3: + return tuple(2 if (q >> i) & 1 else -1 for i in range(9)) + a, b = [i for i in range(9) if not (q >> i) & 1] + return tuple(3 * (int(i == a) - int(i == b)) for i in range(9)) + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b, strict=True)) + + +def validate_ports(ports): + require(type(ports) is list and len(ports) == 104, "need 104 ports") + roots = [root3(q) for q in ports] + require(len(set(ports)) == 104, "duplicate port") + for q, root in zip(ports, roots, strict=True): + require(sum(root) == 0 and dot(root, root) == 18, "invalid root") + parity = sum((x % 2) << i for i, x in enumerate(root)) + require(parity == (MASK ^ q), "root/label parity mismatch") + require(xor_sum(ports) == 0, "total port XOR is not zero") + return roots + + +def parity_upper_bound(labels): + """Apply the written parity lemma; triangle XOR is its hypothesis.""" + require(2 <= len(labels) <= 120, "parity domain size") + require(all(type(q) is int and 0 <= q <= MASK for q in labels), "bad label") + require(len(set(labels)) == len(labels), "parity needs distinct labels") + require(len(labels) % 6 == 2, "parity needs size 6m+2") + require(xor_sum(labels) == 0, "parity needs total XOR zero") + return len(labels) // 3 - 1 + + +def validate_packing(ports, certificate): + roots = validate_ports(ports) + require(type(certificate) is dict, "packing is not an object") + require(set(certificate) == {"schema_version", "triangles", "uncovered"}, + "unexpected packing fields") + require(type(certificate["schema_version"]) is int and + certificate["schema_version"] == 1, "packing schema") + triangles = certificate["triangles"] + require(type(triangles) is list and len(triangles) == 33, "need 33 triangles") + used = set() + for triangle in triangles: + require(type(triangle) is list and len(triangle) == 3, "triangle arity") + require(all(type(i) is int and 0 <= i < 104 for i in triangle), + "triangle index") + require(triangle == sorted(set(triangle)), "triangle ordering/distinctness") + require(not used.intersection(triangle), "triangles overlap") + require(all((ports[u] & ports[v]).bit_count() % 2 == 0 + for u, v in itertools.combinations(triangle, 2)), + "conflicting ports in triangle") + a, b, c = (roots[i] for i in triangle) + ab, bc, ca = dot(a, b), dot(b, c), dot(c, a) + require(all(abs(x) == 9 for x in (ab, bc, ca)) and + ab * bc * ca == -729, "not an A2 triangle") + require(all(c[i] == (ca // 9) * a[i] + (bc // 9) * b[i] + for i in range(9)), "signed root relation") + require(xor_sum(ports[i] for i in triangle) == MASK, "triangle XOR") + used.update(triangle) + uncovered = certificate["uncovered"] + require(type(uncovered) is list and + all(type(i) is int for i in uncovered), "uncovered index types") + require(uncovered == sorted(set(range(104)) - used), "uncovered indices") + require(len(used) == 99 and len(uncovered) == 5, "coverage") + require(xor_sum(ports[i] for i in uncovered) == MASK, "uncovered XOR") + require(parity_upper_bound(ports) == len(triangles), "upper/lower bound gap") + return {"maximum_triangles": len(triangles), "covered_ports": len(used), + "minimum_uncovered": len(uncovered), "uncovered_indices": uncovered, + "uncovered_labels": [ports[i] for i in uncovered]} + + +def expect_rejection(label, function, *args): + try: + function(*args) + except ValueError: + return label + raise ValueError("control accepted: " + label) + + +def controls(ports, certificate): + rejected = [] + for label, replacement in (("duplicate triangle", certificate["triangles"][0]), + ("nontriangle", [0, 1, 2]), + ("invalid index", [0, 45, 104]), + ("boolean index", [False, 45, 67])): + bad = copy.deepcopy(certificate) + bad["triangles"][1 if label == "duplicate triangle" else 0] = replacement + rejected.append(expect_rejection(label, validate_packing, ports, bad)) + bad = copy.deepcopy(certificate) + bad["uncovered"] = [12, 13] + rejected.append(expect_rejection("false two-port leave", validate_packing, ports, bad)) + bad = copy.deepcopy(certificate) + bad["triangles"].pop() + rejected.append(expect_rejection("missing triangle", validate_packing, ports, bad)) + bad_ports = ports.copy() + bad_ports[0] = ports[1] + rejected.append(expect_rejection("duplicate port", validate_ports, bad_ports)) + for q in (True, -1, 512, 1): + rejected.append(expect_rejection("invalid root " + repr(q), root3, q)) + for labels in ([0, 1], [0, 0], [0, 1, 2, 3], [False, 0]): + rejected.append(expect_rejection("parity premise " + repr(labels), + parity_upper_bound, labels)) + return rejected + + +def local_lemma_controls(): + """An independent complete small-label check of the parity argument.""" + cases = 0 + for labels in itertools.combinations(range(16), 8): + if xor_sum(labels): + continue + for first in itertools.combinations(labels, 3): + remaining = tuple(q for q in labels if q not in first) + for second in itertools.combinations(remaining, 3): + require(xor_sum(first) != xor_sum(second), + "two disjoint equal-XOR triples in zero-XOR eight-set") + cases += 1 + require(parity_upper_bound(labels) == 1, "small parity bound") + return cases + + +def main(): + sources, _ = load_json(HERE / "SOURCES.json") + pins = [row for row in sources["files"] if row["path"] == PORT_PATH] + require(len(pins) == 1 and pins[0]["usage"] == "input" and + pins[0]["sha256"] == PORT_SHA, "port source declaration") + ports, raw = load_json(ROOT / PORT_PATH) + require(hashlib.sha256(raw).hexdigest() == PORT_SHA, "port source hash") + certificate, _ = load_json(HERE / "PACKING.json") + result = validate_packing(ports, certificate) + result["rejected_controls"] = controls(ports, certificate) + result["small_label_cases"] = local_lemma_controls() + payload = sorted(HERE.iterdir()) + require(len(payload) <= 16 and all(p.is_file() for p in payload), "payload shape") + result["sha256"] = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in payload} + result["input_sha256"] = {PORT_PATH: hashlib.sha256(raw).hexdigest()} + print(json.dumps(result, indent=2, sort_keys=True)) + print("PASS_P104_A2_PACKING_MAXIMUM") + + +if __name__ == "__main__": + main()