diff --git a/.github/workflows/cyclic-stride-effective-depth.yml b/.github/workflows/cyclic-stride-effective-depth.yml new file mode 100644 index 0000000000..07bcfb457b --- /dev/null +++ b/.github/workflows/cyclic-stride-effective-depth.yml @@ -0,0 +1,41 @@ +name: Cyclic stride effective depth + +on: + workflow_dispatch: + pull_request: + paths: + - 'research/cyclic-stride-effective-depth/**' + - '.github/workflows/cyclic-stride-effective-depth.yml' + push: + branches: ['codex/stride-effective-depth-20261013'] + paths: + - 'research/cyclic-stride-effective-depth/**' + - '.github/workflows/cyclic-stride-effective-depth.yml' + +permissions: + contents: read + +jobs: + verify: + runs-on: ubuntu-latest + timeout-minutes: 30 + strategy: + fail-fast: false + matrix: + python: ['3.11', '3.14'] + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: ${{ matrix.python }} + - name: Effective depth, original and cubic kernels, and defect controls + run: python -I -O -B research/cyclic-stride-effective-depth/verify.py --out /tmp/stride-depth-math.json + - name: Package rejection controls and full read-only relocation + run: python -I -O -B research/cyclic-stride-effective-depth/test_package.py --out /tmp/stride-depth-package.json + - uses: actions/upload-artifact@v4 + if: always() + with: + name: stride-depth-python-${{ matrix.python }} + path: | + /tmp/stride-depth-math.json + /tmp/stride-depth-package.json diff --git a/research/cyclic-stride-effective-depth-validation/LINUX314-MATH.json.gz b/research/cyclic-stride-effective-depth-validation/LINUX314-MATH.json.gz new file mode 100644 index 0000000000..8f7abb0657 Binary files /dev/null and b/research/cyclic-stride-effective-depth-validation/LINUX314-MATH.json.gz differ diff --git a/research/cyclic-stride-effective-depth-validation/LINUX314-PACKAGE.json b/research/cyclic-stride-effective-depth-validation/LINUX314-PACKAGE.json new file mode 100644 index 0000000000..a5a0fa2d79 --- /dev/null +++ b/research/cyclic-stride-effective-depth-validation/LINUX314-PACKAGE.json @@ -0,0 +1,66 @@ +{ + "controls": [ + { + "name": "missing manifest", + "rejected": true, + "terminal": "ValueError: missing package manifest" + }, + { + "name": "altered implementation", + "rejected": true, + "terminal": "ValueError: package hash: early.py" + }, + { + "name": "extra file", + "rejected": true, + "terminal": "ValueError: package file coverage" + }, + { + "name": "missing source", + "rejected": true, + "terminal": "ValueError: package file coverage" + }, + { + "name": "source hash independent of manifest", + "rejected": true, + "terminal": "ValueError: source SHA256: vendor/pr846/PROOF.md" + }, + { + "name": "source Git object independent of manifest", + "rejected": true, + "terminal": "ValueError: source Git blob: vendor/pr846/stride.py" + }, + { + "name": "duplicate manifest key", + "rejected": true, + "terminal": "ValueError: duplicate JSON key: files" + }, + { + "name": "symlink injection", + "rejected": true, + "terminal": "ValueError: package symlink" + }, + { + "name": "preloaded module substitution", + "rejected": true, + "terminal": "ValueError: local module binding: common" + }, + { + "name": "false receipt boolean integer confusion", + "rejected": true, + "terminal": "ValueError: mathematical receipt mismatch" + }, + { + "name": "existing output preserved", + "rejected": true + }, + { + "name": "full read-only isolated optimized relocation", + "passed": true, + "receipt_sha256": "f30ad0e119c9928f30e2fc97e1911e053fe347bc4fe3f2b328b295141bda1552" + } + ], + "full_readonly_replay": true, + "rejected": 11, + "status": "PASS_STRIDE_DEPTH_PACKAGE" +} diff --git a/research/cyclic-stride-effective-depth-validation/LINUX314-PLATFORM.json b/research/cyclic-stride-effective-depth-validation/LINUX314-PLATFORM.json new file mode 100644 index 0000000000..57a1c500f0 --- /dev/null +++ b/research/cyclic-stride-effective-depth-validation/LINUX314-PLATFORM.json @@ -0,0 +1,9 @@ +{ + "bytecode_disabled": true, + "isolated": true, + "machine": "aarch64", + "manifest_sha256": "0b40eccb5d47d2ac152ed7fe47c259eb71bc17d3c818a71c63e2bc026e9377e3", + "optimized": true, + "platform": "Linux-6.17.0-1032-nvidia-aarch64-with-glibc2.39", + "python": "3.14.8" +} diff --git a/research/cyclic-stride-effective-depth-validation/LINUX314-TERMINAL.json b/research/cyclic-stride-effective-depth-validation/LINUX314-TERMINAL.json new file mode 100644 index 0000000000..a481613cf4 --- /dev/null +++ b/research/cyclic-stride-effective-depth-validation/LINUX314-TERMINAL.json @@ -0,0 +1,6 @@ +{ + "full_package_controls": true, + "manifest_sha256": "0b40eccb5d47d2ac152ed7fe47c259eb71bc17d3c818a71c63e2bc026e9377e3", + "math_sha256": "f30ad0e119c9928f30e2fc97e1911e053fe347bc4fe3f2b328b295141bda1552", + "status": "PASS_FROZEN_STRIDE_DEPTH_PACKAGE" +} diff --git a/research/cyclic-stride-effective-depth-validation/LINUX314.log.txt b/research/cyclic-stride-effective-depth-validation/LINUX314.log.txt new file mode 100644 index 0000000000..5fc04dddac --- /dev/null +++ b/research/cyclic-stride-effective-depth-validation/LINUX314.log.txt @@ -0,0 +1,24 @@ +PASS stride cases 423 scalar coefficient paths 90 +PASS depth controls 12 log boundaries 1545 +PASS cubic budget rows 216 identities 3 +PASS 300 original kernel cases with uniform depth admission +PASS actual cubic stride radix 3 cumulative cases 16 +PASS actual cubic stride radix 4 cumulative cases 32 +PASS actual cubic stride radix 5 cumulative cases 48 +PASS actual cubic stride radix 7 cumulative cases 64 +PASS_CYCLIC_STRIDE_EFFECTIVE_DEPTH arrays=423 kernels=300 uniform=64 scalar_paths=90 budgets=216 kappa=unchanged +PASS package control missing manifest +PASS package control altered implementation +PASS package control extra file +PASS package control missing source +PASS package control source hash independent of manifest +PASS package control source Git object independent of manifest +PASS package control duplicate manifest key +PASS package control symlink injection +PASS package control preloaded module substitution +PASS package control false receipt boolean integer confusion +PASS package control existing output preserved +PASS full read-only isolated optimized relocation +PASS_STRIDE_DEPTH_PACKAGE rejected=11 full_readonly_replay=True +PASS_STRIDE_DEPTH_BINDINGS sources=12 +PASS_FROZEN_STRIDE_DEPTH_PACKAGE diff --git a/research/cyclic-stride-effective-depth-validation/MACOS311-MATH.json.gz b/research/cyclic-stride-effective-depth-validation/MACOS311-MATH.json.gz new file mode 100644 index 0000000000..8f7abb0657 Binary files /dev/null and b/research/cyclic-stride-effective-depth-validation/MACOS311-MATH.json.gz differ diff --git a/research/cyclic-stride-effective-depth-validation/MACOS311-PACKAGE.json b/research/cyclic-stride-effective-depth-validation/MACOS311-PACKAGE.json new file mode 100644 index 0000000000..a5a0fa2d79 --- /dev/null +++ b/research/cyclic-stride-effective-depth-validation/MACOS311-PACKAGE.json @@ -0,0 +1,66 @@ +{ + "controls": [ + { + "name": "missing manifest", + "rejected": true, + "terminal": "ValueError: missing package manifest" + }, + { + "name": "altered implementation", + "rejected": true, + "terminal": "ValueError: package hash: early.py" + }, + { + "name": "extra file", + "rejected": true, + "terminal": "ValueError: package file coverage" + }, + { + "name": "missing source", + "rejected": true, + "terminal": "ValueError: package file coverage" + }, + { + "name": "source hash independent of manifest", + "rejected": true, + "terminal": "ValueError: source SHA256: vendor/pr846/PROOF.md" + }, + { + "name": "source Git object independent of manifest", + "rejected": true, + "terminal": "ValueError: source Git blob: vendor/pr846/stride.py" + }, + { + "name": "duplicate manifest key", + "rejected": true, + "terminal": "ValueError: duplicate JSON key: files" + }, + { + "name": "symlink injection", + "rejected": true, + "terminal": "ValueError: package symlink" + }, + { + "name": "preloaded module substitution", + "rejected": true, + "terminal": "ValueError: local module binding: common" + }, + { + "name": "false receipt boolean integer confusion", + "rejected": true, + "terminal": "ValueError: mathematical receipt mismatch" + }, + { + "name": "existing output preserved", + "rejected": true + }, + { + "name": "full read-only isolated optimized relocation", + "passed": true, + "receipt_sha256": "f30ad0e119c9928f30e2fc97e1911e053fe347bc4fe3f2b328b295141bda1552" + } + ], + "full_readonly_replay": true, + "rejected": 11, + "status": "PASS_STRIDE_DEPTH_PACKAGE" +} diff --git a/research/cyclic-stride-effective-depth-validation/MACOS311-PLATFORM.json b/research/cyclic-stride-effective-depth-validation/MACOS311-PLATFORM.json new file mode 100644 index 0000000000..01a868eb85 --- /dev/null +++ b/research/cyclic-stride-effective-depth-validation/MACOS311-PLATFORM.json @@ -0,0 +1,9 @@ +{ + "bytecode_disabled": true, + "isolated": true, + "machine": "arm64", + "manifest_sha256": "0b40eccb5d47d2ac152ed7fe47c259eb71bc17d3c818a71c63e2bc026e9377e3", + "optimized": true, + "platform": "macOS-27.0.1-arm64-arm-64bit", + "python": "3.11.15" +} diff --git a/research/cyclic-stride-effective-depth-validation/MACOS311-TERMINAL.json b/research/cyclic-stride-effective-depth-validation/MACOS311-TERMINAL.json new file mode 100644 index 0000000000..a481613cf4 --- /dev/null +++ b/research/cyclic-stride-effective-depth-validation/MACOS311-TERMINAL.json @@ -0,0 +1,6 @@ +{ + "full_package_controls": true, + "manifest_sha256": "0b40eccb5d47d2ac152ed7fe47c259eb71bc17d3c818a71c63e2bc026e9377e3", + "math_sha256": "f30ad0e119c9928f30e2fc97e1911e053fe347bc4fe3f2b328b295141bda1552", + "status": "PASS_FROZEN_STRIDE_DEPTH_PACKAGE" +} diff --git a/research/cyclic-stride-effective-depth-validation/MACOS311.log.txt b/research/cyclic-stride-effective-depth-validation/MACOS311.log.txt new file mode 100644 index 0000000000..5fc04dddac --- /dev/null +++ b/research/cyclic-stride-effective-depth-validation/MACOS311.log.txt @@ -0,0 +1,24 @@ +PASS stride cases 423 scalar coefficient paths 90 +PASS depth controls 12 log boundaries 1545 +PASS cubic budget rows 216 identities 3 +PASS 300 original kernel cases with uniform depth admission +PASS actual cubic stride radix 3 cumulative cases 16 +PASS actual cubic stride radix 4 cumulative cases 32 +PASS actual cubic stride radix 5 cumulative cases 48 +PASS actual cubic stride radix 7 cumulative cases 64 +PASS_CYCLIC_STRIDE_EFFECTIVE_DEPTH arrays=423 kernels=300 uniform=64 scalar_paths=90 budgets=216 kappa=unchanged +PASS package control missing manifest +PASS package control altered implementation +PASS package control extra file +PASS package control missing source +PASS package control source hash independent of manifest +PASS package control source Git object independent of manifest +PASS package control duplicate manifest key +PASS package control symlink injection +PASS package control preloaded module substitution +PASS package control false receipt boolean integer confusion +PASS package control existing output preserved +PASS full read-only isolated optimized relocation +PASS_STRIDE_DEPTH_PACKAGE rejected=11 full_readonly_replay=True +PASS_STRIDE_DEPTH_BINDINGS sources=12 +PASS_FROZEN_STRIDE_DEPTH_PACKAGE diff --git a/research/cyclic-stride-effective-depth-validation/README.md b/research/cyclic-stride-effective-depth-validation/README.md new file mode 100644 index 0000000000..56324bc9e3 --- /dev/null +++ b/research/cyclic-stride-effective-depth-validation/README.md @@ -0,0 +1,46 @@ +# Frozen stride-depth validation + +Complete macOS arm64 / Python 3.11.15 and Linux aarch64 / Python 3.14.8 +replays passed with isolation, optimization and bytecode disabled. Their +full mathematical receipts are byte-identical to each other and to the +decompressed `../cyclic-stride-effective-depth/EXPECTED.json.gz`. + +Frozen package manifest SHA256: +`0b40eccb5d47d2ac152ed7fe47c259eb71bc17d3c818a71c63e2bc026e9377e3`. +Complete mathematical receipt SHA256: +`f30ad0e119c9928f30e2fc97e1911e053fe347bc4fe3f2b328b295141bda1552`. + +Each platform recomputed the full mathematics three times: default replay, +rejection of an altered expected receipt, and a read-only relocated replay +in a path containing spaces. Eleven package rejection controls passed on +each platform. Linux also began with the supplied package read-only, outside +a Git checkout, under a durable supervisor that recorded exit status zero. + +The full `*-MATH.json.gz` receipts, package controls, platform information, +terminal records and logs are retained here. Compare decompressed receipt +bytes; container compression identity is not required. `VALIDATION.json` +records their hashes. All 12 retained source files match their pinned Git +objects and SHA256 hashes, as recorded in `SOURCE-GIT-CHECK.json`. + +Evidence includes 423 array cases, 90 scalar coefficient paths, all 300 +original PR846 kernel cases, 64 actual cubic-width kernel executions, +216 integer budgets, three exact nonnegative polynomial identities, +54 admission checks, 1,545 logarithm boundaries, 12 new mathematical +controls and four inherited controls, 12 zero-base checks and 33 traffic +cases through length 131,072. Scalar paths are not huge-array executions. +Original and early-exit outputs agree exactly; the two traffic bills are +40L and 44L respectively, with the additional head returns charged. + +The source record preserves preparation base +`007664306fff84fbb1c9a1b4053b69f439764034`. Before publication the branch was +fast-forwarded to `bbc600db2fc15007b7c914f4f2b2ed55fa909c87`, without changing +any frozen package byte. Selected-record consistency passed there at +`1661960547713947/1000000000000000000`; staged whitespace and byte checks +also passed. Only two new research directories and their workflow are added. +The full repository suite and hosted CI are separate from these local +prepublication records. The scoped workflow repeats both Python versions. + +Finite exact checks support the written universal argument; they are not +independent human review or proof-assistant verification. Clean scratch, +phase access and remaining transform obligations remain explicit. No new +kappa or bit-reversible/borrowed-array implementation is claimed. diff --git a/research/cyclic-stride-effective-depth-validation/SOURCE-GIT-CHECK.json b/research/cyclic-stride-effective-depth-validation/SOURCE-GIT-CHECK.json new file mode 100644 index 0000000000..9eb91072d8 --- /dev/null +++ b/research/cyclic-stride-effective-depth-validation/SOURCE-GIT-CHECK.json @@ -0,0 +1,101 @@ +{ + "sources": [ + { + "git_blob": "9229a4193b004d0dd939a502cfae75c27791dc76", + "git_bytes_equal": true, + "head": "4bdb3e755ea7118170a7a34764df955880dec282", + "path": "vendor/pr846/stride.py", + "sha256": "da56e45f414a633453e06e8d058bcec6c815c73950816fcf049d92c570f8928e", + "source_path": "research/cyclic-inverse-stride-bridge/stride.py" + }, + { + "git_blob": "0cc3867b79082894a18732f7751bc30414da0822", + "git_bytes_equal": true, + "head": "4bdb3e755ea7118170a7a34764df955880dec282", + "path": "vendor/pr846/verify.py", + "sha256": "a56acd90c79597fa57602b053de09fa66930f262c39b849362b49b3cce707f2c", + "source_path": "research/cyclic-inverse-stride-bridge/verify.py" + }, + { + "git_blob": "e1624e72ddffcd9fc2271691f79edcedeffc3c91", + "git_bytes_equal": true, + "head": "4bdb3e755ea7118170a7a34764df955880dec282", + "path": "vendor/pr846/SOURCE.json", + "sha256": "07bc9fe307f254b68810f664bcef0f30eabd130226d39804bb38517777e3a92b", + "source_path": "research/cyclic-inverse-stride-bridge/SOURCE.json" + }, + { + "git_blob": "8987bfdfc4ba6635cc3e0e984ca24d91da429084", + "git_bytes_equal": true, + "head": "4bdb3e755ea7118170a7a34764df955880dec282", + "path": "vendor/pr846/PROOF.md", + "sha256": "3937696d2156e000519fb185a8a55fa7fd55dc12266fe0fe806dba42b2acf4e1", + "source_path": "research/cyclic-inverse-stride-bridge/PROOF.md" + }, + { + "git_blob": "4dcef892b50028a3c9bce2d84954bca2fce44879", + "git_bytes_equal": true, + "head": "4bdb3e755ea7118170a7a34764df955880dec282", + "path": "vendor/pr846/NOTICE.md", + "sha256": "9403006a0d8193298ac9c5dd4036619190aea29bfe37b03d2d716d8be264fc75", + "source_path": "research/cyclic-inverse-stride-bridge/NOTICE.md" + }, + { + "git_blob": "5ef6dd67b6c6cf949fedf16c0cd7b34ca4ccafc2", + "git_bytes_equal": true, + "head": "4bdb3e755ea7118170a7a34764df955880dec282", + "path": "vendor/pr846/vendor/check.py", + "sha256": "a3e46b556894d71a1c83bbbac01c50c1a541285fc9422a3567d5eb1d1ee86e7d", + "source_path": "research/cyclic-inverse-stride-bridge/vendor/check.py" + }, + { + "git_blob": "d3894bd2a1660229f1a7ed16c9d982689effc96f", + "git_bytes_equal": true, + "head": "4bdb3e755ea7118170a7a34764df955880dec282", + "path": "vendor/pr846/vendor/FACTORS.json", + "sha256": "643d60ac24d5e67f6c9305175bd1c99bf5e42edfef6d1995c051e0b98ba446a7", + "source_path": "research/cyclic-inverse-stride-bridge/vendor/FACTORS.json" + }, + { + "git_blob": "1182175a55cb871481de0f56ea9ae56e474705fe", + "git_bytes_equal": true, + "head": "4bdb3e755ea7118170a7a34764df955880dec282", + "path": "vendor/pr846/vendor/interval_kernel.py", + "sha256": "9b7bb24640a9a7d3f83c7951dfef483ec933db4c50de6c0130b85f450eeddfbe", + "source_path": "research/cyclic-inverse-stride-bridge/vendor/interval_kernel.py" + }, + { + "git_blob": "d620e493596f12578c1ce47f216c44c79b65de08", + "git_bytes_equal": true, + "head": "4bdb3e755ea7118170a7a34764df955880dec282", + "path": "vendor/pr846/vendor/scan.py", + "sha256": "1a9c01ca1a29a9be1e756858161202621db29d5d332a4266b4017a9502a50d7e", + "source_path": "research/cyclic-inverse-stride-bridge/vendor/scan.py" + }, + { + "git_blob": "22fbeb8ef0a28dd6b3feea718492091319ceb96e", + "git_bytes_equal": true, + "head": "4bdb3e755ea7118170a7a34764df955880dec282", + "path": "vendor/pr846/vendor/PR628-NOTICE.md", + "sha256": "abeacf1ad1491d5797cfcf1f3832799bbf3b24b99597229d7bc884059a51ec68", + "source_path": "research/cyclic-inverse-stride-bridge/vendor/PR628-NOTICE.md" + }, + { + "git_blob": "0196499f010857b58ea297611f44721a4b7a0ec6", + "git_bytes_equal": true, + "head": "57e0659150d323b784580110b36aa64a2dca2a33", + "path": "vendor/PR862-PROOF.md", + "sha256": "bdb0518892c631f8b6ac149535ac5a92270def19fe7778ca737641cd56b7da0b", + "source_path": "research/cubic-cyclic-inverse/PROOF.md" + }, + { + "git_blob": "737060bd4d9666a925dfd1e17fc6eaa53c289b8d", + "git_bytes_equal": true, + "head": "57e0659150d323b784580110b36aa64a2dca2a33", + "path": "vendor/PR862-NOTICE.md", + "sha256": "08c25cd6248e8c4dc7008e14e9ea7690f9084e94f927bb602363773637a89921", + "source_path": "research/cubic-cyclic-inverse/NOTICE.md" + } + ], + "status": "PASS" +} diff --git a/research/cyclic-stride-effective-depth-validation/VALIDATION.json b/research/cyclic-stride-effective-depth-validation/VALIDATION.json new file mode 100644 index 0000000000..45bc833ff7 --- /dev/null +++ b/research/cyclic-stride-effective-depth-validation/VALIDATION.json @@ -0,0 +1,23 @@ +{ + "files": { + "LINUX314-MATH.json.gz": "05dc40a5df4a6c8f4835ac5e047d02a6e7afe6be1ead8660d4a5a2089800ad5a", + "LINUX314-PACKAGE.json": "84bc7c9843f0d85b2867d0a624f34705c731b143edaeeff6aae50f61894a12c0", + "LINUX314-PLATFORM.json": "1ca3a6ab323b46e44d0b10f6aa94ddaba2b1e7fe079a6fdad57666c386901d93", + "LINUX314-TERMINAL.json": "1097cf983a44389035416ddfe59f4d263a2714a9e6c9e6eb5c22679aed0bbc5a", + "LINUX314.log.txt": "b38bdebffad89473da23fb38560e6ab044d46d50218138ba7c5a52f7cb857224", + "MACOS311-MATH.json.gz": "05dc40a5df4a6c8f4835ac5e047d02a6e7afe6be1ead8660d4a5a2089800ad5a", + "MACOS311-PACKAGE.json": "84bc7c9843f0d85b2867d0a624f34705c731b143edaeeff6aae50f61894a12c0", + "MACOS311-PLATFORM.json": "d822644750410e2d3b295400ddccaf3c96440905143c695179634cc6f2e5947b", + "MACOS311-TERMINAL.json": "1097cf983a44389035416ddfe59f4d263a2714a9e6c9e6eb5c22679aed0bbc5a", + "MACOS311.log.txt": "b38bdebffad89473da23fb38560e6ab044d46d50218138ba7c5a52f7cb857224", + "SOURCE-GIT-CHECK.json": "9693bf2d995bfce75c1921c317033a6171529065b797f3c6da069923b2b5f041" + }, + "full_decompressed_receipts_byte_equal": true, + "linux_source_read_only": true, + "linux_supervisor_exit": 0, + "manifest_sha256": "0b40eccb5d47d2ac152ed7fe47c259eb71bc17d3c818a71c63e2bc026e9377e3", + "math_sha256": "f30ad0e119c9928f30e2fc97e1911e053fe347bc4fe3f2b328b295141bda1552", + "package_rejections_per_platform": 11, + "read_only_full_replay_per_platform": true, + "status": "PASS_TWO_COMPLETE_FROZEN_PLATFORM_REPLAYS" +} diff --git a/research/cyclic-stride-effective-depth/EXPECTED.json.gz b/research/cyclic-stride-effective-depth/EXPECTED.json.gz new file mode 100644 index 0000000000..8f7abb0657 Binary files /dev/null and b/research/cyclic-stride-effective-depth/EXPECTED.json.gz differ diff --git a/research/cyclic-stride-effective-depth/MANIFEST.json b/research/cyclic-stride-effective-depth/MANIFEST.json new file mode 100644 index 0000000000..65e7eb0c80 --- /dev/null +++ b/research/cyclic-stride-effective-depth/MANIFEST.json @@ -0,0 +1,31 @@ +{ + "files": { + "EXPECTED.json.gz": "05dc40a5df4a6c8f4835ac5e047d02a6e7afe6be1ead8660d4a5a2089800ad5a", + "NOTICE.md": "b6e1bab630faf7eb4ad0952173dd789a7f5d6333bf938b275bcf087474f4f189", + "PROOF.md": "30c296d4f1947cbcaaeb0fe575c36e3c2308f1583dde6029efb4a162fb7a4b27", + "README.md": "9a471a07d5f7350d964c91d5b9e760371d3f91f75d6cd878477709e26b5d633a", + "SOURCE-PINS.json": "40757757e517e59149e9152cf9b150b3e3ddf337eb72aef8a3a35649646e019e", + "cases.py": "967143d52063f8697725b5946ee3a6067a85c5179ef31e9e394562bd80a3f70c", + "common.py": "567437ed0bff6cfa13561282ecb537bea06e964da8de3051516846fd4e44bdf6", + "controls.py": "830748252120e15b5fa54a525a7d6d033487d107889ba3f02bf4e5b33637d2b6", + "cubic.py": "7c6cbeedeb77dee4a167fb32b4e14b33f8bd00d69a560d0d2232ecfca7ee59f8", + "early.py": "5b6b23971bfccb4e8d48ebeff2475d48613971645f224db6d4736a77dd1854a4", + "kernels.py": "06c840b27ab4e60f38c0dd75cf18004011300f73024b59935f4bcc3d2d604da4", + "test_package.py": "6d82d4155cdef277018c5eb9ab153f7b5306a9cccec7114480b427fae361d210", + "uniform.py": "51ac9885191f1645f530110e60b92e009560e8f6a0242cdad5396925b5e20308", + "uniform_kernels.py": "f55b60f93e0375f52b538eb06c2e9016b6fcbb6af048ea0f3bd7054ae031d351", + "vendor/PR862-NOTICE.md": "08c25cd6248e8c4dc7008e14e9ea7690f9084e94f927bb602363773637a89921", + "vendor/PR862-PROOF.md": "bdb0518892c631f8b6ac149535ac5a92270def19fe7778ca737641cd56b7da0b", + "vendor/pr846/NOTICE.md": "9403006a0d8193298ac9c5dd4036619190aea29bfe37b03d2d716d8be264fc75", + "vendor/pr846/PROOF.md": "3937696d2156e000519fb185a8a55fa7fd55dc12266fe0fe806dba42b2acf4e1", + "vendor/pr846/SOURCE.json": "07bc9fe307f254b68810f664bcef0f30eabd130226d39804bb38517777e3a92b", + "vendor/pr846/stride.py": "da56e45f414a633453e06e8d058bcec6c815c73950816fcf049d92c570f8928e", + "vendor/pr846/vendor/FACTORS.json": "643d60ac24d5e67f6c9305175bd1c99bf5e42edfef6d1995c051e0b98ba446a7", + "vendor/pr846/vendor/PR628-NOTICE.md": "abeacf1ad1491d5797cfcf1f3832799bbf3b24b99597229d7bc884059a51ec68", + "vendor/pr846/vendor/check.py": "a3e46b556894d71a1c83bbbac01c50c1a541285fc9422a3567d5eb1d1ee86e7d", + "vendor/pr846/vendor/interval_kernel.py": "9b7bb24640a9a7d3f83c7951dfef483ec933db4c50de6c0130b85f450eeddfbe", + "vendor/pr846/vendor/scan.py": "1a9c01ca1a29a9be1e756858161202621db29d5d332a4266b4017a9502a50d7e", + "vendor/pr846/verify.py": "a56acd90c79597fa57602b053de09fa66930f262c39b849362b49b3cce707f2c", + "verify.py": "bf72f42102a044d7db81d2e69a9e4b173113ff5474a1b628ecbaed242fe6ba96" + } +} diff --git a/research/cyclic-stride-effective-depth/NOTICE.md b/research/cyclic-stride-effective-depth/NOTICE.md new file mode 100644 index 0000000000..57939c758d --- /dev/null +++ b/research/cyclic-stride-effective-depth/NOTICE.md @@ -0,0 +1,40 @@ +# Attribution and scope + +New effective-depth argument, cubic-stride integration and checks by Chafik +Boukhalfa (@chafreaky), with substantial OpenAI Codex assistance, under the +repository's Apache-2.0 license. No independent human/delegated-agent review +or literature-priority claim is made. + +- Rohan Guliani (@Rohansguliani), PR846, head + `4bdb3e755ea7118170a7a34764df955880dec282`: arbitrary-stride Euclidean + chain/closure solver, fixed-tape FIFO accounting, uniform error argument + and kernel integration. Its solver, checker, proof, source record and + notice are retained unchanged. `early.py` is an explicitly attributed + adaptation of its `solve` function, adding a charged exact-zero base case. +- Charles Bethin (@cbethin), PR764, head + `983d66f0f2e48ee500ec7eee2da9244c001c5064`: shared-suffix scan identity and + inverse-square error analysis, used through the retained PR846 proof. +- Chafik Boukhalfa, PR628, head + `0768f97d06c623b8211e651543c66135796b62bf`: root-factor certificates, + preparation/phase budgets and exact arithmetic. The five files retained + by PR846 remain byte-identical and independently hash-bound here. +- Chafik Boukhalfa, PR862, head + `57e0659150d323b784580110b36aa64a2dca2a33`: common-operator complement + bound and cubic preparation/execution precision. Its proof and notice + are retained unchanged. +- Ali Romman (@aliromman), PR621, head + `520774462b19b29af41554b74def31f9d01e997e`: prime-power kernel and its + uniform inverse bound, retained through the cited preparation lineage. + +Original notices retain the OpenAI exact-DFT manuscript, classical +Mahler/Wiener arguments, Pan factorization, fast elementary arithmetic, +and the standard queue-from-two-stacks attribution. Their credits and +licenses remain unchanged. Nearest-grid extinction and pointwise-zero +substitution are elementary; no priority claim is made for those ideas. + +The new result removes the stride solver's length-dependent precision +admission and combines its unchanged local error with PR862's cubic bound. +It does not replace the inherited preparation theorem with the finite root +fixtures or claim that the Python reference implements its asymptotic cost. +Clean scratch, phase access and all remaining transform/physical obligations +stay explicit. No new multiplication exponent is claimed. diff --git a/research/cyclic-stride-effective-depth/PROOF.md b/research/cyclic-stride-effective-depth/PROOF.md new file mode 100644 index 0000000000..6019f4d03f --- /dev/null +++ b/research/cyclic-stride-effective-depth/PROOF.md @@ -0,0 +1,238 @@ +# An effective depth bound for the rounded stride solver + +This research argument extends PR846 at head +4bdb3e755ea7118170a7a34764df955880dec282. The original source is retained +unchanged in vendor/pr846/stride.py. Its clean scratch and sequential-tape model +remain unchanged. No borrowed-array, bit-reversible or kappa claim. + +Let beta=2^-g, g>=1, and let u=2^-W with W>=2g+8. Assume every input +coefficient has modulus at most 1-beta. Add one exact zero test at each +recursion level: when every coefficient is zero, return the data rounded +once. This solves that level exactly up to one rounding. Count the test as +one full coefficient scan and head return; traffic is at most 44L records instead of +the original conservative 40L. + +For the early-terminated solver, the number K of non-base levels is bounded independently of L by + + D(g,W)=2g+ceil(log2 W)+4. + +Consequently 4(K+1)u<=beta follows from W>=2g+8. This removes the original +p>=log2(log2 L+2) admission condition, after imposing this sufficient local +working-precision condition instead. + +## Decay of the rounded closure coefficients + +Write rho for the maximum coefficient modulus at a level. Every chain has +at least two coefficients. Its product is initialized with the first exact +coefficient and then rounded after each multiplication. For chain length +ell>=2, its magnitude is bounded by + + rho^ell+u*(1+rho+...+rho^(ell-2)) <= rho^2+u/(1-rho). + +Thus a scalar majorant for the next maximum is rho^2+u/(1-rho). + +First suppose beta<=m=1-rho<=1/2. Since u<=beta^2/16<=m^2/16, + + 1-rho_next >= m(2-m)-u/m >= (23/16)m > sqrt(2)m. + +Within at most 2g levels, the margin therefore reaches 1/2, unless recursion +has already terminated. While rho<=1/2, the majorant is rho^2+2u. +This stays below 1/2, and two further levels give rho<=1/4 (W>=10 is more +than sufficient for these elementary inequalities). + +While rho>2sqrt(u), the same majorant satisfies rho_next<=3rho^2/2. +For t=2rho, this implies t_next<=t^2, starting from t<=1/2. After at most +ceil(log2 W) additional levels, rho<=2sqrt(u): otherwise repeated squaring +would give rho<=2^(-2^j-1)<=u/2, a contradiction. + +One more level gives rho<=6u. At the following level the first multiplication +in every chain has modulus at most 36u^2=2g+8, ceil(log2 W)<=W-1 and 2g<=W-8, hence + + 4(D+1)<=8W-16. + +Also W-g>=ceil(W/2)+4 and 2^ceil(W/2)>=W for W>=4, so + + 2^(W-g)>=16W>4(D+1). + +This proves 4(K+1)u<=beta, and u<=beta/3 is automatic. PR846's margin, +weighted-data and shared-suffix error arguments now apply through at most +D levels. The new terminal system has exact solution x; rounding it once +has error at most u, matching the old terminal bound. Therefore the stated all-length error bound holds for both implementations, +with K equal to the truncated depth, or conservatively min(D,1/beta) in its +geometric error factor. The original structural depth is not used for admission. + +The algebraic source/input restoration properties are unchanged: this is +still a clean-tape solver with the input unmodified. The optional early-exit check adds at most 2 sum L_k<=4L coefficient records +to the original 40L traffic bound. Executing the unchanged implementation +needs no extra scan and retains 40L. +Any full-kernel composition must use a working precision satisfying both +its existing error target and W>=2g+8. That added local condition is O(g) +and preserves the previous polynomial-in-r precision order. + +## Cubic precision for the full kernel at arbitrary strides + +This section combines the local result above with PR862's retained +common-operator argument. The target is the same prime-power kernel +P(U), with U=tau Z_L^w and |tau|=1, as in PR846. All inverse factors use +this one operator. Different noncommuting shifts are outside the argument. + +A stride solve on input norm at most X has error at most + + (u/beta^2)(5+4X/beta)+u. + +After the outer scalar or inner unit rotation and its rounding, its error +is at most 7(X+1)u/beta^3 for beta<=1/2. This is exactly the local bound +required by PR862. Its proof only needs stable factors and that bound; +it does not require the neighboring-stride implementation. + +Let n=r-1, let Q=(1/r) product(z-rho_j), and suppose + + ||Q||_1<=M, ||Q(U)^-1||<=H, + B=max(1,2^n M H). + +The complementary-factor/Mahler argument in the retained PR862 proof +bounds every inverse prefix and contiguous inverse subproduct by B. +Starting with r x, ||x||<=D, the maximum prefix execution error E obeys + + E <= t(r B D+E+1), t=7nB beta^-3 u. + +For t<1 this yields E<=t(rBD+1)/(1-t). This does not repeatedly multiply +the worst reciprocal root margin at every factor. + +For prime-power r>=3 and p,m>=0, retain the source preparation hypotheses +and put + + ell=ceil(log2 r), c=ceil(log2(r-1)), phi=EulerPhi(r), + d=1+2ell+r(r-1)phi, a0=2d+r+2, + g=d+ell+2r+2, beta=2^-g, h=a0+2r, + e=max(d+1,a0+1,p+2a0+m+3), + b=max((r-1)ell,e+r+3). + +PR628/862's charged approximate factorization and coefficient verification +supply prepared roots with stable margin beta, ||Q||_1<=2^r, +||Q(U)^-1||<=2^(a0+1), and source-scaled kernel perturbation at most +2^(-p-2) for D<=2^m. Thus B<=2^h. These are certified premises, not +conclusions drawn merely from a numerical root list. + +Choose + + J=c+2h+3g+ell+m+5, W=p+J+2. + +This W exceeds 2g+8, so the stride admission holds for every L and every +stride. Moreover n<=2^c and 7<=2^3 imply + + t <= 2^(c+h+3+3g-W) <= 1/2, + rBD+1 <= 2^(ell+h+m+1), + E <= 2t(rBD+1) <= 2^(J-W)=2^(-p-2). + +Adding the independently charged kernel preparation perturbation gives +error at most 2^(-p-1), within the target 2^-p. Approximate phase oracles +still need their separately charged perturbation and access budget. + +A sufficient integer guard for data/state magnitudes is + + G=m+ell+h+g+8. + +Indeed each factor input is bounded by rBD+E. PR846's weighted-data +invariant bounds recursive data and closure values by O(rBD/beta); +its corresponding recursive rounding error is at most one under the +chosen W (h>=g). Chain values, products, scalar application and division +fit this guard. Exact arithmetic accumulators and numerator/denominator +products may use a constant-factor wider representation, as usual. + +Using phi<=r, ell<=r and c<=r gives the explicit cubic bounds + + W <= p+m+9r^3, G <= m+6r^3, b <= p+m+6r^3. + +The exact nonnegative remainders in t=r-3 are + +| Bound | Remainder after removing p and m as appropriate | +| --- | --- | +| 9r^3 minus the working overhead | 65t+25t^2+2t^3 | +| 6r^3 minus the integer guard overhead | 51+85t+30t^2+3t^3 | +| 6r^3 minus the factor-precision overhead | 43+67t+22t^2+2t^3 | + +For the final row, the alternative (r-1)ell<=r^2 also fits the cap. +`cubic.py` checks these coefficient identities and exact exponent +inequalities; it does not infer an all-size bound from sampled radices. + +If the incoming data have fractional width w, define the word scale +A=max(p,w)+2m+16r^3. With a supplied exact rational phase of representation +size B_tau, the one-kernel bill is + + soft-O(r^3(p+m+r^3)) + + O(rL) M(A+B_tau) + + O(rL(A+B_tau)). + +The terms are factor preparation/coefficient verification, rounded +execution, and sequential tape traffic. Here M is the cost of the charged +integer arithmetic; the Python reference is not a measured implementation +of asymptotically fast multiplication or factorization. Longer initial +coefficient/phase descriptions retain their actual input-reading cost. +Execution uses the inherited clean scratch tapes and O(L) data records; +there is no borrowed-array or bit-reversible realization claim. + +The original solver retains its 40L traffic bound per stable factor. +Exact inner rotations and scalar applications add their inherited O(L) +work. The optional zero-truncated solver has at most 44L per factor. +Neither bound has a sorting factor or a precision admission depending +on L. Transform-level layout, phase collection, normalization, common +labels and the multiplication reduction remain separate. + +## Evidence and attribution + +The checks compare 423 array cases exactly between the unchanged and +truncated solver, with independent geometric oracles for the short cases. +They include non-dyadic margins and four deeper arrays through L=5741. +Ninety scalar coefficient paths test exact extinction for gaps through +2^-256; they are not huge-array executions. + +All 300 original PR846 kernel cases pass using the uniform effective-depth +admission, with exact output equivalence and their original residual/dense +checks. An additional 64 executions at the actual cubic W cover radices +3/4/5/7, every stride at lengths 1/2/5, two unit phases, and arbitrary odd +lowest working bits. Roots are rounded to no more than the stated +preparation budget. Every common-operator hypothesis and the independent +kernel perturbation are checked before using the cubic budget. + +The source lineage is PR846 (Rohan Guliani), PR764 (Charles Bethin), PR628 +and PR862 (Chafik Boukhalfa), and PR621 (Ali Romman), together with their +retained classical references. This argument and its exact integration +checks do not claim independent human peer review or formal verification. +No new kappa is claimed. diff --git a/research/cyclic-stride-effective-depth/README.md b/research/cyclic-stride-effective-depth/README.md new file mode 100644 index 0000000000..6f0079ca6f --- /dev/null +++ b/research/cyclic-stride-effective-depth/README.md @@ -0,0 +1,47 @@ +# Cubic precision at arbitrary strides, with no length admission + +PR846's clean-tape stride inverse had a precision admission depending on +`log log L`. This package removes that condition. Rounded chain coefficients +become exactly zero after at most `2g+ceil(log2 W)+4` effective levels when +`beta=2^-g` and `W>=2g+8`. The unchanged solver's remaining zero-coefficient +subtree is exactly pointwise rounding, so its original output and 40L +traffic bound are preserved. An optional early-exit version is retained +for direct comparison and charged at 44L, including head returns. + +Combining that result with PR862's existing common-operator inverse bound +gives **working precision `W<=p+m+9r^3` for every cycle length and stride**, +under the inherited certified prime-power preparation hypotheses. The +input norm is at most `2^m`, and the target error is `2^-p`. Root preparation +has an explicit cubic budget too. The complete proof and cost bill are in +[PROOF.md](PROOF.md). + +This is the original clean-scratch tape model. It is separate from PR951's +neighboring-cycle construction without a borrowed data array. It does not +supply bit-reversible arithmetic, physical common labels, transform-level +composition or a multiplication theorem. **No new kappa.** + +## Replay + +Python 3.11+, standard library only, offline: + +```sh +python3 -I -O -B research/cyclic-stride-effective-depth/verify.py +python3 -I -O -B research/cyclic-stride-effective-depth/test_package.py +``` + +The expected marker is `PASS_CYCLIC_STRIDE_EFFECTIVE_DEPTH`. The default +replay checks the manifest, 12 retained source SHA256/Git objects, local +module bindings and every field of the recomputed receipt. `--out` writes +a fresh external copy after comparison. `--bindings-only` checks package +bindings. `--write` is explicit authoring mode, not verification. + +Evidence includes 423 array comparisons, 90 scalar coefficient paths, +300 original kernel cases, 64 actual cubic-budget kernel executions, +216 exact integer budget rows, three nonnegative polynomial identities, +54 admission checks, 1,545 logarithm boundaries, 12 new mathematical controls, four inherited controls, +12 zero-base checks and 33 tape-traffic cases through length 131,072. +Finite checks and the written all-size argument are distinct. + +The original PR846 solver and checker, its five PR628 inputs, and PR862's +proof and notice are retained unchanged. [SOURCE-PINS.json](SOURCE-PINS.json) +and [NOTICE.md](NOTICE.md) identify their exact versions and contributions. diff --git a/research/cyclic-stride-effective-depth/SOURCE-PINS.json b/research/cyclic-stride-effective-depth/SOURCE-PINS.json new file mode 100644 index 0000000000..8fb635094f --- /dev/null +++ b/research/cyclic-stride-effective-depth/SOURCE-PINS.json @@ -0,0 +1,90 @@ +{ + "base_commit": "007664306fff84fbb1c9a1b4053b69f439764034", + "repository": "https://github.com/CrocSwap/integer-mult-bounds", + "sources": [ + { + "git_blob": "9229a4193b004d0dd939a502cfae75c27791dc76", + "head": "4bdb3e755ea7118170a7a34764df955880dec282", + "path": "vendor/pr846/stride.py", + "sha256": "da56e45f414a633453e06e8d058bcec6c815c73950816fcf049d92c570f8928e", + "source_path": "research/cyclic-inverse-stride-bridge/stride.py" + }, + { + "git_blob": "0cc3867b79082894a18732f7751bc30414da0822", + "head": "4bdb3e755ea7118170a7a34764df955880dec282", + "path": "vendor/pr846/verify.py", + "sha256": "a56acd90c79597fa57602b053de09fa66930f262c39b849362b49b3cce707f2c", + "source_path": "research/cyclic-inverse-stride-bridge/verify.py" + }, + { + "git_blob": "e1624e72ddffcd9fc2271691f79edcedeffc3c91", + "head": "4bdb3e755ea7118170a7a34764df955880dec282", + "path": "vendor/pr846/SOURCE.json", + "sha256": "07bc9fe307f254b68810f664bcef0f30eabd130226d39804bb38517777e3a92b", + "source_path": "research/cyclic-inverse-stride-bridge/SOURCE.json" + }, + { + "git_blob": "8987bfdfc4ba6635cc3e0e984ca24d91da429084", + "head": "4bdb3e755ea7118170a7a34764df955880dec282", + "path": "vendor/pr846/PROOF.md", + "sha256": "3937696d2156e000519fb185a8a55fa7fd55dc12266fe0fe806dba42b2acf4e1", + "source_path": "research/cyclic-inverse-stride-bridge/PROOF.md" + }, + { + "git_blob": "4dcef892b50028a3c9bce2d84954bca2fce44879", + "head": "4bdb3e755ea7118170a7a34764df955880dec282", + "path": "vendor/pr846/NOTICE.md", + "sha256": "9403006a0d8193298ac9c5dd4036619190aea29bfe37b03d2d716d8be264fc75", + "source_path": "research/cyclic-inverse-stride-bridge/NOTICE.md" + }, + { + "git_blob": "5ef6dd67b6c6cf949fedf16c0cd7b34ca4ccafc2", + "head": "4bdb3e755ea7118170a7a34764df955880dec282", + "path": "vendor/pr846/vendor/check.py", + "sha256": "a3e46b556894d71a1c83bbbac01c50c1a541285fc9422a3567d5eb1d1ee86e7d", + "source_path": "research/cyclic-inverse-stride-bridge/vendor/check.py" + }, + { + "git_blob": "d3894bd2a1660229f1a7ed16c9d982689effc96f", + "head": "4bdb3e755ea7118170a7a34764df955880dec282", + "path": "vendor/pr846/vendor/FACTORS.json", + "sha256": "643d60ac24d5e67f6c9305175bd1c99bf5e42edfef6d1995c051e0b98ba446a7", + "source_path": "research/cyclic-inverse-stride-bridge/vendor/FACTORS.json" + }, + { + "git_blob": "1182175a55cb871481de0f56ea9ae56e474705fe", + "head": "4bdb3e755ea7118170a7a34764df955880dec282", + "path": "vendor/pr846/vendor/interval_kernel.py", + "sha256": "9b7bb24640a9a7d3f83c7951dfef483ec933db4c50de6c0130b85f450eeddfbe", + "source_path": "research/cyclic-inverse-stride-bridge/vendor/interval_kernel.py" + }, + { + "git_blob": "d620e493596f12578c1ce47f216c44c79b65de08", + "head": "4bdb3e755ea7118170a7a34764df955880dec282", + "path": "vendor/pr846/vendor/scan.py", + "sha256": "1a9c01ca1a29a9be1e756858161202621db29d5d332a4266b4017a9502a50d7e", + "source_path": "research/cyclic-inverse-stride-bridge/vendor/scan.py" + }, + { + "git_blob": "22fbeb8ef0a28dd6b3feea718492091319ceb96e", + "head": "4bdb3e755ea7118170a7a34764df955880dec282", + "path": "vendor/pr846/vendor/PR628-NOTICE.md", + "sha256": "abeacf1ad1491d5797cfcf1f3832799bbf3b24b99597229d7bc884059a51ec68", + "source_path": "research/cyclic-inverse-stride-bridge/vendor/PR628-NOTICE.md" + }, + { + "git_blob": "0196499f010857b58ea297611f44721a4b7a0ec6", + "head": "57e0659150d323b784580110b36aa64a2dca2a33", + "path": "vendor/PR862-PROOF.md", + "sha256": "bdb0518892c631f8b6ac149535ac5a92270def19fe7778ca737641cd56b7da0b", + "source_path": "research/cubic-cyclic-inverse/PROOF.md" + }, + { + "git_blob": "737060bd4d9666a925dfd1e17fc6eaa53c289b8d", + "head": "57e0659150d323b784580110b36aa64a2dca2a33", + "path": "vendor/PR862-NOTICE.md", + "sha256": "08c25cd6248e8c4dc7008e14e9ea7690f9084e94f927bb602363773637a89921", + "source_path": "research/cubic-cyclic-inverse/NOTICE.md" + } + ] +} diff --git a/research/cyclic-stride-effective-depth/cases.py b/research/cyclic-stride-effective-depth/cases.py new file mode 100644 index 0000000000..023e57a229 --- /dev/null +++ b/research/cyclic-stride-effective-depth/cases.py @@ -0,0 +1,80 @@ +"""Exact small-cycle, long-chain and scalar-decay evidence.""" +from fractions import Fraction as F +from common import need,original as st +from early import solve as truncated +from uniform import admission,error_bound + + +def compare(length,stride,beta,bits,dense): + u=F(1,1<bound*bound for a,e in zip(bad,exact)), + 'defect not detected: '+name) + controls.append(dict(name=name,detected=True)) + + u=F(1,1<<16) + need(st.rounded((u/2,F(0)),16)!=st.ZERO,'positive half-grid tie is not zero') + need(st.rounded((u/4,-u/4),16)==st.ZERO,'strict zero threshold') + controls.append(dict(name='strict threshold distinguishes half-grid tie',detected=True)) + zeros=[] + for length in [1,2,7,19]: + for stride in [-1,0,length//2]: + x=[(F(1,3),F(-2,7))]*length + b=[st.ZERO]*length + trace=[] + tape=st.Tape() + short=solve(x,b,stride,10,tape,trace) + full=st.solve(x,b,stride,10,st.Tape()) + need(short==full and len(trace)==1,'zero subtree rounds once') + zeros.append(dict(length=length,stride=stride,records=tape.records)) + + traffic=[] + for length in [1,2,7,64,1000,4096,65536,131072]: + for stride in sorted({0,1,length//2,length-1,97%length}): + full_tape,short_tape=st.Tape(),st.Tape() + st.solve([None]*length,[None]*length,stride,None,full_tape) + solve([None]*length,[None]*length,stride,None,short_tape) + need(full_tape.records<=40*length and short_tape.records<=44*length,'traffic with head returns') + traffic.append(dict(length=length,stride=stride,original_records=full_tape.records, + truncated_records=short_tape.records)) + logarithms=[] + for exponent in range(-257,258): + power=F(2)**exponent + for value,expected in [(power*(1-F(1,1<<20)),exponent),(power,exponent), + (power*(1+F(1,1<<20)),exponent+1)]: + answer=ceil_log2(value) + need(answer==expected and F(2)**(answer-1)2 and q1=3 and 1<=phi<=r and p>=0 and m>=0, + 'integer cubic budget inputs') + ell,c=ceil_log2(r),ceil_log2(r-1) + d=1+2*ell+r*(r-1)*phi + a0=2*d+r+2 + g=d+ell+2*r+2 + h=a0+2*r + e=max(d+1,a0+1,p+2*a0+m+3) + factor_bits=max((r-1)*ell,e+r+3) + J=c+2*h+3*g+ell+m+5 + W=p+J+2 + guard=m+ell+h+g+8 + depth=2*g+(W-1).bit_length()+4 + need(W>=2*g+8 and ceil_log2(4*(depth+1))<=W-g,'uniform stride admission') + # n<=2^c, 7<=2^3 and r*2^(h+m)+1<=2^(ell+h+m+1). + # These exact exponent bounds avoid constructing enormous fractions. + t_exponent=c+h+3+3*g-W + need(r-1<=1<=0 for v in width+guard+factor),'all-size nonnegative remainders') + print('PASS cubic budget rows',len(rows),'identities 3',flush=True) + return dict(rows=rows,working_width_remainder=width,integer_guard_remainder=guard, + factor_preparation_remainder=factor) diff --git a/research/cyclic-stride-effective-depth/early.py b/research/cyclic-stride-effective-depth/early.py new file mode 100644 index 0000000000..edb120c955 --- /dev/null +++ b/research/cyclic-stride-effective-depth/early.py @@ -0,0 +1,60 @@ +"""Optional exact-zero truncation of PR846; extra scans and head returns charged.""" +from common import original as st + + +def solve(x, b, w, bits, tape, trace=None, level=0): + """Return the rounded solution. trace collects per-level (L, w, data, + coefficients) for invariant checks. Values may be None in count-only + mode (structure and traffic only).""" + L = len(x) + st.need(L >= 1 and len(b) == L, 'shape') + w %= L + if 2 * w > L: # reverse orientation: stride L-w <= L/2 + tape.records += 2 * L # read backwards, write forwards + y = solve(x[::-1], b[::-1], L - w, bits, tape, trace, level) + tape.records += 2 * L + return y[::-1] + tape.levels.append((L, w)) + if trace is not None: + trace.append(dict(level=level, length=L, stride=w, x=x, b=b)) + count_only = x[0] is None + # Experimental coefficient scan and return to its initial head position. + tape.records += 2 * L + if not count_only and all(bi == st.ZERO for bi in b): + tape.records += 2 * L + return [st.rounded(xi, bits) for xi in x] + if w == 0: # every point is its own cycle + tape.records += 2 * L + if count_only: + return [None] * L + return [st.rounded(st.div(xi, st.sub(st.ONE, bi)), bits) for xi, bi in zip(x, b)] + # Pass A: zero-seed chains along +w, with rounded chain products. + fifo = st.Fifo(tape, [None] * w) + z = [None] * L + p = [None] * L + for i in range(L): + tape.records += 2 # read x_i, b_i + prev = fifo.pop() + if count_only: + fifo.push(None) + continue + if prev is None: + z[i], p[i] = x[i], b[i] + else: + z[i] = st.rounded(st.add(x[i], st.mul(b[i], prev[0])), bits) + p[i] = st.rounded(st.mul(b[i], prev[1]), bits) + fifo.push((z[i], p[i])) + # Closure system on the w chain ends: Y_k = c_k + a_k Y_((k+L) mod w). + c, a = z[L - w:], p[L - w:] + tape.records += 2 * w # the ends are the tail of the pass-A output + Y = solve(c, a, (-L) % w, bits, tape, trace, level + 1) + # Pass C: reseed chain starts from the closure values (Y_k feeds start k). + fifo = st.Fifo(tape, Y) + y = [None] * L + for i in range(L): + tape.records += 3 # read x_i, b_i; write y_i + prev = fifo.pop() + if not count_only: + y[i] = st.rounded(st.add(x[i], st.mul(b[i], prev)), bits) + fifo.push(y[i]) + return y diff --git a/research/cyclic-stride-effective-depth/kernels.py b/research/cyclic-stride-effective-depth/kernels.py new file mode 100644 index 0000000000..8e2f83b823 --- /dev/null +++ b/research/cyclic-stride-effective-depth/kernels.py @@ -0,0 +1,56 @@ +"""All original PR846 kernels with uniform admission and exact output equivalence.""" +from fractions import Fraction as F +from common import need,predecessor as source,original as st +from early import solve as truncated +from uniform import admission,error_bound + + +def main(): + predecessor=source.pinned_vendor() + rows=[] + original_bound,original_apply=source.cascade_bound,source.apply_kernel + comparisons=[] + + def bound(state,length,stride): + beta,bits,r=state['beta'],state['bits'],state['radix'] + record=admission(beta,bits) + beta0=record['beta0'] + u=F(1,1<0,'positive exact logarithm') + value=F(value) + n,d=value.numerator,value.denominator + e=n.bit_length()-d.bit_length() + larger=n>(d<=0 else (n<<-e)>d + return e+int(larger) + + +def admission(beta,bits): + need(type(beta) in (F,int) and 0=2*g+8,'uniform working precision W>=2g+8') + depth=2*g+(bits-1).bit_length()+4 + beta0=F(1,1<=0,'nonnegative exact source bound') + record=admission(beta,bits) + return original.solve_error_bound(B,record['beta0'],bits,record['effective_depth']) diff --git a/research/cyclic-stride-effective-depth/uniform_kernels.py b/research/cyclic-stride-effective-depth/uniform_kernels.py new file mode 100644 index 0000000000..93188b9864 --- /dev/null +++ b/research/cyclic-stride-effective-depth/uniform_kernels.py @@ -0,0 +1,84 @@ +"""Actual cubic-width executions with each common-operator premise checked.""" +from fractions import Fraction as F +from math import gcd +import json +from common import P,need,predecessor as source,original as st +from early import solve as truncated +from cubic import plan + + +def main(): + checker=source.pinned_vendor() + fixtures=json.loads((P/'vendor/pr846/vendor/FACTORS.json').read_text()) + rows=[] + for fixture in fixtures: + r=fixture['radix'] + if r not in (3,4,5,7): + continue + phi=sum(gcd(r,j)==1 for j in range(1,r)) + budget=plan(r,phi,128,4) + prepared=json.loads(json.dumps(fixture)) + prepared['factor_bits']=min(fixture['factor_bits'],budget['factor_bits']) + prepared['working_bits']=budget['W'] + prepared['roots']=[[str(v) for v in st.rounded(tuple(F(z) for z in pair),prepared['factor_bits'])] + for pair in fixture['roots']] + state=checker.certify(prepared) + need(prepared['factor_bits']<=budget['factor_bits'],'bounded input root preparation') + beta=F(1,1<=beta and mass<=1<=3, the PR628 neighboring +cyclic scan needs working precision + + max(p,w) + O(r^3 + log(D+1)), + +including integer magnitude bits, to approximate the inverse to absolute +error 2^-p on a source of norm <=D initially on the 2^-w grid. The same +precision suffices for coarse-grid in-place source recovery. The previous +uniform scan composition charged O(r^4) because it propagated every local +error through a product of individual reciprocal margins. Here every +partial inverse is bounded by the full inverse and complementary factors. + +Array execution still costs O(rL) rounded scalar operations. With the same +charged approximate-factorization and coefficient-verification algorithms, +the bit cost for a neighboring cyclic layout is + + soft-O((Lr+r^3)(max(p,w)+r^3+log(D+1))). + +This is a standard-arithmetic, supplied-layout theorem. The worst-case +factorization and fast arithmetic are inherited algorithms, not implemented +by the Fraction reference. The restored-source version needs owned widened +source words whose low working bits are initially zero; those bits are +charged. No arbitrary dirty-bit, Clifford, common-label, complete-transform +or multiplication-exponent claim follows. +Phase-oracle costs and the cost of reading a longer phase description are +additional to the displayed bit bound. + +## Full inverse controls every partial inverse + +Let U be an invertible isometry in the maximum norm: ||U^k||=1 for every +integer k. A unit-weighted permutation, including a weighted cyclic shift, +has this property. Let + + f(z)=product_(j=1)^n (z-rho_j) = s Q(z), + M >= sum_j |Q_j|, ||Q(U)^-1|| <= A. + +Assume Q(U) is invertible. All factors are polynomials in the **same U**. +The assertion below does not apply to different noncommuting shifts. + +For a monic polynomial f define its Mahler measure + + M(f)=product_j max(1,|rho_j|). + +For completeness, the elementary circle identity +mean_t log|exp(it)-rho| = log max(1,|rho|) follows by integrating the +power series of log(1-z) when |z|<1 and factoring out rho when |rho|>1. +There are no unit-circle roots in this application. Summing the identities, +then applying concavity of log and Parseval, gives + + log M(f) = mean log|f(exp(it))| + <= (1/2) log(mean |f(exp(it))|^2) + = (1/2) log(sum_j |f_j|^2). + +Thus M(f)<=||f||_2<=||f||_1<=sM. For any subset J of the root occurrences +(multiplicities included), the complementary factor has coefficient norm + + ||product_(j notin J)(z-rho_j)||_1 + <= product_(j notin J)(1+|rho_j|) + <= 2^n M(f) <= 2^n sM. + +As the factors commute, + + product_(j in J)(U-rho_j I)^-1 + = product_(j notin J)(U-rho_j I) Q(U)^-1 / s. + +Every such inverse, including every prefix and every contiguous suffix, +therefore has norm <= B=max(1,2^n M A). Importantly, log B depends on the +full inverse bound, not n times the worst individual reciprocal margin. + +For later source restoration, let K_j=1+|Re rho_j|+|Im rho_j|. Then +K_j<=3 max(1,|rho_j|), so every forward subproduct has norm bounded by +its product of K_j, which is <=F=3^n sM. This also bounds amplification of +the rounding errors introduced during forward restoration. + +## Rounded execution without repeated reciprocal-margin multiplication + +Suppose every factor is implemented by PR628's stable scan with margin +beta, and u=2^-W<=beta^2/2. Including the final outer scalar or inner unit +shift, its local error for an input of norm <=X is at most + + a (X+1)u, a=7 beta^-3. + +Begin with s x and apply all n inverse factors. The exact prefix norm is +<=sBD. Let E_j be the computed prefix error, E=max_(0<=j<=n) E_j, and +delta_j the local error at stage j. Then + + |delta_j| <= a(sBD+E+1)u. + +The error at any prefix is the sum of earlier delta_j propagated through +contiguous inverse subproducts. Each propagation has norm <=B, hence + + E <= nBa(sBD+E+1)u. + +For t=nBa u<1 this implies + + E <= t(sBD+1)/(1-t). (1) + +This rearrangement is not an inductive assumption that the error is small: +all finite computed prefixes exist by the stable closure condition, and +their maximum obeys the displayed inequality. The strict contraction +condition then bounds it. The verifier compares every prefix with an +independent exact dense oracle in its small-cycle cases. + +## Recovering a coarse-grid source + +The cyclic inverse's first pass computes the boundary seed read-only. Its +second pass reads each original source entry before overwriting that slot. +An inner factor's unit shift is performed in place with one saved boundary +entry; an outer factor needs a scalar pass. Thus no full-length intermediate +array is required for evaluation on a neighboring cyclic layout. + +After adding the computed inverse to a distinct working-grid target, +apply the forward factors in reverse order. Each forward pass saves the +original cyclic predecessor before overwriting the current entry. It has +error at most u per output entry. Divide by s and round at W bits. Relative +to the original source, the resulting error is at most + + R <= F E/s + nF u/s + u. (2) + +Alternatively, the finite checker uses the sharper exact recurrence +R=E, then R=K_j R+u for j=n,...,1, then R=R/s+u. If R<2^(-w-1), rounding +each component to the original grid recovers the source exactly. The target +increment is independent of its initial value. The low W-w source bits +are explicit reserved zeros; their capacity is 2L(W-w) bits. Integer guards, +target widening and arithmetic workspace are also charged. + +For a fixed coarse-grid external shear, round the computed increment to +the original grid before its exact addition to the target. The resulting +function f(x) approximates Q(U)^-1 x, depends only on x, and gives the exact +grid bijection (x,y)->(x,y+f(x)). Subtracting the identical f(x) is its inverse. +All arrays then stay on the same coarse grid between calls. The separate +composition proof gives a fixed (w,W) budget for an entire prescribed word; +it does not require new low bits at every stage. + +## Explicit prime-power budgets + +Let r>=3 be a prime power, n=r-1, Dfield=phi(r), H=2^r-1 and +ell=ceil(log2 r), c=ceil(log2 n). To avoid overloading D, write the source +bound as D<=2^m with m>=0. PR621 supplies + + delta = 1/(2rn H^(n Dfield-1)), + |P(z)|>=delta on |z|=1, + ||P(U)^-1|| <= delta^-1 + 2nH/(r delta^2). + +Its absolutely summable Laurent-series argument applies to the isometry U +above, including varying unit phases. No phase table is constructed for +this norm argument. Put + + d=1+2ell+r n Dfield, delta>=2^-d, + a0=2d+r+2, ||P(U)^-1||<=2^a0, + g=d+ell+2r+2, beta=2^-g, + h=a0+2r, + e=max(d+1,a0+1,p+2a0+m+3), epsilon=2^-e, + b=max(n ell,e+r+3). + +As in PR628, approximate-factorization and exact coefficient verification +produce dyadic roots for Q=(1/r)product(z-rho_j) with ||P-Q||_1<=epsilon. +The first two e constraints imply |Q|>=delta/2 on the circle and +||Q(U)^-1||<=2^(a0+1). The last one gives + + D ||P(U)^-1-Q(U)^-1|| <= 2^(-p-2). + +Also ||Q||_1<=H/r+epsilon<=2^r. PR628's radial derivative argument applied +to Q supplies the stated stable margin beta for its inner or reciprocal +outer roots. Consequently the complementary-factor bound gives B<=2^h. +The forward product bound gives F<=2^v for v=3r+ell. + +Define + + J=c+2h+3g+ell+m+5, + W=J+max(p+2,w+v+3). (3) + +This W satisfies u<=beta^2/2 and t<=1/2. Since rBD+1<=2^(ell+h+m+1), +equation (1) yields E<=2^(J-W)<=2^(-p-2). Combining with coefficient +perturbation gives total inverse error <=2^(-p-1), leaving extra slack. +Since 2^J>=n+1, equation (2) gives + + R <= 2^(v+J+1-W) <= 2^(-w-2) < 2^(-w-1), + +which proves exact source recovery after coarse rounding. + +These are explicit integer exponent inequalities, not numerical fits. +Using Dfield<=r, ell<=r, c<=r and r>=3 gives the convenient bounds + + W <= max(p,w)+12r^3+m, + b <= p+6r^3+m. + +For example, J+v+3 <= 7r^3+35r+25+m <=12r^3+m. Likewise +e+r+3<=p+4r^3+11r+14+m<=p+6r^3+m, and n ell<=r^2. +Intermediate magnitude bits also have order O(r^3+m): exact prefixes are +bounded by rBD, scan closure state adds at most O(g) magnitude bits, and +forward subproducts add O(r) bits. A target additionally needs the bits +for its own initial magnitude. Bounds (3) concern fractional precision; +the complete word width includes these integer bits. + +## Preparation, phases, and scope + +The monic exact polynomial rP has coefficient norm <=H and logarithmic +root bound O(r). Pan's approximate-factorization bound, as stated in +Mehlhorn–Sagraloff–Wang, Theorem 2 and Corollary 1, applies at b>=n log n +with cost soft-O(nb+n^2 Gamma) and O(b+n Gamma) coefficient precision. +Here Gamma=O(r) and b=O(p+r^3+m). The same coefficient oracle and +conservative exact product verification from PR628 cost +soft-O(r^3(p+r^3+m)); the latter forms exact O(rb)-bit coefficients. +Repeated roots need not be individually isolated. This inherits the cited +algorithms; the finite fixture checker does not implement their worst-case +runtime. [Approximate-factorization source](https://arxiv.org/pdf/1301.4870), +PDF page 8. + +A supplied exact rational unit phase uses its actual numerator/denominator +length in scalar costs. For an approximate phase oracle, bound the induced +polynomial coefficient perturbation separately and allocate additional +slack by replacing p with p+O(1). Its required precision is O(p+r^3+m) +under the same bounded description assumptions as PR628. An arbitrarily +long phase description remains an extra input cost. + +The proof applies to any implementation of each factor with the stated +local error bound. The concrete in-place and restored-source schedule here +covers neighboring cyclic layouts only. PR846's clean-tape arbitrary-stride +solver has a compatible local bound and an additional depth admission +condition; extending the present tape claim would require retaining that +condition and its clean-scratch model. That solver is not part of this +package or its certified source-restoration claim. + +The cubic improvement comes from bounding intermediate inverse products, +not from improving PR621's circle lower bound. The full multiplication +assembly, common-label and Clifford interfaces, arbitrary dirty storage, +transform-level phase and normalization accounting remain separate. +No new kappa, practical timing improvement, or literature-priority claim +is made. + +## Executable evidence and attribution + +The exact verifier checks 5,220 integer budgets over all 116 prime-power +radices from 3 through 512, five target precisions, three source precisions +and three magnitude bounds. These support implementation of (3); the +inequalities above are the all-size proof. + +There are 120 kernel executions on ten pinned PR628 fixtures, with both +directions, varying exact rational unit phases and lengths 1,2,3,8,17,64. +Sixty executions compare every prefix to independent dense solves. All +120 check the expanded polynomial residual, pre-round recovery error, +exact coarse-grid restoration and total true-kernel error <=2^-128. +The finite tests use PR628's existing, conservative supplied inverse-norm +certificates; they do not claim that those finite certificates are tighter +than every previous finite execution budget. Six controls reject omitted +complement growth, insufficient target/recovery/coefficient precision, +nonshared shifts and lost prefix contraction. + +Credit Ali Romman for PR621, Chafik Boukhalfa for PR628, and the standard +Mahler-measure, cyclic-filtering and approximate-factorization methods. +This extension was prepared by Chafik Boukhalfa with substantial OpenAI +Codex assistance. The independent dense checker is a separate implementation, +not an independent human or delegated-agent review. Source pins are in +`SOURCE.json`. diff --git a/research/cyclic-stride-effective-depth/vendor/pr846/NOTICE.md b/research/cyclic-stride-effective-depth/vendor/pr846/NOTICE.md new file mode 100644 index 0000000000..4dcef892b5 --- /dev/null +++ b/research/cyclic-stride-effective-depth/vendor/pr846/NOTICE.md @@ -0,0 +1,22 @@ +# Notice and attribution + +New material in this directory is by Rohan Guliani (@Rohansguliani) and is +released under Apache-2.0. Substantial AI assistance was used in the +derivation, implementation and writing. No human peer review or +proof-assistant verification is claimed. + +Predecessor work: + +* **#621, Ali Romman (aliromman).** Kernel and the `L`-uniform circle and + inverse bounds (`research/prime-power-cyclic-inverse`). +* **#628, Chafik Boukhalfa (chafreaky).** Certified approximate + factorization, preparation and phase budgets, the two-scan primitive, the + dirty-shear composition and the sort-route layout charge. The files in + `vendor/` are byte-identical to #628 head `0768f97d`. Its notice is + retained in `vendor/PR628-NOTICE.md`. +* **#764, Charles Bethin (cbethin).** The shared-suffix identity + `1-Q >= beta G` and the inverse-square scan bound, used in Lemma 1. No + #764 code is consumed. + +The two-stack queue and Euclidean stride reduction are standard techniques. +No literature-priority claim is made. diff --git a/research/cyclic-stride-effective-depth/vendor/pr846/PROOF.md b/research/cyclic-stride-effective-depth/vendor/pr846/PROOF.md new file mode 100644 index 0000000000..8987bfdfc4 --- /dev/null +++ b/research/cyclic-stride-effective-depth/vendor/pr846/PROOF.md @@ -0,0 +1,211 @@ +# Linear-traffic rounded inversion for every cyclic stride + +## Result and scope + +PR628 inverts PR621's kernel `P(tau Z_L^w)` for neighbouring strides with +precision `p+O(r^4)` that does not depend on `L`. For other strides it routes +the cycles into contiguous order with two merge sorts, at a cost of +`O(L(B+log L)log L)`. That sort cost brings back a `log L` traffic factor. +This note removes the sort. The solver below handles every stride `w` with +`O(L)` sequential record moves and `O(L)` rounded operations per factor. Its +error bound does not depend on `L`. + +**Theorem 1 (one stable factor, any stride).** Let `L>=1`, let `w` be any +integer, and let `0= g+2+log2(K+1)`, where `beta=2^-g`. Any execution +budget for target precision `p >= log2(log2 L + 2)` already meets it. + +## Algorithm + +Normalize `w` modulo `L`. If `2w>L`, reverse the arrays. Reversal turns the +stride into `L-w`, which is at most `L/2`. A tape reads one array backwards +while it writes another forwards, which costs `2L` record moves each way. +If `w=0`, return `x_i/(1-b_i)` rounded. + +Otherwise the residue classes modulo `w` form chains. Chain `c` contains +`c, c+w, c+2w, ...`. Each chain has at least two members because `w<=L/2`. + +1. **Pass A.** Scan `i=0..L-1`. Read the lag-`w` predecessor from a FIFO + that starts with `w` start markers. Compute the zero-seed value + `zhat_i = rnd(x_i + b_i zhat_(i-w))` and the chain product + `pihat_i = rnd(b_i pihat_(i-w))`. At a chain start, `zhat=x` and + `pihat=b` exactly. +2. **Closure.** The last `w` positions `e=L-w+k` are the chain ends. The + start of chain `c` has predecessor `c-w+L`, which is end `k=c`. Hence the + end values satisfy + + Y_k = zhat_(L-w+k) + pihat_(L-w+k) Y_((k+L) mod w). + + This is the same problem on `w` entries with stride `(-L) mod w`. + Solve it recursively. +3. **Pass C.** Scan `i=0..L-1` again. This time the FIFO starts with + `Y_0..Y_(w-1)`. Compute `yhat_i = rnd(x_i + b_i * pop())` and push it. + +Each level at least halves the length, so `sum_k L_k <= 2L` and +`K <= floor(log2 L)+1`. A FIFO built from two stacks moves each record at +most four times: a push, a transfer pop, a transfer push and a pop. A stack +on a tape keeps its head at the top. Pass A, the closure handoff, pass C and +the two reversals therefore cost at most a fixed multiple of `L_k` record +moves at level `k`. In the finite replay through `L=131072` the maximum is +29.68 per entry. For comparison, PR628's two sorts make +`4L ceil(log2 L)` record moves. A record holds the `O(B)` bits of one or +two numbers. Moving it costs `O(B)` tape cells. Loop counters need only +amortized `O(1)` bit changes per step, plus `O(log L)` per level for the +values `L_k` and `w_k`. Stride arithmetic over all levels costs +`O(log^2 L)` bit operations. + +## Proof of Theorem 1 + +**Notation.** `Shat_k` is the computed system at level `k`, with data +`xhat^k` and coefficients `bhat^k`. `Ytilde^k` is its exact solution, and +`m_k = min_i (1-|bhat^k_i|)` is its margin. `S*` is the exact Schur +complement of `Shat_k` on the chain ends. The solution of `S*` is the +restriction of `Ytilde^k` to those ends. + +**Lemma 1 (PR764's shared-suffix identity).** Let `q_1..q_l` lie in +`[0,1-m]`. Put `P_j = q_(j+1)...q_l` and `G = sum_j P_j`. Then + + sum_j (1-q_j) P_j = 1 - q_1...q_l, hence G <= (1-|pi|)/m. + +The quantity `pi` is the chain product. A rounded recursion multiplies its +previous error by `b` and adds at most `u`, so after a chain its error is at +most `uG`. Therefore + + |zhat_e - z_e| <= u(1-|pi_e|)/m_k, |pihat_e - pi_e| <= u(1-|pi_e|)/m_k. + +**Lemma 2 (margins never shrink below beta).** From Lemma 1, +`1-|pihat| >= (1-|pi|)(1-u/m_k)`. A chain has at least two members, so +`1-|pi| >= 1-(1-m_k)^2 = m_k(2-m_k)`. Hence `m_(k+1) >= f(m_k)` with +`f(m)=(2-m)(m-u)`. The function `f` is concave on `[beta,1]`. At the +endpoints, + + f(beta) = (2-beta)(beta-u) >= (3/2)(2beta/3) = beta when beta<=1/2 and u<=beta/3, + f(1) = 1-u >= beta. + +Therefore `m_k >= beta` at every level. The bound does not depend on depth. +The replay checks `|bhat|<=1-beta` exactly at every level of all 2052 +generic cases. + +**Lemma 3 (weighted data).** Suppose `|xhat^k_i| <= A_k(1-|bhat^k_i|)`. +Then the telescoping identity gives `|z_e| <= A_k(1-|pi_e|)`. Lemma 1 adds +at most `u(1-|pi_e|)/m_k`, and Lemma 2 compares `1-|pi|` with `1-|pihat|`. +Together they give the same invariant at level `k+1` with + + A_(k+1) = (A_k + u/beta)/(1-u/beta), A_0 = B/beta. + +The admission condition `4(K+1)u <= beta` gives `A_k <= 2A_0+1` at every +level. + +**Lemma 4 (weighted inverse).** Suppose `|v_i| <= C(1-|b_i|)`. Then the +solution of `Y = v + b W Y` satisfies `|Y_i| <= C`. The Neumann series has +weights `P_j(1-q_j)`, and these telescope to at most one. In particular, +`|Ytilde^k| <= A_k`. + +**Error recursion.** `Shat_(k+1)` differs from `S*` only by the pass-A +rounding. The two solutions satisfy + + (I - Bhat W)(Ytilde^(k+1) - Y*) = Delta x + Delta B * W Y*. + +By Lemma 1, each entry of the right side is at most +`(u/beta)(1+A_k)(1-|pi_e|)`, and `1-|pi_e| <= (1-|pihat_e|)/(1-u/beta)`. +Lemma 4 then bounds the solution difference by +`(u/beta)(1+A_k)/(1-u/beta) <= 2(u/beta)(1+A_k)`. Pass C seeds every chain +with the closure value. The seed error is multiplied by the chain prefix +product. That product contains at least one coefficient, so its modulus is +at most `1-beta`. Pass C's own rounding adds at most `u/beta`. Let +`e_k = |Yhat^k - Ytilde^k|`. Then + + e_k <= (1-beta)(e_(k+1) + 2(u/beta)(1+A_k)) + u/beta, + e_K <= u (base case: one exactly rounded division, |1-b|>=beta). + +Sum this recursion. At level 0 the data are exact, so `Ytilde^0 = y`. With +`A_k <= 2B/beta+1` and `sum_(k= log2(log2 L+2)`. + +## Not closed here + +* PR628's dirty-array contract allows `ceil(log2(r-1))` borrowed arrays and + only `O(1)` clean scalars. That contract arises in the exact-width word + model. The stride solver here uses blank scratch tape, which is free in + the sequential-tape model and is erased at linear cost. It has not been + recast for borrowed arrays. That case still uses PR628's + `O(p+log(D+1)+r^5)` precision and neighbouring-stride leaves. +* The guard `O(r^4)` is a proof bound. Numerical probes for `r<=32` put + `min_|z|=1 |P(z)|` near `2^-10`, while PR621's bound gives up to + `2^-27880`. A sharper lower bound would shrink every budget above. + This package does not certify those probe values. +* Composition across the complete transform, the transform's phase + collection, normalization and the integer-multiplication reduction remain + open. No integer kappa, complex b, or BIT c changes. diff --git a/research/cyclic-stride-effective-depth/vendor/pr846/SOURCE.json b/research/cyclic-stride-effective-depth/vendor/pr846/SOURCE.json new file mode 100644 index 0000000000..e1624e72dd --- /dev/null +++ b/research/cyclic-stride-effective-depth/vendor/pr846/SOURCE.json @@ -0,0 +1,15 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "pr621": {"url": "https://github.com/CrocSwap/integer-mult-bounds/pull/621", "head": "520774462b19b29af41554b74def31f9d01e997e", "author": "Ali Romman (aliromman)", "use": "circle lower bound and L-uniform inverse bound; on main at research/prime-power-cyclic-inverse"}, + "pr628": {"url": "https://github.com/CrocSwap/integer-mult-bounds/pull/628", "head": "0768f97d06c623b8211e651543c66135796b62bf", "author": "Chafik Boukhalfa (chafreaky)", "use": "certified factors, preparation and perturbation budget, dirty-shear composition, sort-route layout charge; vendored files below are byte-identical to that head"}, + "pr764": {"url": "https://github.com/CrocSwap/integer-mult-bounds/pull/764", "head": "983d66f0f2e48ee500ec7eee2da9244c001c5064", "author": "Charles Bethin (cbethin)", "use": "shared-suffix identity 1-Q >= beta*G, reused in Lemma 1; no code consumed"}, + "vendored_sha256": { + "check.py": "a3e46b556894d71a1c83bbbac01c50c1a541285fc9422a3567d5eb1d1ee86e7d", + "FACTORS.json": "643d60ac24d5e67f6c9305175bd1c99bf5e42edfef6d1995c051e0b98ba446a7", + "interval_kernel.py": "9b7bb24640a9a7d3f83c7951dfef483ec933db4c50de6c0130b85f450eeddfbe", + "scan.py": "1a9c01ca1a29a9be1e756858161202621db29d5d332a4266b4017a9502a50d7e", + "PR628-NOTICE.md": "abeacf1ad1491d5797cfcf1f3832799bbf3b24b99597229d7bc884059a51ec68" + }, + "two_stack_queue": "standard amortized queue from two stacks (folklore; e.g. Okasaki, Purely Functional Data Structures, 1998)", + "unimplemented": "Pan worst-case factorizer, fast elementary functions, a literal Turing-machine tape, borrowed-array (dirty) form of the stride solver, transform-level composition and the multiplication reduction." +} diff --git a/research/cyclic-stride-effective-depth/vendor/pr846/stride.py b/research/cyclic-stride-effective-depth/vendor/pr846/stride.py new file mode 100644 index 0000000000..9229a4193b --- /dev/null +++ b/research/cyclic-stride-effective-depth/vendor/pr846/stride.py @@ -0,0 +1,168 @@ +"""Rounded stride-w cyclic first-order solver with linear sequential traffic. + +Solves y_i = x_i + b_i * y_((i-w) mod L) for |b_i| <= 1-beta by a +Euclidean chain/closure recursion. Every array pass is in natural order +(or its reverse) and reads the lag-w predecessor from a FIFO built from two +stacks, which a fixed number of sequential tapes implement with amortized +O(1) record moves. See PROOF.md. Exact rational arithmetic is used; the only +inexactness is the explicit nearest-dyadic rounding on a grid of spacing u. +""" +from fractions import Fraction as F + +ZERO = (F(0), F(0)) +ONE = (F(1), F(0)) + + +def add(a, b): return (a[0] + b[0], a[1] + b[1]) +def sub(a, b): return (a[0] - b[0], a[1] - b[1]) +def mul(a, b): return (a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0]) +def norm2(a): return a[0] * a[0] + a[1] * a[1] + + +def div(a, b): + d = norm2(b) + if not d: + raise ValueError('zero divisor') + c = mul(a, (b[0], -b[1])) + return (c[0] / d, c[1] / d) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def rounded(a, bits): + """Nearest point of the grid 2^-bits in each component, ties upward.""" + if bits is None: + return a + scale = 1 << bits + + def component(v): + w = v * scale + F(1, 2) + return F(w.numerator // w.denominator, scale) + return (component(a[0]), component(a[1])) + + +class Tape: + """Counts sequential record traffic. One unit is one B-bit record moved + past a tape head (read or write). Stacks are tapes whose head sits at + the top; a FIFO is two stacks; reversal copies one record per unit.""" + + def __init__(self): + self.records = 0 + self.levels = [] + + +class Fifo: + def __init__(self, tape, initial): + self.tape = tape + self.inbox = [] + self.outbox = [] + for v in initial: + self.push(v) + + def push(self, v): + self.tape.records += 1 + self.inbox.append(v) + + def pop(self): + if not self.outbox: + while self.inbox: # one transfer per record, amortized O(1) + self.tape.records += 2 + self.outbox.append(self.inbox.pop()) + self.tape.records += 1 + return self.outbox.pop() + + +def solve(x, b, w, bits, tape, trace=None, level=0): + """Return the rounded solution. trace collects per-level (L, w, data, + coefficients) for invariant checks. Values may be None in count-only + mode (structure and traffic only).""" + L = len(x) + need(L >= 1 and len(b) == L, 'shape') + w %= L + if 2 * w > L: # reverse orientation: stride L-w <= L/2 + tape.records += 2 * L # read backwards, write forwards + y = solve(x[::-1], b[::-1], L - w, bits, tape, trace, level) + tape.records += 2 * L + return y[::-1] + tape.levels.append((L, w)) + if trace is not None: + trace.append(dict(level=level, length=L, stride=w, x=x, b=b)) + count_only = x[0] is None + if w == 0: # every point is its own cycle + tape.records += 2 * L + if count_only: + return [None] * L + return [rounded(div(xi, sub(ONE, bi)), bits) for xi, bi in zip(x, b)] + # Pass A: zero-seed chains along +w, with rounded chain products. + fifo = Fifo(tape, [None] * w) + z = [None] * L + p = [None] * L + for i in range(L): + tape.records += 2 # read x_i, b_i + prev = fifo.pop() + if count_only: + fifo.push(None) + continue + if prev is None: + z[i], p[i] = x[i], b[i] + else: + z[i] = rounded(add(x[i], mul(b[i], prev[0])), bits) + p[i] = rounded(mul(b[i], prev[1]), bits) + fifo.push((z[i], p[i])) + # Closure system on the w chain ends: Y_k = c_k + a_k Y_((k+L) mod w). + c, a = z[L - w:], p[L - w:] + tape.records += 2 * w # the ends are the tail of the pass-A output + Y = solve(c, a, (-L) % w, bits, tape, trace, level + 1) + # Pass C: reseed chain starts from the closure values (Y_k feeds start k). + fifo = Fifo(tape, Y) + y = [None] * L + for i in range(L): + tape.records += 3 # read x_i, b_i; write y_i + prev = fifo.pop() + if not count_only: + y[i] = rounded(add(x[i], mul(b[i], prev)), bits) + fifo.push(y[i]) + return y + + +def levels(L, w): + """Number of non-base recursion levels K (stride halves every level).""" + K = 0 + while True: + w %= L + if 2 * w > L: + w = L - w + if w == 0: + return K + L, w, K = w, (-L) % w, K + 1 + + +def exact_cycle_solve(x, b, w): + """Independent oracle: per-cycle finite geometric closure.""" + L = len(x) + y = [None] * L + for i in range(L): + total, weight, j = ZERO, ONE, i + while True: + total = add(total, mul(weight, x[j])) + weight = mul(weight, b[j]) + j = (j - w) % L + if j == i: + break + y[i] = div(total, sub(ONE, weight)) + return y + + +def solve_error_bound(B, beta, bits, K): + """PROOF.md, Theorem 1: kappa*(u/beta)*(5+4B/beta)+u, kappa=min(K,1/beta).""" + u = F(1, 1 << bits) + kappa = min(F(max(K, 1)), 1 / beta) + return kappa * (u / beta) * (5 + 4 * B / beta) + u + + +def admitted(beta, bits, K): + u = F(1, 1 << bits) + return beta <= F(1, 2) and u <= beta / 3 and u * 4 * (K + 1) <= beta diff --git a/research/cyclic-stride-effective-depth/vendor/pr846/vendor/FACTORS.json b/research/cyclic-stride-effective-depth/vendor/pr846/vendor/FACTORS.json new file mode 100644 index 0000000000..d3894bd2a1 --- /dev/null +++ b/research/cyclic-stride-effective-depth/vendor/pr846/vendor/FACTORS.json @@ -0,0 +1,402 @@ +[ + { + "radix": 3, + "embedding": 1, + "roots": [ + [ + "-49530798732358771146118901080958076273052470912342260266258914227109710325121387637640669783171544976658235453737966492290535102314016775076196131137253281608605845416954368911072190053165368500463077348683479820730223655747230034954087192637416985282711781569366341015472238222901103154593890125768068166111/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "13475305001181955152635744113343228941870362999235845156852762789867665164197346764233250937361286208084929252607275859697194884125876348244811537318304219573113812813781235059890295167053180994008138010725194287959555680271101985158640265590661977057048524039192974778963502923615772560082862029626247356915/11235582092889474423308157442431404585112356118389416079589380072358292237843810195794279832650471001320007117491962084853674360550901038905802964414967132773610493339054092829768888725077880882465817684505312860552384417646403930092119569408801702322709406917786643639996702871154982269052209770601514008576" + ], + [ + "-170592372764629843867157976456437557496591605016661465377627293282379593058008669423781376417268214078363699912331157051907114448593591383586878883684704623349440149303389490092308949295538404178253469730760549011796778712019234252302695280536406885179602202888146765328976392461917368148065254242900199873601/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-46411209039859540974176647362240554857493432165837745376222291831822369430116719300153189465225800706342648078500395279868781491155333745970178758722507111433403998868313736485156740909917748907461424289090884948593897673112150836753179290605396652366677201787911857343898640266500768045571317618646184981515/22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152" + ] + ], + "beta": "1/32", + "factor_bits": 1024, + "working_bits": 768, + "target_bits": 128 + }, + { + "radix": 4, + "embedding": 1, + "roots": [ + [ + "18839227606306460928750436776825014273496077882053237212856774153163841259423959845929808348046828320902424357370784726029073309579224150022196016795678227966011136545266483378669974662335269472502528125472018535885295396863622929964034462260120294171947340433492325221872688727385544533583048885326400903597/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "12796926340379968523293584046788682991068081520875261248350397459182248423294625032260126325308015563095435234200881380927938236702421262255195096551267084999719624023209458696352316971284756123109784206671973205284974765619111294724890379061690528176512207203087118838657451331182211930074180553022205037717/11235582092889474423308157442431404585112356118389416079589380072358292237843810195794279832650471001320007117491962084853674360550901038905802964414967132773610493339054092829768888725077880882465817684505312860552384417646403930092119569408801702322709406917786643639996702871154982269052209770601514008576" + ], + [ + "-67937135992698413485848028692002309503217002121030373236286063853851112002834956545147982981350737462809662177353146777437281023159349478379475061510263643694108201092716816673971478633600166383954345966000686009575573734331558302198133439150275018280298091260360209316562436177361876091474717502741308380027/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304", + "5835616822424528393018276731807351617575339522981934688817604363901147520344005371600541622764811103253229296878826668528234697818556822582094397306602957922127281544555831623274134108430066605792876461395490781682749981003075479237572505884700169238753265724966398880489058963937223602091905317904711941499/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304" + ], + [ + "73140002878255602241711158912281750377574232707837598458857400104507930946414903201953646254948585509216110472170409026061261014243757141002856798605902222432653774400735298040913720270819301943861772786445719733578848858120147397354586183800152541785894513923362213804429810043582243527480464796014608479295/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-101965650555502300179425242688687701922297090080040644000576714490063310164897746283818166254598757360914998703650200531654685086831846027226086641171539829015447750993610037727758956893880614628095284026104635045032186714065136378505612299766669091235639722208461448795105675773286000398597466612399588126671/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304" + ] + ], + "beta": "1/32", + "factor_bits": 1024, + "working_bits": 768, + "target_bits": 128 + }, + { + "radix": 5, + "embedding": 1, + "roots": [ + [ + "18410399432434593285169076294769602275894540638275295419244544381879773242101229303192661033873560946309710294140171891893900372823577853227464636318197065166893737578492060390055766605671671799743745029504200984650324085253453636489088551766233790345264477955593735634726155875498225455897152145422527110857/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304", + "88926944313291886897540182389959275756316664511795052113045934836868436387626350644157761509746590523735127289561482706452011713192888368531757723983026280383546034048812998372260884484021077768824721106874944498264700931287184901932524740060871613024772296891180592599727648764929046216006068462246504374811/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "-167545453603640477774873977068820521490816283320967799058419418306745166535530698475752796883467944874062781699503482002031721106189111733803133269028126037337336557647540282023493990675410251006273872459992624200925878916492155324954465535073616098706096481035319289799489810569175272312690818408702357774707/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "154556349957963769064367096421348364953192572923709918873780464142362058554060160862470338328380796109257170485631887393041866922712420579126848130118663444268007905141768967672162702816973919207497792878550271826416467017062585388767141690359055369161984340591026398951036705551282299373389928249065466957777/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-246025941110189748337782398645962696281966535596390989644134716992878047915802819087254020031137007742552596547220618828803263741659091725736455982888598484589330876923271022291321628747736395867996706991862080909718783945688678933156172363230796038024619721716767295126085355526352538295019215908632644428645/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-80017827675325207808535539612151904575968566998857213977754346138586638701168117409273474539675100516306047838318004762335480802433891996015633286597935493715465198565408881501720917279311214162172063959383782684101469915657487668687514739767345963311117394934914437584673901163128059865890829000565376585079/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "215712256432223249791838888842272962081449782057642246390000600800148072180501294511436300947360881829332748816482640829932179778301978229874156851415522923858548828681148808544326153700577210577826268148302190110772732181100719565734873230271520263077404047413202169567004576671193383551882477838906429979943/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-343345360254883912964398674422494284929201599795775129858953529504351638375339699421889616865554200011416676596545392950323715795619267003477668104686330984199520110843844773329958643601792506764296355657817381043552933491542452533905205092594361844214785757345776857492089057313413558295951124845050277505639/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ] + ], + "beta": "1/64", + "factor_bits": 1024, + "working_bits": 768, + "target_bits": 128 + }, + { + "radix": 7, + "embedding": 1, + "roots": [ + [ + "120836177722361423700961200616746340939117621826067821546283999942075497210076949759460370715678904626969473270870038244427213482017330996532718477962097048482765518680096123147561488619800104812093083654163138766755667970537231472653449243809561047362543545086368385980168510507433365046715788937161703716085/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "68125532188584294286663341974472312621216872199921619246009406654878430278942492383247031997235044995684216361049673718348715972217344544049530857813500428243332162775155119877092074201530144921889140264057120091137424453307505120185335081880162914431352955991832950471916200413514695655590549673800742347681/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "-23352251484866588814984102757151938020295470378892869474143458720257279649755690100107547794252764950418419952156812046731260229125257633674879904341802608588717478148648944135150233501962993159400202815681865439334171539946279604850805926161998688918951893236128852170350420117380648887992523528703050194783/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "12132115037519896013585104434007386698287966150528447173769745653094849377705471451533571302407701987585405260939215552836593163546110098278844478687559077536413118639791236269008047600329470759689721901333721666143586701098282693338033702985076136987291514686849805451278368411427725280317893977203863584583/11235582092889474423308157442431404585112356118389416079589380072358292237843810195794279832650471001320007117491962084853674360550901038905802964414967132773610493339054092829768888725077880882465817684505312860552384417646403930092119569408801702322709406917786643639996702871154982269052209770601514008576" + ], + [ + "-92291382711014775221380021171202817794657125260699000287682436525116249639100986456003288102293593362503506340776371812568234629218022304094954295338321708547490187028615230917002633870289187269289797994714342072570440381702763361962356356505306507682202967183538465154964375441642931008189553934230981931559/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "119712689918657651145189233762925546457090337327810229148877839636675818166345698397220337691661044465436596246450977563970023691296540621113539611731979073364553791157261962787179002477238112224575127636003783615332436194461854998451162028079761177278027679849503098212639903585808693056859631675024978403655/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-241550214101542094297167535638151897507830585201411331736006717246868123702109366984690181768784545848116906421886000314994526788327659530751761942604584557795696877540130891932133377552105984741145270626005788962709578395270874088233819746015884483414705471639012552028950063730900626438412769308246134412423/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-44636521770478560155358654717184927568066750073373513015128082461673476496822166780757639936727928123676721979818426533919863914831246651250724819329685161786373417321779253128206274251444083819402120012005681947845516990805594334226921578412078056649090375828519802643691118444466847932595531100425230751867/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "-30203061381136258809439665112684149466527548721381460346906377733218206927673101886508360525270680857362678859262610296498976901610754244593890353821856268232116927740493603349537265139809747876075016798077935946460243881062966294672661437770702005876180419387161259974619074523496342984580783717368906963491/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "-305110068800135848497848181573777483300901124284310624770759696080464881064477659631992063113691884421747360163819890589058455217115247182223505704124808283746309249249359889226760626023333388774388559141421503453637601946482828567415910388069454422041311561341290600832629150554612317238895704865818852456303/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "321370196207928824720915204711075455015246912340098126751032311594524033112453537345445629309422537818066392684089031234715114932786141935425039670921672922753033036803089443416637226862726853593951312786044577899391357952048006221305816041423551248138900234992740786667031784280806046850529260976098348049203/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-24530473927531504467392407392323938052443883461832126187972943992643983667419063708657378422819680820353364287646948211385092126125885316040368239976682069981937416789728921378575979136146542456286295719081463657034678512460199743093437741946258402070242087927157968777687527815825283515074190769218475070497/22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152" + ] + ], + "beta": "1/512", + "factor_bits": 1024, + "working_bits": 768, + "target_bits": 128 + }, + { + "radix": 8, + "embedding": 1, + "roots": [ + [ + "8676521756510435418408946804461767324891306204862417174847745121263025946650658922911780062841899310292089809846830833767424385518217195893825119278967539421517248349379935548836275419185719990536047729374806106190931483190985689626709113976582272252929209174868395094303365494483709135736692733466731317795/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "46927175506395187795687931561127127492542914401987186784106756230323458946080644106593751363160127877209084537223858819579870206674713563202937305209536930043680869885123270522345465099010053820092378973496193748874813123926250211050432217802376301722910925291572156201602782436939032617502745379314433603689/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304" + ], + [ + "66202580992830939447277596770820976547224187818360015042315917699790056190563629777404288554237323292216596605503553003282188641500233854198283302909676455062335042428271478810798541736972692302397024682764300702362971680590029381246736867638520196791172922404288387541122616211813091943463685403402194819637/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "121765996413538109244722158430733772946581021648295379494316178425975201830123378250127037871022862140665047768946333869871635524590445958253367982270652171353818448747755198251644533171986927552011666923832137891571028711514868831622149886611924577771659219065857057020727239216653669500246218019089692681775/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-63004972185514719302016938882476801018029290150894658797428428794872008178224844068489106570343956469890320581237050176572657244106576400241496924996645905145525690133237596136064437406720491787085549650786601720713499367232077045311041089715211178346785441054922158278590254819899949862505839484404422514173/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "162089912107789904580698670024539381013319877304490279642065801647607770297007606234339566380838505368774389327096714260667996331814249381137709093996072587356720324791880511287815302447216666542808264118488552050522502999610415668210833042811542567219354932850746955158614010677677778588862432609198364889609/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-114541150781975074659493858700499576773418741657487570824179357865241951223155018561684267907712799100922762526706741412523928902105409038951683693424204620570355075936652546398681787931145609090635335092259268023627437543404884939870413071359280803563668076790897925194743799223677433801998275248938099138653/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "28536383328959703993730430075303364190020911254551649423945663982045094704274492977093462377686393175454598424578736919668575596341930388955047068633656361481992620692814813327812876623975978375572536423322145652113828759035405388077251778997084312380853597717028602612494470837499099867849196700594746333193/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-201517388249894989478411032097072751718656423446768498708508564928448662660651229648295542554051448907899318156973678948290345776073447986354173204606393763408869392055271224486081374851034619526102418795206963640221560398265963426462213308991975932816594775660953319668579841424702426262528857537080463794965/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-174513042277315163849266924439208792551210027773319873062117112212107791949617487997311514602133978721591638988373550045126013490861600577744660221983293741489328994487990284644844821816190752936317045684025385986252691736431523152528005392504331486525860129092504396317973074372934850065698391093382548690683/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "20853952201633312877387277508463847055126394746254519899742972932555894208910866792849243688527659586695779456772099102381103863965624564255350878448532450809472846089800434934408081189773222964612807975923115727341248896300480297539550915338524351483735093086771402116129065052573895987568833471894650866121/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-312641081391502269606656250395689464714521237121044730843195101985540858918629890694914712449559446202158312842962672451031785756934401273144496289056535368585556084621907933962326641902682587075123817870096547428328478755021925309233810847720403976729205559662801376490464233034499544774061638742784145893525/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "166672131806845776192896885973661042124973372869940345006468266318743480528703466414015865739675637832291806442497067063319157094307655919219743641987468037062277740025664176448810213542701871758655081692776525610517996057224630655703118199190067622390022656134231632552577778502578893106037108271941930607565/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "-4376967838200489497250994948825473623872235696381225795629850903139948925947408138790254476399212615558494266176816561458243901205759824715627651584088611054101239737165343081922176424447484738906847833188948761892037696110205922052863065492314158621446222809067390965832669530284377833079714832042153910245/5617791046444737211654078721215702292556178059194708039794690036179146118921905097897139916325235500660003558745981042426837180275450519452901482207483566386805246669527046414884444362538940441232908842252656430276192208823201965046059784704400851161354703458893321819998351435577491134526104885300757004288" + ] + ], + "beta": "1/8192", + "factor_bits": 1024, + "working_bits": 768, + "target_bits": 128 + }, + { + "radix": 9, + "embedding": 1, + "roots": [ + [ + "333910482659483459438655528550746003905249000982454975806894848438737707753764976869561366054330641369183833856032301628669487010009234742939505872476695122089942073608783197493524773122513229557328670182714416409970596568787760524274687406159411184511162472265702547672362929076759614595740589264277517789373/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-47752137171466876261593994891268639759720371836251849522631883826242730835462895269072450253303956251409642499713362915697132486294075863280378249136595798406260146271799670133428231669418934780402000503782168565275986637683350570973550359499708480182227099344116449794282936783930506661431843381346792007145/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "180857061429154340683796569249229633634282740219290917942321763794161703285567755908320831766805092839199995120635992701965884419377793868614453316178802274842846369150241658175248894374357637462187419868434067659967756992677108864166432671147587357826434832424046949718532074646758771501650950393504125313/702223880805592151456759840151962786569522257399338504974336254522393264865238137237142489540654437582500444843247630303354647534431314931612685275935445798350655833690880801860555545317367555154113605281582053784524026102900245630757473088050106395169337932361665227499793929447186391815763110662594625536", + "89031252177887495190665762976190738719635134333314194291508015840329805457255816648024444476560108063934040996807695532427466053700897943316995019084184510458211965571902286576252834532496294909472140013944090159918770767649059087712467909540838463240479671623720707864757601071992191516521915069518033316617/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "-77570549831923552874388989142731030044682007042905840083400846000380141528891579777851595702752702328774473303959132662315889278783543232097424451580806347987068043391866782113060657867967927073555566291117612044119958405987268589066112630178066419315079209294063775976558795584459682150886660045413954013769/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "179897435173147029214413437523250288359207247872041518170502120727641382930349650875642891171666569302908673314657961466832174273548337212606432197485311335192890539535613453859826823968059826198019685012450454506061510186429992789952527736462387221084655053453668251388987921959301870000019796834301705370287/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-190010959094347690462269137172070133553459071158786598796602362999138607180514755593009011514443911574926856975116553278070950196565545016104446202259984121956425990468540175254088981798543541253103375431235218242689895049528330746625788021572824829150972581783014458284949616718799691063891716331606263765491/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "99030770506346274571412767249597026710488468973300656614141769044065104917082032751052659130642873032747152401206156730746432904390655127956658220469005080826426402974997601139897941906522466353259384287497934337081931282143875656631456401729850661272991846764776573277336890519241664182121666563815825108741/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-233081207055107292068614793986538528139321828237103534257403268711362307316433680696116996201453280211587720811602707281081949546040375748910078559633641468576989928431965548210945788819468022114946692214502141994372721141673746177085180557226353646152761400166555794272666489885938550232614191513505184437909/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-55943527093538648994131853774327760706423292404958516460832453352530715831038895988364294084379075527404154738093222713072803156085772412806543739693673201174982311509658713101771928709767111169834072902328747368130517026338521314072319621096339894710376582330134409800137590938355592424671582274968784888015/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-73674816051867153651072739874884099639564752966078427342019842615755828513593612394516445502429253037266855084255963456491511864584968452239949356574902784890872662314770973795626380106098390700582613148829779523841278267045301960823172752044249996830463280555136131109752238430106594324223891786255349386507/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "-229807430732849177117110644126555193643659835289545136715286801956254443227030503648670842696618870987609340139528277927495657195520865722750609252335913869508408276603724155327353030563572875987772902902949206596449124196495306939290344827467222870442728695524546121120411264232478377181674795998646854090937/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "21321939274995178538221961206791871382984274797017580984543305003879576871583449027897925288200755917559935688963418115740792809342472296149539253956569356996997885510566587640382490543578910073936695660519193238722044786613345993169911490333550849222184308269478701581148338439803843307487853418615205531513/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304", + "-150737439183938417466026541943664853780573301677390200716773762546802420416786746939455291356847900573293657693272612561521417054798588970409780434875913176859075028648525952666660665297532915477471545641607412073362848129142966744244476665807658602486321803579387819475245914693110974696229125922432406831735/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "35114167688248708489705226725520322239757602458420567049561448419515293002391419875052402245031950661384666638645168035176238701372703027255979313802828205032500024750897988872631333460681293263507451895457087663973744113306278768660451880594853026913028478026418649968409550880245338037923086078312777680791/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304", + "27546478297781289342951459913655862154150871859653605939980547557514582388613385010841997426553751173842745619847075795184069081850799605852120546322776304239444231584968459156764651674979961647993059971657017151034383284332304041936961882154160895082836934427447719866692376787959364467530446014008721598863/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304" + ] + ], + "beta": "1/1024", + "factor_bits": 1024, + "working_bits": 768, + "target_bits": 128 + }, + { + "radix": 9, + "embedding": 2, + "roots": [ + [ + "36627579605007658966659778461203634251371697379108157264801251842963340495317878340007270952160418991100126967216105106719737629728806468143838917422932843178173126209184087556635317452073232467886327807084905993395510516160589404741476340166934455525421308327705599519861799297110888754524674156034983913189/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "91213904696706307172757488630720409637634441273504301106383789102894171902182804905443189017899008504696948838212829861096814223539148482614848676923111790231266756795679293509188920363735763072749479237417340538439822705330283204140328446148978965322292213168306231351893475906153300657761895447665575697199/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "84035680545684351602473661021561463081168863906638834415994052385965625479101474846868259017791131826318727391437910192088726625481437554020823348149067175314300228396308280676735847981399985641700401470915484644497581666130585473688371033657369860576189725447930344844832440162634723948823836250202417994515/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "8148013099263468190653788738472861941241579884501632117571698363380494060372231299699288233780855988276576215383902261263316045847213105572379987687627519561818982137927974561918890474195006623065707914273566644830852081228319342987631236139162161704438123829472498354324469835175859687317768243701014103519/11235582092889474423308157442431404585112356118389416079589380072358292237843810195794279832650471001320007117491962084853674360550901038905802964414967132773610493339054092829768888725077880882465817684505312860552384417646403930092119569408801702322709406917786643639996702871154982269052209770601514008576" + ], + [ + "-100078953961497513827019582958503948692313436745489773412119737617020533859319405373115780371895107700252180090915260674831636736234959936041881253145088199481284819872914984423224863245178613426667354296068721645475017118632587754300463918861969486842414948740548757053004934043822785610986714760398365599679/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "3398809930139403861148899090261015484845408816967426658162601582201664636905280230206674173374829015640972007851858863447180055375534479268107072312487849563160091306886763149122921123989532906823269948436995082554330272656634564774170850622113683532802699002449190529818559937755553698477368426140195610501/2808895523222368605827039360607851146278089029597354019897345018089573059460952548948569958162617750330001779372990521213418590137725259726450741103741783193402623334763523207442222181269470220616454421126328215138096104411600982523029892352200425580677351729446660909999175717788745567263052442650378502144" + ], + [ + "-183338193122679443380740560128812455004059475231783258422114826847995734608876245819348478430541727370982727757486771145154226239259518782402684145929956021883455556122678489997638290182053381073341880321623966722662080562479192139016173619844654784754986657599090969957280567175733144107276191731039944767793/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "69544043884892615520046310400849713710736128335193355114162837516266036707296210585162307101033581669414559740283356404136662487557992456157952373635087040782218145130401822170858673477542223017483990259128019803079762888726928377309670948765232529247230492706760919274284002471550667971352710783976141811759/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-286271387236816925280241522879228420963755468856311152978521691079419985629370744590058055558139090150368540678259547716089060942385350516235204508672078069739575899105386310373908278914441421362759756269445058265422389064137253935790453915270461746334070802354549224387950778330302172659661620800950476186749/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-82918958338806825753830833680976263062074588869905593699233198939242160296448906481827055827641905389023514571488788279137339639543608846689251136263565750412573086750041060060195606898601160434500732786154396471493243930049913562346718453598705146259982726005531537274756750753151714066487137785910761431947/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-49807632985904636056327801309165668569949679703177249904015612774568110724009981257491882061879367530463687202275856313301341867893146717453038446249068471976860842053788497157502426856271448101222353866671376525212460060433231010076669364400926876741344107657680474212816727791674300296404422336397687738749/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "-177362022940644076757392587993194089526114195004881930778497281946886928035272836044916000656700084837927346549061559295412976727004631522383668857538236746314783697433474028860696915143971089197553031019918950340000537004506529613569767212474004309695951498140271896557248889203205304701749822638973665710421/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "151726435005196152503621229407512430240201194430624150994328999718615893705101127231153874291153282523199899481986566943279721987880106907314573029521495326835809641098557389722103622116104726637641894632029695112812573695921454951502415653852282073265566820064948245713045069992446951560447509654860385758977/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-384822354883360534431812042911405387725218348666290124845083009057711843252196160570381320302098793490714437674025650657316209395944001060980319931861297115592823638687839794408498221389027544281560445374349368840423996714188312856799321242909238654232390908052313482832343212428064897303568712693638467285975/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "41081431198079572611558466625440658048255168639522243169055624589826066923314664776521434977008446938486253681718692790654307094043265416041383699295454020975360572161215700150415363540172271447445087225207715238810462166560904016969936740545340760747113041037652787910341644753600676564529962945902837220001/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304", + "-4118711747111065465143117971635801376758138406433752164082253287354658505291179385338879623132445718177109921503638931942611426340975801223027948444391682221345950298080184044770827371312364405460096337648485815254515555637274146065727250436766509743948076237782619108756462233723207660043495600271274827343/5617791046444737211654078721215702292556178059194708039794690036179146118921905097897139916325235500660003558745981042426837180275450519452901482207483566386805246669527046414884444362538940441232908842252656430276192208823201965046059784704400851161354703458893321819998351435577491134526104885300757004288" + ] + ], + "beta": "1/128", + "factor_bits": 1024, + "working_bits": 768, + "target_bits": 128 + }, + { + "radix": 11, + "embedding": 1, + "roots": [ + [ + "19987067627228188344629069299179400482723624880399215433823291767545287429199097189201872739530866475858846834340571882225835111913315556842511345498467666815253246841468908666504463346483028254245326381190693095283853100267355904488055841487849491381199845949444150700195520393828374821557134768600767466237/11235582092889474423308157442431404585112356118389416079589380072358292237843810195794279832650471001320007117491962084853674360550901038905802964414967132773610493339054092829768888725077880882465817684505312860552384417646403930092119569408801702322709406917786643639996702871154982269052209770601514008576", + "-16371177452751777825563018362473384628992592467063145384041920070193938502884230358731455517486303546488422975735506625293320144959392098974784869852824091878513232785682339953450977565251051966045793101131935501779170807314388776610230256291440229867741336996952861254445223349520745729923222550176564288491/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "18856846747548568697588208088342677025973301317628666942362894682533954455666322781604686688583386331954228030929273184779113235417601784513933283718249884792714800236464676089878514996628927413059992636963593921322785923317037817194703770654332326501994334024022987493666601426630817081203976984338145763405/22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152", + "92987134558769461110036206867296860043881621638534166853641725913226172224366088756826381486275497978147294133585381794639930001435905110892538226145300666954747499650465654558096450639522609112222032585019033582960779504653453557208357386268301504380446208517791958035784800586179182112037390042935466531117/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-8755627176049049991226664047137245698863739906064153437347452970558147035098726451283760392997679178295614102787623006912674241102405755920868082634752574119386112664741472162925566921061850884242496676415467646079844403140934545444691802820099406918031463518136566579394224020189874248767924449767942783925/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "184869178819451977603611176386928738242876901648101569688171783567941034492292441694469196166591126057251772941746470171157037212752090292935695497021766339398687078438294125034073412980357691297887600434603353395394298477189459158524716423700412207205879422399971470449045719677938588065634394716581191836817/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-54478583300645253822831870111416997505140953588934025523583341251965664154365796078024298205741864555549713807076133144301802106929744713687687990384993502959532496048549753489310281500438525352868503316582822328826656480517864695496618221362284012857411443021555596782792697074220181225526863918268300639411/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "20286205262628437605254043475721537150966571526564811549532640552204714056754728803364947802459551692869353686447919641018139868478560640763273306515452613049046891837083267506195031814938252858003236870013002284111289860505997396859958206617069856782707127987927582577818632717973254483287992421656734652759/22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152" + ], + [ + "-95898183509014184241500254592800463383859036505354131097291586846162888704186664657955359052988941231121132518651068021267889402827792190056019212109768207300155797496969688201128119018149578616452527735438289364195597833846776297049494445152908588057194749724385825905412784224692093180207921450384112242461/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "42778814428655042090098870059327487099864258445354926673871694836725119840952203199861360259612720795076463940032853087688047118369165810858094712277252996243488507752097503657331562950399220905133886815882248888535031166708361760343306732503522179656046809130881476963896662304795263022774723587080694995587/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "-225921504279610020642388278131970798218208536978767361355204927337288732255627291982651523854880824990070444198973400989148467743303745890374317986738214990201636073279077380395278347044974050305694703888747355737926977743906487115905900433985192373300492134362778507994126188996113276482333293522946874166163/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-18512006630388580492498585919316792146843256940712140321718354870283077911759945301636725256521424427374811915420777847665766697831971631267719642616122994338671795328699256187096082707061323572720759145517912510241431847044219321767359552211168619158510793131072148281713269420146872738380344999839805482673/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "-180384503040408332969274788910647993002194348933408627006352614755504198801432827860872973900664892565262188160970148757056307523990146812970216425530483920281444046886004414828488834832305952363622670602928505922661923912562146105294903808098488454307366830380059864074416998974794846587590490652864169574297/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-176646969751708359448147936704547232946199217170499539675033536510376224673878639512761397186205834591084970427821916955369563206972314869103885725048066220048023304706002429705664922747797907812155061260294680552052160516977538525542207321666484952876348281560646346378263539923187144743564731897674171100239/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-38861837212388384976420529976991509417115833041275628837436068047549600060280382176786322036369939502791851622004559175908329336385610877310085063200757697917251570206071466998822689139170709736990644246151849501271239337143095479406182219416332143451639476774213058321348321744184322700650862375330310963823/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-277565260286031004677878130054188583191705289863934684844268782639173497999273973903587616669187872134632967542328894598608374892255412381085758974558621898023147837402060395658900058771526410416451986547731710938161234642213649079303903522523174051553608817790842230009020182395206171132818408527279761433361/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "21488211622826500960553162925976956012202845211007392491489641798267308432671711630040098232679466316650764179735598419427366676486749904192558644332299235921421144714023516384651586190355271133895433014816047193327744219762731373547159612179053454955452144677625900088969121688703953521421817439565637653255/22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152", + "-128511894661549286531404877158872813325425204854650114042374504318410629316789283103583139449251533177702910299315398368686906037165442415057629373076402635077289348627984153358667785498500978795932314288919594386024513282286275663286707605543358820950021120445081138909212973329449308021598533550888061275955/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "83585712907819930372525737678387002726043373066088394654745598301106562580077687197093984735045193590830082209556833412016347775904780083057550263000319559749883171904511683435215084292917686994094634613938974636571702338378693688527807890580242888639214849494751714712417179164070115873698326690655414974855/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "39527043648482950010229499119972439999724135181397298119791477377378696955872414923351111484626654042810194997537223158576386497412597956774521165982556008744194574609655834444282255397016231889321227196472166056329130778270908426382465705876154201534793629442915901015100724328325125021229484333621969864103/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304" + ] + ], + "beta": "1/1024", + "factor_bits": 1024, + "working_bits": 768, + "target_bits": 128 + }, + { + "radix": 13, + "embedding": 1, + "roots": [ + [ + "18692326237161478268382893815511145026088685648190526628486457135249558896952920917514467617130261745382206732573150104474804362843637309165023312885970700945843085407379411136466208630482730176116475442280579227987505293153616103902239142645063037996256214288997875546400775697052054140996875722199535144377/11235582092889474423308157442431404585112356118389416079589380072358292237843810195794279832650471001320007117491962084853674360550901038905802964414967132773610493339054092829768888725077880882465817684505312860552384417646403930092119569408801702322709406917786643639996702871154982269052209770601514008576", + "6486859248533430000780273205701654512173970909417755732036832012643583151844496919483104176207017793400666110165169957902541959012070998111285223760348081928328199544477282093388192150307015875863662558373792923793254558604148460967249276341192795957495960108311024542088237938103987924150576546911604521261/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "157323348664187956666822829330189664661635426810358914253796127992247865612061106690649235990527526045899298682970108967127473022845446753514004123946631683036181536536551113663594714055940804627834938973774495105472785669307840365432825878956659739101252967010629991460289857031165177301889783427611928177035/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "40452681226070075570072472344401074944712003983589808887925600577667159697646220867905051803615621855045591166578947446549771630680539405755136473452812017494827925564012739248547906421181216869880258586492201563801160785331284811700400735399327336162196251093715630564873576011674857714278044254516933544179/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "34899392812722428966123339680611544816703491872217428378010116691058846226498126253227436478273425414652638211700583485046158136663268894227982165278243907434398134769506468269248093633129553630375056939180388351514797408409815225914896580843925098996214002147635347069013543757886234918338529369491958625833/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "88011579740709610420551536777095471880520733731329804909182057295159138856658844441946791253952523971367978325361906101288855444899057938251340285018035035161867960959529967697490808156919827046584265520088861647898766523277648589169329276572810161414081405603460615665641982272371797657744614418548585824559/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "-23632344362636047103245294315793142313888805211632242345277872394180256512662942947584023084035033218243173110811282908595282258284332226870800162079433188907613058231842037992245668397834548268318570993706111537983389312729510092584842380438077530588177371098312347383358971591168761951695032633273140864129/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "179549417839364571074172991064461500088264697781045040638237379539937742850790852186678832881823049512825498163936194969819369072795634141188946475578546985346143228307209114122988494462198458310511930360221307110264021454197646686772971727200632632260525068224424641531327341793787119527322865955849707710265/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-64171504828073803152954152937711567711542666684035601356646712378688470076580612870475769092135067000533842853688036144897397023533079657883641351971704778429165978068814538057468601770310658772323207554597087096804145799486637998411913965567996425496787598923735682562388421874636442133233905377559485353157/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "73251115769149306473345828646266294966486765451643471177403942814435204983959223865491318323457407052192740413543012493039306909122000661827522200300183854470520931139463523567192277441532807875169028627798601616463280909274217382738236473252288608372738895951142823317852525506369814133883275719630758807137/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "-96104599738951769633676493389601285253005282559510584694569816846333257502863917660923538247139087495252208921646849092614916922614604316843162321832456288793741483649147875280476706456286703917113215728033231503625203893643516836727765185675495923663427569333306934484123850806643288701454825729811953604323/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "9516631030430603547304258413179041787814767345466107116984577378638068226215235344637777767447480019230821635109605408066669055840851972438579815757178810228708736258218847736218387748283693992362423328654952423382366630325601232318115927373324378897688359132242894713899973429384583590542101150580140274839/22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152" + ], + [ + "-55062228354540215497376005863565840475664320925484203015301893653352734911931366500499734179862501376983233255651835114951841126300871292416409994938947913247339808265695383764522624850188675657931604747407328681915351414694957246542297547449812418192888195444651234827845753423977115916824720713929628153581/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304", + "-12496569895905601754496446211252110954226257293968968523070001442676531897713204634587293165700868423273240811744498014947415054071256992206134858336956107724864774886993506222731936628197452918495709094251331874681454069575341628004137867852588704373449128871488326320348282721855230926986775081427488534319/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "-97236621922926488171753094952475321839966850867104708437058094218576032195216305246450562921641655245078955900922369570464505990156267416121818652856643194067118861143473065056879134133679172250527578434553971705148706518072819842042031704168804575722945478691295867602666460085505768296696878111825723393123/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "-139974366379725222238941562299015165007954582856054307766040303104694071987798318784342412584103837521837750166553176969910384907399840762917340723142586181202439284159762153726030716323608885065258852362112003980666178559063919724073261539914546317386542228981943211320210328234291676368809663605528890583427/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-12916153817227395308964320333307521693172637922378933961237847141531974139138197199274579477201858620610500507563920459598428400153777012639967564196276145126945301605944903521853118392469464413956941118844472993633600262566258024731392397410303362620852019080248276163503519613363724636522615542062596291175/22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152", + "-238994272365838385358698151204558291126185120423482408759980968611149377358699437412307564621248256757262516810026759206258728546995344843798934973819120821031754741483239472065190876326354096946934497360840975069467809446930323282385605750700824263085431792466905140472727845592124191127039452483105619360915/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "6013043937133886929785992231257511969627667249481246735439580322562221982328578577554836403334984733439034934735034117774148354364364987263562214790340175882986670622045334794157783337444852881404655139096629253059946504379613666594193738691315078072319789952637941430021364779329441507323583528933381210005/22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152", + "-278679923529189704360039255534940158059487346553817563199472560610069982490137529352759281333079523373930862003820159709004193000121849875645389874369158065539387537232566451095140876980715405549825629533527920059018461562814145916859044343901996440993708624557401126980979858868823094800991662382134844602877/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "109989007535808651476018626898092526943022773744744817418914845584436965704556653332778848051969834606627072091810750458326495050646220897112757542708660487042684367750689381549049479775617896373974012758542109149431726669145658671611746929890662655791701705849605871346529807065359253700271713756945440448383/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "-51882011778821188484364240793453110774348786484062001914177257798483135937985388930919631365603190565770832669699636056548063889192925119116887789197614808884804148831874399739412809224443826013793004508047851389354227654919416055982643722487389332768423157423587133671627261738239235292352438537394793285609/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304" + ], + [ + "105894466188666824637797522379481298816044382741836996193011641682857452110816736028928950018833122381771371198703803457128745525851017334778410249826879397875759195534689495859965994904874626346162905042038177007336006951294064455526202243127641508935278616124494878183999313811884724475030368145374684989523/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "70513352389598145213663477133635023707890899921823566159207226270576916995395924683079445594271942693838367850660040457845959093720558038483352469338574636265642119180155548293660979873985809604194360555360145016038237726142654627699688283243073137486408739406691752226458425337231524766414622661143826464579/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ] + ], + "beta": "1/4096", + "factor_bits": 1024, + "working_bits": 768, + "target_bits": 128 + }, + { + "radix": 16, + "embedding": 1, + "roots": [ + [ + "134039650432496433101295605159145494804947147618859989214825957778126813783946265379824234530653079795983300535220081531974499830210731306488624875267801121995052729438299927149721093666927526785655754801147235486784301827065913383198135946696241002975265831017168785200446019385215181318777012203053206775435/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "10043776175087489111857420427705466089122018604250422834704851221257606484042652956267827527042103582138401817998484317090147751084140645935922861891946502301969712627060390112286498548692413675638854082746767615556998261778873625372575511704320589333963130560858950109780981665146820923938000446283595843981/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304" + ], + [ + "163698198267763187271175317732354162942142798991132287897605537834861074139898973926663170112137318749861087075458509497866923709014367775583409379820255381037822285641799332965596998682187512678394888610812074850883841645394925104103931217581714852536893012837648469034763538149987146660169793180318525683963/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "34154907814115855601778002615718880203068084565931904547779687937911408288344869439590995495717368706638636414617448243280929199776252293685154663952500722290615662112290390816093868694604275838431637064859423302174318393837094657848778434379080583038727143019868879816065247203874832557642095346180510541817/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "125972697409629971610668644095806954773026269483836139794069300342348858033512225247311677027781101220433900638850299785029618718841248714192496025858197851778421685409754264599923508300047622246726630559684778235132368096407527643305232066166954976575730325609055979040383084148029612053926198944646591312277/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "15167790659874947924589060300057100404989113576637779018845337397852208471948163165837442910874732484685189549202575299032263922362242746686661085009319025178790114153139930066286476936454793858408781296809315075998603335912470151363640101092646280120351957483245267415973808462131927199015047640649421685169/22471164185778948846616314884862809170224712236778832159178760144716584475687620391588559665300942002640014234983924169707348721101802077811605928829934265547220986678108185659537777450155761764931635369010625721104768835292807860184239138817603404645418813835573287279993405742309964538104419541203028017152" + ], + [ + "13853536865015261579911150032049872304272006558508656999350196565098776518334784731805531655741656799427586114638867558728051351302042284720128353136488689847220369858233808059733505486343038607449224336533854935610047845464572670709769013819513710914519750342782309697087053886069773135656466958608061541769/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "177545851147179895490196191648273709559870852473948635168982933050035672511543664292889660396400875012049726711091359491491643948309945736293014186853449971590825791166882789030071391843162221062181697202769315484013800917514554939433749527198631298084673567294376435632058165815416832640235572073617726120941/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-52210378056113995222526794456200026551550434350267615704607002484161409961625123864247636241912256583356359184500954597575895892110205892926433892520877857803012652172002684435938465544783335544671181399418477865628149454975798200306362483024809010252305140774988065045567446320437361416053738363358747644443/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "87648308710707093471187039917458706451472578491021738770540393300719242093206053400276097328660396266053722682800563211432811793974391639650142917556304518681178604701687327846402527191048522814812999729648713916842250073122954579935163661634587626288322854319550536493507991774193503157659239580292987842157/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608" + ], + [ + "-116664073824034912718051835779935450320038013857443941308097484208019490686854521720422334021093095268154662714097019061138743852755115144088228123078315232346900394049166264273018455963049040513237001187564736700035245183063339192035351382225907798789582613795974065118752512750692942562782534375193614661861/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "149449269678260753521945326074791968079519019469792743136375292271466248404832296872514640066703937306939051683043529915596390678603913779661604066173180108039752595884583226240160259044735240089986116711339120429442816430176353855415258845446067522565220002881930958366647672375789662340506634532555558066251/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-85610957404387028634243322426648242688663257839375635069698465559559419377521551982033761821736612609921595358004172251326835155119996617686944093557730406618580170261786725657706867217353963671009491290423195732204000640025294244393939752267572032643929785491689258684316664163295188812404572449637311320451/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "99615833663101054301816080147826293655285718447019552564330413357835145945778960092597289825973787281964918942430276502793281215764935713502351704443126657759517272838966727793208748184206115834330960302736430555573552466912693730743584134891685941797179902285300308856534717258649051539716231977831990434935/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-206470925126790414958903095327931072696188278347167769164325237872418927430185815104414777620540205015448274164195641352218542457975169039791010753378777708716944076446597350330115681723054142766603880278838717720575430103778172708862328494065918713903827091679242299103863352097855468435963485647011288487845/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "28326730094049526360308020645864856724598891128838513609367588904514833835204347361667185978800994436970191543152173345365891935121884286237303162650500563575271973969509154285033455092089962932786873166080400502570268738193931444116625301385853996639117280974700258567439169279262226550039720244993440086577/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-212793201622109962448330100692808593439645159644577548679667883054110536914612983822159045347472254754395342771708966598767283083523909873556284381276124835470115664134649247694090104295004718385271153849431718533152316853933967919972046963990390480364949318130626453951329110678301062337081449200475601735875/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-57964249005932469131896837719919287256295100537523457777437606447238450243954529094264672294496860934864424519386491456408615251057823684209861120741434670159618673936343232127524840096572869938406481577342691505214852241781904532730223280532007263456890157126325151281429988053858853115810915974956182248013/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-181906514405143036384357434995971625275836390798303598349017616251000415282024441569357952686816616444878672327665448828051994214624348737805868406889846662816154885625310561267277397135353478192043756460106331313083421328902239020972755544322708347048855909898995764083966273823919667161396109476550719848725/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-147945663340461763698212430143771286414026284146309945071685010721085537380641268203814890803383015075422455405339014135542776026293391412163500686456905034790428849048670266153134094858649998069511486106390629359568273414843847740088984032890568291491121209596476991217967574780912075401622245788540973317237/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "-109295650712632922954470152700014140962344687784228817505917409852933900860213282982253187319663670767937851495649957296830456277490544817826798947725684889752695688092754004821393186285277520453649669774004548684876352062161227459330029625465970767406457202300678613241928430071212855440266575276167464763807/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "-56200741848002868079111868432724886507129621548125121648642474266599250489673841691778046881437449293933434722648357280706913445930283045991236908716738562916199191451345481529063774448710946467551285759609323141571550416355308596877200595274065373565280076263027603986562578831336689401091825392816459762247/44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304" + ], + [ + "15968822176892792285891476438139425317687583108455281192008770761103687215213981897594608046751009662616135817210933151016991807601573680585709456982599855455736137633949541869722566316681492518193528500018722529515726386747292338115274696063766393314538517893691137581991598848479112650484943606294759671/1404447761611184302913519680303925573139044514798677009948672509044786529730476274474284979081308875165000889686495260606709295068862629863225370551870891596701311667381761603721111090634735110308227210563164107569048052205800491261514946176100212790338675864723330454999587858894372783631526221325189251072", + "-266324790638046954468748086815326096854011998014910958879637384810491281671701735342579622902906841022217262017537242815542832447116697353634706329017518582629343845840130883918382746688279956080610789278337184153491906948023245930590272626869013417164765399270940382908317755754807962553226947387458433481969/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "1060865642031292630770255648031651464303955219241748845301061404301449150107131123877033982501236564870546734157170738071205142825981730629211934466958373310795930234883644313113012070731987912222503770737372313560840648279391481374684780737322726034313967342539259478356716096981485614792922808816297076935/1404447761611184302913519680303925573139044514798677009948672509044786529730476274474284979081308875165000889686495260606709295068862629863225370551870891596701311667381761603721111090634735110308227210563164107569048052205800491261514946176100212790338675864723330454999587858894372783631526221325189251072", + "-246799233700152837800565619104070457222176842192478672102595825359550055541867252492449227477274629665694532828700249246838030620913792598556947021011742874894999694125075108903854687975235844168506798118891370394456073402356817011957930168970746212902758217822556747842079095849448037149783703853881509351465/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "74864797941206513281047175374406371423373655545874336711328481273747977974984455616940936075339467433634151221026156653070150698647294564580345247390350645817572015177013890581338145235391049860293804890641833349803840457797326162410138640935908664989180260619163393823243511563841284652103776498758852275761/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216", + "158507016237416030279508951176317259509379692049347194102510424353036380843727700204504205980624447511489013333078714007658126019484831026660454241743943509290714726174111157436372813963025263036212831092360360315950519574485871493725846468575071813444421951074798721371147434849601216160281721594412331444679/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ], + [ + "126287595802823388378145790573347116516250877023657551588569070335106577368621778092749228800089231992059072999369812292461321688715048725080489109408634374024142218044000898630952519239661477382516567361587110636505950019813691734756152201601098996057298499115007197346303456331071237494888612444968034206643/89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678164812112068608", + "-143526397691224128056251209454968080411106577138808675995376721394908697117978740021220231248704896684803444156609685788793425078524968774144075750535259582404256698559171991950020896681595928832179228331976729295065837037698098662420392076528307364731612360503267270299597486337931330781272500922478650324859/179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216" + ] + ], + "beta": "1/512", + "factor_bits": 1024, + "working_bits": 768, + "target_bits": 128 + } +] diff --git a/research/cyclic-stride-effective-depth/vendor/pr846/vendor/PR628-NOTICE.md b/research/cyclic-stride-effective-depth/vendor/pr846/vendor/PR628-NOTICE.md new file mode 100644 index 0000000000..22fbeb8ef0 --- /dev/null +++ b/research/cyclic-stride-effective-depth/vendor/pr846/vendor/PR628-NOTICE.md @@ -0,0 +1,24 @@ +# Attribution and scope + +Ali Romman's PR621, exact head 520774462b19b29af41554b74def31f9d01e997e, +supplies the prime-power kernel circle bound. Its kernel attribution is +OpenAI's exact-DFT preprint at adc7f1241b42e322a6451854ab7e4b4c146bf78a +(`loc:newton`, `loc:fourier-factorization`) and classical q-Pochhammer/Newton +factorization, including Alexey Kuznetsov's cited q-calculus work. This +package does not claim to originate those constructions. + +Pan's approximate-factorization theorem is used in the form stated by +Mehlhorn, Sagraloff and Wang; Brent's work supplies fast elementary-function +evaluation. Causal/anticausal recursive filtering is standard, as illustrated +by the Briand-Davy source listed in SOURCE.json. Sources are cited for these +specific tools, not as proofs of this package's complete claim. + +The scan rounding analysis, explicit budget composition, interval and +factor certificates, routed reference execution, and packaging were +prepared with substantial OpenAI Codex assistance for chafreaky. The dense +matrix solver and algebraic coefficient crosschecks provide independent +computational paths, not human peer review or formal Lean verification. + +No new multiplication exponent, literature priority, maintainer acceptance, +physical tape execution, or production performance result is claimed. +The code and documents use the repository's Apache-2.0 license. diff --git a/research/cyclic-stride-effective-depth/vendor/pr846/vendor/check.py b/research/cyclic-stride-effective-depth/vendor/pr846/vendor/check.py new file mode 100644 index 0000000000..5ef6dd67b6 --- /dev/null +++ b/research/cyclic-stride-effective-depth/vendor/pr846/vendor/check.py @@ -0,0 +1,178 @@ +"""Rational proof of mixed inside/outside cyclic factor inversion.""" +from pathlib import Path +from fractions import Fraction as F +import argparse,importlib.util,json,math,sys +sys.set_int_max_str_digits(100000) +P=Path(__file__).resolve().parent +def module(name): + s=importlib.util.spec_from_file_location(name,P/(name+'.py'));m=importlib.util.module_from_spec(s);s.loader.exec_module(m);return m +c=module('scan');ik=module('interval_kernel') + +def prime_power(r): + if type(r)!=int or r<3:return False + p=next((d for d in range(2,math.isqrt(r)+1) if r%d==0),r) + while r%p==0:r//=p + return r==1 + +def certify(data): + r,k=data['radix'],data['embedding'] + c.need(prime_power(r) and type(k)==int and 00 and type(target)==int and target>0,'precision budget') + c.need(type(fb)==int and 0=F(1,2),'gauge chart') + parameters=[im/(1+re) for im in v[1] for re in v[0]] + mid=(min(parameters)+max(parameters))/2 + t=c.rounded((mid,F(0)),1024)[0] + sigma=c.mul(center,((1-t*t)/(1+t*t),2*t/(1+t*t))) + c.need(c.norm2(sigma)==1,'exact rational unit phase') + error=sum(max(abs(endpoint-coordinate) for endpoint in iv) for iv,coordinate in zip(box,sigma)) + c.need(error0) + for name in ('unit_root','missing_root','wrong_embedding','low_precision','bad_margin'): + row=json.loads(json.dumps(mixed)) + if name=='unit_root':row['roots'][0]=['1','0'] + if name=='missing_root':row['roots'].pop() + if name=='wrong_embedding':row['embedding']=row['radix'] + if name=='low_precision':row['working_bits']=8 + if name=='bad_margin':row['beta']='1' + try:certify(row) + except ValueError as error:controls.append(dict(name=name,rejected=str(error))) + else:raise ValueError('bad control accepted '+name) + state=certify(mixed);x=[c.ONE,c.ZERO,(F(1,2),F(1,4))] + bad=apply(x,state,1,omit_inner_shift=True) + try:residual_check(x,bad,state,1) + except ValueError as error:controls.append(dict(name='omitted_inner_shift',rejected=str(error))) + else:raise ValueError('inner-shift mutation accepted') + try:apply(x,state,1,(F(1),F(1))) + except ValueError as error:controls.append(dict(name='nonunit_gauge',rejected=str(error))) + else:raise ValueError('nonunit gauge accepted') + args.out.write_text(json.dumps(dict(status='passed',kernel_crosschecks=crosschecks,irrational_gauge=gauge_record,certificates=certificates,cases=cases,controls=controls),indent=2)+'\n') + print(json.dumps(dict(status='passed',certificates=len(certificates),cases=len(cases),dense_cases=sum(row['dense_comparison'] for row in cases),controls=len(controls)))) + +if __name__=='__main__':main() diff --git a/research/cyclic-stride-effective-depth/vendor/pr846/vendor/interval_kernel.py b/research/cyclic-stride-effective-depth/vendor/pr846/vendor/interval_kernel.py new file mode 100644 index 0000000000..1182175a55 --- /dev/null +++ b/research/cyclic-stride-effective-depth/vendor/pr846/vendor/interval_kernel.py @@ -0,0 +1,61 @@ +"""Outward-rounded rational enclosures for prime-power cyclic kernels.""" +from fractions import Fraction as F +import math +from functools import lru_cache + +BITS=1536 +SCALE=1<4:raise ValueError('angle bound') + itheta=(point(0),theta) + total=term=ONE + # Taylor remainder for complex exp: <=exp(4)*4^(N+1)/(N+1)! <128*... + n=0 + while True: + n+=1;term=cmul(term,itheta);term=(scale(term[0],F(1,n)),scale(term[1],F(1,n)));total=cadd(total,term) + remainder=F(128*4**(n+1),math.factorial(n+1)) + if remainder 0, 'empty cycle') + need(direction in (-1, 1), 'invalid direction') + need(0 < beta <= 1, 'invalid margin') + need(norm2(b) <= (1-beta)**2, 'uncertified stable factor') + u = F(1, 1 << bits) + need(u <= beta*beta/2, 'precision too low for closure') + order = list(range(len(x))) if direction == 1 else list(reversed(range(len(x)))) + z, power = ZERO, ONE + for i in order: + z = rounded(add(x[i], mul(b, z)), bits) + power = rounded(mul(b, power), bits) + den = sub(ONE, power) + need(norm2(den) >= (beta/2)**2, 'closure lower bound failed') + seed = rounded(div(z, den), bits) + y, previous = [ZERO]*len(x), seed + for i in order: + previous = rounded(add(x[i], mul(b, previous)), bits) + y[i] = previous + return y + +def dense_solve(x, b, direction): + """Independent exact Gaussian elimination on the cyclic matrix.""" + n = len(x) + a = [[ZERO for _ in range(n)] + [x[i]] for i in range(n)] + for i in range(n): + a[i][i] = add(a[i][i], ONE) + j = (i-direction) % n + a[i][j] = sub(a[i][j], b) + for k in range(n): + pivot = next(i for i in range(k, n) if a[i][k] != ZERO) + a[k], a[pivot] = a[pivot], a[k] + p = a[k][k] + a[k] = [div(v, p) for v in a[k]] + for i in range(n): + if i == k: continue + p = a[i][k] + a[i] = [sub(v, mul(p, w)) for v, w in zip(a[i], a[k])] + return [row[-1] for row in a] + +def residual_bound(x, y, b, beta, direction, bound): + # Neumann inverse norm <= 1/beta converts residual to forward error. + for i in range(len(x)): + residual = sub(sub(y[i], mul(b, y[(i-direction) % len(x)])), x[i]) + need(norm2(residual) <= (beta*bound)**2, 'residual error bound failed') + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--out', type=Path, required=True) + args = parser.parse_args() + cases = [] + for beta in (F(1, 2), F(1, 16), F(1, 4096)): + for unit in (ONE, (F(-1), F(0)), (F(3, 5), F(4, 5))): + b = mul((1-beta, F(0)), unit) + for n in (1, 2, 3, 8, 17, 64): + x = [(F((i*7)%13-6, 8), F((i*11)%17-8, 16)) for i in range(n)] + B = max(abs(v[0])+abs(v[1]) for v in x) + for direction in (-1, 1): + bits = 64 + bound = 6*(B+1)*F(1, 1 << bits)/beta**3 + y = scan(x, b, beta, bits, direction) + residual_bound(x, y, b, beta, direction, bound) + if n <= 8: + exact = dense_solve(x, b, direction) + need(all(norm2(sub(v,w)) <= bound**2 for v,w in zip(y,exact)), 'dense comparison failed') + cases.append(dict(beta=str(beta), b=[str(v) for v in b], length=n, + direction=direction, bits=bits, forward_error_bound=str(bound), + dense_crosscheck=n<=8, residual_check=True)) + controls = [] + for name, x, b, beta, bits, direction in ( + ('unstable', [ONE], ONE, F(1,2), 64, 1), + ('underprecision', [ONE], (F(15,16),F(0)), F(1,16), 3, 1), + ('empty', [], ZERO, F(1,2), 64, 1), + ('bad_direction', [ONE], ZERO, F(1,2), 64, 0), + ): + try: scan(x,b,beta,bits,direction) + except ValueError as error: controls.append(dict(name=name,rejected=str(error))) + else: raise ValueError('negative control accepted: '+name) + x = [ONE, ZERO, ONE] + b, beta = (F(1,2),F(0)), F(1,2) + y = scan(x,b,beta,64,1) + y[0] = add(y[0],ONE) + try: residual_bound(x,y,b,beta,1,F(1,1<<40)) + except ValueError as error: controls.append(dict(name='corrupt_output',rejected=str(error))) + else: raise ValueError('corrupt output accepted') + args.out.write_text(json.dumps(dict(status='passed',cases=cases,controls=controls),indent=2)+'\n') + print(json.dumps(dict(status='passed',cases=len(cases),dense_cases=sum(c['dense_crosscheck'] for c in cases),controls=len(controls)))) + +if __name__ == '__main__': main() diff --git a/research/cyclic-stride-effective-depth/vendor/pr846/verify.py b/research/cyclic-stride-effective-depth/vendor/pr846/verify.py new file mode 100644 index 0000000000..0cc3867b79 --- /dev/null +++ b/research/cyclic-stride-effective-depth/vendor/pr846/verify.py @@ -0,0 +1,234 @@ +"""Replay for the stride bridge. Standard library only. + + python3 -B research/cyclic-inverse-stride-bridge/verify.py --check + python3 -B research/cyclic-inverse-stride-bridge/verify.py --write # regenerate EXPECTED.json +""" +from fractions import Fraction as F +from pathlib import Path +import argparse +import hashlib +import importlib.util +import json +import math +import sys + +sys.set_int_max_str_digits(100000) +HERE = Path(__file__).resolve().parent + + +def load(path, name): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +st = load(HERE / 'stride.py', 'bridge_stride') +need = st.need + + +def pinned_vendor(): + source = json.loads((HERE / 'SOURCE.json').read_text()) + for name, digest in source['vendored_sha256'].items(): + need(hashlib.sha256((HERE / 'vendor' / name).read_bytes()).hexdigest() == digest, + 'vendored source drift: ' + name) + # check.py loads scan.py and interval_kernel.py from its own directory. + return load(HERE / 'vendor' / 'check.py', 'pr628_check') + + +def unit(t): + t = F(t) + return ((1 - t * t) / (1 + t * t), 2 * t / (1 + t * t)) + + +def coefficients(L, beta, seed): + out = [] + for i in range(L): + scale = (F(1), F(1, 2), F(0), F(1))[(i * 7 + seed) % 4] + out.append(tuple((1 - beta) * scale * v for v in unit(F((i * 5 + seed) % 13 - 6, 5)))) + return out + + +def inputs(L, seed): + return [(F((5 * i + seed) % 9 - 4, 8), F((7 * i + 3 * seed) % 11 - 5, 16)) for i in range(L)] + + +def generic(): + cases = 0 + worst = F(0) + for g in (2, 3, 5): + beta = F(1, 1 << g) + for bits in (g + 6, 2 * g + 9): + for L in range(1, 19): + for w in range(-L, L): + K = st.levels(L, w) + need(st.admitted(beta, bits, K), 'admission') + b, x = coefficients(L, beta, L + w), inputs(L, L * w) + trace = [] + y = st.solve(x, b, w, bits, st.Tape(), trace) + for row in trace: # margin is preserved at every level + need(all(st.norm2(c) <= (1 - beta) ** 2 for c in row['b']), 'level margin') + need(2 * row['stride'] <= row['length'], 'stride halving') + exact = st.exact_cycle_solve(x, b, w) + bound = st.solve_error_bound(F(1), beta, bits, K) + for v, e in zip(y, exact): + err2 = st.norm2(st.sub(v, e)) + need(err2 <= bound ** 2, 'generic error bound L=%d w=%d' % (L, w)) + worst = max(worst, err2 / bound ** 2) + cases += 1 + return dict(cases=cases, max_error_to_bound_squared=float(worst)) + + +def traffic(): + rows = [] + worst = 0 + for L in (1, 2, 3, 7, 64, 1000, 4096, 65536, 99991, 131072): + phi = int(L * 0.6180339887) or 1 + for w in sorted({0, 1, 2, 3, L // 2, L // 2 + 1, L - 1, phi, (L // 3) or 1, 97 % L}): + tape = st.Tape() + st.solve([None] * L, [None] * L, w, None, tape) + K = st.levels(L, w) + need(K <= max(1, L).bit_length(), 'depth bound') + need(sum(n for n, _ in tape.levels) <= 2 * L, 'geometric level sizes') + ratio = F(tape.records, L) + need(ratio <= 40, 'linear traffic L=%d w=%d' % (L, w)) + worst = max(worst, ratio) + sort_route = 4 * L * max(1, math.ceil(math.log2(L))) if L > 1 else 0 + rows.append(dict(length=L, stride=w, levels=K, records=tape.records, + records_per_entry=float(ratio), pr628_sort_route_records=sort_route)) + return dict(max_records_per_entry=float(worst), rows=rows) + + +def apply_kernel(c, state, x, w, tau, bits, tape, mutate=None): + r = state['radix'] + L = len(x) + y = [(v[0] * r, v[1] * r) for v in x] + taubar = (tau[0], -tau[1]) + for inside, b in state['factors']: + if inside: # (U-rho)^-1 = (I - rho U^-1)^-1 U^-1, U = tau Z^w + shift = w if mutate != 'wrong_inner_shift' else -w + v = [y[(i + shift) % L] for i in range(L)] + y = st.solve(v, [st.mul(b, taubar)] * L, -w, bits, tape) + y = [st.rounded(st.mul(taubar, t), bits) for t in y] + else: # (U-rho)^-1 = -rho^-1 (I - rho^-1 U)^-1, here b = 1/rho + y = st.solve(y, [st.mul(b, tau)] * L, w, bits, tape) + y = [st.rounded(st.mul((-b[0], -b[1]), t), bits) for t in y] + return y + + +def cascade_bound(state, L, w): + """Execution budget for the factor cascade, Theorem 2 of PROOF.md.""" + beta, bits, r = state['beta'], state['bits'], state['radix'] + K = max(st.levels(L, w), st.levels(L, -w)) + need(st.admitted(beta, bits, K), 'cascade admission') + u = F(1, 1 << bits) + error, norm = F(0), F(r) + for _ in state['factors']: + # one solve plus one rounded scalar multiplication of modulus <= 1 + error = error / beta + st.solve_error_bound(norm + error, beta, bits, K) + u + norm /= beta + return error + + +def kernels(c): + data = json.loads((HERE / 'vendor' / 'FACTORS.json').read_text()) + rows = [] + for row in data: + state = c.certify(row) + perturbation = F(state['certificate']['factorization_inverse_error_bound']) + for tau_name, tau in (('1', st.ONE), ('3/5+4i/5', (F(3, 5), F(4, 5)))): + for L in (1, 2, 3, 5, 8): + strides = range(L) if L <= 5 else (1, 3, 5, 7) + for w in strides: + x = inputs(L, w + L) + tape = st.Tape() + y = apply_kernel(c, state, x, w, tau, state['bits'], tape) + bound = cascade_bound(state, L, w) + need(bound + perturbation <= F(1, 1 << row['target_bits']), 'target budget') + q = c.phased_polynomial(state['q'], tau) + dense = L <= 2 or (L == 3 and row['radix'] <= 9 and tau_name == '1') + if dense: # independent exact Gauss-Jordan solve of Q(tau Z^w) + exact = c.matrix_solve(x, q, w) + need(all(st.norm2(st.sub(v, e)) <= bound ** 2 for v, e in zip(y, exact)), + 'dense kernel comparison r=%d L=%d w=%d' % (row['radix'], L, w)) + # expanded residual: ||Q(U)y - x|| <= ||Q||_1 * execution bound + scale = sum(abs(v[0]) + abs(v[1]) for v in q) * bound + for i in range(L): + total = st.ZERO + for j, v in enumerate(q): + total = st.add(total, st.mul(v, y[(i - w * j) % L])) + need(st.norm2(st.sub(total, x[i])) <= scale ** 2, 'kernel residual') + rows.append(dict(radix=row['radix'], embedding=row['embedding'], gauge=tau_name, + length=L, stride=w, dense=dense, + execution_bound_log2=round(math.log2(bound), 3), + total_bound_log2=round(math.log2(bound + perturbation), 3), + target_bits=row['target_bits'])) + return rows + + +def controls(c): + out = [] + # 1. Reseeding with the wrong closure rotation must break the solution. + L, w, beta, bits = 7, 3, F(1, 4), 16 + b, x = coefficients(L, beta, 1), inputs(L, 2) + good = st.solve(x, b, w, bits, st.Tape()) + original = st.Fifo.__init__ + + def rotated(self, tape, initial): + initial = list(initial) + original(self, tape, initial[1:] + initial[:1]) + st.Fifo.__init__ = rotated + try: + bad = st.solve(x, b, w, bits, st.Tape()) + finally: + st.Fifo.__init__ = original + exact = st.exact_cycle_solve(x, b, w) + bound = st.solve_error_bound(F(1), beta, bits, st.levels(L, w)) + need(all(st.norm2(st.sub(v, e)) <= bound ** 2 for v, e in zip(good, exact)), 'control baseline') + need(any(st.norm2(st.sub(v, e)) > bound ** 2 for v, e in zip(bad, exact)), 'rotated reseed accepted') + out.append('rotated_closure_reseed_rejected') + # 2. Precision below the admission is refused. + need(not st.admitted(F(1, 8), 4, 3), 'low precision admitted') + out.append('low_precision_refused') + # 3. Margin-free coefficient (|b|=1) is not a contraction: the oracle divides by zero. + try: + st.exact_cycle_solve([st.ONE], [st.ONE], 0) + except ValueError: + out.append('unit_coefficient_rejected') + else: + raise ValueError('unit coefficient accepted') + # 4. Wrong inner shift direction in the kernel cascade is caught by the dense solve. + data = json.loads((HERE / 'vendor' / 'FACTORS.json').read_text()) + state = next(s for s in map(c.certify, data) if any(inside for inside, _ in s['factors'])) + x = inputs(3, 3) + y = apply_kernel(c, state, x, 1, st.ONE, state['bits'], st.Tape(), mutate='wrong_inner_shift') + exact = c.matrix_solve(x, c.phased_polynomial(state['q'], st.ONE), 1) + bound = cascade_bound(state, 3, 1) + need(any(st.norm2(st.sub(v, e)) > bound ** 2 for v, e in zip(y, exact)), 'wrong inner shift accepted') + out.append('wrong_inner_shift_rejected') + return out + + +def main(): + parser = argparse.ArgumentParser() + mode = parser.add_mutually_exclusive_group(required=True) + mode.add_argument('--check', action='store_true') + mode.add_argument('--write', action='store_true') + args = parser.parse_args() + c = pinned_vendor() + result = dict(status='passed', generic=generic(), traffic=traffic(), + kernels=kernels(c), controls=controls(c)) + text = json.dumps(result, indent=1, sort_keys=True) + '\n' + target = HERE / 'EXPECTED.json' + if args.write: + target.write_text(text) + else: + need(target.read_text() == text, 'replay differs from EXPECTED.json') + print('PASS_CYCLIC_INVERSE_STRIDE_BRIDGE generic=%d kernel_cases=%d controls=%d max_records_per_entry=%s' + % (result['generic']['cases'], len(result['kernels']), len(result['controls']), + result['traffic']['max_records_per_entry'])) + + +if __name__ == '__main__': + main() diff --git a/research/cyclic-stride-effective-depth/verify.py b/research/cyclic-stride-effective-depth/verify.py new file mode 100644 index 0000000000..155506daeb --- /dev/null +++ b/research/cyclic-stride-effective-depth/verify.py @@ -0,0 +1,112 @@ +"""Offline source-bound stride-depth replay, standard-library Python 3.11+.""" +import argparse +import gzip +import hashlib +import importlib +import json +from pathlib import Path +import re +import sys + +P = Path(__file__).resolve().parent +sys.dont_write_bytecode = True +sys.set_int_max_str_digits(100000) + + +def require(value, message): + if not value: + raise ValueError(message) + + +def unique_object(pairs): + out = {} + for key, value in pairs: + require(key not in out, 'duplicate JSON key: '+key) + out[key] = value + return out + + +def read_json(path): + data = gzip.decompress(path.read_bytes()) if path.suffix == '.gz' else path.read_bytes() + return json.loads(data, object_pairs_hook=unique_object) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':'), default=str) + + +def bindings(authoring=False): + manifest = P/'MANIFEST.json' + require(manifest.exists() or authoring, 'missing package manifest') + require(not any(path.is_symlink() for path in P.rglob('*')), 'package symlink') + if manifest.exists(): + record = read_json(manifest) + require(set(record) == {'files'} and type(record['files']) is dict, 'manifest schema') + files = record['files'] + actual = {str(path.relative_to(P)) for path in P.rglob('*') if path.is_file() and path != manifest} + require(set(files) == actual, 'package file coverage') + for name, sha in files.items(): + require(not Path(name).is_absolute() and '..' not in Path(name).parts, 'relative package path') + require(type(sha) is str and re.fullmatch('[0-9a-f]{64}', sha), 'manifest hash type') + require(hashlib.sha256((P/name).read_bytes()).hexdigest() == sha, 'package hash: '+name) + pins = read_json(P/'SOURCE-PINS.json') + require(len(pins['sources']) == 12, 'source inventory') + require(len({row['path'] for row in pins['sources']}) == 12, 'unique source inventory') + for row in pins['sources']: + name = row['path'] + require(not Path(name).is_absolute() and '..' not in Path(name).parts, 'relative source path') + raw = (P/name).read_bytes() + require(hashlib.sha256(raw).hexdigest() == row['sha256'], 'source SHA256: '+name) + require(hashlib.sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() == row['git_blob'], + 'source Git blob: '+name) + return dict(files=12, source_pins_sha256=hashlib.sha256((P/'SOURCE-PINS.json').read_bytes()).hexdigest()) + + +def modules(): + sys.path.insert(0, str(P)) + names = ['common', 'uniform', 'early', 'cases', 'kernels', 'controls', 'cubic', 'uniform_kernels'] + loaded = {} + for name in names: + loaded[name] = importlib.import_module(name) + require(Path(loaded[name].__file__).resolve() == P/(name+'.py'), 'local module binding: '+name) + return loaded + + +def calculate(): + loaded = modules() + result = dict(status='PASS_CYCLIC_STRIDE_EFFECTIVE_DEPTH', kappa='unchanged') + for name in ['cases', 'controls', 'cubic', 'kernels', 'uniform_kernels']: + result[name] = loaded[name].main() + result['scope'] = ('Effective nonzero depth independent of L, exact equivalence with the ' + 'unchanged stride solver, and cubic prepared-kernel precision. ' + 'Inherited clean scratch model; no dirty-array, bit-reversible or kappa claim.') + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', type=Path, help='authoring: write a fresh external receipt') + parser.add_argument('--out', type=Path, help='verify expected mathematics and write a fresh external copy') + parser.add_argument('--bindings-only', action='store_true') + args = parser.parse_args() + require(sum(bool(v) for v in (args.write, args.out, args.bindings_only)) <= 1, 'choose one mode') + destination = args.write or args.out + if destination: + require(not destination.exists(), 'output already exists') + require(not destination.resolve().is_relative_to(P), 'output must be outside package') + pins = bindings(authoring=args.write is not None) + if args.bindings_only: + print('PASS_STRIDE_DEPTH_BINDINGS sources=12') + return + result = calculate() + result['sources'] = pins + if not args.write: + require(canonical(result) == canonical(read_json(P/'EXPECTED.json.gz')), 'mathematical receipt mismatch') + if destination: + with destination.open('x') as handle: + handle.write(json.dumps(result, indent=2, sort_keys=True, default=str)+'\n') + print('PASS_CYCLIC_STRIDE_EFFECTIVE_DEPTH arrays=423 kernels=300 uniform=64 scalar_paths=90 budgets=216 kappa=unchanged') + + +if __name__ == '__main__': + main()