Research: exact 96-dimensional P104 shared correction space

research/p104-minimum-shared-space/README.md

@@ -0,0 +1,188 @@
+# The fixed P104 shared correction space has minimum dimension 96
+
+This closes the **96-versus-97 algebraic question** in
+[Gonzalo Mier's PR #2173](https://github.com/CrocSwap/integer-mult-bounds/pull/2173),
+head `d9b784ca86fba060f0264370536ccd322c89998a`. An explicit rational space of
+dimension **96** supplies every `I-G/2` correction row modulo that target's
+fixed pooled snapshot span. The predecessor proves the lower bound 96 and
+exhibits a 97-dimensional space generated by natural correction rows. Our
+witness allows arbitrary rational directions and attains the lower bound.
+
+**This is a relaxed algebraic interface, not a chronological correction word
+or a cheaper supplier.** Snapshot pooling grants access at different times;
+constructing, transporting and restoring the new shared directions is not
+priced here. No new κ or selected-frontier change is claimed.
+
+## Exact model and evidence
+
+The frozen 4,058-event PR #1972 channel, retained in PR #1991's native package,
+has 104 source inputs, 104 target inputs and 72 arbitrary dirty helper inputs.
+We replay all **280 independent input columns**, every frame and private
+lifetime, and the original `G/2` endpoint. The inherited paid rank mass remains
+2,368; no new native invoice is inferred from the dimension calculation.
+
+At each of the 4,059 cuts, let `v_r(c)` be the current logical row of live
+register `r` in the original channel. For target `t`, define
+
+```
+S_t = span_Q { v_r(c) : r != Y_t,
+              frame(r,c) = frame(Y_t,c) as binary subspaces }.
+C = I - G/2.
+```
+
+All live sources, helpers, private copies and other targets are eligible.
+Rows from different cuts are pooled, and chart-basis changes within the same
+subspace are free in this model. The snapshots themselves remain unchanged:
+new shared rows are not fed back through the old word to create new snapshots.
+The question is the least dimension of any rational subspace `H` of the full
+280-coordinate boundary space for which `C_t in S_t + H` for all 104 targets.
+
+The two checkers reconstruct 1,488 distinct rows seen in target-containing
+frame classes. Individual pools have 1,053–1,080 distinct eligible rows.
+Their source-coordinate ranks have histogram
+`{2:12, 3:24, 4:32, 5:24, 6:12}`; the full ranks are these numbers plus 175.
+These agree with the predecessor's 177–181 full-span ranks.
+
+[WITNESS.json](WITNESS.json) contains only **41 weighted contacts**
+`[target, cut, register, rational_weight]`, on 23 target rows. A cut is the
+number of completed original events: cut zero is the initial state. All 41
+contacts use dirty `D` helpers, and all weights are `±1/2` or `±1`.
+The contacts are a certificate of vector-space membership, not 41 new
+chronologically executable operations.
+
+## Proof
+
+Let `R` be the 8-by-104 matrix of **doubled integer root coordinates**, with
+ports in the pinned lexicographic order. Exact enumeration gives
+
+```
+R R^T = 104 I_8,       G = R^T R / 4,
+C = I_104 - R^T R / 8, C^-1 = I_104 - R^T R / 96.
+```
+
+In particular, `C` is nonsingular and `R C = -12 R`.
+
+**The fixed-span lemma.** Every captured snapshot's source-coordinate
+projection lies in `row(R)`. At cut zero, `S_t` contains all 175 non-source
+coordinate units except its own target input `Y_t`. No eligible snapshot has
+a coefficient on that missing input. These statements are checked on the
+full frozen trace, not inferred from just its final `G/2` identity. Thus any
+captured row can have all its non-source coefficients removed using those
+175 units. In particular `pi_X(S_t) = S_t intersect X`, and this space is
+contained in `row(R)`.
+
+**Lower bound (the predecessor's bound, with a direct certificate).** If an
+arbitrary full-boundary space `H` serves every target, then
+`C_t in row(R) + pi_X(H)` for every `t`. The rows of `C` span all of `X`, so
+
+```
+104 <= 8 + dim(pi_X(H)) <= 8 + dim(H).
+```
+
+This also permits shared directions with dirty or target coordinates; those
+coordinates cannot evade the projection bound.
+
+**Attainment.** For a certified contact with projected row `x`, its unique
+root-code coefficient row is `a = x R^T / 104`. Sum those coefficient rows
+with the recorded weights, separately for each target, to form a rational
+104-by-8 matrix `A`. The contacts and the fixed-span lemma give
+`(A R)_t in S_t intersect X`. Both checkers verify the exact identity
+
+```
+R A = I_8.
+```
+
+Consequently `E = I_104 - A R` is an idempotent of rank 96. Define
+
+```
+K = E C = C + 12 A R,       H = row(K),
+```
+
+embedded in the first 104 boundary coordinates. Since `C` is invertible,
+`rank(K)=96`. Also `K_t - C_t = 12(AR)_t` lies in `S_t`, so this single
+96-dimensional space serves every target. The lower and upper bounds match.
+Both checkers additionally compute the exact rank of the explicit `K`.
+The independent checker verifies each of the 104 identities in all 280
+coordinates, including cancellation of the snapshot's original dirty input.
+The sparse checker also verifies the right kernel `C^-1 A = A - R^T/96`;
+right multiplication by `C` changes the kernel of `E`.
+
+The optional generator searches the 416 available local basis directions
+using a rational linear system with 64 equations. It finds a full-rank
+system and a 41-term solution. Acceptance does not rerun or trust that search:
+the recorded contacts, `RA=I`, full-space memberships and ranks suffice.
+
+## Reproduce and controls
+
+Standard library, no network or predecessor checker imports:
+
+```sh
+python3 -I -B research/p104-minimum-shared-space/verify.py
+python3 -I -O -B research/p104-minimum-shared-space/independent.py
+python3.12 scripts/research_package.py --package research/p104-minimum-shared-space
+```
+
+The first checker uses sparse rational rows, reduced binary bases and sparse
+elimination. The second uses dense integer rows on the independently checked
+denominator-four lattice, explicit enumeration of every binary subspace, and
+dense rational elimination. Only strict I/O and receipt encoding are shared.
+Both compare against [RESULT.json](RESULT.json). `--out NEW.json` writes a
+receipt exclusively to a fresh caller-selected path; default replay is read-only.
+
+`test_package.py` tests all 41 coefficient sign changes, unavailable contacts,
+use of a target's own row, missing initial dirty compensation and final helper
+cleanup, a missing puncture, an incorrect transport rank, JSON/schema faults,
+source and receipt drift, occupied outputs, and a read-only export without Git.
+Reversing every frame basis is a positive representation-invariance control.
+These checks also run with optimization enabled in the exported replay.
+
+To regenerate the witness without modifying committed evidence:
+
+```sh
+python3 -I -B research/p104-minimum-shared-space/build.py --out /tmp/NEW-WITNESS.json
+```
+
+The registered replay uses CPython 3.12; source-export validation on CPython
+3.14 is recorded in the PR. No native Clifford regeneration, chronological
+owner assignment, new private-copy contract, global recursive moment,
+precision/all-size argument, selected cold replay or formal proof assistant
+check is part of this package. The predecessor's finite native realization
+is inherited, not re-certified by our scalar replay.
+
+## Open next questions
+
+Dimension is an information-space quantity, not a count of paid child ranks.
+The already known 208-rank end-cut correction is unfavorable under the
+unchanged coverage contract (only `328/9` surplus rank units per call, as
+reported in [PR #2082](https://github.com/CrocSwap/integer-mult-bounds/pull/2082)).
+This package does not substitute 96 for 208 in that bill or rerun that cost
+model. It resolves the explicitly requested dimension handoff only.
+
+Can a changed chronological producer realize this complement, or another
+96-dimensional complement, with useful transport sharing? Start by assigning
+actual frame paths and source reads to the certificate's 23 nonzero `A` rows,
+then replay arbitrary dirty restoration and charge every changed transport,
+COPY, idle child and owner obligation. The existing fixed-path/retained-cost
+obstructions remain applicable to their models. The present witness grants
+pooled access and arbitrary new shared directions, so it supplies neither
+such a schedule nor a favorable cost bound. See `TASK.json` for the handoff.
+
+## Attribution and provenance
+
+Gonzalo Mier / PR #2173 posed this exact minimum-dimension question, proved
+96 as a lower bound, and supplied the 97-dimensional witness. No part of that
+lower-bound idea or the fixed pooled-span model is claimed new. No pending
+predecessor code is imported or copied; its exact head is pinned for credit.
+
+Rohan Arun / PR #1972 supplies the scalar/frame channel
+(`fd82d172f46933fd253c2c6de4bd5eaff5429cfd`), Chafik Boukhalfa / PR #1991 its
+native realization, Adam Gall / PR #1940 the schedule, and Josie Elliston /
+PR #1071 the fixture, with Ali Romman / PR #1125 and the retained geometry,
+decoder and compiler lineage. Frozen inputs and their notices remain unchanged.
+
+The scientific base is `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, priority
+revision 4. `TASK.json` records the preserved random draw, scoped handoff
+override and Discussion links; `SOURCES.json` binds every external input.
+New mathematics, implementation and prose were prepared by Gareth Davidson
+(@bitplane) with substantial OpenAI Codex assistance. Both checkers are
+AI-assisted implementations, not independent human review. Apache-2.0.

research/p104-minimum-shared-space/RESULT.json

@@ -0,0 +1,142 @@
+{
+  "A_sha256": "05d1386b2386a35d11a9df7fc2eba20c5cb18e66985c7140eb66575fe88f3998",
+  "H_sha256": "e0d953df50999619b5a7823b3d4ed4490ddd0b9c50e0fedb96e99094e3d55dac",
+  "arbitrary_input_columns": 280,
+  "captured_snapshot_rows": 1488,
+  "certificate_terms": 41,
+  "cuts": 4059,
+  "minimum_dimension": 96,
+  "nonzero_A_rows": 23,
+  "original_paid_profile": {
+    "1": 1074,
+    "2": 58,
+    "3": 86,
+    "4": 104,
+    "5": 48,
+    "6": 24,
+    "7": 8,
+    "8": 8
+  },
+  "original_scalar_events": {
+    "add": 2624,
+    "copy": 8,
+    "erase": 8,
+    "zero": 8
+  },
+  "pool_sizes": [
+    1063,
+    1071,
+    1064,
+    1063,
+    1072,
+    1065,
+    1062,
+    1063,
+    1064,
+    1072,
+    1064,
+    1063,
+    1062,
+    1067,
+    1053,
+    1064,
+    1064,
+    1071,
+    1063,
+    1063,
+    1063,
+    1066,
+    1068,
+    1067,
+    1065,
+    1063,
+    1075,
+    1065,
+    1066,
+    1067,
+    1064,
+    1068,
+    1067,
+    1068,
+    1068,
+    1069,
+    1064,
+    1064,
+    1063,
+    1063,
+    1075,
+    1059,
+    1061,
+    1066,
+    1062,
+    1075,
+    1074,
+    1077,
+    1067,
+    1067,
+    1066,
+    1066,
+    1077,
+    1078,
+    1066,
+    1068,
+    1077,
+    1080,
+    1069,
+    1080,
+    1070,
+    1069,
+    1076,
+    1062,
+    1063,
+    1062,
+    1055,
+    1066,
+    1056,
+    1056,
+    1055,
+    1063,
+    1055,
+    1055,
+    1053,
+    1054,
+    1065,
+    1064,
+    1054,
+    1064,
+    1056,
+    1055,
+    1057,
+    1064,
+    1064,
+    1056,
+    1058,
+    1067,
+    1066,
+    1055,
+    1057,
+    1058,
+    1068,
+    1078,
+    1063,
+    1075,
+    1074,
+    1061,
+    1062,
+    1074,
+    1075,
+    1075,
+    1074,
+    1079
+  ],
+  "pooled_x_rank_histogram": {
+    "2": 12,
+    "3": 24,
+    "4": 32,
+    "5": 24,
+    "6": 12
+  },
+  "schema": "p104-minimum-shared-space/1",
+  "scope": "Exact algebraic pooled-span minimum only; no chronological producer, transport price, supplier or new kappa.",
+  "targets": 104
+}

research/p104-minimum-shared-space/SOURCES.json

@@ -0,0 +1,51 @@
+{
+  "schema_version": 1,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "e8870e5917057d59b730eb14721a778639eca050",
+      "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7"
+    },
+    {
+      "path": "research/p104-native-channel/inputs/LOWRANK-RESULT.json",
+      "usage": "input",
+      "git_blob": "cbd1c6bdc9e34b25c64b2636ccd6acd2392232d4",
+      "sha256": "7143ec7780f6f38a8c294df8009c3621936b281d05ae79946ce22f581b73d1b1"
+    },
+    {
+      "path": "research/p104-native-channel/inputs/LOWRANK-WITNESS.json",
+      "usage": "input",
+      "git_blob": "86beaf424e9f0f800ae3a62797d94ec9386b7706",
+      "sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e"
+    },
+    {
+      "path": "research/p104-native-channel/inputs/P104-FIXTURE.json",
+      "usage": "input",
+      "git_blob": "2e16f99b295bb386fd13bd8fbd57b42ef54143a9",
+      "sha256": "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4"
+    }
+  ],
+  "predecessors": [
+    {
+      "pr": 2173,
+      "author": "Gonzalo Mier",
+      "head": "d9b784ca86fba060f0264370536ccd322c89998a",
+      "role": "Fixed pooled-span model, lower96 and upper97; explicit arbitrary-direction minimum handoff."
+    },
+    {
+      "pr": 1972,
+      "author": "Rohan Arun",
+      "head": "fd82d172f46933fd253c2c6de4bd5eaff5429cfd",
+      "role": "Frozen4058-event scalar/frame word."
+    }
+  ],
+  "credit": "Gonzalo Mier/2173 model and96..97 handoff; Rohan Arun/1972 scalar channel; Chafik Boukhalfa/1991 native binding; Adam Gall/1940 schedule; Josie Elliston/1071 fixture; retained Ali Romman/1125 and geometry lineage. No predecessor code imported."
+}