Bound generalized BIT summary support (0% κ change)

docs/ci-verification.md

@@ -1,8 +1,25 @@
 # CI verification
 
-## Current selected-family replay: #6030
+## Current selected-family replay: #7000 with #7001
 
 The [selected record](../certificates/selected-result.json) binds conditional
+κ = 0.00363005817 to the [application review](research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md),
+[validation receipts](research/pr-intake-evidence/pr7000-application/VALIDATION.json),
+and [explicit source closure](../certificates/frontier7000-source.json).
+`make frontier7000-verify` follows that exact-source selected replay. The review
+reuses eleven authenticated preceding executions and records seven fresh serial
+application, scalar and complete native-catalogue executions. The earlier
+monolithic timeout is retained separately and is not completed coverage.
+Consult the receipts for exact commands, source heads and limits.
+
+The five inherited framework assumptions remain. No complete uniform word,
+literal multiplier execution, independent human proof or formal-kernel proof
+is asserted. Routine research submissions do not need to rerun this
+selected-family replay. The sections below preserve historical checkpoints.
+
+## Historical selected-family replay: #6030
+
+The [historical checkpoint](../certificates/checkpoints/frontier6030.json) binds conditional
 κ = 0.003125804 to the [proof review](research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md),
 [validation receipts](research/pr-intake-evidence/pr6030-audit/VALIDATION.json),
 and [explicit source closure](../certificates/frontier6030-source.json).

research/bit-generalized-summary-support/PROOF.md

@@ -0,0 +1,120 @@
+# Generalized support bound for selected BIT summary descents
+
+Fix the paired #7001 native word, its rational chart catalogue and
+its monotone source flow. The only new downward transports are
+collectors descending to chart zero. A new collector can use
+earlier descended values. Take its main-coordinate row modulo
+the span of those earlier values and all retained summary rows.
+Co-chart XOR, zero initialization and monotone transport preserve
+support on the original lines contained in the current chart
+in this quotient. Subtract earlier rows in chronological order
+to obtain supported innovations without changing the span of
+all rows available for recovery. Timing and recovery are otherwise
+overgranted.
+
+The nine literal summary rows projected onto 111 original main
+coordinates generate a binary code C of dimension nine. Its
+minimum nonzero weight is 48 and its minimum support union for
+a two-dimensional subspace is 75. The 111 coordinate functionals
+are distinct and nonzero on C. The replay verifies these facts
+from the pinned word and checks all catalogue capacities and
+2,862 public monotone MOVEs.
+
+## Paid rank budget
+
+Let k of the nine summary rows be replaced, at the target
+κ=0.0040075385047236, and write p=1−κ. Require at least 5/3
+net paid units per native copy. This is a relaxation of the
+full target deficit per 36 repeated copies. The cost of the
+k old descents is k·7^p. All catalogue ranks are at most eight.
+For total new rank R, the cost is at least R·8^(−κ).
+If R≥7k−1, the saving is at most
+7^(−κ)+(7k−1)(7^(−κ)−8^(−κ)), which is at most
+1+62κ/7 by the mean value theorem and log(8/7)≤1/7.
+This is strictly below 5/3. Therefore R≤7k−2.
+
+## Two support tests
+
+Choose linear XOR recovery for the k independent summary
+rows modulo the retained rows. Cancel the coefficients of
+the k−t highest-rank collectors in those recovery equations.
+At least t independent target combinations remain. Select
+a t-dimensional subspace of their codeword representatives
+in C. Every column outside the union of the remaining
+collectors is zero in this subspace.
+
+The support union must have size at least d_t, the minimum
+support of a t-dimensional subspace of C. For t≥2,
+averaging the two-dimensional subspaces gives the bound
+ceil((2^t−1)·75/(3·2^(t−2))). Indeed, a nonzero coordinate
+functional on a t-space occurs in a fraction
+3·2^(t−2)/(2^t−1) of its two-dimensional subspaces.
+Distinct nonzero columns also give d_t≥112−2^(9−t),
+since the kernel of restriction to a t-space has dimension
+9−t. Use the larger lower bound.
+
+There is a second necessary condition on the sum I of
+the remaining collectors' support sizes. A rank-t linear
+map of the original nine-dimensional column space can
+repeat an output column at most 2^(9−t) times. At least
+112−2^(9−t) output columns are nonzero. With N remaining
+collectors, each nonzero column incident to at most h
+collectors is the sum of at most h of the N coefficient
+vectors. There are at most sum(j=1..h, binomial(N,j))
+possible subsets. Thus for each h≥0 the number of columns
+incident to more than h collectors is at least
+
+```text
+max(0, 112−2^(9−t) − 2^(9−t)·sum(j=1..h, binomial(N,j))).
+```
+
+Summing these bounds over h bounds I below. The catalogue
+capacities bound I above, even with overlapping charts
+overcounted. This argument also permits a collector to
+use only part of the support of its chart.
+
+## Exact enumeration and pair test
+
+Enumerate sorted rank histograms within R≤7k−2. Keep only
+profiles whose tail after dropping k−1 collectors can
+cover 48 lines. This precondition is necessary. The
+enumeration exhausts 18, 74, 270 and 782 histograms for
+k=6,7,8,9. The two support tests leave zero, zero, one and
+three profiles, respectively.
+
+The k=8 profile has nine rank-six transports. Two k=9
+profiles have ten rank-six transports or one rank-seven
+and nine rank-six transports. In each of these three
+profiles there are k+1 transports. Cancel every transport
+except a chosen pair of rank-six collectors. This imposes
+k−1 homogeneous conditions on k target coefficients and
+leaves a nonzero codeword supported in the union of that
+pair. Equal masks cover at most 30 lines and fail immediately.
+For every one of the 16,110 distinct pairs, the columns
+outside that union have rank nine. Hence no nonzero
+codeword can be supported in the pair and all three
+profiles fail.
+
+The final profile has ten rank-six collectors and one rank-one
+collector. Cancel eight rank-six collectors and retain any two
+rank-six collectors plus the rank-one collector. The eight
+conditions leave a nonzero codeword. Its support must lie in
+the union of the pair and at most one extra coordinate, since
+each rank-one chart contains at most one original line. A
+repeated pair plus one line covers at most 31 coordinates.
+
+For a distinct pair, let D be the matrix of columns outside
+the pair. The condition requires rank(D)<9 or a column whose
+deletion drops rank. The verifier tracks the input columns in
+each row reduction. Each dependent column yields a relation
+with its own last nonzero index. These relations form a basis
+of the column kernel, so a column lies in some relation exactly
+when it appears in a basis relation. Deleting a column lowers
+rank precisely when it lies in no relation. All 16,110 matrices
+have rank nine and zero such columns. A separate direct codeword
+enumeration over the same pairs also finds zero with uncovered
+weight at most one. This excludes the last profile. The extra
+line is allowed to differ arbitrarily between pairs in the test.
+
+The exclusion leaves smaller paid savings, changed chart spaces,
+nonmonotone transports and new target contracts open.

research/bit-generalized-summary-support/README.md

@@ -0,0 +1,46 @@
+# Generalized support bounds for joint BIT summary replacements
+
+**NO VERIFIED GAIN.** On the exact selected paired #7001 word,
+no six- through nine-summary replacement under the fixed monotone
+catalogue can save the target 5/3 paid units per native copy.
+The final profile has ten rank-six collectors and one rank-one
+collector. It fails even with an arbitrary extra line.
+
+The summary code has minimum two-dimensional support 75 and
+111 distinct nonzero columns. The proof combines generalized
+support, column incidence and a projected rank test on all
+16,110 distinct rank-six chart pairs. [Proof](PROOF.md)
+
+## Replay
+
+Use a clean checkout and CPython 3.12.
+
+```sh
+python3.12 -B scripts/research_package.py --package research/bit-generalized-summary-support
+```
+
+The verifier reconstructs the weights and chart masks from the
+canonical pinned BIT word, exhausts the four histogram domains,
+and checks all pair exclusions by rank of the uncovered columns,
+including the effect of deleting any one column. Positive and
+negative projection controls run from the same word.
+The exact dependency is the existing selected BIT word. [Selected BIT package](../paired-query-only-bit/README.md)
+
+## Scope and credit
+
+[#7146](https://github.com/CrocSwap/integer-mult-bounds/pull/7146)
+covers up to four summaries and the five-summary target scope.
+This package covers larger joint changes with different support
+bounds. Ali Romman's #5421 supplied the owned relations.
+DreamingOfClouds, zxv, CubeJerry and the retained authors supplied
+the native and paired-controller lineage. Substantial OpenAI Codex
+and subagent assistance. Apache-2.0.
+
+## Open next questions
+
+Can an existing public MOVE be redirected to import a summary
+row across a nonmonotone chart change? Start with a nested,
+equal-paid-rank redirect in the literal word. Check source
+availability, exact output rows and restoration before recomputing
+the paid and ordinary invoices. This proof fixes monotone public
+transport, so that changed source flow is outside its scope.

research/bit-generalized-summary-support/RECEIPT.json

@@ -0,0 +1,125 @@
+{
+  "dependencies": {
+    "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78"
+  },
+  "profiles": {
+    "6": {
+      "survivors": [],
+      "tested": 18
+    },
+    "7": {
+      "survivors": [],
+      "tested": 74
+    },
+    "8": {
+      "survivors": [
+        [
+          6,
+          6,
+          6,
+          6,
+          6,
+          6,
+          6,
+          6,
+          6
+        ]
+      ],
+      "tested": 270
+    },
+    "9": {
+      "survivors": [
+        [
+          6,
+          6,
+          6,
+          6,
+          6,
+          6,
+          6,
+          6,
+          6,
+          6
+        ],
+        [
+          6,
+          6,
+          6,
+          6,
+          6,
+          6,
+          6,
+          6,
+          6,
+          6,
+          1
+        ],
+        [
+          7,
+          6,
+          6,
+          6,
+          6,
+          6,
+          6,
+          6,
+          6,
+          6
+        ]
+      ],
+      "tested": 782
+    }
+  },
+  "rank_six_pair_complement_ranks": {
+    "9": 16110
+  },
+  "rank_six_pair_deletion_rank_drops": {
+    "0": 16110
+  },
+  "remaining_profiles": [],
+  "required_support_by_dimension": {
+    "1": 48,
+    "2": 75,
+    "3": 88,
+    "4": 94,
+    "5": 97,
+    "6": 104,
+    "7": 108,
+    "8": 110,
+    "9": 111
+  },
+  "status": "PASS_GENERALIZED_BIT_SUMMARY_SUPPORT",
+  "weights": {
+    "d1": 48,
+    "d2": 75,
+    "distinct_columns": 111,
+    "enumerated_pairs": 130305,
+    "maximum_column_multiplicity": 1,
+    "minimizing_subspaces": 216,
+    "status": "PASS_GENERALIZED_SUMMARY_SUPPORT",
+    "union_weight_histogram": {
+      "75": 648,
+      "76": 2466,
+      "77": 4236,
+      "78": 4494,
+      "79": 5715,
+      "80": 10692,
+      "81": 14526,
+      "82": 12462,
+      "83": 10452,
+      "84": 14700,
+      "85": 16098,
+      "86": 10854,
+      "87": 6408,
+      "88": 6315,
+      "89": 5418,
+      "90": 2790,
+      "91": 972,
+      "92": 252,
+      "93": 42,
+      "111": 765
+    },
+    "word_sha256": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78",
+    "zero_columns": 0
+  }
+}

research/bit-generalized-summary-support/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz",
+      "usage": "input",
+      "git_blob": "b718d6b2848215ad785022106dfa9f871a3d1c0c",
+      "sha256": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78"
+    }
+  ]
+}