Certify support obstructions for source-consuming productive helpers

research/productive-helper-inverse-support/.gitattributes

@@ -0,0 +1,3 @@
+*.py text eol=lf
+*.md text eol=lf
+*.json text eol=lf

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.

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.