From 37b1066d809eeca075e34ae6d00990e18da8340d Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Fri, 23 Oct 2026 13:53:27 +0000 Subject: [PATCH] Prove the depth-first continuation stack is O_q(V) at the new c. The level-1 allowance in the bit-stock first step fails by at least q^4096, while the geometric ancestor chain plus parameter bits stays within 26041 V for every stream of volume at least e. Co-authored-by: unpaidmoon --- .../pr2809-continuation-stack-space/PROOF.md | 174 +++++++++++ .../pr2809-continuation-stack-space/README.md | 135 +++++++++ .../SOURCES.json | 36 +++ .../pr2809-continuation-stack-space/TASK.json | 80 +++++ .../VERIFY.json | 31 ++ .../test_verify.py | 55 ++++ .../pr2809-continuation-stack-space/verify.py | 273 ++++++++++++++++++ 7 files changed, 784 insertions(+) create mode 100644 research/pr2809-continuation-stack-space/PROOF.md create mode 100644 research/pr2809-continuation-stack-space/README.md create mode 100644 research/pr2809-continuation-stack-space/SOURCES.json create mode 100644 research/pr2809-continuation-stack-space/TASK.json create mode 100644 research/pr2809-continuation-stack-space/VERIFY.json create mode 100644 research/pr2809-continuation-stack-space/test_verify.py create mode 100644 research/pr2809-continuation-stack-space/verify.py diff --git a/research/pr2809-continuation-stack-space/PROOF.md b/research/pr2809-continuation-stack-space/PROOF.md new file mode 100644 index 0000000000..1f36e92591 --- /dev/null +++ b/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. diff --git a/research/pr2809-continuation-stack-space/README.md b/research/pr2809-continuation-stack-space/README.md new file mode 100644 index 0000000000..50033ed7ba --- /dev/null +++ b/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. diff --git a/research/pr2809-continuation-stack-space/SOURCES.json b/research/pr2809-continuation-stack-space/SOURCES.json new file mode 100644 index 0000000000..85152bbf1a --- /dev/null +++ b/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" + } + ] +} diff --git a/research/pr2809-continuation-stack-space/TASK.json b/research/pr2809-continuation-stack-space/TASK.json new file mode 100644 index 0000000000..d14cf2ad89 --- /dev/null +++ b/research/pr2809-continuation-stack-space/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Whether the BIT.md depth-first continuation stack keeps O_q(V) visited space at c=8667/5000000, and whether the suggested per-level allowance V/(W N q^(4096(w-1)))^level holds at level 1.", + "scope_change_reason": "The card asks for one caller-bound #4100 implication. This package takes only the continuation-stack question left open by research/bit-stock-recurrence-audit after the finite and algebraic BIT.md sections 1-4 were checked. The PR2809 simulator is not executed.", + "bottleneck_link": "Side result for the #4100 fixed-tape space claim. A constant-factor visited-space bound does not raise the selected exponent. The selected conditional kappa stays 60403/20000000.", + "budget_minutes": 60, + "stop_rule": "Stop after the level-1 comparison and the depth-first encoding bound. Do not execute the PR2809 simulator, retune c, or audit another #4100 sentence.", + "outcome": "completed", + "evidence": "PROOF.md and verify.py. Exact encoding constant 26040, total cell constant 26041, witness e=448, bitlength(K(2))=729117. q=2^89-1 and |GL_64(F_q)| are computed.", + "author": "unpaidmoon", + "ai_assistance": "Prepared by unpaidmoon with substantial Cursor Grok assistance.", + "open_questions": [ + { + "question": "Does the PR2809 continuation serializer park the ancestor chain, or one root-sized stream per cut?", + "why_it_matters": "The second reading is not O_q(V): D(2^26050) is at least 26042, above the constant 26041.", + "first_step": "Compare the bytes written at one recursive cut with the child capsule in the pinned PR2809 serializer.", + "blocked_by": "This package does not extract or run that serializer." + }, + { + "question": "Are marker, template and erased-backing cells inside the 26041 V budget?", + "why_it_matters": "BIT.md includes those cells in the O_q(V) sentence, and section 2 does not give the live role count.", + "first_step": "Charge one fixed template per live role against the parked payload V/(G-1).", + "blocked_by": "The live role count during recursion is not stated in BIT.md section 2." + } + ] +} diff --git a/research/pr2809-continuation-stack-space/VERIFY.json b/research/pr2809-continuation-stack-space/VERIFY.json new file mode 100644 index 0000000000..107a17a40c --- /dev/null +++ b/research/pr2809-continuation-stack-space/VERIFY.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-stock-recurrence-audit/README.md", + "research/bit-stock-recurrence-audit/TASK.json", + "research/unconditional-batched-crt/BIT.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Bind the BIT.md stack sentences and the bit-stock open question; compute |GL_64(F_q)| and bitlength(K(2)); prove w=2 on 2..2^576; prove the level-1 factor is at least q^4096; prove the geometric payload sum; prove the sharp encoding constant 26040 and its tail, including addresses with w>2; record that full root copies exceed 26041." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 60, + "checks": "Reject w=1 at e=2, a non-halving coefficient 64, and the constant 26039 at the witness e=448. Accept the depth samples D(63)=0, D(64)=1, D(448)=4." + } + ] +} diff --git a/research/pr2809-continuation-stack-space/test_verify.py b/research/pr2809-continuation-stack-space/test_verify.py new file mode 100644 index 0000000000..79fb5690a4 --- /dev/null +++ b/research/pr2809-continuation-stack-space/test_verify.py @@ -0,0 +1,55 @@ +#!/usr/bin/env python3 +"""Rejecting controls for the continuation-stack bound.""" + +import importlib.util +from pathlib import Path + +PATH = Path(__file__).resolve().parent / "verify.py" +SPEC = importlib.util.spec_from_file_location("stack_space", PATH) +stack = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(stack) + + +def require_failure(name, fn): + try: + fn() + except SystemExit: + return + raise SystemExit("control accepted a bad instance: " + name) + + +def main(): + if stack.D(63) != 0 or stack.D(64) != 1 or stack.D(448) != 4: + raise SystemExit("depth samples moved") + # j = 1 is admissible only for e = 1. + if pow(1, stack.C_DEN) < pow(1, stack.C_NUM): + raise SystemExit("e=1 should admit w=1") + if pow(2, stack.C_NUM) <= pow(1, stack.C_DEN): + raise SystemExit("e=2 should reject w=1") + # Replacing 42 by 64 does not halve. + n = 128 + stuck = 64 * ((64 * (n // 64)) // 64) + if 2 * stuck <= n: + raise SystemExit("the 64-coefficient mutant unexpectedly halved") + # The recorded constant is one larger than a failing bound. + bits = 16 * stack.K2_BITS_EXPECTED + if (stack.C_EXPECTED - 1) * stack.WITNESS_E >= bits: + raise SystemExit("C-1 covers the witness") + if stack.C_EXPECTED * stack.WITNESS_E < bits: + raise SystemExit("C misses the witness") + # A factor of 1 is the e=1 allowance, not the e>=2 allowance. + if stack.Q**4096 <= 1: + raise SystemExit("q^4096 collapsed") + + def bad_halving(): + f = 2 + x = (64 * f) // 64 + if 2 * 64 * x > 64 * f: + raise SystemExit("mutant") + + require_failure("coefficient 64", bad_halving) + print("PASS_PR2809_CONTINUATION_STACK_SPACE_CONTROLS") + + +if __name__ == "__main__": + main() diff --git a/research/pr2809-continuation-stack-space/verify.py b/research/pr2809-continuation-stack-space/verify.py new file mode 100644 index 0000000000..0338297ae9 --- /dev/null +++ b/research/pr2809-continuation-stack-space/verify.py @@ -0,0 +1,273 @@ +#!/usr/bin/env python3 +"""Depth-first continuation-stack space at c=8667/5000000. + +Proves two facts about the BIT.md section 2 model, without running PR2809: + +1. For every integer e >= 2 the level-1 child payload V/(W N) exceeds the + allowance V/(W N q^(4096(w-1))) by q^(4096(w-1)) >= q^4096. +2. Parking the geometric ancestor payloads plus one K(w)^D-sized integer per + cut uses at most 26041 V cells whenever the stream volume satisfies V >= e. + +Standard library only. The arithmetic is integral. +""" + +from fractions import Fraction +from pathlib import Path + +PKG = Path(__file__).resolve().parent +ROOT = PKG.parents[1] +BIT = ROOT / "research" / "unconditional-batched-crt" / "BIT.md" +TASK = ROOT / "research" / "bit-stock-recurrence-audit" / "TASK.json" +README = ROOT / "research" / "bit-stock-recurrence-audit" / "README.md" + +Q = 2**89 - 1 +C_NUM = 8667 +C_DEN = 5_000_000 +W = 28416 +M = 269241600 +SCAN = 200_000 +C_EXPECTED = 26040 +K2_BITS_EXPECTED = 729117 +WITNESS_E = 448 +REGION_B_CHECKED_UNTIL = 20_000 + + +def D(n): + depth = 0 + while n >= 64: + n = 42 * (n // 64) + depth += 1 + return depth + + +def gl_order(n, prime): + prime_n = prime**n + order = 1 + prime_i = 1 + for _ in range(n): + order *= prime_n - prime_i + prime_i *= prime + return order + + +def bind_sources(): + bit = BIT.read_text(encoding="utf-8") + for needle in ( + "c=8667/5000000,", + "K(w)=269241600 N q^(4096(w-1)),", + "D(n)=0 (n<64), D(n)=1+D(42 floor(n/64)) (n>=64).", + "Each child's payload has volume V/(WN).", + "Active ancestor payloads therefore", + "form a geometric series.", + "Hence visited space is O_q(V)", + "Serialize parent streams and arithmetic", + "Two coarse levels reduce width by at least a factor two", + ): + if needle not in bit: + raise SystemExit("missing BIT.md sentence: " + needle) + task = TASK.read_text(encoding="utf-8") + readme = README.read_text(encoding="utf-8") + question = ( + "Does the PR2809 block construction's serialized continuation stack " + "keep O_q(V) visited space at the new c when it parks at every recursive cut?" + ) + step = "V/(W N q^(4096(w-1)))^level" + if question not in task or step not in task: + raise SystemExit("bit-stock TASK.json no longer states the stack question") + if "encoded stack keep the claimed `O_q(V)`" not in readme or step not in readme: + raise SystemExit("bit-stock README.md no longer states the stack question") + + +def prove_two_steps_halve(): + """84 * floor(42 f / 64) <= 64 f for every integer f >= 0.""" + if 441 > 512: + raise SystemExit("441 <= 512 is the last step of the remainder identity") + # The identity 672 x + 21 (r/2) = 441 f is checked on a full set of + # residues and then extended by the closed form in PROOF.md. The residue + # period of 42 f modulo 64 divides 32. + for f in range(32): + x, r = divmod(42 * f, 64) + if r % 2: + raise SystemExit("remainder must be even") + if 672 * x + 21 * (r // 2) != 441 * f: + raise SystemExit("remainder identity failed at f=" + str(f)) + if 84 * x > 64 * f: + raise SystemExit("two-step halving failed at f=" + str(f)) + # Affine extension: both sides of the identity scale from the period. + for f in (32, 64, 265, 10**6, 2**20 + 3): + x, r = divmod(42 * f, 64) + if 672 * x + 21 * (r // 2) != 441 * f or 84 * x > 64 * f: + raise SystemExit("halving identity failed at f=" + str(f)) + for n in (64, 65, 127, 128, 448, 10**5): + f = n // 64 + two = 42 * ((42 * f) // 64) + if 2 * two > n: + raise SystemExit("two steps exceed n/2 at n=" + str(n)) + + +def prove_depth_bound(limit): + previous = 0 + for n in range(1, limit + 1): + depth = D(n) + if depth < previous: + raise SystemExit("D decreased") + previous = depth + if n < 64: + if depth != 0: + raise SystemExit("D(n) should be 0 below 64") + continue + bound = 2 * (n.bit_length() - 6) + if depth > bound: + raise SystemExit("depth bound failed at n=" + str(n)) + if (n // 2).bit_length() != n.bit_length() - 1: + raise SystemExit("bit length of n//2") + f = n // 64 + two = 42 * ((42 * f) // 64) + if two > n // 2: + raise SystemExit("integer halving failed") + + +def prove_child_lower_bound(): + # 20 n >= 5292 iff n >= 265, which is the threshold in PROOF.md. + if 20 * 264 >= 5292 or 20 * 265 < 5292: + raise SystemExit("half-width threshold") + for n in range(265, 265 + 128): + if 42 * (n // 64) < n // 2: + raise SystemExit("child fell below n/2") + # Drops bit length by at most one, so D(2^m) >= m + 1 - 9. + if D(1 << 16) < 16 + 1 - 9: + raise SystemExit("depth lower bound disagrees with a computed value") + + +def w_upper(bitlen): + # e < 2^bitlen, so e^8667 < 2^(bitlen*8667). + t = (bitlen * C_NUM + C_DEN - 1) // C_DEN + return 1 << t + + +def encoding_constant(k2_bits): + best_num = 0 + best_e = 1 + witness_depth = None + for e in range(2, SCAN + 1): + depth = D(e) + num = depth * depth * k2_bits + if num * best_e > best_num * e: + best_num = num + best_e = e + witness_depth = depth + if best_e != WITNESS_E or witness_depth != 4: + raise SystemExit("unexpected maximizing address length " + str(best_e)) + if best_num != 16 * k2_bits: + raise SystemExit("witness depth did not contribute 16 K(2) bits") + constant = (best_num + best_e - 1) // best_e + if constant != C_EXPECTED: + raise SystemExit("constant changed: " + str(constant)) + if (constant - 1) * best_e >= best_num: + raise SystemExit("constant is not sharp") + if constant * best_e < best_num: + raise SystemExit("constant does not cover the witness") + # w = 2 through 2^576, checked by exponents rather than by building e^8667. + if 576 * C_NUM >= C_DEN: + raise SystemExit("2^576 is not inside the w=2 range") + for bitlen in range((SCAN + 1).bit_length(), 577): + n0 = max(SCAN + 1, 1 << (bitlen - 1)) + bound = 2 * (bitlen - 6) + if bound * bound * k2_bits > constant * n0: + raise SystemExit("w=2 tail failed at bit length " + str(bitlen)) + e = 1 << 576 + bound = 2 * (e.bit_length() - 6) + if bound * bound * k2_bits > constant * e: + raise SystemExit("endpoint 2^576 failed") + return constant, best_e, best_num + + +def prove_region_b(constant, mn_bits): + """Parameter bits stay <= C e after w leaves 2. + + Bit lengths 577 through 20000 are checked with the explicit w upper + bound. Bit lengths through 100000 use the power-of-two majorant. + Beyond that, one 577-step window cannot spend the slack at 100000. + """ + scale_base = mn_bits + 89 * 4096 + for bitlen in range(577, REGION_B_CHECKED_UNTIL + 1): + w_hi = w_upper(bitlen) + kbits = mn_bits + 89 * 4096 * (w_hi - 1) + bound = 2 * (bitlen - 6) + n0 = (1 << 576) + 1 if bitlen == 577 else 1 << (bitlen - 1) + if bound * bound * kbits > constant * n0: + raise SystemExit("region B failed at bit length " + str(bitlen)) + for bitlen in range(REGION_B_CHECKED_UNTIL, 100_001): + t = (bitlen * C_NUM) // C_DEN + 1 + upper = (4 * bitlen * bitlen * scale_base).bit_length() + t + if upper > bitlen - 2: + raise SystemExit("exponent gap closed at bit length " + str(bitlen)) + bitlen = 100_000 + s_bits = scale_base.bit_length() + # 4 L^2 S < 2^(2 + 2 bitlength(L) + bitlength(S)). + if (4 * bitlen * bitlen * scale_base).bit_length() > 2 + 2 * bitlen.bit_length() + s_bits: + raise SystemExit("power majorant is not an upper bound") + upper = bitlen // 577 + 1 + 2 * bitlen.bit_length() + s_bits + 4 + slack = bitlen // 2 - 2 - upper + # One step can add 1 to floor(L/577) and 2 to twice the bit length while + # floor(L/2) stays put. The slack has to survive that three-bit drop. + if slack < 4: + raise SystemExit("slack at bit length 100000 is too small") + window = 577 + half_gain = (bitlen + window) // 2 - bitlen // 2 + if half_gain - 1 - 2 < 1: + raise SystemExit("577-step window does not restore the slack") + + +def level1_factor_bits(): + # q^4096 < 2^(89*4096), and the exact bit length is recorded. + return (Q**4096).bit_length() + + +def full_copy_bitlen(): + # D(2^26050) >= 26051 - 9 = 26042 > 26041. + return 26051 + + +def main(): + bind_sources() + prove_two_steps_halve() + prove_depth_bound(4_000) + prove_child_lower_bound() + order = gl_order(64, Q) + if M != W * 9475: + raise SystemExit("M is not W*9475") + k2_bits = (M * order * Q**4096).bit_length() + if k2_bits != K2_BITS_EXPECTED: + raise SystemExit("K(2) bit length changed: " + str(k2_bits)) + mn_bits = (M * order).bit_length() + constant, witness, numerator = encoding_constant(k2_bits) + prove_region_b(constant, mn_bits) + group = W * order + if group <= 2: + raise SystemExit("payload ratio is not a contraction") + # sum_{k>=1} G^{-k} = 1/(G-1). + step = Fraction(1, group) + if step / (1 - step) != Fraction(1, group - 1): + raise SystemExit("series identity") + factor_bits = level1_factor_bits() + if factor_bits <= 1: + raise SystemExit("q^4096 did not exceed 1") + copy_bits = full_copy_bitlen() + if copy_bits - 9 <= constant + 1: + raise SystemExit("full-copy reading is still inside the constant") + print( + "PASS_PR2809_CONTINUATION_STACK_SPACE" + f" C={constant}" + f" witness_e={witness}" + f" witness_bits={numerator}" + f" K2_bits={k2_bits}" + f" level1_factor_bits={factor_bits}" + f" payload_ratio=1/(WN-1)" + f" full_copy_exceeds_bitlen={copy_bits}" + " no_new_kappa=true" + ) + + +if __name__ == "__main__": + main()