Prove source gauges cannot help before the third use (no new κ)

research/low-use-source-gauges/PROOF.md

@@ -0,0 +1,126 @@
+# Restored gauges have a sharp source-use threshold
+
+This is a scoped scalar-cost theorem. It answers the low-use part of the
+coupled source/target question in Dugongue's PR #4518. Its native word and
+its target-only interval theorem are predecessor work, not replay targets.
+
+## Model
+
+Let X be a finite collection of sources and Y a disjoint collection of
+targets. Every field starts with arbitrary data. Fix a list of nonzero
+dyadic contributions, indexed by e,
+
+    Y_t(e) <- Y_t(e) + q_e X_s(e),    q_e = o_e 2^v_e,
+
+where o_e is a signed odd integer and v_e is an integer. Parallel list
+entries count separately. Each listed contribution executes exactly once,
+in any order. No other ADDs, role mixing, scratch, or factorizations are
+allowed. Sources never receive contributions. Targets never supply them.
+
+Each role may undergo any finite sequence of positive power-of-two SCALEs.
+Its integer gauge starts and ends at zero. With current source and target
+gauges a_s and b_t, the physical ADD coefficient must be
+
+    q_e 2^(b_t-a_s).
+
+SCALE by 2^h costs 2|h|. The retained #4518 tariff for a nonzero ADD is
+
+    c(o) + 2|v|,    c(o) = 2(2 + bit_length(|o|) + popcount(|o|)).
+
+Thus the charged cost of a schedule is
+
+    C + 2 sum_roles TV(g_role)
+      + 2 sum_e |v_e + b_t(e) - a_s(e)|,                 (1)
+
+where C=sum_e c(o_e). Gauge paths have zero endpoints, and TV includes both
+entry and return. Nothing is assumed zero initially. The representation
+invariant is X_stored=2^a X_initial and
+Y_stored=2^b(Y_initial + sum of completed logical contributions).
+It proves exactness of every schedule in this model and full dirty return.
+
+## Theorem 1: remove every source used at most twice
+
+For any schedule, erase all SCALEs of a source s used d_s<=2 times, leave
+every other gauge path and the ADD order unchanged, and adjust its ADD
+coefficients to the displayed representation invariant. The new schedule
+has the same exact endpoint and costs no more.
+
+Proof. Let M=max|a_s| over that source's complete path. Its zero endpoints
+imply TV(a_s)>=2M. Erasing its SCALEs saves at least 4M. For each use,
+
+    |v+b| - |v+b-a_s| <= |a_s| <= M.
+
+Consequently its ADD cost grows by at most 2 d_s M <= 4M. Odd parts are
+unchanged. The representation invariant proves the endpoint, including the
+restored arbitrary source. This argument does not modify any target gauge
+or rely on the timing of another source. Apply it to each such source. QED.
+
+The same argument removes a target used at most twice. Interchanging the
+two gauge variables only changes a sign inside the absolute value. This
+observation is used below for the sharpness family.
+
+## Corollary: an exact optimum with no coupled-source search
+
+If every source has at most two list entries, the minimum over all coupled
+source/target paths equals the target-only minimum
+
+    C + sum_t min_(L<=0<=H)
+        [4(H-L) + 2 sum_(e:t(e)=t) dist(-v_e,[L,H])].    (2)
+
+Each endpoint can be chosen among zero and the -v_e incident to that target.
+The new implication is Theorem 1. The target-only interval formula and its
+attaining walk 0 -> L -> H -> 0 are #4518 Theorem 2, used as a cited premise.
+Targets are independent when sources are fixed. Serve them consecutively to
+attain the sum, with no extra fields and every entry/return SCALE charged.
+Formula (2) covers arbitrary finite graph size, odd parts, valuation sizes,
+ADD orders and finite integer gauge paths under the model above.
+
+## Theorem 2: three uses are the first possible strict gain
+
+Consider one source and d distinct targets, with every coefficient o 2^v.
+For d>=1, the exact coupled optimum is
+
+    d c(o) + 2 min(d,2)|v|.                             (3)
+
+The target-only optimum is d c(o)+2d|v|. Hence for d>=3 and v!=0 the exact
+gain is 2(d-2)|v|, and the source-use threshold in Theorem 1 is sharp.
+
+Proof. Remove all target gauges by the symmetric low-use argument. Let M
+be the largest absolute source gauge visited. Return costs at least 4M,
+and the d ADDs cost at least d c(o)+2d max(|v|-M,0). For M<=|v| the variable
+part is 2d|v|+(4-2d)M; for M>=|v| it is at least 4|v|. Minimizing these two
+pieces gives (3). With d<=2, use no SCALEs. With d>=2, scale the source to
+gauge v, execute all ADDs with coefficient o, and restore it to zero.
+These constructions attain the bound. Without source gauges each target
+has one contribution, and its return costs cannot improve that direct ADD.
+
+At d=3, o=1, v=-1, the direct/target-only optimum is 30. Scaling the dirty
+source by 1/2, executing three coefficient-one ADDs and scaling it by 2
+costs 2+3*8+2=28. Every source and target retains its required arbitrary-input
+endpoint. This is a scalar allowance gain for this star, not an invoice gain
+for a complete supplier. QED.
+
+## Both dual interfaces
+
+Elementwise inverse-transpose dualization in the same execution order sends
+ADD(t,s,q) to ADD(s,t,-q) and SCALE(r,2^h) to SCALE(r,2^-h). It gives the
+inverse transpose of the full product and preserves every tariff. This is
+the classical Levi homomorphism, used in #4518 Theorem 3. The star's dual
+is one target receiving -o 2^v from d distinct sources. Both interfaces
+restore every gauge and have the same optimum and dirty-state contract.
+The finite checker independently multiplies both physical words.
+
+## Scope
+
+This supplies a new source-elimination theorem and an attaining sharpness
+family for the declared ADD-once bipartite class. It is not optimality over
+general scalar circuits. Repeated use count, source writes, target reads,
+borrowing, non-diagonal changes, unreturned gauges, and alternative tariffs
+can change the conclusion. The minimum includes a fixed list of ADDs;
+coalescing or deleting that list is a separate optimization.
+
+Ali Romman's PR #5824/#5830 already provide optimal signed representations
+on different fixed P104 gauge graphs, using exact cuts and flow certificates.
+No global gauge-optimization invention is claimed here. No existing native
+word, recursive paid/target histogram, physical precision/tape bill or selected
+frontier is changed. All five selected framework assumptions remain.

research/low-use-source-gauges/README.md

@@ -0,0 +1,145 @@
+# Source gauges cannot help before the third use
+
+**Claim type: scoped proof with exact finite corroboration. No new κ.**
+This contribution was produced by Nick Petalas.
+
+In the restored dyadic ADD-once bipartite model of [PROOF.md](PROOF.md),
+temporarily scaling sources cannot reduce the optimum if every source is
+used at most twice. This holds with arbitrary simultaneous target gauges,
+ADD order, integer gauge excursions and arbitrary dirty initial fields.
+The optimum reduces to Dugongue's target-only interval formula from
+[PR #4518](https://github.com/CrocSwap/integer-mult-bounds/pull/4518).
+
+Three uses are the first possible strict gain. For one source feeding d
+distinct targets with coefficient o 2^v, o signed odd, the exact optimum is
+
+```text
+d c(o) + 2 min(d,2)|v|,
+c(o) = 2(2 + bit_length(|o|) + popcount(|o|)).
+```
+
+The target-only optimum is d c(o)+2d|v|. At d=3, o=1, v=-1, a restored
+source scaling gives cost 28, versus the exact target-only minimum 30.
+The inverse-dual word has the same cost and full dirty-state correctness.
+The star construction is elementary shared-factor extraction. The new
+contribution is the elimination theorem, its exact coupled optimum and
+sharp source-use threshold under this schedule contract.
+
+The proof erases a source's gauges, saving at least four times its maximum
+absolute gauge. Each incident ADD can lose at most twice that maximum.
+At two uses the saving covers the entire possible loss. This supplies a
+pruning rule for the coupled source/target question in #4518 Open next
+question 2. A single row with distinct sources is an immediate special case.
+
+## Reproduce
+
+CPython 3.12, standard library only, from the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -X dev -I -B research/low-use-source-gauges/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -X dev -I -O -B research/low-use-source-gauges/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/low-use-source-gauges
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/low-use-source-gauges --check-source-history
+```
+
+Another CPython 3.12 path may replace the one shown. Direct replay prints
+`PASS_LOW_USE_SOURCE_GAUGES no_new_kappa` and a freshly generated stdout
+receipt binding the package files by SHA256. It writes no files. Registered
+replay runs both normal and optimized modes with warnings treated as errors.
+
+The exact finite checks enumerate:
+
+- All 256 two-source/two-target lists with each of four pairs absent or
+  carrying valuation -1, 0 or 1, and fixed alternating odd parts 1 and -3.
+  A separate Dijkstra oracle searches every ADD order and gauge state in
+  {-1,0,1}. Coupled and source-fixed minima equal the interval formula.
+- 81 prescribed gauge-path fixtures at levels -2, 0, 2, comparing each
+  original and source-erased program on all arbitrary-input coefficients.
+- 18 star shortest-path problems and their 18 reversed-incidence versions,
+  with one to three leaves, valuations -1, 0, 1 and odd parts -3 or 1;
+  51 additional degree-three witnesses with valuations -8 through 8 and
+  odd parts -3, 1, 5. Reversed stars exercise profitable target gauges while
+  all sources remain low-use.
+- Full physical and inverse-transpose endpoints and tariff equality for
+  every checked word. Six invalid contracts are rejected. Two further
+  controls detect wrong coefficient compensation and failure of the
+  low-use premise at degree three.
+
+The finite gauge box corroborates the new theorem; it does not prove the
+unbounded optimum by enumeration. The written proof carries that quantifier.
+The predecessor's native program, counts and scientific suite are not replayed.
+
+## Scope and sources
+
+Base `721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision 8.
+[SOURCES.json](SOURCES.json) pins the retained #4518 model, tariff, interval
+theorem and dualization statement at head
+`2b71c89a7ca0ad41f12149d7971e73f16f320e81`. The catalogue and selected
+record are historical provenance. Both predecessor files are authenticated
+before direct replay. Its mathematical results are cited inputs.
+
+The scope requires disjoint source/target roles, each listed contribution
+once, only positive power-of-two gauge scales, and every gauge returned to
+zero. Repeated entries count as repeated uses. Role mixing, factoring the
+ADD list, borrowing, source writes, target reads, different prices and
+unreturned gauges are outside the result. No actual P104 word is changed.
+No paid recursive gain, physical implementation, precision/tape saving,
+supplier admission or complete multiplication theorem is claimed. All five
+selected framework assumptions remain. Selected cold replay, Lean, Docker,
+independent human review and proof-kernel review are unrun.
+
+Before reservation, live open PRs, recent account PRs, handoff comments,
+active Discussions, local locks and main/merged-work searches were checked.
+The overlap helper reported complete pagination of 379 open PRs and 5,780
+Discussion records, but only 60 of 8,348 local notes. Searches of main's
+README objects and relevant merged PRs supplemented that sparse cache.
+These searches do not establish global literature priority.
+
+Ali Romman's [#5824](https://github.com/CrocSwap/integer-mult-bounds/pull/5824)
+and [#5830](https://github.com/CrocSwap/integer-mult-bounds/pull/5830) already
+optimize different fixed P104 representation graphs with exact flow duals;
+[#5783](https://github.com/CrocSwap/integer-mult-bounds/pull/5783) supplies
+related exact binary-cut tooling. Richard Hoekstra's
+[#1235](https://github.com/CrocSwap/integer-mult-bounds/pull/1235) normalizes
+endpoint gauge tours in a different rank-priced phase model. None is an
+audit target or an executable dependency here. No new general gauge,
+shared-factor, shortest-path or flow algorithm is claimed.
+
+## Open next questions
+
+Which sources with at least three uses in a named complete native window
+admit a profitable restored gauge after all surrounding interfaces are
+charged? Start by extracting one ADD-once bipartite window and its existing
+target-only optimum, then remove low-use source variables with this theorem.
+The remaining emitted-window, caller, native and precision/tape contracts
+block physical adoption. The present package stops at the sharp threshold.
+
+## Verification design
+
+The verifier is a separate standard-library implementation and imports no
+predecessor code. Its finite domain enforces at most four roles, four ADDs,
+valuation magnitude eight and 1,000 events. The oracle has at most 1,296
+states and 15,553 heap pops, with parent reconstruction bounded by the state
+count. Other enumerations have literal finite products. Functions have
+fewer than 60 lines. Explicit exception-based invariants remain active under
+`-O`; all arithmetic is exact. No recursion, runtime code generation or
+external solver is used.
+
+Power-of-Ten rule 3 has a managed-runtime deviation in `verify.py`: CPython,
+Fraction and heap/dictionary operations allocate during execution. The
+enforced capacities bound live state and rational sizes; no retained
+external resources or output files exist. Static input sizes and the finite
+loop bounds compensate for the lack of allocation-free Python operation.
+A fixed-storage implementation would be needed for an allocation-free
+runtime; that is outside this scientific check. Warning-strict normal and
+optimized runs are the available local diagnostics.
+
+## Credit
+
+Credit David Ganz / Dugongue for #4518's native dyadic tariff, target-only
+interval theorem, emitted interfaces and coupled-path question. Its
+PR #4502/#4505 borrowed-adapter and native lineage retain their attribution.
+The Levi inverse-transpose identity is classical and used as in #4518.
+Credit Ali Romman and Richard Hoekstra for the related gauge work above.
+New work is Apache-2.0. Independent human and formal proof-kernel review
+are unclaimed.

research/low-use-source-gauges/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "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/levi-adaptive-gauges/PROOF.md",
+      "usage": "input",
+      "git_blob": "78ce6bc0a8797934bc6906336bf1d5a9fb37f99a",
+      "sha256": "4bd623c249866389837591edb3972a6456570e83aa82354d1905914de3b74d4c"
+    },
+    {
+      "path": "research/levi-adaptive-gauges/README.md",
+      "usage": "input",
+      "git_blob": "577b69b92b9d71330c7d80e5ee56faaa55e04318",
+      "sha256": "b3ed2bffa4b3c6d9d530c45b9f8516820edc02663ca5723089040bb9006552d7"
+    }
+  ]
+}