diff --git a/research/p111-parseval-copy-interface/README.md b/research/p111-parseval-copy-interface/README.md new file mode 100644 index 0000000000..046ea695cb --- /dev/null +++ b/research/p111-parseval-copy-interface/README.md @@ -0,0 +1,234 @@ +# P111 Parseval blocks: a scalar-copy interface audit + +**Exact fixed-class obstruction, not a new supplier or kappa claim.** + +PR [1900](https://github.com/CrocSwap/integer-mult-bounds/pull/1900), pinned at +`9a891c9cb25b15f5a189bcad1d022198adeaf885`, gives a valid F2 Parseval +factorization of the selected P111 bit decoder. This audit **confirms** that +identity on all 111 targets and all 661 formal dirty input columns. It does +not repeat the complex-field obstruction in PR1889: F2 is the correct payload +field here. + +The new result concerns the next implication: can the five coefficient blocks +be implemented as ordinary scalar copied totals at the sum of their five +union-support pairing ranks, `40`? **No.** In the explicitly bounded inherited +scalar model below, their exact minimum is **73**, versus the original decoder's +**63**. The literal ten Parseval scalar channels cost **74**. A hypothetical new +physical block-valued primitive is outside this lower bound; its cost is **not** +proved to be twice a union-support rank. + +## Exact object and result + +Reconstruct the selected PR589 word after its `D` and `A` sections. Its nine +retained channels and scatter supports give factors `P,Q`, with the entire +dirty update `P Q^T`. PR1900 uses the following columns of a 9-by-10 matrix `A`: + +```text +3, 5, 6, 7, 8, 16, 32, 64, 128, 256 (little-endian binary vectors) +``` + +They satisfy `A A^T = I9` over F2. Group columns into `(0,1)`, `(2,3)`, `(4,5)`, +`(6,7)`, `(8,9)`. For each block, let `L` be its two transformed target columns +and `R` its two transformed source columns, including every dirty input. Its +map is `L R^T`, of rank two even after restricting to the 111 source ports. + +A **scalar copied total** with support vectors `l,r` implements the rank-one +update `l r^T`. Its priced objective is the inherited rational pairing rank + +```text +beta(l,r) = rank_Q( G[target_support(l), source_port_support(r)] ), +G = root_lines * root_lines^T / 2. +``` + +This is the per-total objective of PR446 Theorem C, retained in +[the P111 certificate](../p111-copy-rank-certificate/PROOF.md) and +[the bit label-decoder model](../bit-orthogonal-pair-decoders/PROOF.md). +It is not an assertion that every abstract term has a simultaneously legal +physical realization at exactly that price. Those additional costs remain +nonnegative obligations. + +**The audited class:** in each fixed block, every scalar term has factors +`l=Lx`, `r=Ry` for nonzero `x,y in F2^2`. Arbitrarily many terms, asymmetric +factors, all basis changes, and repeated terms are allowed. Different blocks +are not rebased or canceled together. There is no new block-valued copy, +operator-valued encoding, or changed port geometry in this class. +Each total reads the fixed retained-channel values at this boundary and +preserves them; complete scalar calls restore private scratch. Source-mutating +or operator-valued encodings are outside the class, not assumed impossible. + +| Block | Rank of the union-support pairing | Literal two scalar terms | Exact minimum, any number of within-block scalar terms | +|---|---:|---:|---:| +| 0 | 8 | 16 | 16 | +| 1 | 8 | 16 | 15 | +| 2 | 8 | 14 | 14 | +| 3 | 8 | 14 | 14 | +| 4 | 8 | 14 | 14 | +| **Total** | **40 (not a scalar invoice)** | **74** | **73** | + +The optimum has seven rank-7 and three rank-8 scalar copies. For block 1 an +attaining factorization, in its local two-column coordinates, is + +```text +(x,y,cost) = (2,3,7), (3,1,8). +``` + +The other blocks attain their minima with `(1,1)` and `(2,2)`. This improves +the literal Parseval scalar expansion by one, but still loses ten copy-rank +units to the original nine-channel decoder. The existing global optimum 63 +for the broader scalar label-decoder model is predecessor work, not a new +claim here. Cross-block cancellation can recover the original nine-channel +factorization; that is why the fixed-block restriction is explicit. + +## Proof of completeness and the interface counterexample + +Both `L` and the source-port restriction of `R` have full column rank two. +They therefore have left inverses over F2. Consequently + +```text +sum (L x_i)(R y_i)^T = L R^T iff sum x_i y_i^T = I2. +``` + +There are exactly nine nonzero pairs `(x,y)`. Two identical pairs cancel over +F2 and have strictly positive cost, so deleting both never increases cost. +Every finite factorization has a no-more-expensive representative among the +`2^9=512` subsets. The verifier exhausts all 512 for each block: 32 subsets per +block give `I2`, for 160 exact factorizations overall. All six ordered GL2(F2) +bases per block occur, but the census also covers every longer decomposition. +Each accepted subset is replayed against the full dirty block, not merely its +2-by-2 coefficient identity. + +Every rank is exact. Rational reduction computes the support subspaces and +pairing rank; separate modular elimination on the original, uncompressed +Gram submatrix supplies the same rank lower bound. A field-control fixture +has rational rank three but F2 rank two, so these two rank notions are not +silently interchanged. The finite source checks support the written +all-length reduction; no proof-assistant verification is claimed. + +A single scalar copied total has rank at most one, so it cannot implement +any rank-two block, regardless of how its rank-one supports are chosen. +In particular, actually using the two support unions as one scalar term per +block gives **5,838 wrong source-target entries** and **17,146 wrong entries** +on the full dirty input matrix. A smallest explicit source input is port 0 +set to one, all other input registers zero: target 0 should receive one but +receives zero. The verifier also supplies 45 explicit two-bit witnesses +against the nine within-span single-total choices for each block. + +This does **not** say a primitive with two independent operator-valued +channels must be two separately charged scalar copies. It says the inherited +scalar primitive does not perform the asserted block update. A physical +block-copy lemma must supply its own complete operator and invoice. + +## Coverage law and favorable paid screen + +The coefficient planes are planes in a **binary factor space**, not supplied +rational port planes on each of the 111 physical data families. Keeping the +selected line-port geometry keeps the one-unpaid-coordinate contract. Merely +regrouping decoder coefficients does not establish the source `E -> FULL`, +target `0 -> E^perp` endpoint for two-dimensional physical `E`. This is the +separate plane-port obligation posed by ctoth in +[Discussion1587](https://github.com/CrocSwap/integer-mult-bounds/discussions/1587#discussioncomment-18914510). + +For a deliberately favorable screen of the fixed scalar interpretation, keep +all incumbent non-copy children, use its minimum copies, and set *all extra* +basis, storage, cleanup, routing, hosting and precision costs to zero. No such +cost is declared free in a completed construction. With `m=64`, `W=888/9=296/3`, +`R=42`, and unpaid=1: + +| Quantity, per call | Original | Best fixed-block scalar screen | +|---|---:|---:| +| Centre copy charge | 63 | 73 | +| Total paid mass, `63 W + C` | 6279 | 6289 | +| Local paid mass | 5129 | 5139 | +| Idle mass | 1150 | 1150 | +| Deficit, `W-C` | 107/3 | 77/3 | +| Certified upper bound on `a` | 0.001947467559 | 0.001401325233 | + +The complete profiles and certified adjacent-grid brackets are in +[RESULT.json](RESULT.json). They use the unchanged pinned `ceiling.py` with +`unpaid=1`, **not** the unproved `unpaid=2` physical interface. The changed +profile replaces two rank-7 children by three rank-8 children. Its moment is +larger throughout `0 <= a < 1`, since +`3(8/64)^(1-a) - 2(7/64)^(1-a) > 0`, with unchanged idle mass. Adding the omitted +implementation costs cannot rescue this fixed-profile route. Deleting or +redesigning other side work would change the screened hypothesis. + +This is not a recalculation of the price of a genuinely new plane supplier. +No physical word, hosted template, precision invoice, assembly, selected-bound +change, or new kappa follows from this audit. + +## Reproduction and evidence + +From the repository root, with standard-library CPython 3.12: + +```sh +python3.12 -I -O -B research/p111-parseval-copy-interface/verify.py +python3.12 scripts/research_package.py --package research/p111-parseval-copy-interface +``` + +`verify.py --write` regenerates the deterministic receipt. Normal replay +compares all proof-relevant fields with it. Explicit `require` checks remain +active under `-O`. The replay includes baseline and Parseval positive +controls, all subset/GL2 cases, 45 one-channel failures, ten optimal-term +omissions, a broken frame, an omitted block, switched channels, and the +rank-field control. Source bytes are hash-bound before use. The wrapper +checks package metadata and historical provenance too. + +Locally exercised on **CPython 3.12.12, Darwin arm64** via +`uv run --python 3.12 --no-project python`: the optimized isolated generator +smoke and the registered replay both passed. The exact replay output was: + +```text +PASS_P111_PARSEVAL_COPY_INTERFACE blocks=5 subsets=2560 factorizations=160 dirty_columns=661 copy_min=73 baseline=63 union_failure_entries=17146 +PASS_REGISTERED_RESEARCH_PACKAGE research/p111-parseval-copy-interface outcome=negative-result +``` + +The first wrapper attempt rejected an invalid TASK outcome enum; it was +corrected to `negative-result` before the successful registered replay. +No mathematical verifier failure was suppressed. + +The catalogue's complex-ceiling working example and lever script were run +as orientation controls; they do not verify a new bit construction. No full +repository suite, selected cold replay, native proof build, or human proof +review is claimed. + +## Provenance and credit + +- Independent OS-random seed `3cc9f4c8f3719f13f4ae6bf28c9ba982`, recursive-interfaces, + coverage-law-change; all emitted cards are retained in [SELECTION.json](SELECTION.json). +- Exact baseline `0b1cccf86e2f5132ed286a26ef0a681a495740ea`; selected-record hash + `10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. +- Cinna Davis / 1337isnot1337's PR1900 supplies the valid Parseval construction + and the audited copy claim. Exact head, Git blobs, constants and scope are + in [SOURCE-CLAIM.json](SOURCE-CLAIM.json). No predecessor executable is imported. +- The selected PR589/PR555 word, DreamingOfClouds' PR446 pricing premise, + and bit orthogonal-pair decoder proof retain their attribution. The + P111 scalar-copy certificate was prepared with Codex at Russell Seligmann's + request; Joel Pulikkan / GamingPuzzled's PR620 supplied the earlier cost-63 + experiments and cost classification. Their global scalar optimum is not + claimed as new here; see the predecessor's [NOTICE](../p111-copy-rank-certificate/NOTICE.md). + ctoth's Discussion1587 establishes the plane-port endpoint question. + Douglas Colkitt's ceiling engine, prepared with Claude assistance, is reused + unchanged. PR1889's complex scalar-lift audit is distinct and not reused. +- [Claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1929#discussioncomment-18925833). + The shared 2026-10-14 overlap snapshot covered 579 open PRs and 547 discussion + records with complete pagination; targeted queries found PR1900 and its + handoff, not a prior audit of this scalar-copy implication. Immediately before + publication, live `Parseval` title/body search returned only PR1900, a + `blockwise`/`copy` search returned no open PR, and the PR1900 head remained + `9a891c9cb25b15f5a189bcad1d022198adeaf885`. Search coverage is not a novelty proof. +- Prepared by Adam Gall with substantial OpenAI Codex assistance in research, + exact calculations, verification and writing. No independent human review. + New work is Apache-2.0; existing source notices are unchanged. + +## Open next questions + +1. **Can a new physical block-valued copy implement these blocks at one + union-support charge?** This is the mechanism that could bypass this + scalar obstruction. First write its full operator on independent dirty + source/target streams, including restored scratch and legal frames. The + blocker is that no such typed primitive is supplied by coefficient grouping. +2. **Can a completed physical two-dimensional port contract share boundary + work that the scalar interpretation cannot?** This is what could justify + unpaid=2. First specify each data family's rational plane and a small dirty + endpoint with all copies, frame changes and restoration charged. The + coefficient-space factorization does not supply those physical planes. diff --git a/research/p111-parseval-copy-interface/RESULT.json b/research/p111-parseval-copy-interface/RESULT.json new file mode 100644 index 0000000000..6194b9ef09 --- /dev/null +++ b/research/p111-parseval-copy-interface/RESULT.json @@ -0,0 +1,1398 @@ +{ + "baseline_scalar_charge": 63, + "best_blockwise_scalar_charge": 73, + "blocks": [ + { + "block": 0, + "columns": [ + 0, + 1 + ], + "direct_scalar_charge": 16, + "feasible_subsets": [ + { + "charge": 16, + "subset": 17, + "terms": 2 + }, + { + "charge": 16, + "subset": 96, + "terms": 2 + }, + { + "charge": 16, + "subset": 132, + "terms": 2 + }, + { + "charge": 24, + "subset": 22, + "terms": 3 + }, + { + "charge": 24, + "subset": 41, + "terms": 3 + }, + { + "charge": 24, + "subset": 88, + "terms": 3 + }, + { + "charge": 24, + "subset": 131, + "terms": 3 + }, + { + "charge": 24, + "subset": 266, + "terms": 3 + }, + { + "charge": 24, + "subset": 324, + "terms": 3 + }, + { + "charge": 24, + "subset": 416, + "terms": 3 + }, + { + "charge": 32, + "subset": 46, + "terms": 4 + }, + { + "charge": 32, + "subset": 202, + "terms": 4 + }, + { + "charge": 32, + "subset": 269, + "terms": 4 + }, + { + "charge": 32, + "subset": 306, + "terms": 4 + }, + { + "charge": 32, + "subset": 323, + "terms": 4 + }, + { + "charge": 32, + "subset": 408, + "terms": 4 + }, + { + "charge": 40, + "subset": 103, + "terms": 5 + }, + { + "charge": 40, + "subset": 188, + "terms": 5 + }, + { + "charge": 40, + "subset": 205, + "terms": 5 + }, + { + "charge": 40, + "subset": 242, + "terms": 5 + }, + { + "charge": 40, + "subset": 309, + "terms": 5 + }, + { + "charge": 40, + "subset": 465, + "terms": 5 + }, + { + "charge": 48, + "subset": 95, + "terms": 6 + }, + { + "charge": 48, + "subset": 187, + "terms": 6 + }, + { + "charge": 48, + "subset": 245, + "terms": 6 + }, + { + "charge": 48, + "subset": 380, + "terms": 6 + }, + { + "charge": 48, + "subset": 423, + "terms": 6 + }, + { + "charge": 48, + "subset": 470, + "terms": 6 + }, + { + "charge": 48, + "subset": 489, + "terms": 6 + }, + { + "charge": 56, + "subset": 379, + "terms": 7 + }, + { + "charge": 56, + "subset": 415, + "terms": 7 + }, + { + "charge": 56, + "subset": 494, + "terms": 7 + } + ], + "minimum_scalar_charge": 16, + "one_channel_counterexamples": [ + { + "actual": 0, + "expected": 2, + "input": 2, + "left": 1, + "right": 1 + }, + { + "actual": 0, + "expected": 1, + "input": 1, + "left": 1, + "right": 2 + }, + { + "actual": 1, + "expected": 2, + "input": 2, + "left": 1, + "right": 3 + }, + { + "actual": 2, + "expected": 1, + "input": 1, + "left": 2, + "right": 1 + }, + { + "actual": 0, + "expected": 1, + "input": 1, + "left": 2, + "right": 2 + }, + { + "actual": 2, + "expected": 1, + "input": 1, + "left": 2, + "right": 3 + }, + { + "actual": 3, + "expected": 1, + "input": 1, + "left": 3, + "right": 1 + }, + { + "actual": 0, + "expected": 1, + "input": 1, + "left": 3, + "right": 2 + }, + { + "actual": 3, + "expected": 1, + "input": 1, + "left": 3, + "right": 3 + } + ], + "operator_rank": 2, + "term_cost_grid": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + "union_support_charge": 8, + "witness": [ + [ + 1, + 1, + 8 + ], + [ + 2, + 2, + 8 + ] + ] + }, + { + "block": 1, + "columns": [ + 2, + 3 + ], + "direct_scalar_charge": 16, + "feasible_subsets": [ + { + "charge": 15, + "subset": 96, + "terms": 2 + }, + { + "charge": 15, + "subset": 132, + "terms": 2 + }, + { + "charge": 16, + "subset": 17, + "terms": 2 + }, + { + "charge": 22, + "subset": 324, + "terms": 3 + }, + { + "charge": 22, + "subset": 416, + "terms": 3 + }, + { + "charge": 23, + "subset": 22, + "terms": 3 + }, + { + "charge": 23, + "subset": 41, + "terms": 3 + }, + { + "charge": 23, + "subset": 266, + "terms": 3 + }, + { + "charge": 24, + "subset": 88, + "terms": 3 + }, + { + "charge": 24, + "subset": 131, + "terms": 3 + }, + { + "charge": 30, + "subset": 46, + "terms": 4 + }, + { + "charge": 30, + "subset": 269, + "terms": 4 + }, + { + "charge": 30, + "subset": 306, + "terms": 4 + }, + { + "charge": 31, + "subset": 323, + "terms": 4 + }, + { + "charge": 31, + "subset": 408, + "terms": 4 + }, + { + "charge": 32, + "subset": 202, + "terms": 4 + }, + { + "charge": 37, + "subset": 309, + "terms": 5 + }, + { + "charge": 38, + "subset": 103, + "terms": 5 + }, + { + "charge": 38, + "subset": 188, + "terms": 5 + }, + { + "charge": 39, + "subset": 205, + "terms": 5 + }, + { + "charge": 39, + "subset": 242, + "terms": 5 + }, + { + "charge": 39, + "subset": 465, + "terms": 5 + }, + { + "charge": 45, + "subset": 380, + "terms": 6 + }, + { + "charge": 45, + "subset": 423, + "terms": 6 + }, + { + "charge": 46, + "subset": 245, + "terms": 6 + }, + { + "charge": 46, + "subset": 470, + "terms": 6 + }, + { + "charge": 46, + "subset": 489, + "terms": 6 + }, + { + "charge": 47, + "subset": 95, + "terms": 6 + }, + { + "charge": 47, + "subset": 187, + "terms": 6 + }, + { + "charge": 53, + "subset": 494, + "terms": 7 + }, + { + "charge": 54, + "subset": 379, + "terms": 7 + }, + { + "charge": 54, + "subset": 415, + "terms": 7 + } + ], + "minimum_scalar_charge": 15, + "one_channel_counterexamples": [ + { + "actual": 0, + "expected": 2, + "input": 2, + "left": 1, + "right": 1 + }, + { + "actual": 0, + "expected": 1, + "input": 1, + "left": 1, + "right": 2 + }, + { + "actual": 1, + "expected": 2, + "input": 2, + "left": 1, + "right": 3 + }, + { + "actual": 2, + "expected": 1, + "input": 1, + "left": 2, + "right": 1 + }, + { + "actual": 0, + "expected": 1, + "input": 1, + "left": 2, + "right": 2 + }, + { + "actual": 2, + "expected": 1, + "input": 1, + "left": 2, + "right": 3 + }, + { + "actual": 3, + "expected": 1, + "input": 1, + "left": 3, + "right": 1 + }, + { + "actual": 0, + "expected": 1, + "input": 1, + "left": 3, + "right": 2 + }, + { + "actual": 3, + "expected": 1, + "input": 1, + "left": 3, + "right": 3 + } + ], + "operator_rank": 2, + "term_cost_grid": [ + 8, + 8, + 7, + 8, + 8, + 7, + 8, + 8, + 7 + ], + "union_support_charge": 8, + "witness": [ + [ + 2, + 3, + 7 + ], + [ + 3, + 1, + 8 + ] + ] + }, + { + "block": 2, + "columns": [ + 4, + 5 + ], + "direct_scalar_charge": 14, + "feasible_subsets": [ + { + "charge": 14, + "subset": 17, + "terms": 2 + }, + { + "charge": 15, + "subset": 96, + "terms": 2 + }, + { + "charge": 15, + "subset": 132, + "terms": 2 + }, + { + "charge": 21, + "subset": 88, + "terms": 3 + }, + { + "charge": 21, + "subset": 131, + "terms": 3 + }, + { + "charge": 22, + "subset": 22, + "terms": 3 + }, + { + "charge": 22, + "subset": 41, + "terms": 3 + }, + { + "charge": 22, + "subset": 266, + "terms": 3 + }, + { + "charge": 23, + "subset": 324, + "terms": 3 + }, + { + "charge": 23, + "subset": 416, + "terms": 3 + }, + { + "charge": 28, + "subset": 202, + "terms": 4 + }, + { + "charge": 29, + "subset": 323, + "terms": 4 + }, + { + "charge": 29, + "subset": 408, + "terms": 4 + }, + { + "charge": 30, + "subset": 46, + "terms": 4 + }, + { + "charge": 30, + "subset": 269, + "terms": 4 + }, + { + "charge": 30, + "subset": 306, + "terms": 4 + }, + { + "charge": 36, + "subset": 205, + "terms": 5 + }, + { + "charge": 36, + "subset": 242, + "terms": 5 + }, + { + "charge": 36, + "subset": 465, + "terms": 5 + }, + { + "charge": 37, + "subset": 103, + "terms": 5 + }, + { + "charge": 37, + "subset": 188, + "terms": 5 + }, + { + "charge": 38, + "subset": 309, + "terms": 5 + }, + { + "charge": 43, + "subset": 95, + "terms": 6 + }, + { + "charge": 43, + "subset": 187, + "terms": 6 + }, + { + "charge": 44, + "subset": 245, + "terms": 6 + }, + { + "charge": 44, + "subset": 470, + "terms": 6 + }, + { + "charge": 44, + "subset": 489, + "terms": 6 + }, + { + "charge": 45, + "subset": 380, + "terms": 6 + }, + { + "charge": 45, + "subset": 423, + "terms": 6 + }, + { + "charge": 51, + "subset": 379, + "terms": 7 + }, + { + "charge": 51, + "subset": 415, + "terms": 7 + }, + { + "charge": 52, + "subset": 494, + "terms": 7 + } + ], + "minimum_scalar_charge": 14, + "one_channel_counterexamples": [ + { + "actual": 0, + "expected": 2, + "input": 2, + "left": 1, + "right": 1 + }, + { + "actual": 0, + "expected": 1, + "input": 1, + "left": 1, + "right": 2 + }, + { + "actual": 1, + "expected": 2, + "input": 2, + "left": 1, + "right": 3 + }, + { + "actual": 2, + "expected": 1, + "input": 1, + "left": 2, + "right": 1 + }, + { + "actual": 0, + "expected": 1, + "input": 1, + "left": 2, + "right": 2 + }, + { + "actual": 2, + "expected": 1, + "input": 1, + "left": 2, + "right": 3 + }, + { + "actual": 3, + "expected": 1, + "input": 1, + "left": 3, + "right": 1 + }, + { + "actual": 0, + "expected": 1, + "input": 1, + "left": 3, + "right": 2 + }, + { + "actual": 3, + "expected": 1, + "input": 1, + "left": 3, + "right": 3 + } + ], + "operator_rank": 2, + "term_cost_grid": [ + 7, + 7, + 8, + 7, + 7, + 8, + 7, + 7, + 8 + ], + "union_support_charge": 8, + "witness": [ + [ + 1, + 1, + 7 + ], + [ + 2, + 2, + 7 + ] + ] + }, + { + "block": 3, + "columns": [ + 6, + 7 + ], + "direct_scalar_charge": 14, + "feasible_subsets": [ + { + "charge": 14, + "subset": 17, + "terms": 2 + }, + { + "charge": 15, + "subset": 96, + "terms": 2 + }, + { + "charge": 15, + "subset": 132, + "terms": 2 + }, + { + "charge": 21, + "subset": 88, + "terms": 3 + }, + { + "charge": 21, + "subset": 131, + "terms": 3 + }, + { + "charge": 22, + "subset": 22, + "terms": 3 + }, + { + "charge": 22, + "subset": 41, + "terms": 3 + }, + { + "charge": 22, + "subset": 266, + "terms": 3 + }, + { + "charge": 23, + "subset": 324, + "terms": 3 + }, + { + "charge": 23, + "subset": 416, + "terms": 3 + }, + { + "charge": 28, + "subset": 202, + "terms": 4 + }, + { + "charge": 29, + "subset": 323, + "terms": 4 + }, + { + "charge": 29, + "subset": 408, + "terms": 4 + }, + { + "charge": 30, + "subset": 46, + "terms": 4 + }, + { + "charge": 30, + "subset": 269, + "terms": 4 + }, + { + "charge": 30, + "subset": 306, + "terms": 4 + }, + { + "charge": 36, + "subset": 205, + "terms": 5 + }, + { + "charge": 36, + "subset": 242, + "terms": 5 + }, + { + "charge": 36, + "subset": 465, + "terms": 5 + }, + { + "charge": 37, + "subset": 103, + "terms": 5 + }, + { + "charge": 37, + "subset": 188, + "terms": 5 + }, + { + "charge": 38, + "subset": 309, + "terms": 5 + }, + { + "charge": 43, + "subset": 95, + "terms": 6 + }, + { + "charge": 43, + "subset": 187, + "terms": 6 + }, + { + "charge": 44, + "subset": 245, + "terms": 6 + }, + { + "charge": 44, + "subset": 470, + "terms": 6 + }, + { + "charge": 44, + "subset": 489, + "terms": 6 + }, + { + "charge": 45, + "subset": 380, + "terms": 6 + }, + { + "charge": 45, + "subset": 423, + "terms": 6 + }, + { + "charge": 51, + "subset": 379, + "terms": 7 + }, + { + "charge": 51, + "subset": 415, + "terms": 7 + }, + { + "charge": 52, + "subset": 494, + "terms": 7 + } + ], + "minimum_scalar_charge": 14, + "one_channel_counterexamples": [ + { + "actual": 0, + "expected": 2, + "input": 2, + "left": 1, + "right": 1 + }, + { + "actual": 0, + "expected": 1, + "input": 1, + "left": 1, + "right": 2 + }, + { + "actual": 1, + "expected": 2, + "input": 2, + "left": 1, + "right": 3 + }, + { + "actual": 2, + "expected": 1, + "input": 1, + "left": 2, + "right": 1 + }, + { + "actual": 0, + "expected": 1, + "input": 1, + "left": 2, + "right": 2 + }, + { + "actual": 2, + "expected": 1, + "input": 1, + "left": 2, + "right": 3 + }, + { + "actual": 3, + "expected": 1, + "input": 1, + "left": 3, + "right": 1 + }, + { + "actual": 0, + "expected": 1, + "input": 1, + "left": 3, + "right": 2 + }, + { + "actual": 3, + "expected": 1, + "input": 1, + "left": 3, + "right": 3 + } + ], + "operator_rank": 2, + "term_cost_grid": [ + 7, + 7, + 8, + 7, + 7, + 8, + 7, + 7, + 8 + ], + "union_support_charge": 8, + "witness": [ + [ + 1, + 1, + 7 + ], + [ + 2, + 2, + 7 + ] + ] + }, + { + "block": 4, + "columns": [ + 8, + 9 + ], + "direct_scalar_charge": 14, + "feasible_subsets": [ + { + "charge": 14, + "subset": 17, + "terms": 2 + }, + { + "charge": 15, + "subset": 96, + "terms": 2 + }, + { + "charge": 15, + "subset": 132, + "terms": 2 + }, + { + "charge": 21, + "subset": 88, + "terms": 3 + }, + { + "charge": 21, + "subset": 131, + "terms": 3 + }, + { + "charge": 22, + "subset": 22, + "terms": 3 + }, + { + "charge": 22, + "subset": 41, + "terms": 3 + }, + { + "charge": 22, + "subset": 266, + "terms": 3 + }, + { + "charge": 23, + "subset": 324, + "terms": 3 + }, + { + "charge": 23, + "subset": 416, + "terms": 3 + }, + { + "charge": 28, + "subset": 202, + "terms": 4 + }, + { + "charge": 29, + "subset": 323, + "terms": 4 + }, + { + "charge": 29, + "subset": 408, + "terms": 4 + }, + { + "charge": 30, + "subset": 46, + "terms": 4 + }, + { + "charge": 30, + "subset": 269, + "terms": 4 + }, + { + "charge": 30, + "subset": 306, + "terms": 4 + }, + { + "charge": 36, + "subset": 205, + "terms": 5 + }, + { + "charge": 36, + "subset": 242, + "terms": 5 + }, + { + "charge": 36, + "subset": 465, + "terms": 5 + }, + { + "charge": 37, + "subset": 103, + "terms": 5 + }, + { + "charge": 37, + "subset": 188, + "terms": 5 + }, + { + "charge": 38, + "subset": 309, + "terms": 5 + }, + { + "charge": 43, + "subset": 95, + "terms": 6 + }, + { + "charge": 43, + "subset": 187, + "terms": 6 + }, + { + "charge": 44, + "subset": 245, + "terms": 6 + }, + { + "charge": 44, + "subset": 470, + "terms": 6 + }, + { + "charge": 44, + "subset": 489, + "terms": 6 + }, + { + "charge": 45, + "subset": 380, + "terms": 6 + }, + { + "charge": 45, + "subset": 423, + "terms": 6 + }, + { + "charge": 51, + "subset": 379, + "terms": 7 + }, + { + "charge": 51, + "subset": 415, + "terms": 7 + }, + { + "charge": 52, + "subset": 494, + "terms": 7 + } + ], + "minimum_scalar_charge": 14, + "one_channel_counterexamples": [ + { + "actual": 0, + "expected": 2, + "input": 2, + "left": 1, + "right": 1 + }, + { + "actual": 0, + "expected": 1, + "input": 1, + "left": 1, + "right": 2 + }, + { + "actual": 1, + "expected": 2, + "input": 2, + "left": 1, + "right": 3 + }, + { + "actual": 2, + "expected": 1, + "input": 1, + "left": 2, + "right": 1 + }, + { + "actual": 0, + "expected": 1, + "input": 1, + "left": 2, + "right": 2 + }, + { + "actual": 2, + "expected": 1, + "input": 1, + "left": 2, + "right": 3 + }, + { + "actual": 3, + "expected": 1, + "input": 1, + "left": 3, + "right": 1 + }, + { + "actual": 0, + "expected": 1, + "input": 1, + "left": 3, + "right": 2 + }, + { + "actual": 3, + "expected": 1, + "input": 1, + "left": 3, + "right": 3 + } + ], + "operator_rank": 2, + "term_cost_grid": [ + 7, + 7, + 8, + 7, + 7, + 8, + 7, + 7, + 8 + ], + "union_support_charge": 8, + "witness": [ + [ + 1, + 1, + 7 + ], + [ + 2, + 2, + 7 + ] + ] + } + ], + "controls": { + "broken_frame": "REJECTED", + "omitted_block": "REJECTED", + "rank_one_rejections": 45, + "rational_vs_binary_rank": [ + 3, + 2 + ], + "switched_channel": "REJECTED", + "winning_term_omissions": 10 + }, + "copy_only_line_port_screens": { + "baseline_line": { + "a_bracket": [ + "973733779/500000000000", + "1947467559/1000000000000" + ], + "centre": 63, + "model": { + "R": "42", + "deficit": "107/3", + "idle_mass": "1150", + "local_mass": "5129", + "total_mass": "6279", + "w": "296/3" + }, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "unpaid": 1 + }, + "blockwise_scalar_copy_only": { + "a_bracket": [ + "87582827/62500000000", + "1401325233/1000000000000" + ], + "centre": 73, + "model": { + "R": "42", + "deficit": "77/3", + "idle_mass": "1150", + "local_mass": "5139", + "total_mass": "6289", + "w": "296/3" + }, + "profile": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 17, + "8": 3 + }, + "unpaid": 1 + } + }, + "direct_ten_channel_charge": 74, + "dirty_input_columns": 661, + "dirty_map_sha256": "ae93f3411b3c799e482738a89db1e8a7f48bac8768030a649b2ffd63034e6b62", + "enumerated_subsets": 2560, + "exact_factorizations": 160, + "literal_union_copy_failure": { + "actual": 0, + "dirty_entries": 17146, + "expected": 1, + "input": "source port 0 = 1, all other inputs = 0", + "source_entries": 5838, + "target": 0 + }, + "ordered_gl2_bases": 30, + "parseval_identity": "PASS", + "predecessor_head": "9a891c9cb25b15f5a189bcad1d022198adeaf885", + "scope": "Exact all-length floor only within each fixed rank-two coefficient block; no cross-block rebasing, new physical block-copy primitive, new plane geometry, complete supplier or kappa claim.", + "seed": "3cc9f4c8f3719f13f4ae6bf28c9ba982", + "source_decoder_rank": 9, + "status": "PASS_P111_PARSEVAL_COPY_INTERFACE", + "targets": 111, + "track": "recursive-interfaces", + "union_support_sum_not_scalar_invoice": 40 +} diff --git a/research/p111-parseval-copy-interface/SELECTION.json b/research/p111-parseval-copy-interface/SELECTION.json new file mode 100644 index 0000000000..74f1ad0cab --- /dev/null +++ b/research/p111-parseval-copy-interface/SELECTION.json @@ -0,0 +1,60 @@ +{ + "seed": "3cc9f4c8f3719f13f4ae6bf28c9ba982", + "track": "recursive-interfaces", + "suggestions": [ + { + "task_id": "coverage-law-change", + "scope_key": "f383d8fc405ee6982cdd", + "question": "Can a template or call contract leave two or more unpaid coordinates per live family?", + "method": "Find an obstruction: show which data-endpoint obligation forces exactly one unpaid coordinate in the current template.", + "starting_points": ["research/complex-local-word-ceiling/README.md", "research/idle-axis-hosting/PROOF.md", "certificates/selected-result.json"], + "acceptance_gate": "An explicit replacement identity, verified on a small complete instance with dirty inputs, priced with ceiling.ceiling(unpaid=...).", + "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": "Explain where the single unpaid coordinate per family comes from in the hosted template; propose one change and price it. Ideal budget: two unpaid coordinates per family is 3.77x (levers.py).", + "bottleneck_link": "The deficit is one coordinate per family minus the centre charge; doubling unpaid coordinates per family scales it directly.", + "allowed_variations": ["One template change or one endpoint-contract change.", "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": ["Counting a coordinate as unpaid while leaving it unadvanced in the data endpoint."], + "overlap_terms": ["coverage identity", "unpaid coordinate", "deficit law", "W - 64N"], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + }, + { + "task_id": "connector-alphabet-change", + "scope_key": "ff4f5113ed2256ab19ed", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "method": "Construct and charge a legal extra operation on a minimal instance.", + "starting_points": ["research/universal-connector-boundary/README.md", "certificates/selected-result.json"], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free.", + "first_step": {"command": ["python3", "-B", "research/universal-connector-boundary/verify.py"], "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."}, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": ["Choose one additional operation and a small source count for its first counterexample."], + "scope_change_triggers": ["Keeping the alphabet and only increasing the source count; record this as a changed assignment."], + "overlap_terms": ["universal connector", "source-toggle", "connector alphabet"], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + }, + { + "task_id": "persistent-boundary", + "scope_key": "73c0a233e7e1abdccbfe", + "question": "Can a specified pair of consecutive calls eliminate a restoration that the next call reconstructs?", + "method": "Derive a lower bound for the compulsory transitions of one proposed typed interface.", + "starting_points": ["research/heterogeneous-owner-assembly/README.md", "certificates/selected-result.json"], + "acceptance_gate": "Show actual eliminated work and legal composition; changing a scalar recurrence into a matrix is insufficient.", + "first_step": {"command": ["python3", "-B", "scripts/research_baseline.py"], "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", "inspect": "Find a concrete consecutive-call boundary in the selected review and list its entry/exit obligations.", "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."}, + "first_experiment": "Specify two call types and one operation actually removed by composition; derive the normalized recurrence.", + "bottleneck_link": "Eliminating compulsory boundary work can lower recursive cost beyond packing gains.", + "allowed_variations": ["A two-type pilot or one explicit deferred restoration."], + "scope_change_triggers": ["Rewriting the old scalar recurrence as a matrix without eliminating work."], + "overlap_terms": ["persistent boundary", "deferred restoration", "multitype"], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + } + ], + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "catalog_assessed_on": "2026-10-13", + "priority_revision": 3, + "priority_log": "docs/research/research-priority-log.md", + "catalog_sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "selected": {"kappa": "836330098538459/500000000000000000", "review": "docs/research/community-batch1099-review.md", "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json", "reproduce": "make frontier1094-verify"}, + "status": "SUGGESTIONS_ONLY_NOT_RESERVED", + "next_step": "Check live overlap, refine one question's object and domain, and record a bounded task card. A different seed or scope key is not evidence of novelty." +} diff --git a/research/p111-parseval-copy-interface/SOURCE-CLAIM.json b/research/p111-parseval-copy-interface/SOURCE-CLAIM.json new file mode 100644 index 0000000000..30167c6b80 --- /dev/null +++ b/research/p111-parseval-copy-interface/SOURCE-CLAIM.json @@ -0,0 +1,16 @@ +{ + "predecessor_pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/1900", + "head_commit": "9a891c9cb25b15f5a189bcad1d022198adeaf885", + "author": "Cinna Davis / 1337isnot1337, with substantial OpenAI Codex assistance", + "files": { + "research/bit-p111-parseval-plane-decoder-seedceccc765/README.md": "c6d2da4dfb23a62746c896305021be204fd104b8", + "research/bit-p111-parseval-plane-decoder-seedceccc765/verify.py": "0728799018f6dc6fb6c4724d406dc868ed80af72" + }, + "claimed_copy_charge": 40, + "baseline_copy_charge": 63, + "claimed_unpaid_coordinates": 2, + "frame_columns_little_endian": [3, 5, 6, 7, 8, 16, 32, 64, 128, 256], + "blocks_zero_based": [[0, 1], [2, 3], [4, 5], [6, 7], [8, 9]], + "source_extraction": "Exact constants and claims transcribed from the pinned README and verifier; no predecessor executable imported. Git blob IDs obtained from the live PR files API on 2026-10-14.", + "audit_scope": "All scalar rank-one factorizations whose two factors stay in each fixed block's two-dimensional binary source and target coefficient spans; no cancellation or rebasing across blocks. This is not a bound on a new physical block-valued operation." +} diff --git a/research/p111-parseval-copy-interface/SOURCES.json b/research/p111-parseval-copy-interface/SOURCES.json new file mode 100644 index 0000000000..3e3d20c2ff --- /dev/null +++ b/research/p111-parseval-copy-interface/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/complex-local-word-ceiling/ceiling.py", + "usage": "input", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + }, + { + "path": "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "usage": "input", + "git_blob": "e293ddc557742637f9f679f083a1a282d87b1b13", + "sha256": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4" + }, + { + "path": "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + { + "path": "research/p111-copy-rank-certificate/PROOF.md", + "usage": "provenance", + "git_blob": "0ce5a7974295ab568778a2a7548b82bf0568f608", + "sha256": "d9fb73cfa2bf986e8f5d93d49a94451c15a510e2033aeafbba0f3d05a9cc28fc" + }, + { + "path": "research/bit-orthogonal-pair-decoders/PROOF.md", + "usage": "provenance", + "git_blob": "be3243952be4a1a8f5901829c73ce425ab217d16", + "sha256": "d89b42d4aa2e6bf2c3ac454404fd1aeddbf2eb07f6ff1fc606057e3b2a928f78" + } + ] +} diff --git a/research/p111-parseval-copy-interface/TASK.json b/research/p111-parseval-copy-interface/TASK.json new file mode 100644 index 0000000000..2d7465a7eb --- /dev/null +++ b/research/p111-parseval-copy-interface/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "coverage-law-change", + "question": "Can a template or call contract leave two or more unpaid coordinates per live family?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/idle-axis-hosting/PROOF.md", + "certificates/selected-result.json" + ], + "methods": [ + "State a replacement for the coverage identity (mass = 72W + 64N) and the contract change that realizes it, with its implementation cost.", + "Find an obstruction: show which data-endpoint obligation forces exactly one unpaid coordinate in the current template." + ], + "acceptance_gate": "An explicit replacement identity, verified on a small complete instance with dirty inputs, priced with ceiling.ceiling(unpaid=...).", + "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": "Explain where the single unpaid coordinate per family comes from in the hosted template; propose one change and price it. Ideal budget: two unpaid coordinates per family is 3.77x (levers.py).", + "bottleneck_link": "The deficit is one coordinate per family minus the centre charge; doubling unpaid coordinates per family scales it directly.", + "allowed_variations": [ + "One template change or one endpoint-contract change.", + "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": [ + "Counting a coordinate as unpaid while leaving it unadvanced in the data endpoint." + ], + "overlap_terms": [ + "coverage identity", + "unpaid coordinate", + "deficit law", + "W - 64N" + ] + }, + "scope_status": "changed", + "actual_scope": "Independently audit the implication from PR1900's valid five rank-two coefficient blocks to a copy charge of 40 and two geometric unpaid coordinates. Compute the exact minimum inherited scalar-copy invoice over every finite factorization whose factors stay in each fixed block's two-dimensional binary spans, and check dirty endpoint equality and one-channel counterexamples.", + "scope_change_reason": "The sampled endpoint-obstruction question is already answered for line ports in Discussion1587. Its active plane-port handoff and PR1900 provide a concrete changed contract to audit. This is a bounded missing-implication audit, not a new plane supplier or a proof against all block-valued operations.", + "bottleneck_link": "A claimed copy reduction 63 to 40 and unpaid=2 both alter the coverage deficit. They require distinct operator and geometric endpoint obligations; coefficient grouping alone must not be priced as if these obligations were discharged.", + "budget_minutes": 120, + "stop_rule": "Exhaust all 512 subsets of nine scalar rank-one products per fixed block; repeated products cancel, so this covers arbitrary finite within-block factorizations. Include all six ordered GL2(F2) bases of each block. Reconstruct all 111 target forms on all 661 dirty columns. Do not search new decoders or infer lower bounds for new physical block-valued operations.", + "outcome": "negative-result", + "result": "Exact scoped obstruction: blockwise scalar optimum 73, literal Parseval expansion 74, baseline 63. The union-support sum 40 is not a scalar invoice; a literal one-copy-per-union replacement differs on 17146 dirty matrix entries. The valid F2 Parseval identity is confirmed. No new supplier or kappa.", + "evidence": "Independent source-bound reconstruction; rational support-pairing ranks cross-checked by full-Gram modular elimination; 2560 subsets and 160 exact factorizations including all 30 ordered GL2 bases; 45 one-channel counterexamples, 10 winning-term omissions and semantic field/frame/channel controls; exact copy-only line-port ceiling 0.001401325233; registered Python 3.12 replay command in VERIFY.json.", + "author": "Adam Gall, with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance with source analysis, exact calculations, implementation and writing; no independent human review claimed.", + "assignment_seed": "3cc9f4c8f3719f13f4ae6bf28c9ba982", + "track": "recursive-interfaces", + "catalogue_scope_key": "f383d8fc405ee6982cdd", + "concrete_scope_key": "p111-pr1900-fixed-five-blocks-minimal-scalar-factorization-copy-interface", + "predecessor": { + "pr": 1900, + "head": "9a891c9cb25b15f5a189bcad1d022198adeaf885", + "author": "Cinna Davis / 1337isnot1337", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1929#discussioncomment-18925833", + "nearest_handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1587#discussioncomment-18925111" + }, + "optimistic_full_cost_budget": "Keep every incumbent side child and physical line-port contract; charge each actual scalar copy by its rational support-pairing rank, all basis changes and cleanup nonnegative. Compare the mandatory copy-only invoice against baseline63; if it is already worse, no synthesis for this fixed blockwise route. Hypothetical block-valued plane operations remain outside the lower bound.", + "success_or_falsification": "The exact within-block scalar floor 73 already exceeds baseline63 before implementation extras, so synthesis of this fixed route stops. Rank-two/full-dirty-map checks and exhaustive coverage guard the reduction. Hypothetical physical block primitives and cross-block factorization are outside the obstruction.", + "open_questions": [ + { + "question": "Can a genuinely block-valued physical operation implement these rank-two coefficient blocks at one union-support B14 charge?", + "why_it_matters": "Such a changed operation, rather than renaming two scalar channels, could bypass the inherited scalar realization floor.", + "first_step": "Write the complete operator on two independent dirty source and target streams, including frames and restored scratch, and compare it with one legal copy call.", + "blocked_by": "No typed physical block-copy implementation is supplied by the coefficient factorization." + }, + { + "question": "Can a completed physical two-dimensional port contract share boundary work unavailable to the scalar interpretation?", + "why_it_matters": "Only a changed physical endpoint can justify two unpaid coordinates per family.", + "first_step": "Specify each data family's rational plane and replay a small dirty endpoint with every copy, frame change and restoration charged.", + "blocked_by": "The binary coefficient planes do not specify physical port planes or their route." + } + ] +} diff --git a/research/p111-parseval-copy-interface/VERIFY.json b/research/p111-parseval-copy-interface/VERIFY.json new file mode 100644 index 0000000000..6fcf38ded3 --- /dev/null +++ b/research/p111-parseval-copy-interface/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/complex-local-word-ceiling/ceiling.py", + "research/e8-bit-p111-tuned/tune/EXPECTED.json", + "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All 661 dirty columns and 111 source rows; exact rational plus modular support ranks; all 2560 within-block subsets, 160 factorizations and 30 GL2 bases; 45 single-channel and ten term-omission failures; frame/channel/field controls; exact copy-only line-port moment brackets; source pins and deterministic receipt." + } + ] +} diff --git a/research/p111-parseval-copy-interface/verify.py b/research/p111-parseval-copy-interface/verify.py new file mode 100755 index 0000000000..185b7d3937 --- /dev/null +++ b/research/p111-parseval-copy-interface/verify.py @@ -0,0 +1,351 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Audit fixed P111 Parseval blocks in the inherited scalar-copy model. + +Adam Gall, with substantial OpenAI Codex assistance. No predecessor executable +is imported. The exact interval engine is reused unchanged and source-pinned. +""" + +import argparse +from collections import Counter +from fractions import Fraction +from functools import lru_cache +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +WORD = "research/e8-bit-p111-tuned/tune/bitE8mut-p111-tuned.json.gz" +EXPECTED = "research/e8-bit-p111-tuned/tune/EXPECTED.json" +CEILING = "research/complex-local-word-ceiling/ceiling.py" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def combine(vectors, coefficients): + value = 0 + for i, vector in enumerate(vectors): + if coefficients >> i & 1: + value ^= vector + return value + + +def binary_rank(vectors): + pivots = {} + for value in vectors: + while value: + bit = value.bit_length() - 1 + if bit not in pivots: + pivots[bit] = value + break + value ^= pivots[bit] + return len(pivots) + + +def rational_basis(rows): + """Incremental exact row reduction; no numerical rank tolerance.""" + pivots = {} + for original in rows: + row = [Fraction(value) for value in original] + for col, pivot in sorted(pivots.items()): + coefficient = row[col] + if coefficient: + row = [a - coefficient * b for a, b in zip(row, pivot)] + col = next((i for i, value in enumerate(row) if value), None) + if col is not None: + coefficient = row[col] + pivots[col] = [value / coefficient for value in row] + return list(pivots.values()) + + +def modular_rank(rows, prime=101): + """Separate full-matrix elimination supplies a certified rank lower bound.""" + matrix = [[value % prime for value in row] for row in rows] + if not matrix: + return 0 + rank = 0 + for col in range(len(matrix[0])): + pivot = next((i for i in range(rank, len(matrix)) if matrix[i][col]), None) + if pivot is None: + continue + matrix[rank], matrix[pivot] = matrix[pivot], matrix[rank] + inverse = pow(matrix[rank][col], -1, prime) + matrix[rank] = [(value * inverse) % prime for value in matrix[rank]] + for i in range(rank + 1, len(matrix)): + factor = matrix[i][col] + if factor: + matrix[i] = [(a - factor * b) % prime + for a, b in zip(matrix[i], matrix[rank])] + rank += 1 + return rank + + +def decoder_map(left, right, targets): + return [combine(right, sum(((column >> target) & 1) << i + for i, column in enumerate(left))) + for target in range(targets)] + + +def outer2(left, right): + return sum(1 << (2 * i + j) for i in range(2) for j in range(2) + if left >> i & 1 and right >> j & 1) + + +def apply2(matrix, vector): + return sum(((matrix >> (2 * i) & 3 & vector).bit_count() % 2) << i + for i in range(2)) + + +def parseval(columns): + return all(sum(((c >> i) & 1) * ((c >> j) & 1) for c in columns) % 2 + == (i == j) for i in range(9) for j in range(9)) + + +def audit(): + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + for entry in sources["files"]: + if entry["usage"] == "input": + require(hashlib.sha256((ROOT / entry["path"]).read_bytes()).hexdigest() + == entry["sha256"], "source pin mismatch: " + entry["path"]) + claim = json.loads((PACKAGE / "SOURCE-CLAIM.json").read_text()) + selection = json.loads((PACKAGE / "SELECTION.json").read_text()) + require(selection["seed"] == "3cc9f4c8f3719f13f4ae6bf28c9ba982" + and selection["track"] == "recursive-interfaces", "selection changed") + require(claim["head_commit"] == "9a891c9cb25b15f5a189bcad1d022198adeaf885", + "audited predecessor head changed") + columns = claim["frame_columns_little_endian"] + blocks = claim["blocks_zero_based"] + require(columns == [3, 5, 6, 7, 8, 16, 32, 64, 128, 256] + and blocks == [[0, 1], [2, 3], [4, 5], [6, 7], [8, 9]], + "audited factorization changed") + + word = json.loads(gzip.decompress((ROOT / WORD).read_bytes())) + expected = json.loads((ROOT / EXPECTED).read_text()) + ports = word["v"] + registers = 2 * ports + word["R"] + require((ports, registers, word["h"]) == (111, 661, 8), "not selected P111") + require(word["punctured"] == [10, 15, 51, 53, 56, 66, 72, 89, 111], + "selected puncture changed") + values = [1 << i for i in range(registers)] + for section in ("D", "A"): + for _frame, destination, sources in word[section]: + for source in sources: + values[destination] ^= values[source] + left = [sum(1 << t for t, row in enumerate(word["scatter"]) if i in row) + for i in range(9)] + right = [values[index] for index in word["ret"]] + require(len(right) == 9, "retained channel count changed") + old_map = decoder_map(left, right, ports) + source_mask = (1 << ports) - 1 + lines = word["lines"] + gram = [[sum(a * b for a, b in zip(t, s)) for s in lines] for t in lines] + require(all(value % 2 == 0 for row in gram for value in row), "nonintegral G") + b0 = [sum(((1 + value // 2) & 1) << s for s, value in enumerate(row)) + for row in gram] + require([row & source_mask for row in old_map] == b0, "selected B0 map mismatch") + require(binary_rank(b0) == 9, "selected source decoder must have rank nine") + require(binary_rank(left) == binary_rank(right) == 9, "channels not independent") + require(parseval(columns), "Parseval identity failed") + new_left = [combine(left, column) for column in columns] + new_right = [combine(right, column) for column in columns] + require(decoder_map(new_left, new_right, ports) == old_map, + "valid Parseval decoder differs on a dirty column") + + @lru_cache(None) + def support_basis(mask): + return rational_basis([row for i, row in enumerate(lines) if mask >> i & 1]) + + @lru_cache(None) + def pairing_cost(target_mask, input_mask): + input_mask &= source_mask + targets = support_basis(target_mask) + inputs = support_basis(input_mask) + small = [[sum(a * b for a, b in zip(t, s)) for s in inputs] for t in targets] + rank = len(rational_basis(small)) + # Independent elimination on the original (not basis-compressed) Gram + # matrix proves the matching lower bound over Q; equality is required. + full = [[gram[t][s] for s in range(ports) if input_mask >> s & 1] + for t in range(ports) if target_mask >> t & 1] + require(modular_rank(full) == rank, "modular/rational rank disagreement") + return rank + + baseline_costs = [pairing_cost(a, b) for a, b in zip(left, right)] + require(baseline_costs == expected["word"]["copy_ranks"] == [7] * 9, + "baseline copy ranks changed") + reports = [] + winning_ranks = Counter() + rank_one_controls = 0 + gl2_count = 0 + for number, (i, j) in enumerate(blocks): + ls = [new_left[i], new_left[j]] + rs = [new_right[i], new_right[j]] + require(binary_rank(ls) == binary_rank(rs) == 2, "rank-two block collapsed") + require(binary_rank([r & source_mask for r in rs]) == 2, + "source-restricted block collapsed") + block_map = decoder_map(ls, rs, ports) + require(binary_rank(block_map) == 2, "block operator has wrong rank") + terms = [(a, b, outer2(a, b), pairing_cost(combine(ls, a), combine(rs, b))) + for a in (1, 2, 3) for b in (1, 2, 3)] + union_cost = pairing_cost(ls[0] | ls[1], rs[0] | rs[1]) + require(union_cost == 8, "predecessor union-support rank changed") + # Nine possible nonzero scalar products, any repeated product cancels + # modulo two while its strictly positive price cannot improve a bill. + # Therefore these 512 subsets cover arbitrary finite scalar words in + # the declared two-dimensional factor spans, not merely two terms. + feasible = [] + for subset in range(1 << len(terms)): + matrix = charge = 0 + chosen_left, chosen_right = [], [] + for bit, (a, b, product, price) in enumerate(terms): + if subset >> bit & 1: + matrix ^= product + charge += price + chosen_left.append(combine(ls, a)) + chosen_right.append(combine(rs, b)) + if matrix == 9: # row-major identity matrix over F2 + require(decoder_map(chosen_left, chosen_right, ports) == block_map, + "coefficient equality did not preserve the dirty block") + feasible.append({"subset": subset, "charge": charge, + "terms": subset.bit_count()}) + require(len(feasible) == 32, "incomplete subset census") + feasible.sort(key=lambda item: (item["charge"], item["subset"])) + best = feasible[0] + winners = [term for bit, term in enumerate(terms) if best["subset"] >> bit & 1] + for _a, _b, _product, price in winners: + winning_ranks[price] += 1 + # Each ordered GL2 basis has a unique dual; all six are represented by + # the three unordered two-term factorizations in the full subset list. + two_term = [item for item in feasible if item["terms"] == 2] + require(len(two_term) == 3, "missing GL2 factorization") + gl2_count += 2 * len(two_term) + one_channel_witnesses = [] + for a, b, product, _price in terms: + require(product != 9, "one scalar channel unexpectedly has rank two") + require(decoder_map([combine(ls, a)], [combine(rs, b)], ports) != block_map, + "one-channel dirty counterexample missing") + witness = next(x for x in (1, 2, 3) if apply2(product, x) != x) + one_channel_witnesses.append({"left": a, "right": b, "input": witness, + "expected": witness, + "actual": apply2(product, witness)}) + rank_one_controls += 1 + for omitted in range(len(winners)): + retained = winners[:omitted] + winners[omitted + 1:] + require(decoder_map([combine(ls, a) for a, _b, _p, _c in retained], + [combine(rs, b) for _a, b, _p, _c in retained], + ports) != block_map, + "deleting a winning term failed to break the dirty endpoint") + reports.append({ + "block": number, "columns": [i, j], "operator_rank": 2, + "union_support_charge": union_cost, + "term_cost_grid": [term[3] for term in terms], + "direct_scalar_charge": terms[0][3] + terms[4][3], + "minimum_scalar_charge": best["charge"], + "witness": [[a, b, price] for a, b, _product, price in winners], + "feasible_subsets": feasible, + "one_channel_counterexamples": one_channel_witnesses, + }) + minima = [report["minimum_scalar_charge"] for report in reports] + require(minima == [16, 15, 14, 14, 14], "fixed-block optimum changed") + require(dict(winning_ranks) == {8: 3, 7: 7}, "winning copy profile changed") + + union_left = [new_left[i] | new_left[j] for i, j in blocks] + union_right = [new_right[i] | new_right[j] for i, j in blocks] + union_map = decoder_map(union_left, union_right, ports) + differences = [a ^ b for a, b in zip(old_map, union_map)] + source_differences = sum((row & source_mask).bit_count() for row in differences) + dirty_differences = sum(row.bit_count() for row in differences) + require((source_differences, dirty_differences) == (5838, 17146), + "literal one-union-copy counterexample changed") + require((old_map[0] & 1, union_map[0] & 1) == (1, 0), "small witness changed") + + broken = columns.copy() + broken[3] ^= 256 + require(not parseval(broken), "broken-frame control accepted") + require(decoder_map(new_left[:-2], new_right[:-2], ports) != old_map, + "omitted-block control accepted") + switched = new_right.copy() + switched[0], switched[1] = switched[1], switched[0] + require(decoder_map(new_left, switched, ports) != old_map, + "switched-channel control accepted") + field_fixture = [[1, 1, 0], [1, 0, 1], [0, 1, 1]] + require(len(rational_basis(field_fixture)) == 3 + and binary_rank([3, 5, 6]) == 2, "rank field control failed") + + profile = {int(rank): count for rank, count in expected["word"]["local_histogram"].items()} + changed = profile.copy() + changed[7] -= 9 + for rank, count in winning_ranks.items(): + changed[rank] = changed.get(rank, 0) + count + # No extra basis, route, storage or cleanup credit is assumed. Setting all + # of those nonnegative charges to zero is deliberately favorable. + spec = importlib.util.spec_from_file_location("pinned_ceiling", ROOT / CEILING) + ceiling = importlib.util.module_from_spec(spec) + spec.loader.exec_module(ceiling) + screens = {} + for name, local, centre in (("baseline_line", profile, 63), + ("blockwise_scalar_copy_only", changed, 73)): + model = ceiling.model(local, 64, 888, 9, centre, R=42, unpaid=1) + bracket = ceiling.ceiling(local, 64, 888, 9, centre, R=42, unpaid=1, + grid=Fraction(1, 10**12)) + screens[name] = {"profile": {str(k): n for k, n in sorted(local.items())}, + "centre": centre, "unpaid": 1, + "model": {k: str(value) for k, value in model.items()}, + "a_bracket": [str(value) for value in bracket]} + require(screens["blockwise_scalar_copy_only"]["a_bracket"] + == ["87582827/62500000000", "1401325233/1000000000000"], + "changed exact ceiling mismatch") + require(screens["baseline_line"]["a_bracket"] + == ["973733779/500000000000", "1947467559/1000000000000"], + "baseline exact ceiling mismatch") + require(Fraction(screens["blockwise_scalar_copy_only"]["a_bracket"][1]) + < Fraction(screens["baseline_line"]["a_bracket"][0]), + "copy-only route does not fail the target") + width = (registers + 7) // 8 + digest = hashlib.sha256(b"".join(row.to_bytes(width, "little") for row in old_map)).hexdigest() + return { + "status": "PASS_P111_PARSEVAL_COPY_INTERFACE", + "seed": selection["seed"], "track": selection["track"], + "predecessor_head": claim["head_commit"], + "targets": ports, "dirty_input_columns": registers, + "source_decoder_rank": 9, "dirty_map_sha256": digest, + "parseval_identity": "PASS", "baseline_scalar_charge": sum(baseline_costs), + "direct_ten_channel_charge": sum(r["direct_scalar_charge"] for r in reports), + "best_blockwise_scalar_charge": sum(minima), + "union_support_sum_not_scalar_invoice": sum(r["union_support_charge"] for r in reports), + "enumerated_subsets": 5 * 512, "exact_factorizations": 5 * 32, + "ordered_gl2_bases": gl2_count, "blocks": reports, + "literal_union_copy_failure": {"source_entries": source_differences, + "dirty_entries": dirty_differences, + "input": "source port 0 = 1, all other inputs = 0", + "target": 0, "expected": 1, "actual": 0}, + "controls": {"rank_one_rejections": rank_one_controls, + "winning_term_omissions": 10, "broken_frame": "REJECTED", + "omitted_block": "REJECTED", "switched_channel": "REJECTED", + "rational_vs_binary_rank": [3, 2]}, + "copy_only_line_port_screens": screens, + "scope": "Exact all-length floor only within each fixed rank-two coefficient block; no cross-block rebasing, new physical block-copy primitive, new plane geometry, complete supplier or kappa claim.", + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="regenerate deterministic RESULT.json") + args = parser.parse_args() + report = audit() + result = PACKAGE / "RESULT.json" + if args.write: + result.write_text(json.dumps(report, indent=2, sort_keys=True) + "\n") + else: + require(json.loads(result.read_text()) == report, "RESULT.json differs from exact replay") + print(report["status"], "blocks=5 subsets=2560 factorizations=160", + "dirty_columns=661 copy_min=73 baseline=63 union_failure_entries=17146") + + +if __name__ == "__main__": + main()