From 0622d9a6648ca33b9b7595cdff0cb27f57896155 Mon Sep 17 00:00:00 2001 From: James Reed Date: Thu, 22 Oct 2026 21:43:18 -0700 Subject: [PATCH] Derive the complex row coefficient of the selected outer reserve The #4470 complex row field is q_0 = ceil(log2 B_c) floor(log_N d) chunks (batched-complex-rows, AUDIT s6, rank-one compiled children), so the proportionality assumed as c_row <= 2^64 in lockstep-live-role-audit is exactly one. Rerunning the pinned constant computation gives log2 C <= 64,215,200,000,024 (64 bits lower) and fit log2 p = 64,473,100,659,050. The A_old term never binds. No new kappa. Co-Authored-By: Claude Opus 5.5 --- .../README.md | 117 ++++++++++++++++++ .../SOURCES.json | 72 +++++++++++ .../TASK.json | 82 ++++++++++++ .../VERIFY.json | 28 +++++ .../verify.py | 111 +++++++++++++++++ 5 files changed, 410 insertions(+) create mode 100644 research/selected-complex-row-coefficient/README.md create mode 100644 research/selected-complex-row-coefficient/SOURCES.json create mode 100644 research/selected-complex-row-coefficient/TASK.json create mode 100644 research/selected-complex-row-coefficient/VERIFY.json create mode 100644 research/selected-complex-row-coefficient/verify.py diff --git a/research/selected-complex-row-coefficient/README.md b/research/selected-complex-row-coefficient/README.md new file mode 100644 index 0000000000..621abc3cee --- /dev/null +++ b/research/selected-complex-row-coefficient/README.md @@ -0,0 +1,117 @@ +# The complex row coefficient of the selected outer reserve is one + +**Source-bound audit with an exact recomputation. No new κ.** +The selected conditional exponent stays 60403/20000000. + +## Result + +`research/lockstep-live-role-audit` bounds the #4470 outer-reserve constant +`C` of OUTER-TRANSFER-AUDIT §5 at `log2 C ≤ 64,215,200,000,088`. That bound +rests on two inherited, assumed coefficients: the complex row proportionality +`c_row ≤ 2^64` and the old-supplier stock `A_old ≤ 2^64`. Its open question 1 +asks for both. + +1. **`c_row = 1`.** The complex row field is exactly + `q_0 = ⌈log2 B_c⌉ · ⌊log_{N_c} d⌋ ≤ ⌈log2 B_c⌉ · log_{N_c} d` chunks. +2. **`A_old` never binds.** It enters only as `log2 A_old + 10` inside a + maximum whose complex term exceeds `6·10^13`. ([#4970](https://github.com/CrocSwap/integer-mult-bounds/pull/4970) + separately derives `S_old = 1`.) +3. **New figures.** Rerunning lockstep's own pinned computation with `c_row = 1` + gives: + +| Quantity | Assumed `c_row ≤ 2^64` | Derived `c_row = 1` | +|---|---:|---:| +| Complex share `log2` | 64,215,200,000,086 | **64,215,200,000,022** | +| `log2 C` upper bound | 64,215,200,000,088 | **64,215,200,000,024** | +| Fit point `log2 p` | 64,473,100,659,114 | **64,473,100,659,050** | + +The same computation gives a lower bound of `2^64,215,199,999,954` for the +complex share in this realization. So the upper and lower complex shares now +differ by 68 bits instead of 132. + +## Derivation + +Each step is a verbatim phrase checked against a pinned source. + +1. **The reservation.** `notes/batched-complex-rows.tex` (a #4470 proof + supplement) replaces the complex row reservation with + `k_0 = D_c(d)` and `q_0 = ⌈log2 W⌉ k_0`. The row field "consists only of + the first `q_0` chunks". It is padded once to a multiple of `W^{k_0}`, and + every child gets exactly `1/W` of its parent's volume. OUTER-TRANSFER-AUDIT + §5 counts `q0` in the same unit, "reserved complete chunks". +2. **`W` is `B`, and the child ratio is `1/N`.** + `research/kappa-rebuild/transfer-audit/AUDIT.md` §6 says: "The row stock is + based on B, not B+O", with the retained bound proportional to + `ceil(log2 B)*log_N(d)`. It adds: "The new child ratio is `1/N`". Its + semantic recurrence uses `f = ⌊e/N⌋`. +3. **No deeper recursion hides inside the compiled program.** + FINITE-PRECOMPILATION: "Induction removes all recursive calls: the only + remaining paid children have rank one." Exit batches handled by smaller + uniform programs are finite composition inside the fixed rank-`N` program. + They are not extra outer depth. Every outer recursive child is a tensor job + of size `⌊d/N⌋`. +4. **Depth.** So `D_c(d)` counts the steps `d ↦ ⌊d/N⌋` until `d < N`, which + is `⌊log_N d⌋`. The verifier checks this at five ranks over thousands of + widths, including `N^j ± 1`. Hence + `q_0 = ⌈log2 B_c⌉⌊log_{N_c} d⌋ ≤ ⌈log2 B_c⌉ log_{N_c} d`, and the + proportionality is `c_row = 1`. + +The old-lineage "row coefficient" 20,161, cited in lockstep's comment, was +an allowance in the κ≈0.0015 assemblies (16,467 used out of 20,161). That +was a different reservation, counting chart digits per level. It is not a +coefficient of the #4470 batched-complex-rows formula. + +## Recomputation + +`verify.py` authenticates the bytes of +`research/lockstep-live-role-audit/constant_c.py`. It runs `compute()` +unchanged and reproduces lockstep's published values. Then it substitutes +exactly one assumption line in memory, `log2_c_row = 64` → `log2_c_row = 0`, +and runs `compute()` again. The pinned file on disk is never modified. + +All of lockstep's internal checks still pass in the substituted run. These +include the threshold proofs `q0 ≤ h/512` at `h = H` for six values of `L`, +and the dominance of the #4618 term. + +## Scope + +Card `selected-stock-envelope` (adversarial audit), scope **refined** (see +`TASK.json`). This does not re-derive: +- `B_c` or the compiled ranks; +- the support router; +- the BIT share; +- the analytic outer premises. + +It is a source-bound reading of the retained reservation, not a new proof of +it. Base: canonical main `b91956876e5b4122fd89179f1b57557ff8378f15`, +priority revision 7. Claim: +[#1166 comment](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19138183). + +## Reproduce + +```sh +python3.12 -B research/selected-complex-row-coefficient/verify.py +python3.12 -B scripts/research_package.py --package research/selected-complex-row-coefficient +``` + +It runs in under a second. Changing the derived `log2 C`, using +`log2_c_row = 1`, or perturbing the depth recursion makes it fail. + +## Open next questions + +1. **Close the 68-bit gap.** The upper and lower complex shares of `C` now + differ by 68 bits. *First step:* compare lockstep's upper bound for + `log2 B_c / N` with its `2^(N−m)` lower bound term by term, and locate the + rounding steps that contribute the gap. *Blocked by:* nothing. + +## Credit + +- Mark (Matarener), `lockstep-live-role-audit`, for the constant `C`, its + computation and the open question. +- The `batched-complex-rows` authors, for the reservation. +- The authors of `research/kappa-rebuild` (AUDIT, OUTER-TRANSFER-AUDIT, + FINITE-PRECOMPILATION). +- Cinna Davis and zxv, for the #4440/#4470 chain. + +Prepared by James Reed with substantial Anthropic Claude (Claude Code) +assistance. Apache-2.0. No independent human review is claimed. diff --git a/research/selected-complex-row-coefficient/SOURCES.json b/research/selected-complex-row-coefficient/SOURCES.json new file mode 100644 index 0000000000..0d62a31ac4 --- /dev/null +++ b/research/selected-complex-row-coefficient/SOURCES.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "base_commit": "b91956876e5b4122fd89179f1b57557ff8378f15", + "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": "notes/batched-complex-rows.tex", + "usage": "input", + "git_blob": "e13bd96eb29bdc6526f10dc32e0a146bc17848a4", + "sha256": "64c70926a8705874f1c9b42a2f703e42cad4e90f927f544458cfdf729540236c" + }, + { + "path": "research/kappa-rebuild/transfer-audit/AUDIT.md", + "usage": "input", + "git_blob": "ee8c49a3450f812011eb3f7f40c25f5ade26b2d0", + "sha256": "032488343667d19613cab84df5dad554cfd2a283fb4fc0d4c9b4d165cfa04669" + }, + { + "path": "research/kappa-rebuild/architecture/FINITE-PRECOMPILATION.md", + "usage": "input", + "git_blob": "4badb40f0919c515823cb07e44c6470d4d6469ca", + "sha256": "4cb32f6b8e388ecf6ed41b5bbdeeb4539cb40c8424f194974afea58f7e0921e8" + }, + { + "path": "research/kappa-rebuild/transfer-audit/OUTER-TRANSFER-AUDIT.md", + "usage": "input", + "git_blob": "e8b7ef8956ece5bd493cbf52113916e5dc288535", + "sha256": "67569961d068633c6ff3ac9dfde47a0c17f0da6d20432799dcc920cff92b5779" + }, + { + "path": "research/lockstep-live-role-audit/constant_c.py", + "usage": "input", + "git_blob": "a0fc4aecb910a353dd049926e25e13c20324112c", + "sha256": "74939dfa06092a6ea2cc7c94ce376f89d08c60c66af46ce5923341ed356ab51f" + }, + { + "path": "research/lockstep-live-role-audit/README.md", + "usage": "input", + "git_blob": "158858c0a330465589c6b584926ec8b050191490", + "sha256": "0f3de4ae60ec52ad8096f5979db88e9949d8a54b50364b902ffb66a9b39eb075" + }, + { + "path": "research/query-thinned-controllers/RESULT.json", + "usage": "input", + "git_blob": "e0695152c98d727edfd0d2034b58a1c7e8682c0c", + "sha256": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f" + }, + { + "path": "research/joint-helper-lattice/RESULT.json", + "usage": "input", + "git_blob": "edf41a49a0350862c23378f837c7397fc5dc7596", + "sha256": "c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21" + }, + { + "path": "research/capped-phase-fusion/SUPPLIER-SUPPORT-AUDIT.md", + "usage": "input", + "git_blob": "ae676a6504cc7987863da1827551c18e7ec20ce1", + "sha256": "c41a2571b9c4c1d7920633f10c3ed2c74da39ca3bc8d6a910e6ffed380327413" + } + ] +} diff --git a/research/selected-complex-row-coefficient/TASK.json b/research/selected-complex-row-coefficient/TASK.json new file mode 100644 index 0000000000..46cb7cf829 --- /dev/null +++ b/research/selected-complex-row-coefficient/TASK.json @@ -0,0 +1,82 @@ +{ + "schema_version": 1, + "task_id": "selected-stock-envelope", + "priority_revision": 7, + "base_commit": "b91956876e5b4122fd89179f1b57557ff8378f15", + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2972 stock-margin chain and the selected stock audit. The new source archive reports the remaining cutoff comparisons, but leaves every actual stock coefficient unresolved; it is not an independently validated reserve envelope.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "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": "Derive the complex row proportionality c_row of the #4470 outer-reserve constant C (lockstep-live-role-audit open question 1) and recompute C and its fit point with the derived value.", + "scope_change_reason": "lockstep-live-role-audit bound C with two assumed coefficients, c_row <= 2^64 and A_old <= 2^64. This package derives c_row = 1 from the batched-complex-rows reservation, the AUDIT section 6 child ratio and the rank-one compiled children. It shows that A_old never binds. It does not change the supplier, the support router or any analytic premise.", + "bottleneck_link": "It removes the last assumed coefficient from the selected record's outer-reserve constant. log2 C falls by 64 bits, and kappa and the frontier are unchanged.", + "budget_minutes": 60, + "stop_rule": "Stop at the c_row derivation and the exact recomputation of the pinned constant. Do not revisit B_c, the compiled ranks or the router.", + "outcome": "completed", + "evidence": "python3.12 -B scripts/research_package.py --package research/selected-complex-row-coefficient", + "author": "James Reed", + "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code, Opus 5.5).", + "open_questions": [ + { + "question": "Can the remaining 68-bit gap between the upper and lower complex shares of C be closed by evaluating ceil(log2 B_c) exactly for the joint-helper-lattice compiled realization?", + "why_it_matters": "With c_row = 1 the complex share is determined by ceil(log2 B_c) and the nesting and width constants. The gap is now only rounding in those factors and the B_c bound.", + "first_step": "Compare lockstep's upper bound on log2 B_c/N with its lower bound 2^(N-m) term by term, and see which rounding steps contribute the 68 bits.", + "blocked_by": "nothing" + } + ] +} diff --git a/research/selected-complex-row-coefficient/VERIFY.json b/research/selected-complex-row-coefficient/VERIFY.json new file mode 100644 index 0000000000..e7a317b9ee --- /dev/null +++ b/research/selected-complex-row-coefficient/VERIFY.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "notes/batched-complex-rows.tex", + "research/kappa-rebuild/transfer-audit/AUDIT.md", + "research/kappa-rebuild/architecture/FINITE-PRECOMPILATION.md", + "research/kappa-rebuild/transfer-audit/OUTER-TRANSFER-AUDIT.md", + "research/lockstep-live-role-audit/constant_c.py", + "research/lockstep-live-role-audit/README.md", + "research/query-thinned-controllers/RESULT.json", + "research/joint-helper-lattice/RESULT.json", + "research/capped-phase-fusion/SUPPLIER-SUPPORT-AUDIT.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Pins and verbatim phrases for the complex row reservation (batched-complex-rows q_0 = ceil(log2 W) D_c(d), AUDIT section 6 child ratio 1/N, FINITE-PRECOMPILATION rank-one children); D_c(d) = floor(log_N d) on tested widths; the pinned lockstep constant_c rerun unchanged (log2 C <= 64215200000088) and with c_row = 1 (log2 C <= 64215200000024, fit log2 p = 64473100659050); upper/lower complex-share gap 68 bits; A_old term not binding." + } + ] +} diff --git a/research/selected-complex-row-coefficient/verify.py b/research/selected-complex-row-coefficient/verify.py new file mode 100644 index 0000000000..ed80715dab --- /dev/null +++ b/research/selected-complex-row-coefficient/verify.py @@ -0,0 +1,111 @@ +#!/usr/bin/env python3 +"""The complex row coefficient c_row of the #4470 outer-reserve constant is one. + +Checks the chain of custody for the complex row reservation, then reruns the +pinned lockstep-live-role-audit computation of C with c_row = 1 in place of +the assumed 2^64. The pinned script is not modified on disk: its bytes are +authenticated, exactly two assumption lines are substituted in memory, and the +result is compared with the original run. No new kappa is claimed. +""" + +from __future__ import annotations + +import hashlib +import json +import types +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = ROOT / "research" / "selected-complex-row-coefficient" +CONSTANT_C = ROOT / "research/lockstep-live-role-audit/constant_c.py" + +PHRASES = ( + ("notes/batched-complex-rows.tex", " k_0=D_{\\rm c}(d),\\qquad"), + ("notes/batched-complex-rows.tex", " q_0=\\lceil\\log_2 W\\rceil\\,k_0,"), + ("notes/batched-complex-rows.tex", "chunks; neither compact field is included in it. Pad its count to the"), + ("notes/batched-complex-rows.tex", "$1/W$ of its parent's volume, with enough row divisibility for its"), + ("research/kappa-rebuild/transfer-audit/AUDIT.md", "The row stock is based on B, not B+O. Its reserved-axis coefficient may be"), + ("research/kappa-rebuild/transfer-audit/AUDIT.md", "`ceil(log2 B)*log_N(d)=O(log d)`. The new child ratio is `1/N`, with a strict"), + ("research/kappa-rebuild/transfer-audit/AUDIT.md", "\\[\nA(e)\\le A(f)+Pf+E,\\qquad f=\\lfloor e/N\\rfloor.\n\\]"), + ("research/kappa-rebuild/architecture/FINITE-PRECOMPILATION.md", + "Induction removes all recursive calls: the only remaining paid children"), + ("research/kappa-rebuild/transfer-audit/OUTER-TRANSFER-AUDIT.md", "reserved complete chunks. This bound retains the **product** of stock"), + ("research/lockstep-live-role-audit/constant_c.py", + " # AUDIT s6: complex row stock proportional to ceil(log2 B_c) * log_{N_c}(d);"), + ("research/lockstep-live-role-audit/README.md", "1. Derive the two inherited coefficients of `C` (`c_row <= 2^64`,"), +) + +ASSUMED_ROW = " log2_c_row = 64\n" +DERIVED_ROW = " log2_c_row = 0\n" +ORIGINAL = {"log2_C_upper": 64215200000088, "complex_share_log2": 64215200000086, "fit_log2p": 64473100659114} +DERIVED = {"log2_C_upper": 64215200000024, "complex_share_log2": 64215200000022, "fit_log2p": 64473100659050} + + +def need(condition: bool, message: str) -> None: + if not condition: + raise SystemExit("FAIL: " + message) + + +def pins_and_phrases() -> None: + sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + pinned = {row["path"] for row in sources["files"]} + for row in sources["files"]: + digest = hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() + need(digest == row["sha256"], "pin " + row["path"]) + for path, phrase in PHRASES: + need(path in pinned, "unpinned phrase source " + path) + need(phrase in (ROOT / path).read_text(encoding="utf-8"), f"phrase in {path}: {phrase[:60]}") + selected = json.loads((ROOT / "certificates/selected-result.json").read_text(encoding="utf-8")) + need(selected["kappa"] == "60403/20000000", "selected kappa") + + +def depth(d: int, n: int) -> int: + """Outer complex recursion: rank-one paid children are jobs of size floor(d/N).""" + k = 0 + while d >= n: + d //= n + k += 1 + return k + + +def depth_lemma() -> None: + # D_c(d) = floor(log_N d) <= log_N d, so q_0 = ceil(log2 W) D_c(d) <= ceil(log2 W) log_N d: c_row = 1. + for n in (2, 3, 7, 64, 1 << 20): + for d in list(range(1, 5000)) + [n**j + s for j in range(1, 6) for s in (-1, 0, 1)]: + k = depth(d, n) + need(n**k <= d < n ** (k + 1) or (k == 0 and d < n), f"depth is floor(log_N d) at N={n}, d={d}") + + +def rerun_constant(source: str, label: str) -> dict: + module = types.ModuleType("lockstep_constant_c_" + label) + module.__file__ = str(CONSTANT_C) + exec(compile(source, str(CONSTANT_C), "exec"), module.__dict__) + return module.compute() + + +def recompute() -> None: + source = CONSTANT_C.read_text(encoding="utf-8") + need(source.count(ASSUMED_ROW) == 1, "assumed c_row line is unique") + original = rerun_constant(source, "original") + for key, value in ORIGINAL.items(): + need(original[key] == value, f"original {key}") + derived = rerun_constant(source.replace(ASSUMED_ROW, DERIVED_ROW), "derived") + for key, value in DERIVED.items(): + need(derived[key] == value, f"derived {key}") + need(original["log2_C_upper"] - derived["log2_C_upper"] == 64, "c_row = 1 removes 64 bits from log2 C") + lower = derived["complex_share_lower_log2_same_realization"] + need(derived["complex_share_log2"] - lower == 68, "upper and lower complex shares now differ by 68 bits") + # The old-supplier term log2 A_old + 10 never binds: the complex share dominates. + need(derived["log2_C_upper"] > 64 + 10 + 10**13, "A_old term is not binding") + + +def main() -> None: + pins_and_phrases() + depth_lemma() + recompute() + print("PASS_SELECTED_COMPLEX_ROW_COEFFICIENT c_row=1 log2_C<=64215200000024 " + "fit_log2p=64473100659050 no_new_kappa") + + +if __name__ == "__main__": + main()