diff --git a/research/productive-helper-color-cut/.gitattributes b/research/productive-helper-color-cut/.gitattributes new file mode 100644 index 0000000000..fa1385d99a --- /dev/null +++ b/research/productive-helper-color-cut/.gitattributes @@ -0,0 +1 @@ +* -text diff --git a/research/productive-helper-color-cut/PROOF-FAMILY.md b/research/productive-helper-color-cut/PROOF-FAMILY.md new file mode 100644 index 0000000000..b979e33476 --- /dev/null +++ b/research/productive-helper-color-cut/PROOF-FAMILY.md @@ -0,0 +1,108 @@ +# The whole three-output basis family fixing the protected value + +This extends the color-cut obstruction in [PROOF.md](PROOF.md) to an infinite +family of direct targets. It uses the same 24 input registers, four colors, +ascending canonical scalar model and nine required monochrome output caps. +It makes no claim about arbitrary native operations, changed output caps or a +paid nonascending circuit. + +Write `u = H output416 = input13 + input416`. For rational parameters +`lambda, mu`, change the other two output rows by + +```text +output419 += lambda*u, +output421 += mu*u. +``` + +All other output rows remain those of `H = P T M`. In particular, the nine +monochrome output roles and their caps remain unchanged. Even if a parameter +choice fails an additional physical support condition, granting it here only +enlarges the class to be obstructed. + +## Exact uniform rank certificate + +Let `G` be the 15-by-8 dirty-output/hot-input block reconstructed from `H`, +in the row and column orders in `PROOF.md`. The changed block is + +```text +G(lambda,mu) = G + (lambda*e419 + mu*e421)*e13^T. +``` + +The seven columns other than column13 are unchanged and have exact rank7. +For every rational parameter pair, an exact right-kernel vector, in hot order +`13,16,43,44,51,78,99,104`, is + +```text +n(lambda,mu) = + (2, mu, -1-lambda-mu, mu, -2*lambda, + lambda-1, lambda-1, 1+lambda-mu). +``` + +Its first coordinate is always2, so it is never zero. Thus the rank of +`G(lambda,mu)` is exactly7 for all parameters, and its rowspace is precisely +the hyperplane perpendicular to `n(lambda,mu)`. + +`check_family.py` checks this as a polynomial identity, without selecting a +grid of parameters. Writing `n=n0+lambda*nL+mu*nM`, it verifies the constant, +both linear and all three quadratic coefficients of `G(lambda,mu)*n` on +every row. In particular, `nL[13]=nM[13]=0` makes the quadratic coefficients +vanish. It independently checks the rank7 unaffected-column minor and the +rank5 block obtained by deleting both changed rows. + +## The single-color directions never span the rowspace + +A hyperplane in eight coordinates intersects a two-coordinate color plane +in dimension2 if both corresponding normal coordinates vanish, and otherwise +in dimension1. Applying this to the four disjoint color pairs gives: + +| Color pair | Restriction of the normal | Intersection dimension | +|---|---|---| +| 13,51 | `(2,-2*lambda)` | 1 | +| 78,99 | `(lambda-1,lambda-1)` | `1 + [lambda=1]` | +| 16,44 | `(mu,mu)` | `1 + [mu=0]` | +| 43,104 | `(-1-lambda-mu,1+lambda-mu)` | `1 + [lambda=-1 and mu=0]` | + +The final row follows by adding the two equations to get `mu=0`, then +substituting to get `lambda=-1`. Since the color pairs have disjoint support, +their intersection subspaces form a direct sum. Their total dimension is + +```text +4 + [lambda=1] + [mu=0] + [lambda=-1 and mu=0] <= 6 < 7. +``` + +For `mu != 0` the sum is at most5. For `mu=0`, the conditions `lambda=1` +and `lambda=-1` are disjoint over the rationals, so the sum is at most6. +The necessary color-cut condition therefore fails for every parameter pair. +There is no ascending realization of any target in this family under the +stated model and boundary caps. + +## Coverage of arbitrary invertible mixing that fixes u + +Consider any rational invertible basis change on the three output values +`(u, output419, output421)` that fixes the value `u` exactly. Its matrix has +the block form + +```text +F = [[1, 0], + [v, A]], A in GL(2,Q), v in Q^2. +``` + +It factors exactly as + +```text +F = diag(1,A) * [[1, 0], + [A^-1*v, I2]]. +``` + +The right factor is the two-shear family above. The left factor mixes only +dirty output rows419 and421 by an invertible matrix. It preserves the +rowspace of the complete dirty-output/hot-input block. Hence it cannot repair +the failure of the color-cut condition. This proves the same obstruction for +every invertible rational basis change on these three outputs that fixes `u`. + +If these three channels pass through the same native map, this is the natural +entire commuting three-channel basis family fixing the protected value. +The obstruction itself does not require native-map equality: it applies to +the direct scalar targets irrespective of their later native feasibility. +It does not cover mixing another output into the family, changing `u`, or +letting one of the nine monochrome output caps become multicolor. diff --git a/research/productive-helper-color-cut/PROOF.md b/research/productive-helper-color-cut/PROOF.md new file mode 100644 index 0000000000..5592953206 --- /dev/null +++ b/research/productive-helper-color-cut/PROOF.md @@ -0,0 +1,279 @@ +# A color-cut obstruction for one direct scalar encoder + +The proposed direct encoder `H = P T M` has no ascending canonical-chart +ADD/SCALE realization on its 24 registers with the entry and exit charts +specified below. This statement permits arbitrary rational coefficients, +arbitrary intermediate charts and arbitrary interleavings. It assumes no +particular preparation, cold basis, Schur factorization or compensation prefix. + +This is a scoped obstruction to a scalar encoder. It is not a lower bound for +general multiplication, a tariff optimum, or an improvement to the selected +bound. In particular, nonascending transports, changed external charts, native +operations inside the interval and a different direct target remain outside +the main claim. + +## 1. Exact source and proposed target + +The immutable input is the adjacent package's +[`COMBINED-WORD.json.gz`](../productive-helper-fusion-certificate/COMBINED-WORD.json.gz): + +- compressed-byte SHA256: + `6caa29e474375298847fac8a53508f65037dc45e64d2ea0125ece9faf32b2ce4`; +- canonical JSON SHA256, using sorted keys and compact separators: + `aa4a8241da76abd2c06e6576a3ac09e77781321deaac3ad7d3ce4519342a36e6`. + +Delete `climb` records from its forward program. The half-open interval +`[9961, 10111)` contains 150 invertible scalar instructions and exactly the +registers + +```text +13, 16, 43, 44, 51, 78, 99, 104, 416, 417, ..., 431. +``` + +Let `M` be its exact rational 24-by-24 matrix, acting on a column of register +values. All 24 input values are independent and arbitrary. A zero chart never +means a zero register value. + +Define `T` on output registers 417 and 419 by + +```text +T = [[1/2, -1], + [1/2, 1]]. +``` + +Chronologically, this is `419 += 417/2; 417 -= 419`. Let `P` swap output +registers 416 and 417. The target is `H = P T M`. The checker reconstructs `M` +from every scalar instruction, applies these two row additions and the row +swap, and checks both inverse products of `M` and `H` exactly. In particular, + +```text +H output416 = input13 + input416. +``` + +The candidate was motivated by the source's exactly equal native maps 34 and +35 on registers 417 and 419. Their equality is checked, but the obstruction +does not depend on assuming that equal maps alone make a changed encoder cheap. + +The source entry charts are eight binary lines and sixteen zero subspaces: + +| Input role | Binary line generator | +|---|---:| +| 13 | 73 | +| 51 | 100 | +| 78 | 506 | +| 99 | 471 | +| 16 | 49 | +| 44 | 28 | +| 43 | 386 | +| 104 | 431 | +| 416 through 431 | zero subspace | + +These charts are reconstructed by replaying the prefix's chart annotations; +they are not supplied as a generated matrix certificate. Adapter records in +the prefix are checked to preserve their current canonical chart. + +The fixed output charts are the original local exit charts, with the output +416/417 permutation, except that output416 is required to use line73. This +is the intended one-port native input. The full list is in `RESULT.json`. +Nine of these outputs have the following charts: + +| Output roles | Chart basis | Color | +|---|---|---:| +| 13, 51 | 45, 73 | 1 | +| 78, 99 | 45, 471 | 2 | +| 427, 429 | 28, 45 | 3 | +| 425, 431 | 45, 386 | 4 | +| 416 | 73 | 1 | + +Each two-dimensional chart contains the two input lines of its color and no +input line of another color. For example, `73 XOR 100 = 45`. The checker +enumerates these small binary spans and verifies all nine assertions. No +statement about maximal relaxed suffix charts is required. + +The ordinary two-sided support tests nevertheless pass: whenever `H[j,i]` +or `H^-1[i,j]` is nonzero, input chart `i` is contained in fixed output chart +`j`. Each register's own entry chart is also contained in its exit chart. +The checker verifies all of these statements exactly. The obstruction below +therefore detects something that these entry/exit support tests do not. + +## 2. Circuit model and the general color-cut lemma + +A canonical chart is a binary linear subspace of `F_2^9`. Each register has +a chart, and an ADD can act on two registers only at a common chart. Nonzero +scalar SCALE gates act on one register. Chart transitions act as identities +on logical register values. A circuit is **ascending** when each register's +chart can only grow by subspace inclusion. There are no native maps, resets, +owned-copy centers, or additional registers inside the main claim's interval. + +Partition the eight nonzero input lines into four groups: + +```text +{13,51}, {78,99}, {16,44}, {43,104}. +``` + +The color set of a chart consists of the groups for which it contains at +least one of those input lines. Call a scalar gate monochrome if its common +chart has at most one color, and mixed if that chart has at least two colors. +Zero-color gates count as monochrome. + +**Forward support fact.** If the current logical value on a register has a +nonzero coefficient of a hot input, its chart contains that input's initial +line. Initially this holds by construction. At an ADD, both input values are +at the common chart, so it remains true for their linear combination; a +nonzero scale preserves it. Ascending transitions preserve every already +contained line. Cancellation of a coefficient can only remove an obligation. + +**No-return commutation lemma.** Every earlier mixed gate and later +monochrome gate are disjoint in their register sets. + +Indeed, if they shared a register, that register's chart at the later gate +would contain its chart at the earlier gate. It would therefore still have +at least two colors, contrary to the later gate being monochrome. It follows +that any out-of-order adjacent mixed/monochrome pair commutes as an exact +linear operation on arbitrary input values. Repeatedly exchanging such pairs +puts every monochrome scalar gate before every mixed scalar gate, without +changing the order of gates on any one register or the logical matrix. + +The argument is algebraic: it does not claim that this reordering preserves +an invoice. Chart transitions can be retained in their per-register order, +or omitted while proving the matrix identity. Before the first mixed scalar +gate on any wire, its last monochrome gate has produced a value whose hot +support belongs to at most one group. A wire with no preceding gate retains +its original value and has the same property. Any unused chart promotions +between those gates change no logical coefficients. + +Suppose a set of final registers is constrained to monochrome output caps. +No mixed gate can ever touch any of these registers: an ascending chart could +not subsequently fit its final cap. Thus, in the reordered circuit, the mixed +suffix acts invertibly only on the remaining registers. + +Let `G` be the target matrix restricted to those remaining output rows and +the eight hot input columns. Let `B` be the corresponding hot block after the +monochrome prefix, and let `R` be the mixed suffix's invertible matrix on the +remaining registers. Then + +```text +G = R B, rowspace(G) = rowspace(B). +``` + +Every row of `B` is supported within one hot-input group, by the forward +support fact. Consequently: + +> The rowspace of `G` must be spanned by its vectors supported within single +> color groups. + +No assertion that the monochrome outputs depend only on hot inputs is needed. +In this application output416 also contains its independent dirty input. +There is likewise no requirement that a particular cold subblock of the +prefix be invertible; only the actual scalar suffix `R` is used. + +## 3. Source-specific contradiction + +For `H`, the nine monochrome output roles are + +```text +13, 51, 78, 99, 427, 429, 425, 431, 416. +``` + +The other fifteen output roles, in the order used by the receipt, are + +```text +16,43,44,104,417,418,419,420,421,422,423,424,426,428,430. +``` + +The checker extracts their hot-input block `G` directly from `H`. Its exact +rank is 7. In the hot-column order + +```text +13,16,43,44,51,78,99,104, +``` + +its unique column relation, with the stated normalization, is + +```text +2 G[:,13] - G[:,43] - G[:,78] - G[:,99] + G[:,104] = 0. +``` + +In particular, every row vector `beta` in `rowspace(G)` obeys + +```text +2 beta13 - beta43 - beta78 - beta99 + beta104 = 0. +``` + +If `beta` is supported in color group `{13,51}`, the relation forces +`beta13 = 0`. A vector supported in any other color group already has +`beta13 = 0`. Hence every one-color vector in `rowspace(G)` has zero +13-coordinate, as does their span. But the source-reconstructed target has + +```text +G[output43, input13] = 1. +``` + +The necessary color-cut condition is therefore false. This proves the main +claim for all ascending scalar factorizations of the direct target with the +specified boundary charts, including arbitrary temporary uses of register416. + +For a fuller exact census, the dimensions of the four single-color +intersections of `rowspace(G)` are `1,1,2,1`. Their supports are disjoint, so +their sum has dimension 5, strictly smaller than 7. The map `w -> wG` from +15 coefficient coordinates has kernel dimension 8. Thus the preimages of all +single-color subspaces together span dimension `8+5=13`, not 15. + +`RESULT.json` records complete exact nullspace bases for the 13 masks +(empty, eight singletons and four pairs), and two common annihilators in the +15 remaining-output coordinates. These data provide independently checkable +rank certificates. The shorter column-relation contradiction above is already +sufficient for the theorem. + +## 4. Positive and mutation controls + +The original 150-instruction source is a nontrivial positive control. Its +charts are ascending. The checker classifies 40 gates as monochrome and 110 +as mixed, verifies all 72 mixed-before-monochrome inversions are disjoint, +and checks the exact 24-input matrix identity after their stable partition. +There are only eight required monochrome outputs in the original source: +register416 retains its original larger chart. Its remaining 16-row hot block +has rank 8, and its four single-color intersections have dimensions `2,2,2,2`. +It therefore passes the necessary condition, as a legal source must. + +Corruption controls reject changed source bytes, a changed target coefficient, +a wrong column-relation sign and a cross-color enlargement of a required +monochrome cap. Scope controls permit particular cross-pair capture masks: +one increases the preimage span rank to 14, and two increase it to 15. These +are checks that the restriction matters, not constructions of a legal circuit. + +The exact checker uses explicit failures rather than Python `assert`, so its +checks remain active under `python -O`. It uses only standard-library rational +arithmetic and binary-space enumeration, with no numerical optimizer. + +## 5. Scope and next questions + +The theorem addresses this exact `P T M`, this local region and these output +contracts. It does not rule out a larger encoder region, a different suffix +that permits a multicolor output416, an internal native operation, or a +nonascending circuit whose extra costs are paid elsewhere. It makes no claim +that a rank-feasible capture scheme necessarily has a legal or cheap circuit. + +The same proof gives a limited workspace corollary: adding finitely many +independent zero-chart registers that must return their exact original values +does not help. A returned auxiliary with a monochrome final cap joins the +excluded output set; a returned auxiliary that can be mixed appends a zero +hot row to `G`. Either way the obstructed rowspace is unchanged. This does +not cover productive auxiliaries with changed final values. + +A useful next question is whether an additional productive, multicolor +output can retain the missing hot direction without consuming the full +physical saving. For example, an auxiliary final value `aux + input13` +would enlarge the hot rowspace, but this is only an algebraic escape. It +requires a complete admissible word, native interfaces, helper credits and +paid invoice; no favorable construction is supplied here. + +The Schur/preconditioning motivation was informed by Cameron, Fairbairn and +Gadouleau, *Computing in matrix groups without memory*, +[arXiv:1310.6009](https://arxiv.org/abs/1310.6009), and Dumas and Grenet, +*In-place accumulation of fast multiplication formulae*, +[arXiv:2307.12712](https://arxiv.org/abs/2307.12712). Their instruction and +cost models do not supply this chart-constrained conclusion. The color-cut +lemma and source-specific obstruction are derived above; source/package +provenance and predecessor attribution are recorded separately in this +package's source manifest. diff --git a/research/productive-helper-color-cut/README.md b/research/productive-helper-color-cut/README.md new file mode 100644 index 0000000000..4da327ddbe --- /dev/null +++ b/research/productive-helper-color-cut/README.md @@ -0,0 +1,72 @@ +# A color-cut obstruction to a productive-helper encoder + +**Scoped impossibility theorem; no improved bound.** A source-derived change of basis would let a native helper enter on `span(73)` instead of its original five-dimensional chart. The required scalar encoder passes ordinary forward and inverse support tests. Nevertheless, no ascending common-chart scalar circuit realizes this local boundary problem, even with arbitrary scalar preparation and interleaving. + +The obstruction is exact: a 15-output hot-input block has rank **7**, while its intersections with four separate input groups span only **5** dimensions. A monotone circuit would force these spaces to span the entire block. This is a proof about arbitrary circuit length and rational coefficients, not a failed search over pivots. + +## Source and boundary + +The only live input is the integrated [combined 98-instruction compression certificate](../productive-helper-fusion-certificate/README.md). Remove `climb` records and take scalar interval `[9961,10111)`, using zero-based indices. Its 150 gates act on 24 independent fields: mains 13,16,43,44,51,78,99,104 and arbitrary dirty helpers 416--431. Let the exact rational transfer be `M`. + +On output 417/419 apply `T=[[1/2,-1],[1/2,1]]`, then swap outputs 416/417 with `P`, defining `H=P T M`. The resulting output 416 is exactly `entry13+dirty_entry416`. Give it final chart `span(73)`; give 417 the old 416 exit chart and retain the other original local exits. All actual input charts are retained. No dirty input is assumed zero. + +The eight hot input lines split into four groups: + +| Input roles | Entry lines | Single-group output roles | +| --- | --- | --- | +|13,51|73,100|13,51 and protected 416| +|78,99|506,471|78,99| +|16,44|49,28|427,429| +|43,104|386,431|425,431| + +The nine listed output charts contain hot lines from only their nominated group. The remaining 15 output roles are 16,43,44,104,417,418,419,420,421,422,423,424,426,428,430. The verifier rebuilds every chart and coefficient from the source. + +## Why interleaving cannot repair it + +Color a chart by the input groups whose hot entry lines it contains. Inclusion-monotone transports can only add colors. Every scalar ADD uses a common chart on both fields. Once a gate has multiple colors, no later single-color gate can share one of its physical fields. Those scalar matrices therefore commute, allowing an **algebraic** ordering with all zero/single-color gates first and all multi-color gates last. This does not assert that the reordered physical word has the same cost. + +The nine single-color output fields never participate in the last part. On the other 15 fields the last part is an invertible matrix `R`. If `B` is the first part's hot-input block and `G` the required final block, then `G=R B`. Each row of `B` is supported within one input group. Consequently the rowspace of `G` must be generated by its intersections with the four group coordinate spaces. + +Direct exact calculation gives `rank(G)=7` and intersection dimensions `1,1,2,1`. The contradiction is already visible in its kernel relation: + +``` +2 beta13 - beta43 - beta78 - beta99 + beta104 = 0. +``` + +A row supported on group 13/51 must therefore have `beta13=0`; rows supported on any other group also have that coordinate zero. But `G` has a nonzero 13 column. [PROOF.md](PROOF.md) states all hypotheses and the complete argument. + +The obstruction also covers every invertible basis change within the complete +three-helper common-native-map class that preserves the desired output +`u=entry13+dirty_entry416`. After an invertible mixing of the other two rows, +the only remaining choices are `419 += lambda*u` and `421 += mu*u`. Their hot +block always has rank 7, while the single-group intersections span at most 6 +dimensions for every rational `lambda,mu`. This is an exact symbolic family, +not a parameter grid. [PROOF-FAMILY.md](PROOF-FAMILY.md) gives the affine kernel +certificate and precise boundary assumptions. + +The proof fixes the 24-register local boundary, pure invertible scalar ADD/SCALE operations, common canonical charts at contacts, and chart inclusion on every paid edge. The proof also survives adding independent zero-chart workspace that must be returned unchanged. It does not rule out paid nonascending steps, a changed productive output or boundary, a native-bearing region, or other productive-helper targets. No physical supplier, compiler admission, multiplication theorem or new kappa is claimed. + +## Reproduction + +From the repository root with Python 3.12 and its standard library: + +```sh +python3 -I -B research/productive-helper-color-cut/verify.py +python3 -I -O -B research/productive-helper-color-cut/verify.py +``` + +The default replay is read-only. It authenticates the source bytes, reconstructs the scalar matrix and boundary charts, verifies the exact ranks and kernel relation, and runs positive and corruption controls. The original 150-gate source has hot rank 8 and group-intersection dimensions 2,2,2,2, so it is not falsely rejected. `SOURCES.json` records provenance and `VERIFY.json` registers the isolated replay. No solver, network, Git history or discovery receipt is needed for direct replay. + +Independent agents reconstructed the source matrices, checked the normal-form proof and audited the packaged implementation. This is AI-assisted verification, not independent human or proof-kernel acceptance. + +## Open next questions + +A useful next candidate must change a hypothesis that the invariant uses. Name the changed output interface, additional productive output or interior native operation, compute its color ranks, and price its full return and cleanup costs before synthesis. Ordinary support containments alone are insufficient. See [TASK.json](TASK.json) for the concrete follow-up gate. + +This differs from PR #5361's inverse/main-support obstructions for a persistent output basis: the present color argument applies directly to `P T M` and allows arbitrary scalar preparation and interleaving. It also differs from PR #5324's theorem with fixed projection heights. + +## Attribution + +Source: Cao Yifan's PR #4610 round3 word and Cinna Davis's PR #4692 compression through flyingviper's integrated PR #5301. Retain Cinna Davis's PR #4470/controller lineage, Dugongue's frame/interface work, zxv's native/compiler work, Jacob Alan Sussman's flow work, and all predecessor credits. The linear-algebra and commutation facts are elementary; no general novelty claim is made for them. The contribution is this source-bound invariant and reproducible obstruction. + +Prepared for flyingviper with substantial OpenAI Codex assistance and independent agent checks. Apache-2.0. Frozen sources and the selected result are unchanged. diff --git a/research/productive-helper-color-cut/RESULT.json b/research/productive-helper-color-cut/RESULT.json new file mode 100644 index 0000000000..7d909f8b4f --- /dev/null +++ b/research/productive-helper-color-cut/RESULT.json @@ -0,0 +1,1297 @@ +{ + "G_rank": 7, + "G_row43_column13": "1", + "G_rows": { + "104": { + "104": "-2", + "44": "-2", + "51": "-2", + "99": "-2" + }, + "16": { + "104": "-2", + "16": "-2", + "43": "-2", + "44": "-2" + }, + "417": { + "104": "-2", + "16": "-2", + "51": "-2", + "78": "-2" + }, + "418": { + "13": "1", + "16": "1", + "43": "1", + "78": "1" + }, + "419": { + "51": "1" + }, + "420": { + "13": "1", + "43": "1", + "44": "1", + "99": "1" + }, + "421": { + "104": "1", + "43": "1" + }, + "422": { + "104": "1", + "16": "1", + "51": "1", + "78": "1" + }, + "423": { + "104": "1", + "44": "1", + "51": "1", + "99": "1" + }, + "424": { + "16": "1/2", + "43": "1/2", + "51": "-1/2", + "99": "-1/2" + }, + "426": { + "16": "-1/2", + "44": "1/2" + }, + "428": { + "43": "1/2", + "44": "1/2", + "51": "-1/2", + "78": "-1/2" + }, + "43": { + "104": "1", + "13": "1", + "16": "1", + "43": "1", + "44": "1", + "51": "1", + "78": "1", + "99": "1" + }, + "430": { + "104": "1/2", + "13": "-1/2", + "16": "1/2", + "99": "-1/2" + }, + "44": { + "104": "1/2", + "13": "-1/2", + "44": "1/2", + "78": "-1/2" + } + }, + "G_sha256": "93608f9163d073b9c369c9389db525b021ce6eb19c80342c8879f93857eb731e", + "H_sha256": "5277af6c46e002020a6dcf5792417dca93cdda6a3bc3ea7e7adb4232f3793290", + "M_sha256": "4a5ba0c3685e5ee1fad1a155232273add26bdceacbd97311fdf66ca0274144a7", + "all_forward_and_inverse_support_containments": true, + "allowed_capture_preimage_span_rank": 13, + "arbitrary_cold_inputs": [ + 416, + 417, + 418, + 419, + 420, + 421, + 422, + 423, + 424, + 425, + 426, + 427, + 428, + 429, + 430, + 431 + ], + "both_M_and_H_inverse_products": true, + "climb_stripped_scalar_interval": [ + 9961, + 10111 + ], + "common_annihilators": [ + { + "104": "4", + "417": "4", + "422": "-2", + "423": "-2", + "424": "1", + "428": "1", + "43": "-2" + }, + { + "418": "-2", + "420": "-2", + "43": "-2", + "430": "1", + "44": "1" + } + ], + "common_native_basis_family": { + "both_changed_rows_removed_rank": 5, + "changed_dirty_outputs": [ + 419, + 421 + ], + "corruption_controls": [ + "changed_shear_row_coefficient", + "lost_unaffected_column_rank", + "wrong_role_binding" + ], + "covers_invertible_complement_mixing": true, + "hot_columns": [ + 13, + 16, + 43, + 44, + 51, + 78, + 99, + 104 + ], + "kernel_constant": [ + "2", + "0", + "-1", + "0", + "0", + "-1", + "-1", + "1" + ], + "kernel_lambda": [ + "0", + "0", + "-1", + "0", + "-2", + "1", + "1", + "1" + ], + "kernel_mu": [ + "0", + "1", + "-1", + "1", + "0", + "0", + "0", + "-1" + ], + "maximum_single_color_span_dimension": 6, + "new_kappa": false, + "pair_dimension_formula": "4 + [lambda=1] + [mu=0] + [lambda=-1 and mu=0]", + "rank_for_every_parameter": 7, + "status": "RULED_OUT_FOR_ALL_RATIONAL_LAMBDA_MU", + "symbolic_coefficients_checked_per_row": [ + "1", + "lambda", + "mu", + "lambda^2", + "lambda*mu", + "mu^2" + ], + "unaffected_seven_columns_rank": 7 + }, + "complete_equal_native_map_class": { + "lenders": [ + 417, + 419, + 421 + ], + "operators": [ + 34, + 35, + 36 + ] + }, + "corruption_and_scope_controls": { + "changed_source_bytes_rejected": true, + "changed_target_coefficient_rejected": true, + "cross_color_clean_cap_rejected": true, + "one_cross_pair_relaxation_rank": 14, + "two_cross_pair_relaxations_rank": 15, + "wrong_relation_sign_rejected": true + }, + "entry_chart_bases": { + "104": [ + 431 + ], + "13": [ + 73 + ], + "16": [ + 49 + ], + "416": [], + "417": [], + "418": [], + "419": [], + "420": [], + "421": [], + "422": [], + "423": [], + "424": [], + "425": [], + "426": [], + "427": [], + "428": [], + "429": [], + "43": [ + 386 + ], + "430": [], + "431": [], + "44": [ + 28 + ], + "51": [ + 100 + ], + "78": [ + 506 + ], + "99": [ + 471 + ] + }, + "fixed_exit_chart_bases": { + "104": [ + 28, + 45, + 73, + 130, + 256 + ], + "13": [ + 45, + 73 + ], + "16": [ + 28, + 45, + 73, + 130, + 256 + ], + "416": [ + 73 + ], + "417": [ + 28, + 45, + 73, + 130, + 256 + ], + "418": [ + 49, + 73, + 386 + ], + "419": [ + 28, + 45, + 73, + 130, + 256 + ], + "420": [ + 28, + 73, + 386 + ], + "421": [ + 28, + 45, + 73, + 130, + 256 + ], + "422": [ + 49, + 85, + 414 + ], + "423": [ + 28, + 100, + 431 + ], + "424": [ + 49, + 85, + 386 + ], + "425": [ + 45, + 386 + ], + "426": [ + 28, + 45, + 73, + 130, + 256 + ], + "427": [ + 28, + 45 + ], + "428": [ + 28, + 100, + 386 + ], + "429": [ + 28, + 45 + ], + "43": [ + 28, + 45, + 73, + 130, + 256 + ], + "430": [ + 49, + 73, + 414 + ], + "431": [ + 45, + 386 + ], + "44": [ + 28, + 73, + 431 + ], + "51": [ + 45, + 73 + ], + "78": [ + 45, + 471 + ], + "99": [ + 45, + 471 + ] + }, + "hot_inputs": [ + 13, + 16, + 43, + 44, + 51, + 78, + 99, + 104 + ], + "local_roles": [ + 13, + 16, + 43, + 44, + 51, + 78, + 99, + 104, + 416, + 417, + 418, + 419, + 420, + 421, + 422, + 423, + 424, + 425, + 426, + 427, + 428, + 429, + 430, + 431 + ], + "masks": [ + { + "complete_nullspace_basis_w": [ + { + "104": "1", + "16": "1", + "43": "2", + "44": "4" + }, + { + "16": "1/2", + "418": "1", + "44": "2" + }, + { + "417": "-1/2", + "420": "1", + "43": "-1" + }, + { + "417": "1/2", + "422": "1" + }, + { + "16": "-1/2", + "423": "1", + "43": "-1", + "44": "-2" + }, + { + "16": "1/2", + "424": "1", + "43": "1/2", + "44": "1" + }, + { + "16": "1/4", + "417": "-1/4", + "428": "1" + }, + { + "16": "1/4", + "417": "1/4", + "43": "1/2", + "430": "1" + } + ], + "hot_support_mask": [], + "nullspace_dimension": 8 + }, + { + "complete_nullspace_basis_w": [ + { + "104": "1", + "16": "1", + "43": "2", + "44": "4" + }, + { + "16": "1/2", + "418": "1", + "44": "2" + }, + { + "417": "-1/2", + "420": "1", + "43": "-1" + }, + { + "417": "1/2", + "422": "1" + }, + { + "16": "-1/2", + "423": "1", + "43": "-1", + "44": "-2" + }, + { + "16": "1/2", + "424": "1", + "43": "1/2", + "44": "1" + }, + { + "16": "1/4", + "417": "-1/4", + "428": "1" + }, + { + "16": "1/4", + "417": "1/4", + "43": "1/2", + "430": "1" + } + ], + "hot_support_mask": [ + 13 + ], + "nullspace_dimension": 8 + }, + { + "complete_nullspace_basis_w": [ + { + "104": "1", + "16": "1", + "43": "2", + "44": "4" + }, + { + "16": "1/2", + "418": "1", + "44": "2" + }, + { + "417": "-1/2", + "420": "1", + "43": "-1" + }, + { + "417": "1/2", + "422": "1" + }, + { + "16": "-1/2", + "423": "1", + "43": "-1", + "44": "-2" + }, + { + "16": "1/2", + "424": "1", + "43": "1/2", + "44": "1" + }, + { + "16": "1/4", + "421": "1/2", + "426": "1" + }, + { + "16": "1/4", + "417": "-1/4", + "428": "1" + }, + { + "16": "1/4", + "417": "1/4", + "43": "1/2", + "430": "1" + } + ], + "hot_support_mask": [ + 16 + ], + "nullspace_dimension": 9 + }, + { + "complete_nullspace_basis_w": [ + { + "104": "1", + "16": "1", + "43": "2", + "44": "4" + }, + { + "16": "1/2", + "418": "1", + "44": "2" + }, + { + "417": "-1/2", + "420": "1", + "43": "-1" + }, + { + "417": "1/2", + "422": "1" + }, + { + "16": "-1/2", + "423": "1", + "43": "-1", + "44": "-2" + }, + { + "16": "1/2", + "424": "1", + "43": "1/2", + "44": "1" + }, + { + "16": "1/4", + "417": "-1/4", + "428": "1" + }, + { + "16": "1/4", + "417": "1/4", + "43": "1/2", + "430": "1" + } + ], + "hot_support_mask": [ + 43 + ], + "nullspace_dimension": 8 + }, + { + "complete_nullspace_basis_w": [ + { + "104": "1", + "16": "1", + "43": "2", + "44": "4" + }, + { + "16": "1/2", + "418": "1", + "44": "2" + }, + { + "417": "-1/2", + "420": "1", + "43": "-1" + }, + { + "417": "1/2", + "422": "1" + }, + { + "16": "-1/2", + "423": "1", + "43": "-1", + "44": "-2" + }, + { + "16": "1/2", + "424": "1", + "43": "1/2", + "44": "1" + }, + { + "16": "-1/4", + "421": "-1/2", + "426": "1" + }, + { + "16": "1/4", + "417": "-1/4", + "428": "1" + }, + { + "16": "1/4", + "417": "1/4", + "43": "1/2", + "430": "1" + } + ], + "hot_support_mask": [ + 44 + ], + "nullspace_dimension": 9 + }, + { + "complete_nullspace_basis_w": [ + { + "104": "1", + "16": "1", + "43": "2", + "44": "4" + }, + { + "16": "1/2", + "418": "1", + "44": "2" + }, + { + "419": "1" + }, + { + "417": "-1/2", + "420": "1", + "43": "-1" + }, + { + "417": "1/2", + "422": "1" + }, + { + "16": "-1/2", + "423": "1", + "43": "-1", + "44": "-2" + }, + { + "16": "1/2", + "424": "1", + "43": "1/2", + "44": "1" + }, + { + "16": "1/4", + "417": "-1/4", + "428": "1" + }, + { + "16": "1/4", + "417": "1/4", + "43": "1/2", + "430": "1" + } + ], + "hot_support_mask": [ + 51 + ], + "nullspace_dimension": 9 + }, + { + "complete_nullspace_basis_w": [ + { + "104": "1", + "16": "1", + "43": "2", + "44": "4" + }, + { + "16": "1/2", + "418": "1", + "44": "2" + }, + { + "417": "-1/2", + "420": "1", + "43": "-1" + }, + { + "417": "1/2", + "422": "1" + }, + { + "16": "-1/2", + "423": "1", + "43": "-1", + "44": "-2" + }, + { + "16": "1/2", + "424": "1", + "43": "1/2", + "44": "1" + }, + { + "16": "1/4", + "417": "-1/4", + "428": "1" + }, + { + "16": "1/4", + "417": "1/4", + "43": "1/2", + "430": "1" + } + ], + "hot_support_mask": [ + 78 + ], + "nullspace_dimension": 8 + }, + { + "complete_nullspace_basis_w": [ + { + "104": "1", + "16": "1", + "43": "2", + "44": "4" + }, + { + "16": "1/2", + "418": "1", + "44": "2" + }, + { + "417": "-1/2", + "420": "1", + "43": "-1" + }, + { + "417": "1/2", + "422": "1" + }, + { + "16": "-1/2", + "423": "1", + "43": "-1", + "44": "-2" + }, + { + "16": "1/2", + "424": "1", + "43": "1/2", + "44": "1" + }, + { + "16": "1/4", + "417": "-1/4", + "428": "1" + }, + { + "16": "1/4", + "417": "1/4", + "43": "1/2", + "430": "1" + } + ], + "hot_support_mask": [ + 99 + ], + "nullspace_dimension": 8 + }, + { + "complete_nullspace_basis_w": [ + { + "104": "1", + "16": "1", + "43": "2", + "44": "4" + }, + { + "16": "1/2", + "418": "1", + "44": "2" + }, + { + "417": "-1/2", + "420": "1", + "43": "-1" + }, + { + "417": "1/2", + "422": "1" + }, + { + "16": "-1/2", + "423": "1", + "43": "-1", + "44": "-2" + }, + { + "16": "1/2", + "424": "1", + "43": "1/2", + "44": "1" + }, + { + "16": "1/4", + "417": "-1/4", + "428": "1" + }, + { + "16": "1/4", + "417": "1/4", + "43": "1/2", + "430": "1" + } + ], + "hot_support_mask": [ + 104 + ], + "nullspace_dimension": 8 + }, + { + "complete_nullspace_basis_w": [ + { + "104": "1", + "16": "1", + "43": "2", + "44": "4" + }, + { + "16": "1/2", + "418": "1", + "44": "2" + }, + { + "419": "1" + }, + { + "417": "-1/2", + "420": "1", + "43": "-1" + }, + { + "417": "1/2", + "422": "1" + }, + { + "16": "-1/2", + "423": "1", + "43": "-1", + "44": "-2" + }, + { + "16": "1/2", + "424": "1", + "43": "1/2", + "44": "1" + }, + { + "16": "1/4", + "417": "-1/4", + "428": "1" + }, + { + "16": "1/4", + "417": "1/4", + "43": "1/2", + "430": "1" + } + ], + "hot_support_mask": [ + 13, + 51 + ], + "nullspace_dimension": 9 + }, + { + "complete_nullspace_basis_w": [ + { + "104": "1", + "16": "1", + "43": "2", + "44": "4" + }, + { + "16": "1/2", + "418": "1", + "44": "2" + }, + { + "417": "-1/2", + "420": "1", + "43": "-1" + }, + { + "417": "1/2", + "422": "1" + }, + { + "16": "-1/2", + "423": "1", + "43": "-1", + "44": "-2" + }, + { + "16": "1/2", + "424": "1", + "43": "1/2", + "44": "1" + }, + { + "16": "-1/4", + "417": "-1/4", + "426": "1", + "43": "-1/2", + "44": "-1" + }, + { + "16": "1/4", + "417": "-1/4", + "428": "1" + }, + { + "16": "1/4", + "417": "1/4", + "43": "1/2", + "430": "1" + } + ], + "hot_support_mask": [ + 78, + 99 + ], + "nullspace_dimension": 9 + }, + { + "complete_nullspace_basis_w": [ + { + "104": "1", + "16": "1", + "43": "2", + "44": "4" + }, + { + "16": "1/2", + "418": "1", + "44": "2" + }, + { + "417": "-1/2", + "420": "1", + "43": "-1" + }, + { + "16": "1/2", + "421": "1" + }, + { + "417": "1/2", + "422": "1" + }, + { + "16": "-1/2", + "423": "1", + "43": "-1", + "44": "-2" + }, + { + "16": "1/2", + "424": "1", + "43": "1/2", + "44": "1" + }, + { + "426": "1" + }, + { + "16": "1/4", + "417": "-1/4", + "428": "1" + }, + { + "16": "1/4", + "417": "1/4", + "43": "1/2", + "430": "1" + } + ], + "hot_support_mask": [ + 16, + 44 + ], + "nullspace_dimension": 10 + }, + { + "complete_nullspace_basis_w": [ + { + "104": "1", + "16": "1", + "43": "2", + "44": "4" + }, + { + "16": "1/2", + "418": "1", + "44": "2" + }, + { + "417": "-1/2", + "420": "1", + "43": "-1" + }, + { + "421": "1" + }, + { + "417": "1/2", + "422": "1" + }, + { + "16": "-1/2", + "423": "1", + "43": "-1", + "44": "-2" + }, + { + "16": "1/2", + "424": "1", + "43": "1/2", + "44": "1" + }, + { + "16": "1/4", + "417": "-1/4", + "428": "1" + }, + { + "16": "1/4", + "417": "1/4", + "43": "1/2", + "430": "1" + } + ], + "hot_support_mask": [ + 43, + 104 + ], + "nullspace_dimension": 9 + } + ], + "monochrome_output_colors": { + "13": [ + 0 + ], + "416": [ + 0 + ], + "425": [ + 3 + ], + "427": [ + 2 + ], + "429": [ + 2 + ], + "431": [ + 3 + ], + "51": [ + 0 + ], + "78": [ + 1 + ], + "99": [ + 1 + ] + }, + "monochrome_outputs": [ + 13, + 51, + 78, + 99, + 427, + 429, + 425, + 431, + 416 + ], + "native34_35_equal_source_maps": true, + "original_source_positive_control": { + "dirty_hot_rank": 8, + "dirty_output_count": 16, + "disjoint_commuting_inversions": 72, + "full24_matrix_identity": true, + "mixed_gates": 110, + "mono_gates": 40, + "pair_intersection_dimensions": [ + 2, + 2, + 2, + 2 + ], + "status": "PASS" + }, + "pair_supported_rowspace_dimensions": [ + 1, + 1, + 2, + 1 + ], + "pair_supported_rowspace_span_dimension": 5, + "protected_output_row": { + "13": "1", + "416": "1" + }, + "remaining_outputs": [ + 16, + 43, + 44, + 104, + 417, + 418, + 419, + 420, + 421, + 422, + 423, + 424, + 426, + 428, + 430 + ], + "scope": "No ascending canonical-chart ADD/SCALE circuit on these24 registers realizes H=P*T*M from the source entry charts to the fixed exit charts. Arbitrary rational coefficients and arbitrary intermediate charts/interleavings are allowed. No preparation prefix is assumed. No new registers or native maps inside the scalar interval; enlarged boundaries, nonascending transports and different target words are not excluded. No tariff or improved-bound claim.", + "source_bytes_sha256": "6caa29e474375298847fac8a53508f65037dc45e64d2ea0125ece9faf32b2ce4", + "source_entry_frames": { + "104": 106, + "13": 15, + "16": 18, + "416": 0, + "417": 0, + "418": 0, + "419": 0, + "420": 0, + "421": 0, + "422": 0, + "423": 0, + "424": 0, + "425": 0, + "426": 0, + "427": 0, + "428": 0, + "429": 0, + "43": 45, + "430": 0, + "431": 0, + "44": 46, + "51": 53, + "78": 80, + "99": 101 + }, + "source_exit_frames": { + "104": 1922, + "13": 581, + "16": 1922, + "416": 1922, + "417": 1922, + "418": 592, + "419": 1922, + "420": 594, + "421": 1922, + "422": 593, + "423": 591, + "424": 595, + "425": 580, + "426": 1922, + "427": 579, + "428": 597, + "429": 579, + "43": 1922, + "430": 598, + "431": 580, + "44": 596, + "51": 581, + "78": 584, + "99": 584 + }, + "source_hot_pairs": [ + [ + 13, + 51 + ], + [ + 78, + 99 + ], + [ + 16, + 44 + ], + [ + 43, + 104 + ] + ], + "source_json_sha256": "aa4a8241da76abd2c06e6576a3ac09e77781321deaac3ad7d3ce4519342a36e6", + "source_orientation": "forward", + "source_segment_sha256": "b3768b4abab33eb0e2b69dc27a421a46b4a2c92e336812b715f6f74c36778441", + "status": "PASS_DIRECT_ENCODER_ASCENDING_OBSTRUCTION", + "unique_G_column_relation": { + "104": "1", + "13": "2", + "43": "-1", + "78": "-1", + "99": "-1" + } +} diff --git a/research/productive-helper-color-cut/SOURCES.json b/research/productive-helper-color-cut/SOURCES.json new file mode 100644 index 0000000000..0aeff761b2 --- /dev/null +++ b/research/productive-helper-color-cut/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "7c472563474e60185e6ca101a17622133d047e56", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/productive-helper-fusion-certificate/COMBINED-WORD.json.gz", + "usage": "input", + "git_blob": "2e14a77f0c4be08b1a9d7acf33525ecfd3a8e3ed", + "sha256": "6caa29e474375298847fac8a53508f65037dc45e64d2ea0125ece9faf32b2ce4" + }, + { + "path": "research/productive-helper-fusion-certificate/check_rewrite.py", + "usage": "provenance", + "git_blob": "31eae7986125f97cf88c1cfc2e2ee6c64ecf6c19", + "sha256": "797d074c0b78dc2f2b02fa1bfcfe3b180b56c3a8236ce2764b4ade20ecb6aa93" + }, + { + "path": "research/scalar-trace-compression/verify.py", + "usage": "provenance", + "git_blob": "59d292131bef552c2823bf068a70bd095f90f680", + "sha256": "b41d69aca44852b4b7b880b74b3b482c2274f7b093573ca663a8f5419c8858be" + } + ] +} diff --git a/research/productive-helper-color-cut/TASK.json b/research/productive-helper-color-cut/TASK.json new file mode 100644 index 0000000000..8a4218830b --- /dev/null +++ b/research/productive-helper-color-cut/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 7, + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "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.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "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": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "base_commit": "7c472563474e60185e6ca101a17622133d047e56", + "scope_status": "changed", + "actual_scope": "Exact no-return color-cut obstruction for a source-derived productive-helper scalar map and every invertible basis change within its complete three-channel common-native-map class that fixes the protected value, with independent rank and physical-interface checks.", + "scope_change_reason": "Explicit productive-helper/native co-optimization found a candidate that passed forward and inverse support gates. A scalar normal form exposes an obstruction beyond those necessary tests.", + "bottleneck_link": "Lowering one native input chart is useful only if a scalar encoder realizes all arbitrary dirty inputs at the retained interfaces. The color-cut invariant can reject entire circuit families before synthesis.", + "budget_minutes": 90, + "stop_rule": "Stop synthesis for a candidate covered by the verified color-cut obstruction. Further work must change a stated boundary, scalar-region, register or operation hypothesis and pass a full optimistic invoice. User cutoff is 30 percent usage remaining.", + "outcome": "completed", + "evidence": "PROOF.md, PROOF-FAMILY.md and exact source-derived rank certificates in verify.py; symbolic polynomial identity for every rational pair of shear parameters and invertible complement mixing; seven corruption controls and two scope controls; independent agent algebra, matrix, chronology and package audits.", + "author": "flyingviper, with substantial OpenAI Codex assistance and independent agents", + "ai_assistance": "Three independent agents derived and checked matrix/inverse identities, graph caps and package semantics. This is AI-assisted evidence, not independent human or proof-kernel acceptance.", + "open_questions": [ + { + "question": "Can a changed boundary or an enlarged native-bearing region evade the color-cut obstruction at a favorable complete price?", + "why_it_matters": "The proof relies on pure scalar operations, fixed available registers and final charts that keep the nominated output fields inside one input group.", + "first_step": "Name the boundary or operation that invalidates the normal form, derive all changed paid costs and credits, and recompute the color ranks before synthesis.", + "blocked_by": "Exact arbitrary-input endpoints in both orientations, native admission, and a full paid-minus-helper invoice; passing a relaxed support gate is insufficient." + } + ], + "coordination": { + "upstream_checkpoint": "7c472563474e60185e6ca101a17622133d047e56", + "priority_and_selected_changed": false, + "predecessors": "PR5301 and PR5324 supply the integrated source and prior fixed-height theorem. PR5361 certifies support obstructions for a different persistent-basis suffix. This package tests the source-consuming candidate via a new scalar color-cut invariant.", + "coverage": "Current canonical main and relevant integrated source packages; recent PR/discussion overlap refresh recorded before submission. Not an exhaustive novelty proof.", + "final_overlap": { + "checked_utc": "2026-10-23T20:04:12Z", + "most_recently_updated_prs": 100, + "local_search": "Canonical main7c4725634 README/PROOF/TASK texts; no-return, monochrome, capture-rank and related terms.", + "finding": "No exact duplicate of the source-derived rank7 versus5 color-cut obstruction found. Recent public coverage is limited and does not establish novelty." + } + } +} diff --git a/research/productive-helper-color-cut/VERIFY.json b/research/productive-helper-color-cut/VERIFY.json new file mode 100644 index 0000000000..0a31c3163a --- /dev/null +++ b/research/productive-helper-color-cut/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/productive-helper-fusion-certificate/COMBINED-WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact source authentication, source-derived scalar map, complete common-native-map class, no-return color partitions, rational rank/intersection certificates, symbolic two-parameter family, original-source positive control, seven corruption controls and two scope controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact source authentication, source-derived scalar map, complete common-native-map class, no-return color partitions, rational rank/intersection certificates, symbolic two-parameter family, original-source positive control, seven corruption controls and two scope controls." + } + ] +} diff --git a/research/productive-helper-color-cut/check.py b/research/productive-helper-color-cut/check.py new file mode 100644 index 0000000000..e97e94596a --- /dev/null +++ b/research/productive-helper-color-cut/check.py @@ -0,0 +1,380 @@ +#!/usr/bin/env python3 +"""Exact source-bound color-cut obstruction to an ascending scalar encoder. + +Standard library only: reconstructs the full 24-input transfer and boundary +charts from the pinned word, without solver output or generated matrix inputs. +The general normal-form argument is in PROOF.md; this checks its source data. +""" +from __future__ import annotations + +import argparse +from fractions import Fraction as Q +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path + +SOURCE_BYTES_SHA256 = "6caa29e474375298847fac8a53508f65037dc45e64d2ea0125ece9faf32b2ce4" +SOURCE_JSON_SHA256 = "aa4a8241da76abd2c06e6576a3ac09e77781321deaac3ad7d3ce4519342a36e6" +LO, HI = 9961, 10111 +HOT = [13, 16, 43, 44, 51, 78, 99, 104] +LOCAL = HOT + list(range(416, 432)) +CLEAN = [13, 51, 78, 99, 427, 429, 425, 431, 416] +DIRTY = [r for r in LOCAL if r not in CLEAN] +PAIRS = [(13, 51), (78, 99), (16, 44), (43, 104)] +MASKS = [()] + [(r,) for r in HOT] + PAIRS +NORMAL = [Q(x) for x in (2, 0, -1, 0, 0, -1, -1, 1)] +IX = {r: i for i, r in enumerate(LOCAL)} + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def digest(value): + return hashlib.sha256(json.dumps(value, sort_keys=True, separators=(",", ":")).encode()).hexdigest() + + +def eye(n): + return [[Q(i == j) for j in range(n)] for i in range(n)] + + +def mm(a, b): + return [[sum(x * b[k][j] for k, x in enumerate(row) if x) + for j in range(len(b[0]))] for row in a] + + +def rref(rows, width): + rows = [[Q(x) for x in row] for row in rows if any(row)] + pivots = [] + for column in range(width): + k = len(pivots) + pivot = next((i for i in range(k, len(rows)) if rows[i][column]), None) + if pivot is None: + continue + rows[k], rows[pivot] = rows[pivot], rows[k] + value = rows[k][column] + rows[k] = [x / value for x in rows[k]] + for i in range(len(rows)): + if i != k and rows[i][column]: + value = rows[i][column] + rows[i] = [x - value * y for x, y in zip(rows[i], rows[k])] + pivots.append(column) + if len(pivots) == len(rows): + break + return rows[:len(pivots)], pivots + + +def rank(rows, width): + return len(rref(rows, width)[1]) + + +def nullspace(rows, width): + reduced, pivots = rref(rows, width) + basis = [] + for c in range(width): + if c in pivots: + continue + v = [Q(0)] * width + v[c] = Q(1) + for row, p in zip(reduced, pivots): + v[p] = -row[c] + need(all(sum(x * y for x, y in zip(row, v)) == 0 for row in rows), "nullspace equation") + basis.append(v) + need(len(basis) + len(pivots) == width, "nullspace dimension") + return basis + + +def inverse(matrix): + n = len(matrix) + reduced, pivots = rref([row[:] + unit for row, unit in zip(matrix, eye(n))], 2 * n) + need(pivots == list(range(n)), "matrix singular") + answer = [row[n:] for row in reduced] + need(mm(matrix, answer) == eye(n) and mm(answer, matrix) == eye(n), "both inverse products") + return answer + + +def sparse(row, labels): + return {str(label): str(x) for label, x in zip(labels, row) if x} + + +def matrix_hash(matrix, rows, columns): + return digest({"rows": rows, "columns": columns, "coefficients": [[str(x) for x in row] for row in matrix]}) + + +def span(vectors): + result = {0} + for v in vectors: + result |= {x ^ v for x in tuple(result)} + return frozenset(result) + + +def basis(space): + rows, seen = [], {0} + for v in sorted(space): + if v not in seen: + rows.append(v) + seen |= {x ^ v for x in tuple(seen)} + return rows + + +def refs(event): + gate = event[1] + return gate[1:3] if gate[0] == "add" else gate[1:2] + + +def scalar_matrix(events): + matrix = eye(len(LOCAL)) + for event in events: + need(event[0] == "scalar", "local interval must be scalar") + gate = event[1] + need(gate[0] in ("add", "scale"), "unrecognized or noninvertible gate") + need(all(kind == "L" and r in IX for kind, r in refs(event)), "local role binding") + target = IX[gate[1][1]] + if gate[0] == "add": + source, coefficient = IX[gate[2][1]], Q(*gate[3:5]) + need(source != target, "self-add excluded") + matrix[target] = [x + coefficient * y for x, y in zip(matrix[target], matrix[source])] + else: + coefficient = Q(*gate[2:4]) + need(coefficient != 0, "singular scale") + matrix[target] = [coefficient * x for x in matrix[target]] + return matrix + + +def load_source(data): + need(hashlib.sha256(data).hexdigest() == SOURCE_BYTES_SHA256, "compressed source byte hash") + word = json.loads(gzip.decompress(data)) + need(digest(word) == SOURCE_JSON_SHA256, "canonical source JSON hash") + return word + + +def reconstruct(word): + program = [event for event in word["programs"]["forward"] if event[0] != "climb"] + need(len(program) == 18061, "source event census") + segment = program[LO:HI] + need(sorted({r for e in segment for _, r in refs(e)}) == LOCAL, "local role census") + M = scalar_matrix(segment) + inverse(M) + # T: 419 += 417/2; 417 -= 419. P swaps output416 and417. + H = [row[:] for row in M] + H[IX[419]] = [x + y / 2 for x, y in zip(H[IX[419]], H[IX[417]])] + H[IX[417]] = [x - y for x, y in zip(H[IX[417]], H[IX[419]])] + H[IX[416]], H[IX[417]] = H[IX[417]], H[IX[416]] + need(H[IX[416]] == [Q(r in (13, 416)) for r in LOCAL], "protected output row") + inverse(H) + maps = {x["op"]: x for x in word["canonical"]["warps"]} + need(maps[34]["lender"] == 417 and maps[35]["lender"] == 419, "native role binding") + need(maps[34]["G_columns"] == maps[35]["G_columns"], "equal native maps34/35 motivation") + need(maps[36]["lender"] == 421, "third native role binding") + need(sorted(op for op, row in maps.items() + if row["G_columns"] == maps[34]["G_columns"]) == [34, 35, 36], + "complete common native-map class") + return M, H, program, segment + + +def source_boundaries(word, program): + canonical = word["canonical"] + need(canonical["h"] == 9 and len(canonical["start"]) == 632, "source dimension/register census") + frames = list(map(span, canonical["frames"])) + current = canonical["start"][:] + for ordinal, event in enumerate(program[:HI]): + if ordinal == LO: + entry_labels = {r: current[r] for r in LOCAL} + if event[0] == "scalar": + for kind, role in refs(event): + if kind == "L": + current[role] = event[2] + elif event[0] == "warp": + current[event[1][1]] = event[4] + elif event[0] == "adapter": + need(current[event[2]] == event[3], "adapter preserves current canonical chart") + else: + need(event[0] == "phase", "unexpected chart-changing prefix instruction") + source_exits = {r: current[r] for r in LOCAL} + entries = {r: frames[entry_labels[r]] for r in LOCAL} + need(all(len(entries[r]) == 2 for r in HOT), "eight hot entry lines") + need(all(entries[r] == frozenset({0}) for r in LOCAL if r not in HOT), "sixteen arbitrary cold entries") + expected_lines = {13: 73, 16: 49, 43: 386, 44: 28, 51: 100, 78: 506, 99: 471, 104: 431} + need(all(entries[r] == span([v]) for r, v in expected_lines.items()), "source input line binding") + fixed_exits = {r: frames[source_exits[r]] for r in LOCAL} + fixed_exits[417] = frames[source_exits[416]] + fixed_exits[416] = entries[13] + need(all(entries[r] <= fixed_exits[r] for r in LOCAL), "physical entry contained in fixed exit") + return frames, entries, fixed_exits, entry_labels, source_exits + + +def colors(chart, entries): + return [i for i, pair in enumerate(PAIRS) if any(entries[r] <= chart for r in pair)] + + +def check_clean_caps(exits, entries): + expected = {13: 0, 51: 0, 78: 1, 99: 1, 427: 2, 429: 2, 425: 3, 431: 3, 416: 0} + answer = {str(r): colors(exits[r], entries) for r in CLEAN} + need(all(answer[str(r)] == [color] for r, color in expected.items()), "nine fixed output caps are monochrome") + return answer + + +def pair_dimensions(G): + total = rank(G, len(HOT)) + return [total - rank([[row[k] for k, r in enumerate(HOT) if r not in pair] for row in G], 6) + for pair in PAIRS] + + +def analyze(H): + G = [[H[IX[r]][IX[s]] for s in HOT] for r in DIRTY] + need(rank(G, 8) == 7, "dirty-hot block rank7") + need(nullspace(G, 8) == [NORMAL], "unique coupled hot-column relation") + need(H[IX[43]][IX[13]] == 1, "nonzero hot13 coefficient") + parts = pair_dimensions(G) + need(parts == [1, 1, 2, 1], "one-pair rowspace dimensions") + masks, all_rows = [], [] + for mask in MASKS: + outside = [k for k, r in enumerate(HOT) if r not in mask] + equations = [[G[j][k] for j in range(len(DIRTY))] for k in outside] + vectors = nullspace(equations, len(DIRTY)) + all_rows.extend(vectors) + masks.append({"hot_support_mask": list(mask), "nullspace_dimension": len(vectors), + "complete_nullspace_basis_w": [sparse(v, DIRTY) for v in vectors]}) + need(rank(all_rows, 15) == 13, "allowed capture preimage span rank13") + annihilators = nullspace(all_rows, 15) + need(len(annihilators) == 2, "two independent common annihilators") + return G, parts, masks, annihilators + + +def source_positive_control(M, segment, frames, entries, source_exits): + current = dict(entries) + mono, mixed, classified = [], [], [] + for event in segment: + touched = {r for _, r in refs(event)} + chart = frames[event[2]] + need(all(current[r] <= chart for r in touched), "original scalar source is ascending") + multi = len(colors(chart, entries)) >= 2 + (mixed if multi else mono).append(event) + classified.append((multi, touched)) + for r in touched: + current[r] = chart + inversions = 0 + for i, (multi, touched) in enumerate(classified): + if multi: + for later_multi, later_touched in classified[i + 1:]: + if not later_multi: + need(touched.isdisjoint(later_touched), "out-of-order source gates must commute") + inversions += 1 + J, L = scalar_matrix(mono), scalar_matrix(mixed) + need(mm(L, J) == M, "source full24 normal-form matrix identity") + source_clean = [r for r in CLEAN if r != 416] + source_dirty = [r for r in LOCAL if r not in source_clean] + need(all(len(colors(frames[source_exits[r]], entries)) == 1 for r in source_clean), "source clean caps") + need(all(r not in source_clean for event in mixed for _, r in refs(event)), "source mixed suffix excludes clean outputs") + for r in source_dirty: + support = [s for s in HOT if J[IX[r]][IX[s]]] + need(any(set(support) <= set(pair) for pair in PAIRS), "source prefix hot support is one-pair") + G0 = [[M[IX[r]][IX[s]] for s in HOT] for r in source_dirty] + need(rank(G0, 8) == 8 and pair_dimensions(G0) == [2, 2, 2, 2], "original source passes rowspace test") + need((len(mono), len(mixed), inversions) == (40, 110, 72), "source normal-form census") + return {"status": "PASS", "mono_gates": len(mono), "mixed_gates": len(mixed), + "disjoint_commuting_inversions": inversions, "full24_matrix_identity": True, + "dirty_output_count": 16, "dirty_hot_rank": 8, "pair_intersection_dimensions": [2, 2, 2, 2]} + + +def rejected(action): + try: + action() + except (ValueError, KeyError, IndexError, ZeroDivisionError): + return True + return False + + +def corruption_controls(raw, H, G, exits, entries): + controls = {"changed_source_bytes_rejected": rejected(lambda: load_source(raw + b" "))} + wrong = [row[:] for row in H] + wrong[IX[43]][IX[13]] += 1 + controls["changed_target_coefficient_rejected"] = rejected(lambda: analyze(wrong)) + bad_normal = NORMAL[:] + bad_normal[0] *= -1 + controls["wrong_relation_sign_rejected"] = bool(any(sum(x * y for x, y in zip(row, bad_normal)) for row in G)) + bad_caps = dict(exits) + bad_caps[13] = span(exits[13] | entries[78]) + controls["cross_color_clean_cap_rejected"] = rejected(lambda: check_clean_caps(bad_caps, entries)) + need(all(controls.values()), "a corruption control was accepted") + def union_rank(masks): + vectors = [] + for mask in masks: + equations = [[G[j][k] for j in range(15)] for k, r in enumerate(HOT) if r not in mask] + vectors.extend(nullspace(equations, 15)) + return rank(vectors, 15) + controls["one_cross_pair_relaxation_rank"] = union_rank(MASKS + [(13, 43)]) + controls["two_cross_pair_relaxations_rank"] = union_rank(MASKS + [(13, 43), (13, 78)]) + need(controls["one_cross_pair_relaxation_rank"] == 14, "one cross-pair scope control") + need(controls["two_cross_pair_relaxations_rank"] == 15, "two cross-pair scope controls") + return controls + + +def run(source_path=None, *, controls=True): + path = (Path(source_path) if source_path is not None else + Path(__file__).resolve().parent.parent / "productive-helper-fusion-certificate" / "COMBINED-WORD.json.gz") + raw = path.read_bytes() + word = load_source(raw) + M, H, program, segment = reconstruct(word) + frames, entries, exits, entry_labels, source_exits = source_boundaries(word, program) + clean_colors = check_clean_caps(exits, entries) + G, parts, masks, annihilators = analyze(H) + family_spec = importlib.util.spec_from_file_location("productive_color_family", Path(__file__).with_name("check_family.py")) + family = importlib.util.module_from_spec(family_spec) + family_spec.loader.exec_module(family) + family_result = family.verify(G, DIRTY, HOT) + Hi = inverse(H) + for output in LOCAL: + for input_role in LOCAL: + if H[IX[output]][IX[input_role]] or Hi[IX[input_role]][IX[output]]: + need(entries[input_role] <= exits[output], "two-sided ordinary support containment") + positive = source_positive_control(M, segment, frames, entries, source_exits) + receipt = { + "status": "PASS_DIRECT_ENCODER_ASCENDING_OBSTRUCTION", + "source_bytes_sha256": SOURCE_BYTES_SHA256, "source_json_sha256": SOURCE_JSON_SHA256, + "source_orientation": "forward", "climb_stripped_scalar_interval": [LO, HI], + "source_segment_sha256": digest(segment), "local_roles": LOCAL, + "hot_inputs": HOT, "arbitrary_cold_inputs": [r for r in LOCAL if r not in HOT], + "monochrome_outputs": CLEAN, "remaining_outputs": DIRTY, + "M_sha256": matrix_hash(M, LOCAL, LOCAL), "H_sha256": matrix_hash(H, LOCAL, LOCAL), + "both_M_and_H_inverse_products": True, "native34_35_equal_source_maps": True, + "complete_equal_native_map_class": {"operators": [34, 35, 36], "lenders": [417, 419, 421]}, + "all_forward_and_inverse_support_containments": True, + "protected_output_row": {"13": "1", "416": "1"}, + "source_entry_frames": {str(r): value for r, value in entry_labels.items()}, + "source_exit_frames": {str(r): value for r, value in source_exits.items()}, + "entry_chart_bases": {str(r): basis(entries[r]) for r in LOCAL}, + "fixed_exit_chart_bases": {str(r): basis(exits[r]) for r in LOCAL}, + "monochrome_output_colors": clean_colors, "source_hot_pairs": [list(pair) for pair in PAIRS], + "G_sha256": matrix_hash(G, DIRTY, HOT), "G_rank": 7, + "G_rows": {str(r): sparse(row, HOT) for r, row in zip(DIRTY, G)}, + "unique_G_column_relation": sparse(NORMAL, HOT), "G_row43_column13": "1", + "pair_supported_rowspace_dimensions": parts, + "pair_supported_rowspace_span_dimension": sum(parts), + "allowed_capture_preimage_span_rank": 13, + "common_annihilators": [sparse(v, DIRTY) for v in annihilators], "masks": masks, + "original_source_positive_control": positive, + "common_native_basis_family": family_result, + "scope": "No ascending canonical-chart ADD/SCALE circuit on these24 registers realizes H=P*T*M from the source entry charts to the fixed exit charts. Arbitrary rational coefficients and arbitrary intermediate charts/interleavings are allowed. No preparation prefix is assumed. No new registers or native maps inside the scalar interval; enlarged boundaries, nonascending transports and different target words are not excluded. No tariff or improved-bound claim.", + } + if controls: + receipt["corruption_and_scope_controls"] = corruption_controls(raw, H, G, exits, entries) + family_result["corruption_controls"] = family.controls(G, DIRTY, HOT) + return receipt + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--source", type=Path) + parser.add_argument("--out", type=Path) + args = parser.parse_args() + result = run(args.source) + if args.out: + args.out.write_text(json.dumps(result, indent=2) + "\n", encoding="utf-8") + print(json.dumps({"status": result["status"], "G_rank": result["G_rank"], + "pair_span_dimension": result["pair_supported_rowspace_span_dimension"], + "capture_span_rank": result["allowed_capture_preimage_span_rank"], + "controls": result.get("corruption_and_scope_controls")}, sort_keys=True)) diff --git a/research/productive-helper-color-cut/check_family.py b/research/productive-helper-color-cut/check_family.py new file mode 100644 index 0000000000..0d89f8e7c7 --- /dev/null +++ b/research/productive-helper-color-cut/check_family.py @@ -0,0 +1,112 @@ +"""Exact two-parameter output-family certificate; no parameter sampling. + +The caller supplies the source-reconstructed rational dirty/hot block G. +PROOF-FAMILY.md gives the universal parameter and basis-change argument. +""" +from fractions import Fraction as Q + + +HOT = [13, 16, 43, 44, 51, 78, 99, 104] +DIRTY = [16, 43, 44, 104, 417, 418, 419, 420, 421, 422, + 423, 424, 426, 428, 430] +N0 = [Q(x) for x in (2, 0, -1, 0, 0, -1, -1, 1)] +NL = [Q(x) for x in (0, 0, -1, 0, -2, 1, 1, 1)] +NM = [Q(x) for x in (0, 1, -1, 1, 0, 0, 0, -1)] + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def rank(rows): + """Independent exact row elimination, used only on tiny matrices.""" + rows = [[Q(value) for value in row] for row in rows] + if not rows: + return 0 + width = len(rows[0]) + need(all(len(row) == width for row in rows), "ragged matrix") + count = 0 + for column in range(width): + pivot = next((i for i in range(count, len(rows)) if rows[i][column]), None) + if pivot is None: + continue + rows[count], rows[pivot] = rows[pivot], rows[count] + divisor = rows[count][column] + rows[count] = [value / divisor for value in rows[count]] + for i in range(count + 1, len(rows)): + multiplier = rows[i][column] + if multiplier: + rows[i] = [a - multiplier * b for a, b in zip(rows[i], rows[count])] + count += 1 + if count == len(rows): + break + return count + + +def verify(G, dirty, hot): + """Certify every rational shear419+=lambda*u,421+=mu*u at once.""" + need(list(dirty) == DIRTY and list(hot) == HOT, "source role order") + need(len(G) == len(DIRTY) and all(len(row) == len(HOT) for row in G), + "source block dimensions") + G = [[Q(value) for value in row] for row in G] + need(rank([row[1:] for row in G]) == 7, "seven unaffected columns independent") + need(rank([row for role, row in zip(DIRTY, G) if role not in (419, 421)]) == 5, + "both changed rows removed rank") + # G' = G + (lambda*e419 + mu*e421)*e13^T. + # Match ALL coefficients of G'*(N0 + lambda*NL + mu*NM). + for role, row in zip(DIRTY, G): + dot = lambda vector: sum(a * b for a, b in zip(row, vector)) + e419, e421 = Q(role == 419), Q(role == 421) + coefficients = [dot(N0), dot(NL) + e419 * N0[0], + dot(NM) + e421 * N0[0], e419 * NL[0], + e419 * NM[0] + e421 * NL[0], e421 * NM[0]] + need(coefficients == [0] * 6, "symbolic kernel coefficient identity") + need(N0[0] == 2 and NL[0] == NM[0] == 0, "uniformly nonzero kernel") + # Each coordinate below is the affine triple (constant, lambda, mu). + triples = [tuple(v) for v in zip(N0, NL, NM)] + pair_triples = [[triples[HOT.index(role)] for role in pair] + for pair in [(13, 51), (78, 99), (16, 44), (43, 104)]] + need(pair_triples == [[(2, 0, 0), (0, -2, 0)], + [(-1, 1, 0), (-1, 1, 0)], + [(0, 0, 1), (0, 0, 1)], + [(-1, -1, -1), (1, 1, -1)]], + "four exact pair restrictions") + return { + "status": "RULED_OUT_FOR_ALL_RATIONAL_LAMBDA_MU", + "hot_columns": HOT, + "changed_dirty_outputs": [419, 421], + "unaffected_seven_columns_rank": 7, + "both_changed_rows_removed_rank": 5, + "kernel_constant": [str(x) for x in N0], + "kernel_lambda": [str(x) for x in NL], + "kernel_mu": [str(x) for x in NM], + "symbolic_coefficients_checked_per_row": ["1", "lambda", "mu", "lambda^2", "lambda*mu", "mu^2"], + "rank_for_every_parameter": 7, + "pair_dimension_formula": "4 + [lambda=1] + [mu=0] + [lambda=-1 and mu=0]", + "maximum_single_color_span_dimension": 6, + "covers_invertible_complement_mixing": True, + "new_kappa": False, + } + + +def controls(G, dirty, hot): + """Substantive input and algebra mutations, without sampling parameters.""" + rejected = [] + changed = [[Q(value) for value in row] for row in G] + changed[DIRTY.index(419)][HOT.index(13)] += 1 + damaged_column = [[Q(value) for value in row] for row in G] + for row in damaged_column: + row[HOT.index(16)] = 0 + for name, matrix, row_order, column_order in [ + ("changed_shear_row_coefficient", changed, dirty, hot), + ("lost_unaffected_column_rank", damaged_column, dirty, hot), + ("wrong_role_binding", G, list(reversed(dirty)), hot), + ]: + try: + verify(matrix, row_order, column_order) + except ValueError: + rejected.append(name) + else: + raise ValueError("negative control accepted: " + name) + return rejected diff --git a/research/productive-helper-color-cut/verify.py b/research/productive-helper-color-cut/verify.py new file mode 100644 index 0000000000..7b17e1c04b --- /dev/null +++ b/research/productive-helper-color-cut/verify.py @@ -0,0 +1,41 @@ +#!/usr/bin/env python3 +"""Read-only source-bound replay; --write explicitly authors RESULT.json.""" +from pathlib import Path +import argparse +import hashlib +import importlib.util +import json + +HERE = Path(__file__).resolve().parent +REPO = HERE.parent.parent + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def run(): + manifest = json.loads((HERE / 'SOURCES.json').read_bytes()) + inputs = [row for row in manifest['files'] if row['usage'] == 'input'] + need(len(inputs) == 1, 'one source input') + row = inputs[0] + source = REPO / row['path'] + need(hashlib.sha256(source.read_bytes()).hexdigest() == row['sha256'], 'live source byte hash') + spec = importlib.util.spec_from_file_location('productive_color_check', HERE / 'check.py') + check = importlib.util.module_from_spec(spec) + spec.loader.exec_module(check) + return check.run(source, controls=True) + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true') + args = parser.parse_args() + result = run() + path = HERE / 'RESULT.json' + if args.write: + path.write_bytes((json.dumps(result, indent=2, sort_keys=True) + '\n').encode()) + else: + need(result == json.loads(path.read_bytes()), 'fresh result matches committed receipt') + print(json.dumps({'status': result['status'], 'new_bound': False}, sort_keys=True))