Bound paired BIT volume across cover labels (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-full-cover-volume-cut/PROOF.md

@@ -0,0 +1,41 @@
+# Full-cover volume bound for two smaller BIT children
+
+## Exact interface
+
+The two fields are independent at the replacement boundary. Each is a binary function on the same complete cover rows C_w and physical address lattice Z_w over the admitted odd q-power digits. Extra common spectators can be included in Z_w. Write V_w = |C_w| |Z_w| for one field's volume. In each cover row g, the required difference-address map is T_g = g(I−2P)g⁻¹ with rank(P)=a, leaving the common sum address and spectators fixed. Each paid child is a fixed rational projector Q_i of proper positive rank r_i<a, acting at its current cover row by h(I−2Q_i)h⁻¹. The allowed digit primes make the rational chart and route denominators units.
+
+The proposed replacement has at most two chronological paid positions. It permits arbitrary pointwise binary mixing within a cover row, copying and scratch, and a finite sequence of fixed rational right cover routes, including routes that visit different cover labels for different roles or paths. These ordinary operations preserve the full physical address, although they may change the cover label or normalized coordinates. The finite path graph and rational route multipliers are width-independent. Pull back the common permissible external weight. There are no paid or ordinary address-changing operations besides the declared children in this replacement. The scope includes variable bank occupancies when every occupied cell is charged. It does not assume an actual lowered replacement in the current compiler.
+
+## Uniform bound on bypasses
+
+A chronological path ending at output cover g and using zero or one paid child acts on the physical difference address by g B_j g⁻¹. To see this, walk the fixed right multipliers backwards from g. The cover at the single child is g S_j for a fixed product S_j. In the zero-child case B_j is the identity. In the single-child case it is a rational conjugate of the corresponding child map. Its rank defect from identity is at most r_i<a. In particular B_j differs from T=I−2P. The index j ranges over the entire finite set of bypass paths, including those beginning in a different cover row. Pointwise scalar factors can suppress paths, which only reduces this set.
+
+For a fixed output cover g and a path j, the coincidence T_g z = g B_j g⁻¹ z has relative size at most q^(v_j−w) among all physical addresses, for all sufficiently large w. Multiply a nonzero rational row of T−B_j by a fixed denominator, and let v_j be the minimum q-adic valuation of its nonzero entries. A coefficient of valuation v_j gives the stated bound by counting that coordinate after fixing all others. The bijection z↦g⁻¹z makes the bound uniform in g. If there are no bypass paths use zero as the bound. The finite union bound ε_w tends to zero. The other physical coordinates are unchanged and can be counted as spectators.
+
+The same argument applied to all paths shows that a successful replacement needs a path with rank sum at least a. Indeed, the rank defect of a product is at most the sum of its factors' defects, from I−AB=(I−A)+A(I−B). If all sums were below a, a generic physical address could never reach its required output coordinate. This also excludes any single proper child, regardless of volume.
+
+## Count distinct cells across all cover labels
+
+Fix a single **physical** input address z common to all cover rows, rather than a common normalized address. Call g good at z when every bypass misses the output address T_g z. Restrict inputs to both roles at physical z on those good rows, and restrict outputs to the corresponding two target cells at each good row. The required matrix is a permutation of an identity of rank 2 times the number of good rows. Because all bypasses to those outputs were excluded from **every** input cover, the restricted actual matrix factors through the first paid child's input cells at physical z. All ordinary operations before that child preserve z. Paths may use different cover labels, but one bank cell at a given physical z and label contributes at most one to the rank, even if many paths reuse it. Thus the first child needs at least 2 times the number of good rows at z in distinct charged cells. This rank argument permits arbitrary cancellations among paths that use the child.
+
+Sum over z. The slices are disjoint within the first bank. The uniform bound says that the number of good (g,z) pairs is at least (1−ε_w)V_w. Hence the first child's charged volume is at least 2(1−ε_w)V_w. For the second child apply the same argument to the transposed chronological network, with roles of input and output exchanged. Right routes invert, ordinary transposes still preserve physical address, and the child and target projector permutations invert to themselves. Rectangular scratch maps transpose as well. This gives the same volume bound for the second bank. For one complete bank field per cover row, even a single fixed physical slice with more than half the rows good is impossible. With variable bank volume, the limiting coefficient of each child is at least two full fields.
+
+The argument also applies to m simultaneous independent fields on this domain when both child ranks are below every target rank by summing the identity ranks for the good field/cover cells and applying the finite union bound uniformly. This supports aggregation of genuinely simultaneous field instances. It does not justify grouping different caller times with intervening paid work into a two-child replacement. A shared bank may not be billed twice as though independently available at disjoint chronological replacements.
+
+## Full-caller stock and price
+
+The exact #7001 export has 32 IDLE_ONE events and 16 equal-mask pairs. Seven pairs have no intervening touch of either role in the original order, accounting for 777 placements across 111 ports. For each of the other nine pairs, the later IDLE's own role is untouched before it fires. An operation on its independent field commutes with each intervening event that uses disjoint roles. The fixed stage mask is explicit in the event. The verifier moves each later IDLE left in the same caller, performs 243 individually checked disjoint-role adjacent swaps, and leaves all 16 pairs adjacent simultaneously. The pinned #7001 forward evaluator checks all 1,444 formal coefficients before and after. No native event, QUERY, mask or paid rank is removed. This caller-level reordering is an overgrant for the finite physical schedule and route bill.
+
+There are therefore **1,776** distinct candidate pair placements under the formal adjacent schedule, including **222** rank-56 placements. The stock counts each old paid event/port once. If a new fixed-tape condition rejects an adjacent placement it only reduces this stock. The argument keeps other caller events and paid fields separate from each local two-child replacement.
+
+Put H_r=r^(1−κ). For two positive proper ranks the path condition gives r₁+r₂≥a, and the capacity bound charges at least 2V(H_r₁+H_r₂) in leading paid volume. Monotonicity and strict concavity give the minimum at ranks (1,a−1), and this is strictly greater than the old 2V H_a. Therefore the aggregate optional saving is exactly **zero**, even if all 1,776 candidate placements could be replaced independently. The directed minimum surcharge if all 1,776 are replaced is about 59.952168596218 normalized raw units at the target. The 777 quiet original placements alone would add about 27.43486935603151. For the literal pair of rank-49 factors replacing rank 56, the surcharge is about 82.75903922 per pair. Exact directed endpoints and both caller deficits are in RESULT.json.
+
+The whole #7001 BIT invoice remains about **60.10389921914735** raw units below the target, and about **60.345980724331845** at the stricter trial. This upper grants free new setup, route formation, ownership, restoration, precision and fixed-tape costs. It permits the removal of old ordinary work within these slots, which cannot change the necessary raw inequality. It retains all other paid positions and productive targets. No new ordinary budget or compiler admission is claimed.
+
+## Verification and scope
+
+The checker authenticates the literal caller, existing full invoice, canonical forward evaluator and directed interval implementation at exact canonical e54523517d0f03e58352e647c403a5af3e525a57. It recounts every pair and intervening contact, checks the full reordered formal endpoint, recomputes the raw shortfalls and prices, and checks three complete finite physical address grids in a synthetic two-cover model. The model permits label-changing intake and release. Its paid maps compose to the target at either fixed label, but the globally selected four independent values factor through two bank cells with a one-field bank. The argument above proves the all-width claim. The finite controls illustrate why both the common physical slice and the global cover rank matter.
+
+Pivot away from at most two smaller children with unchanged ordinary addressing. Three or more paid children, new ordinary physical-address maps, changed ambient or width-dependent routes are different mechanisms and need their own whole-construction bound. The proof does not certify any candidate, κ gain, or physical compiler.
+
+Credit CubeJerry #7001, #6726/#6834/#6980 and the delayed-cover authors for the retained word, address action and whole-role route; #7163 and #7190 for related reflection-rank and grade-preserving bounds; the Round 16 port-1 and two-cover proof for the local obstruction and collision example; and Clear1nsight #7161 for the complete comparable benchmark. Codex and subagents materially assisted.

research/bit-full-cover-volume-cut/README.md

@@ -0,0 +1,23 @@
+# Bound both paid BIT bank volumes across cover labels
+
+**κ change 0%.** Two proper-rank BIT projector children, with ordinary operations preserving the physical address, each need at least two original field volumes to replace two independent equal-mask IDLE fields. Fixed right cover routes may visit different labels. A global rank cut uses one common physical address and all good cover labels at once, so each bank cell is counted once.
+
+The exact #7001 caller has **1,776 same-mask same-port pair placements** after a checked disjoint-role reorder. This includes 777 quiet placements in the original order. The best total paid saving is **zero** even with free new setup, routing, ownership, restoration, precision and tape. The full raw BIT gap is about **60.10389921914735** at κ = 0.0040075385047236. The reorder preserves all 1,444 formal coefficients. Finite route and tape admission remain separate. [Proof](PROOF.md) · [Exact directed receipt](RESULT.json)
+
+## Clean replay
+
+From a clean checkout, run with CPython 3.12 and assertions:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/bit-full-cover-volume-cut
+```
+
+Four exact in-tree #7001 files bind the literal caller, invoice, canonical forward evaluator and directed arithmetic. The checker reconstructs all mask pairs, every intervening contact, both raw deficits and the charged lower tariff. It checks complete address grids for digit cardinalities 3, 5 and 9. The written proof supplies the all-width result. The corrupt-source and changed-receipt controls reject.
+
+## Open next questions
+
+Can a third paid child create a different cost mechanism? Before choosing any site, bound the middle bank's volume under distinct incoming physical address maps, count the compatible caller slots, and compare their total optimistic credit with the full deficit. Width-dependent routes, new ordinary physical address maps and cross-pair schedules with intervening paid work remain outside this result.
+
+## Credit
+
+CubeJerry #7001 supplied the retained caller and invoice. Credit #6726/#6834/#6980 and the delayed-cover authors for the native and whole-fibre projector lineage, #7163/#7190 for earlier rank bounds, and the Round 16 #7111 two-cover pilot. Clear1nsight #7161 supplies the comparable complete benchmark. OpenAI Codex and subagents materially assisted. Apache-2.0.