Prove the depth-first continuation stack is O_q(V) at the new c.

research/pr2809-continuation-stack-space/PROOF.md

@@ -0,0 +1,174 @@
+# Depth-first continuation stack at the new c
+
+The PR2809 simulator is not executed. The model is the depth-first reading of
+`BIT.md` §2 at `c = 8667/5000000`, with the width recurrence written there.
+
+## Parameters
+
+`q = 2^89 - 1`, `W = 28416`, `M = 269241600 = W · 9475`, and
+`N = |GL_64(F_q)|`. Let `G = W N` and
+
+```text
+K(w) = M · N · q^(4096(w-1)).
+```
+
+For an integer address length `e ≥ 1`,
+
+```text
+w(e) = min { j ≥ 1 : j^5000000 ≥ e^8667 },
+D(0) = 0 for n < 64,
+D(n) = 1 + D(42 · floor(n/64)) for n ≥ 64.
+```
+
+`w(e)` is `ceil(e^c)`. `D(e)` is the number of recursive cuts in the written
+width recursion. `BIT.md` calls a bound on this depth `h`.
+
+## Model
+
+One ancestor chain is parked. After a node of volume `V`, the next parked
+payload has volume at most `V/G`, then `V/G^2`, and so on, for `D(e)` cuts.
+Each cut stores one integer of size at most `K(w)^{D(e)}`. A stream that
+contains an `e`-bit address field has volume `V ≥ e`. The physical stream
+`P G S q^(2e)` of the older ordinary-interchange proof is a special case.
+
+Cells count payload symbols and parameter bits in the same unit. One bit is
+one cell. That is the more expensive of the two natural units, because a
+`q`-ary digit holds 89 bits.
+
+## Lemma 1. Width for small addresses
+
+For every integer `e` with `2 ≤ e ≤ 2^576`, `w(e) = 2`. For every integer
+`e ≥ 2`, `w(e) ≥ 2`.
+
+`576 · 8667 = 4992192 < 5000000`, so `(2^576)^8667 = 2^4992192 < 2^5000000`.
+Any positive integer `e ≤ 2^576` therefore satisfies `e^8667 < 2^5000000`,
+and `j = 2` is admissible. For `e ≥ 2`, `e^8667 ≥ 2^8667 > 1`, so `j = 1` is
+not admissible.
+
+## Lemma 2. The suggested level-1 allowance fails
+
+`BIT.md` gives the child payload the volume `V/G`. The first step named by
+`research/bit-stock-recurrence-audit` compares a level against
+
+```text
+V / (G · q^(4096(w-1))).
+```
+
+At level 1 the two quantities differ by exactly `q^(4096(w-1))`. Lemma 1
+makes this factor at least `q^4096` for every integer `e ≥ 2`. The child
+payload alone is already larger than that allowance. The same comparison at
+`e = 1` has `w = 1` and factor `1`, so the hypothesis `e ≥ 2` is sharp.
+
+This does not by itself refute `O_q(V)`. The allowance is smaller than the
+geometric ratio `1/G` by that same factor.
+
+## Lemma 3. Payload series
+
+For `G > 1`,
+
+```text
+sum_{k ≥ 1} V / G^k = V / (G - 1) < V.
+```
+
+`G = W N > 2`. The sum does not depend on `c`, on `e`, or on cutting the
+chain off early.
+
+## Lemma 4. Two coarse steps halve the width
+
+For every integer `n ≥ 64`, the value after two steps of `n ↦ 42·floor(n/64)`
+is at most `floor(n/2)`.
+
+Let `f = floor(n/64)`, `x = floor(42 f / 64)` and `r = (42 f) mod 64`. Then
+`42 f = 64 x + r` with `0 ≤ r < 64`. Both `42 f` and `64 x` are even, so `r`
+is even. Write `r = 2 s`. Then
+
+```text
+672 x = (21/2) · (42 f - 2 s) = 441 f - 21 s ≤ 441 f ≤ 512 f,
+```
+
+hence `84 x ≤ 64 f ≤ n`. The two-step value is `42 x`, so twice that value
+is at most `n`.
+
+## Lemma 5. Depth bound
+
+For every integer `n ≥ 64`, `D(n) ≤ 2 (bitlength(n) - 6)`. For `n < 64`,
+`D(n) = 0`.
+
+If the two-step value is below 64, then `D(n) ≤ 2`. Every `n ≥ 64` has
+bit length at least 7, so the claimed bound is at least 2. If the two-step
+value `n2` is at least 64, then `D(n) = 2 + D(n2)` and `n2 ≤ floor(n/2)`, so
+`bitlength(n2) ≤ bitlength(n) - 1`. The inductive hypothesis on `n2` gives
+
+```text
+D(n) ≤ 2 + 2 (bitlength(n) - 1 - 6) = 2 (bitlength(n) - 6).
+```
+
+`n2 < n`, so the induction is well founded.
+
+## Lemma 6. Encoding bits
+
+`bitlength(K(w)^D) ≤ D · bitlength(K(w))`, because
+`K(w) < 2^{bitlength(K(w))}`. Across `D(e)` cuts the parameter bits are at
+most
+
+```text
+D(e)^2 · bitlength(K(w(e))).
+```
+
+On `2 ≤ e ≤ 2^576`, Lemma 1 gives `w = 2`. The exact value
+`bitlength(K(2)) = 729117` is computed in `verify.py` from the product
+formula for `|GL_64(F_q)|`. The maximum of `D(e)^2 · 729117 / e` on
+`2 ≤ e ≤ 200000` is attained at `e = 448`, where `D(448) = 4` and the
+quotient is `11665872 / 448`. The least integer `C` with
+`C · e ≥ D(e)^2 · 729117` for every such `e` is therefore `26040`.
+`26039 · 448 < 11665872`, so `26039` is not enough.
+
+For `200000 < e ≤ 2^576` the Lemma 5 bound is still at most `26040 · e`.
+`verify.py` checks the left edge of every bit length in that range, which is
+where a fixed numerator over a growing denominator is largest. For
+`e > 2^576`, `w(e) ≤ 2^{ceil(bitlength(e) · 8667 / 5000000)}`, and
+
+```text
+bitlength(K(w)) ≤ bitlength(M N) + 89 · 4096 · (w - 1),
+```
+
+because `q < 2^89`. The same depth bound times this bit length stays at most
+`26040 · e` for every bit length from 577 through 20000. From there through
+bit length 100000, `4 L^2 (bitlength(MN) + 89·4096) · 2^{t(L)}` still has
+bit length at most `L - 2`, with `t(L) = floor(L · 8667 / 5000000) + 1`.
+At bit length 100000 the coarser majorant `L/577 + O(log L)` leaves
+thousands of bits of slack against `L/2`. One later step can spend at most
+three of those bits. Any window of 577 bit lengths increases `floor(L/2)`
+by 288 and increases the majorant by at most 3, so the slack keeps growing.
+Thus for every integer `e ≥ 2`,
+
+```text
+parameter bits ≤ 26040 · e.
+```
+
+The maximizing address length has `w = 2`. Any smaller positive `c` that
+still forces `w(448) = 2` produces the same constant.
+
+## Theorem
+
+Under the model above, for every integer `e ≥ 2` and every volume `V ≥ e`,
+
+```text
+parked payload + parameter bits ≤ V/(G-1) + 26040 V ≤ 26041 V.
+```
+
+The constant depends on `q` through `N` and `K`, and on the checked
+arithmetic. It does not depend on `e` or on `V`. In this model the serialized
+ancestor stack keeps `O_q(V)` visited space at the new `c`.
+
+## A different parking reading
+
+If each of the `D(e)` cuts instead parked a fresh copy of the root volume
+`V`, the total would be `D(e) · V`. For every `n ≥ 265`,
+`42 · floor(n/64) ≥ floor(n/2)`, so each step drops the bit length by at most
+one while the width stays above 264. Hence `D(n) ≥ bitlength(n) - 9` once
+the bit length is at least 9. At `e = 2^26050`, `D(e) ≥ 26042 > 26041`, and
+`D(e) · V` exceeds the constant of the theorem. That reading is not
+`O_q(V)`. `BIT.md`'s geometric sentence is the reading proved here. The
+serializer that would decide which reading the machine implements is not
+inspected in this package.

research/pr2809-continuation-stack-space/README.md

@@ -0,0 +1,135 @@
+# Depth-first continuation stack keeps O_q(V) at the new c
+
+**Scoped space lemma. No new κ.** The selected conditional exponent stays
+`60403/20000000`. The PR2809 simulator is not run.
+
+## Result
+
+In the depth-first model written in `BIT.md` §2, with
+`c = 8667/5000000`, the parked ancestor stack is `O_q(V)` for every stream
+whose volume satisfies `V ≥ e`. The constant proved here is **26041**. The
+per-level allowance named as the first step of
+`research/bit-stock-recurrence-audit` fails at level 1 for every integer
+`e ≥ 2`.
+
+Let `q = 2^89 - 1`, `W = 28416`, `N = |GL_64(F_q)|`, `G = W N`, and
+`w = ceil(e^c)`. `BIT.md` gives the child payload volume `V/G`. The suggested
+level-1 allowance is `V / (G q^{4096(w-1)})`. For `2 ≤ e ≤ 2^576` one has
+`w = 2`, and for every `e ≥ 2` one has `w ≥ 2`, so the child payload is
+exactly `q^{4096(w-1)} ≥ q^{4096}` times that allowance. At `e = 1` the
+factor is 1, so the bound `e ≥ 2` is sharp. The geometric ratio `1/G` is a
+different, larger allowance. The infinite sum of the ancestor payloads is
+`V/(G-1) < V`, with no dependence on `c`.
+
+Parameter bits are charged one cell each. `D(e)` cuts, each storing one
+integer of size at most `K(w)^{D(e)}`, cost at most `D(e)^2 bitlength(K(w))`
+bits. On the `w = 2` plateau, `bitlength(K(2)) = 729117`. The ratio of those
+bits to `e` is largest at `e = 448`, where `D(448) = 4` and the least integer
+`C` with `C e` at least the bit count is **26040**. The same `C` covers every
+larger address length, including those with `w > 2`. Therefore
+
+```text
+parked payload + parameter bits ≤ V/(G-1) + 26040 V ≤ 26041 V.
+```
+
+The constant depends on `q` and not on `e` or `V`. The argument is
+[PROOF.md](PROOF.md).
+
+A different reading, in which each of the `D(e)` cuts parks a fresh copy of
+the root volume, is not `O_q(V)`. For `e = 2^26050`, `D(e) ≥ 26042 > 26041`.
+`BIT.md`'s geometric sentence is the reading proved here.
+
+## Scope
+
+Task card `uniform-transfer-audit`, priority revision 7, base
+`ff3cc58e370d0f678e529246f8c73e8094e18fcf`. Scope status is **refined**.
+
+The card asks whether one quantified step of #4100 holds at its caller. This
+package takes only the continuation-stack question left by
+`research/bit-stock-recurrence-audit` after that package checked the finite
+and algebraic statements of `BIT.md` §§1–4. It does not audit another #4100
+sentence and it does not change the selected record.
+
+This is item 2 of the eligible list below. Fewer than eight items remained,
+so the assigned index is `(8-1) mod 3 = 1`.
+
+Ordered eligible list for session r30. Open handoffs from the 19 October
+index come first, with a closed smallest task removed and a still-open
+remainder kept when it is distinct. Priority-table rows whose stated next
+decision is still open come next. Catalogue cards that are not already those
+rows follow. Dropped before the cut: work this account already delivered,
+results on current main, questions covered by an open pull request, and
+topics already on a fork `cursor/*` branch. The sibling branches visible at
+selection included `cursor/qq16-l546-head-move-306b`,
+`cursor/r437-parent-spectator-blank-7c47`,
+`cursor/r437-source87-fibre-multiplicity-9b2b`, and
+`cursor/ledger-boundary-exponent-efc8`.
+
+1. A caller that accepts `(w, q, v_N)` without restoring the original source
+   slots (discussion comment 19030045; open question 1 of
+   `research/p104-role-exchange-caller-audit`). The cleanup consumer in
+   `research/p104-residual-consumer` leaves that caller open.
+2. **This package.** The PR2809 encoded continuation stack at the new `c`.
+3. A 14-point difference basis of `F_2^6` with a simple closed walk of step
+   weight at most 3. The displayed witness in
+   `research/fixed-fourteen-basis-walk` needs weight 4, and open question 1
+   of `research/f2-six-difference-basis` asks about any other 14-point basis.
+
+Excluded before this cut: the fresh T385 wrapper, closed by
+`research/t385-r437-copy-audit`; the six-tape head-move bill, on
+`cursor/qq16-l546-head-move-306b`; the retiming handoff, covered by #4122
+and #4128; the four-provider rebind, on main in
+`research/mixed-provider-admission`; the matched park/restore bill, covered
+by open #4167 and #4172; the R437 fixed-tape blank-return, on
+`cursor/r437-parent-spectator-blank-7c47`; the #4100 ledger boundary
+exponent, on `cursor/ledger-boundary-exponent-efc8`; the #4091 word, capacity
+and stock equivalence, on main in `research/fourth-entry-ceiling-transfer`;
+the compact-switch contract and its sharp-window density; the rank-8/u2
+producer topic, on `cursor/rank8-u2-separate-idle-a7b8` and
+`cursor/rank8-u2-slack-stop-7249`; and the replay-runtime and portable-replay
+cards, which already have measured fast paths and the gzip payload
+convention on main.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3 scripts/research_package.py --package research/pr2809-continuation-stack-space --check-only
+python3.12 -B scripts/research_package.py --package research/pr2809-continuation-stack-space
+```
+
+`verify.py` prints
+
+```text
+PASS_PR2809_CONTINUATION_STACK_SPACE C=26040 witness_e=448 witness_bits=11665872 K2_bits=729117 level1_factor_bits=364544 payload_ratio=1/(WN-1) full_copy_exceeds_bitlen=26051 no_new_kappa=true
+```
+
+`test_verify.py` prints `PASS_PR2809_CONTINUATION_STACK_SPACE_CONTROLS`.
+Not run: the PR2809 simulator, Lean, Docker, and the selected cold replay.
+
+## Open next questions
+
+1. Does the PR2809 continuation serializer park the ancestor chain, or one
+   root-sized stream per cut? The second reading is not `O_q(V)`, because
+   `D(2^26050) ≥ 26042`. First compare the bytes written at one recursive cut
+   with the child capsule. Blocked here because this package does not extract
+   or run that serializer.
+2. Are the marker, template and erased-backing cells inside the `26041 V`
+   budget, or do they add another `q`-dependent multiple of `V`? `BIT.md`
+   includes them in the `O_q(V)` sentence. First charge one fixed template per
+   live role against `V/(G-1)`. Blocked here because §2 does not give the
+   live role count during recursion.
+
+## Credit
+
+The construction and the `O_q(V)` sentence are Cinna Davis's #4100
+(`research/unconditional-batched-crt/BIT.md`). Mark (Matarener), with
+Claude Code assistance, checked `BIT.md` §§1–4 in
+`research/bit-stock-recurrence-audit` and left this stack question open.
+Jose Manuel's `research/physical-ordinary-interchange` proves an `O_q(V)+F_q`
+space bound for the older `c = 17/10000` on the stream `P G S q^{2e}`; that
+replay is not a dependency of the arithmetic here.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
+No independent human review and no formal-kernel acceptance are claimed.

research/pr2809-continuation-stack-space/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/bit-stock-recurrence-audit/README.md",
+      "usage": "input",
+      "git_blob": "2b24598d635098fffe57ab6a5ed8dc69c1e74f60",
+      "sha256": "5a35dff0ffed7bd5e2c46ed2c5b75844bab07d4fe601caf0f5f5db76b2c8e293"
+    },
+    {
+      "path": "research/bit-stock-recurrence-audit/TASK.json",
+      "usage": "input",
+      "git_blob": "b740c1b4467adaff91da07d95667d39715e068ae",
+      "sha256": "d133d79f9ab9ceac9173fb5a70d207fb4d907ae81a8c25e3625a2a0f68b855a5"
+    },
+    {
+      "path": "research/unconditional-batched-crt/BIT.md",
+      "usage": "input",
+      "git_blob": "2aa2544fa61259ac48b936b8c906ec9d31d813fa",
+      "sha256": "83a0cc082e52219a5f142becc8b5b92019e091cb3ede6c5bccbd8508993fc4da"
+    }
+  ]
+}