Bound the paired BIT schedule at the moonshot target (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-paired-schedule-bound/PROOF.md

@@ -0,0 +1,141 @@
+# Paired BIT schedule bound at the fixed target
+
+Keep the exact 38-role clean endpoint in the selected #7001 paired BIT
+caller, its 18 independent body variables, the retained native invoice
+per LOCAL, and the rank-one QUERY and body-only distinct-stage IDLE
+tariffs. Allow arbitrary placement and invertible constant bases and
+additional auxiliary roles initialized and restored to zero. The native
+count and its stage multiplicities may vary. The signed paid moment is
+strictly negative at κ = 0.0040075385047236 throughout this family.
+
+## Rank conditions
+
+Normalize each factor at q=1 and all body variables equal to 1, and
+conjugate its derivative by the accumulated constant prefix. The
+target stage derivatives E_s are the pinned diagonal projections on
+public space A. A LOCAL contributes a rank-two stage projector P
+and a square-zero rank-one head defect N with PN=NP=N. QUERY gives
+a square-zero rank-one head defect. An IDLE serving s gives a rank-one
+stage projector.
+
+Let n be the number of LOCALs and q_count the number of QUERYs.
+The complete head derivative factors as UV with n+q_count rank-one
+terms and restricts to the identity on A. V embeds A into the
+fixed space of VU, so rank(I−VU)≤n+q_count−38. Each diagonal
+pairing of VU is zero by square-zero, forcing q_count≥39−n.
+
+A stage is saturated when its serving ranks sum to rank(E_s).
+In a saturated stage, the images of all its projectors form a
+direct sum equal to im(E_s), by the full ambient rank and the exact
+clean restriction. They annihilate one another, since E_s is the
+identity on that sum. Each LOCAL head defect stays inside the
+column and row support of E_s. The head terms of any a same-stage
+LOCALs give a principal identity block of size a in I−VU.
+
+The 81 opposite-arm pairs have the same two common root coordinates,
+0 and 19, in their diagonal E_s supports. For opposite stages with a
+and b LOCALs, the principal block of I−VU has diagonal blocks I_a
+and I_b. Both cross blocks factor through the two root coordinates,
+so the Schur complement has rank at least b−2. If a and b denote
+the actual largest multiplicities in the two arms, then at full
+saturation
+
+```text
+q_count ≥ max(0, 39−n, 38−n+max(a,b,a+b−2)).
+```
+
+## The price of IDLE masks
+
+Write f(r)=r^(1−κ). For fixed per-stage demands d_s, nested masks
+{ s : d_s ≥ j } minimize the moment. For every k their k longest
+lengths sum to ∑ min(k,d_s), an upper bound for any k masks.
+Concavity of f gives the cost lower bound.
+
+Each saturated IDLE projector crossing arms has its image and row on
+the two root coordinates. At most two cross incidences can serve a
+stage. Splitting a mask of x left stages and y right stages costs
+111[f(7x)+f(7y)−f(7(x+y))]. By concavity and the decrease of f(r)/r,
+this is at most h(x+y), with h=111[2f(7)−f(14)]/2. Consequently the
+optimal separate-arm bill minus 36h is a lower bound for any
+grouping. The computation encloses all powers and sums with outward
+rounding to 22 decimal places.
+
+## Higher multiplicities
+
+The nine half-ranks in each arm are 2 through 10. At saturation
+a half-idle demand at capacity c has bounds max(0,c−a)≤d≤c if the
+arm's largest LOCAL multiplicity is a. Given n_arm LOCALs, the
+sum of the half-demands is 54−n_arm.
+
+To minimize the separate-arm bill, start with the lower demands.
+Allocate the remaining increments in order of increasing depth
+among all columns, respecting their caps. At every mask length
+cutoff k, the marginal increase in ∑ min(k,2d) is first two,
+possibly one, then zero. This same allocation maximizes the
+sum for every k, giving the least nested cost. The table relaxes
+actual maxima a,b to upper bounds only for this IDLE price. It
+charges the QUERY lower bound for the declared actual maxima.
+
+There are 331 feasible count/max cells per arm. Across the
+108,832 paired cells with max(a,b)≥3, the highest directed signed
+upper is −28.3066209237471478769601. For exactly 36 LOCALs it is
+−46.0926684363776335553730. The 272 legal ordered one-slot transfers
+also fail individually. All two-slot transfers introducing a higher
+multiplicity are included in the grouped bound.
+
+## Zero, one or two LOCALs per stage
+
+Here write m=36−n. At saturation with a stage retaining two LOCALs,
+the head identity block gives q_count≥m+4. Suppose each arm has a
+stage with two LOCALs and two cross IDLE incidences. In each such
+stage the cross IDLE images and rows span the two root spaces.
+Both LOCAL defects then have column and row only on the private
+coordinates of that arm. The four terms across the two arms
+give a four-by-four identity minor, requiring q_count≥m+6.
+Thus at q_count=m+4 at least one arm has at most one cross
+incidence per stage retaining two LOCALs. The total is at most
+min(36,27+m).
+
+The original IDLE masks attain the separate-arm nested minimum.
+Each additional incidence increases it by at least
+δ=111[f(63)−f(56)]. Two additional incidences and one paid QUERY
+per retirement cost at least 2.92315928489496 more than the saved
+net native moment. This exceeds h. Hence the upper at q_count=m+4
+is greatest at m=0 using 27h and is below −2.36106060201144.
+With q_count≥m+5 the extra 111 units dominate all 36 cross
+incidences. If every stage has at most one LOCAL, the first 18
+retirements increase the nested separate-arm minimum by four
+rank-63 masks. At q_count≥m+3 and with all 36 cross incidences
+granted the upper there is below −28.64227303907207. Each further
+retirement only decreases this upper.
+
+## Extra incidence and excessive native count
+
+Every stage needs at least rank(E_s) serving dimensions. If any
+stage has excess, there are at least 217−2n IDLE incidences
+for n≤108. Grant arbitrary grouping into masks of up to 18 stages
+and charge only q_count≥max(0,39−n). Concavity permits a lower bill
+using full masks and one remainder. Across 0≤n≤108 the best
+signed upper is −161.1964987524476534781450. For n≥109, even
+granting every IDLE and QUERY free, the root productive moment
+minus the native net debit is strictly negative and decreases
+with n.
+
+The remaining mechanisms change the native invoice, the endpoint,
+the LOCAL or QUERY operator, the IDLE tariff, or the recursive
+admission proof. The replay authenticates the exact #7001 caller,
+receipt and interval engine, reconstructs the original paid and
+productive profiles, and checks the exact integer price cells.
+It also compares the greedy allocation against 96 small
+bounded-demand fixtures.
+
+Credit DreamingOfClouds, CubeJerry, zxv and the retained #7001
+authors for the paired BIT source. [#7160](https://github.com/CrocSwap/integer-mult-bounds/pull/7160)
+supplies independent-stage saturation and the 36-LOCAL rank bound.
+[#6984](https://github.com/CrocSwap/integer-mult-bounds/pull/6984),
+[#6800](https://github.com/CrocSwap/integer-mult-bounds/pull/6800)
+and [#6825](https://github.com/CrocSwap/integer-mult-bounds/pull/6825)
+supply related fixed-window and rank-factorization methods. The
+two-LOCAL retirement argument was independently audited in Round 7.
+OpenAI Codex and subagents materially assisted the proof, replay
+and independent rank and price checks.

research/bit-paired-schedule-bound/README.md

@@ -0,0 +1,37 @@
+# Paired BIT schedule bound at the fixed target
+
+**NO VERIFIED GAIN.** On the exact #7001 paired BIT endpoint, every
+LOCAL count and stage multiplicity fails the signed paid-moment test
+at κ = 0.0040075385047236 under the retained per-LOCAL invoice and
+rank-one QUERY and distinct-stage IDLE tariffs. The bound allows arbitrary
+invertible scalar bases and clean auxiliary roles restored to zero.
+[Proof](PROOF.md) · [Directed receipt](RECEIPT.json)
+
+## Clean replay
+
+Run from the repository root with CPython 3.12 and assertions enabled.
+
+```sh
+python3.12 -B scripts/research_package.py --package research/bit-paired-schedule-bound
+```
+
+The verifier authenticates the paired caller, frozen invoice and retained
+interval code. It reconstructs the original counts and covers 81 exact
+opposite-arm support pairs, 108,832 relaxed higher-multiplicity price
+cells, and every possible native count. Separate inequalities cover
+zero-to-two LOCALs, excess stage incidence and counts above saturation.
+A small brute-force control checks bounded-demand mask packing.
+
+## Open next questions
+
+The next supplier change needs a lower native net debit or a changed
+head/body endpoint. Start by pinning a changed native charge and pricing
+it against the complete paired target, including every setup, transport
+and restoration. A positive relaxed price still needs an all-width
+operator, physical replay and the larger BIT atom and tape admission.
+
+This result extends [#7160](https://github.com/CrocSwap/integer-mult-bounds/pull/7160)
+from a fixed 36-LOCAL rank bound to arbitrary multiplicities and a
+complete target-moment obstruction for this alphabet. The proof credits
+the paired source and related head-rank precedents. OpenAI Codex and
+subagents materially assisted. Apache-2.0.

research/bit-paired-schedule-bound/RECEIPT.json

@@ -0,0 +1,39 @@
+{
+  "above_saturated_native_cap_maximum": "-8369.4606944275198565329965",
+  "best_one_slot": [
+    18,
+    10
+  ],
+  "dependencies": {
+    "EFREE-CALLER.json.gz": "757b3523798f840bdb02028b23708c3416627a99ea09e7a3c4bcdc5cd0c7ce4b",
+    "EFREE-RESULT.json": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b",
+    "retained/inputs/independent_interval.py": "9293f567aa4afd9b4e618f1cddd3cf66eea51c5e194e3c578e7a8f4db6e04a57"
+  },
+  "lower_multiplicity_saturated": {
+    "at_least_one_extra_query": "-94.1134477296328029670842",
+    "minimum_queries_with_two_local_stage": "-2.3610606020114406897430",
+    "no_two_local_stage": "-28.6422730390720785911148"
+  },
+  "max_for_36": "-46.0926684363776335553730",
+  "native_counts_considered": 109,
+  "one_slot_upper": "-74.8227702474738125629074",
+  "opposite_stage_pairs": 81,
+  "ordered_one_slot_transfers": 272,
+  "per_arm_tables": [
+    331,
+    331
+  ],
+  "saturated_higher_multiplicity_maximum": "-28.3066209237471478769601",
+  "saturated_higher_multiplicity_price_cells": 108832,
+  "saturated_maximizing_cell": [
+    3,
+    2,
+    26,
+    15,
+    0
+  ],
+  "target": "10018846261809/2500000000000000",
+  "unsaturated_maximizing_locals": 37,
+  "unsaturated_maximum": "-161.1964987524476534781450",
+  "water_fill_toy_controls": 96
+}

research/bit-paired-schedule-bound/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "path": "certificates/selected-result.json",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1",
+      "usage": "provenance"
+    },
+    {
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "path": "docs/research/agent-task-catalog.json",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81",
+      "usage": "provenance"
+    },
+    {
+      "git_blob": "f022272a8d51ede841778dec76e2bfb24b614d04",
+      "path": "research/paired-query-only-bit/EFREE-CALLER.json.gz",
+      "sha256": "757b3523798f840bdb02028b23708c3416627a99ea09e7a3c4bcdc5cd0c7ce4b",
+      "usage": "input"
+    },
+    {
+      "git_blob": "575f76487f9999ecc3e7b1b70f9f71bc582ef8a8",
+      "path": "research/paired-query-only-bit/EFREE-RESULT.json",
+      "sha256": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b",
+      "usage": "input"
+    },
+    {
+      "git_blob": "30ae586ea0714513802930561b6223065f377573",
+      "path": "research/paired-query-only-bit/retained/inputs/independent_interval.py",
+      "sha256": "9293f567aa4afd9b4e618f1cddd3cf66eea51c5e194e3c578e7a8f4db6e04a57",
+      "usage": "input"
+    }
+  ],
+  "schema_version": 1
+}

research/bit-paired-schedule-bound/TASK.json

@@ -0,0 +1,64 @@
+{
+  "actual_scope": "Exact selected #7001 clean paired endpoint, arbitrary LOCAL stage multiplicity and scalar chronology, fixed native invoice, rank-one QUERY and distinct-stage IDLE tariff.",
+  "ai_assistance": "Substantial OpenAI Codex and subagent assistance with proof, replay and independent rank and price audits.",
+  "author": "ToikY",
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "bottleneck_link": "Every raw BIT schedule in the stated family loses directed moment at the campaign target, so a stronger provider or changed interface is needed.",
+  "budget_minutes": 30,
+  "evidence": "Exact paired invoice reconstruction, 81 root support intersections, 108832 directed relaxed higher-multiplicity cells, 272 one-slot transfers, 96 exhaustive small packing fixtures and all other count classes bounded analytically.",
+  "open_questions": [
+    {
+      "blocked_by": "All-width native and restored ownership proof, explicit transport and larger BIT atom and tape admission.",
+      "first_step": "Pin a literal native debit change and reprice the complete paired invoice with every added charge.",
+      "question": "Can a changed native provider reduce the per-LOCAL debit while preserving the same paired target?",
+      "why_it_matters": "A reduction changes the binding raw moment beyond this schedule bound."
+    }
+  ],
+  "original_card": {
+    "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "allowed_variations": [
+      "Choose a fixed larger register count or a specified nonabelian operation family."
+    ],
+    "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.",
+    "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "id": "bit-new-register-model",
+    "methods": [
+      "Construct the smallest exact identity in a newly specified legal operation alphabet.",
+      "Derive a target-specific relaxation bound for that same explicit alphabet."
+    ],
+    "overlap_terms": [
+      "three-register",
+      "nonabelian",
+      "group algebra"
+    ],
+    "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?",
+    "scope_change_triggers": [
+      "Remaining inside the already-excluded three-register abelian model.",
+      "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result."
+    ],
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/bit-three-register-lower-bound/README.md",
+      "certificates/selected-result.json",
+      "research/bit-gl3-mixed-targets-length10/README.md",
+      "docs/research/community-efficient1000-review.md"
+    ]
+  },
+  "outcome": "negative-result",
+  "priority_revision": 8,
+  "schema_version": 1,
+  "scope_change_reason": "Determine whether changing LOCAL count, stage assignment and IDLE grouping can reach the exact campaign target in the retained paired caller alphabet.",
+  "scope_status": "changed",
+  "stop_rule": "Stop when the signed upper bound is strictly negative for every native count and incidence class. Build only on a positive fully charged class.",
+  "task_id": "bit-new-register-model"
+}

research/bit-paired-schedule-bound/VERIFY.json

@@ -0,0 +1,23 @@
+{
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "checks": "Recount exact paired BIT costs and verify every directed schedule-family bound and mask-packing control.",
+      "timeout_seconds": 60
+    }
+  ],
+  "inputs": [
+    "research/paired-query-only-bit/EFREE-CALLER.json.gz",
+    "research/paired-query-only-bit/EFREE-RESULT.json",
+    "research/paired-query-only-bit/retained/inputs/independent_interval.py"
+  ],
+  "python": "3.12",
+  "requirements": [],
+  "schema_version": 1,
+  "status": "ready"
+}