Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions .github/workflows/p112-common-slice.yml
Original file line number Diff line number Diff line change
Expand Up @@ -15,9 +15,9 @@ jobs:
if: github.repository == 'CrocSwap/integer-mult-bounds'
runs-on: ubuntu-24.04
timeout-minutes: 20
env:
TMPDIR: ${{ runner.temp }}/p112-common-slice
steps:
- name: Initialise P112 work directory
run: echo "TMPDIR=$RUNNER_TEMP/p112-common-slice" >> "$GITHUB_ENV"
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
with:
fetch-depth: 0
Expand Down
69 changes: 69 additions & 0 deletions research/p104-role-exchange-residue/PROOF.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,69 @@
# Exact boundary and sharp residual replacement bound

## 1. Algebra and inherited channel

Let D be `Z[i,1/2]`, the Gaussian dyadic ring. All identities below hold for arbitrary elements of a free D-module, hence coordinatewise on arbitrary finite arrays. No input target is zero, and no dirty helper is clean. Write x and y for the original 104 source and target fields. The retained channel has normalised boundary `(x,y,h) -> (x,v=y+A x,h)` for 72 independent dirty fields h. This boundary theorem and its native chart interpretation are inherited from PR1972/PR1991.

The source extraction constructs the 120 unoriented doubled E8 root representatives in canonical sorted order and deletes the 16 retained F0/C vectors. The resulting matrix R satisfies `RR^t=104I`. Set `A=R^t R/8`. The eight chosen pivot columns J are an orthogonal frame, so `R_J^t R_J=8I` and `R_J R_J^t=8I`. With `B=R_J^t R_N/8`, direct multiplication gives

```
A = [[I, B], [B^t, B^t B]]
```

in J,N order. Thus `v_J=y_J+x_J+B x_N` and `v_N=y_N+B^t(x_J+B x_N)`. Every nonzero entry of B is a signed half. The finite verifier checks each entry and every identity used here.

## 2. A source-consuming tail without a clean bank

All source arrays finish in FULL. First lift every Y target from its existing eight-dimensional hyperplane to FULL. The following common-chart equations are then legal scalar operations on the available banks.

For each unchanged nonpivot source, add its signed half to each incident pivot X and subtract that same signed half from the corresponding pivot Y. The two streams may be interleaved because no nonpivot source has yet been changed permanently. They give `X_J=q=x_J+B x_N` and `Y_J=w_J=x_J+y_J`.

Next subtract `B^t q` from X_N and then add Y_N. This gives

```
X_N = x_N - B^t q + v_N = x_N+y_N = w_N.
```

Return X_N to the target hyperplanes indexed by N and Y_J to those indexed by J. The residual banks X_J and Y_N remain in FULL. This is an explicit output-role assignment, not a claim that data movement or arbitrary caller relabelling is free. The 72 inherited dirty-helper banks are never targeted or read by this tail. Their inherited logical restoration is therefore preserved.

The literal scalar schedule halves each X_N once, applies all of its incident unit additions and subtractions, and doubles it before proceeding. It then halves each pivot q once, applies its incident scatter subtractions, and doubles it. Finally it performs 96 direct X_N += Y_N additions. This uses 1,248 unit Gaussian ADDs, 104 halves, and 104 doubles. Every arithmetic source and target is in FULL. The 104 initial lifts and 104 final descents are rank-one pairs, for 208 formal native occurrences. They require their usual paid native implementation, not free frame relabelling.

The inverse boundary is explicit. From `(w,q,v_N)`, compute `x_N=w_N-v_N+B^t q`, then `x_J=q-B x_N`, and finally `y=w-x`. These are D-linear equations. Their existence proves an invertible encoding, but not the cost or legal availability of a physical downstream decoder.

The statement does not preserve the original source bank. In particular, Y_N still contains the original channel-produced v_N, whereas the eight would-be residual values v_J are replaced by q. Requiring the original source outputs again changes the contract and demands a priced continuation.

## 3. Why every old residual cannot be retained

Consider the tempting alternative boundary that returns all corrected sums w and all old residuals v, with arbitrary dirty helpers restored and no other persistent source-dependent output. Its data matrix is

```
T = [[I,I], [A,I]].
```

The previously known covariance identity implies `A^2=13A`, with A of rational rank eight. Hence `C=I-A` has eigenvalues 1 with multiplicity 96 and -12 with multiplicity eight, and `det(T)=det(C)=12^8`. This determinant was already implicit in the predecessor correction certificate; the new use is its odd-prime obstruction to this changed return contract.

Reduce D modulo 3. The quotient is the field F9 because `z^2+1` is irreducible over F3 and 2 remains invertible. The matrix R has rank eight modulo 3 since `RR^t=104I=2I`. Therefore A is an idempotent of rank eight, C has rank 96, and T has rank 200 rather than 208. The primary checker separately eliminates both C and T modulo 3. Since all entries of these particular matrices are rational dyadics, their rank over F3 equals their rank after scalar extension to F9.

A reversible D-linear circuit must remain invertible modulo 3. This includes arbitrary invertible D-linear recoding, exact dyadic scaling, phase multiplication, and invertible dyadic native chart changes. Appending any number of arbitrary dirty inputs and returning them unchanged only adds an identity block, so it cannot repair T's eight-dimensional defect. Clean temporary banks that are returned to zero likewise do not provide a final source-dependent observation.

Now keep every w output but permit replacing k of the old v outputs by arbitrary D-linear outputs. Modulo 3, replacing k scalar rows increases rank by at most k. Reversibility therefore requires `200+k >= 208`, or `k >= 8`. Our boundary replaces exactly the eight v_J outputs and has the explicit D-linear inverse in section 2. Eight is thus the exact minimum in this residual-row replacement model.

For arrays with d Gaussian coordinates, the naive defect has dimension 8d. Replacing k whole arrays contributes at most kd scalar rows even when arbitrary cross-coordinate D-linear mixing is allowed, so the whole-array minimum remains eight. This is a count of changed residual outputs, not a transport-rank, lifetime, storage-width, or recursive-cost lower bound.

A related necessary statement holds when all v outputs are retained and extra persistent clean-carrier output coordinates are allowed. They must supply at least 8d independent residues modulo 3. This does not establish a physical attaining carrier scheme or allow an arbitrary dirty bank to be treated as clean.

## 4. Scope controls

The ordinary source-preserving correction shear `[[I,0],[C,I]]` is invertible over D for every C. The verifier checks its full rank modulo 3 as a positive scope control. Thus the argument is not an impossibility theorem for correcting P104.

The lower bound also does not cover division by an odd Gaussian prime, nonlinear rounding/residue encoders, nonzero private erasure, extra persistent source-dependent outputs, restricted correlated input domains, or a consumer that requires fewer sums or a different residual contract. Those are separate hypotheses and have their own implementation and price obligations. In particular, the ideal dyadic argument does not silently validate the literal signed-floor execution on arbitrary integer arrays.

The fixed-cover support and source-preconditioner models preserve different data contracts. Reading and modifying channel Y, consuming X, and replacing residual outputs are explicit changes here. The result neither repeats the 208-flag static cover nor refutes the 23-dimensional preconditioner obstruction reported in PR3810.

## 5. Exact evidence and budget boundary

The primary implementation replays every new scalar instruction on 280 independent columns, including all original dirty variables. It verifies every sum, every residual, every helper, and every final frame dimension. Its separate inverse calculation uses the boundary equations rather than reversing the instruction list. The second implementation rebuilds the root geometry by a different enumeration and evaluates the endpoint in quarter-integer coefficients with a block ordering distinct from the primary schedule. It compares the full 280 by 280 endpoint digest.

With normalised integer x,y inputs, every scalar prefix coefficient is a multiple of one quarter. A quarter is actually attained, so two fractional bits are sharp for this scalar instruction list. The maximum row one-norm is 26, including the channel-exit input rows; this bounds each real component by 26H when every original component is at most H. Neither statement includes the native frame-conversion arithmetic or proves that an outer physical producer supplies these normalised integer inputs.

The formal added native profile is 208 H1. The retained profile therefore becomes `(1282,58,86,104,48,24,8,8)` and has mass 2576. Under the unchanged width-nine, 280-role bare mass relaxation, `2576/(9*280)=46/45>1` already fails. This is the predecessor terminal-tariff stop applied to the same numeric profile, not a lower bound for all changed consumer laws. Owner routing, a physical residual consumer or decoder, literal native admission, precision, tape, and complete all-size hosting remain unresolved. Their costs are unknown, not zero.
84 changes: 84 additions & 0 deletions research/p104-role-exchange-residue/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,84 @@
# P104 source-consuming role exchange with eight residual replacements

This is a changed terminal consumer contract, not another fixed-cover census and not an admitted multiplication supplier. It starts after the retained PR1972/PR1991 forward channel, consumes its source bank, and produces every corrected sum `w = x+y`. It returns an explicit invertible encoding of the remaining data instead of pretending that the original source bank is restored.

The new result has two parts. An exact chronological tail returns `(w,q,v_N)` without adding a clean bank or touching the 72 original dirty helpers. A modulo-three argument proves that replacing at least eight of the naive 104 residual outputs is necessary in the specified reversible dyadic-linear model, even when arbitrary dyadic recoding and native chart changes are granted. Our tail replaces exactly eight. The corrected sums are not left in the original Y bank locations.

Canonical base is `20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority revision 6. The selected conditional kappa remains `0.001672660197076918`. Only this opt-in package is added. `TASK.json` records the explicit user assignment and changed scope.

## The exact boundary

Write `A=G/2=R^t R/8`, where R is the retained 8 by 104 doubled-root matrix. The predecessor channel leaves X holding x in FULL, Y holding `v=y+A x` in each target hyperplane, and its 72 arbitrary dirty helpers logically restored in FULL. Its native channel identity is inherited, not re-proved by this package.

Choose the eight mutually orthogonal retained roots `2(e0 +/- e2)`, `2(e1 +/- e3)`, `2(e4 +/- e6)`, and `2(e5 +/- e7)`. In canonical port order their indices are

```
J = [0, 1, 3, 6, 22, 31, 93, 103].
```

Let N be the other 96 indices and `B=A[J,N]`. All 384 nonzero B entries are signed halves. The pivot block is `A[J,J]=I`, and `A[N,N]=B^t B`.

Lift all 104 Y arrays to FULL. While every X_N source is still unchanged, perform both `X_J += B X_N` and `Y_J -= B X_N`. Thus X_J becomes `q=x_J+B x_N`, and Y_J already equals `w_J`. Then perform `X_N -= B^t X_J` and `X_N += Y_N`, producing `w_N`. Return X_N and Y_J to their respective target hyperplanes. Leave X_J and Y_N in FULL.

The final corrected-sum locations are X_N and Y_J. The residual locations are X_J for q and Y_N for v_N. All original dirty helper locations are untouched by the tail. Logical restoration at a changed frame is not a claim that the original physical input array is bitwise unchanged.

The inverse boundary equations are

```
x_N = w_N - v_N + B^t q,
x_J = q - B x_N,
y = w - x.
```

They use only dyadic coefficients. They prove information preservation, not a free decoder or a caller that already accepts this representation. PROOF.md proves the identity, the modulo-three lower bound, and its precise exclusions.

## Invoice and stopping decision

The generated tail contains 1,664 formal events. These comprise 1,248 unit Gaussian array additions/subtractions, 104 exact array halvings, 104 restoring doublings, and 208 rank-one frame conversions. There are no new banks, private erasures, or clean-input assumptions. No source-independent dirty helper is substituted for a data pivot.

Under the inherited native dimension-gap tariff, the added profile is `208 H1`. Adding it to the retained channel gives `(1282,58,86,104,48,24,8,8)` at ranks 1 through 8, with total rank mass 2,576. These are formal frame conversions of the same hyperplane/FULL pairs already considered by the predecessor terminal audit. We have not recompiled their native recipes or executed their signed-floor implementations under the changed bank roles.

For 512 complex words per array, the scalar part alone has 1,277,952 real additions/subtractions, 106,496 real halvings, and 106,496 real doublings. These counts exclude native-pair arithmetic, addressing, movement, and control. In normalised common-chart coordinates, integer initial x and y require at most two fractional bits during the scalar tail, with a sharp coefficient denominator of four. The maximum row one-norm, including the channel-exit entrance, is exactly 26, giving a `26H` bound per real component. This does not certify the physical native entrance, the original channel's internal width, or accumulated rounding error.

Even granting the unchanged width-nine, 280-role bare local-mass relaxation, this profile has `M(0)=2576/(9*280)=46/45>1`. That numerical stop is inherited from the earlier 208-rank terminal-correction tariff, not a new general P104 lower bound. The changed logical boundary supplies no additional capacity or coverage by itself. A different consumer needs its own law and complete bill.

The decision is **NARROW**. Retain the exact changed-boundary module and the sharp eight-replacement result. Do not expand it into a supplier construction under the unchanged failed budget.

## Reproduction and evidence boundaries

From a complete checkout at the contribution head, use Python 3.12 and the standard library.

```sh
python3.12 -I -B scripts/research_package.py --package research/p104-role-exchange-residue
```

The default primary command authenticates all three frozen source files, compares the 16-root extraction, and binds every original X, Y, and dirty-helper exit frame. It then checks all 280 independent input columns through the newly generated tail. The second implementation imports no primary code and reconstructs the complete endpoint using quarter-integer arithmetic and a different root enumeration. It also checks 16 signed fixtures. Tests distinguish the new output locations, arbitrary dirty inputs, the ordinary source-preserving correction shear, and malformed or altered receipts.

A portable algebra-only mode is deliberately weaker.

```sh
python3 -I -B research/p104-role-exchange-residue/verify.py --algebra-only
python3 -I -O -B research/p104-role-exchange-residue/verify.py --algebra-only
python3 -I -B research/p104-role-exchange-residue/independent.py --algebra-only
python3 -I -O -B research/p104-role-exchange-residue/test_verify.py
```

This mode uses the explicitly transcribed geometry and prints `ALGEBRA_ONLY`. It does not authenticate the complete repository sources. Normal mode fails closed when those files are missing. Frozen RESULT.json is compared without rewriting it. The canonical result digest is `0b869d0e68b8e21468a15977a31432d8b17f5a528558edec7eaf6c5461d63b78`.

Local algebra replays passed on CPython 3.13.5. Full source-bound and registered Python 3.12 results, where subsequently observed, belong in the PR handoff with their exact public head and run identifier. No native recipe replay, original 4,058-event channel replay, full selected cold replay, independent human review, or formal proof-kernel acceptance is claimed here.

## Relationship to predecessor work

Rohan Arun's PR1972 and Chafik Boukhalfa's PR1991 supply the forward channel and native lineage. The retained `p104-side-correction-rank-obstruction` package already proves the rational correction rank and determinant, the root-coordinate factorisation, and the 208-rank terminal screen. Its 2,376-add common-chart word and 1,352-add snapshot word are not new contributions here. The covariance identity `RR^t=104I`, ordinary Gaussian elimination, and modular rank arguments are likewise not claimed as new mathematics.

PR2383 already grants the complete root code for free under its monotone immutable-source contract. PR3427 and Sagar Thakrar's PR3810 address changed source preconditioning and fixed-cover support; the latter's channel-Y-read probe motivates testing coefficients and dirty-state semantics rather than interpreting support as a circuit. Their bounds do not transfer to a source-consuming changed output interface. Our eight-replacement result does not contradict PR3810's rank-23 preconditioner bound.

Clear1nsight's PR3609 uses eight in-place data pivots for a different dual-entrance completion. That pivot technique is related, not a newly discovered general technique here. The present object is the original forward 104-source/104-target terminal channel, with a different returned-source contract and a sharp modular obstruction to leaving every old channel-Y residual intact. PR3620 and the later caller audit reinforce the need to price the actual changed consumer rather than donate a boundary conversion.

Prepared by Clear1nsight with substantial OpenAI assistance. The two checking implementations share the same assisted session and sources. New work is Apache-2.0; source geometry and predecessor results retain their authorship and notices. See SOURCES.json for immutable source bindings and bounded overlap coverage.

## Open next questions

A useful continuation must name an actual consumer of `(w,q,v_N)` and prove its input/output intertwiner, ownership, return, and complete coverage law. Its first test is the full budget, because the unchanged width-nine relaxation already fails. Original-source decoding, residual erasure, and physical bank relabelling are not free operations.

Only after that gate passes should the 208 hyperplane/FULL recipes be rebound to the new bank roles and replayed with an actually supplied physical entrance. The scalar two-bit result alone does not establish exact native halves, finite-width safety, routing, tape use, or all-size admission. TASK.json records these concrete blockers without reserving them.
Loading