From 7653e0cc72527c1e7fc02499122d383713ee9d54 Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Wed, 14 Oct 2026 23:32:25 -0500 Subject: [PATCH] Add exact two-frame shared correction census --- .../CERTIFICATE.json | 486 ++++++++++++++++++ .../cycle47-shared-frame-correction/README.md | 102 ++++ .../SOURCES.json | 54 ++ .../cycle47-shared-frame-correction/TASK.json | 95 ++++ .../VERIFY.json | 22 + .../cycle47-shared-frame-correction/verify.py | 341 ++++++++++++ 6 files changed, 1100 insertions(+) create mode 100644 research/cycle47-shared-frame-correction/CERTIFICATE.json create mode 100644 research/cycle47-shared-frame-correction/README.md create mode 100644 research/cycle47-shared-frame-correction/SOURCES.json create mode 100644 research/cycle47-shared-frame-correction/TASK.json create mode 100644 research/cycle47-shared-frame-correction/VERIFY.json create mode 100644 research/cycle47-shared-frame-correction/verify.py diff --git a/research/cycle47-shared-frame-correction/CERTIFICATE.json b/research/cycle47-shared-frame-correction/CERTIFICATE.json new file mode 100644 index 0000000000..1aa8ddab0e --- /dev/null +++ b/research/cycle47-shared-frame-correction/CERTIFICATE.json @@ -0,0 +1,486 @@ +{ + "q_to_line": [ + { + "q": 11, + "line": 2 + }, + { + "q": 13, + "line": 6 + }, + { + "q": 14, + "line": 56 + }, + { + "q": 19, + "line": 7 + }, + { + "q": 21, + "line": 3 + }, + { + "q": 22, + "line": 76 + }, + { + "q": 26, + "line": 92 + }, + { + "q": 28, + "line": 104 + }, + { + "q": 35, + "line": 63 + }, + { + "q": 37, + "line": 75 + }, + { + "q": 38, + "line": 16 + }, + { + "q": 41, + "line": 91 + }, + { + "q": 44, + "line": 36 + }, + { + "q": 49, + "line": 111 + }, + { + "q": 50, + "line": 37 + }, + { + "q": 56, + "line": 17 + }, + { + "q": 67, + "line": 69 + }, + { + "q": 69, + "line": 81 + }, + { + "q": 70, + "line": 20 + }, + { + "q": 73, + "line": 97 + }, + { + "q": 74, + "line": 30 + }, + { + "q": 81, + "line": 117 + }, + { + "q": 84, + "line": 31 + }, + { + "q": 88, + "line": 21 + }, + { + "q": 98, + "line": 114 + }, + { + "q": 100, + "line": 102 + }, + { + "q": 104, + "line": 86 + }, + { + "q": 112, + "line": 66 + }, + { + "q": 131, + "line": 70 + }, + { + "q": 133, + "line": 82 + }, + { + "q": 134, + "line": 22 + }, + { + "q": 137, + "line": 98 + }, + { + "q": 138, + "line": 32 + }, + { + "q": 140, + "line": 46 + }, + { + "q": 145, + "line": 118 + }, + { + "q": 146, + "line": 47 + }, + { + "q": 148, + "line": 33 + }, + { + "q": 152, + "line": 23 + }, + { + "q": 161, + "line": 52 + }, + { + "q": 162, + "line": 113 + }, + { + "q": 164, + "line": 101 + }, + { + "q": 168, + "line": 85 + }, + { + "q": 176, + "line": 65 + }, + { + "q": 191, + "line": 53 + }, + { + "q": 193, + "line": 42 + }, + { + "q": 194, + "line": 107 + }, + { + "q": 196, + "line": 95 + }, + { + "q": 200, + "line": 79 + }, + { + "q": 208, + "line": 59 + }, + { + "q": 223, + "line": 43 + }, + { + "q": 224, + "line": 12 + }, + { + "q": 239, + "line": 108 + }, + { + "q": 247, + "line": 88 + }, + { + "q": 251, + "line": 72 + }, + { + "q": 253, + "line": 60 + }, + { + "q": 254, + "line": 13 + }, + { + "q": 259, + "line": 71 + }, + { + "q": 261, + "line": 83 + }, + { + "q": 262, + "line": 24 + }, + { + "q": 265, + "line": 99 + }, + { + "q": 266, + "line": 34 + }, + { + "q": 268, + "line": 48 + }, + { + "q": 273, + "line": 119 + }, + { + "q": 274, + "line": 49 + }, + { + "q": 276, + "line": 35 + }, + { + "q": 280, + "line": 25 + }, + { + "q": 289, + "line": 50 + }, + { + "q": 290, + "line": 112 + }, + { + "q": 292, + "line": 100 + }, + { + "q": 296, + "line": 84 + }, + { + "q": 304, + "line": 64 + }, + { + "q": 319, + "line": 51 + }, + { + "q": 321, + "line": 40 + }, + { + "q": 322, + "line": 106 + }, + { + "q": 324, + "line": 94 + }, + { + "q": 328, + "line": 78 + }, + { + "q": 336, + "line": 58 + }, + { + "q": 351, + "line": 41 + }, + { + "q": 352, + "line": 10 + }, + { + "q": 367, + "line": 109 + }, + { + "q": 375, + "line": 89 + }, + { + "q": 379, + "line": 73 + }, + { + "q": 381, + "line": 61 + }, + { + "q": 382, + "line": 11 + }, + { + "q": 385, + "line": 38 + }, + { + "q": 386, + "line": 105 + }, + { + "q": 388, + "line": 93 + }, + { + "q": 392, + "line": 77 + }, + { + "q": 400, + "line": 57 + }, + { + "q": 415, + "line": 39 + }, + { + "q": 416, + "line": 8 + }, + { + "q": 431, + "line": 110 + }, + { + "q": 439, + "line": 90 + }, + { + "q": 443, + "line": 74 + }, + { + "q": 445, + "line": 62 + }, + { + "q": 446, + "line": 9 + }, + { + "q": 448, + "line": 4 + }, + { + "q": 463, + "line": 116 + }, + { + "q": 471, + "line": 96 + }, + { + "q": 475, + "line": 80 + }, + { + "q": 477, + "line": 68 + }, + { + "q": 478, + "line": 5 + }, + { + "q": 487, + "line": 28 + }, + { + "q": 491, + "line": 18 + }, + { + "q": 493, + "line": 14 + }, + { + "q": 494, + "line": 67 + }, + { + "q": 499, + "line": 15 + }, + { + "q": 501, + "line": 19 + }, + { + "q": 502, + "line": 87 + }, + { + "q": 505, + "line": 29 + }, + { + "q": 506, + "line": 103 + }, + { + "q": 508, + "line": 115 + } + ], + "witness": { + "r_bits": [ + 0, + 0, + 1, + 0, + 0, + 0, + 1, + 0 + ], + "frames": [ + [ + 2, + 3, + 16, + 17, + 46, + 47, + 52, + 53 + ], + [ + 2, + 3, + 20, + 21, + 42, + 43, + 46, + 47 + ] + ] + } +} diff --git a/research/cycle47-shared-frame-correction/README.md b/research/cycle47-shared-frame-correction/README.md new file mode 100644 index 0000000000..ce4703c666 --- /dev/null +++ b/research/cycle47-shared-frame-correction/README.md @@ -0,0 +1,102 @@ +# Shared correction basis for two plane-upgraded frames + +**Exact local mechanism; no new κ or complete supplier.** This package answers a follow-up to the +single-frame plane-upgrade probe in [Discussion #2278](https://github.com/CrocSwap/integer-mult-bounds/discussions/2278). +For the selected P112 label set, two distinct orthogonal frames with the same binary direction use +correction matrices in one common rational rank-8 row space. The verifier constructs the coefficient +maps and tests their integrality denominator and F2 support ranks over the complete finite domain. + +## Scope and model + +The input is the selected 112-label `complex-nine-native/DATA-PHASES.json` member. The certificate +maps its 112 q labels bijectively to the 112 live lines of the exact E8 root-line model. It checks the +entire selected-label pairing and all eight deleted-frame signatures before using integer inner +products. For a frame `S` and binary direction `r` with `beta(r,a)=1` on `S`, let + +```text +T(S,r) = { b in P112 \ S : beta(r,b)=0 and is odd for some a in S } +M(S,r)[a,b] = for b in T(S,r), and 0 otherwise. +``` + +Each `M(S,r)` is an exact 8 by 112 correction matrix of rational rank 8. Within each fixed-r +family, `verify.py` chooses one matrix `M0`, computes each exact coefficient matrix `C` from a +fixed nonsingular 8-column minor, and verifies `M=C M0` entrywise. Every family has denominator +LCM 2, so the common basis can be written `B=M0/2` with integer coefficient matrices `D=2C` and +`M=D B`. Their combined F2 row span has rank 4 in every family. Thus every pair in a same-r family +uses one rank-8 rational basis and at most a rank-4 F2 coefficient interface. The witness pair in +`CERTIFICATE.json` has pair coefficient rank 1. This is a finite exact construction, not an +inference from equal ranks. + +The exhaustive domain contains all 1,260 orthogonal frames in P112, all 16 valid r values per frame, +all 135 distinct common directions, and all 1,539,720 same-r unordered frame pairs (20,160 +frame-direction correction blocks). The certificate contains an explicit q-to-line map and a witness +pair; the verifier recomputes the entire census. + +## Cost screen and limits + +The selected local profile is `{1:2412, 2:418, 3:432, 4:142, 5:82, 8:8}` per call, with `m=73`, +896 families, nine stages, centre charge 64, and exact selected ceiling endpoint +`1690054109089/10^15`. At the 5% target `a*=35491136290869/20000000000000000`, the existing exact +ceiling calculator gives: + +| Favorable scenario | Centre charge | Unpaid coordinates/family | Relaxation at a* | Gate | +|---|---:|---:|---:|---| +| One frame with its full correction charge | 72 | 15/14 | 1.000367800102… | fails | +| Two frames with one shared correction charge | 72 | 8/7 | 0.999388703606… | passes | +| Two frames charged independently | 80 | 8/7 | 1.000490187164… | fails | + +These are exact outward intervals from the pinned calculator, displayed as decimals. The passing line +is only a favorable local screen. It does not include source access, copies, hosting, legality and +timing of both frames, interface transitions, restoration, precision/tape charges, all-size +realization, or the matching bit-side construction. The common rational basis has denominator 2; +its precision must be charged in a completed supplier. +Accordingly this package claims a shared correction mechanism, not an admitted local profile, a new +conditional bound, or a κ improvement. + +## Reproduce + +Python 3.10+ and the standard library are enough for the direct verifier: + +```sh +python3 -B research/cycle47-shared-frame-correction/verify.py +``` + +Expected final line: + +```text +PASS_CYCLE47_SHARED_FRAME_CORRECTION: 112 labels; 1260 frames; 1,539,720 pairs; 20,160 exact factorizations; ... +``` + +The registered package metadata uses the repository's Python 3.12 runner. Source commits, Git blobs, +and SHA-256 pins are in [SOURCES.json](SOURCES.json); exact run settings and controls are in +[VERIFY.json](VERIFY.json). Cycle metadata and remaining obligations are in [TASK.json](TASK.json). + +## Open next questions + +1. Embed the common-basis identity into a real nine-stage schedule where both frames and their source + data are available, then account for all reads, copies, frame transitions and restoration. +2. Price the rational coefficient denominator and precision in the producer's actual coefficient + convention. The local rank/F2 census does not establish that the projected +8 remains the complete + correction charge. +3. Only after those steps, combine the local profile with a matching bit-side improvement and rerun + the selected-record acceptance gates. + +## Provenance, predecessors and credit + +- Cycle 47; seed `95720468bbdedd321824e249074fc5a3`; track `complex-mechanisms`; task + `complex-rank-shape-decoder`; scope key `02b31ebd160542c86299`; priority revision 4. +- Exact base commit `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`; selected-record SHA-256 + `10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. +- The direct predecessor is philippeVV's single-frame question in [Discussion #2278](https://github.com/CrocSwap/integer-mult-bounds/discussions/2278). + Related but distinct work: [PR #1825](https://github.com/CrocSwap/integer-mult-bounds/pull/1825), + [Discussion #2126](https://github.com/CrocSwap/integer-mult-bounds/discussions/2126), + [PR #2041](https://github.com/CrocSwap/integer-mult-bounds/pull/2041), and + [Discussion #2292](https://github.com/CrocSwap/integer-mult-bounds/discussions/2292). Current nearby + work in [Discussion #2245](https://github.com/CrocSwap/integer-mult-bounds/discussions/2245) and + [PR #2251](https://github.com/CrocSwap/integer-mult-bounds/pull/2251) finds a 96-dimensional pooled + correction space for P104's fixed trace; it concerns a different live set, matrix and timing model. +- The exact E8 line model follows the pinned `complex-frame-pair-decoders/verify.py` geometry; + pricing reuses the pinned `complex-local-word-ceiling/ceiling.py` interval calculator. Their + authors and upstream notices remain attributed in those source files. +- Prepared by Cinna Davis with substantial OpenAI Codex assistance. No independent human review is + claimed. Apache-2.0. diff --git a/research/cycle47-shared-frame-correction/SOURCES.json b/research/cycle47-shared-frame-correction/SOURCES.json new file mode 100644 index 0000000000..b1d77b3e97 --- /dev/null +++ b/research/cycle47-shared-frame-correction/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "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/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + }, + { + "path": "research/complex-frame-pair-decoders/verify.py", + "usage": "input", + "git_blob": "57dd8993e8ac016e8a92a9a885392b58014137bb", + "sha256": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" + }, + { + "path": "research/complex-local-word-ceiling/ceiling.py", + "usage": "input", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + } + ] +} diff --git a/research/cycle47-shared-frame-correction/TASK.json b/research/cycle47-shared-frame-correction/TASK.json new file mode 100644 index 0000000000..3fbdf82881 --- /dev/null +++ b/research/cycle47-shared-frame-correction/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "track": "complex-mechanisms", + "seed": "95720468bbdedd321824e249074fc5a3", + "scope_key": "02b31ebd160542c86299", + "priority_revision": 4, + "catalogue_sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "task_id": "complex-rank-shape-decoder", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "For the selected P112 pairing model, do two distinct orthogonal 8-frames that share one binary direction r have correction blocks in one common rational rank-8 row space, with a low-rank coefficient interface over F2?", + "scope_change_reason": "The claimed #2278 single-frame probe priced the correction at 16 additively or 8 under matrix coefficients, both at the boundary of the one-frame gate. The distinct experiment pairs frames with common r and tests whether one correction basis can serve both, rather than optimizing a single frame or the incumbent exact 8-term decoder.", + "mathematical_object": "The 112 selected q labels in complex-nine-native DATA-PHASES.json, mapped by their full binary pairing and deleted-frame signature to P112 in the pinned E8 line model. For each common r and frame S, M(S,r) is the 8 by 112 integer Gram correction supported on T={b in P112\\S: beta(r,b)=0 and some a in S has odd inner product with b}.", + "changed_assumption_or_expense": "Two distinct frame upgrades may share one rank-8 rational correction basis, with coefficient transformations priced jointly over F2, instead of charging the two frame corrections independently. Interface access, copying, frame transitions and restoration remain unpriced until a supplier is assembled.", + "method": "Exact E8 Gram and F2 arithmetic; enumerate all 1260 orthogonal frames in selected P112 and every r in F2^8 satisfying beta(r,a)=1 on the frame. For each same-r family, choose a full-rank 8-column minor from one correction block and compute exact coefficients for every other block; check reconstruction entrywise, rational rank, integrality and coefficient rank over F2.", + "domain_and_stop_rule": "Finite exhaustive domain: all 1260 selected P112 frames, all valid r values (16 per frame), all 135 distinct directions and 1,539,720 unordered same-r frame pairs. Stop after the exact factorization census and one pinned favorable moment screen; do not claim supplier or kappa without interface and restoration charges.", + "predecessors_and_overlap": [ + "Discussion #2278, philippeVV: single-frame plane-upgrade probe and request to test whether corrections can be absorbed; this work changes the object to pairs of frames sharing r.", + "PR #1825: paired plane-port decoder (related plane interface, no same-r shared correction census).", + "Discussion #2126: scalar identity fit over 56 shared matched planes (different fitting object).", + "Discussion #2024 / PR #2041: selected-P112 tri-plane factorization (different multi-plane decomposition).", + "Discussion #2292: five-dimensional port decoder (different cover and correction structure).", + "Discussion #2245 / PR #2251: P104 pooled correction-space dimension 96 (different trace, target matrices and question; noted as current related work)." + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2278#discussioncomment-18940341", + "claim_expiry_utc": "2026-10-15T06:15:00Z", + "bottleneck_link": "The correction charge was the limiting local price for plane upgrades. Sharing one rational correction basis across two frames could halve that charge and move the selected-word 5% moment screen from above one to below one, provided all other interface costs can be admitted.", + "budget_minutes": 60, + "outcome": "completed", + "evidence": "CERTIFICATE.json records the 112-label isomorphism and a witness pair. verify.py exhaustively checks the 1,539,720 same-r pairs through 20,160 correction blocks, exact common rational row spaces, integral coefficient maps, F2 ranks, mutation controls, and exact-rational moment controls.", + "author": "Cinna Davis with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for literature/overlap search, exact-model implementation, code, arithmetic checks, packaging and documentation. No independent human review is claimed.", + "open_questions": [ + { + "question": "Can the shared correction basis and its F2 coefficient interface be realized while both source and target frames are available in the actual nine-stage supplier?", + "why_it_matters": "The local moment screen has only a finite margin; extra access, copies, hosting, transitions, precision and restoration charges may erase it.", + "first_step": "Place the two witness frames into a concrete selected-word schedule and write the complete read/write and restoration ledger before synthesizing a larger word.", + "blocked_by": "No chronological host schedule or physical source/target representation for these exact correction factors has been constructed." + }, + { + "question": "Does the joint correction charge stay at 8 after the exact factors are embedded in the producer's coefficient convention?", + "why_it_matters": "The exact factorization proves a common rational row space, while the +8 moment charge assumes the rank-8/rank-4 coefficient pricing from the local model.", + "first_step": "Derive the producer-level bilinear identity for one witness pair and account for its complete copied-information support.", + "blocked_by": "No full producer identity has yet been assembled." + } + ], + "stop_rule": "Enumerate the full finite domain once, complete exact reconstruction and negative controls, run the favorable moment gate, and stop without claiming a supplier if any required hosting/interface/restoration term is missing." +} diff --git a/research/cycle47-shared-frame-correction/VERIFY.json b/research/cycle47-shared-frame-correction/VERIFY.json new file mode 100644 index 0000000000..fd6e5353dc --- /dev/null +++ b/research/cycle47-shared-frame-correction/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1094-audit/selected-replay.tar.gz", + "research/complex-frame-pair-decoders/verify.py", + "research/complex-local-word-ceiling/ceiling.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Exact label-map controls; full 1260-frame/135-direction census; all 20160 correction factorizations, denominator and F2 coefficient ranks; exact moment screen and failing controls." + } + ] +} diff --git a/research/cycle47-shared-frame-correction/verify.py b/research/cycle47-shared-frame-correction/verify.py new file mode 100644 index 0000000000..a8584b0220 --- /dev/null +++ b/research/cycle47-shared-frame-correction/verify.py @@ -0,0 +1,341 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact census for shared rank-8 corrections on the selected P112 E8 model. + +All arithmetic used in the correction factorization and screening is exact. +The only float values are display summaries. Standard library only. +""" +import hashlib +import importlib.util +import itertools +import json +import tarfile +import time +from collections import Counter, defaultdict +from fractions import Fraction as Q +from math import gcd +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +CERT = json.loads((HERE / 'CERTIFICATE.json').read_text()) +FAILS = [] + + +def check(tag, ok, detail=''): + print(('PASS ' if ok else 'FAIL ') + tag + ((' | ' + detail) if detail else ''), flush=True) + if not ok: + FAILS.append(tag) + + +def load_module(name, path): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def inverse(A): + n = len(A) + M = [[Q(x) for x in row] + [Q(int(i == j)) for j in range(n)] for i, row in enumerate(A)] + for c in range(n): + p = next((r for r in range(c, n) if M[r][c]), None) + if p is None: + raise ValueError('singular pivot matrix') + M[c], M[p] = M[p], M[c] + z = M[c][c] + M[c] = [x / z for x in M[c]] + for r in range(n): + if r != c and M[r][c]: + z = M[r][c] + M[r] = [x - z * y for x, y in zip(M[r], M[c])] + return [row[n:] for row in M] + + +def row_pivots(rows): + A = [[Q(x) for x in row] for row in rows] + n = len(A[0]) + pivots = [] + r = 0 + for c in range(n): + p = next((i for i in range(r, len(A)) if A[i][c]), None) + if p is None: + continue + A[r], A[p] = A[p], A[r] + z = A[r][c] + A[r] = [x / z for x in A[r]] + for i in range(len(A)): + if i != r and A[i][c]: + z = A[i][c] + A[i] = [x - z * y for x, y in zip(A[i], A[r])] + pivots.append(c) + r += 1 + if r == len(A): + break + return pivots + + +def qrank(rows): + return len(row_pivots(rows)) + + +def f2rank(rows): + basis = {} + rank = 0 + for row in rows: + x = sum((int(v) & 1) << j for j, v in enumerate(row)) + while x: + h = x.bit_length() - 1 + if h in basis: + x ^= basis[h] + else: + basis[h] = x + rank += 1 + break + return rank + + +def matmul(A, B): + return [[sum(A[i][k] * B[k][j] for k in range(len(B))) for j in range(len(B[0]))] + for i in range(len(A))] + + +def e8_binary_images(lines, gram, dot): + # The same integral E8 basis as the geometry probe in the #2278 handoff. + basis = [(2, -2, 0, 0, 0, 0, 0, 0), (0, 2, -2, 0, 0, 0, 0, 0), + (0, 0, 2, -2, 0, 0, 0, 0), (0, 0, 0, 2, -2, 0, 0, 0), + (0, 0, 0, 0, 2, -2, 0, 0), (0, 0, 0, 0, 0, 2, -2, 0), + (0, 0, 0, 0, 0, 2, 2, 0), (-1,) * 8] + + def solve(v): + n = 8 + A = [[Q(basis[j][i]) for j in range(n)] + [Q(v[i])] for i in range(n)] + for c in range(n): + p = next(r for r in range(c, n) if A[r][c]) + A[c], A[p] = A[p], A[c] + z = A[c][c] + A[c] = [x / z for x in A[c]] + for r in range(n): + if r != c and A[r][c]: + z = A[r][c] + A[r] = [x - z * y for x, y in zip(A[r], A[c])] + x = [A[i][n] for i in range(n)] + if any(t.denominator != 1 for t in x): + raise ValueError('root is not in the declared E8 basis') + return tuple(int(t) & 1 for t in x) + + bgram = [[dot(basis[i], basis[j]) & 1 for j in range(8)] for i in range(8)] + images = [solve(v) for v in lines] + + def beta(x, y): + return sum(x[i] * bgram[i][j] * y[j] for i in range(8) for j in range(8)) & 1 + + if any(beta(images[i], images[j]) != (gram[i][j] & 1) + for i in range(120) for j in range(120)): + raise ValueError('E8 binary form disagrees with the pinned Gram matrix') + return images, beta + + +def selected_labels(): + source = ROOT / 'research/community-frontier1094-audit/selected-replay.tar.gz' + expected = 'f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6' + digest = hashlib.sha256(source.read_bytes()).hexdigest() + if digest != expected: + raise ValueError('selected replay archive SHA256 mismatch') + member = 'candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json' + with tarfile.open(source, 'r:gz') as tf: + data = json.load(tf.extractfile(member)) + q = sorted(int(row['q']) for row in data['recipes']) + if len(q) != 112 or len(set(q)) != 112: + raise ValueError('selected source does not contain 112 distinct q labels') + return q + + +def map_checks(m, q): + q_to_line = CERT['q_to_line'] + qkeys = [int(item['q']) for item in q_to_line] + lines = [int(item['line']) for item in q_to_line] + C = {x for x in range(512) if x.bit_count() in (3, 7)} + O = sorted(C - set(q)) + if len(C) != 120 or len(O) != 8 or qkeys != q or len(set(lines)) != 112: + return False, 'label-map cardinality' + if set(lines) != set(m.P112): + return False, 'map does not cover the selected P112 lines' + by_q = dict(zip(qkeys, lines)) + # The 112-by-112 binary pairing and the eight deleted-frame signatures agree. + for x in q: + i = by_q[x] + for y in q: + j = by_q[y] + if ((x & y).bit_count() & 1) != ((m.NROW[i] >> j) & 1): + return False, 'selected-label pairing mismatch' + for k, o in enumerate(O): + if ((x & o).bit_count() & 1) != ((m.NROW[i] >> m.FRAME0[k]) & 1): + return False, 'deleted-frame signature mismatch' + # Mutation control: one incorrect line assignment must break the exact isomorphism. + wrong = dict(by_q) + wrong[q[0]] = next(i for i in m.P112 if i != wrong[q[0]]) + rejected = any(((x & y).bit_count() & 1) != ((m.NROW[wrong[x]] >> wrong[y]) & 1) + for x in q for y in q) + return rejected, '112 labels mapped bijectively to P112; all internal/deleted signatures match; mutation rejected' + + +def enumerate_frames(selected, ip): + orth = [[ip[a][b] == 0 for b in range(120)] for a in range(120)] + frames = set() + + def extend(cur, cand): + if len(cur) == 8: + frames.add(tuple(cur)) + return + for c in cand: + if c > cur[-1]: + extend(cur + [c], [z for z in cand if z > c and orth[c][z]]) + + for a in selected: + extend([a], [z for z in selected if z > a and orth[a][z]]) + return sorted(frames) + + +def correction_block(S, rp, selected, ip, images, beta): + Sset = set(S) + T = [b for b in selected if b not in Sset and beta(rp, images[b]) == 0 + and any(ip[a][b] & 1 for a in S)] + rows = [[ip[a][b] if b in T else 0 for b in selected] for a in S] + return rows, T + + +def main(): + started = time.monotonic() + m = load_module('frame_pair_base', ROOT / 'research/complex-frame-pair-decoders/verify.py') + q = selected_labels() + mapped_ok, map_note = map_checks(m, q) + check('selected-label-isomorphism', mapped_ok, map_note) + selected = sorted(int(item['line']) for item in CERT['q_to_line']) + ip = m.IP + images, beta = e8_binary_images(m.LINES, ip, m.ip) + frames = enumerate_frames(selected, ip) + check('frame-domain', len(frames) == 1260, 'all orthogonal 8-frames in the selected 112 lines') + + groups = defaultdict(list) + per_frame = Counter() + for S in frames: + rs = [tuple((x >> i) & 1 for i in range(8)) for x in range(256) + if all(beta(tuple((x >> i) & 1 for i in range(8)), images[a]) == 1 for a in S)] + per_frame[len(rs)] += 1 + for rp in rs: + groups[rp].append(S) + pair_count = sum(len(v) * (len(v) - 1) // 2 for v in groups.values()) + group_sizes = Counter(map(len, groups.values())) + check('common-direction-domain', len(groups) == 135 and per_frame == Counter({16: 1260}) + and group_sizes == Counter({105: 16, 150: 112, 240: 7}) + and pair_count == 1539720, + '135 directions; frame multiplicities 105x16, 150x112, 240x7; 1,539,720 unordered pairs') + + blocks = 0 + group_f2_ranks = Counter() + scale_hist = Counter() + scaled_block_f2_ranks = Counter() + witness_data = None + for rp, ss in groups.items(): + if len(ss) < 2: + continue + M0, T0 = correction_block(ss[0], rp, selected, ip, images, beta) + pivots = row_pivots(M0) + if len(pivots) != 8: + raise ValueError('baseline correction block does not have rational rank 8') + P0 = [[M0[i][j] for j in pivots] for i in range(8)] + invP0 = inverse(P0) + union_coeffs = [] + family_coeffs = [] + common_scale = 1 + for S in ss: + M, T = correction_block(S, rp, selected, ip, images, beta) + if len(T) not in (48, 52, 56): + raise ValueError('unexpected correction target size') + # M = C M0, with C computed from the fixed pivot minor. This is an + # exact rational row-space test and an explicit factorization. + C = matmul([[M[i][j] for j in pivots] for i in range(8)], invP0) + scale_s = 1 + for row in C: + for x in row: + scale_s = scale_s * x.denominator // gcd(scale_s, x.denominator) + Ds = [[int(x * scale_s) for x in row] for row in C] + if matmul(Ds, M0) != [[v * scale_s for v in row] for row in M] or qrank(Ds) != 8: + raise ValueError('exact shared rank-8 factorization failed') + for row in C: + for x in row: + common_scale = common_scale * x.denominator // gcd(common_scale, x.denominator) + family_coeffs.append((Ds, scale_s, M)) + blocks += 1 + if witness_data is None and tuple(rp) == tuple(CERT['witness']['r_bits']) \ + and tuple(S) == tuple(CERT['witness']['frames'][1]): + witness_data = (rp, tuple(S), tuple(T), M, Ds, scale_s, M0, pivots) + scale_hist[common_scale] += 1 + for Ds, scale_s, M in family_coeffs: + D = [[x * (common_scale // scale_s) for x in row] for row in Ds] + if matmul(D, M0) != [[v * common_scale for v in row] for row in M]: + raise ValueError('scaled shared-basis reconstruction failed') + scaled_block_f2_ranks[f2rank(D)] += 1 + union_coeffs.extend(D) + shared_f2 = f2rank(union_coeffs) + group_f2_ranks[shared_f2] += 1 + + check('shared-correction-census', blocks == 20160 and scale_hist == Counter({2: 135}) + and group_f2_ranks == Counter({4: 135}), + '20,160 rank-8 blocks; per-direction common Q basis; scale lcm %s; family F2 ranks %s; scaled block F2 ranks %s' + % (dict(scale_hist), dict(group_f2_ranks), dict(scaled_block_f2_ranks))) + check('witness-factorization', witness_data is not None, + 'certificate names two distinct frames with the same r; M_i = C_i M_0 checked entrywise') + + if witness_data is not None: + rp, S2, T2, M2, D2s, scale2, M0, pivots = witness_data + S1 = tuple(CERT['witness']['frames'][0]) + M1, T1 = correction_block(S1, rp, selected, ip, images, beta) + invP0 = inverse([[M0[i][j] for j in pivots] for i in range(8)]) + C1 = matmul([[M1[i][j] for j in pivots] for i in range(8)], invP0) + scale1 = 1 + for row in C1: + for x in row: + scale1 = scale1 * x.denominator // gcd(scale1, x.denominator) + D1 = [[int(x * scale1) for x in row] for row in C1] + assert matmul(D1, M0) == [[x * scale1 for x in row] for row in M1] + pair_scale = scale1 * scale2 // gcd(scale1, scale2) + D1 = [[x * (pair_scale // scale1) for x in row] for row in D1] + D2 = [[x * (pair_scale // scale2) for x in row] for row in D2s] + pair_f2 = f2rank(D1 + D2) + if S1 == S2 or pair_f2 > 4: + raise ValueError('witness pair does not fit the shared F2 rank-4 coefficient space') + # A one-entry coefficient mutation is a meaningful failure control. + bad = [row[:] for row in D2] + bad[0][0] += 1 + check('factorization-negative-control', matmul(bad, M0) != [[x * pair_scale for x in row] for row in M2], + 'one changed coefficient is detected by exact reconstruction') + + # Favorable moment screen: the two upgrades create 8/7 unpaid coordinates per + # family; one shared rank-8/rank-4 correction is charged as +8 centre units. + ceiling = load_module('local_word_ceiling', ROOT / 'research/complex-local-word-ceiling/ceiling.py') + local = {1: 2412, 2: 418, 3: 432, 4: 142, 5: 82, 8: 8} + a_star = Q(35491136290869, 20000000000000000) # 1.05 * selected a_hi + shared = ceiling.relax(local, 73, 896, 9, 72, a_star, unpaid=Q(8, 7)) + one_frame = ceiling.relax(local, 73, 896, 9, 72, a_star, unpaid=Q(15, 14)) + unshared = ceiling.relax(local, 73, 896, 9, 80, a_star, unpaid=Q(8, 7)) + check('favorable-five-percent-screen', shared[1] < 1 and one_frame[0] > 1 and unshared[0] > 1, + 'shared two-frame relaxation %.15f; one-frame %.15f; unshared two-frame %.15f' + % (float(shared[1]), float(one_frame[0]), float(unshared[0]))) + + print('DOMAIN frames=1260 directions=135 pairs=%d correction_blocks=%d' % (pair_count, blocks)) + if witness_data is not None: + print('FACTOR witness_r=%s frame_sizes=(%d,%d) target_sizes=(%d,%d) q_rank=8 common_scale=%d pair_f2_rank=%d' + % (''.join(map(str, rp)), len(S1), len(S2), len(T1), len(T2), pair_scale, pair_f2)) + print('PRICE target=%s shared_upper=%s one_frame_lower=%s unshared_lower=%s' + % (a_star, shared[1], one_frame[0], unshared[0])) + print('SCOPE No complete supplier, interface charge, restoration, or new kappa is certified.') + if not FAILS: + print('PASS_CYCLE47_SHARED_FRAME_CORRECTION: 112 labels; 1260 frames; 1,539,720 pairs; 20,160 exact factorizations; time %.1fs' + % (time.monotonic() - started)) + raise SystemExit(1 if FAILS else 0) + + +if __name__ == '__main__': + main()