Bound BIT QUERY rank with 36 LOCAL calls (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-local-query-rank-bound/PROOF.md

@@ -0,0 +1,107 @@
+# Four QUERYs with retained BIT LOCAL stage incidence
+
+The pinned selected paired #7001 caller has 38 scalar roles per
+port pair, 111 replicated port pairs, 18 independent body
+variables and two real LOCAL calls per stage. Its exact target is
+diagonal with head factor $q$ on every role. Keep those 36
+LOCAL occurrences and that target. Allow arbitrary placement
+and constant conjugation of the LOCAL, QUERY and IDLE factors,
+including a fixed ambient space of auxiliary roles initialized and
+returned to zero. Constant gates are invertible. The scope retains each LOCAL's original stage assignment and its
+literal two-dimensional body contribution and rank-one head
+transvection. [Pinned #7001 source](https://github.com/CrocSwap/integer-mult-bounds/tree/e54523517d0f03e58352e647c403a5af3e525a57/research/paired-query-only-bit)
+
+## Independent stage derivatives
+
+Work over F₂ and write $q=1+\epsilon$ with $\epsilon^2=0$.
+Differentiate each body variable $z_s$ independently at all
+$z_s=1,q=1$. Normalize every event by its value at this base
+and conjugate by the accumulated constant prefix. The resulting
+normalized factors all have constant term the identity.
+
+At stage s each normalized LOCAL gives a rank-two projector P
+in the body derivative and a rank-one square-zero map N in the
+head derivative. Its original two local coordinates imply
+$PN=NP=N$, and conjugation preserves that identity. An IDLE
+serving s gives a rank-one projector. The sum of serving
+projectors equals the exact diagonal target projector E_s on the
+public input space A. The retained serving ranks sum to
+$\operatorname{rank} E_s$ for every stage, as checked on the
+actual word.
+
+This saturation holds with clean helpers too. The full body
+derivative has rank at least $\operatorname{rank} E_s$ from
+its restriction to A and at most the sum of serving ranks.
+Thus the images of the serving projectors are a direct sum
+whose sum is exactly $\operatorname{im} E_s\subseteq A$.
+On each serving image E_s acts as the identity. Uniqueness in
+the direct sum implies that all other serving projectors kill
+that image. In particular the two normalized same-stage LOCAL
+defects annihilate each other. This argument allows the LOCALs
+to be separated by arbitrary constant operations, other stages
+or QUERYs.
+
+## Head rank
+
+On A the normalized head derivative is the identity of rank
+38. Write its rank-one decomposition as UV, using the 36 LOCAL
+defects and r QUERY slots. For clean auxiliary roles, compress
+each QUERY defect to input and output A. Its rank is at most
+one. The LOCAL terms have image in A, and their reciprocal
+pairings and self-pairings stay zero under compression. The
+base whole word is the identity on A, so removing its constant
+factor does not change these public derivatives.
+
+From $UV=I_{38}$, the matrix $I-VU$ has rank
+$36+r-38$. On the two same-stage LOCAL indices it has a
+principal $2\times2$ identity minor. Thus its rank is at
+least two, so $r\ge4$. This does not require a trace or
+diagonal condition on compressed QUERYs. The argument extends
+the dual-number method from a fixed central cut to independent
+body stages and arbitrary placement.
+[Related dual-number scopes](https://github.com/CrocSwap/integer-mult-bounds/pull/6825),
+[Related rank method](https://github.com/CrocSwap/integer-mult-bounds/pull/6800)
+
+## Arbitrary idle masks with extra incidence
+
+Retain the same 36 LOCALs and target. At each stage the IDLE
+incidence cannot fall below the original required value, because
+the rank of the stage derivative is at most the sum of serving
+ranks. If every incidence stays equal, the rank argument above
+applies. Otherwise at least one stage has an extra incidence.
+
+For a required incidence vector $a_s$, form nested masks
+$S_j=\{s:a_s\ge j\}$. The sum of the k largest mask lengths
+in any realization is at most $\sum_s\min(k,a_s)$, which
+the nested masks attain for every k. Thus their sizes majorize
+every realization. Concavity of $r^{1-\kappa}$ makes the
+nested assignment cheapest even when granting unrestricted
+cross-stage mask grouping. The minimum is nondecreasing in
+each required incidence.
+
+At $\kappa=.0040075385047236$, all 18 directed profiles
+with one extra incidence cost more than four paid units per
+port above the original IDLE bill. The least is about
+4.08432343047. Deleting every QUERY would rebate only four
+per port. Thus an extra body incidence cannot make this
+lower-QUERY proposal price-positive, even with all packing
+and realization barriers waived. This concerns the retained
+LOCAL count and stage assignment, and the original rank-one QUERY and body-only IDLE charging rules.
+An IDLE mask contains distinct stages and pays rank seven per stage.
+Combined higher-rank QUERYs, altered IDLE operators and interfaces
+that erase live auxiliary data are outside this scope.
+
+The independent replay checks 1,444 original polynomial
+coefficients, all 18 stage derivatives, and the head rank.
+Changing one QUERY to a constant ADD keeps the base and body
+derivatives but changes the head derivative by rank one.
+Omitting one IDLE stage changes just that stage derivative by
+rank one. A two-helper padding control uses the added lanes
+inside a LOCAL and a QUERY and preserves all ranks. No caller
+with a smaller paid bill was built.
+
+Run with CPython 3.12 and assertions enabled from the repository root.
+
+```sh
+python3.12 -I -B research/bit-local-query-rank-bound/verify.py
+```

research/bit-local-query-rank-bound/README.md

@@ -0,0 +1,50 @@
+# BIT QUERY rank with 36 LOCAL calls
+
+**NO VERIFIED GAIN.** Retaining the selected #7001 paired caller's 36
+LOCAL stage assignments and exact 38-role endpoint requires at least four
+paid rank-one QUERY terms at the original stage incidence. The proof
+allows arbitrary constant bases and chronology, including initialized-clean
+helpers returned to zero. Granting arbitrary IDLE masks with extra
+incidence still cannot pay for reducing QUERY rank at the moonshot target.
+[Proof](PROOF.md) · [Exact receipt](RECEIPT.json)
+
+## Replay
+
+From a clean checkout, run with CPython 3.12 and assertions enabled.
+
+```sh
+python3.12 -B scripts/research_package.py --package research/bit-local-query-rank-bound
+```
+
+The replay authenticates three canonical paths, checks 1,444 original
+polynomial coefficients and 18 independent stage derivatives, and prices
+the 18 possible added stage incidences. It verifies a clean-helper padding
+control and detects dropped QUERY and body terms.
+
+## Scope and credit
+
+This proof concerns the existing LOCAL and IDLE tariff on the paired caller.
+It leaves changed LOCAL counts, native body rank, endpoint contracts and
+complete BIT/complex composition open. The strongest comparable κ remains
+0.003644407895539 on [#7156](https://github.com/CrocSwap/integer-mult-bounds/pull/7156).
+
+DreamingOfClouds supplied the chain-root BIT and empty-root-free lineage,
+CubeJerry the #6980 QUERY-only replacement, and zxv and the retained
+authors the #6726 native BIT lineage. The #7001 paired specialization
+supplies the literal controller. Credit Nick Petalas's
+[#6800](https://github.com/CrocSwap/integer-mult-bounds/pull/6800) rank method
+and [#6825](https://github.com/CrocSwap/integer-mult-bounds/pull/6825) for
+dual-number clean-column analysis of a different endpoint. The fixed-window
+[#6984](https://github.com/CrocSwap/integer-mult-bounds/pull/6984)
+audit specializes the body variable, while this result uses all 18
+independent body derivatives. Codex and subagents materially assisted the
+proof and replay. Apache-2.0.
+
+## Open next questions
+
+Retire one actual LOCAL and replace its head action by a QUERY and its body
+action by two stage incidences. The direct replacement adds paid moment.
+Can the two new incidences be paid for by changing the existing IDLE slots
+and preserving the complete polynomial endpoint? Start by determining
+which slots' normalized rank-one projectors can serve each stage. Reprice
+every new slot and incidence before building a caller.