Bound BIT middle-bank volume by cover orbit (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-cover-orbit-grade/PROOF.md

@@ -0,0 +1,47 @@
+# Middle bank capacity from a grade on each cover orbit
+
+## Scope
+
+Use the retained #7001 BIT whole-fibre interface and the two independent equal-mask fields counted in [#7201](https://github.com/CrocSwap/integer-mult-bounds/pull/7201). A field has complete cover labels g in GL_d(R) and a complete physical difference-address lattice R^d at admitted odd prime-power digit cardinality s, where R=Z/sZ. A common sum address, the other columns and spectators can be included in the per-field volume V. Choosing a grade on one fixed admitted column suffices, with the projector and right-route matrices acting componentwise. In a row g, the prescribed action on each field is T_g=g(I−2P)g⁻¹ with rank(P)=a. This leaves the cover label, role and other physical addresses unchanged. Pull back the permitted common weight.
+
+The proposed replacement has three chronological paid projectors of positive proper ranks r₁,r₂,r₃. Every two ranks sum to less than a. Each paid projector Q_j acts by a reflection g(I−2Q_j)g⁻¹ in its current row, as an involutive permutation of its charged bank cells. All ordinary linear operations preserve physical addresses. Scalar mixing is within a cover row, and a finite list of fixed right multipliers S may move among rows. This list and the projector matrices are width-independent, with denominators and route determinants invertible at the admitted odd prime. All occupied bank cells, including extra role or spectator slices, are charged. The replacement acts on one pair at a time. Sharing a paid bank across distinct pairs or adding address-changing ordinary work changes the contract.
+
+## An invariant subspace suffices
+
+Let W be a nonzero rational row subspace invariant under every right multiplier, contained in
+
+    { l : lP=l, lQ₁=0, lQ₃=0 }.
+
+An individual row need not be fixed by the multipliers. Let K_w be the subgroup of GL_d(R) generated by their reductions. Its right cover orbits are g₀ K_w. Choose any nonzero primitive integer row l₀ in W by clearing denominators and dividing out the common factor. On the whole orbit choose the *physical* grade z ↦ l₀ g₀⁻¹ z. It has equal-sized residue fibres, since at least one coefficient is a unit mod the underlying prime.
+
+For g=g₀S with S in K_w, the normalized row for this same physical grade is l₀S. Rational invariance extends to the group including inverses, and the required projector identities reduce modulo s because the fixed denominators are units. In particular l₀S P=l₀S and l₀S Q₁=l₀S Q₃=0. The outer children and ordinary operations preserve this orbit's physical grade. Both required external actions negate it. A right multiplier can negate or mix the normalized rows in W while leaving the orbit grade unchanged. Different orbits can use different physical grades, since no declared operation connects their rows.
+
+The verifier computes the largest such W. In column coordinates, start with the span of the columns of I−P, Q₁ and Q₃. Close it under all S by adding the image of every new basis vector. Its annihilator is W. Closure under the invertible generators gives closure under their inverses. At most d independent vectors enter the queue.
+
+## Middle bank lower bound
+
+In each orbit select one grade from every nonzero pair {v,−v}. In the target matrix, select input columns on these grades and output rows on the opposite grades, including both independent fields. The target restriction is a permuted identity of rank V_orbit(1−1/s), where V_orbit counts one full field in that orbit. The grade-preserving operators contribute zero to the selected minor.
+
+Modify the middle involution only by replacing each transposition whose two endpoints have different grades by two fixed points. This makes the entire reference network preserve the orbit grade. Each replaced transposition has a rank-one difference over F₂ on its two cells. Thus the full middle difference has rank at most V₂/2 over all charged cells, even if some middle transpositions are grade-preserving or change the grade by something other than negation. Multiplying this difference on each side by the ordinary and outer maps cannot increase rank. The selected target minor, summed across disjoint orbits, forces
+
+    V₂ ≥ 2(1−1/s) V.
+
+The asymptotic charged middle volume is at least 2V. This argument counts each cell once, regardless of the number of useful prefix address maps into it.
+
+The fixed-physical-address input and transposed output cuts of #7201 also force first and last volume at least 2V asymptotically. Their bypass argument applies here because any path omitting a given child uses at most two paid reflections. Its rank defect is below a. The finite list of rational bypasses misses the target at all but a vanishing address fraction uniformly in the cover label. The exact target also needs some path with rank sum at least a. These are necessary all-width statements, including when the paid volumes differ.
+
+## Full price and controls
+
+For H_r=r^(1−κ) and 0<κ<1, the leading paid bill is at least 2V(H_r₁+H_r₂+H_r₃). Among positive ranks with sum at least a the concave sum is minimized at (1,1,a−2). That bill is strictly above the old 2V H_a. The result grants new setup, routing, ownership, restoration, precision and tape free. Removal of ordinary work cannot close the separate negative raw paid margin.
+
+The literal stock has 16 equal-mask pairs at 111 ports, or at most 1,776 distinct placements. #7201 gives a simultaneous formal reorder placing those pairs adjacently. Credit each old event and port at most once, and grant all these placements if their candidate tables satisfy the orbit criterion. The best aggregate optional recursive saving is zero. The exact old raw deficit is approximately 60.10389921914735 at target 0.0040075385047236. Forced replacement of all 1,776 qualifying pairs adds at least about 119.16019753858147 at this target. The exact interval receipt also encloses the stricter trial.
+
+The explicit port-1 table uses old active axes 8 through 63. The outer rank-one projectors use 8 and 63. The tested right multiplier swaps those two axes and negates every middle coordinate. The 54-dimensional grade space is invariant although its fixed normalized subspace is zero. The separate full binary-table replay finds the same failed one-field middle action. A control cycling all 56 active axes erases the invariant grade space. A zero space leaves the grade criterion silent.
+
+The small controls use two distinct cover orbits, choose a different physical grade in each, and exhaust the three-dimensional address grids at digit cardinalities 3, 5 and 9. They check both outer actions preserve grade, the middle reflection is involutive, and the selected target and crossing-transposition ranks are exact. The controls corroborate the finite counts. The proof supplies the all-width volume bound.
+
+## Next question
+
+A candidate that could reduce the middle volume must escape this grade criterion. For rank sum exactly a there is a further exact path test. Express the three projectors in one physical coframe. If their reflected product equals I−2P, the telescoping image lies in the sum of their image spaces. Rank equality forces those spaces to be a direct sum equal to im(P). Project the telescoping identity onto each summand in chronological order. It gives Q₁ as the first component of P, then Q₂ and Q₃ as the remaining components, since earlier reflections act diagonally on the already determined components. Thus the useful-path projectors mutually annihilate and sum to P. A future width-independent table should check this identity and the full independent field response before crediting any saving. The charged physical compiler and tape remain outside this proof.
+
+Credit CubeJerry #7001 and the #6726/#6834/#6980 native/caller lineage, the delayed-cover authors for whole-fibre right routing, #7163/#7190/#7201 for the rank and physical-address cut arguments, and Round 17–18 of #7111 for the three-child price and explicit port-1 table. Clear1nsight #7161 supplies the comparable complete result. OpenAI Codex and subagents materially assisted.

research/bit-cover-orbit-grade/README.md

@@ -0,0 +1,23 @@
+# Bound the middle BIT bank with a grade on each cover orbit
+
+**κ change 0%.** For three mandatory smaller BIT children, a grade can be fixed in physical coordinates throughout a cover orbit even when no nonzero normalized middle covector is fixed by the right routes. If the grade is preserved by the outer children and negated by the target, the middle bank needs at least two original field volumes asymptotically.
+
+The exact rank-(1,54,1) example has a **54-dimensional invariant grade space** and zero pointwise fixed normalized middle grades. The best optional saving across the upper stock of **1,776** qualifying equal-mask pairs is **zero**. The raw BIT shortfall remains about **60.10389921914735** at κ = 0.0040075385047236. [Proof](PROOF.md) · [Directed receipt](RESULT.json)
+
+## Clean replay
+
+From a clean checkout, use CPython 3.12 with assertions:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/bit-cover-orbit-grade
+```
+
+The three exact in-tree #7001 files bind the caller, invoice and interval arithmetic. The verifier computes the invariant subspace by exact rational elimination, checks two distinct cover orbits at digit cardinalities 3, 5 and 9, and prices the entire stock. An active-cycle control makes the invariant subspace zero. The written argument supplies the uniform bank bound.
+
+## Open next questions
+
+First check whether an explicit width-independent route table escapes the invariant grade. A passing table still needs the exact independent output and ownership return, a charge for every bank and route, and sufficient compatible stock. More than three children, new physical addressing, cross-pair sharing and a new compiler or fixed tape remain separate work.
+
+## Credit
+
+CubeJerry #7001 supplied the retained caller and tariff. Credit #6726/#6834/#6980 and the delayed-cover authors for the native projector and whole-fibre route, #7163/#7190/#7201 for rank cuts, and Round 17–18 of #7111 for the three-child price and port-1 table. Clear1nsight #7161 supplies the comparable complete result. OpenAI Codex and subagents materially assisted. Apache-2.0.

research/bit-cover-orbit-grade/RESULT.json

@@ -0,0 +1,97 @@
+{
+  "directed_prices": [
+    {
+      "kappa": "10018846261809/2500000000000000",
+      "minimum_surcharge_if_all_1776_qualifying_pairs_replaced": [
+        "37237561730806710280273622060132269175657637603942500856988016446371157893964287/312500000000000000000000000000000000000000000000000000000000000000000000000000",
+        "1489502469232268411210944882405290767026305504157700034279520657854846315760424847/12500000000000000000000000000000000000000000000000000000000000000000000000000000"
+      ],
+      "optimistic_optional_saving": [
+        "0",
+        "0"
+      ],
+      "rank56_minimum_surcharge": [
+        "1987475115419346443791243482654398889011659993518261434873732404912546021035261/25000000000000000000000000000000000000000000000000000000000000000000000000000000",
+        "1987475115419346443791243482654398889011659993518261434873732404912546021038979/25000000000000000000000000000000000000000000000000000000000000000000000000000000"
+      ],
+      "unchanged_raw_deficit": [
+        "1502597480478683846599820932032388206481822134974419886612337024425207154047098731/25000000000000000000000000000000000000000000000000000000000000000000000000000000",
+        "1502597480478683846599820932032388206481822134974419886612337024425207154056670591/25000000000000000000000000000000000000000000000000000000000000000000000000000000"
+      ]
+    },
+    {
+      "kappa": "1002040748181/250000000000000",
+      "minimum_surcharge_if_all_1776_qualifying_pairs_replaced": [
+        "372433168503855787580633820837916137496637723018601368302261410692227385028968163/3125000000000000000000000000000000000000000000000000000000000000000000000000000",
+        "744866337007711575161267641675832274993275446037202736604522821384454770058865063/6250000000000000000000000000000000000000000000000000000000000000000000000000000"
+      ],
+      "optimistic_optional_saving": [
+        "0",
+        "0"
+      ],
+      "rank56_minimum_surcharge": [
+        "248472730614166807967532357336170877714912648678154713803329809186735812970697/3125000000000000000000000000000000000000000000000000000000000000000000000000000",
+        "1987781844913334463740258858689367021719301189425237710426638473493886503769323/25000000000000000000000000000000000000000000000000000000000000000000000000000000"
+      ],
+      "unchanged_raw_deficit": [
+        "1508649518108296133439099805441247369369954037474358092796307749315623322655158281/25000000000000000000000000000000000000000000000000000000000000000000000000000000",
+        "377162379527074033359774951360311842342488509368589523199076937328905830666216337/6250000000000000000000000000000000000000000000000000000000000000000000000000000"
+      ]
+    }
+  ],
+  "finite_controls": [
+    {
+      "cover_orbits": 2,
+      "digit_cardinality": 3,
+      "field_volume": 108,
+      "one_middle_field_rank_defect": 36,
+      "required_middle_field_multiplier": 2,
+      "target_minor_rank_two_fields": 72
+    },
+    {
+      "cover_orbits": 2,
+      "digit_cardinality": 5,
+      "field_volume": 500,
+      "one_middle_field_rank_defect": 200,
+      "required_middle_field_multiplier": 2,
+      "target_minor_rank_two_fields": 400
+    },
+    {
+      "cover_orbits": 2,
+      "digit_cardinality": 9,
+      "field_volume": 2916,
+      "one_middle_field_rank_defect": 1296,
+      "required_middle_field_multiplier": 2,
+      "target_minor_rank_two_fields": 2592
+    }
+  ],
+  "pair_stock_total_upper": 1776,
+  "pair_stock_upper": {
+    "7": 222,
+    "14": 222,
+    "21": 222,
+    "28": 222,
+    "35": 222,
+    "42": 222,
+    "49": 222,
+    "56": 222
+  },
+  "pins": {
+    "EFREE-CALLER.json.gz": "757b3523798f840bdb02028b23708c3416627a99ea09e7a3c4bcdc5cd0c7ce4b",
+    "EFREE-RESULT.json": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b",
+    "independent/interval_gate.py": "8dc2bc4c64cba3f83c664373984a075f1a14b4d53958084091345c8cab189dec"
+  },
+  "rank56_layout": {
+    "ambient": 127,
+    "cycle_control_orbit_grade_space": 0,
+    "initial_grade_space": 54,
+    "middle_rank": 54,
+    "orbit_grade_space": 54,
+    "outer_ranks": [
+      1,
+      1
+    ],
+    "pointwise_fixed_middle_grades": 0,
+    "target_rank": 56
+  }
+}

research/bit-cover-orbit-grade/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "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/EFREE-CALLER.json.gz",
+      "usage": "input",
+      "git_blob": "f022272a8d51ede841778dec76e2bfb24b614d04",
+      "sha256": "757b3523798f840bdb02028b23708c3416627a99ea09e7a3c4bcdc5cd0c7ce4b"
+    },
+    {
+      "path": "research/paired-query-only-bit/EFREE-RESULT.json",
+      "usage": "input",
+      "git_blob": "575f76487f9999ecc3e7b1b70f9f71bc582ef8a8",
+      "sha256": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b"
+    },
+    {
+      "path": "research/paired-query-only-bit/independent/interval_gate.py",
+      "usage": "input",
+      "git_blob": "6d5a751dde7554b2bb3ccb9a958a3508d74ea155",
+      "sha256": "8dc2bc4c64cba3f83c664373984a075f1a14b4d53958084091345c8cab189dec"
+    }
+  ]
+}