diff --git a/research/orthogonal-plane-triple-decoder/CERTIFICATE.json b/research/orthogonal-plane-triple-decoder/CERTIFICATE.json new file mode 100644 index 0000000000..32324324c3 --- /dev/null +++ b/research/orthogonal-plane-triple-decoder/CERTIFICATE.json @@ -0,0 +1,610 @@ +{ + "blocks": [ + [ + 0, + 91, + 335 + ], + [ + 1, + 94, + 328 + ], + [ + 2, + 76, + 329 + ], + [ + 3, + 81, + 279 + ], + [ + 4, + 74, + 334 + ], + [ + 5, + 86, + 276 + ], + [ + 6, + 99, + 270 + ], + [ + 7, + 102, + 265 + ], + [ + 8, + 128, + 315 + ], + [ + 9, + 75, + 319 + ], + [ + 10, + 95, + 316 + ], + [ + 11, + 142, + 314 + ], + [ + 12, + 98, + 278 + ], + [ + 13, + 90, + 318 + ], + [ + 14, + 87, + 264 + ], + [ + 15, + 132, + 238 + ], + [ + 16, + 97, + 271 + ], + [ + 17, + 62, + 330 + ], + [ + 18, + 67, + 287 + ], + [ + 19, + 60, + 333 + ], + [ + 20, + 72, + 284 + ], + [ + 21, + 103, + 266 + ], + [ + 22, + 143, + 326 + ], + [ + 23, + 116, + 307 + ], + [ + 24, + 61, + 311 + ], + [ + 25, + 120, + 239 + ], + [ + 26, + 93, + 308 + ], + [ + 27, + 145, + 254 + ], + [ + 28, + 89, + 310 + ], + [ + 29, + 149, + 251 + ], + [ + 30, + 66, + 269 + ], + [ + 31, + 104, + 327 + ], + [ + 32, + 48, + 331 + ], + [ + 33, + 53, + 295 + ], + [ + 34, + 46, + 332 + ], + [ + 35, + 58, + 292 + ], + [ + 36, + 109, + 262 + ], + [ + 37, + 96, + 268 + ], + [ + 38, + 59, + 267 + ], + [ + 39, + 47, + 303 + ], + [ + 40, + 105, + 299 + ], + [ + 41, + 92, + 300 + ], + [ + 42, + 151, + 259 + ], + [ + 43, + 88, + 302 + ], + [ + 44, + 191, + 297 + ], + [ + 45, + 108, + 236 + ], + [ + 49, + 171, + 221 + ], + [ + 50, + 122, + 253 + ], + [ + 51, + 134, + 245 + ], + [ + 52, + 127, + 218 + ], + [ + 54, + 118, + 291 + ], + [ + 55, + 130, + 290 + ], + [ + 56, + 139, + 208 + ], + [ + 57, + 187, + 243 + ], + [ + 63, + 175, + 219 + ], + [ + 64, + 110, + 261 + ], + [ + 65, + 135, + 244 + ], + [ + 68, + 106, + 283 + ], + [ + 69, + 131, + 282 + ], + [ + 71, + 115, + 216 + ], + [ + 73, + 136, + 200 + ], + [ + 77, + 183, + 212 + ], + [ + 78, + 111, + 260 + ], + [ + 79, + 123, + 252 + ], + [ + 82, + 107, + 275 + ], + [ + 83, + 119, + 274 + ], + [ + 112, + 174, + 285 + ], + [ + 113, + 186, + 277 + ], + [ + 117, + 194, + 203 + ], + [ + 121, + 166, + 249 + ], + [ + 126, + 172, + 293 + ], + [ + 129, + 182, + 210 + ], + [ + 133, + 178, + 241 + ], + [ + 137, + 141, + 246 + ], + [ + 153, + 181, + 209 + ], + [ + 154, + 169, + 217 + ], + [ + 155, + 184, + 214 + ], + [ + 157, + 177, + 225 + ], + [ + 158, + 165, + 226 + ], + [ + 160, + 164, + 230 + ], + [ + 161, + 188, + 228 + ], + [ + 211, + 242, + 294 + ], + [ + 233, + 248, + 309 + ], + [ + 234, + 240, + 317 + ], + [ + 70, + 168 + ], + [ + 80, + 207 + ], + [ + 84, + 101 + ], + [ + 85, + 100 + ], + [ + 114, + 170 + ], + [ + 124, + 140 + ], + [ + 125, + 146 + ], + [ + 138, + 190 + ], + [ + 144, + 263 + ], + [ + 147, + 237 + ], + [ + 148, + 232 + ], + [ + 150, + 298 + ], + [ + 152, + 296 + ], + [ + 156, + 206 + ], + [ + 159, + 176 + ], + [ + 162, + 189 + ], + [ + 163, + 201 + ], + [ + 167, + 281 + ], + [ + 173, + 220 + ], + [ + 179, + 273 + ], + [ + 180, + 215 + ], + [ + 185, + 304 + ], + [ + 192, + 202 + ], + [ + 193, + 205 + ], + [ + 195, + 204 + ], + [ + 196, + 280 + ], + [ + 197, + 272 + ], + [ + 198, + 224 + ], + [ + 199, + 227 + ], + [ + 213, + 257 + ], + [ + 222, + 250 + ], + [ + 235, + 312 + ], + [ + 256, + 286 + ], + [ + 223 + ], + [ + 229 + ], + [ + 231 + ], + [ + 247 + ], + [ + 255 + ], + [ + 258 + ], + [ + 288 + ], + [ + 289 + ], + [ + 301 + ], + [ + 305 + ], + [ + 306 + ], + [ + 313 + ], + [ + 320 + ], + [ + 321 + ], + [ + 322 + ], + [ + 323 + ], + [ + 324 + ], + [ + 325 + ] + ] +} diff --git a/research/orthogonal-plane-triple-decoder/README.md b/research/orthogonal-plane-triple-decoder/README.md new file mode 100644 index 0000000000..354f0f2628 --- /dev/null +++ b/research/orthogonal-plane-triple-decoder/README.md @@ -0,0 +1,177 @@ +# A rank-135 fitting matrix on all 336 alternating-plane ports + +This contribution was produced by Nick Petalas. It is a finite exact +construction with a scoped rank and tariff proof. No new kappa is claimed. + +For the 336 nondegenerate alternating planes in the even subspace of F2^7, +the explicit partition in [CERTIFICATE.json](CERTIFICATE.json) gives a +fitting matrix of exact scalar rank **135**. This is 33 below the rank-168 +minimum of the spectral family reported in Ali Romman's +[PR #5624](https://github.com/CrocSwap/integer-mult-bounds/pull/5624). +That predecessor result is cited, not audited or replayed here. + +The new factorization has 84 terms of binary pairing tariff six, 33 of +tariff four and 18 of tariff two. Its complete additive full-plane COPY +mass is **672**, the same as the predecessor's cited constructions. Thus +the rank improvement does not create a COPY surplus or establish a better +recursive invoice. The changed fitting matrix advances #5624's second +open question; it does not settle the question of a tariff below 672. + +## Construction and proof + +Let V be the even-weight subspace of F2^7, with the standard binary dot +product. It has dimension six and its form is nondegenerate alternating. +Indeed its orthogonal complement in F2^7 is the line generated by the odd +all-ones vector, which does not lie in V. The ports are the nondegenerate +two-dimensional subspaces E of V. There are 63 choices of a nonzero first +vector and 32 choices of a second vector pairing to one. Each plane is +counted by its six ordered bases, giving 63*32/6 = 336 ports. + +A fitting matrix has diagonal one and entry zero between distinct ports +whose planes are not orthogonal. Entries between orthogonal planes are +free. This is precisely the one-scalar-per-plane convention of #5624. +It differs from the two-scalar-port convention in the older 56-plane +full-plane tariff lineage. + +The certificate indexes planes by the lexicographically sorted triples of +their three nonzero seven-bit vectors. Each vector is the integer with +those seven coordinate bits. It partitions the ports into 84 orthogonal +triples, 33 orthogonal pairs and 18 singletons. For each block B, let u_B +be its 0-1 indicator vector and set + + F = sum_B u_B u_B^T. + +Every port occurs once, so F has unit diagonal. An off-diagonal one occurs +only within an orthogonal block, proving the fitting condition. Reordering +by blocks makes F the direct sum of 84 all-ones 3-by-3 matrices, 33 all-ones +2-by-2 matrices and 18 unit matrices. Each block has scalar rank one. +Equivalently the displayed factorization proves rank at most 135, while +one representative of each block gives an identity minor of order 135. +Thus rank F = 135 over every scalar field, in particular over Q and C. +This is an upper bound for the unrestricted fitting minimum, not its value. + +The tariff of a term u v^T is the binary pairing rank between the spans of +the complete planes in its two supports, as in the credited full-plane +contract. For a block of k pairwise-orthogonal nondegenerate planes, their +sum is an orthogonal direct sum of dimension 2k, with nondegenerate form. +Both supports of u_B u_B^T span this same space, so its tariff is exactly +2k. Hence the complete tariff is + + 84*6 + 33*4 + 18*2 = 672 = 2*336. + +No coefficient, source support or reader support is omitted from that +declared additive tariff. This remains an algebraic tariff, not a paid +physical COPY program. A clique in this geometry has at most three planes, +so this particular partition family needs at least 112 blocks. Attainment +of 112, optimality of 135 and a global fitting-rank lower bound are unproved. + +## Deterministic reproduction and evidence + +Use CPython 3.12 with its standard library, from the worktree root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error research/orthogonal-plane-triple-decoder/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error research/orthogonal-plane-triple-decoder/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/orthogonal-plane-triple-decoder +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/orthogonal-plane-triple-decoder --check-source-history +``` + +Another CPython 3.12 interpreter may replace the absolute local path. Both +registered checks have 120-second limits. The direct verifier prints a +generated SHA-256 receipt binding all six package files, then +`PASS_ORTHOGONAL_PLANE_TRIPLE_DECODER rank=135 copy_mass=672`. It writes +nothing and needs no Git, network, solver or predecessor executable. + +Local CPython 3.12.15 on macOS 27.0.1 arm64 passed both registered commands. +The separately timed direct checks took 0.435 and 0.431 seconds in normal +and optimized mode. Three actual optimized CLI corruptions also reject +missing coverage, a doubled factorization coefficient and a lowered tariff. +These are verification timings, not a performance comparison. Hosted CI is +reported separately in the PR body. + +The construction is reproducible without optimization. Visit orthogonal +triples in lexicographic order and keep each disjoint triple. Then visit +remaining ports in ascending order and pair a port with its least available +orthogonal neighbor, leaving the others as singletons. The verifier checks +the stored partition against this recipe and separately verifies its actual +mathematics. + +The complete checks cover both the vector-pair enumeration and an independent +RREF enumeration of all 651 binary two-spaces, retaining the same 336 +nondegenerate planes. They check every block, all 112,896 fitting entries, +all 18,225 entries of the identity minor, the literal binary rank of F and +every term's span and Gram rank. Eight controls reject missing or duplicated +coverage, a nonorthogonal pair, a Boolean or out-of-range index, a repeated +index, a four-member block and an empty block. Checks use exceptions and +remain active under optimized Python. + +The advance CLAIM targeted a full 112-triple partition. A bounded +backtracking attempt returned no cover; a 45-second +full-partition integer-program attempt also returned no feasible witness. +Neither run proves infeasibility. The first deterministic greedy construction +then gave the strict rank improvement above, and further search stopped. +The published result is the explicit 135-block witness, not a search failure +or a claim of optimality. Search software is unnecessary for its replay. + +## Limits and implementation decisions + +The finite geometry, fitting matrix and its additive support tariff are the +entire claim. Native preparation, physical acquisition and delivery, dirty +restoration, ownership, compiler closure, routing, precision, stock, BIT +compatibility and the complete outer caller remain unpriced. No supplier +admission, selected-frontier change or complete multiplication theorem is +supplied. Independent human and formal proof-kernel review are unclaimed. +No Lean, Docker, selected cold replay or predecessor scientific replay was run. + +The verifier has no recursion, subprocess or variable-size search. Loops have +fixed domains of at most 336 ports, 651 RREF planes, 336 blocks, seven address +bits and 336 rank pivots. Certificate bytes are capped at 1 MiB before parsing. +The incidence matrix has at most 336^2 entries and matrix construction uses +at most 336^3 scalar products. Every function is below 60 physical lines. +Warning-strict normal and optimized executions provide runtime diagnostics. +Ruff was unavailable in the local environment; source compilation passed. + +Power-of-ten rule 3 has a managed-runtime deviation. Python allocates integer, +list, tuple, set and JSON objects during this offline calculation. Fixed +domains bound the mathematical tables above; each receipt file is streamed +with a 1 MiB cap and released before the next. There is no steady service, +shared mutable state or persistent resource. Larger geometries would require +new explicit capacities and a new verification budget. No repository-wide +analysis configuration is changed for this isolated standard-library checker. + +## Open next questions + +1. Can all 336 ports be partitioned into 112 orthogonal triples? This is the + dimension lower bound in the clique-partition family. Start with the 1,120 + admissible triples as an exact-cover instance and publish a literal witness + if one is found. The bounded searches above leave existence unresolved. +2. Can a changed fitting matrix or factorization achieve COPY mass below 672? + Start with one exact factorization and every literal source/reader pairing + rank. The present rank reduction leaves that tariff question open, and + physical acquisition and restoration would still require a separate bill. + +Structured first steps and blockers are in [TASK.json](TASK.json). + +## Credit and source boundary + +Produced by Nick Petalas. Ali Romman's #5624 supplies the exact port geometry, +fitting convention, rank-168 spectral comparison and changed-matrix question. +Mark / Matarener's `plane-port-global-rank-dual` and CubeJerry's #4365 supply +the additive complete-plane support-pairing contract, with Ryanson Jonathan, +Philippe Van Velzen, Cinna Davis, Adam Gall and the retained endpoint lineage. +Chris R / Clear1nsight, Chafik Boukhalfa, Rohan Arun, Ali Romman and icekylinx +retain the native-plane lineage cited by #5624. No native theorem or +predecessor executable is imported here. Orthogonal clique partitions and +block-matrix ranks are elementary tools; no historical priority for them is +claimed. The new artifact is this explicit rank-135 fitting construction. + +Canonical base is `19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority +revision 8. [SOURCES.json](SOURCES.json) pins the unchanged main-source +documents as historical provenance. The original task card is explicitly +changed to this geometric side result; its complete supplier admission gate +is not met. Source-binding orientation passed. Live PRs and claims, recent +account contributions, active Discussions, main and merged searches were +checked before reservation. Cached remote coverage was complete at the +reported checkpoint; sparse local-note coverage was incomplete and provides +no novelty guarantee. The selected result and all frozen predecessors remain +unchanged. Apache-2.0. diff --git a/research/orthogonal-plane-triple-decoder/SOURCES.json b/research/orthogonal-plane-triple-decoder/SOURCES.json new file mode 100644 index 0000000000..2b1bc911cb --- /dev/null +++ b/research/orthogonal-plane-triple-decoder/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/alternating-plane-spectral-copy/README.md", + "usage": "provenance", + "git_blob": "5275ad3748602aa20d06ccbd9686af83fda2a4fe", + "sha256": "6c270429599180ddc3185ba3026d549ca27dfe1f8a9cd493f0d20b0dcee28ccd" + }, + { + "path": "research/alternating-plane-spectral-copy/PROOF.md", + "usage": "provenance", + "git_blob": "362d32ef149c00568027d0dd86f62a71352697c3", + "sha256": "87c80caea668ac82ccb114ecd09252cce434dc78098f9b19d241e134e595ce51" + }, + { + "path": "research/plane-port-global-rank-dual/README.md", + "usage": "provenance", + "git_blob": "ee074b60df481c564a82d7324cde8ca9f8a81056", + "sha256": "7596b1c9fb0739295a30d506d7b7e4cdabdda4ea9dd13afb34f12b58764d1196" + } + ] +} diff --git a/research/orthogonal-plane-triple-decoder/TASK.json b/research/orthogonal-plane-triple-decoder/TASK.json new file mode 100644 index 0000000000..6f9f4cada8 --- /dev/null +++ b/research/orthogonal-plane-triple-decoder/TASK.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "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", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "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": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Finite exact 135-term clique-partition fitting matrix on all 336 nondegenerate alternating-plane ports, with complete additive full-plane tariff 672.", + "scope_change_reason": "Take the changed-fitting-matrix question in Ali Romman PR5624, rather than audit a supplier. This geometric side construction reduces scalar rank without improving the COPY tariff or supplying a complete physical invoice.", + "bottleneck_link": "This supplies a concrete changed fitting matrix below the cited 168-rank spectral family, while exposing the unchanged two-coordinate COPY bill. Algebraic rank alone is insufficient for a supplier improvement.", + "budget_minutes": 60, + "stop_rule": "Package the first verified strict rank improvement and stop searching.", + "outcome": "completed", + "evidence": "Explicit orthogonal partition, complete 336-by-336 fitting and incidence-factor check, 135-by-135 identity minor, independent RREF plane census and literal binary support-pairing ranks.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can all 336 ports be partitioned into 112 orthogonal triples?", + "why_it_matters": "112 is the dimension lower bound for this clique-partition family and would reduce the scalar rank further, with the same tariff.", + "first_step": "Use the 1120 admissible triples as an exact-cover instance and retain an explicit exact witness if one is found.", + "blocked_by": "The bounded full-partition searches returned no witness or exclusion; no optimality is claimed." + }, + { + "question": "Can a changed fitting matrix or factorization achieve additive full-plane COPY mass below 672?", + "why_it_matters": "The rank-135 construction still consumes the full two-coordinate allowance.", + "first_step": "Give one exact factorization with literal source and reader support-pairing ranks.", + "blocked_by": "Neither this construction nor PR5624 settles the unrestricted cost minimum; physical acquisition and restoration are additionally unpriced." + } + ] +} diff --git a/research/orthogonal-plane-triple-decoder/VERIFY.json b/research/orthogonal-plane-triple-decoder/VERIFY.json new file mode 100644 index 0000000000..6a7a163c8d --- /dev/null +++ b/research/orthogonal-plane-triple-decoder/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete independent port enumerations, explicit partition, every fitting entry, identity minor, support tariffs and eight rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete independent port enumerations, explicit partition, every fitting entry, identity minor, support tariffs and eight rejection controls." + } + ] +} diff --git a/research/orthogonal-plane-triple-decoder/verify.py b/research/orthogonal-plane-triple-decoder/verify.py new file mode 100644 index 0000000000..170b708582 --- /dev/null +++ b/research/orthogonal-plane-triple-decoder/verify.py @@ -0,0 +1,210 @@ +#!/usr/bin/env python3 +"""Check the rank-135 alternating-plane fitting construction. Writes nothing.""" + +from collections import Counter +from hashlib import sha256 +from itertools import combinations, product +import json +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +FILES = ("CERTIFICATE.json", "README.md", "SOURCES.json", "TASK.json", + "VERIFY.json", "verify.py") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dot(a, b): + return (a & b).bit_count() % 2 + + +def planes(): + vectors = [a for a in range(1, 128) if a.bit_count() % 2 == 0] + result = {tuple(sorted((a, b, a ^ b))) + for a, b in combinations(vectors, 2) if dot(a, b) == 1} + require(len(vectors) == 63 and len(result) == 336, "port count") + return tuple(sorted(result)) + + +def rref_planes(): + """Independent complete two-space enumeration in six even coordinates.""" + result = set() + total = 0 + for i, j in combinations(range(6), 2): + slots = [(0, k) for k in range(i + 1, 6) if k != j] + slots += [(1, k) for k in range(j + 1, 6)] + for values in product((0, 1), repeat=len(slots)): + rows = [1 << i, 1 << j] + for (r, k), value in zip(slots, values, strict=True): + rows[r] |= value << k + a, b = [x | ((x.bit_count() % 2) << 6) for x in rows] + total += 1 + if dot(a, b): + result.add(tuple(sorted((a, b, a ^ b)))) + require(total == 651, "RREF coverage") + return tuple(sorted(result)) + + +def orthogonal(e, f): + return all(dot(a, b) == 0 for a in e for b in f) + + +def greedy_partition(ports): + """Replay the finite construction, without a search or optimization.""" + adjacent = [{j for j, f in enumerate(ports) if orthogonal(e, f)} + for e in ports] + require(all(len(neighbors) == 20 for neighbors in adjacent), "degree") + blocks = [] + left = set(range(336)) + triples = 0 + for i in range(336): + for j in sorted(adjacent[i]): + if j <= i: + continue + for k in sorted(adjacent[i] & adjacent[j]): + if k > j: + triples += 1 + if {i, j, k} <= left: + blocks.append([i, j, k]) + left.difference_update((i, j, k)) + require(triples == 1120, "triple census") + for i in sorted(left.copy()): + if i not in left: + continue + options = sorted(left & adjacent[i]) + if options: + blocks.append([i, options[0]]) + left.difference_update(blocks[-1]) + blocks.extend([i] for i in sorted(left)) + return blocks + + +def check_partition(ports, blocks): + require(type(blocks) is list and 1 <= len(blocks) <= 336, "block list") + seen = [] + for block in blocks: + require(type(block) is list and 1 <= len(block) <= 3, "block size") + require(all(type(i) is int and 0 <= i < 336 for i in block), "index") + require(len(set(block)) == len(block), "repeated index") + require(all(orthogonal(ports[i], ports[j]) + for i, j in combinations(block, 2)), "orthogonality") + seen.extend(block) + require(sorted(seen) == list(range(336)), "partition coverage") + + +def binary_rank(rows, width): + require(0 <= width <= 336 and len(rows) <= 336, "rank dimensions") + pivots = [0] * width + rank = 0 + for original in rows: + require(type(original) is int and 0 <= original < (1 << width), "row") + row = original + for bit in range(width - 1, -1, -1): + if row & (1 << bit): + if pivots[bit]: + row ^= pivots[bit] + else: + pivots[bit] = row + rank += 1 + break + return rank + + +def check_matrix(ports, blocks): + incidence = [[int(i in block) for block in blocks] for i in range(336)] + matrix = [[sum(a * b for a, b in zip(u, v, strict=True)) + for v in incidence] for u in incidence] + owner = {i: b for b, block in enumerate(blocks) for i in block} + for i in range(336): + for j in range(336): + require(matrix[i][j] == int(owner[i] == owner[j]), "factorization") + if i == j: + require(matrix[i][j] == 1, "diagonal") + elif not orthogonal(ports[i], ports[j]): + require(matrix[i][j] == 0, "forbidden entry") + anchors = [block[0] for block in blocks] + for a, i in enumerate(anchors): + for b, j in enumerate(anchors): + require(matrix[i][j] == int(a == b), "identity minor") + packed = [sum(x << j for j, x in enumerate(row)) for row in matrix] + require(binary_rank(packed, 336) == len(blocks), "independent binary rank") + return matrix + + +def check_tariff(ports, blocks): + tariffs = [] + for block in blocks: + generators = [a for i in block for a in ports[i][:2]] + require(binary_rank(generators, 7) == 2 * len(block), "span dimension") + gram = [sum(dot(a, b) << j for j, b in enumerate(generators)) + for a in generators] + tariff = binary_rank(gram, len(generators)) + require(tariff == 2 * len(block), "term tariff") + tariffs.append(tariff) + require(sum(tariffs) == 672, "total tariff") + return tariffs + + +def controls(ports, blocks): + bad_pair = next([i, j] for i, j in combinations(range(336), 2) + if not orthogonal(ports[i], ports[j])) + cases = [(blocks[:-1], "partition coverage"), + (blocks + [blocks[0]], "partition coverage"), + ([bad_pair] + blocks[1:], "orthogonality"), + ([[True]] + blocks[1:], "index"), + ([[336]] + blocks[1:], "index"), + ([[0, 0]] + blocks[1:], "repeated index"), + ([[0, 1, 2, 3]] + blocks[1:], "block size"), + ([[]] + blocks[1:], "block size")] + for candidate, expected in cases: + try: + check_partition(ports, candidate) + except ValueError as exc: + require(str(exc) == expected, "wrong rejection reason") + else: + raise ValueError("accepted invalid partition") + return len(cases) + + +def read_small(path): + with path.open("rb") as stream: + data = stream.read(1_048_577) + require(len(data) <= 1_048_576, "file capacity") + return data + + +def main(): + ports = planes() + require(ports == rref_planes(), "independent port enumeration") + certificate = json.loads(read_small(HERE / "CERTIFICATE.json")) + require(type(certificate) is dict and set(certificate) == {"blocks"}, + "certificate schema") + blocks = certificate["blocks"] + check_partition(ports, blocks) + require(blocks == greedy_partition(ports), "construction replay") + require(Counter(map(len, blocks)) == {1: 18, 2: 33, 3: 84}, "block counts") + require(len(blocks) == 135 < 168, "strict rank improvement") + matrix = check_matrix(ports, blocks) + tariffs = check_tariff(ports, blocks) + rejected = controls(ports, blocks) + receipt = { + "status": "PASS_ORTHOGONAL_PLANE_TRIPLE_DECODER", + "ports": len(ports), "blocks": len(blocks), + "block_sizes": dict(sorted(Counter(map(len, blocks)).items())), + "fitting_entries": sum(map(len, matrix)), "exact_rank": len(blocks), + "identity_minor_entries": len(blocks) ** 2, + "tariffs": dict(sorted(Counter(tariffs).items())), + "copy_mass": sum(tariffs), "rejection_controls": rejected, + "sha256": {name: sha256(read_small(HERE / name)).hexdigest() + for name in FILES}, + } + print(json.dumps(receipt, indent=2, sort_keys=True)) + print("PASS_ORTHOGONAL_PLANE_TRIPLE_DECODER rank=135 copy_mass=672") + + +if __name__ == "__main__": + main()