diff --git a/research/productive-helper-inverse-support/.gitattributes b/research/productive-helper-inverse-support/.gitattributes new file mode 100644 index 0000000000..71cb1cfd0c --- /dev/null +++ b/research/productive-helper-inverse-support/.gitattributes @@ -0,0 +1,3 @@ +*.py text eol=lf +*.md text eol=lf +*.json text eol=lf diff --git a/research/productive-helper-inverse-support/PROOF.md b/research/productive-helper-inverse-support/PROOF.md new file mode 100644 index 0000000000..5528ffc6e6 --- /dev/null +++ b/research/productive-helper-inverse-support/PROOF.md @@ -0,0 +1,186 @@ +# Proof of the scoped support obstructions + +## 1. Reverse-support necessity + +Work with arbitrary independent vector-valued registers over the rationals. +Every scalar instruction is an invertible ADD or nonzero SCALE. At a scalar +contact, all participating registers use one common canonical binary chart. +Along a paid transport assume chart inclusion `A subset B` in the forward +direction. Retained transport changes representation, not the logical scalar +register value. There are no native operators inside the replaced local block. + +Let `R` be its invertible scalar matrix, with input charts `A_i` and output +charts `B_j`. Then + +``` +R[j,i] != 0 implies A_i subset B_j, +R^-1[i,j] != 0 implies A_i subset B_j. +``` + +For the first implication, a nonzero coefficient has at least one chronological +dependency path from input `i` to output `j`. Charts increase along that path. +For the second, reverse every instruction and transport. The inverse scalar +circuit has decreasing charts. A nonzero inverse coefficient has a reverse +dependency path from output `j` to input `i`, giving the same containment. +Cancellations can remove coefficients; they cannot produce a nonzero coefficient +without a path. This proves necessity, not sufficiency. + +## 2. Source-derived block factorization + +Use the source and interval in README.md. All 24 local inputs are independent; +the fifteen cold helpers have zero charts but arbitrary data. Let `B=P T`, where +`T` acts on outputs 417/419 and `P` exchanges outputs 416/417. Exact row replay +gives `(B M x)_416 = x_13 + x_416`. Thus the available ascending preparation +`E:416+=13` makes `S=B M E^-1` fix its carrier row. After ordering carrier 416 +first, write + +``` +S = [[1,0],[c,D]], +S^-1 = [[1,0],[-D^-1 c,D^-1]], +alpha = D^-1 c. +``` + +The checker verifies inverses and the factorization exactly. The only nonzero +entries of `alpha` are `+1/2` on 418,419,420,421,424,425 and `-1/2` on 430,431. +All are in the cold set `C={417,...,431}`. Matrix notation in the implementation +retains an identity carrier row and column; `D` here denotes its outside block. + +Consider **any** invertible rational `Q` supported on `C`, extended by identity +on the other outside registers. Grant its implementation without imposing any +extra restriction. With protected value `u` fixed, apply all prefix compensation +`z -> z + beta u`, where `beta=Q alpha`. To reach `c u + D x` from `Q x+beta u`, +the remaining outside matrix is uniquely `R=D Q^-1`. It leaves carrier 416 +untouched. Every row with nonzero `beta_i` has received `u` at a common chart +containing direction 73; subsequent ascending transports retain 73 there. + +The exact, source-reconstructed identity is + +``` +alpha_C = -D^-1[C,78] + (1/2) D^-1[C,431]. (1) +``` + +This is a projected identity on `C`, not an asserted identity on foreign main +coordinates. In particular it does not justify ruling out changes to main +carriers, interleaved compensation, or a larger scalar region. + +## 3. Suffix caps without native or helper constraints + +After the local output basis `B`, emit the same source suffix conjugated by `B` +and append `B^-1`. The paired source native maps are equal on helpers 417/419, +so this is the nominated logical continuation. The checker verifies their exact +map columns and all positive/inverse occurrences. The backward program uses +the corresponding inverse-transpose basis. + +Build the chronological graph of scalar contacts and final main endpoints. +Every paid edge imposes inclusion from its earlier to later node. Owned contacts +have their source chart; all other scalar contacts have variable charts. +For the feasibility relaxation, delete **every native relation**, omit all +adapter pins, and leave **every helper final chart free**. Each remaining graph +component is a directed acyclic graph with identity inclusions. Propagating the +intersection of descendant fixed charts backwards therefore gives the greatest +allowed chart at each node. These are necessary constraints for any actual +native choices and helper boundaries, since removing constraints cannot reduce +the feasible set. + +The exact caps at local outputs 78 and 431 are respectively +`span(25,45,462)` and `span(45,76)`. Neither contains 73. A separately validated +paid-only path of length 8 from 78 and length 9 from 431 ends at main 125's fixed +chart, which excludes 73. No native choice, helper return chart, or adapter +interpretation occurs on those paths. The checker derives the same caps in both +orientations and for both declared suffix variants. Coalescing is only by exact +commuting ADD merges; every crossed instruction is checked. + +## 4. Contradiction for every cold basis + +Since `Q` is invertible and `alpha` is nonzero, choose a cold row `i` with +`beta_i != 0`. Its input to `R` contains 73. Section 1 and the output caps in +section 3 require + +``` +(Q D^-1)[i,78] = (Q D^-1)[i,431] = 0. +``` + +Row `i` of `Q` is supported on `C`, so multiplying (1) by that row gives + +``` +beta_i = -(Q D^-1)[i,78] + (1/2)(Q D^-1)[i,431] = 0, +``` + +a contradiction. This includes concentration into one slot and compensation +distributed among any number of cold slots. It does not depend on pivot order, +temporary matrix fill-in, or the scalar instruction count used to realize `R`. +The obstruction in the forward program alone rules out a complete dual supplier in this scope; +checking both suffix orientations provides additional source validation. + +## 5. Entire scalar-encoder extension + +The same argument also applies to the larger source interval `[6347,10315)`. +This begins immediately after phase A's last native operation and ends at the +centers marker. Every intervening instruction is an invertible scalar ADD or +SCALE on persistent registers. Treat all 632 entries at this cut as independent, +including every dirty register. Reconstructing their actual current charts +gives 457 zero-chart outside registers, including cold main registers. + +The desired row is again exactly `entry13+entry416`. With this larger `M`, form +the same `S=B M E^-1`, `D`, and `alpha`. Exact sparse inverse replay gives the +same compensation coefficients as section 2 except that entry 424 vanishes. +The two-column identity (1) holds on **all 457** cold coordinates, and alpha +has no support outside this set. The checker derives this from the full source, +not by extrapolating the 24-role calculation or assuming untouched spectators. + +Rebuild the declared conjugated suffix from cut 10315. With all native edges, +helper final pins, and adapter pins removed, its caps at 78 and 431 still exclude +73. Applying section 4 rules out every invertible basis on the 457 cold inputs +and every distribution of the complete upfront compensation, followed by an +ascending outside scalar circuit and that suffix. This closes enlargement to +the whole scalar encoder under the same scheduling premise. + +## 6. Stronger main-input obstruction for the same suffix + +Let `M` now denote the whole scalar encoder from section 5. Direct exact replay +of its input-51 column gives `M[51,51]=1/2`. Independently constructing the full +sparse matrix gives the same coefficient. Its actual input chart is `span(100)`. +The output change `B=P T` fixes role 51, so `H=B M` also has `H[51,51]=1/2`. + +For either declared globally conjugated suffix, the greatest relaxed chart at +output 51 is `span(45,76)`, which excludes 100. A separately checked 13-edge +paid-only path leads from this output to main 114's fixed frame 144, also +excluding 100. As in section 3, native relations, helper final constraints and +intermediate adapter pins are absent from the relaxation. Section 1's forward +support condition alone is contradicted: + +``` +H[51,51] != 0, but span(100) is not contained in the allowed output chart. +``` + +Consequently no pure-scalar realization of this required whole-encoder map +with ascending paid charts and the actual entry charts can feed either +declared suffix. This argument does not require upfront compensation, a cold +basis, or a particular factorization. It includes compensation interleaved +within the encoder and cold preparation before the protected value is formed. +The forward obstruction suffices; checking both suffix orientations and both +coalescing variants adds source validation. + +As a positive control, the checker rebuilds the original unmodified suffix and +tests all 3352 nonzero entries of `M` and all 3168 of `M^-1` against its caps. +Every containment holds. Three additional corruption controls change the +required main coefficient, omit a path edge and release the terminal exclusion. + +This stronger result still fixes the suffix contact graph. For example, +undoing `T` immediately after the common paired native operations gives a +different graph and is not ruled out. Nor does it rule out nonascending paid +transports or native operations inside the replacement. + +## 7. Limits + +Sections 2--5 fix the nominated source-consuming block, prefix placement of +all compensation, and one of the two explicitly generated suffix contact +graphs. Section 6 removes the prefix-placement restriction for the nominated +whole-encoder map, while keeping those suffix graphs. Neither theorem fixes +local exit charts beyond necessary suffix caps. Each +assumes subspace inclusion on paid edges; equal-dimensional rotations and +downward transports must be charged and are outside this proof. Different +scalar suffixes, main interfaces, native-bearing replacement blocks, larger +encoder regions crossing native operations require +a fresh calculation. +No global lower bound on productive-helper algorithms or kappa is inferred. diff --git a/research/productive-helper-inverse-support/README.md b/research/productive-helper-inverse-support/README.md new file mode 100644 index 0000000000..0128fc7f36 --- /dev/null +++ b/research/productive-helper-inverse-support/README.md @@ -0,0 +1,141 @@ +# Support obstructions for a source-consuming productive helper + +**Scoped obstruction; no improved bound.** A proposed encoder would prepare +native input 34 on the one-dimensional chart `span(73)`, replacing its source +five-dimensional chart. Its desired value is exactly the sum of source entry 13 +and arbitrary dirty entry 416. Computing that value is easy; returning the other +independent inputs is the obstacle. + +This package proves that **no invertible basis change on the fifteen cold +helpers 417–431, including distributing the compensation among them, can finish +this particular source-consuming construction by ascending scalar transports**. +The same obstruction holds after replacing the entire scalar encoder, allowing +an arbitrary basis on all **457 zero-chart entry registers**, including cold +main registers. Enlarging the local replacement alone therefore does not help. +The result allows arbitrary local exit charts compatible with either declared +suffix. It even drops every suffix native relation, every helper final-frame +constraint, and every intermediate adapter pin. Two retained paths to fixed +main outputs still force the contradiction. + +There is also a simpler, stronger obstruction for this same retained suffix: +the required transfer from main input 51 to main output 51 is `1/2`, its input +chart is `span(100)`, but the greatest permitted output chart is `span(45,76)`. +It excludes 100. This rules out **every ascending pure-scalar realization of +the nominated whole-encoder map**, including interleaved compensation and +preparation on cold inputs. The original encoder and original suffix pass all +forward and inverse support checks, providing a positive control. + +These are proofs about specified families, not conclusions from an unsuccessful +pivot search. They do not exclude changed scalar suffix contacts, paid +nonmonotone transports, or other productive-helper constructions. In particular, +undoing `T` immediately after the paired native operations changes the suffix +and falls outside both theorems. Ascending means inclusion of the actual binary +subspaces, not merely nondecreasing dimension. There is no new physical supplier, +compiler admission, multiplication theorem, or value of kappa. + +## Exact mechanism and result + +The source is the integrated [98-instruction compression certificate](../productive-helper-fusion-certificate/README.md), +with decompressed canonical payload SHA256 +`aa4a8241da76abd2c06e6576a3ac09e77781321deaac3ad7d3ce4519342a36e6`. +Indices below are zero-based after removing `climb` records. + +The scalar interval `[9961,10111)` contains 150 instructions on 24 independent +roles. Let its rational matrix be `M`. Change the output basis of helpers +417/419 by `T = [[1/2,-1],[1/2,1]]`, then exchange roles 416/417 by `P`. +The desired output on 416 is exactly `entry13 + entry416`. Prepare that output +with `E: 416 += 13`. In coordinates with 416 first, + +``` +S = P T M E^-1 = [[1, 0], [c, D]], alpha = D^-1 c. +``` + +Here `alpha` is supported on the fifteen initially zero-chart outside helpers. +For an arbitrary invertible basis `Q` on these helpers, prefix compensation +installs `beta = Q alpha` copies of the protected value. The remaining exact +outside transformation must be `D Q^-1`. The checker reconstructs, over the +rationals, the following identity on **all fifteen cold coordinates**: + +``` +alpha = -D^-1[:,78] + (1/2) D^-1[:,431]. +``` + +If `beta_i != 0`, that input slot must carry direction 73. Reversing an ascending +scalar circuit shows that a nonzero inverse coefficient requires its input chart +to be contained in the corresponding output chart. Both outputs 78 and 431 +exclude 73, so both entries in row `i` of `Q D^-1` must vanish. The displayed +identity then gives `beta_i = 0`, a contradiction. Invertibility of `Q` ensures +some component of `beta` is nonzero. [PROOF.md](PROOF.md) gives the full argument. + +The independently rebuilt suffix bounds are: + +| Local output | Greatest relaxed suffix chart | Shortest retained path | +| --- | --- | --- | +| 78 | `span(25,45,462)` | 8 paid edges to main 125 | +| 99 | `span(45,76,411)` | 8 paid edges to main 114 | +| 431 | `span(45,76)` | 9 paid edges to main 125 | + +All exclude 73. Outputs 78 and 431 suffice for the universal cold-basis argument; +99 is retained as a supplementary suffix-cap check. Both program orientations +and both the literal and coalesced suffix are +checked. Coalescing uses the credited commuting-ADD rule from PR4692, checking +every crossed instruction. No claim of arbitrary suffix equivalence is made. + +The stronger replay replaces `[6347,10315)`, the complete scalar part of phase A +after its last early native operation. It keeps all 632 independent inputs and +reconstructs its sparse rational matrix and inverse. The same two-column +annihilator identity holds on all 457 zero-chart entry coordinates; the +compensation now has seven nonzero entries. Fresh suffix graphs from cut 10315 +give the same excluding caps at 78 and 431. The proof is therefore unchanged. + +The main-input obstruction uses the same whole-encoder interval. Since `P T` +fixes output 51, its required coefficient on input 51 remains `1/2`. An explicit +13-edge paid path from output 51 to main 114 at fixed frame 144 excludes input +direction 100, even after every native relation, helper final pin and adapter +pin is released. Both declared suffix variants and orientations are checked. +The original source control checks all 3352 forward and 3168 inverse nonzero +coefficients with no violation. See section 6 of [PROOF.md](PROOF.md). + +## Reproduction + +From the repository root, using Python 3.12 and its standard library: + +```sh +python3 -I -B research/productive-helper-inverse-support/verify.py +python3 -I -O -B research/productive-helper-inverse-support/verify.py +``` + +The default replay is read-only and needs no solver, network, Git history, or +discovery artifacts. It authenticates its live source, reconstructs the local +matrix and Schur factorization, verifies the exact annihilator, rebuilds both +suffix graphs, and validates explicit paths to main pins. Sixteen corruption +controls address source coefficients, compensation, the identity, native pairing, +path continuity, and terminal constraints. The checked source preserves all +632 arbitrary inputs; this local result never treats dirty helpers as zero data. + +The new argument has been checked by separately developed agent scripts and +the packaged replay. This is AI-assisted verification, not independent human +review or proof-kernel verification. Source pins and executable dependencies +are listed in [SOURCES.json](SOURCES.json) and [VERIFY.json](VERIFY.json). + +## Open next questions + +The structured questions are in [TASK.json](TASK.json). A useful next test is +to change an actual suffix dependency, then check +the corresponding exact inverse-support equations before synthesis. Another +escape is to price a nonmonotone realization; it must beat the complete +paid-minus-helper invoice, including any return transport and native changes. +Passing the necessary equations alone would not establish a cheaper circuit. + +## Attribution + +This starts from Cao Yifan's PR4610 round3 word and Cinna Davis's PR4692 scalar +compression, through flyingviper's PR5301 combined source. Retain Cinna Davis's +PR4470/controller lineage, Dugongue's frame and physical-interface work, zxv's +native/compiler work, Jacob Alan Sussman's flow work, and all predecessor credits. +The elementary reverse-dependency and block-matrix arguments are not claimed +as new general linear-algebra results. The contribution is their source-bound +application, the exact annihilator, and the suffix certificates. + +Prepared for flyingviper with substantial OpenAI Codex assistance and independent +agent checks. Apache-2.0. The selected result and frozen sources are unchanged. diff --git a/research/productive-helper-inverse-support/RESULT.json b/research/productive-helper-inverse-support/RESULT.json new file mode 100644 index 0000000000..c7eb78f400 --- /dev/null +++ b/research/productive-helper-inverse-support/RESULT.json @@ -0,0 +1,1908 @@ +{ + "controls": { + "local": { + "count": 8, + "passed": [ + "source_payload_changed", + "source_local_coefficient_changed", + "annihilator_sign_changed", + "compensation_coefficient_changed", + "paired_native_map_changed", + "suffix_path_edge_deleted", + "suffix_terminal_pin_removed", + "suffix_terminal_contains73" + ] + }, + "main_support": { + "count": 3, + "passed": [ + "required_main_coefficient_changed", + "main_witness_edge_omitted", + "main_terminal_admits100" + ] + }, + "whole_encoder": { + "count": 5, + "passed": [ + "whole_source_compensation_value_changed", + "whole_cold_role_omitted", + "whole_noncold_main_role_added", + "whole_inverse_column_coefficient_changed", + "whole_full_inverse_product_corrupted" + ] + } + }, + "local": { + "alpha": { + "418": "1/2", + "419": "1/2", + "420": "1/2", + "421": "1/2", + "424": "1/2", + "425": "1/2", + "430": "-1/2", + "431": "-1/2" + }, + "annihilator": { + "coefficients": [ + "-1", + "1/2" + ], + "columns": [ + 78, + 431 + ], + "identity": "alpha = -D^-1[:,78] + (1/2)D^-1[:,431] on cold coordinates" + }, + "cold_roles": [ + 417, + 418, + 419, + 420, + 421, + 422, + 423, + 424, + 425, + 426, + 427, + 428, + 429, + 430, + 431 + ], + "directions": { + "backward": { + "coalescing": { + "cancellations": 4, + "crossed_checks": 38, + "merges": 22 + }, + "variants": { + "coalesced": { + "caps": { + "431": { + "basis": [ + 45, + 76 + ], + "witness": { + "length": 9, + "roles": [ + 431, + 431, + 431, + 431, + 163, + 125, + 125, + 125, + 125 + ], + "source_ordinals": [ + 10920, + 10922, + 10924, + 10933, + 11993, + 11994, + 12404, + 12412, + null + ], + "suffix_ordinals": [ + 809, + 811, + 813, + 822, + 1886, + 1887, + 2303, + 2311, + 8027 + ], + "terminal_basis": [ + 2, + 4, + 9, + 16, + 32, + 65, + 128, + 256 + ], + "terminal_frame": 155, + "terminal_kind": "main_final", + "terminal_role": 125 + } + }, + "78": { + "basis": [ + 25, + 45, + 462 + ], + "witness": { + "length": 8, + "roles": [ + 78, + 127, + 239, + 125, + 125, + 125, + 125, + 125 + ], + "source_ordinals": [ + 10874, + 10881, + 10891, + 11993, + 11994, + 12404, + 12412, + null + ], + "suffix_ordinals": [ + 763, + 770, + 780, + 1886, + 1887, + 2303, + 2311, + 8027 + ], + "terminal_basis": [ + 2, + 4, + 9, + 16, + 32, + 65, + 128, + 256 + ], + "terminal_frame": 155, + "terminal_kind": "main_final", + "terminal_role": 125 + } + }, + "99": { + "basis": [ + 45, + 76, + 411 + ], + "witness": { + "length": 8, + "roles": [ + 99, + 99, + 445, + 137, + 114, + 114, + 114, + 114 + ], + "source_ordinals": [ + 10942, + 10944, + 10953, + 11879, + 11880, + 12100, + 12104, + null + ], + "suffix_ordinals": [ + 831, + 833, + 842, + 1772, + 1773, + 1995, + 2002, + 8027 + ], + "terminal_basis": [ + 3, + 4, + 8, + 16, + 33, + 64, + 128, + 256 + ], + "terminal_frame": 144, + "terminal_kind": "main_final", + "terminal_role": 114 + } + } + }, + "omitted_native_occurrences": 144, + "paid_incidences": 15203, + "scalar_event_count": 7644, + "suffix_event_count": 8027, + "suffix_sha256": "8436081ef62128605ba60514f70562c55669a7a8eeff0912d319a1db06b13850" + }, + "uncoalesced": { + "caps": { + "431": { + "basis": [ + 45, + 76 + ], + "witness": { + "length": 9, + "roles": [ + 431, + 431, + 431, + 431, + 163, + 125, + 125, + 125, + 125 + ], + "source_ordinals": [ + 10920, + 10922, + 10924, + 10933, + 11993, + 11994, + 12404, + 12412, + null + ], + "suffix_ordinals": [ + 809, + 811, + 813, + 822, + 1890, + 1891, + 2307, + 2315, + 8053 + ], + "terminal_basis": [ + 2, + 4, + 9, + 16, + 32, + 65, + 128, + 256 + ], + "terminal_frame": 155, + "terminal_kind": "main_final", + "terminal_role": 125 + } + }, + "78": { + "basis": [ + 25, + 45, + 462 + ], + "witness": { + "length": 8, + "roles": [ + 78, + 127, + 239, + 125, + 125, + 125, + 125, + 125 + ], + "source_ordinals": [ + 10874, + 10881, + 10891, + 11993, + 11994, + 12404, + 12412, + null + ], + "suffix_ordinals": [ + 763, + 770, + 780, + 1890, + 1891, + 2307, + 2315, + 8053 + ], + "terminal_basis": [ + 2, + 4, + 9, + 16, + 32, + 65, + 128, + 256 + ], + "terminal_frame": 155, + "terminal_kind": "main_final", + "terminal_role": 125 + } + }, + "99": { + "basis": [ + 45, + 76, + 411 + ], + "witness": { + "length": 8, + "roles": [ + 99, + 99, + 445, + 137, + 114, + 114, + 114, + 114 + ], + "source_ordinals": [ + 10942, + 10944, + 10953, + 11879, + 11880, + 12100, + 12104, + null + ], + "suffix_ordinals": [ + 831, + 833, + 842, + 1776, + 1777, + 1999, + 2006, + 8053 + ], + "terminal_basis": [ + 3, + 4, + 8, + 16, + 33, + 64, + 128, + 256 + ], + "terminal_frame": 144, + "terminal_kind": "main_final", + "terminal_role": 114 + } + } + }, + "omitted_native_occurrences": 144, + "paid_incidences": 15255, + "scalar_event_count": 7670, + "suffix_event_count": 8053, + "suffix_sha256": "3bf154b9ff0878c5c6a7a467e9f68bca74655a57de840e7eb7b7c22643e499ff" + } + } + }, + "forward": { + "coalescing": { + "cancellations": 4, + "crossed_checks": 38, + "merges": 21 + }, + "variants": { + "coalesced": { + "caps": { + "431": { + "basis": [ + 45, + 76 + ], + "witness": { + "length": 9, + "roles": [ + 431, + 431, + 431, + 431, + 163, + 163, + 125, + 125, + 125 + ], + "source_ordinals": [ + 10920, + 10922, + 10924, + 10933, + 11993, + 11994, + 12404, + 12412, + null + ], + "suffix_ordinals": [ + 809, + 811, + 813, + 822, + 1886, + 1887, + 2303, + 2311, + 8026 + ], + "terminal_basis": [ + 2, + 4, + 9, + 16, + 32, + 65, + 128, + 256 + ], + "terminal_frame": 155, + "terminal_kind": "main_final", + "terminal_role": 125 + } + }, + "78": { + "basis": [ + 25, + 45, + 462 + ], + "witness": { + "length": 8, + "roles": [ + 78, + 127, + 239, + 125, + 163, + 125, + 125, + 125 + ], + "source_ordinals": [ + 10874, + 10881, + 10891, + 11993, + 11994, + 12404, + 12412, + null + ], + "suffix_ordinals": [ + 763, + 770, + 780, + 1886, + 1887, + 2303, + 2311, + 8026 + ], + "terminal_basis": [ + 2, + 4, + 9, + 16, + 32, + 65, + 128, + 256 + ], + "terminal_frame": 155, + "terminal_kind": "main_final", + "terminal_role": 125 + } + }, + "99": { + "basis": [ + 45, + 76, + 411 + ], + "witness": { + "length": 8, + "roles": [ + 99, + 99, + 445, + 137, + 137, + 114, + 114, + 114 + ], + "source_ordinals": [ + 10942, + 10944, + 10953, + 11879, + 11880, + 12100, + 12104, + null + ], + "suffix_ordinals": [ + 831, + 833, + 842, + 1772, + 1773, + 1995, + 2002, + 8026 + ], + "terminal_basis": [ + 3, + 4, + 8, + 16, + 33, + 64, + 128, + 256 + ], + "terminal_frame": 144, + "terminal_kind": "main_final", + "terminal_role": 114 + } + } + }, + "omitted_native_occurrences": 144, + "paid_incidences": 15201, + "scalar_event_count": 7643, + "suffix_event_count": 8026, + "suffix_sha256": "bb42ee922a28f476ea1de0389431a012675cc5fc22155734d4580b3f98193b6a" + }, + "uncoalesced": { + "caps": { + "431": { + "basis": [ + 45, + 76 + ], + "witness": { + "length": 9, + "roles": [ + 431, + 431, + 431, + 431, + 163, + 163, + 125, + 125, + 125 + ], + "source_ordinals": [ + 10920, + 10922, + 10924, + 10933, + 11993, + 11994, + 12404, + 12412, + null + ], + "suffix_ordinals": [ + 809, + 811, + 813, + 822, + 1890, + 1891, + 2307, + 2315, + 8051 + ], + "terminal_basis": [ + 2, + 4, + 9, + 16, + 32, + 65, + 128, + 256 + ], + "terminal_frame": 155, + "terminal_kind": "main_final", + "terminal_role": 125 + } + }, + "78": { + "basis": [ + 25, + 45, + 462 + ], + "witness": { + "length": 8, + "roles": [ + 78, + 127, + 239, + 125, + 163, + 125, + 125, + 125 + ], + "source_ordinals": [ + 10874, + 10881, + 10891, + 11993, + 11994, + 12404, + 12412, + null + ], + "suffix_ordinals": [ + 763, + 770, + 780, + 1890, + 1891, + 2307, + 2315, + 8051 + ], + "terminal_basis": [ + 2, + 4, + 9, + 16, + 32, + 65, + 128, + 256 + ], + "terminal_frame": 155, + "terminal_kind": "main_final", + "terminal_role": 125 + } + }, + "99": { + "basis": [ + 45, + 76, + 411 + ], + "witness": { + "length": 8, + "roles": [ + 99, + 99, + 445, + 137, + 137, + 114, + 114, + 114 + ], + "source_ordinals": [ + 10942, + 10944, + 10953, + 11879, + 11880, + 12100, + 12104, + null + ], + "suffix_ordinals": [ + 831, + 833, + 842, + 1776, + 1777, + 1999, + 2006, + 8051 + ], + "terminal_basis": [ + 3, + 4, + 8, + 16, + 33, + 64, + 128, + 256 + ], + "terminal_frame": 144, + "terminal_kind": "main_final", + "terminal_role": 114 + } + } + }, + "omitted_native_occurrences": 144, + "paid_incidences": 15251, + "scalar_event_count": 7668, + "suffix_event_count": 8051, + "suffix_sha256": "9b1ad31a6b4333fd848af928648c3ddb6927cfb37c8e980c844cf020dc2b52d0" + } + } + } + }, + "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 + ], + "native_source_bindings": { + "backward": [ + { + "op": 34, + "role": 417, + "source_ordinal": 11491 + }, + { + "op": 35, + "role": 419, + "source_ordinal": 11492 + }, + { + "op": -35, + "role": 419, + "source_ordinal": 13455 + }, + { + "op": -34, + "role": 417, + "source_ordinal": 13456 + } + ], + "forward": [ + { + "op": 34, + "role": 417, + "source_ordinal": 11491 + }, + { + "op": 35, + "role": 419, + "source_ordinal": 11492 + }, + { + "op": -35, + "role": 419, + "source_ordinal": 13455 + }, + { + "op": -34, + "role": 417, + "source_ordinal": 13456 + } + ] + }, + "quotient_matrix_sha256": "d1f46116a3aab8538cc68570b53e5c95b935fa11207d2560531213b5d4673668", + "relaxations": [ + "all suffix native edges removed", + "all helper final pins removed", + "intermediate adapter pins omitted" + ], + "scope": "No invertible cold-helper basis Q with all beta=Q*alpha compensation performed as a prefix can be followed by a pure-scalar realization of DQ^-1 and either declared retained suffix whose paid canonical chart spaces only grow by inclusion. Distributed prefix compensation is included. Interleaved compensation, changed suffix contacts, nonmonotone paid transports and new multiplication bounds are not claimed.", + "source_interval": [ + 9961, + 10111 + ], + "source_local_matrix_sha256": "e2add2fd3ff9cee196c91461b430cd8fb9a5b66573467ff7a870b36eb8e4721f", + "source_sha256": "aa4a8241da76abd2c06e6576a3ac09e77781321deaac3ad7d3ce4519342a36e6", + "status": "PASS_SCOPED_INVERSE_SUPPORT_OBSTRUCTION" + }, + "main_support": { + "B_fixes_output51": true, + "directions": { + "backward": { + "coalescing": { + "cancellations": 4, + "crossed_checks": 38, + "merges": 22 + }, + "variants": { + "coalesced": { + "output51_cap": [ + 45, + 76 + ], + "suffix_sha256": "6e6f607c5f03227d5bd30f9b1533dcfd3b240f0e2aeb0dd429480dac3513ca1e", + "witness100": { + "length": 13, + "roles": [ + 51, + 51, + 447, + 223, + 121, + 121, + 173, + 173, + 173, + 419, + 419, + 596, + 114 + ], + "source_ordinals": [ + 10919, + 10923, + 10926, + 10927, + 10931, + 11876, + 11877, + 12101, + 12101, + 12102, + 12103, + 12104, + null + ], + "suffix_ordinals": [ + 604, + 608, + 611, + 612, + 616, + 1565, + 1566, + 1792, + 1793, + 1795, + 1797, + 1798, + 7823 + ], + "terminal_basis": [ + 3, + 4, + 8, + 16, + 33, + 64, + 128, + 256 + ], + "terminal_frame": 144, + "terminal_kind": "main_final", + "terminal_role": 114 + } + }, + "uncoalesced": { + "output51_cap": [ + 45, + 76 + ], + "suffix_sha256": "48ee616f081302b9d219a7d595add10cca3e6121d46176f6a5d1ebac337e0774", + "witness100": { + "length": 13, + "roles": [ + 51, + 51, + 447, + 223, + 121, + 121, + 173, + 173, + 173, + 419, + 419, + 596, + 114 + ], + "source_ordinals": [ + 10919, + 10923, + 10926, + 10927, + 10931, + 11876, + 11877, + 12101, + 12101, + 12102, + 12103, + 12104, + null + ], + "suffix_ordinals": [ + 604, + 608, + 611, + 612, + 616, + 1569, + 1570, + 1796, + 1797, + 1799, + 1801, + 1802, + 7849 + ], + "terminal_basis": [ + 3, + 4, + 8, + 16, + 33, + 64, + 128, + 256 + ], + "terminal_frame": 144, + "terminal_kind": "main_final", + "terminal_role": 114 + } + } + } + }, + "forward": { + "coalescing": { + "cancellations": 4, + "crossed_checks": 38, + "merges": 21 + }, + "variants": { + "coalesced": { + "output51_cap": [ + 45, + 76 + ], + "suffix_sha256": "ce119ec1542cddff43ee7b92eeafa81398c3628dbe1ac8ad4ca7e301fcb295e1", + "witness100": { + "length": 13, + "roles": [ + 51, + 51, + 447, + 223, + 121, + 121, + 121, + 173, + 173, + 419, + 419, + 596, + 114 + ], + "source_ordinals": [ + 10919, + 10923, + 10926, + 10927, + 10931, + 11876, + 11877, + 12101, + 12101, + 12102, + 12103, + 12104, + null + ], + "suffix_ordinals": [ + 604, + 608, + 611, + 612, + 616, + 1565, + 1566, + 1792, + 1793, + 1795, + 1797, + 1798, + 7822 + ], + "terminal_basis": [ + 3, + 4, + 8, + 16, + 33, + 64, + 128, + 256 + ], + "terminal_frame": 144, + "terminal_kind": "main_final", + "terminal_role": 114 + } + }, + "uncoalesced": { + "output51_cap": [ + 45, + 76 + ], + "suffix_sha256": "13ef7921eb50f6f402e179a1333ebb7c906be52f061f8834d91c67beae63e680", + "witness100": { + "length": 13, + "roles": [ + 51, + 51, + 447, + 223, + 121, + 121, + 121, + 173, + 173, + 419, + 419, + 596, + 114 + ], + "source_ordinals": [ + 10919, + 10923, + 10926, + 10927, + 10931, + 11876, + 11877, + 12101, + 12101, + 12102, + 12103, + 12104, + null + ], + "suffix_ordinals": [ + 604, + 608, + 611, + 612, + 616, + 1569, + 1570, + 1796, + 1797, + 1799, + 1801, + 1802, + 7847 + ], + "terminal_basis": [ + 3, + 4, + 8, + 16, + 33, + 64, + 128, + 256 + ], + "terminal_frame": 144, + "terminal_kind": "main_final", + "terminal_role": 114 + } + } + } + } + }, + "encoder_interval": [ + 6347, + 10315 + ], + "positive_control": { + "forward_violations": 0, + "inverse_violations": 0, + "original_forward_support_checks": 3352, + "original_inverse_support_checks": 3168, + "original_output51_cap": [ + 5, + 40, + 73 + ] + }, + "required_coefficient": { + "input_basis": [ + 100 + ], + "input_role": 51, + "output_role": 51, + "value": "1/2" + }, + "scope": "With the actual scalar-A input charts, the required transfer H=P*T*M has a nonzero main51-to-main51 coefficient. No pure-scalar realization whose paid canonical chart spaces grow by inclusion can feed either declared globally B-conjugated suffix. This is independent of cold prefix choices and compensation interleaving. All suffix native edges/helper-final/adapter pins are released. It does not cover a changed suffix, including transient T undone immediately after the paired natives, or nonmonotone paid transports. No new bound is claimed.", + "source_sha256": "aa4a8241da76abd2c06e6576a3ac09e77781321deaac3ad7d3ce4519342a36e6", + "status": "PASS_MAIN_SUPPORT_RETAINED_SUFFIX_OBSTRUCTION" + }, + "status": "PASS_PRODUCTIVE_HELPER_INVERSE_SUPPORT", + "whole_encoder": { + "alpha": { + "418": "1/2", + "419": "1/2", + "420": "1/2", + "421": "1/2", + "425": "1/2", + "430": "-1/2", + "431": "-1/2" + }, + "annihilator": "alpha = -D^-1[:,78] + (1/2)D^-1[:,431] on every actual cold entry role", + "arbitrary_input_roles": 632, + "both_full632_inverse_products": true, + "cold_main_role_count": 100, + "cold_role_count": 457, + "cold_role_list_sha256": "87b8e8c84e310c3b45b71ebb1f90891723e639ce2fddacc410b32c1788279da6", + "directions": { + "backward": { + "coalescing": { + "cancellations": 4, + "crossed_checks": 38, + "merges": 22 + }, + "variants": { + "coalesced": { + "caps": { + "431": { + "basis": [ + 45, + 76 + ], + "witness": { + "length": 9, + "roles": [ + 431, + 431, + 431, + 431, + 163, + 125, + 125, + 125, + 125 + ], + "source_ordinals": [ + 10920, + 10922, + 10924, + 10933, + 11993, + 11994, + 12404, + 12412, + null + ], + "suffix_ordinals": [ + 605, + 607, + 609, + 618, + 1682, + 1683, + 2099, + 2107, + 7823 + ], + "terminal_basis": [ + 2, + 4, + 9, + 16, + 32, + 65, + 128, + 256 + ], + "terminal_frame": 155, + "terminal_kind": "main_final", + "terminal_role": 125 + } + }, + "78": { + "basis": [ + 25, + 45, + 462 + ], + "witness": { + "length": 8, + "roles": [ + 78, + 127, + 239, + 125, + 125, + 125, + 125, + 125 + ], + "source_ordinals": [ + 10874, + 10881, + 10891, + 11993, + 11994, + 12404, + 12412, + null + ], + "suffix_ordinals": [ + 559, + 566, + 576, + 1682, + 1683, + 2099, + 2107, + 7823 + ], + "terminal_basis": [ + 2, + 4, + 9, + 16, + 32, + 65, + 128, + 256 + ], + "terminal_frame": 155, + "terminal_kind": "main_final", + "terminal_role": 125 + } + }, + "99": { + "basis": [ + 45, + 76, + 411 + ], + "witness": { + "length": 8, + "roles": [ + 99, + 99, + 445, + 137, + 114, + 114, + 114, + 114 + ], + "source_ordinals": [ + 10942, + 10944, + 10953, + 11879, + 11880, + 12100, + 12104, + null + ], + "suffix_ordinals": [ + 627, + 629, + 638, + 1568, + 1569, + 1791, + 1798, + 7823 + ], + "terminal_basis": [ + 3, + 4, + 8, + 16, + 33, + 64, + 128, + 256 + ], + "terminal_frame": 144, + "terminal_kind": "main_final", + "terminal_role": 114 + } + } + }, + "omitted_native_occurrences": 144, + "suffix_event_count": 7823, + "suffix_sha256": "6e6f607c5f03227d5bd30f9b1533dcfd3b240f0e2aeb0dd429480dac3513ca1e" + }, + "uncoalesced": { + "caps": { + "431": { + "basis": [ + 45, + 76 + ], + "witness": { + "length": 9, + "roles": [ + 431, + 431, + 431, + 431, + 163, + 125, + 125, + 125, + 125 + ], + "source_ordinals": [ + 10920, + 10922, + 10924, + 10933, + 11993, + 11994, + 12404, + 12412, + null + ], + "suffix_ordinals": [ + 605, + 607, + 609, + 618, + 1686, + 1687, + 2103, + 2111, + 7849 + ], + "terminal_basis": [ + 2, + 4, + 9, + 16, + 32, + 65, + 128, + 256 + ], + "terminal_frame": 155, + "terminal_kind": "main_final", + "terminal_role": 125 + } + }, + "78": { + "basis": [ + 25, + 45, + 462 + ], + "witness": { + "length": 8, + "roles": [ + 78, + 127, + 239, + 125, + 125, + 125, + 125, + 125 + ], + "source_ordinals": [ + 10874, + 10881, + 10891, + 11993, + 11994, + 12404, + 12412, + null + ], + "suffix_ordinals": [ + 559, + 566, + 576, + 1686, + 1687, + 2103, + 2111, + 7849 + ], + "terminal_basis": [ + 2, + 4, + 9, + 16, + 32, + 65, + 128, + 256 + ], + "terminal_frame": 155, + "terminal_kind": "main_final", + "terminal_role": 125 + } + }, + "99": { + "basis": [ + 45, + 76, + 411 + ], + "witness": { + "length": 8, + "roles": [ + 99, + 99, + 445, + 137, + 114, + 114, + 114, + 114 + ], + "source_ordinals": [ + 10942, + 10944, + 10953, + 11879, + 11880, + 12100, + 12104, + null + ], + "suffix_ordinals": [ + 627, + 629, + 638, + 1572, + 1573, + 1795, + 1802, + 7849 + ], + "terminal_basis": [ + 3, + 4, + 8, + 16, + 33, + 64, + 128, + 256 + ], + "terminal_frame": 144, + "terminal_kind": "main_final", + "terminal_role": 114 + } + } + }, + "omitted_native_occurrences": 144, + "suffix_event_count": 7849, + "suffix_sha256": "48ee616f081302b9d219a7d595add10cca3e6121d46176f6a5d1ebac337e0774" + } + } + }, + "forward": { + "coalescing": { + "cancellations": 4, + "crossed_checks": 38, + "merges": 21 + }, + "variants": { + "coalesced": { + "caps": { + "431": { + "basis": [ + 45, + 76 + ], + "witness": { + "length": 9, + "roles": [ + 431, + 431, + 431, + 431, + 163, + 163, + 125, + 125, + 125 + ], + "source_ordinals": [ + 10920, + 10922, + 10924, + 10933, + 11993, + 11994, + 12404, + 12412, + null + ], + "suffix_ordinals": [ + 605, + 607, + 609, + 618, + 1682, + 1683, + 2099, + 2107, + 7822 + ], + "terminal_basis": [ + 2, + 4, + 9, + 16, + 32, + 65, + 128, + 256 + ], + "terminal_frame": 155, + "terminal_kind": "main_final", + "terminal_role": 125 + } + }, + "78": { + "basis": [ + 25, + 45, + 462 + ], + "witness": { + "length": 8, + "roles": [ + 78, + 127, + 239, + 125, + 163, + 125, + 125, + 125 + ], + "source_ordinals": [ + 10874, + 10881, + 10891, + 11993, + 11994, + 12404, + 12412, + null + ], + "suffix_ordinals": [ + 559, + 566, + 576, + 1682, + 1683, + 2099, + 2107, + 7822 + ], + "terminal_basis": [ + 2, + 4, + 9, + 16, + 32, + 65, + 128, + 256 + ], + "terminal_frame": 155, + "terminal_kind": "main_final", + "terminal_role": 125 + } + }, + "99": { + "basis": [ + 45, + 76, + 411 + ], + "witness": { + "length": 8, + "roles": [ + 99, + 99, + 445, + 137, + 137, + 114, + 114, + 114 + ], + "source_ordinals": [ + 10942, + 10944, + 10953, + 11879, + 11880, + 12100, + 12104, + null + ], + "suffix_ordinals": [ + 627, + 629, + 638, + 1568, + 1569, + 1791, + 1798, + 7822 + ], + "terminal_basis": [ + 3, + 4, + 8, + 16, + 33, + 64, + 128, + 256 + ], + "terminal_frame": 144, + "terminal_kind": "main_final", + "terminal_role": 114 + } + } + }, + "omitted_native_occurrences": 144, + "suffix_event_count": 7822, + "suffix_sha256": "ce119ec1542cddff43ee7b92eeafa81398c3628dbe1ac8ad4ca7e301fcb295e1" + }, + "uncoalesced": { + "caps": { + "431": { + "basis": [ + 45, + 76 + ], + "witness": { + "length": 9, + "roles": [ + 431, + 431, + 431, + 431, + 163, + 163, + 125, + 125, + 125 + ], + "source_ordinals": [ + 10920, + 10922, + 10924, + 10933, + 11993, + 11994, + 12404, + 12412, + null + ], + "suffix_ordinals": [ + 605, + 607, + 609, + 618, + 1686, + 1687, + 2103, + 2111, + 7847 + ], + "terminal_basis": [ + 2, + 4, + 9, + 16, + 32, + 65, + 128, + 256 + ], + "terminal_frame": 155, + "terminal_kind": "main_final", + "terminal_role": 125 + } + }, + "78": { + "basis": [ + 25, + 45, + 462 + ], + "witness": { + "length": 8, + "roles": [ + 78, + 127, + 239, + 125, + 163, + 125, + 125, + 125 + ], + "source_ordinals": [ + 10874, + 10881, + 10891, + 11993, + 11994, + 12404, + 12412, + null + ], + "suffix_ordinals": [ + 559, + 566, + 576, + 1686, + 1687, + 2103, + 2111, + 7847 + ], + "terminal_basis": [ + 2, + 4, + 9, + 16, + 32, + 65, + 128, + 256 + ], + "terminal_frame": 155, + "terminal_kind": "main_final", + "terminal_role": 125 + } + }, + "99": { + "basis": [ + 45, + 76, + 411 + ], + "witness": { + "length": 8, + "roles": [ + 99, + 99, + 445, + 137, + 137, + 114, + 114, + 114 + ], + "source_ordinals": [ + 10942, + 10944, + 10953, + 11879, + 11880, + 12100, + 12104, + null + ], + "suffix_ordinals": [ + 627, + 629, + 638, + 1572, + 1573, + 1795, + 1802, + 7847 + ], + "terminal_basis": [ + 3, + 4, + 8, + 16, + 33, + 64, + 128, + 256 + ], + "terminal_frame": 144, + "terminal_kind": "main_final", + "terminal_role": 114 + } + } + }, + "omitted_native_occurrences": 144, + "suffix_event_count": 7847, + "suffix_sha256": "13ef7921eb50f6f402e179a1333ebb7c906be52f061f8834d91c67beae63e680" + } + } + } + }, + "forward_matrix_nonzeros": 3352, + "independent_vector_column_round_trips": true, + "inverse_matrix_nonzeros": 3168, + "scalar_events": 3968, + "scope": "The same obstruction covers arbitrary invertible bases on all457 zero-chart persistent entry roles of the entire scalar-A interval, including cold main roles, with all compensation placed before its pure-scalar quotient. Paid canonical chart spaces must grow by inclusion through the declared retained suffix. Native edges, helper final pins and intermediate adapter pins are released. Interleaved compensation, changed suffix contacts, nonmonotone transports and a new bound remain outside the claim.", + "selected_inverse_columns": [ + 416, + 78, + 431 + ], + "source_interval": [ + 6347, + 10315 + ], + "source_sha256": "aa4a8241da76abd2c06e6576a3ac09e77781321deaac3ad7d3ce4519342a36e6", + "status": "PASS_WHOLE_SCALAR_ENCODER_INVERSE_SUPPORT" + } +} diff --git a/research/productive-helper-inverse-support/SOURCES.json b/research/productive-helper-inverse-support/SOURCES.json new file mode 100644 index 0000000000..0aeff761b2 --- /dev/null +++ b/research/productive-helper-inverse-support/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-inverse-support/TASK.json b/research/productive-helper-inverse-support/TASK.json new file mode 100644 index 0000000000..2458779a1f --- /dev/null +++ b/research/productive-helper-inverse-support/TASK.json @@ -0,0 +1,84 @@ +{ + "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 support obstructions for one source-consuming encoder: a cold-basis inverse identity and a stronger main-input obstruction for every ascending pure-scalar realization of the nominated whole-encoder map with the retained suffix.", + "scope_change_reason": "Explicit user assignment is productive-helper/native co-optimization. An attractive one-dimensional native input led to an algorithm-independent obstruction rather than an improved paid profile.", + "bottleneck_link": "A lower apparent native-input chart is useful only when preserving all dirty inputs and the suffix costs. The certificate eliminates a whole misleading family before scalar synthesis.", + "budget_minutes": 90, + "stop_rule": "Stop every ascending scalar realization of the nominated whole-encoder map with either declared retained suffix. Any subsequent construction must change an explicit hypothesis and pass a fully charged optimistic budget. User research cutoff is30percent usage remaining.", + "outcome": "completed", + "evidence": "PROOF.md; exact local and whole-encoder inverse identities, cold annihilator, main51 coefficient, rebuilt suffix caps and terminal paths, original-source positive control and sixteen corruption controls in verify.py.", + "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 undoing the temporary T basis immediately after the common paired natives enable an inexpensive encoder?", + "why_it_matters": "It changes the suffix contact graph and therefore the hypotheses of both support obstructions.", + "first_step": "For this explicit changed suffix, rebuild the forward and inverse support caps, then synthesize only if all necessary constraints and a fully charged optimistic budget pass.", + "blocked_by": "A concrete ascending encoder, all632 arbitrary-input endpoints in both orientations, native admission and a favorable complete paid-minus-helper invoice. Passing support gates alone is insufficient." + }, + { + "question": "Can a changed suffix dependency or a priced nonmonotone circuit make the extracted native slot useful?", + "why_it_matters": "The exact terminal paths retain the obstructing chart caps even when every native map and helper final chart is released.", + "first_step": "Name and change a particular scalar contact path or supply a fully charged contraction budget, then rerun the forward and inverse support checks.", + "blocked_by": "Exact arbitrary-input endpoints in both orientations, native physical admission, and a favorable whole-call invoice." + } + ], + "coordination": { + "upstream_checkpoint": "7c472563474e60185e6ca101a17622133d047e56", + "priority_and_selected_changed": false, + "predecessors": "PR5301 and PR5324 are now archived on canonical main; their scientific review remains open. This is a new scalar-factorization obstruction, not a repetition of their finite chart family or fixed-height theorem.", + "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-23T19:17:53Z", + "most_recently_updated_prs": 100, + "oldest_updated": "2026-10-23T16:25:41Z", + "finding": "No duplicate of the exact cold-basis annihilator or457-role extension found; limited recent coverage, not a proof of novelty. Earlier discussion checks1163/1166/5125 retained from this research round." + } + } +} diff --git a/research/productive-helper-inverse-support/VERIFY.json b/research/productive-helper-inverse-support/VERIFY.json new file mode 100644 index 0000000000..7ef16a5494 --- /dev/null +++ b/research/productive-helper-inverse-support/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 local and whole scalar-encoder inverse/annihilator identities, stronger main-input support obstruction, original-source positive control, both suffix orientations/variants, explicit native-free terminal paths and sixteen corruption controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact local and whole scalar-encoder inverse/annihilator identities, stronger main-input support obstruction, original-source positive control, both suffix orientations/variants, explicit native-free terminal paths and sixteen corruption controls." + } + ] +} diff --git a/research/productive-helper-inverse-support/check.py b/research/productive-helper-inverse-support/check.py new file mode 100644 index 0000000000..7952ce3447 --- /dev/null +++ b/research/productive-helper-inverse-support/check.py @@ -0,0 +1,575 @@ +#!/usr/bin/env python3 +"""Exact cold-basis inverse-support obstruction; Python standard library only. + +Apache-2.0. Substantial OpenAI Codex assistance. The commuting-ADD +coalescer is adapted, with credit, from Cinna Davis's +research/scalar-trace-compression/verify.py (PR4692). Its crossed +instructions are independently checked here before each merge. + +The source matrix, quotient, annihilator and suffix graphs are rebuilt +from the integrated combined word. No discovery compiler, matrix fixture, +numerical optimizer, native-suite execution or network access is used. +""" +from copy import deepcopy +from fractions import Fraction as Q +from hashlib import sha256 +from pathlib import Path +import argparse +import gzip +import json + +HERE = Path(__file__).resolve().parent +SOURCE = HERE.parent / 'productive-helper-fusion-certificate/COMBINED-WORD.json.gz' +SOURCE_SHA256 = 'aa4a8241da76abd2c06e6576a3ac09e77781321deaac3ad7d3ce4519342a36e6' +LO, HI = 9961, 10111 +PAIRED = (417, 419) +TARGETS = (78, 99, 431) +EXPECTED_CAPS = {78: [25, 45, 462], 99: [45, 76, 411], 431: [45, 76]} + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')).encode() + + +def digest(value): + return sha256(canonical(value)).hexdigest() + + +def read_source(path=SOURCE): + return json.loads(gzip.decompress(Path(path).read_bytes())) + + +def span(vectors): + values = {0} + for vector in vectors: + values |= {x ^ vector for x in tuple(values)} + return frozenset(values) + + +def basis(values): + result, seen = [], {0} + for vector in sorted(values): + if vector not in seen: + result.append(vector) + seen |= {x ^ vector for x in tuple(seen)} + return result + + +def ident(n): + return [[Q(i == j) for j in range(n)] for i in range(n)] + + +def mul(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 inverse(a): + n = len(a) + rows = [list(row) + unit for row, unit in zip(a, ident(n))] + for column in range(n): + pivot = next((r for r in range(column, n) if rows[r][column]), None) + need(pivot is not None, 'singular rational matrix') + rows[pivot], rows[column] = rows[column], rows[pivot] + scale = rows[column][column] + rows[column] = [x / scale for x in rows[column]] + for r in range(n): + if r != column: + scale = rows[r][column] + rows[r] = [x - scale * y for x, y in zip(rows[r], rows[column])] + result = [row[n:] for row in rows] + need(mul(a, result) == mul(result, a) == ident(n), 'two-sided rational inverse') + return result + + +def refs(event): + if event[0] == 'scalar': + g = event[1] + return g[1:3] if g[0] in ('add', 'copy') else g[1:2] + if event[0] == 'warp': + return [event[1]] + return [] + + +def add(dst, src, coefficient, frame): + coefficient = Q(coefficient) + return ['scalar', ['add', list(dst), list(src), coefficient.numerator, coefficient.denominator], frame] + + +def scale(dst, coefficient, frame): + coefficient = Q(coefficient) + return ['scalar', ['scale', list(dst), coefficient.numerator, coefficient.denominator], frame] + + +def scalar_matrix(events, roles): + index = {r: i for i, r in enumerate(roles)} + rows = ident(len(roles)) + for event in events: + need(event[0] == 'scalar' and all(t == 'L' and r in index for t, r in refs(event)), + 'pure persistent local scalar circuit') + g = event[1] + i = index[g[1][1]] + if g[0] == 'add': + j, c = index[g[2][1]], Q(*g[3:5]) + need(i != j, 'distinct ADD roles') + rows[i] = [x + c * y for x, y in zip(rows[i], rows[j])] + elif g[0] == 'scale': + c = Q(*g[2:4]) + need(bool(c), 'invertible scalar SCALE') + rows[i] = [c * x for x in rows[i]] + else: + raise ValueError('noninvertible local scalar operation') + return rows + + +def local_boundaries(payload, program): + current = payload['canonical']['start'][:] + entrance = None + for ordinal, event in enumerate(program): + if ordinal == LO: + entrance = current[:] + if ordinal == HI: + need(entrance is not None, 'local source boundaries') + return entrance, current + if event[0] == 'scalar': + for typ, role in refs(event): + if typ == 'L': + current[role] = event[2] + elif event[0] == 'warp': + current[event[1][1]] = event[4] + raise ValueError('missing local source interval') + + +def annihilator(alpha, dinv, index, cold, terms=((78, Q(-1)), (431, Q(1, 2)))): + need(any(alpha.values()), 'nonzero compensation vector') + for role in cold: + need(alpha[role] == sum(coef * dinv[index[role]][index[column]] for column, coef in terms), + 'cold-projected annihilator identity') + + +def local_model(payload): + program = [e for e in payload['programs']['forward'] if e[0] != 'climb'] + need(program[6262] == ['phase', 'A'] and program[10315] == ['phase', 'centers'], 'source phase bounds') + segment = program[LO:HI] + roles = sorted({r for e in segment for t, r in refs(e)}) + need(roles == [13, 16, 43, 44, 51, 78, 99, 104] + list(range(416, 432)), 'exact24 local roles') + n, index = len(roles), {r: i for i, r in enumerate(roles)} + matrix = scalar_matrix(segment, roles) + transformed = deepcopy(matrix) + a, b = matrix[index[417]], matrix[index[419]] + transformed[index[417]] = [x / 2 - y for x, y in zip(a, b)] + transformed[index[419]] = [x / 2 + y for x, y in zip(a, b)] + transformed[index[416]], transformed[index[417]] = transformed[index[417]], transformed[index[416]] + need(transformed[index[416]] == [Q(r in (13, 416)) for r in roles], 'reserved row is entry13 plus dirty entry416') + # S=P*T*M*E^-1, E:416+=13. Right multiplication subtracts + # column416 from column13, and makes row416 an identity row. + schur = deepcopy(transformed) + for row in schur: + row[index[13]] -= row[index[416]] + need(schur[index[416]] == ident(n)[index[416]], 'S fixes reserved carrier') + sinv = inverse(schur) + alpha = {r: -sinv[index[r]][index[416]] for r in roles if r != 416} + dbase = deepcopy(schur) + for i in range(n): + dbase[i][index[416]] = Q(i == index[416]) + dinv = inverse(dbase) + lower = ident(n) + for r, c in alpha.items(): + lower[index[r]][index[416]] = c + need(mul(dbase, lower) == schur, 'exact block-LU factorization') + entrance, exits = local_boundaries(payload, program) + frames = payload['canonical']['frames'] + cold = [r for r in roles if r != 416 and entrance[r] == 0] + need(cold == list(range(417, 432)), 'fifteen cold outside inputs') + need(frames[entrance[416]] == [] and frames[entrance[13]] == [73], 'E prefix availability') + need(all(not c for r, c in alpha.items() if r not in cold), 'all compensation supported on cold inputs') + annihilator(alpha, dinv, index, cold) + need(all(payload['canonical']['start'][r] == 0 and payload['canonical']['final'][r] == 1 + for r in (416, 417, 419)), 'nominated helper endpoint contracts') + return {'roles': roles, 'index': index, 'cold': cold, 'alpha': alpha, + 'D_inverse': dinv, 'entrance': entrance, 'exits': exits, + 'matrix_hash': digest([[str(x) for x in row] for row in matrix]), + 'quotient_hash': digest([[str(x) for x in row] for row in dbase])} + + +def native_binding(payload): + maps = {w['op']: w['G_columns'] for w in payload['canonical']['warps']} + need(maps[34] == maps[35], 'paired full native maps equal') + result = {} + for direction, raw in payload['programs'].items(): + program = [e for e in raw if e[0] != 'climb'] + uses = [(i, e) for i, e in enumerate(program) if e[0] == 'warp' and e[1][1] in (416, 417, 419)] + need([i for i, e in uses] == [11491, 11492, 13455, 13456], 'complete paired native census') + need([e[2] for i, e in uses] == [34, 35, -35, -34], 'paired positive/inverse operator order') + for (i, e), (j, f) in (uses[:2], uses[2:]): + need(j == i + 1 and e[3:] == f[3:], 'adjacent equal-chart native block') + need(not any(e[0] == 'adapter' and e[2] in (416, 417, 419) for e in program), 'no nominated helper adapter') + result[direction] = [{'source_ordinal': i, 'op': e[2], 'role': e[1][1]} for i, e in uses] + return result + + +def emit_two(matrix, frame): + """Deterministic two-row Gaussian factorization, checked exactly.""" + a, operations = deepcopy(matrix), [] + + def row_add(i, j, c): + if c: + operations.append(('add', i, j, c)) + a[i] = [x + c * y for x, y in zip(a[i], a[j])] + + def row_scale(i, c): + if c != 1: + operations.append(('scale', i, c)) + a[i] = [c * x for x in a[i]] + + if not a[0][0]: + row_add(0, 1, Q(1)) + need(bool(a[0][0]), 'two-row first pivot') + row_scale(0, 1 / a[0][0]) + row_add(1, 0, -a[1][0]) + need(bool(a[1][1]), 'two-row second pivot') + row_scale(1, 1 / a[1][1]) + row_add(0, 1, -a[0][1]) + need(a == ident(2), 'two-row elimination') + events = [] + for operation in reversed(operations): + if operation[0] == 'add': + _, i, j, c = operation + events.append(add(['L', PAIRED[i]], ['L', PAIRED[j]], -c, frame)) + else: + _, i, c = operation + events.append(scale(['L', PAIRED[i]], 1 / c, frame)) + need(scalar_matrix(events, PAIRED) == matrix, 'exact emitted two-row matrix') + return events + + +def conjugate(event, a, ai): + if event[0] != 'scalar' or not any(t == 'L' and r in PAIRED for t, r in refs(event)): + return [deepcopy(event)] + g, frame = event[1:] + pair = [['L', r] for r in PAIRED] + if g[0] == 'add': + dst, src, c = g[1], g[2], Q(*g[3:5]) + if dst in pair and src in pair: + elementary = ident(2) + elementary[pair.index(dst)][pair.index(src)] += c + return emit_two(mul(mul(a, elementary), ai), frame) + if dst in pair: + j = pair.index(dst) + return [add(pair[i], src, c * a[i][j], frame) for i in range(2) if a[i][j]] + j = pair.index(src) + return [add(dst, pair[i], c * ai[j][i], frame) for i in range(2) if ai[j][i]] + need(g[0] == 'scale', 'invertible conjugated helper scalar') + elementary = ident(2) + elementary[pair.index(g[1])][pair.index(g[1])] = Q(*g[2:4]) + return emit_two(mul(mul(a, elementary), ai), frame) + + +def check_conjugation(event, emitted, a, ai): + """Check each changed scalar transfer on all its arbitrary input rows.""" + need(event[0] == 'scalar' and all(t == 'L' for t, r in refs(event)), 'paired helper has no owned scalar contact') + roles = sorted(set(PAIRED) | {r for t, r in refs(event)}) + index = {r: i for i, r in enumerate(roles)} + embedded, embedded_inverse = ident(len(roles)), ident(len(roles)) + for i, r in enumerate(PAIRED): + for j, s in enumerate(PAIRED): + embedded[index[r]][index[s]] = a[i][j] + embedded_inverse[index[r]][index[s]] = ai[i][j] + expected = mul(mul(embedded, scalar_matrix([event], roles)), embedded_inverse) + need(scalar_matrix(emitted, roles) == expected, 'exact conjugated scalar transfer') + + +def rename(event): + event = deepcopy(event) + for ref in refs(event): + if ref[0] == 'L' and ref[1] in (416, 417): + ref[1] = 833 - ref[1] + if event[0] == 'adapter' and event[2] in (416, 417): + event[2] = 833 - event[2] + return event + + +def dual(event): + event = deepcopy(event) + g = event[1] + if g[0] == 'add': + g[1], g[2], g[3] = g[2], g[1], -g[3] + else: + need(g[0] == 'scale', 'dual scalar kind') + g[2], g[3] = g[3], g[2] + return event + + +def make_suffix(payload, direction, cut=HI): + t = [[Q(1, 2), Q(-1)], [Q(1, 2), Q(1)]] + ti = inverse(t) + a, ai = (t, ti) if direction == 'forward' else (list(map(list, zip(*ti))), list(map(list, zip(*t)))) + program = [e for e in payload['programs'][direction] if e[0] != 'climb'] + events, provenance = [], [] + for ordinal in range(cut, len(program)): + emitted = conjugate(program[ordinal], a, ai) + if program[ordinal][0] == 'scalar' and any(t == 'L' and r in PAIRED for t, r in refs(program[ordinal])): + check_conjugation(program[ordinal], emitted, a, ai) + emitted = [rename(e) for e in emitted] + events.extend(emitted) + provenance.extend([ordinal] * len(emitted)) + # Undo B=P*T at the common full endpoint: P, then T^-1. + tail = [add(['L', 416], ['L', 417], 1, 1), add(['L', 417], ['L', 416], -1, 1), + add(['L', 416], ['L', 417], 1, 1), scale(['L', 417], -1, 1)] + tail += [add(['L', 417], ['L', 419], 1, 1), add(['L', 419], ['L', 417], Q(-1, 2), 1)] + if direction == 'backward': + tail = [dual(e) for e in tail] + binding = ident(3) + for i in range(2): + for j in range(2): + binding[i + 1][j + 1] = a[i][j] + binding[0], binding[1] = binding[1], binding[0] + need(mul(scalar_matrix(tail, (416, 417, 419)), binding) == ident(3), 'exact final B inverse') + events.extend(tail) + provenance.extend([None] * len(tail)) + return events, provenance + + +def live_add(event): + return event[0] == 'scalar' and event[1][0] == 'add' and all(t == 'L' for t, r in refs(event)) + + +def commute(add_event, other): + if other[0] == 'phase': + return False + a, b = map(tuple, add_event[1][1:3]) + if other[0] == 'scalar' and other[1][0] == 'add': + x, y = map(tuple, other[1][1:3]) + return a != y and b != x + if other[0] in ('scalar', 'warp'): + return not ({a, b} & set(map(tuple, refs(other)))) + need(other[0] in ('center', 'adapter'), 'known crossed marker') + return True + + +def combine(events, provenance): + """Credited PR4692 coalescer plus independent crossed-event checks.""" + out, origins, previous, writes, reads, barriers = [], [], {}, {}, {}, {} + phase, merges, cancellations, crossed = -1, 0, 0, 0 + for event, origin in zip(events, provenance): + index = len(out) + if live_add(event): + a, b = map(tuple, event[1][1:3]) + prior = previous.get((a, b), -1) + barrier = max(phase, writes.get(b, -1), reads.get(a, -1), barriers.get(a, -1), barriers.get(b, -1)) + if prior > barrier: + need(out[prior] is not None and out[prior][1][1:3] == event[1][1:3], 'merge endpoints') + for intermediate in out[prior + 1:]: + if intermediate is not None: + need(commute(event, intermediate), 'noncommuting merge crossing') + crossed += 1 + value = Q(*out[prior][1][3:5]) + Q(*event[1][3:5]) + merges += 1 + if value: + out[prior] = add(a, b, value, out[prior][2]) + else: + out[prior] = None + previous.pop((a, b)) + cancellations += 1 + continue + previous[a, b] = index + if event[0] == 'scalar' and event[1][0] == 'add': + a, b = map(tuple, event[1][1:3]) + writes[a], reads[b] = index, index + else: + for ref in refs(event): + barriers[tuple(ref)] = index + if event[0] == 'phase': + phase = index + out.append(deepcopy(event)) + origins.append(origin) + kept = [(e, o) for e, o in zip(out, origins) if e is not None] + return [e for e, o in kept], [o for e, o in kept], {'merges': merges, 'cancellations': cancellations, 'crossed_checks': crossed} + + +def suffix_graph(payload, events, provenance): + frames = list(map(span, payload['canonical']['frames'])) + nodes = [{'pin': None, 'kind': 'local_exit', 'role': r} for r in range(632)] + current, outgoing, edges = list(range(632)), [[] for _ in nodes], [] + + def node(pin, kind, role=None): + index = len(nodes) + nodes.append({'pin': pin, 'kind': kind, 'role': role}) + outgoing.append([]) + return index + + def move(role, target, ordinal): + edge = {'a': current[role], 'b': target, 'role': role, 'suffix_ordinal': ordinal} + outgoing[edge['a']].append(len(edges)) + edges.append(edge) + current[role] = target + + dropped = 0 + for ordinal, event in enumerate(events): + if event[0] == 'scalar': + references = refs(event) + owned = any(t != 'L' for t, r in references) + target = node(event[2] if owned else None, 'owned_contact' if owned else 'scalar') + for typ, role in references: + if typ == 'L': + move(role, target, ordinal) + elif event[0] == 'warp': + role = event[1][1] + move(role, node(None, 'native_input', role), ordinal) + current[role] = node(None, 'native_output', role) + dropped += 1 + else: + need(event[0] in ('phase', 'center', 'adapter'), 'known suffix event') + # All helper final charts are released. Only intrinsic main finals and + # actual owned contacts constrain this optimistic suffix relaxation. + for role, label in enumerate(payload['canonical']['final']): + move(role, node(label if role < 224 else None, 'main_final' if role < 224 else 'free_helper_final', role), len(events)) + full = frozenset(range(512)) + upper = [frames[n['pin']] if n['pin'] is not None else full for n in nodes] + distance = [0 if n['pin'] is not None and 73 not in frames[n['pin']] else float('inf') for n in nodes] + for edge in reversed(edges): + upper[edge['a']] &= upper[edge['b']] + distance[edge['a']] = min(distance[edge['a']], 1 + distance[edge['b']]) + return {'nodes': nodes, 'edges': edges, 'outgoing': outgoing, 'upper': upper, + 'distance': distance, 'frames': frames, 'events': events, 'provenance': provenance, + 'omitted_native_occurrences': dropped} + + +def witness(graph, role): + at, path = role, [] + while graph['nodes'][at]['pin'] is None or 73 in graph['frames'][graph['nodes'][at]['pin']]: + options = [i for i in graph['outgoing'][at] if 73 not in graph['upper'][graph['edges'][i]['b']]] + need(bool(options), 'excluded vector has a fixed suffix descendant') + chosen = min(options, key=lambda i: graph['distance'][graph['edges'][i]['b']]) + path.append(chosen) + at = graph['edges'][chosen]['b'] + result = {'local_exit_role': role, 'edge_ids': path, 'terminal_node': at} + validate_witness(graph, result) + return result + + +def validate_witness(graph, certificate): + at = certificate['local_exit_role'] + need(at in TARGETS and certificate['edge_ids'], 'nonempty nominated suffix witness') + for edge_id in certificate['edge_ids']: + need(type(edge_id) is int and 0 <= edge_id < len(graph['edges']), 'suffix edge range') + edge = graph['edges'][edge_id] + need(edge['a'] == at, 'continuous suffix paid path') + at = edge['b'] + need(at == certificate['terminal_node'], 'suffix terminal node') + terminal = graph['nodes'][at] + need(terminal['pin'] is not None and 73 not in graph['frames'][terminal['pin']], 'fixed suffix terminal excludes73') + + +def compact_witness(graph, certificate): + terminal = graph['nodes'][certificate['terminal_node']] + path = [graph['edges'][i] for i in certificate['edge_ids']] + return {'length': len(path), 'roles': [e['role'] for e in path], + 'suffix_ordinals': [e['suffix_ordinal'] for e in path], + 'source_ordinals': [graph['provenance'][e['suffix_ordinal']] if e['suffix_ordinal'] < len(graph['events']) else None for e in path], + 'terminal_kind': terminal['kind'], 'terminal_role': terminal['role'], + 'terminal_frame': terminal['pin'], 'terminal_basis': basis(graph['frames'][terminal['pin']])} + + +def check_suffix(payload, direction): + raw, origins = make_suffix(payload, direction) + coalesced, coalesced_origins, counts = combine(raw, origins) + graphs = {'uncoalesced': suffix_graph(payload, raw, origins), + 'coalesced': suffix_graph(payload, coalesced, coalesced_origins)} + result = {'coalescing': counts, 'variants': {}} + for name, graph in graphs.items(): + caps = {} + for role in TARGETS: + need(graph['upper'][role] == span(EXPECTED_CAPS[role]), 'exact greatest suffix cap') + need(73 not in graph['upper'][role], 'suffix cap excludes73') + certificate = witness(graph, role) + caps[str(role)] = {'basis': basis(graph['upper'][role]), + 'witness': compact_witness(graph, certificate)} + result['variants'][name] = {'scalar_event_count': sum(e[0] == 'scalar' for e in graph['events']), + 'suffix_event_count': len(graph['events']), + 'suffix_sha256': digest(graph['events']), + 'paid_incidences': len(graph['edges']), + 'omitted_native_occurrences': graph['omitted_native_occurrences'], + 'caps': caps} + return result, graphs + + +def verify(payload=None): + payload = read_source() if payload is None else payload + need(digest(payload) == SOURCE_SHA256, 'pinned combined source payload') + need(payload['canonical']['h'] == 9 and len(payload['canonical']['start']) == 632, 'source dimensions') + local = local_model(payload) + natives = native_binding(payload) + directions = {direction: check_suffix(payload, direction)[0] for direction in ('forward', 'backward')} + return {'status': 'PASS_SCOPED_INVERSE_SUPPORT_OBSTRUCTION', 'source_sha256': SOURCE_SHA256, + 'source_interval': [LO, HI], 'local_roles': local['roles'], + 'source_local_matrix_sha256': local['matrix_hash'], 'quotient_matrix_sha256': local['quotient_hash'], + 'cold_roles': local['cold'], 'alpha': {str(r): str(c) for r, c in local['alpha'].items() if c}, + 'annihilator': {'identity': 'alpha = -D^-1[:,78] + (1/2)D^-1[:,431] on cold coordinates', + 'columns': [78, 431], 'coefficients': ['-1', '1/2']}, + 'native_source_bindings': natives, 'directions': directions, + 'relaxations': ['all suffix native edges removed', 'all helper final pins removed', 'intermediate adapter pins omitted'], + 'scope': 'No invertible cold-helper basis Q with all beta=Q*alpha compensation performed as a prefix can be followed by a pure-scalar realization of DQ^-1 and either declared retained suffix whose paid canonical chart spaces only grow by inclusion. Distributed prefix compensation is included. Interleaved compensation, changed suffix contacts, nonmonotone paid transports and new multiplication bounds are not claimed.'} + + +def controls(payload=None): + payload = read_source() if payload is None else payload + local = local_model(payload) + _, graphs = check_suffix(payload, 'forward') + graph = graphs['coalesced'] + certificate = witness(graph, 78) + passed = [] + + def rejected(name, operation): + try: + operation() + except ValueError: + passed.append(name) + else: + raise ValueError('corruption control accepted: ' + name) + + bad = deepcopy(payload) + bad['canonical']['start'][0] = 0 + rejected('source_payload_changed', lambda: verify(bad)) + bad = deepcopy(payload) + program = [e for e in bad['programs']['forward'] if e[0] != 'climb'] + program[LO][1][3] *= -1 + rejected('source_local_coefficient_changed', lambda: local_model(bad)) + rejected('annihilator_sign_changed', lambda: annihilator(local['alpha'], local['D_inverse'], local['index'], local['cold'], ((78, Q(1)), (431, Q(1, 2))))) + bad_alpha = dict(local['alpha']) + bad_alpha[418] += 1 + rejected('compensation_coefficient_changed', lambda: annihilator(bad_alpha, local['D_inverse'], local['index'], local['cold'])) + bad = deepcopy(payload) + next(w for w in bad['canonical']['warps'] if w['op'] == 35)['G_columns'][0] ^= 2 + rejected('paired_native_map_changed', lambda: native_binding(bad)) + bad_certificate = deepcopy(certificate) + bad_certificate['edge_ids'] = bad_certificate['edge_ids'][1:] + rejected('suffix_path_edge_deleted', lambda: validate_witness(graph, bad_certificate)) + bad_graph = dict(graph) + bad_graph['nodes'] = deepcopy(graph['nodes']) + bad_graph['nodes'][certificate['terminal_node']]['pin'] = None + rejected('suffix_terminal_pin_removed', lambda: validate_witness(bad_graph, certificate)) + bad_graph = dict(graph) + bad_graph['frames'] = list(graph['frames']) + pin = graph['nodes'][certificate['terminal_node']]['pin'] + bad_graph['frames'][pin] = frozenset(range(512)) + rejected('suffix_terminal_contains73', lambda: validate_witness(bad_graph, certificate)) + return {'passed': passed, 'count': len(passed)} + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--source', type=Path, default=SOURCE) + parser.add_argument('--write', action='store_true', help='explicitly write CHECK-RESULT.json beside this checker') + args = parser.parse_args() + data = read_source(args.source) + result = verify(data) + result['controls'] = controls(data) + if args.write: + (HERE / 'CHECK-RESULT.json').write_text(json.dumps(result, indent=2, sort_keys=True) + '\n', encoding='utf-8') + print(json.dumps(result, indent=2, sort_keys=True)) diff --git a/research/productive-helper-inverse-support/check_main.py b/research/productive-helper-inverse-support/check_main.py new file mode 100644 index 0000000000..3694f3f53b --- /dev/null +++ b/research/productive-helper-inverse-support/check_main.py @@ -0,0 +1,201 @@ +#!/usr/bin/env python3 +"""One main-input support obstruction for the globally conjugated suffix. + +Apache-2.0. Substantial OpenAI Codex assistance. This strengthens the +prefix-only obstruction for the SAME retained B=P*T suffix. It does not +apply to a different suffix which undoes T immediately after the natives. +""" +from collections import deque +from copy import deepcopy +from fractions import Fraction as Q +from functools import lru_cache +from pathlib import Path +import argparse +import importlib.util +import json + +HERE = Path(__file__).resolve().parent +ROLE, VECTOR, EXPECTED = 51, 100, Q(1, 2) + + +@lru_cache(None) +def peer(name): + spec = importlib.util.spec_from_file_location('productive_main_' + name, HERE / (name + '.py')) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def source_column(payload): + whole = peer('check_whole') + program = [e for e in payload['programs']['forward'] if e[0] != 'climb'] + column = [Q(0)] * whole.N + column[ROLE] = 1 + result = whole.apply_vector(column, program[whole.LO:whole.HI]) + need(result[ROLE] == EXPECTED, 'required main51 coefficient is one half') + frames = whole.entry_frames(payload, program) + need(payload['canonical']['frames'][frames[ROLE]] == [VECTOR], 'main51 actual entry line100') + need(ROLE not in (416, 417, 419), 'B fixes nominated output role') + return program, frames, result[ROLE] + + +def forward_inverse_violations(matrix, inverse_matrix, entrance_spaces, graph): + """Every nonzero scalar dependency is checked, not just main51.""" + forward, backward = [], [] + for output, row in enumerate(matrix): + for input_role, coefficient in row.items(): + if coefficient and not entrance_spaces[input_role] <= graph['upper'][output]: + forward.append([input_role, output, str(coefficient)]) + for input_role, row in enumerate(inverse_matrix): + for output, coefficient in row.items(): + if coefficient and not entrance_spaces[input_role] <= graph['upper'][output]: + backward.append([input_role, output, str(coefficient)]) + return forward, backward + + +def path_to_excluding_pin(graph, role=ROLE, vector=VECTOR): + """Ordinary BFS on paid edges; no73-specific core witness is used.""" + queue = deque([role]) + previous = {role: None} + terminal = None + while queue: + node = queue.popleft() + pin = graph['nodes'][node]['pin'] + if pin is not None and vector not in graph['frames'][pin]: + terminal = node + break + for edge_id in graph['outgoing'][node]: + edge = graph['edges'][edge_id] + if edge['b'] not in previous: + previous[edge['b']] = edge_id + queue.append(edge['b']) + need(terminal is not None, 'main support has an excluding fixed descendant') + at, path = terminal, [] + while at != role: + edge_id = previous[at] + need(edge_id is not None, 'nonempty main witness predecessor') + path.append(edge_id) + at = graph['edges'][edge_id]['a'] + certificate = {'role': role, 'vector': vector, 'edges': list(reversed(path)), 'terminal': terminal} + validate_path(graph, certificate) + return certificate + + +def validate_path(graph, certificate): + at = certificate['role'] + need(at == ROLE and certificate['vector'] == VECTOR and certificate['edges'], 'nominated main witness') + for edge_id in certificate['edges']: + need(type(edge_id) is int and 0 <= edge_id < len(graph['edges']), 'main witness edge range') + edge = graph['edges'][edge_id] + need(edge['a'] == at, 'continuous main paid path') + at = edge['b'] + need(at == certificate['terminal'], 'main witness terminal identity') + pin = graph['nodes'][at]['pin'] + need(pin is not None and VECTOR not in graph['frames'][pin], 'main terminal excludes100') + + +def compact(graph, certificate): + core = peer('check') + terminal = graph['nodes'][certificate['terminal']] + path = [graph['edges'][i] for i in certificate['edges']] + return {'length': len(path), 'roles': [e['role'] for e in path], + 'suffix_ordinals': [e['suffix_ordinal'] for e in path], + 'source_ordinals': [graph['provenance'][e['suffix_ordinal']] if e['suffix_ordinal'] < len(graph['events']) else None for e in path], + 'terminal_kind': terminal['kind'], 'terminal_role': terminal['role'], + 'terminal_frame': terminal['pin'], 'terminal_basis': core.basis(graph['frames'][terminal['pin']])} + + +def verify(payload=None): + core, whole = peer('check'), peer('check_whole') + payload = core.read_source() if payload is None else payload + need(core.digest(payload) == core.SOURCE_SHA256, 'pinned main-support source') + program, entries, coefficient = source_column(payload) + matrix = whole.sparse_matrix(program[whole.LO:whole.HI]) + inverse_matrix = whole.sparse_matrix(program[whole.LO:whole.HI], True) + whole.identity_product(matrix, inverse_matrix) + whole.identity_product(inverse_matrix, matrix) + need(matrix[ROLE][ROLE] == coefficient, 'independent column/full-row coefficient agreement') + entrance_spaces = [core.span(payload['canonical']['frames'][label]) for label in entries] + + original = program[whole.HI:] + original_origins = list(range(whole.HI, len(program))) + original_graph = core.suffix_graph(payload, original, original_origins) + fwd, inv = forward_inverse_violations(matrix, inverse_matrix, entrance_spaces, original_graph) + need(not fwd and not inv, 'original encoder/original suffix positive control') + result = {'status': 'PASS_MAIN_SUPPORT_RETAINED_SUFFIX_OBSTRUCTION', + 'source_sha256': core.SOURCE_SHA256, 'encoder_interval': [whole.LO, whole.HI], + 'required_coefficient': {'input_role': ROLE, 'output_role': ROLE, 'value': str(coefficient), 'input_basis': [VECTOR]}, + 'B_fixes_output51': True, + 'positive_control': {'original_forward_support_checks': sum(map(len, matrix)), + 'original_inverse_support_checks': sum(map(len, inverse_matrix)), + 'forward_violations': len(fwd), 'inverse_violations': len(inv), + 'original_output51_cap': core.basis(original_graph['upper'][ROLE])}, + 'directions': {}} + for direction in ('forward', 'backward'): + raw, origins = core.make_suffix(payload, direction, cut=whole.HI) + combined, combined_origins, counts = core.combine(raw, origins) + variants = {} + for name, events, provenance in (('uncoalesced', raw, origins), ('coalesced', combined, combined_origins)): + graph = core.suffix_graph(payload, events, provenance) + need(graph['upper'][ROLE] == core.span([45, 76]) and VECTOR not in graph['upper'][ROLE], + 'retained output51 greatest cap excludes100') + certificate = path_to_excluding_pin(graph) + variants[name] = {'suffix_sha256': core.digest(events), + 'output51_cap': core.basis(graph['upper'][ROLE]), + 'witness100': compact(graph, certificate)} + result['directions'][direction] = {'coalescing': counts, 'variants': variants} + result['scope'] = ('With the actual scalar-A input charts, the required transfer H=P*T*M has a nonzero main51-to-main51 coefficient. ' + 'No pure-scalar realization whose paid canonical chart spaces grow by inclusion can feed either declared globally ' + 'B-conjugated suffix. This is independent of cold prefix choices and compensation interleaving. All suffix native ' + 'edges/helper-final/adapter pins are released. It does not cover a changed suffix, including transient T undone ' + 'immediately after the paired natives, or nonmonotone paid transports. No new bound is claimed.') + return result + + +def controls(payload=None): + core, whole = peer('check'), peer('check_whole') + payload = core.read_source() if payload is None else payload + raw, origins = core.make_suffix(payload, 'forward', cut=whole.HI) + events, provenance, _ = core.combine(raw, origins) + graph = core.suffix_graph(payload, events, provenance) + certificate = path_to_excluding_pin(graph) + passed = [] + + def rejected(name, operation): + try: + operation() + except ValueError: + passed.append(name) + else: + raise ValueError('main corruption control accepted: ' + name) + + bad = deepcopy(payload) + pure = [e for e in bad['programs']['forward'] if e[0] != 'climb'] + need(pure[9994] == ['scalar', ['add', ['L', 51], ['L', 13], -1, 2], 581], 'source main51 instruction') + pure[9994][1][3] *= -1 + rejected('required_main_coefficient_changed', lambda: source_column(bad)) + bad_path = deepcopy(certificate) + bad_path['edges'] = bad_path['edges'][1:] + rejected('main_witness_edge_omitted', lambda: validate_path(graph, bad_path)) + bad_graph = dict(graph) + bad_graph['frames'] = list(graph['frames']) + pin = graph['nodes'][certificate['terminal']]['pin'] + bad_graph['frames'][pin] = frozenset(range(512)) + rejected('main_terminal_admits100', lambda: validate_path(bad_graph, certificate)) + return {'count': len(passed), 'passed': passed} + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true') + args = parser.parse_args() + result = verify() + result['controls'] = controls() + if args.write: + (HERE / 'MAIN-CHECK-RESULT.json').write_text(json.dumps(result, indent=2, sort_keys=True) + '\n', encoding='utf-8') + print(json.dumps(result, indent=2, sort_keys=True)) diff --git a/research/productive-helper-inverse-support/check_whole.py b/research/productive-helper-inverse-support/check_whole.py new file mode 100644 index 0000000000..2c3ad1a863 --- /dev/null +++ b/research/productive-helper-inverse-support/check_whole.py @@ -0,0 +1,250 @@ +#!/usr/bin/env python3 +"""Whole scalar-A encoder extension of the cold inverse-support certificate. + +Apache-2.0. Substantial OpenAI Codex assistance. The three required inverse +columns are replayed directly as632-entry vectors. Independently, sparse +forward/inverse matrices are reconstructed and both full identity products +are checked. No dense inversion, optimizer or discovery fixture is used. +""" +from copy import deepcopy +from fractions import Fraction as Q +from functools import lru_cache +from pathlib import Path +import argparse +import importlib.util +import json + +HERE = Path(__file__).resolve().parent +LO, HI, N = 6347, 10315, 632 + + +@lru_cache(None) +def core(): + spec = importlib.util.spec_from_file_location('productive_inverse_support_core', HERE / 'check.py') + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def instruction(event): + need(event[0] == 'scalar', 'whole interval is pure scalar') + g = event[1] + need(g[1][0] == 'L' and 0 <= g[1][1] < N, 'persistent scalar target') + if g[0] == 'add': + need(g[2][0] == 'L' and 0 <= g[2][1] < N and g[1] != g[2], 'distinct persistent scalar source') + return 'add', g[1][1], g[2][1], Q(*g[3:5]) + need(g[0] == 'scale' and Q(*g[2:4]) != 0, 'invertible scalar scale') + return 'scale', g[1][1], None, Q(*g[2:4]) + + +def apply_vector(vector, program, backwards=False): + result = list(vector) + for event in reversed(program) if backwards else program: + kind, dst, src, coefficient = instruction(event) + if kind == 'add': + result[dst] += (-coefficient if backwards else coefficient) * result[src] + else: + result[dst] *= 1 / coefficient if backwards else coefficient + return result + + +def pull_row(functional, program): + """Compute a row of M by backward propagation of its output weights.""" + row = list(functional) + for event in reversed(program): + kind, dst, src, coefficient = instruction(event) + if kind == 'add': + row[src] += coefficient * row[dst] + else: + row[dst] *= coefficient + return row + + +def accumulate(target, source, coefficient): + for column, value in source.items(): + value = target.get(column, Q(0)) + coefficient * value + if value: + target[column] = value + else: + target.pop(column, None) + + +def sparse_matrix(program, backwards=False): + rows = [{i: Q(1)} for i in range(N)] + for event in reversed(program) if backwards else program: + kind, dst, src, coefficient = instruction(event) + if kind == 'add': + accumulate(rows[dst], rows[src], -coefficient if backwards else coefficient) + else: + coefficient = 1 / coefficient if backwards else coefficient + rows[dst] = {j: coefficient * value for j, value in rows[dst].items()} + return rows + + +def identity_product(a, b): + for i, row in enumerate(a): + result = {} + for j, coefficient in row.items(): + accumulate(result, b[j], coefficient) + need(result == {i: Q(1)}, 'full632 sparse inverse product') + + +def entry_frames(payload, program): + current = payload['canonical']['start'][:] + for event in program[:LO]: + if event[0] == 'scalar': + for typ, role in core().refs(event): + if typ == 'L': + current[role] = event[2] + elif event[0] == 'warp': + current[event[1][1]] = event[4] + return current + + +def validate_cold(payload, frames, cold): + actual = [r for r, label in enumerate(frames) if r != 416 and not payload['canonical']['frames'][label]] + need(cold == actual, 'complete actual cold-role census') + need(len(cold) == 457, 'source whole-encoder cold count') + + +def check_identity(alpha, column78, column431, cold): + need(any(alpha), 'nonzero whole-encoder compensation') + for role in cold: + need(alpha[role] == -column78[role] + column431[role] / 2, 'whole cold-projected annihilator') + + +def model(payload): + m = core() + program = [e for e in payload['programs']['forward'] if e[0] != 'climb'] + phase = program.index(['phase', 'A']) + need(program.index(['phase', 'centers']) == HI + and 1 + max(i for i in range(phase, HI) if program[i][0] == 'warp') == LO, + 'whole scalar encoder starts after last A prelude and ends before centers') + segment = program[LO:HI] + for event in segment: + instruction(event) + frames = entry_frames(payload, program) + need(payload['canonical']['frames'][frames[416]] == [] + and payload['canonical']['frames'][frames[13]] == [73], 'whole E prefix availability') + cold = [r for r, label in enumerate(frames) if r != 416 and not payload['canonical']['frames'][label]] + validate_cold(payload, frames, cold) + + functional = [Q(0)] * N + functional[417], functional[419] = Q(1, 2), Q(-1) + wanted = [Q(r in (13, 416)) for r in range(N)] + need(pull_row(functional, segment) == wanted, 'whole reserved value entry13 plus dirty entry416') + + forward = sparse_matrix(segment) + backward = sparse_matrix(segment, True) + identity_product(forward, backward) + identity_product(backward, forward) + selected = {} + for column in (416, 78, 431): + seed = [Q(0)] * N + # T^-1*P*e416=e417-e419/2; the other two columns are unchanged. + if column == 416: + seed[417], seed[419] = Q(1), Q(-1, 2) + else: + seed[column] = Q(1) + inverse_column = apply_vector(seed, segment, True) + need(apply_vector(inverse_column, segment) == seed, 'selected inverse-column forward round trip') + need(apply_vector(apply_vector(seed, segment), segment, True) == seed, 'selected inverse-column backward round trip') + independent_column = [sum(value * seed[j] for j, value in row.items()) for row in backward] + need(inverse_column == independent_column, 'vector and full-matrix inverse-column agreement') + inverse_column[416] += inverse_column[13] # Left multiplication by E. + need(inverse_column[416] == Q(column == 416), 'reserved inverse row on selected columns') + selected[column] = inverse_column + alpha = [-x if i != 416 else Q(0) for i, x in enumerate(selected[416])] + need(all(not value or r in cold for r, value in enumerate(alpha)), 'whole compensation only on cold inputs') + check_identity(alpha, selected[78], selected[431], cold) + expected_alpha = {418: Q(1, 2), 419: Q(1, 2), 420: Q(1, 2), 421: Q(1, 2), + 425: Q(1, 2), 430: Q(-1, 2), 431: Q(-1, 2)} + need({r: value for r, value in enumerate(alpha) if value} == expected_alpha, 'exact whole alpha support') + need(all(backward[416].get(j, Q(0)) + backward[13].get(j, Q(0)) + == (Q(1, 2) if j == 417 else Q(-1) if j == 419 else Q(0)) for j in range(N)), + 'full reserved inverse row before right T inverse P') + return {'frames': frames, 'cold': cold, 'alpha': alpha, 'columns': selected, + 'forward_nnz': sum(map(len, forward)), 'inverse_nnz': sum(map(len, backward))} + + +def suffix(payload, direction): + m = core() + events, provenance = m.make_suffix(payload, direction, cut=HI) + combined, combined_origins, counts = m.combine(events, provenance) + result = {'coalescing': counts, 'variants': {}} + for name, word, origins in (('uncoalesced', events, provenance), ('coalesced', combined, combined_origins)): + graph = m.suffix_graph(payload, word, origins) + caps = {} + for role in m.TARGETS: + need(graph['upper'][role] == m.span(m.EXPECTED_CAPS[role]), 'whole-A greatest suffix cap') + certificate = m.witness(graph, role) + caps[str(role)] = {'basis': m.basis(graph['upper'][role]), 'witness': m.compact_witness(graph, certificate)} + result['variants'][name] = {'suffix_event_count': len(word), 'suffix_sha256': m.digest(word), + 'omitted_native_occurrences': graph['omitted_native_occurrences'], + 'caps': caps} + return result + + +def verify(payload=None): + m = core() + payload = m.read_source() if payload is None else payload + need(m.digest(payload) == m.SOURCE_SHA256, 'pinned whole-encoder source') + data = model(payload) + m.native_binding(payload) + return {'status': 'PASS_WHOLE_SCALAR_ENCODER_INVERSE_SUPPORT', 'source_sha256': m.SOURCE_SHA256, + 'source_interval': [LO, HI], 'scalar_events': HI - LO, 'arbitrary_input_roles': N, + 'both_full632_inverse_products': True, 'selected_inverse_columns': [416, 78, 431], + 'independent_vector_column_round_trips': True, + 'forward_matrix_nonzeros': data['forward_nnz'], 'inverse_matrix_nonzeros': data['inverse_nnz'], + 'cold_role_count': len(data['cold']), 'cold_main_role_count': sum(r < 224 for r in data['cold']), + 'cold_role_list_sha256': m.digest(data['cold']), + 'alpha': {str(r): str(c) for r, c in enumerate(data['alpha']) if c}, + 'annihilator': 'alpha = -D^-1[:,78] + (1/2)D^-1[:,431] on every actual cold entry role', + 'directions': {d: suffix(payload, d) for d in ('forward', 'backward')}, + 'scope': 'The same obstruction covers arbitrary invertible bases on all457 zero-chart persistent entry roles of the entire scalar-A interval, including cold main roles, with all compensation placed before its pure-scalar quotient. Paid canonical chart spaces must grow by inclusion through the declared retained suffix. Native edges, helper final pins and intermediate adapter pins are released. Interleaved compensation, changed suffix contacts, nonmonotone transports and a new bound remain outside the claim.'} + + +def controls(payload=None): + m = core() + payload = m.read_source() if payload is None else payload + data = model(payload) + passed = [] + + def rejected(name, action): + try: + action() + except ValueError: + passed.append(name) + else: + raise ValueError('whole corruption accepted: ' + name) + + bad = deepcopy(payload) + pure = [e for e in bad['programs']['forward'] if e[0] != 'climb'] + pure[9961][1][3] *= -1 + rejected('whole_source_compensation_value_changed', lambda: model(bad)) + rejected('whole_cold_role_omitted', lambda: validate_cold(payload, data['frames'], data['cold'][:-1])) + rejected('whole_noncold_main_role_added', lambda: validate_cold(payload, data['frames'], sorted(data['cold'] + [13]))) + wrong = list(data['columns'][78]) + wrong[418] += 1 + rejected('whole_inverse_column_coefficient_changed', lambda: check_identity(data['alpha'], wrong, data['columns'][431], data['cold'])) + corrupted_inverse = sparse_matrix([e for e in payload['programs']['forward'] if e[0] != 'climb'][LO:HI], True) + corrupted_inverse[0][0] = corrupted_inverse[0].get(0, Q(0)) + 1 + forward = sparse_matrix([e for e in payload['programs']['forward'] if e[0] != 'climb'][LO:HI]) + rejected('whole_full_inverse_product_corrupted', lambda: identity_product(forward, corrupted_inverse)) + return {'count': len(passed), 'passed': passed} + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true') + args = parser.parse_args() + result = verify() + result['controls'] = controls() + if args.write: + (HERE / 'WHOLE-CHECK-RESULT.json').write_text(json.dumps(result, sort_keys=True, indent=2) + '\n', encoding='utf-8') + print(json.dumps(result, sort_keys=True, indent=2)) diff --git a/research/productive-helper-inverse-support/verify.py b/research/productive-helper-inverse-support/verify.py new file mode 100644 index 0000000000..62a55ed8b3 --- /dev/null +++ b/research/productive-helper-inverse-support/verify.py @@ -0,0 +1,55 @@ +#!/usr/bin/env python3 +"""Read-only exact replay, with an explicit receipt authoring option.""" +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 load(name): + spec = importlib.util.spec_from_file_location(name, HERE / (name + '.py')) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def run(): + sources = json.loads((HERE / 'SOURCES.json').read_bytes()) + inputs = [row for row in sources['files'] if row['usage'] == 'input'] + need(len(inputs) == 1, 'one pinned scientific source') + for row in inputs: + data = (REPO / row['path']).read_bytes() + need(hashlib.sha256(data).hexdigest() == row['sha256'], 'live source byte hash') + local, whole, main = load('check'), load('check_whole'), load('check_main') + payload = local.read_source() + result = {'status': 'PASS_PRODUCTIVE_HELPER_INVERSE_SUPPORT', + 'local': local.verify(payload), 'whole_encoder': whole.verify(payload), + 'main_support': main.verify(payload), + 'controls': {'local': local.controls(payload), 'whole_encoder': whole.controls(payload), + 'main_support': main.controls(payload)}} + need(sum(r['count'] for r in result['controls'].values()) == 16, 'all sixteen controls ran') + return result + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true', help='explicitly replace RESULT.json with this fresh replay') + 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 proof result matches committed receipt') + print(json.dumps({'status': result['status'], 'cold_roles_local': len(result['local']['cold_roles']), + 'cold_roles_whole_encoder': result['whole_encoder']['cold_role_count'], + 'corruption_controls': 16, 'new_bound': False}, sort_keys=True))