Bound the selected BIT role digit by 2^(H1+13) (no new κ)

research/bit-role-digit-bound/PROOF.md

@@ -0,0 +1,134 @@
+# The selected BIT role digit satisfies c_B <= 2^(H1+13) <= N^2
+
+This is a scoped arithmetic consequence of an inherited nested-width bound.
+It is not a new census of the compiler, a materialized role count, a smaller
+fit threshold, or a change to the selected frontier.
+
+## 1. Selected stage
+
+The selected claim `certificates/frontier6030/CLAIM.json` records
+
+```text
+admitted_BIT_saving = 17/5000
+BIT before cover rank_encoding = 2^25986965159937
+```
+
+The same rank and admitted saving are the ordinary BIT record in
+`research/query-thinned-controllers/RESULT.json`: `uniform_H1 = H1`,
+`uniform_N = 2^H1`, `tensor_power = 1024`, `target_floor_base = 18`,
+`atom = 1/250`, and
+
+```text
+prime_rule = odd q > 2^26*N^5
+```
+
+with the recorded avoidance of fixed denominators and rank witnesses.
+Write `N = 2^H1`. For every prime allowed by that rule,
+
+```text
+log2(q) > 26 + 5*H1.
+```
+
+The stock formula in `research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md`
+section 8 is written there as a LaTeX display. The selected-stage band
+proof transcribes it as:
+
+```text
+k <= D*(N^2*(w-1) + ceil(log_q(B*|GL_N(F_q)|))) + ceil(log_q S_old) + 1.
+```
+
+`B` is the productive role count of the compiled uniform program. Define
+
+```text
+c_B = ceil(log_q B).
+```
+
+`research/selected-bit-stage-stock-band/PROOF.md` proves that the parent
+stock fits for `t = log2(e) >= 52182660963735` once `c_B <= N^2` and
+`k_old <= e/4`. `research/selected-old-leaf-reserve/README.md` proves the
+external old-leaf reading `S_old = 1`, hence `k_old = 1`, and leaves `c_B`
+open because `B` is not materialized.
+
+## 2. Inherited nested-width bound
+
+This package does not re-prove the source census. It uses the bound stated
+in `research/lockstep-live-role-audit/constant_c.py` for the #4436 nested
+widths, and the identification that file already makes when it bounds the
+`log2 B` term of `W(w)` by `N*X`. In that reading the stock formula's
+productive role count is the nested-width count `B_N`. The mixed-flow note
+states a different, untensored `C_N`; this proof uses the tensored formula.
+
+```text
+Wv = W^v,  Pv = M^v + Wv*b^v,
+C_N = Wv*(Wv+Pv+1)^(h+1),  h <= H1,
+B_N <= C_N^N.
+```
+
+Here `W` is the productive-field count of the BIT invoice, `M` is its paid
+rank mass, `b = 18` and `v = 1024`. For a positive integer `n`,
+
+```text
+ulog2(n) = n.bit_length() = floor(log2 n)+1 > log2 n.
+```
+
+Therefore
+
+```text
+X = ulog2(Wv) + (H1+1)*ulog2(Wv+Pv+1)
+```
+
+satisfies `log2(C_N) < X` whenever `h <= H1`, and
+
+```text
+log2(B_N) <= N*log2(C_N) < N*X.
+```
+
+The verifier recomputes `X = 471715391583208384` from the pinned invoice.
+That integer has 59 bits, so `X < 2^59`.
+
+## 3. Comparison with the prime rule
+
+Let `den = 5*H1+26`. The recomputed values satisfy
+
+```text
+X < 2^13 * den.
+```
+
+Combine this with section 2 and `log2(q) > den`:
+
+```text
+log_q(B) = log2(B)/log2(q) < (N*X)/den < 2^(H1+13).
+```
+
+If `0 <= y < 2^E` and `2^E` is an integer, then `ceil(y) <= 2^E`. Hence
+
+```text
+c_B <= 2^(H1+13).
+```
+
+Since `H1 >= 13`,
+
+```text
+2^(H1+13) <= 2^(2*H1) = N^2,
+```
+
+so `c_B <= N^2`. The band note already says this comparison follows from
+the nested-width bound; the arithmetic above is the missing calculation.
+Together with the cited reading `S_old = 1`, the sufficient guard
+
+```text
+t >= 52182660963735  implies  k < e/2
+```
+
+no longer depends on an unknown role count.
+
+## 4. What this does not do
+
+The obstruction side of the band, `t <= 52182660963729`, does not use `B`.
+The six integers of `log2(e)` between that obstruction and the sufficient
+guard remain unresolved. The additive role term is at most `2^(H1+13)`,
+while the matrix term at one level is `N^2*w = 2^(2*H1)*w`. Their ratio is
+at most `2^(13-H1)`, so replacing the hypothesis `c_B <= N^2` by this
+sharper digit bound does not move the published guard by one bit of
+`log2(e)`. No `actual_stock_coefficient` is chosen, and kappa stays
+`781451/250000000`.

research/bit-role-digit-bound/README.md

@@ -0,0 +1,60 @@
+# Selected BIT role digit is at most 2^(H1+13)
+
+**Scoped comparison. No new κ.** The selected frontier stays
+`781451/250000000`. The ordinary BIT stage retained by
+`certificates/frontier6030/CLAIM.json` has admitted saving `17/5000` and
+rank `2^25986965159937`. Its published sufficient stock guard at
+`log2(e) >= 52182660963735` needed `c_B <= N^2`. The compiled role count
+`B` is not materialized. Under the nested-width bound already used by the
+lockstep audit,
+
+```text
+c_B = ceil(log_q B) <= 2^(H1+13) <= N^2
+```
+
+for every prime allowed by the recorded rule `q > 2^26*N^5`. The band note
+asserts this comparison and does not compute the digit. With the cited
+reading `S_old = 1`, the guard no longer needs a role count beyond that
+inherited bound. The six-bit gap below the guard is unchanged.
+
+The argument is in [PROOF.md](PROOF.md). The nested-width census is an
+inherited hypothesis, not a theorem proved here.
+
+## Reproduce
+
+From the repository root, CPython 3.12 and the standard library:
+
+```sh
+python3 -B research/bit-role-digit-bound/verify.py
+python3 -B scripts/research_package.py --package research/bit-role-digit-bound
+```
+
+Expected marker:
+
+```text
+PASS_BIT_ROLE_DIGIT c_B<=2^(H1+13)<=N^2 X=471715391583208384 no_new_kappa
+```
+
+The verifier recomputes the role upper bound from the pinned BIT invoice,
+checks the prime-rule comparison, and rejects a rank that is too small to
+absorb the exponent and an upper bound shifted by the full slack. It does
+not run a selected-frontier replay.
+
+## Open next questions
+
+1. Can a `D = 2` depth lemma move the sufficient guard below
+   `t = 52182660963735`? The role digit is now at most `2^(H1+13)`, which
+   is smaller than the matrix term by a factor `2^(H1-13)`, so a sharper
+   `c_B` does not close the six-bit gap. The first step is an exact
+   comparison of `D*(N^2*w + c_B)` with `e/4` at `D = 2` and
+   `w = ceil(e^(1/250))`. It is blocked by the slack the published band
+   proof spends on the exponent arithmetic.
+
+## Credit
+
+The band theorem is JoyboyBrian's PR #4954. The old-leaf reading `S_old = 1`
+is James Reed's PR #4970. The nested-width formula is the #4436 bound as
+used by Mark (Matarener) in `research/lockstep-live-role-audit`. The stock
+formula is the delayed-cover bridge. The selected claim is PR #6030.
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+No independent human or proof-kernel acceptance is claimed.

research/bit-role-digit-bound/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840",
+  "files": [
+    {
+      "path": "certificates/frontier6030/CLAIM.json",
+      "usage": "input",
+      "git_blob": "f32ff3779274a349dc8af2e84a4c6234c6d62406",
+      "sha256": "9cee8a1304fa893be3d3b641eda42fdd9b2fd6a5ac2124fb891de7a1a5e8d92e"
+    },
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md",
+      "usage": "input",
+      "git_blob": "a58774e237c9362869a60a22bda35be09fb85872",
+      "sha256": "9731b93026717f5fa15851e3633cbb4bdc76eba2bffb9d6b4a3b69f7dd502443"
+    },
+    {
+      "path": "research/lockstep-live-role-audit/constant_c.py",
+      "usage": "input",
+      "git_blob": "a0fc4aecb910a353dd049926e25e13c20324112c",
+      "sha256": "74939dfa06092a6ea2cc7c94ce376f89d08c60c66af46ce5923341ed356ab51f"
+    },
+    {
+      "path": "research/query-thinned-controllers/RESULT.json",
+      "usage": "input",
+      "git_blob": "e0695152c98d727edfd0d2034b58a1c7e8682c0c",
+      "sha256": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f"
+    },
+    {
+      "path": "research/selected-bit-stage-stock-band/PROOF.md",
+      "usage": "input",
+      "git_blob": "50ba408ec79d7fbed1b5e4d0e24366eb152ad006",
+      "sha256": "b93430458a861ae26d41a544f25b6bf3b89ca3693793e27b51e2a49c4e80d507"
+    },
+    {
+      "path": "research/selected-old-leaf-reserve/README.md",
+      "usage": "input",
+      "git_blob": "366a377aa15a6814bc2a4a80b85b8d889eb33499",
+      "sha256": "f6d288a36fe18f50eb6d7ecc5ce367e7b3e22d8ab1aecd8c07f2c9090a9dc05f"
+    }
+  ]
+}

research/bit-role-digit-bound/TASK.json

@@ -0,0 +1,82 @@
+{
+  "schema_version": 1,
+  "task_id": "selected-stock-envelope",
+  "priority_revision": 8,
+  "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840",
+  "original_card": {
+    "id": "selected-stock-envelope",
+    "question": "What explicit uniform stock envelope does the actual selected stopped producer supply at one bootstrap stage?",
+    "starting_points": [
+      "research/selected-bootstrap-stock-audit/README.md",
+      "research/bootstrap-cutoff-time-space-split/README.md",
+      "certificates/selected-result.json",
+      "docs/research/community-efficient1000-review.md",
+      "research/stock-margin-chain/README.md"
+    ],
+    "methods": [
+      "Derive a source-bound reserve recurrence at the actual selected atom widths, separating parent stock from completed inner borrowing.",
+      "Find an exact missing implication or counterexample to a proposed selected-stage stock envelope."
+    ],
+    "acceptance_gate": "Bind every coefficient and depth factor to the selected producer and state the width domain. Compare a proved envelope with the sufficient cutoff guard; a large numerical headroom or a historical m=120 coefficient is not a selected m=73 proof.",
+    "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."
+    },
+    "first_experiment": "Choose one actual selected producer/stage and derive its parent reserve and depth coefficient from source. Check whether newer handoffs already cover that exact obligation. Stop with the missing implementation lemma if it cannot be bounded; do not rerun #2972 cutoff/headroom arithmetic as a new contribution.",
+    "bottleneck_link": "This reduces a concrete inherited implementation obligation without confusing unchanged kappa arithmetic with a completed theorem.",
+    "allowed_variations": [
+      "One stage or one explicit reserve/depth implication.",
+      "An independently checked same-domain proof repair, retaining all remaining assumptions."
+    ],
+    "scope_change_triggers": [
+      "Importing the historical 57604 or 252 allowance without a selected-producer binding.",
+      "Calling a conditional fit lemma a full outer-proof adoption.",
+      "Replacing an actual selected stock coefficient with cutoff comparisons or a conditional fit inequality."
+    ],
+    "overlap_terms": [
+      "selected stock",
+      "stock envelope",
+      "bootstrap cutoff",
+      "1956",
+      "1965",
+      "1990",
+      "2972",
+      "stock-margin-chain",
+      "actual_stock_coefficient"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Retained stock audit identifies missing actual selected-stage coefficients; later cutoff-chain arithmetic does not supply them.",
+        "evidence": "docs/research/research-family-status.md#revision-6-handoffs-source-archives-awaiting-independent-validation",
+        "remaining": "Derive one actual reserve/depth coefficient from the selected producer.",
+        "status": "reviewed",
+        "source_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Bound the role digit c_B=ceil(log_q B) of the selected ordinary BIT stage whose rank encoding is 2^25986965159937 and whose admitted saving is 17/5000. Use the inherited nested-width upper bound, not a materialized role count.",
+  "scope_change_reason": "The card asks for one selected-stage reserve coefficient. PR #4954 left a six-bit fit window whose remaining hypothesis was c_B<=N^2, and selected-old-leaf-reserve left that hypothesis open because B is not materialized. This package discharges the hypothesis. It does not move the six-bit endpoints or adopt a stock coefficient as the selected envelope.",
+  "bottleneck_link": "The selected #6030 claim retains this BIT rank and the admitted saving 17/5000. The published sufficient stock guard then uses the inherited nested-width bound in place of an open role-count hypothesis, without changing kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once c_B<=2^(H1+13)<=N^2 is proved from the inherited nested-width bound and the recorded prime rule. Do not rerun cutoff margins or shrink the six-bit window.",
+  "outcome": "completed",
+  "evidence": "python3 -B scripts/research_package.py --package research/bit-role-digit-bound",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial Cursor Grok assistance.",
+  "open_questions": [
+    {
+      "question": "Can a D=2 depth lemma, rather than a smaller c_B, move the sufficient stock guard below t=52182660963735?",
+      "why_it_matters": "The role digit is now at most 2^(H1+13), negligible beside N^2*w, so it does not close the six-bit gap between the obstruction and the sufficient guard.",
+      "first_step": "Replace lemma 2(c)'s factor-two slack by an exact comparison of D*(N^2*w+c_B) with e/4 at D=2, using c_B<2^(H1+13) and w=ceil(e^(1/250)).",
+      "blocked_by": "The published band proof spends its slack on the exponent arithmetic, not on c_B. A new lemma has to be written against the same chunk model."
+    }
+  ]
+}

research/bit-role-digit-bound/VERIFY.json

@@ -0,0 +1,25 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/frontier6030/CLAIM.json",
+    "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md",
+    "research/lockstep-live-role-audit/constant_c.py",
+    "research/query-thinned-controllers/RESULT.json",
+    "research/selected-bit-stage-stock-band/PROOF.md",
+    "research/selected-old-leaf-reserve/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Recomputes the inherited nested-width role upper bound X from the pinned BIT invoice and checks c_B <= 2^(H1+13) <= N^2 under the recorded prime rule. Pins the selected claim's admitted BIT saving 17/5000, rank 2^25986965159937 and kappa. Rejects rank 12 and an upper bound shifted by the full slack."
+    }
+  ]
+}