Exclude every unequal three-helper k8 gauge improvement (no κ)

research/k8-unequal-triple-closure/PROOF.md

@@ -0,0 +1,161 @@
+# Unequal three-helper closure
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Statement and inherited contract
+
+Fix either final gauge vector of Philipp / mightyOil's
+[PR1322](https://github.com/CrocSwap/integer-mult-bounds/pull/1322), retained
+in `research/k8-coherent-triples/CERTIFICATE.json`. Fix its 237 eligible
+helpers and its original scalar ADD stream. Let k be that vector, with zero
+at all other registers. For an ADD with coefficient of absolute value
+p 2^e, where p is positive odd, put u=1 when p=1 and u=0 otherwise. Define
+
+```text
+f_u(z) = |z| - u [z=0]
+F(k) = 2 sum_h |k_h| + sum_ADD f_u(e + k_target - k_source).
+```
+
+The complete scalar tariff in PR1322 differs from F only by a constant.
+In particular the first term pays both boundary scales. This tariff and
+the eligibility/conjugation contract are cited premises, not new results.
+The original macro stream, coefficients, boundary contract and lowering
+alphabet remain fixed.
+
+**Theorem.** For every integer vector d supported on at most three of these
+helpers, in either orientation,
+
+```text
+F(k+d) - F(k) >= 8 sum_h max(0, |d_h|-3) >= 0.
+```
+
+Consequently every improving constant integer gauge move needs at least
+four changed helpers. This is a scoped computer-assisted negative proof,
+with an exact finite certificate, not a failed bounded search or a global
+optimum theorem. PR1322 previously established common-shift triple closure
+and explicitly left independently chosen shifts open. It did not assert
+arbitrary pair stationarity at its final vector.
+
+## A finite clipping certificate for an infinite domain
+
+An incident ADD at helper h has signed change +d_h at its target or -d_h
+at its source. At the fixed vector k record it as (u,E,sigma), where
+E=e+k_target-k_source and sigma is +1 or -1. Multiplicities are retained.
+Let I_h be this multiset, and let I_hb contain just the ADDs joining h and
+another eligible helper b. Define the outward unit difference
+
+```text
+V(J,x,s) = sum_(u,E,sigma in J)
+             [ f_u(E+sigma*x) - f_u(E+sigma*(x-s)) ],   s in {-1,+1}.
+
+D_h(x,s) = 2(|k_h+x|-|k_h+x-s|) + V(I_h,x,s).
+m_hb(s) = min_(z in Z) V(I_hb,z,s).
+loss_hb(x,s) = max(0, V(I_hb,x,s)-m_hb(s)).
+L_h(x,s) = D_h(x,s) - sum of the two largest loss_hb(x,s).
+```
+
+A missing largest loss is zero. Suppose d_h=x and at most two other
+helpers change. If such a neighbor b has displacement y, its actual pair
+contribution to the outward difference is V(I_hb,x-y,s), hence is at least
+m_hb(s). Unchanged neighbors contribute their baseline difference exactly.
+Subtracting the two largest nonnegative losses therefore gives a valid
+lower bound on the complete outward difference. It does not assume the
+two independently minimized pair contributions can be attained together.
+
+All minima and all tail inequalities above have finite exact checks. Set
+
+```text
+B_h = max(3, |k_h|, max_(u,E,sigma in I_h) |E|) + 2.
+```
+
+For fixed s, each V(I_hb,z,s) is constant on each integer tail outside
+[-B_h,B_h]. Both arguments of every f then stay strictly on one side of
+zero. Thus its minimum over all integers is attained in that finite
+interval. The same fact applies to D_h(x,s), every loss, and L_h(x,s) on
+the outward tail x=s*t, t>=B_h. The boundary absolute value also has
+constant difference there. Checking t=4,...,B_h covers every outward
+integer displacement beyond three.
+
+In each orientation the verifier checks all 1,540 resulting (h,s,t)
+rows. The least L_h is exactly 8. These are exact integer inequalities,
+including the point discount at exponent zero. Replacing that tariff by
+plain absolute value would be a different problem.
+
+Reduce each coordinate outside [-3,3] one step toward that interval.
+The support size never increases, and each step reduces F by at least
+8. After sum_h max(0,|d_h|-3) steps the resulting displacement d' is in
+[-3,3] and has support at most three. This proves
+
+```text
+F(k+d) - F(k+d') >= 8 sum_h max(0,|d_h|-3).
+```
+
+The remaining obligation is the bounded claim F(k+d')>=F(k).
+
+## Exact bounded decomposition and complete coverage
+
+Let S_h(a)=F(k+a e_h)-F(k). For every helper pair a<b, sum over its
+shared ADDs the correction
+
+```text
+C_ab(x,y) = sum [ f_u(E+sigma*(x-y))
+                 - f_u(E+sigma*x) - f_u(E-sigma*y) + f_u(E) ],
+```
+
+where sigma is +1 when a is the ADD target and -1 otherwise. Direct
+expansion gives, for every displacement on a set T,
+
+```text
+F(k+d)-F(k) = sum_(h in T) S_h(d_h)
+              + sum_(a<b in T) C_ab(d_a,d_b).
+```
+
+Boundary scales occur only in the singleton term. Shared ADDs are
+counted once after the correction. No source-independence assumption is
+needed for this identity of scalar costs.
+
+The undirected interaction graph joins helpers that share any ADD.
+There are 2,414 edges. Every connected triple has a length-two path, so
+generating every pair of neighbors of every vertex and deduplicating
+enumerates exactly its 49,898 connected triples. A separate enumeration
+classifies every three-helper subset by its three possible graph edges and
+confirms complete connected-triple coverage. The verifier visits
+all seven singleton values, all 49 independent pair values, and all 343
+independent values of each connected triple. In each orientation every
+singleton, pair and connected triple has minimum zero.
+
+The two-sided pair search covers all 27,966 pairs, including nonedges.
+A disconnected triple has components of size at most two. There is no
+shared ADD between components, so its cost difference is the sum of their
+nonnegative singleton/pair differences, even when their shifts differ.
+This covers all 2,190,670 three-helper subsets. Disconnected triples are
+counted by the separate graph enumeration; their shift assignments are
+discharged by the component argument rather than individual triple searches.
+
+The bounded minimum is therefore zero. Combining it with clipping proves
+the theorem. The zero displacement attains the lower bound zero; no
+uniqueness or strict local minimum is claimed.
+
+## Evidence and limits
+
+`verify.py` extracts the signed valuation graph directly from the retained
+archive and reads the final gauge vector as input. It imports no predecessor
+executable and runs no predecessor census, invoice or endpoint replay. SHA256
+pins authenticate both inputs. Its generated stdout receipt binds the package
+files, exact input hashes, clipping rows and ordered minimum streams.
+
+The finite certificate uses the Python standard library and exact integers.
+Forty synthetic graphs independently compare the decomposition with literal
+objective differences at all 343 displacement triples. Separate controls
+exercise the zero-exponent discount and both paid boundary scales. These
+tests corroborate the algebra; an unjustified-clipping fixture is rejected,
+and 32 actual-objective controls include displacements of magnitude 2^32.
+The clipping and disconnected-component arguments above justify the
+quantified domain.
+
+The theorem changes no circuit or recursive child. Four or more simultaneous
+changes, temporal gauges, a changed graph, new coefficients, a changed
+lowerer, native/owner integration, global precision, stock and tape costs
+are outside scope. The historical source is not the selected P104 supplier.
+No kappa improvement, supplier admission, complete multiplication theorem,
+independent human review or formal proof-kernel acceptance is claimed.

research/k8-unequal-triple-closure/README.md

@@ -0,0 +1,134 @@
+# Every improving PR1322 constant-gauge move needs four helpers
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Scoped computer-assisted negative proof with an exact finite certificate.**
+In both orientations, the final historical k8 gauge vector of
+[PR1322](https://github.com/CrocSwap/integer-mult-bounds/pull/1322) cannot
+improve under independently chosen integer shifts of any three eligible
+helpers. Every improving move in this fixed constant-gauge model must
+change at least four helpers. No new kappa is claimed.
+
+PR1322 proved closure for common shifts on triples and left unequal shifts
+open. It also left arbitrary pair stationarity at its final vector unclaimed.
+The new result closes both gaps. It cites the predecessor tariff and vector;
+it does not audit that contribution or rerun its scientific suite.
+
+## Result and evidence
+
+Write k for the retained vector and F for the complete scalar gauge
+objective, including both boundary scales and the unit-coefficient discount.
+For every integer displacement d with at most three changed helpers,
+
+```text
+F(k+d) - F(k) >= 8 sum_h max(0, |d_h|-3) >= 0.
+```
+
+[PROOF.md](PROOF.md) gives the clipping lemma, its exact finite premises,
+the singleton/pair decomposition and the disconnected-component argument.
+Each outward clipping step beyond magnitude three costs at least eight
+real-component primitives. This reduces the infinite domain to [-3,3]
+without relying on a solver's failure to find a witness.
+
+The standard-library verifier independently extracts the valuation graph
+from the retained source archive and consumes PR1322's final vector. In each
+orientation it checks all 1,540 clipping rows, with minimum lower bound 8,
+and obtains minimum zero on every tested block:
+
+| Class | Blocks | Independent shift assignments checked |
+| --- | ---: | ---: |
+| Singletons | 237 | 1,659 |
+| Pairs | 27,966 | 1,370,334 |
+| Connected triples | 49,898 | 17,115,014 |
+
+The graph has 2,414 interaction edges and 15,619 incident ADD records per
+orientation, with multiplicity. Disconnected triples reduce to their
+singleton/pair components. The theorem covers all 2,190,670 three-helper
+subsets; the verifier does not execute all shift assignments on every
+disconnected triple. Forty synthetic graphs supply 13,720 literal-objective
+comparisons, and tariff controls exercise the zero-exponent discount and
+paid boundaries. One rejection control prevents clipping without its
+premise. Thirty-two complete-objective controls include shifts of magnitude
+2^32. The stdout receipt is generated and bound to input and
+package hashes; no receipt is handwritten.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/k8-unequal-triple-closure/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/k8-unequal-triple-closure/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/k8-unequal-triple-closure
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/k8-unequal-triple-closure --check-source-history
+```
+
+Another CPython 3.12 executable can replace that local path. The direct
+marker is `PASS_K8_UNEQUAL_TRIPLE_CLOSURE`. Each registered command has a
+120-second limit and writes no files. The committed-byte/history command
+requires a committed package and full Git history. Direct replay also works
+from an official Git-free export containing its two declared live inputs.
+
+## Scope, credit and provenance
+
+Philipp / mightyOil supplies PR1322's open question, final vector, objective,
+common-shift triple result and graph decomposition, following PR1310/1263.
+Hanson Sun / bbMisk supplies PR1214's exact pair method; woklerx supplies
+PR1161's constant gauge mechanism; Sagar Thakrar supplies the retained
+copy-init lowerer. Jeremy Kothe, Rohan Arun, Hao Yan / icekylinx, Douglas
+Colkitt and the original supplier/frame/native/compiler lineage retain their
+credit. Their files and credit lines are unchanged. The new contributions
+are the two-neighbor clipping certificate and unequal-triple closure at
+this final vector. General integer-cost decomposition is not claimed as
+a new mathematical technique.
+
+Scientific base is canonical main
+`a5bff3bf133e482541c09eba4e773884bdb2b1b7`, priority revision 8.
+[SOURCES.json](SOURCES.json) pins the historical source archive, vector,
+question, task catalogue and selected record. The current selected binding
+orientation passed at kappa 0.003125804. This historical scalar result does
+not transfer automatically to that changed P104 supplier. The card's scope
+is explicitly changed in [TASK.json](TASK.json).
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19279574)
+was preceded by live handoff, reservation, open/merged PR, recent-account
+and main README searches. The overlap cache covered 337 open PRs and 5,949
+Discussion records with complete remote pagination; only 89 of 8,623 local
+notes were materialized. Main README searches supplemented those sparse
+notes. These checks do not exclude unpublished work or establish global
+novelty. The time-dependent ADD-once bipartite model of PR6130 is different
+from this fixed cyclic graph with constant gauges.
+
+Four or more changes, temporal gauges, a changed graph or lowerer, native
+integration, ownership, full precision, stock and tape costs remain outside
+scope. No circuit, recursive paid profile, selected frontier or inherited
+framework assumption is changed. Selected scientific replay, predecessor
+scientific suites, Lean and Docker were not run. Independent human and
+formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+Can at least four independently changed helpers improve this final vector?
+Start with one explicit displacement and the complete boundary-inclusive
+objective. A strict witness would identify the next coupled move; no such
+witness or larger-support optimality certificate is supplied. This result
+does not authorize an automatic larger historical construction campaign.
+
+## Implementation constraints
+
+The new verifier is nonrecursive, uses exact integers, has no subprocess,
+network, dynamic import or file-write path, and keeps every function below
+60 physical lines. Source hashes are checked before parsing. The source
+domain has at most 25,000 events per orientation, 16,000 retained terms,
+237 helpers, clipping radius 40 and 60,000 connected triples. The largest
+bounded census has 60,000 times 343 assignments. Input handles have scoped
+cleanup, failures propagate, and explicit checks remain active under -O.
+
+Power of Ten rule 3 has a managed-runtime deviation. CPython, JSON and tar
+parsing allocate dynamically during this finite command. Reads are capped
+at 64 MiB per authenticated input, each decoded member at 16 MiB, and live
+tables are bounded by the domains above. This is not a fixed-allocation or
+real-time claim. A streaming parser/fixed-storage representation is required
+before admitting unbounded data or a persistent service. Warning-strict
+normal/optimized execution and in-memory compilation provide diagnostics;
+no external linter or type analyzer is claimed.

research/k8-unequal-triple-closure/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/community-frontier1042-audit/selected-replay.tar.gz",
+      "usage": "input",
+      "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b",
+      "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754"
+    },
+    {
+      "path": "research/k8-coherent-triples/CERTIFICATE.json",
+      "usage": "input",
+      "git_blob": "552462497e38e9f016cd0b858d2480aab1fa4ae4",
+      "sha256": "d35776232f149e670fcc7a3b37f6000dd5d0f550c27c66bb67a5d33d904501f8"
+    },
+    {
+      "path": "research/k8-coherent-triples/README.md",
+      "usage": "provenance",
+      "git_blob": "675ce355b6ade05ec7a2baa396b0adae0a741407",
+      "sha256": "f46f39bde75c28b5be3f2b41251e2157046941efcd9a17bb46051aca6b836631"
+    }
+  ]
+}