Classify fixed nonlinear role recodings under exact ADD compatibility (no new κ)

research/nonlinear-role-recoding/PROOF.md

@@ -0,0 +1,176 @@
+# Rigidity of independent scalar-role recodings
+
+This scoped written proof was produced by Nick Petalas. Apache-2.0.
+The finite checker corroborates the statements; it is not their universal
+proof or a proof-kernel certificate.
+
+## 1. Exact contract
+
+Let F be any field. Let G be a finite directed graph with at least two
+vertices, no loops, and connected underlying undirected graph. An edge
+e=(j,i) means that role i is updated from the distinct role j. Assign a
+fixed coefficient b_e in F\{0} to each edge.
+
+For every vertex v choose a bijection f_v:F->F with f_v(0)=0. These maps
+are fixed throughout the program. The input to each gate ranges over all
+of F^2, including arbitrary dirty values. Let Phi act on a state by applying
+f_v to each scalar in role v. Require the conjugacy
+
+```text
+Phi ADD_{i<-j}(1) Phi^-1 = ADD_{i<-j}(b_e)                (1)
+```
+
+for every specified edge, where ADD_{i<-j}(b) updates x_i by b*x_j and
+preserves every other coordinate. Equivalently,
+
+```text
+f_i(x+y) = f_i(x) + b_e*f_j(y)  for every x,y in F.       (2)
+```
+
+The maps need not be continuous, measurable, differentiable or polynomial.
+Equation (2) is a gatewise requirement on independent values, not a finite
+trajectory test. An instruction graph records required gate compatibilities;
+its edges need not occur in every orientation or at every time.
+
+## 2. Classification
+
+**Theorem 1.** Equation (2) holds for every edge if and only if there are
+nonzero weights s_v in F and one additive bijection H:F->F such that
+
+```text
+f_v(z) = s_v*H(z),              b_(j,i) = s_i/s_j.        (3)
+```
+
+Choose a root r and normalize s_r=1. Then H=f_r and every s_v is unique.
+Equivalently, compatible maps exist exactly when the product of edge labels
+along every undirected closed walk is one. Reverse traversal uses b_e^-1.
+
+*Proof.* In (2) put x=0. Zero preservation gives f_i(y)=b_e*f_j(y).
+Substitution into (2) gives f_i(x+y)=f_i(x)+f_i(y). Thus f_i is additive,
+and f_j=b_e^-1*f_i is additive. Every vertex is incident with an edge,
+because the graph is connected and has at least two vertices.
+
+Starting at r, traverse any undirected path. The equality f_i=b_e*f_j
+gives f_v=s_v*f_r, with s_v equal to the product of b_e or b_e^-1 on that
+path. Each f_r is onto and nonzero, so two scalars multiplying f_r give the
+same function only when the scalars agree. Therefore path products are
+independent of the path; every closed-walk product is one. This proves
+necessity, uniqueness and (3).
+
+Conversely, closed-walk consistency defines the nonzero s_v by path
+products, and makes every edge label s_i/s_j. Choose any additive bijection
+H, for example the identity. Then
+
+```text
+s_i*H(x+y) = s_i*H(x) + (s_i/s_j)*s_j*H(y),
+```
+
+which is (2). This also proves the converse for every prescribed family
+of the form (3). A spanning tree suffices to compute the weights; each
+remaining edge is a scalar consistency check. No nonlinear search is needed.
+
+The characterization applies separately to every nontrivial connected
+component. An isolated vertex has no ADD constraint and may have an arbitrary
+zero-preserving bijection. Strong connectivity is unnecessary.
+
+## 3. One phase compatibility fixes the coefficient field
+
+Now let F=C. Suppose, in addition, that one role r satisfies the unchanged
+quarter-turn compatibility
+
+```text
+f_r(i*z) = i*f_r(z)  for every z in C.                   (4)
+```
+
+The role need not be the chosen root. From f_r=s_r*H and s_r!=0, (4)
+implies H(i*z)=i*H(z). Additivity implies integer homogeneity and rational
+homogeneity: n*H(z/n)=H(z) for every nonzero integer n. Hence
+
+```text
+H(a*z) = a*H(z)  for every a in Q(i).                  (5)
+```
+
+Thus H is Q(i)-linear. This is an algebraic conclusion; it does not assert
+complex linearity or that H is multiplication by a complex scalar.
+
+The distinction is real. On Q(i,sqrt(2)), the automorphism
+H(a+b*sqrt(2))=a-b*sqrt(2), a,b in Q(i), is Q(i)-linear and bijective,
+but is not multiplication by a scalar. A Q(i)-basis containing 1,sqrt(2)
+extends this to a Q(i)-linear bijection of C by fixing the other basis
+vectors. This existence example requires no computable encoding of arbitrary
+complex numbers, and is not a proposed physical operation.
+
+## 4. Consequence for Gaussian-dyadic native programs
+
+Apply f_v pointwise to the scalar entries of each finite role array.
+The same function is used at every address of that role. For every finite
+matrix M with entries in Q(i), (5) and additivity give
+
+```text
+H(M*x) = M*H(x),
+```
+
+where H acts entrywise. This includes Gaussian-dyadic coefficients and
+every finite tensor power of such a matrix. Multiplication by s_v also
+commutes with M within role v. Therefore every one-role native instruction
+M is unchanged by its role recoding f_v.
+
+**Corollary 2.** Consider a fixed exact word of unit ADDs and one-role
+Q(i)-matrix instructions. Suppose its ADD graph is connected, (1) holds,
+and one role has (4). Replace the recoding f_v by the scalar recoding
+z->s_v*z. The resulting recoded word has exactly the same native operators,
+the same scalar ADD coefficients b_e, the same chronology and the same
+all-input endpoint as with the original f_v.
+
+*Proof.* Theorem 1 gives the ADD coefficients. The preceding commutation
+identity gives the native operators. Thus the two conjugated words have
+identical instructions. Equivalently, if A is the original whole linear
+endpoint, D repeats s_v on every address of role v, and Phi is the nonlinear
+pointwise recoding, then
+
+```text
+Phi A Phi^-1 = D A D^-1.                                (6)
+```
+
+Indeed H commutes with A entrywise, since the finite whole endpoint is a
+Q(i)-matrix. This calculation also covers every finite array width and
+tensor multiplicity. It does not infer a uniform physical implementation
+from finite computations.
+
+In particular, arbitrary dirty restoration x_v->x_v remains restoration,
+zero owned fields remain zero, and all native paid labels are unchanged.
+Every recoded word in this class has a scalar-gauge counterpart with the
+same endpoint and native profile. Scalar gauges themselves are allowed
+recodings, so the sets of attainable endpoints/profiles are equal.
+
+This is a native-profile statement. Ordinary scalar coefficient costs,
+encoding/decoding, precision, storage and movement retain their own costs.
+If allowed coefficients are restricted, the counterpart uses exactly the
+same b_e as the proposed recoded word. Boundary weights do not become free
+physical instructions. No productive target or recursive invoice gain
+follows merely from the conjugacy.
+
+## 5. Boundaries and exact counterexamples
+
+- Without zero preservation, translations on a sink survive. Over F5, take
+  f_source(x)=x and f_target(x)=x+1. Equation (2) holds with b=1, but (3)
+  fails at zero. An affine version would require a separate statement.
+- Without connectedness, an isolated role can carry a nonadditive bijection.
+  Independent nontrivial components may also use different additive maps.
+- Additivity does not imply (4). Complex conjugation preserves ADD but sends
+  i to -i. Over F9, Frobenius x->x^3 gives a finite counterpart.
+- Phase compatibility does not imply additivity. The F9 checker enumerates
+  every zero-preserving permutation and supplies phase-only witnesses.
+- Pointwise recoding matters. Swapping two addresses is Q(i)-linear but
+  does not commute with the address operator diag(1,2).
+- Changing the recoding at different occurrences, changing a native
+  instruction, using input-dependent coefficients, approximate identities,
+  nonzero translations, or restricting reachable inputs changes the contract.
+  General nonlinear circuits and finite-grid rounded implementations are
+  outside the theorem.
+
+The shared-map scalar condition in Cinna Davis's PR #4983 is a predecessor,
+not a new claim here. The new application permits independent maps on every
+role and changed edge coefficients, then identifies their complete residual
+freedom and the Gaussian-native consequence. Cauchy's functional equation,
+spanning-tree gauge consistency and linear-map commutation are classical.

research/nonlinear-role-recoding/README.md

@@ -0,0 +1,132 @@
+# Independent nonlinear scalar-role recodings reduce to scalar gauges
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Claim type: scoped written obstruction, with exact finite corroboration.**
+Fixed arbitrary zero-preserving bijections on separate scalar roles add no
+native-profile freedom to the declared connected ADD/native interface.
+No continuity, measurability or differentiability is assumed.
+
+For a connected directed ADD graph, write an edge as source j to target i.
+Every family satisfying
+
+```text
+f_i(x+y) = f_i(x) + b_(j,i)*f_j(y)  for all independent x,y
+```
+
+has exactly the form f_v=s_v*H, with one common additive bijection H and
+b_(j,i)=s_i/s_j. Existence is equivalent to multiplicative consistency around
+every undirected closed walk. Reverse traversal uses the reciprocal label.
+The graph need only be weakly connected.
+
+If one role also preserves multiplication by i, H is Q(i)-linear. Applied
+pointwise, it commutes with every Gaussian-dyadic native matrix and all its
+finite tensor powers. For every fixed word in this gate class,
+
+```text
+Phi A Phi^-1 = D A D^-1,     D=diag(s_v),
+```
+
+with the weights repeated over each role's addresses. Thus every proposed
+nonlinear recoding has a scalar-gauge counterpart with the identical native
+operators, scalar ADD coefficients, chronology and endpoint, including dirty
+restoration. The native paid profiles attainable in the two classes are equal.
+Boundary adapters and ordinary scalar work retain their costs.
+
+[PROOF.md](PROOF.md) states and proves the universal classification and
+its exact contract. This identifies an escape route that cannot improve
+the current helper mechanism under unchanged gatewise compatibility. It does
+not exclude nonlinear arithmetic with a different instruction contract.
+
+## Evidence and reproduction
+
+The standalone checker imports no predecessor executable and writes only
+standard output. Its generated receipt hashes all six package files.
+It enumerates:
+
+- 5,632 map/label assignments over F3 on all 54 connected directed three-role
+  graphs. Exactly 432 satisfy the literal gate equations and the classification.
+- 1,105,920 map/label assignments over F5 on a directed path and directed
+  triangle, including every zero-preserving role permutation and every nonzero
+  edge label. Exactly 128 are compatible.
+- All 40,320 zero-preserving permutations of F9. There are 48 additive maps,
+  32 maps commuting with multiplication by i, and eight satisfying both.
+  Phase compatibility and additivity are independently necessary.
+- 48 complete seven-event word fixtures over Q(i,sqrt(2)), including all
+  24 rational basis columns and 24 mixed dirty inputs. A genuinely non-scalar
+  Q(i)-linear recoding gives the same 288 scalar outputs as direct scalar
+  gauges and the recoded gate word. These compare 1,152 rational components.
+- Nine graph/domain/ratio and hypothesis controls. The extension census also
+  supplies explicit phase-only and additive-but-not-phase witnesses.
+
+From the repository root, use CPython 3.12 with the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/nonlinear-role-recoding/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/nonlinear-role-recoding/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/nonlinear-role-recoding
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/nonlinear-role-recoding --check-source-history --check-modes
+```
+
+Any CPython 3.12 path may replace the local interpreter path. Expected markers
+are `PASS_NONLINEAR_ROLE_RECODING`, `PASS_REGISTERED_RESEARCH_PACKAGE` and
+`PASS_RESEARCH_COMMIT_BYTES`. The registered commands run the complete same
+finite domains in normal and optimized modes, each with a 60-second limit.
+The written proof, rather than these finite fields, establishes the result
+over C and every finite address width.
+
+## Scope and credit
+
+Cinna Davis's [PR #4983](https://github.com/CrocSwap/integer-mult-bounds/pull/4983)
+proves additivity for a shared frame potential commuting with unchanged ADDs
+and binds that condition to a source word. Its result and source audit are
+cited, not rechecked here. The new application classifies independent role
+maps and changed coefficients, then removes their nonlinear freedom from the
+Gaussian-native interface. Cauchy's functional equation, scalar gauge
+consistency and linear commutation are classical. No general literature
+priority is claimed for those methods.
+
+[SOURCES.json](SOURCES.json) pins the predecessor statements and assignment
+provenance at canonical main `19fdb086ea96af9a9f87936a2b888e10af4ed810`,
+priority revision 8. No scientific external input is executed. The selected
+source-binding orientation passed; it is not a supplier replay.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228562)
+records this original scope. The first classification ended the research.
+
+Maps are fixed per role, scalar, pointwise and zero-preserving; the equations
+hold on arbitrary independent values. One phase compatibility and connected
+ADD graph are explicit hypotheses. Occurrence-dependent maps, non-pointwise
+address operations, changed nonlinear gates, restricted reachable inputs,
+finite-grid rounding and approximate identities remain outside the claim.
+
+No physical encoding, source-specific paid deletion, complete signed invoice,
+precision bound, compiler/hosting admission, new kappa, selected-frontier
+change or complete multiplication theorem is supplied. Independent human
+and formal proof-kernel review are unclaimed. The five retained framework
+assumptions remain.
+
+## Verifier bounds and diagnostics
+
+All domains are fixed. The largest role-permutation table contains 24 maps;
+the F9 permutation iterator holds one eight-entry permutation at a time.
+There are at most 64 label tuples for one graph, and graph propagation uses
+exactly n edge scans. The native fixture contains three roles and two
+addresses per role, with four rational components per scalar. Every function
+is shorter than 60 physical lines, there is no recursion, and failures use
+exceptions that remain active under `-O`. Both modes enable warnings as errors.
+
+Power-of-ten managed-runtime deviation, rules 3 and 9: Python tuples,
+fractions, dictionaries and standard-library iterators allocate dynamically.
+The fixed domains above bound live data; there are no input-provided callbacks,
+subprocesses or external scientific files. Python does not provide a static
+fixed-allocation guarantee. Repository replay diagnostics cover the isolated
+package; no repository-wide analyzer configuration is changed.
+
+## Open next questions
+
+Can occurrence-dependent recodings improve a complete helper invoice? That
+changes the fixed-map hypothesis and could avoid this obstruction. Start with
+one pair of consecutive recodings, write the changed scalar/native instructions
+and every boundary adapter, then price restoration, storage and the complete
+signed bill. No such physical construction or bill is supplied here.
+The structured question is retained in [TASK.json](TASK.json).

research/nonlinear-role-recoding/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/coherent-frame-additivity/README.md",
+      "usage": "provenance",
+      "git_blob": "5c72c03ba7887aedad30acf4c20f40346da2fee5",
+      "sha256": "cf6889e806a9b4fa9a75beccefaa998627a9b35b77be529f0fe26718f60b9d67"
+    },
+    {
+      "path": "research/coherent-frame-additivity/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "67dd02c9d31d77be390a9e3fdfc09c7dd8de56c2",
+      "sha256": "0f72ad943e6f1803d6cdc5749f6b6880463fc8dba8ce57e8de3c3550a8eaea79"
+    }
+  ]
+}