From 7f31a561787864f26eb2242ef35179d07223accf Mon Sep 17 00:00:00 2001 From: Hanson Sun <182361798+bbMisk@users.noreply.github.com> Date: Tue, 13 Oct 2026 17:02:05 -0400 Subject: [PATCH] Independently verify the masked root-star cost floor --- .../CERTIFICATE.json | 164 ++++++++++++ .../CLAIM.json | 47 ++++ .../masked-star-frame-compatibility/README.md | 219 ++++++++++++++++ .../SOURCES.json | 171 +++++++++++++ .../masked-star-frame-compatibility/TASK.json | 61 +++++ .../VALIDATION.json | 166 ++++++++++++ .../VERIFY.json | 19 ++ .../independent_check.py | 180 +++++++++++++ .../test_package.py | 71 ++++++ .../masked-star-frame-compatibility/verify.py | 240 ++++++++++++++++++ 10 files changed, 1338 insertions(+) create mode 100644 research/masked-star-frame-compatibility/CERTIFICATE.json create mode 100644 research/masked-star-frame-compatibility/CLAIM.json create mode 100644 research/masked-star-frame-compatibility/README.md create mode 100644 research/masked-star-frame-compatibility/SOURCES.json create mode 100644 research/masked-star-frame-compatibility/TASK.json create mode 100644 research/masked-star-frame-compatibility/VALIDATION.json create mode 100644 research/masked-star-frame-compatibility/VERIFY.json create mode 100644 research/masked-star-frame-compatibility/independent_check.py create mode 100644 research/masked-star-frame-compatibility/test_package.py create mode 100644 research/masked-star-frame-compatibility/verify.py diff --git a/research/masked-star-frame-compatibility/CERTIFICATE.json b/research/masked-star-frame-compatibility/CERTIFICATE.json new file mode 100644 index 0000000000..3aa023d65d --- /dev/null +++ b/research/masked-star-frame-compatibility/CERTIFICATE.json @@ -0,0 +1,164 @@ +{ + "schema": "masked-star-frame-compatibility-v1", + "scope": "P112; exact C(alpha)/N(alpha) supports; ordinary complex transpose; arbitrary finite term count", + "lines": 120, + "live_lines": 112, + "label_rank": 9, + "roots_sha256": "499909f15616b21ed34b704054685a0c90c244fb81819ba458e076b8dd97308c", + "puncture": [ + 0, + 1, + 6, + 11, + 20, + 29, + 106, + 119 + ], + "frames": 1260, + "frames_sha256": "9f4794b9b10349aa5e4e095547b75fd08c4e895c08980db020c79c525a9a3924", + "frames_per_line": 90, + "orthogonal_pair_extension_histogram": { + "10": 2856, + "15": 448 + }, + "ordered_support_pairs": 57600, + "support_labels": 240, + "distinct_supports": 232, + "rank_histogram": { + "7": 7616, + "8": 37440, + "9": 12544 + }, + "ranks_sha256": "0ff8da9bad5e811a4daf04ea9b4e42111a2e43b6c5cab90602edfae14ad62866", + "rank7_live_normal_count_histogram": { + "1": 1792, + "2": 5824 + }, + "star_zero_frames_sha256": "cdd285f6a21e4871c6aaaf72d6d558a9e94c1adcb3085353c4f8c343c5899c65", + "nonorthogonal_clique_counts": { + "0": 1, + "1": 112, + "2": 2912, + "3": 25088, + "4": 88704, + "5": 161280, + "6": 145152, + "7": 55296, + "8": 4032 + }, + "maximum_nonorthogonal_clique": 8, + "maximum_clique_witness": [ + 2, + 3, + 13, + 22, + 44, + 71, + 80, + 99 + ], + "maximum_clique_root_vectors": [ + [ + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 2, + 0, + -2 + ], + [ + 0, + 0, + 0, + 2, + 0, + -2, + 0, + 0 + ], + [ + 0, + 0, + 2, + 0, + 0, + -2, + 0, + 0 + ], + [ + 1, + -1, + -1, + -1, + -1, + 1, + -1, + -1 + ], + [ + 1, + -1, + 1, + 1, + 1, + -1, + 1, + 1 + ], + [ + 1, + 1, + -1, + -1, + 1, + 1, + -1, + -1 + ], + [ + 1, + 1, + 1, + 1, + -1, + -1, + 1, + 1 + ] + ], + "coordinate_decoder_costs": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + "coordinate_decoder_entries": 12544, + "cost_floor": 64, + "controls": [ + "changed_coordinate_coefficient_rejected", + "zero_decoder_rejected_by_diagonal", + "synthetic_K9_detected_without_depth_cutoff", + "rank_one_singleton_outside_star_family", + "repeated_normal_has_shared_zero_frame", + "orthogonal_normals_have_shared_zero_frame", + "free_odd_entry_patch_vanishes_on_every_frame" + ] +} diff --git a/research/masked-star-frame-compatibility/CLAIM.json b/research/masked-star-frame-compatibility/CLAIM.json new file mode 100644 index 0000000000..d80a96f8f1 --- /dev/null +++ b/research/masked-star-frame-compatibility/CLAIM.json @@ -0,0 +1,47 @@ +{ + "assignment_seed": 36, + "random_source": "Python secrets.randbelow(100), operating-system entropy", + "track": "complex supplier", + "base_commit": "49b3157d1d89adcef16df8be98445451672be5ba", + "task_id": "complex-masked-decoder", + "scope_status": "refined", + "object": "P112 masked root-star decoder with C(alpha) or N(alpha) supports and arbitrary complex coefficients", + "hypothesis": "Simultaneous orthogonal-frame constraints exclude a total copied-information cost below 64, closing the 63-cost case left by the scalar covering relaxation in PR1226.", + "method": "Reconstruct all E8 lines, all support-pair ranks, and all 1260 live frames; reduce nine rank-seven atoms to pairwise compatible live normal lines; exact clique census.", + "seed_diversification": "36 mod 3 = 0 selects simultaneous-frame compatibility before nonlinear ten-term synthesis or helper-boundary design; use cyclic vertex order offset 36 as one verification order.", + "candidates": [ + { + "object": "P112 masked root-star rank-seven assembly", + "method": "simultaneous-frame compatibility; selected because PR1226 explicitly leaves its assembly gap open" + }, + { + "object": "P120 ten-term decoder with one residual direction in each factor", + "method": "exact sparse-factor synthesis; rejected for this session because PR1224 already supplies a two-sided ten-term example and physical pricing is absent" + }, + { + "object": "new helper boundary outside the 71-record provider catalogue", + "method": "derive a paid contract with shared restoration; deferred because no concrete legal boundary saving identified" + } + ], + "nearest_predecessor": { + "pr": 1226, + "author": "Navinor", + "head": "8b10989e4e45f0f9ce41004d7898a21a32f87e11" + }, + "optimistic_budget": "Below cost 64, minimum per-term rank 7 and frame rank 8 restrict a candidate to eight or nine paid atoms. Free odd-entry singleton repairs vanish on every orthogonal frame. All omitted realization costs are nonnegative, so an obstruction already in this relaxation rules out savings in this family.", + "stopping_rule": "Stop once the finite compatibility obstruction is proved with witnesses and controls, or report the exact failed implication if false. No wider support search.", + "expected_deliverable": "One scoped negative result with written proof, exact finite certificate, independently implemented finite verification and meaningful mutation controls; no new kappa.", + "expected_finish_utc": "2026-10-13T21:21:00Z", + "coordination": "No pinned issue returned by the GitHub GraphQL pinnedIssues query; local claim as instructed. Read discussions including #1210 and its PR1226 result, open PR bodies and review ledger before this claim.", + "created_utc": "2026-10-13T20:45:22.648472+00:00", + "attribution": "Hanson Sun (@bbMisk), substantial OpenAI Codex assistance; predecessor credit retained; Apache-2.0.", + "result": { + "status": "completed independent verification", + "finding": "Exact support-family cost floor 64, independently corroborating concurrent PR1236. Both new checkers and the pinned PR1236 registered package pass on Python 3.12; no new kappa.", + "concurrent_result_pr": 1236, + "concurrent_result_head": "ee8437bd9879272094e20c024cd34a53c4e84cd8", + "distinct_evidence": "Weyl-reflection root generation, pivoted maximal-clique census, independent column-rank checks, and previously unreported Python 3.12 registered replay of PR1236.", + "result_url": "https://github.com/bbMisk/integer-mult-bounds/tree/research/p112-star-frame-verification-s36-20261013/research/masked-star-frame-compatibility", + "updated_utc": "2026-10-13T21:00:48.369867+00:00" + } +} diff --git a/research/masked-star-frame-compatibility/README.md b/research/masked-star-frame-compatibility/README.md new file mode 100644 index 0000000000..1d03ef4cd8 --- /dev/null +++ b/research/masked-star-frame-compatibility/README.md @@ -0,0 +1,219 @@ +# Independent finite verification of the P112 masked root-star floor + +**Independent verification of a scoped negative result: the minimum +copied-information cost is 64.** +This holds for the P112 masked complex decoder whose paid terms have exactly +the untrimmed or self-trimmed root-star supports defined below, with arbitrary +complex coefficients and any finite number of terms. The usual eight coordinate +stars attain 64. No new supplier or kappa is claimed. + +The final overlap refresh found **David Arias's concurrent +[PR1236](https://github.com/CrocSwap/integer-mult-bounds/pull/1236)**, at +`ee8437bd9879272094e20c024cd34a53c4e84cd8`, which had already submitted the +same conclusion. Our initial claim and both implementations preceded reading +that PR. This package therefore contributes independent corroboration, with +the same scope and no priority claim. Its distinctive check generates roots +by Weyl reflections and exhausts maximal cliques by pivoted Bron-Kerbosch; +PR1236's second checker instead uses lattice coordinates and a quadratic-form +obstruction. We also give a Python 3.12 replay of its pinned registered package, +the runtime that its initial validation receipt said was untested. + +[Navinor's PR1226](https://github.com/CrocSwap/integer-mult-bounds/pull/1226) +computes the sharp value `784/13` of an aggregate frame-covering relaxation and +leaves open whether cheap trimmed atoms can actually assemble at cost 63. +That relaxation and its census remain correct. The strengthening retains +**which frames each atom misses**: two missed terms already defeat a nine-term +decoder on a common frame. The resulting compatibility condition excludes +cost 63, without a coefficient search or a root-linearity assumption. + +## Model and exact scope + +Let `R` be the 120 norm-two E8 root lines, choosing one sign for each line. +Let `F0 = {e0 +/- e1, e2 +/- e3, e4 +/- e5, e6 +/- e7}` and +`L = R - F0`, the 112 live lines. Write `G[i,j] = ` and +`B[i,j] = (G[i,j] + 1) mod 2` for the binary label pairing. +For any root line `a`, define + +```text +C(a) = {i in L : != 0}, N(a) = C(a) - {a}. +``` + +There are 240 labeled supports and 232 distinct subsets: for the eight +punctured normals, `C(a) = N(a)`. Each paid term is `d_k t_k^T`, where +the **actual nonzero supports** of `d_k` and `t_k` each equal one of these +subsets. Its price is `beta_k = rank_F2 B[supp(d_k), supp(t_k)]`, and prices +add separately across terms. Coefficients can be arbitrary complex numbers; +transpose is ordinary transpose, with no conjugation. + +The masked identity requires `sum_k d_k(i)t_k(j) = 2G[i,j]` only when +`G[i,j]` is even: the diagonal entries are 4 and orthogonal off-diagonal +entries are zero. Any number of rank-zero terms may also be included. +For example, the unrestricted odd entries can be repaired by free singleton +terms. Rank-zero terms vanish on every frame used below. + +The result does **not** cover further deletions inside a star, arbitrary +subsets contained in a star, unions of stars, other punctures, a different +label pairing, or a pricing scheme that jointly charges several terms. + +## Written proof and checked finite premises + +A live frame is eight pairwise orthogonal lines in `L`. Its masked target +is `4 I_8`, of complex rank eight. Every paid term restricts to a matrix of +rank at most one. A rank-zero term has `B[S,T]=0`; if both supports met a +frame, a pair in `S x T` on that frame would instead have binary pairing +one. Thus rank-zero terms contribute nothing on every frame. At least +eight paid terms must be nonzero on each frame. + +The executable finite premises are: + +1. **Atom classification.** All 57,600 ordered labeled support pairs have + rank 7, 8 or 9, with counts 7,616, 37,440 and 12,544. Rank seven occurs + exactly when the two normals have inner product `+/-1` and both supports + are effectively self-trimmed: a live normal must use `N`, while a + punctured normal may use either label. Since the punctured normals are + pairwise orthogonal, every rank-seven atom has at least one live trimmed + normal. +2. **Annihilation and extension.** There are 1,260 live frames; each live + line belongs to 90. The support `N(a)` misses exactly the frames + containing `a`; an untrimmed `C(a)` misses none. Every orthogonal pair + of distinct live lines extends to a live frame: 2,856 pairs have ten + extensions and 448 have fifteen. +3. **Compatibility cap.** A pairwise nonorthogonal set of live lines has + size at most eight. The primary implementation exhausts every clique + of this graph, with no depth cutoff. The counts for sizes zero through + eight are + `1, 112, 2912, 25088, 88704, 161280, 145152, 55296, 4032`; + there are no larger cliques. A separate maximal-clique implementation + finds 896 maximal triples, 23,040 maximal seven-cliques and 4,032 + maximal eight-cliques. An eight-line witness is in the certificate. + +These facts imply the claimed floor. Suppose the total price is below 64, +and let `n` be the number of paid terms. Premise 1 gives `n <= 9`, while +the frame rank argument gives `n >= 8`. + +If `n = 8`, at least one term has rank seven. Choose a live trimmed normal +of that term and a frame containing it. The term is zero on that frame, +leaving at most seven rank-one matrices to produce a rank-eight target: +a contradiction. + +If `n = 9`, every term has rank seven and the total price is 63. Choose +one live trimmed normal `a_k` from each term. No two choices can coincide: +a frame containing the repeated normal would annihilate two terms. +Nor can two choices be orthogonal: their common live-frame extension would +again annihilate two terms. The nine choices must therefore be distinct and +pairwise nonorthogonal, contradicting premise 3. This exhausts the term counts. + +Finally, for the eight normals `f` in `F0`, the coordinate terms +`d_f(i) = t_f(i) = ` satisfy +`sum_f = 2` on all live pairs. Each term costs eight, +so the bound 64 is attained. The checker tests all 12,544 entries and all +eight prices. + +This is a written finite-geometric proof with exhaustive exact checks of +its premises. It is not proof-assistant verification, independent human +review, or a proof of the full asymptotic multiplication theorem. + +## Reproduce + +From the repository root, Python 3.10+ and the standard library: + +```sh +python3 -I -B research/masked-star-frame-compatibility/test_package.py +``` + +Expected: both checker markers below, successful corruption controls, and +`PASS_MASKED_STAR_PACKAGE`. All subprocesses have bounded timeouts. The +package runs offline and does not regenerate predecessor artifacts. + +```text +PASS_MASKED_STAR_FRAME_COMPATIBILITY atoms=57600 frames=1260 max_clique=8 cost_floor=64 controls=7 +PASS_INDEPENDENT_MASKED_STAR weyl_roots=240 atoms=57600 frames=1260 maximal_cliques={3: 896, 7: 23040, 8: 4032} cost_floor=64 +``` + +The primary checker reconstructs roots directly, uses binary row elimination, +enumerates all cliques, and compares every field with +[CERTIFICATE.json](CERTIFICATE.json). `verify.py --write` regenerates that +certificate. The separate checker instead generates the 240 roots by Weyl +reflections, uses binary column elimination and pivoted Bron-Kerbosch +maximal-clique enumeration, with cyclic vertex offset 36. It imports neither +the primary checker nor predecessor code. Both recompute the full atom census, +frame annihilation/extension facts, graph cap and cost-64 construction. +This is implementation independence within one AI-assisted contribution. + +Controls cover a wrong decoder coefficient, the diagonal condition, a +synthetic nine-clique, a rank-one singleton outside the support family, +repeated and orthogonal normal collisions, and free odd-entry patches. +The package runner also corrupts the rank census, clique cap and a clique +witness, requires nonzero exits, tests a path containing spaces, and checks +that verification preserves the committed certificate. + +[VERIFY.json](VERIFY.json) opts into the repository's bounded Python 3.12 +package workflow. With Python 3.12 installed, the registered equivalent is: + +```sh +python3.12 scripts/research_package.py --package research/masked-star-frame-compatibility +``` + +## Provenance, overlap and accounting + +Base: `49b3157d1d89adcef16df8be98445451672be5ba`. Assignment seed **36**, +complex-supplier track; [CLAIM.json](CLAIM.json) records three candidates, +the live overlap check and stopping rule. No pinned coordination issue was +present, so the claim is local, as requested. [TASK.json](TASK.json) records +the refined `complex-masked-decoder` card and the final corroboration status; +[SOURCES.json](SOURCES.json) pins +historical context and predecessor sources. None is an imported executable +dependency. [VALIDATION.json](VALIDATION.json) records the completed checks. + +At this base, the selected conditional kappa is +`836330098538459/500000000000000000`, from the reviewed #1094 construction, +and the complex primitive is binding. This result rejects a proposed +cost-saving route even in the favorable relaxation that gives all source +access, helper preparation, frame changes, restoration and physical hosting +zero additional cost. It does not price or construct a new recursive +supplier. Nonnegative implementation charges cannot rescue a decoder whose +copied-information price already fails to improve 64. The selected bit +supplier, recursive invoice and frontier are unchanged; no new assembly +or complete cold replay is claimed. All inherited compiler, realization, +hosting, precision/tape, recovery and analytic-transfer obligations remain. + +Credit: + +- **David Arias / DavidAriasC, PR1236**, at the head above: the concurrent + cost-64 theorem, primitive-integer-dependence proof and two finite checkers. + The theorem and complete-clique counts here independently agree with that + earlier submission. The maximal-clique/Weyl-orbit check is separately written; + PR1236's code and parity proof are not imported into either new checker. +- **Navinor, PR1226**, head + `8b10989e4e45f0f9ce41004d7898a21a32f87e11`: the exact root-star census, + the aggregate `784/13` covering bound and the explicit unresolved assembly + question. This package independently reconstructs that census and adds + simultaneous frame compatibility; it does not correct the predecessor's + valid relaxation. +- **DreamingOfClouds, PR717/595/604**: the B14 label model, masked reduction, + copied-information accounting and mixed-beta problem. +- **themilkman216, PR968**, **woklerx, PR1077**, and + **Joel Pulikkan / GamingPuzzled, PR620**: + preceding all-pairs decoder floors, root geometry and the coordinate + cost-64 construction. +- Concurrent **burntout76, PR1212**, **David Arias, PR1213**, and + **Philipp / mightyOil, PR1191** address eight-term or one-root-linear-factor + masked classes. Their theorems are not premises here; our support-restricted + result permits any term count and neither factor needs to be root-linear. + **joaqcoo, PR1224** studies nine-term all-pairs normal forms, a different + exactness requirement. + +Prepared by **Hanson Sun (@bbMisk)** with substantial **OpenAI Codex +assistance** in the proof, implementations, experiments and documentation. +New work is Apache-2.0. No predecessor source files are copied into this package. + +## Open next questions + +Can deleting one additional live line from a trimmed support create a +cost-saving masked decoder? Such supports are outside this theorem and could +change both the minimum atom rank and its missed-frame pattern. A feasible +first check is an exact census of their ranks and frame signatures before +attempting coefficient synthesis. No favorable complete supplier budget or +legal realization for that enlarged family is currently established here. +The structured question, relevance, first step and blocker are in +[TASK.json](TASK.json). diff --git a/research/masked-star-frame-compatibility/SOURCES.json b/research/masked-star-frame-compatibility/SOURCES.json new file mode 100644 index 0000000000..106c2903e4 --- /dev/null +++ b/research/masked-star-frame-compatibility/SOURCES.json @@ -0,0 +1,171 @@ +{ + "schema_version": 1, + "base_commit": "49b3157d1d89adcef16df8be98445451672be5ba", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "provenance", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "provenance", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "provenance", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/complex-frame-pair-decoders/README.md", + "usage": "provenance", + "git_blob": "be5bbbee8e30a4ee39fa513896e8fc7e0bb3721e", + "sha256": "edd848b0177dc73a6e2646d4fd82f0b2ceae37e642bf19d6af602579a041a57e" + }, + { + "path": "research/complex-frame-pair-decoders/verify.py", + "usage": "provenance", + "git_blob": "57dd8993e8ac016e8a92a9a885392b58014137bb", + "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" + }, + { + "path": "research/complex-decoder-field-extension-seed44/README.md", + "usage": "provenance", + "git_blob": "a6e6d2e04249191c1bce5c6e2977c11f9969b7a3", + "sha256": "788a99eef3f187c2cbff6d490933fcc8f8e7fd15d1b685c188023605916887d4" + } + ], + "external_predecessors": [ + { + "pr": 1236, + "author": "David Arias / DavidAriasC", + "commit": "ee8437bd9879272094e20c024cd34a53c4e84cd8", + "repository": "https://github.com/DavidAriasC/integer-mult-bounds", + "usage": "Concurrent theorem independently corroborated. No code imported. Separately replayed the pinned registered package using Python 3.12.13.", + "files": [ + { + "path": "research/masked-root-star-assembly/PROOF.md", + "git_blob": "af5b67c89cb55472f709fa214f7705183876f65b", + "sha256": "6cd0a6df96a418b524623e7e39c863af7709a18c4ded453a6a077bcd5ade92a2" + }, + { + "path": "research/masked-root-star-assembly/README.md", + "git_blob": "88e59d04e90a359d3c7d37068f304694d695854b", + "sha256": "f793214c47ed40f51708cdeba627d4c0e52397caba262625b29f1dd2cdb7ef81" + }, + { + "path": "research/masked-root-star-assembly/verify.py", + "git_blob": "1433033d60819ee89e3628940fb9979fb8f5a446", + "sha256": "bc79667459069f704c62780540e6ec2d07e8d623e4e52195b75da8eea342fb9d" + }, + { + "path": "research/masked-root-star-assembly/independent.py", + "git_blob": "d2d20b72d6cb71fed6ef066ac278c9515b646f02", + "sha256": "648d2ee846789eafdcc559f7d893a0159b350cbe925fc5de6c5d809a70093a60" + }, + { + "path": "research/masked-root-star-assembly/CERTIFICATE.json", + "git_blob": "ecc639bca2700c78459ec2e0ca9e7b79ecd846b4", + "sha256": "181eddec639da62417f4176fe275d091e243766c5df69ebb35a19482b8155019" + }, + { + "path": "research/masked-root-star-assembly/INDEPENDENT.json", + "git_blob": "9e05eeb5894efa1f0b99451139780dad3bac3fa3", + "sha256": "7fef1341ad21bb951ab79e307ce49fcb99e5acf543ae709c18576a167db67b1a" + }, + { + "path": "research/masked-root-star-assembly/VERIFY.json", + "git_blob": "28e4ea455a59c0e711d6e11afbb12fc3b4311a80", + "sha256": "38c1d591cbcb4745c16e866f6f9949b3cda0960fc5674907106ad8ff3ca38696" + }, + { + "path": "research/masked-root-star-assembly/VALIDATION.md", + "git_blob": "7256129181074290a93ec7808016cb8984c2d397", + "sha256": "f4f76566053369d2ee0d21621075438b4818c1a518360667c3189b3f488e8c96" + }, + { + "path": "research/masked-root-star-assembly/test_package.py", + "git_blob": "db6e785ad338c00dabef0677eaf5253b57fb146b", + "sha256": "e0245b91eb21206c9a09394626e8e582aff228d6cc953e495fcf06bdf928a0f3" + } + ] + }, + { + "pr": 1226, + "author": "Navinor", + "commit": "8b10989e4e45f0f9ce41004d7898a21a32f87e11", + "repository": "https://github.com/navinor/integer-mult-bounds", + "usage": "Provenance only; independently reconstruct all mathematical premises, no imports or runtime dependency.", + "files": [ + { + "path": "research/masked-root-star-floor/README.md", + "usage": "provenance", + "git_blob": "5440a1de61154bbf2185c7799226012323c027b4", + "sha256": "df3dcacbed655a25dbc71a2761aa43e5b87abe95d3ccff39261ee748a24fe13d" + }, + { + "path": "research/masked-root-star-floor/PROOF.md", + "usage": "provenance", + "git_blob": "65604debc38a0cb4bc4b2052e7f1ce336e6cdbd4", + "sha256": "c30adb551579a2df0ad15e6e4485c5beb5a0342b0e89674d349f57ba0f84db4f" + }, + { + "path": "research/masked-root-star-floor/RESULTS.json", + "usage": "provenance", + "git_blob": "1827eb490341fac9a1ff0ed21f46fbdbc86048b8", + "sha256": "de4c6f61f169479aab410b56051776c52a9f2ce191636d5c679a25afdbd1b8bf" + }, + { + "path": "research/masked-root-star-floor/verify.py", + "usage": "provenance", + "git_blob": "7578bc6bc3084ddbed9f1283332129ee40046f28", + "sha256": "dba3a51d57c9c670ab54172a8b345cdd9fb1065c39b6e41f3f3706b15d374283" + } + ] + }, + { + "pr": 1212, + "author": "burntout76", + "commit": "072ae2f43d5c249a31e5d6ed266bfef3924417f3", + "repository": "https://github.com/burntout76/integer-mult-bounds", + "usage": "Overlap context only; theorem not imported or certified here." + }, + { + "pr": 1213, + "author": "DavidAriasC", + "commit": "8867cf20fbe0d3960f68bcffca118a5ac0624f7f", + "repository": "https://github.com/DavidAriasC/integer-mult-bounds", + "usage": "Overlap context only; theorem not imported or certified here." + }, + { + "pr": 1191, + "author": "mightyOil", + "commit": "640b43bb13d3d476a2d83b74ef0d33f14d1b5711", + "repository": "https://github.com/mightyOil/integer-mult-bounds", + "usage": "Overlap context only; theorem not imported or certified here." + }, + { + "pr": 1224, + "author": "joaqcoo", + "commit": "00e6ed0810b8ebc7f6133e2c036d0f1c9a3a4162", + "repository": "https://github.com/joaqcoo/integer-mult-bounds", + "usage": "Overlap context only; theorem not imported or certified here." + } + ] +} diff --git a/research/masked-star-frame-compatibility/TASK.json b/research/masked-star-frame-compatibility/TASK.json new file mode 100644 index 0000000000..7b8a54e59f --- /dev/null +++ b/research/masked-star-frame-compatibility/TASK.json @@ -0,0 +1,61 @@ +{ + "schema_version": 1, + "task_id": "complex-masked-decoder", + "priority_revision": 2, + "base_commit": "49b3157d1d89adcef16df8be98445451672be5ba", + "original_card": { + "id": "complex-masked-decoder", + "question": "Can one specified masked or overcomplete decoder improve the complete moment budget?", + "starting_points": [ + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md" + ], + "methods": [ + "Synthesize a decoder with exact coefficients and fully priced helper endpoints.", + "Bound the best possible budget for a fixed support alphabet before synthesis." + ], + "acceptance_gate": "Change an assumption of the eight-term all-pairs bound and count all copied information, frames and restoration.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-decoder-field-extension-seed44/verify.py" + ], + "expected": "PASS_COMPLEX_DECODER_FIELD_EXTENSION_S44", + "inspect": "Locate the excluded classes: masked identities, at least nine terms, and deeper punctures.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one finite support alphabet and test exact decoding constraints before building a whole network.", + "bottleneck_link": "A cheaper fully realized decoder could increase deficit or lower recursive cost on the binding complex side.", + "allowed_variations": [ + "Select a specific masked or overcomplete family with exact labels and supports." + ], + "scope_change_triggers": [ + "Repeating the exact eight-term all-pairs search inside its proved scope." + ], + "overlap_terms": [ + "masked decoder", + "overcomplete", + "eight-term" + ] + }, + "scope_status": "refined", + "actual_scope": "Independently corroborate the P112 masked root-star cost-64 floor for arbitrary complex coefficients and finite term counts, with a Weyl-orbit/maximal-clique implementation and a Python 3.12 replay of concurrent PR1236.", + "scope_change_reason": "The claim and two implementations were prepared from PR1226. The final live overlap check found concurrent PR1236 had already submitted the same theorem; credit its priority and submit independent corroboration rather than another new-theorem claim.", + "bottleneck_link": "Closes one copied-information reduction mechanism on the binding complex supplier before physical realization; no supplier improvement or kappa change.", + "budget_minutes": 40, + "stop_rule": "Finish one exact finite obstruction with an attaining witness and independent finite checks; no enlarged support search. Reserve at least the final quarter for verification and handoff.", + "outcome": "negative-result", + "evidence": "README.md written proof; CERTIFICATE.json exhaustive premises; verify.py and independent_check.py; test_package.py mutation and relocation checks; VALIDATION.json execution receipt.", + "author": "Hanson Sun (@bbMisk)", + "ai_assistance": "Substantial OpenAI Codex assistance in proof development, implementation, experiments and documentation; no independent human review claimed.", + "open_questions": [ + { + "question": "Can one additional live-line deletion from a self-trimmed root star reduce the complete masked-decoder cost?", + "why_it_matters": "This changes the support class closed here and may admit atoms of smaller rank or different missed-frame patterns on the binding complex side.", + "first_step": "Compute exact atom ranks and missed-frame signatures for this enlarged alphabet before coefficient synthesis.", + "blocked_by": "No exact decoder, favorable complete recursive budget or legal physical realization has been established for the enlarged family." + } + ], + "contribution_kind": "independent verification / scoped negative result" +} diff --git a/research/masked-star-frame-compatibility/VALIDATION.json b/research/masked-star-frame-compatibility/VALIDATION.json new file mode 100644 index 0000000000..0e4f652e02 --- /dev/null +++ b/research/masked-star-frame-compatibility/VALIDATION.json @@ -0,0 +1,166 @@ +{ + "schema_version": 1, + "date_utc": "2026-10-13T21:00:48.338701+00:00", + "base_commit": "49b3157d1d89adcef16df8be98445451672be5ba", + "platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O", + "machine": "arm64", + "primary_python": "3.14.6", + "registered_python": "Python 3.12.13", + "files_sha256": { + "verify.py": "4b83a0518add3d093bd40bcafbeb6bcc00d2b5170beecdf32d01680d903fe069", + "independent_check.py": "d4d367f4414334c24c2cb4ff6262352cdce626270f66c676bed5b9d62980347b", + "test_package.py": "3c234c2cc5dccecad7bf86b024224a68940a91b50acc3dea38e81d868a1d4d8a", + "CERTIFICATE.json": "83578f9bd6ba44cd24b170591ac2d0dc67a6e104ce97c3773702da3685b465db" + }, + "executions": [ + { + "command": "python3 -I -B research/masked-star-frame-compatibility/test_package.py", + "python": "3.14.6", + "commit": "contribution on recorded base", + "exit_code": 0, + "output": "PASS_MASKED_STAR_FRAME_COMPATIBILITY atoms=57600 frames=1260 max_clique=8 cost_floor=64 controls=7\nPASS_INDEPENDENT_MASKED_STAR weyl_roots=240 atoms=57600 frames=1260 maximal_cliques={3: 896, 7: 23040, 8: 4032} cost_floor=64\nPASS_MUTATION_REJECTED under-counted-rank-seven both_checkers\nPASS_MUTATION_REJECTED false-nine-clique both_checkers\nPASS_MUTATION_REJECTED repeated-clique-vertex both_checkers\nPASS_MASKED_STAR_FRAME_COMPATIBILITY atoms=57600 frames=1260 max_clique=8 cost_floor=64 controls=7\nPASS_INDEPENDENT_MASKED_STAR weyl_roots=240 atoms=57600 frames=1260 maximal_cliques={3: 896, 7: 23040, 8: 4032} cost_floor=64\nPASS_MASKED_STAR_PACKAGE mutations=3 rejected_by_both=6 isolated_relocation=yes certificate_unchanged=yes\n" + }, + { + "command": "python3.12 scripts/research_package.py --package research/masked-star-frame-compatibility", + "python": "3.12.13", + "commit": "contribution on recorded base", + "exit_code": 0, + "output": "CHECK Recompute all exact finite premises with two separate implementations, test the cost-64 attaining decoder, reject three certificate corruptions with both checkers, and replay standalone under optimized Python in a path containing spaces.\nPASS_MASKED_STAR_FRAME_COMPATIBILITY atoms=57600 frames=1260 max_clique=8 cost_floor=64 controls=7\nPASS_INDEPENDENT_MASKED_STAR weyl_roots=240 atoms=57600 frames=1260 maximal_cliques={3: 896, 7: 23040, 8: 4032} cost_floor=64\nPASS_MUTATION_REJECTED under-counted-rank-seven both_checkers\nPASS_MUTATION_REJECTED false-nine-clique both_checkers\nPASS_MUTATION_REJECTED repeated-clique-vertex both_checkers\nPASS_MASKED_STAR_FRAME_COMPATIBILITY atoms=57600 frames=1260 max_clique=8 cost_floor=64 controls=7\nPASS_INDEPENDENT_MASKED_STAR weyl_roots=240 atoms=57600 frames=1260 maximal_cliques={3: 896, 7: 23040, 8: 4032} cost_floor=64\nPASS_MASKED_STAR_PACKAGE mutations=3 rejected_by_both=6 isolated_relocation=yes certificate_unchanged=yes\nPASS_REGISTERED_RESEARCH_PACKAGE research/masked-star-frame-compatibility outcome=negative-result\n" + }, + { + "command": "python3.12 scripts/research_package.py --package research/masked-root-star-assembly", + "python": "3.12.13", + "commit": "ee8437bd9879272094e20c024cd34a53c4e84cd8", + "exit_code": 0, + "output": "CHECK Complete atom and frame census, odd-clique obstruction, sharp decoder and eight controls.\nPASS_MASKED_ROOT_STAR_ASSEMBLY_FLOOR_64 atoms=57600 frames=1260 max_odd_clique=8 controls=8\nCHECK Separate dense/lattice/quadratic verification and five controls.\nPASS_MASKED_ROOT_STAR_INDEPENDENT frames=1260 pairs=57600 quadratic_dimension=8 floor=64 controls=5\nCHECK Optimized relocated read-only replay and changed or missing receipt rejection.\ntest_independent_optimized_relocated_read_only (__main__.PackageControls.test_independent_optimized_relocated_read_only) ... ok\ntest_independent_receipts_agree_on_proof_premises (__main__.PackageControls.test_independent_receipts_agree_on_proof_premises) ... ok\ntest_independent_rejects_changed_quadratic_premise (__main__.PackageControls.test_independent_rejects_changed_quadratic_premise) ... ok\ntest_independent_rejects_missing_receipt (__main__.PackageControls.test_independent_rejects_missing_receipt) ... ok\ntest_primary_optimized_relocated_read_only (__main__.PackageControls.test_primary_optimized_relocated_read_only) ... ok\ntest_primary_rejects_changed_atom_count (__main__.PackageControls.test_primary_rejects_changed_atom_count) ... ok\ntest_primary_rejects_missing_receipt (__main__.PackageControls.test_primary_rejects_missing_receipt) ... ok\n\n----------------------------------------------------------------------\nRan 7 tests in 23.456s\n\nOK\nPASS_REGISTERED_RESEARCH_PACKAGE research/masked-root-star-assembly outcome=negative-result\n" + }, + { + "command": "make selected-record-check", + "python": "3.14.6", + "commit": "contribution on recorded base", + "exit_code": 0, + "output": "python3 -B scripts/verify_selected_result.py\nPASS selected record, exact kappa, original source inventory and proof supplement: 836330098538459/500000000000000000\n" + } + ], + "pr1236_agreement": { + "head": "ee8437bd9879272094e20c024cd34a53c4e84cd8", + "all_equal": true, + "fields": { + "live_lines": 112, + "frames": 1260, + "orthogonal_pair_extensions": { + "10": 2856, + "15": 448 + }, + "rank_histogram": { + "7": 7616, + "8": 37440, + "9": 12544 + }, + "rank7_live_normal_histogram": { + "1": 1792, + "2": 5824 + }, + "all_clique_counts": { + "0": 1, + "1": 112, + "2": 2912, + "3": 25088, + "4": 88704, + "5": 161280, + "6": 145152, + "7": 55296, + "8": 4032 + }, + "coordinate_costs": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + "checked_coordinate_entries": 12544 + } + }, + "overlap": { + "coverage": { + "open_prs": { + "fetched_at": "2026-10-13T20:55:56.078730+00:00", + "complete_pagination": true, + "records": 843 + }, + "discussions": { + "fetched_at": "2026-10-13T20:55:59.278025+00:00", + "complete_pagination": true, + "records": 14 + } + }, + "newest_check": [ + { + "created_at": "2026-10-13T20:52:50Z", + "head": "77dc486aafa0ce89c0af8b7bc012adb40a933fda", + "number": 1240, + "title": "Research note: packing ceiling (+0.87%) and 1/99 budget for the selected complex local word (no new kappa)" + }, + { + "created_at": "2026-10-13T20:51:29Z", + "head": "12e04a30d7381a2a60bf2d7260febcb37f14e454", + "number": 1239, + "title": "Conditional \u03ba = 0.001675809683500501: source-holder fusions and X54 on #1193's mixed T37 construction (independent; equals #1218)" + }, + { + "created_at": "2026-10-13T20:48:02Z", + "head": "50a1c992ce28c95d83d11bc691353aaa289d9d65", + "number": 1238, + "title": "The end-cap wall: why copies are forced in the E8 skeleton's verifier model (no \u03ba claim)" + }, + { + "created_at": "2026-10-13T20:46:58Z", + "head": "ee8437bd9879272094e20c024cd34a53c4e84cd8", + "number": 1236, + "title": "Research: close the masked root-star assembly gap with sharp cost 64 (no new kappa)" + }, + { + "created_at": "2026-10-13T20:46:42Z", + "head": "3941a3c63651d379feceb411019c30310e9e12d0", + "number": 1235, + "title": "research: reduce calibrated endpoint gauges to exact source tours" + }, + { + "created_at": "2026-10-13T20:46:27Z", + "head": "8812ca21c43f5cea16276c7fa539fa8d1559b0f1", + "number": 1234, + "title": "perf: streamline exact rational frame normalization and complements" + }, + { + "created_at": "2026-10-13T20:45:28Z", + "head": "1a0ecf7f534a67a910b7b5a7e0abe46be074c609", + "number": 1232, + "title": "Consolidation: stop historical status sections from claiming to be current (no new kappa)" + }, + { + "created_at": "2026-10-13T20:42:26Z", + "head": "448690c3b7e5c2b5975b760075b162fe0a8cfb03", + "number": 1231, + "title": "[Lean] Derive #540's pending ranges from the PR442 schedule (stacked on #540; no new kappa)" + } + ], + "disposition": "PR1236 submitted the same theorem during this session. This contribution is independent corroboration, with Weyl-orbit/maximal-clique evidence and a successful Python 3.12 registered replay of that exact head.", + "limits": "Full initial/final pagination of open PR bodies and discussions; local README/TASK/ledger search. Not every code diff or arbitrary nested file was searched." + }, + "not_run": [ + "Full selected supplier cold replay", + "Repository-wide historical suite", + "Lean proof", + "Hosted CI at local validation time" + ], + "result_scope": "Independent exact finite corroboration; no new kappa, no physical supplier admission and no independent human review.", + "orientation_controls": { + "research_baseline": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY; complex binding; selected source inventory and arithmetic only.", + "field_extension": "PASS_COMPLEX_DECODER_FIELD_EXTENSION_S44 p=0..24 examples=3 attaining=25 pairing=14400 controls=7", + "pr1226": "Pinned verify.py and RESULTS.json replayed under -I -O -B; 28 PASS lines and FAILS: none; source head unchanged at pre-submission refresh." + } +} diff --git a/research/masked-star-frame-compatibility/VERIFY.json b/research/masked-star-frame-compatibility/VERIFY.json new file mode 100644 index 0000000000..36984b9314 --- /dev/null +++ b/research/masked-star-frame-compatibility/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 180, + "checks": "Recompute all exact finite premises with two separate implementations, test the cost-64 attaining decoder, reject three certificate corruptions with both checkers, and replay standalone under optimized Python in a path containing spaces." + } + ] +} diff --git a/research/masked-star-frame-compatibility/independent_check.py b/research/masked-star-frame-compatibility/independent_check.py new file mode 100644 index 0000000000..d7f9850c22 --- /dev/null +++ b/research/masked-star-frame-compatibility/independent_check.py @@ -0,0 +1,180 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Separate finite checker: Weyl orbit, column elimination, maximal cliques. + +No imports from verify.py or predecessor packages. This is implementation +independence within one AI-assisted contribution, not independent human review. +""" + +import argparse +from collections import Counter +from itertools import combinations +import json +from pathlib import Path +import sys + + +def ensure(condition, message): + if not condition: + raise ValueError(message) + + +def scalar(a, b): + return sum(x * y for x, y in zip(a, b)) + + +def weyl_lines(): + simple = [(1, -1, -1, -1, -1, -1, -1, 1), (2, 2, 0, 0, 0, 0, 0, 0)] + for i in range(6): + root = [0] * 8 + root[i], root[i + 1] = -2, 2 + simple.append(tuple(root)) + found = {simple[0]} + pending = [simple[0]] + while pending: + r = pending.pop() + for a in simple: + pairing = scalar(r, a) + ensure(pairing % 4 == 0, "reflection integrality") + reflected = tuple(x - (pairing // 4) * y for x, y in zip(r, a)) + ensure(scalar(reflected, reflected) == 8, "reflection norm") + if reflected not in found: + found.add(reflected) + pending.append(reflected) + ensure(len(found) == 240, "Weyl orbit size") + return sorted(r for r in found if next(x for x in r if x) > 0) + + +def binary_column_rank(columns): + # Lowest-pivot column elimination, instead of the primary row-echelon routine. + columns = set(columns) - {0} + dimension = 0 + while columns: + pivot = min(columns) + columns.remove(pivot) + low = pivot & -pivot + columns = {v ^ pivot if v & low else v for v in columns} - {0} + dimension += 1 + return dimension + + +def maximal_cliques(neighbors, order): + """Bron-Kerbosch with excluded vertices and a maximum-neighbor pivot.""" + position = {v: i for i, v in enumerate(order)} + result = [] + + def extend(chosen, possible, excluded): + if not possible and not excluded: + result.append(tuple(sorted(chosen))) + return + pivot = max(possible | excluded, + key=lambda v: (len(possible & neighbors[v]), -position[v])) + for v in sorted(possible - neighbors[pivot], key=position.get): + extend(chosen + [v], possible & neighbors[v], excluded & neighbors[v]) + possible.remove(v) + excluded.add(v) + + extend([], set(order), set()) + return sorted(result) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--certificate", type=Path, + default=Path(__file__).with_name("CERTIFICATE.json")) + args = parser.parse_args() + try: + receipt = json.loads(args.certificate.read_text()) + roots = weyl_lines() + ensure(len(roots) == 120, "root-line count") + gram = [[scalar(a, b) // 4 for b in roots] for a in roots] + puncture = [] + for i, r in enumerate(roots): + support = [j for j, x in enumerate(r) if x] + if len(support) == 2 and support[0] % 2 == 0 and support[1] == support[0] + 1: + puncture.append(i) + ensure(puncture == receipt["puncture"] and len(puncture) == 8, "puncture") + live = set(range(120)) - set(puncture) + order = sorted(live) + # Seed 36 diversifies the vertex order, not the mathematical domain. + order = order[36:] + order[:36] + orth = {i: {j for j in live if i != j and gram[i][j] == 0} for i in live} + nonorth = {i: live - orth[i] - {i} for i in live} + orth_maximal = maximal_cliques(orth, order) + frames = [f for f in orth_maximal if len(f) == 8] + ensure(len(frames) == receipt["frames"] == 1260, "independent frame census") + ensure(max(map(len, orth_maximal)) == 8, "orthogonal rank bound") + membership = {i: {k for k, f in enumerate(frames) if i in f} for i in live} + ensure({len(x) for x in membership.values()} == {90}, "normal/frame coverage") + extension_counts = [] + for i, j in combinations(sorted(live), 2): + common = membership[i] & membership[j] + ensure(bool(common) == (gram[i][j] == 0), "pair/frame extension") + if common: + extension_counts.append(len(common)) + ensure({str(k): v for k, v in Counter(extension_counts).items()} + == receipt["orthogonal_pair_extension_histogram"], "extension histogram") + + columns = [sum(((gram[i][j] + 1) % 2) << i for i in range(120)) + for j in range(120)] + supports = [] + for a in range(120): + full = {i for i in live if gram[i][a] != 0} + for trimmed in (False, True): + s = full - {a} if trimmed else full + supports.append((a, trimmed, s)) + missing = {k for k, f in enumerate(frames) if not s.intersection(f)} + ensure(missing == (membership.get(a, set()) if trimmed else set()), + "independent star/frame identity") + rank_histogram = Counter() + rank_cache = {} + for a, ta, s in supports: + row_mask = sum(1 << i for i in s) + for b, tb, t in supports: + col_mask = sum(1 << j for j in t) + key = (row_mask, col_mask) + if key not in rank_cache: + rank_cache[key] = binary_column_rank(columns[j] & row_mask for j in t) + beta = rank_cache[key] + rank_histogram[beta] += 1 + classified = (gram[a][b] in (-1, 1) and (ta or a not in live) + and (tb or b not in live)) + ensure((beta == 7) == classified, "independent rank-seven classification") + ensure(dict(rank_histogram) == {7: 7616, 8: 37440, 9: 12544}, "independent atom floor") + ensure({str(k): v for k, v in rank_histogram.items()} == receipt["rank_histogram"], + "rank receipt mismatch") + + maximal = maximal_cliques(nonorth, order) + histogram = Counter(map(len, maximal)) + ensure(max(histogram) == receipt["maximum_nonorthogonal_clique"] == 8, + "independent nine-normal exclusion") + witness = receipt["maximum_clique_witness"] + ensure(len(set(witness)) == 8 and set(witness) <= live + and all(gram[i][j] != 0 for i, j in combinations(witness, 2)), "clique witness") + complete9 = {i: set(range(9)) - {i} for i in range(9)} + ensure(maximal_cliques(complete9, list(range(9))) == [tuple(range(9))], + "synthetic nine-clique control") + ensure(binary_column_rank([0, 1, 2, 3]) == 2 + and binary_column_rank([0, 1, 2, 3, 4]) == 3, "rank mutation control") + + # Independently check the attaining 8-term construction and every charged support. + for i in live: + for j in live: + ensure(sum(gram[i][f] * gram[j][f] for f in puncture) == 2 * gram[i][j], + "independent coordinate identity") + for f in puncture: + s = {i for i in live if gram[i][f]} + mask = sum(1 << i for i in s) + ensure(binary_column_rank(columns[j] & mask for j in s) == 8, + "independent coordinate price") + ensure(receipt["cost_floor"] == 64, "claimed cost floor") + except (ValueError, OSError, KeyError, TypeError) as error: + print(f"FAIL_INDEPENDENT_MASKED_STAR: {error}", file=sys.stderr) + return 1 + print("PASS_INDEPENDENT_MASKED_STAR weyl_roots=240 atoms=57600 frames=1260 " + f"maximal_cliques={dict(sorted(histogram.items()))} cost_floor=64") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/masked-star-frame-compatibility/test_package.py b/research/masked-star-frame-compatibility/test_package.py new file mode 100644 index 0000000000..9d69bc583e --- /dev/null +++ b/research/masked-star-frame-compatibility/test_package.py @@ -0,0 +1,71 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Bounded replay and adversarial certificate checks; Python standard library.""" + +import copy +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent + + +def run(script, certificate, expected_code, marker): + result = subprocess.run( + [sys.executable, "-I", "-O", "-B", str(script), "--certificate", str(certificate)], + cwd=certificate.parent, capture_output=True, text=True, timeout=60) + if result.returncode != expected_code or marker not in result.stdout + result.stderr: + raise ValueError(f"unexpected result for {script.name}: {result.returncode}\n" + + result.stdout + result.stderr) + if expected_code == 0: + print(result.stdout.strip(), flush=True) + + +def main(): + source = HERE / "CERTIFICATE.json" + original = source.read_bytes() + certificate = json.loads(original) + for name, marker in (("verify.py", "PASS_MASKED_STAR_FRAME_COMPATIBILITY"), + ("independent_check.py", "PASS_INDEPENDENT_MASKED_STAR")): + run(HERE / name, source, 0, marker) + with tempfile.TemporaryDirectory(prefix="masked star controls ") as temporary: + root = Path(temporary) + mutants = [] + mutant = copy.deepcopy(certificate) + mutant["rank_histogram"]["7"] -= 1 + mutants.append(("under-counted-rank-seven", mutant)) + mutant = copy.deepcopy(certificate) + mutant["maximum_nonorthogonal_clique"] = 9 + mutants.append(("false-nine-clique", mutant)) + mutant = copy.deepcopy(certificate) + mutant["maximum_clique_witness"][1] = mutant["maximum_clique_witness"][0] + mutants.append(("repeated-clique-vertex", mutant)) + for label, mutant in mutants: + path = root / (label + ".json") + path.write_text(json.dumps(mutant)) + for name, marker in (("verify.py", "FAIL_MASKED_STAR_FRAME_COMPATIBILITY"), + ("independent_check.py", "FAIL_INDEPENDENT_MASKED_STAR")): + run(HERE / name, path, 1, marker) + print(f"PASS_MUTATION_REJECTED {label} both_checkers", flush=True) + relocated = root / "standalone package with spaces" + relocated.mkdir() + for name in ("verify.py", "independent_check.py", "CERTIFICATE.json"): + shutil.copyfile(HERE / name, relocated / name) + run(relocated / "verify.py", relocated / "CERTIFICATE.json", 0, + "PASS_MASKED_STAR_FRAME_COMPATIBILITY") + run(relocated / "independent_check.py", relocated / "CERTIFICATE.json", 0, + "PASS_INDEPENDENT_MASKED_STAR") + if source.read_bytes() != original: + raise ValueError("verification changed the committed certificate") + print("PASS_MASKED_STAR_PACKAGE mutations=3 rejected_by_both=6 isolated_relocation=yes certificate_unchanged=yes") + + +if __name__ == "__main__": + try: + main() + except (ValueError, OSError, subprocess.TimeoutExpired) as error: + print(f"FAIL_MASKED_STAR_PACKAGE: {error}", file=sys.stderr) + raise SystemExit(1) diff --git a/research/masked-star-frame-compatibility/verify.py b/research/masked-star-frame-compatibility/verify.py new file mode 100644 index 0000000000..251d399e88 --- /dev/null +++ b/research/masked-star-frame-compatibility/verify.py @@ -0,0 +1,240 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact finite premises for the P112 masked root-star cost floor. + +Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance. +See README.md for the written argument, scope and predecessor credit. +No predecessor executable is imported. Python 3.10+, standard library. +""" + +import argparse +from collections import Counter +import hashlib +from itertools import combinations, product +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def digest(value): + return hashlib.sha256(json.dumps(value, separators=(",", ":")).encode()).hexdigest() + + +def bits(mask): + while mask: + bit = mask & -mask + yield bit.bit_length() - 1 + mask ^= bit + + +def rank2(rows): + pivots = {} + for row in rows: + while row: + pivot = row.bit_length() - 1 + if pivot not in pivots: + pivots[pivot] = row + break + row ^= pivots[pivot] + return len(pivots) + + +def model(): + # Twice the usual norm-two roots; choose the first nonzero coordinate positive. + roots = set() + for i, j in combinations(range(8), 2): + for sign in (-1, 1): + v = [0] * 8 + v[i], v[j] = 2, 2 * sign + roots.add(tuple(v)) + for tail in product((-1, 1), repeat=7): + if tail.count(-1) % 2 == 0: + roots.add((1,) + tail) + roots = sorted(roots) + require(len(roots) == 120, "root-line count") + gram = [] + for r in roots: + row = [] + for s in roots: + q, rem = divmod(sum(x * y for x, y in zip(r, s)), 4) + require(rem == 0, "nonintegral root pairing") + row.append(q) + gram.append(row) + puncture = [] + for i in range(0, 8, 2): + for sign in (-1, 1): + v = [0] * 8 + v[i], v[i + 1] = 2, 2 * sign + puncture.append(roots.index(tuple(v))) + puncture.sort() + live = [i for i in range(120) if i not in puncture] + require(all(gram[i][i] == 2 for i in range(120)), "root norms") + require(all(gram[i][j] == 0 for i, j in combinations(puncture, 2)), "punctured frame") + return roots, gram, puncture, live + + +def clique_census(adjacency, vertices, collect_size=None): + """Enumerate *all* cliques, with no depth cutoff; visit each in increasing order.""" + counts = Counter() + witness = [] + collected = [] + + def visit(chosen, candidates): + nonlocal witness + counts[len(chosen)] += 1 + if len(chosen) > len(witness): + witness = chosen + if len(chosen) == collect_size: + collected.append(chosen) + while candidates: + bit = candidates & -candidates + candidates ^= bit + v = bit.bit_length() - 1 + visit(chosen + [v], candidates & adjacency[v]) + + visit([], sum(1 << i for i in vertices)) + return counts, witness, collected + + +def check_decoder(gram, live, left, right): + return all(sum(d[i] * t[j] for d, t in zip(left, right)) == 2 * gram[i][j] + for i in live for j in live) + + +def compute(): + roots, gram, puncture, live = model() + label_rows = [sum(((g + 1) % 2) << j for j, g in enumerate(row)) for row in gram] + require(rank2(label_rows) == 9, "label rank") + orth = {i: sum(1 << j for j in live if i != j and gram[i][j] == 0) for i in live} + nonorth = {i: sum(1 << j for j in live if i != j and gram[i][j] != 0) for i in live} + _, _, frames = clique_census(orth, live, 8) + require(len(frames) == 1260, "frame census") + frame_masks = [sum(1 << i for i in f) for f in frames] + appearances = Counter(i for f in frames for i in f) + extensions = Counter(pair for f in frames for pair in combinations(f, 2)) + require(set(appearances.values()) == {90}, "every live normal must lie in a frame") + require(set(extensions) == {(i, j) for i, j in combinations(live, 2) if gram[i][j] == 0}, + "an orthogonal pair has no live-frame extension") + + supports = [] + zeros = [] + for normal in range(120): + untrimmed = sum(1 << i for i in live if gram[i][normal] != 0) + for trimmed in (False, True): + support = untrimmed & ~(1 << normal) if trimmed else untrimmed + supports.append((normal, trimmed, support)) + zero = [k for k, fm in enumerate(frame_masks) if not support & fm] + expected = [k for k, f in enumerate(frames) if trimmed and normal in f] + require(zero == expected, "star/frame annihilation classification") + zeros.append(zero) + + ranks = [] + rank_hist = Counter() + cheap_types = Counter() + for a, ta, sa in supports: + for b, tb, sb in supports: + beta = rank2(label_rows[i] & sb for i in bits(sa)) + ranks.append(beta) + rank_hist[beta] += 1 + predicted = (abs(gram[a][b]) == 1 and (ta or a in puncture) + and (tb or b in puncture)) + require((beta == 7) == predicted, "rank-seven classification") + if beta == 7: + live_normals = [v for v in (a, b) if v in live] + require(live_normals, "cheap atom without a live trimmed normal") + cheap_types[len(live_normals)] += 1 + require(dict(rank_hist) == {7: 7616, 8: 37440, 9: 12544}, "atom rank census") + + counts, clique, _ = clique_census(nonorth, live) + require(max(counts) == 8, "nine pairwise nonorthogonal live normals exist") + require(all(gram[i][j] != 0 for i, j in combinations(clique, 2)), "clique witness") + + coordinate = [[gram[i][f] for i in range(120)] for f in puncture] + require(check_decoder(gram, live, coordinate, coordinate), "coordinate decoder identity") + coordinate_costs = [] + for d in coordinate: + support = sum(1 << i for i in live if d[i]) + coordinate_costs.append(rank2(label_rows[i] & support for i in bits(support))) + require(coordinate_costs == [8] * 8, "cost-64 attaining decoder") + + # Failure controls address mathematical boundaries, rather than code formatting. + controls = [] + damaged = [row[:] for row in coordinate] + k, i = next((k, i) for k, row in enumerate(damaged) for i in live if row[i]) + damaged[k][i] += 1 + require(not check_decoder(gram, live, damaged, coordinate), "coefficient mutation escaped") + controls.append("changed_coordinate_coefficient_rejected") + require(not check_decoder(gram, live, [], []), "zero decoder escaped diagonal constraint") + controls.append("zero_decoder_rejected_by_diagonal") + full9 = {i: ((1 << 9) - 1) ^ (1 << i) for i in range(9)} + nine_counts, nine, _ = clique_census(full9, list(range(9))) + require(len(nine) == 9 and nine_counts[9] == 1, "clique search silently stops at eight") + controls.append("synthetic_K9_detected_without_depth_cutoff") + first = live[0] + singleton = 1 << first + require(singleton not in {s for _, _, s in supports} + and rank2([label_rows[first] & singleton]) == 1, "outside-family boundary") + controls.append("rank_one_singleton_outside_star_family") + repeated_frame = next(f for f in frames if first in f) + require(not (sum(1 << i for i in live if gram[i][first] and i != first) + & sum(1 << i for i in repeated_frame)), "repeated normal not annihilated") + controls.append("repeated_normal_has_shared_zero_frame") + pair = min(extensions) + shared = next(f for f in frames if all(i in f for i in pair)) + require(all(not any(gram[i][a] for i in shared if i != a) for a in pair), + "orthogonal normals not annihilated") + controls.append("orthogonal_normals_have_shared_zero_frame") + odd_pair = next((i, j) for i in live for j in live if gram[i][j] % 2) + require(rank2([label_rows[odd_pair[0]] & (1 << odd_pair[1])]) == 0 + and not any(all(i in f for i in odd_pair) for f in frames), "free odd repair hits frame") + controls.append("free_odd_entry_patch_vanishes_on_every_frame") + + return { + "schema": "masked-star-frame-compatibility-v1", + "scope": "P112; exact C(alpha)/N(alpha) supports; ordinary complex transpose; arbitrary finite term count", + "lines": 120, "live_lines": 112, "label_rank": 9, + "roots_sha256": digest(roots), "puncture": puncture, + "frames": len(frames), "frames_sha256": digest(frames), + "frames_per_line": 90, + "orthogonal_pair_extension_histogram": dict(sorted(Counter(extensions.values()).items())), + "ordered_support_pairs": len(ranks), "support_labels": len(supports), + "distinct_supports": len({s for _, _, s in supports}), + "rank_histogram": dict(sorted(rank_hist.items())), "ranks_sha256": digest(ranks), + "rank7_live_normal_count_histogram": dict(sorted(cheap_types.items())), + "star_zero_frames_sha256": digest(zeros), + "nonorthogonal_clique_counts": dict(sorted(counts.items())), + "maximum_nonorthogonal_clique": len(clique), "maximum_clique_witness": clique, + "maximum_clique_root_vectors": [roots[i] for i in clique], + "coordinate_decoder_costs": coordinate_costs, "coordinate_decoder_entries": len(live) ** 2, + "cost_floor": 64, "controls": controls, + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="regenerate the package certificate") + parser.add_argument("--certificate", type=Path, default=HERE / "CERTIFICATE.json") + args = parser.parse_args() + try: + actual = json.loads(json.dumps(compute())) + if args.write: + args.certificate.write_text(json.dumps(actual, indent=2) + "\n") + else: + require(json.loads(args.certificate.read_text()) == actual, + "certificate differs from exact recomputation") + except (ValueError, OSError, KeyError, TypeError) as error: + print(f"FAIL_MASKED_STAR_FRAME_COMPATIBILITY: {error}", file=sys.stderr) + return 1 + print("PASS_MASKED_STAR_FRAME_COMPATIBILITY atoms=57600 frames=1260 max_clique=8 cost_floor=64 controls=7") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())