Prove the nonlinear boundary of the abelian no-phase reduction (no new κ)

research/no-phase-nonlinear-boundary/README.md

@@ -0,0 +1,218 @@
+# The exact nonlinear boundary of the abelian no-phase reduction
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Scoped proof with finite corroboration. No new κ.** Let `V = C^(F_2^m)`,
+`m >= 1`, and let `X_v e_x = e_(x+v)`. Put
+
+```
+a = (1+i)/2, b = (1-i)/2, C_v = a I + b X_v,
+A = the group generated by the C_v for v != 0.
+```
+
+For an address permutation `p`, write `P e_x = e_p(x)`. Then
+
+```
+P A P^-1 = A  if and only if  p(x) = Mx + t for some invertible binary M.
+```
+
+Moreover, if `p` is nonlinear, **no abelian group containing `A` is normalized
+by `P`**. Thus enlarging the abelian call group cannot extend the same
+semidirect-product reduction to a nonlinear address permutation. Even the subgroup generated by `A` and `P A P^-1` is already nonabelian.
+
+The exhaustive three-bit census accepts exactly 1,344 of 40,320 permutations.
+It supplies a noncommutation witness for each of the other 38,976. Three bits
+is the first dimension with a nonlinear permutation: all two one-bit and all
+24 two-bit permutations are affine. The written theorem covers every `m`;
+the census covers only `m = 1,2,3`.
+
+## What this adds
+
+Jacob Alan Sussman's [PR #4628](https://github.com/CrocSwap/integer-mult-bounds/pull/4628),
+at `ee4fd87f064017c23e5a86fc1dcfe0a5237caed3`, proves a no-phase block-three
+bound by replacing linear address maps with copies of registers. Its
+[PROOF section 5](https://github.com/CrocSwap/integer-mult-bounds/blob/ee4fd87f064017c23e5a86fc1dcfe0a5237caed3/research/complex-small-m-lower-bounds/PROOF.md)
+uses the abelian call group and its semidirect product with a subgroup of
+`GL_3(F_2)`. That is a cited predecessor, not a result replayed here.
+
+This package identifies the exact address-permutation boundary of that
+reduction, proves the stronger obstruction to every abelian enlargement,
+and gives a literal Toffoli witness. It applies an elementary translation
+normalizer argument to this call-group contract. It does not claim that the
+abstract affine-normalizer argument is a new group-theoretic technique.
+Sussman's method and its eumemic #288 and Swapnil Jain P1/P2 lineage retain
+their credit. No predecessor code or numerical certificate is imported.
+
+This is a changed `complex-new-helper-inventory` scope. It settles one
+proof-method boundary for exploring nonlinear free address maps; it does not
+produce an improved supplier profile. In particular, it supplies no lower or
+upper tariff for a nonlinear no-phase program. Such programs may require a
+different, nonabelian representation or a different invariant. The selected
+κ = 60403/20000000 is unchanged.
+
+## Proof
+
+### 1. The call group contains all translations and lies in the convolution algebra
+
+Since `a^2+b^2=0` and `2ab=1`,
+
+```
+C_v^2 = X_v,   C_v^4 = I.
+```
+
+Every `C_v` is a polynomial in translations, so these calls commute and
+`A` is abelian. In particular, `A` contains the translation group
+`T = {X_v : v in F_2^m}` and lies in its convolution algebra
+
+```
+L = { sum_v k_v X_v : k_v in C }.
+```
+
+If an element of `L` is a literal permutation matrix, it is a translation.
+Indeed, its column at `y` is the translate by `y` of its column at zero.
+The latter must have exactly one coefficient equal to one and all others
+zero. Therefore
+
+```
+L intersect {address permutation matrices} = T,
+and consequently A intersect {address permutation matrices} = T.
+```
+
+### 2. Normalizing the call group forces an affine permutation
+
+Suppose `P A P^-1 = A`. Every `P X_v P^-1` is both a permutation matrix and
+an element of `A`, hence is a translation `X_phi(v)`. This defines an
+invertible additive map `phi` on `F_2^m`, because conjugation preserves
+products and is injective on `T`. Thus `phi(v)=Mv` for some invertible binary
+matrix `M`. Evaluating `P X_v P^-1 = X_(Mv)` at the address `p(0)` gives
+
+```
+p(v) = p(0) + Mv.
+```
+
+Conversely, if `p(x)=Mx+t`, then `P X_v P^-1=X_(Mv)` and
+`P C_v P^-1=C_(Mv)`. The nonzero directions are permuted bijectively, so
+`P A P^-1=A`. This proves both directions.
+
+Translations themselves are already free elements of `A`. An affine map is
+`X_t` followed by its linear map. The existing linear-map reduction can
+therefore absorb its translation part without a new call group.
+
+### 3. An abelian enlargement cannot repair a nonlinear permutation
+
+Let `B` be an abelian group of invertible operators with `A <= B` and
+`P B P^-1=B`. For every `v`, set `Q_v=P X_v P^-1`. Then `Q_v` belongs to
+`B` and commutes with every translation, since `T <= A <= B`.
+
+A permutation `q` commuting with every translation satisfies
+`q(x+v)=q(x)+v`. Taking `x=0` proves `q(v)=q(0)+v`, so it is itself a
+translation. Applying this to every `Q_v` makes `P` normalize `T`, and the
+argument in section 2 makes `p` affine. This contradicts nonlinearity.
+
+Equivalently, for every nonlinear `p`, there are `v,w` with
+
+```
+[P X_v P^-1, X_w] != I.
+```
+
+The same obstruction is present among the call roots. If
+`P C_v P^-1` and `C_w` commuted, their squares would commute; those squares
+are exactly the two displayed translations. This also proves that
+`<A, P A P^-1>` is nonabelian. No assumption about how a proposed larger
+abelian group is represented was used.
+
+### 4. The first nonlinear witness
+
+Use three-bit addresses `(x0,x1,x2)` and the Toffoli permutation
+
+```
+p(x0,x1,x2) = (x0,x1,x2+x0*x1).
+```
+
+It is an involution. With `Q=P X_e0 P^-1`, direct substitution gives
+
+```
+Q(x0,x1,x2) = (x0+1,x1,x2+x1),
+Q X_e1 Q^-1 X_e1^-1 = X_e2 != I.
+```
+
+The verifier checks this as a permutation identity. Separately it constructs
+`2 C_v` as eight-by-eight Gaussian-integer matrices, checks all seven
+identities `(2 C_v)^2=4 X_v`, and verifies that the literal matrices
+`P C_e0 P^-1` and `C_e1` do not commute.
+
+The obstruction persists under tensor powers of these permutation operators:
+a nontrivial permutation remains nontrivial on any positive tensor power.
+The theorem already concerns the one-column group required by the cited
+reduction. No inference from a finite-width test to a full multiplication
+algorithm is made.
+
+## Finite certificate and reproduction
+
+From the repository root, use CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/no-phase-nonlinear-boundary/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/no-phase-nonlinear-boundary
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/no-phase-nonlinear-boundary --check-source-history
+```
+
+The registered replay runs the verifier normally and with `-O`. Acceptance
+uses explicit exceptions, which remain active under optimization. For every
+permutation the conjugated translations are checked directly. Independently,
+all affine permutations are generated from independent binary matrix columns
+and translations, and the two sets are compared pointwise. Each rejected
+permutation gets a checked `(v,w,x)` noncommutation witness.
+
+The exact finite results are:
+
+```
+m=1:       2 permutations,    2 normalizers,     0 nonlinear witnesses
+m=2:      24 permutations,   24 normalizers,     0 nonlinear witnesses
+m=3:   40320 permutations, 1344 normalizers, 38976 nonlinear witnesses
+```
+
+The normalizer counts agree with the proved formula
+`2^m product_(j=0)^(m-1) (2^m-2^j)`.
+Four false-claim controls reject a changed count, an affine label on Toffoli,
+an erased commutator and an idempotent call-root claim. Each run prints
+`PASS_NO_PHASE_NONLINEAR_BOUNDARY` and a generated JSON report bound to SHA256
+hashes of the five package files. No receipt is hand-written.
+
+The historical card's first command was attempted once and stopped with
+`KeyError: 'complex_profile'` against the changed selected-record schema.
+That orientation failure is not scientific evidence and is not repaired here.
+The proof and verifier have no live dependency on the selected construction.
+No predecessor replay, Lean build, Docker run, physical caller, stock,
+precision, complete supplier or complete multiplication theorem is claimed.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Verification design
+
+All enumeration is bounded by the three-bit domain: at most 40,320
+permutations, seven directions, three basis shifts and eight addresses per
+witness search. Affine generation stores at most 1,344 eight-entry tuples.
+Matrices have eight rows and columns. Functions are below 60 physical lines;
+there is no recursion, generated code or external mathematical dependency.
+
+Python's managed allocation is a deviation from literal allocation-free
+operation. Its scope is this finite verifier; fixed domain bounds limit live
+collections, and permutations are streamed. The file-hash report reads only
+the five fixed package files, whose sizes are fixed by the committed artifact.
+The normal/optimized registered runs with warnings treated as errors are the
+diagnostics. No separate static type checker is a declared dependency.
+
+## Open next questions
+
+- Can a nonabelian replacement for the register-copy reduction yield a useful
+  no-phase lower bound with Toffoli maps? Start from the explicit subgroup
+  generated by `A` and `P A P^-1`, rather than treating it as abelian. A kept
+  space and a complete call/demand inequality remain missing.
+- Can a nonlinear no-phase program attain any of the small-unit shapes left
+  open by #4628? Start with one specified alphabet and one all-width target.
+  This normalizer obstruction neither excludes nor constructs such a program.
+
+See [TASK.json](TASK.json) for structured next questions and
+[SOURCES.json](SOURCES.json) for exact predecessor provenance. The canonical
+[claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19141393)
+records the bounded question.

research/no-phase-nonlinear-boundary/SOURCES.json

@@ -0,0 +1,43 @@
+{
+  "schema_version": 1,
+  "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4",
+  "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"
+    }
+  ],
+  "cited_predecessors": [
+    {
+      "pr": 4628,
+      "author": "Jacob Alan Sussman",
+      "commit": "ee4fd87f064017c23e5a86fc1dcfe0a5237caed3",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4628",
+      "usage": "Cited mathematical context only; not vendored or executed; proof here is self-contained.",
+      "files": [
+        {
+          "path": "research/complex-small-m-lower-bounds/README.md",
+          "git_blob": "764fe1ea7b6d31e39f802233fdaeb5514f4b4ab4",
+          "sha256": "565b38d373a333dec701839b71c485d27ec5c1383816a2e816f93f2883763069"
+        },
+        {
+          "path": "research/complex-small-m-lower-bounds/PROOF.md",
+          "git_blob": "46bccf74885682ca3e4bf97aea78d12770eec59c",
+          "sha256": "4a67f8ccb6284bf17389086bd00ff38c3d256fab4e69a184aade1a6ca33eb7fe"
+        }
+      ],
+      "retained_lineage": [
+        "eumemic / PR288",
+        "Swapnil Jain / P1 and P2"
+      ]
+    }
+  ]
+}

research/no-phase-nonlinear-boundary/TASK.json

@@ -0,0 +1,78 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-new-helper-inventory",
+  "priority_revision": 7,
+  "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4",
+  "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"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Classify address permutations normalizing the abelian no-phase call group and prove that nonlinear maps defeat every abelian enlargement.",
+  "scope_change_reason": "A self-contained side result on the algebraic boundary of PR4628 section 5, rather than a changed supplier profile or a replay of its bounds.",
+  "bottleneck_link": "Identifies when a register-copy reduction remains available for nonlinear-address exploration. It supplies no paid-profile improvement or physical admission.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the affine-normalizer theorem and first nonlinear witness after exact bounded verification; do not start a larger unit search.",
+  "outcome": "completed",
+  "evidence": "All-dimension written proof; exact permutation censuses at m=1,2,3; explicit Toffoli commutator and Gaussian-integer call roots; four rejection controls in normal and optimized Python.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a nonabelian replacement for the register-copy reduction yield a useful no-phase lower bound with Toffoli maps?",
+      "why_it_matters": "The proved obstruction excludes every abelian enlargement, while nonlinear programs remain possible.",
+      "first_step": "Construct the subgroup generated by A and P A P^-1 for the displayed Toffoli map and seek a kept space.",
+      "blocked_by": "No replacement kept-space or complete call/demand inequality is supplied."
+    },
+    {
+      "question": "Can a nonlinear no-phase program attain a small-unit shape left open by PR4628?",
+      "why_it_matters": "The reduction boundary does not determine actual word tariffs.",
+      "first_step": "Specify one nonlinear alphabet and an all-width target before searching.",
+      "blocked_by": "A full construction or a different lower-bound invariant remains missing."
+    }
+  ],
+  "claim_type": "scoped proof",
+  "environment": {
+    "python": "CPython 3.12.15",
+    "platform": "macOS arm64",
+    "dependencies": "standard library only"
+  }
+}

research/no-phase-nonlinear-boundary/VERIFY.json

@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Exhaust m=1,2,3, independently generate affine maps, verify every nonlinear commutation witness, literal Toffoli roots and four rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Repeat the exact certificate and rejection controls with assertions disabled."
+    }
+  ]
+}