diff --git a/.github/workflows/averaged-cyclotomic-height.yml b/.github/workflows/averaged-cyclotomic-height.yml new file mode 100644 index 0000000000..c34148c6e2 --- /dev/null +++ b/.github/workflows/averaged-cyclotomic-height.yml @@ -0,0 +1,43 @@ +name: Averaged cyclotomic height + +on: + workflow_dispatch: + pull_request: + paths: + - 'research/averaged-cyclotomic-height/**' + - '.github/workflows/averaged-cyclotomic-height.yml' + push: + branches: ['codex/averaged-cyclotomic-height-20261013'] + paths: + - 'research/averaged-cyclotomic-height/**' + - '.github/workflows/averaged-cyclotomic-height.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: Install exact-algebra dependency + run: python -m pip install -r research/averaged-cyclotomic-height/requirements.txt + - name: Rational intervals, exact resultants and integer budgets + run: python -I -O -B research/averaged-cyclotomic-height/verify.py --out /tmp/averaged-height-math.json + - name: Package rejection controls and full read-only relocation + run: python -I -O -B research/averaged-cyclotomic-height/test_package.py --out /tmp/averaged-height-package.json + - uses: actions/upload-artifact@v4 + if: always() + with: + name: averaged-height-python-${{ matrix.python }} + path: | + /tmp/averaged-height-math.json + /tmp/averaged-height-package.json diff --git a/research/averaged-cyclotomic-height-validation/LINUX314-MATH.json.gz b/research/averaged-cyclotomic-height-validation/LINUX314-MATH.json.gz new file mode 100644 index 0000000000..35906824df Binary files /dev/null and b/research/averaged-cyclotomic-height-validation/LINUX314-MATH.json.gz differ diff --git a/research/averaged-cyclotomic-height-validation/LINUX314-PACKAGE.json b/research/averaged-cyclotomic-height-validation/LINUX314-PACKAGE.json new file mode 100644 index 0000000000..838a0a043a --- /dev/null +++ b/research/averaged-cyclotomic-height-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: budgets.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/pr621/PROOF.md" + }, + { + "name": "source Git object independent of manifest", + "rejected": true, + "terminal": "ValueError: source Git blob: vendor/pr621/PROOF.md" + }, + { + "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: budgets" + }, + { + "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": "b25ae109654d2e3ac16e6348c982b86d8c07fca80d8cff600205511b9d2617bf" + } + ], + "full_readonly_replay": true, + "rejected": 11, + "status": "PASS_AVERAGED_HEIGHT_PACKAGE" +} diff --git a/research/averaged-cyclotomic-height-validation/LINUX314-PLATFORM.json b/research/averaged-cyclotomic-height-validation/LINUX314-PLATFORM.json new file mode 100644 index 0000000000..163297a4b0 --- /dev/null +++ b/research/averaged-cyclotomic-height-validation/LINUX314-PLATFORM.json @@ -0,0 +1,11 @@ +{ + "bytecode_disabled": true, + "isolated": true, + "machine": "aarch64", + "manifest_sha256": "7844dd0039723d9a955a2d0961ff1cb0f710f21277c0b2905577ad7b2b5c2f2a", + "mpmath": "1.3.0", + "optimized": true, + "platform": "Linux-6.17.0-1032-nvidia-aarch64-with-glibc2.39", + "python": "3.14.8", + "sympy": "1.14.0" +} diff --git a/research/averaged-cyclotomic-height-validation/LINUX314-TERMINAL.json b/research/averaged-cyclotomic-height-validation/LINUX314-TERMINAL.json new file mode 100644 index 0000000000..a2c152e250 --- /dev/null +++ b/research/averaged-cyclotomic-height-validation/LINUX314-TERMINAL.json @@ -0,0 +1,6 @@ +{ + "full_package_controls": true, + "manifest_sha256": "7844dd0039723d9a955a2d0961ff1cb0f710f21277c0b2905577ad7b2b5c2f2a", + "math_sha256": "b25ae109654d2e3ac16e6348c982b86d8c07fca80d8cff600205511b9d2617bf", + "status": "PASS_FROZEN_AVERAGED_HEIGHT_PACKAGE" +} diff --git a/research/averaged-cyclotomic-height-validation/LINUX314.log.txt b/research/averaged-cyclotomic-height-validation/LINUX314.log.txt new file mode 100644 index 0000000000..875d8b38ae --- /dev/null +++ b/research/averaged-cyclotomic-height-validation/LINUX314.log.txt @@ -0,0 +1,40 @@ +PASS 752 integer budgets, exact logarithm enclosure and dyadic polynomial +3 PASS rational interval enclosures +4 PASS rational interval enclosures +5 PASS rational interval enclosures +7 PASS rational interval enclosures +8 PASS rational interval enclosures +9 PASS rational interval enclosures +11 PASS rational interval enclosures +13 PASS rational interval enclosures +16 PASS rational interval enclosures +17 PASS rational interval enclosures +19 PASS rational interval enclosures +23 PASS rational interval enclosures +25 PASS rational interval enclosures +27 PASS rational interval enclosures +29 PASS rational interval enclosures +31 PASS rational interval enclosures +32 PASS rational interval enclosures +3 PASS independent exact resultant +4 PASS independent exact resultant +5 PASS independent exact resultant +7 PASS independent exact resultant +8 PASS independent exact resultant +9 PASS independent exact resultant +PASS_AVERAGED_CYCLOTOMIC_HEIGHT interval_radices=17 exact_resultants=6 budgets=752 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_AVERAGED_HEIGHT_PACKAGE rejected=11 full_readonly_replay=True +PASS_AVERAGED_HEIGHT_BINDINGS sources=12 +PASS_FROZEN_AVERAGED_HEIGHT_PACKAGE diff --git a/research/averaged-cyclotomic-height-validation/MACOS311-MATH.json.gz b/research/averaged-cyclotomic-height-validation/MACOS311-MATH.json.gz new file mode 100644 index 0000000000..35906824df Binary files /dev/null and b/research/averaged-cyclotomic-height-validation/MACOS311-MATH.json.gz differ diff --git a/research/averaged-cyclotomic-height-validation/MACOS311-PACKAGE.json b/research/averaged-cyclotomic-height-validation/MACOS311-PACKAGE.json new file mode 100644 index 0000000000..838a0a043a --- /dev/null +++ b/research/averaged-cyclotomic-height-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: budgets.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/pr621/PROOF.md" + }, + { + "name": "source Git object independent of manifest", + "rejected": true, + "terminal": "ValueError: source Git blob: vendor/pr621/PROOF.md" + }, + { + "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: budgets" + }, + { + "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": "b25ae109654d2e3ac16e6348c982b86d8c07fca80d8cff600205511b9d2617bf" + } + ], + "full_readonly_replay": true, + "rejected": 11, + "status": "PASS_AVERAGED_HEIGHT_PACKAGE" +} diff --git a/research/averaged-cyclotomic-height-validation/MACOS311-PLATFORM.json b/research/averaged-cyclotomic-height-validation/MACOS311-PLATFORM.json new file mode 100644 index 0000000000..8839b7ab18 --- /dev/null +++ b/research/averaged-cyclotomic-height-validation/MACOS311-PLATFORM.json @@ -0,0 +1,11 @@ +{ + "bytecode_disabled": true, + "isolated": true, + "machine": "arm64", + "manifest_sha256": "7844dd0039723d9a955a2d0961ff1cb0f710f21277c0b2905577ad7b2b5c2f2a", + "mpmath": "1.3.0", + "optimized": true, + "platform": "macOS-27.0.1-arm64-arm-64bit", + "python": "3.11.15", + "sympy": "1.14.0" +} diff --git a/research/averaged-cyclotomic-height-validation/MACOS311-TERMINAL.json b/research/averaged-cyclotomic-height-validation/MACOS311-TERMINAL.json new file mode 100644 index 0000000000..a2c152e250 --- /dev/null +++ b/research/averaged-cyclotomic-height-validation/MACOS311-TERMINAL.json @@ -0,0 +1,6 @@ +{ + "full_package_controls": true, + "manifest_sha256": "7844dd0039723d9a955a2d0961ff1cb0f710f21277c0b2905577ad7b2b5c2f2a", + "math_sha256": "b25ae109654d2e3ac16e6348c982b86d8c07fca80d8cff600205511b9d2617bf", + "status": "PASS_FROZEN_AVERAGED_HEIGHT_PACKAGE" +} diff --git a/research/averaged-cyclotomic-height-validation/MACOS311.log.txt b/research/averaged-cyclotomic-height-validation/MACOS311.log.txt new file mode 100644 index 0000000000..875d8b38ae --- /dev/null +++ b/research/averaged-cyclotomic-height-validation/MACOS311.log.txt @@ -0,0 +1,40 @@ +PASS 752 integer budgets, exact logarithm enclosure and dyadic polynomial +3 PASS rational interval enclosures +4 PASS rational interval enclosures +5 PASS rational interval enclosures +7 PASS rational interval enclosures +8 PASS rational interval enclosures +9 PASS rational interval enclosures +11 PASS rational interval enclosures +13 PASS rational interval enclosures +16 PASS rational interval enclosures +17 PASS rational interval enclosures +19 PASS rational interval enclosures +23 PASS rational interval enclosures +25 PASS rational interval enclosures +27 PASS rational interval enclosures +29 PASS rational interval enclosures +31 PASS rational interval enclosures +32 PASS rational interval enclosures +3 PASS independent exact resultant +4 PASS independent exact resultant +5 PASS independent exact resultant +7 PASS independent exact resultant +8 PASS independent exact resultant +9 PASS independent exact resultant +PASS_AVERAGED_CYCLOTOMIC_HEIGHT interval_radices=17 exact_resultants=6 budgets=752 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_AVERAGED_HEIGHT_PACKAGE rejected=11 full_readonly_replay=True +PASS_AVERAGED_HEIGHT_BINDINGS sources=12 +PASS_FROZEN_AVERAGED_HEIGHT_PACKAGE diff --git a/research/averaged-cyclotomic-height-validation/README.md b/research/averaged-cyclotomic-height-validation/README.md new file mode 100644 index 0000000000..148464e78b --- /dev/null +++ b/research/averaged-cyclotomic-height-validation/README.md @@ -0,0 +1,38 @@ +# Frozen averaged-height validation + +The complete package in `../averaged-cyclotomic-height` passed on macOS +arm64 / Python 3.11.15 and Linux aarch64 / Python 3.14.8, both with +SymPy 1.14.0 and mpmath 1.3.0. Each replay used `-I -O -B`. + +Each platform ran all 17 rational interval cases, six exact resultants and +752 integer budgets three times: the ordinary verifier, the deliberately +altered-receipt rejection, and the full read-only relocation. Each package +harness rejected eleven faults. The full mathematical receipts are byte +identical after decompression, including all rational endpoints and integer +budget rows. The Linux source tree was read-only and outside Git; its +supervisor recorded exit code zero. + +- Mathematical receipt SHA256: + `b25ae109654d2e3ac16e6348c982b86d8c07fca80d8cff600205511b9d2617bf`. +- Source manifest SHA256: + `7844dd0039723d9a955a2d0961ff1cb0f710f21277c0b2905577ad7b2b5c2f2a`. +- `SOURCE-GIT-CHECK.json` records the twelve retained files checked against + immutable original Git objects before replay. +- `MACOS311-*` and `LINUX314-*` contain the complete math, package-control, + platform and terminal receipts. The logs record successful completion. +- `REPOSITORY-CHECKS.log.txt` records the selected-record check and all + 25 selected-record/inventory/proof-binding tests at the publication base. + +The preparation base recorded in the frozen source pins is +`8bddbee377e2f3ce1f1247196c4b290d55767d20`. The isolated publication branch +was subsequently advanced to main +`2921874911956718fcaaaf9396fe8267b3cfa9f0` without changing any frozen +package byte. Main still selects PR942 at +`1661960547713947/10^18`. This contribution does not change that selection. + +The all-size claim comes from the written proof. The large-radix rows test +exact exponent arithmetic; no inverse at those enormous word sizes was +executed. The full repository suite, selected construction's cold replay +and full multiplication theorem were not verified here. No independent +human/delegated-agent review or practical speedup is claimed. Hosted CI is +separate from these retained local platform results. diff --git a/research/averaged-cyclotomic-height-validation/REPOSITORY-CHECKS.log.txt b/research/averaged-cyclotomic-height-validation/REPOSITORY-CHECKS.log.txt new file mode 100644 index 0000000000..94d20716c3 --- /dev/null +++ b/research/averaged-cyclotomic-height-validation/REPOSITORY-CHECKS.log.txt @@ -0,0 +1,12 @@ +Publication base: 2921874911956718fcaaaf9396fe8267b3cfa9f0 +COMMAND ['make', 'selected-record-check'] +python3 -B scripts/verify_selected_result.py +PASS selected record, exact kappa, original source inventory and proof supplement: 1661960547713947/1000000000000000000 +EXIT 0 +COMMAND ['python3', '-B', '-m', 'unittest', 'discover', '-s', 'tests', '-p', 'test_selected*.py'] +......................... +---------------------------------------------------------------------- +Ran 25 tests in 0.327s + +OK +EXIT 0 diff --git a/research/averaged-cyclotomic-height-validation/SOURCE-GIT-CHECK.json b/research/averaged-cyclotomic-height-validation/SOURCE-GIT-CHECK.json new file mode 100644 index 0000000000..4f324551c4 --- /dev/null +++ b/research/averaged-cyclotomic-height-validation/SOURCE-GIT-CHECK.json @@ -0,0 +1,89 @@ +{ + "status": "PASS_SOURCE_GIT_OBJECTS", + "sources": [ + { + "path": "vendor/pr621/PROOF.md", + "head": "520774462b19b29af41554b74def31f9d01e997e", + "source_path": "research/prime-power-cyclic-inverse/PROOF.md", + "sha256": "2b8056c88e66f692f407450fff0414d41bcd09db8597be22e274a6c3dc20eb9e", + "git_blob": "0c757c37c70fdeb261d73f111ceedd3b233287bf" + }, + { + "path": "vendor/pr621/NOTICE.md", + "head": "520774462b19b29af41554b74def31f9d01e997e", + "source_path": "research/prime-power-cyclic-inverse/NOTICE.md", + "sha256": "96111c95cfec3c03a6f69c8e02c5d0bceff957d187e638d0534c676d6e3ffd77", + "git_blob": "a78e84066711e2f4776152d69d480e9629c26961" + }, + { + "path": "vendor/pr621/verify.py", + "head": "520774462b19b29af41554b74def31f9d01e997e", + "source_path": "research/prime-power-cyclic-inverse/verify.py", + "sha256": "40e5e18cbd98d39ba6d0bb036778ccacc077dff009099a54b9c8f441af5d6a56", + "git_blob": "20a069f42ac2e7102d8b1ddac4f568b83e077074" + }, + { + "path": "vendor/pr621/independent_verify.py", + "head": "520774462b19b29af41554b74def31f9d01e997e", + "source_path": "research/prime-power-cyclic-inverse/independent_verify.py", + "sha256": "515d60fbbb28c025251b5a2929231b4b6124dabe357b8526fdb93c1456c847ce", + "git_blob": "813ffd0304c98c6ea4fea89f021a4247f26f9971" + }, + { + "path": "vendor/pr628/PROOF.md", + "head": "0768f97d06c623b8211e651543c66135796b62bf", + "source_path": "research/prime-power-cyclic-scan/PROOF.md", + "sha256": "595893609764c64a90d9b21b9cbd6d9e61980703f3deb43361105cf8c3d1d093", + "git_blob": "fb8fe7cb3bd036c69047ae7b4f4009a51b11825b" + }, + { + "path": "vendor/pr628/NOTICE.md", + "head": "0768f97d06c623b8211e651543c66135796b62bf", + "source_path": "research/prime-power-cyclic-scan/NOTICE.md", + "sha256": "abeacf1ad1491d5797cfcf1f3832799bbf3b24b99597229d7bc884059a51ec68", + "git_blob": "22fbeb8ef0a28dd6b3feea718492091319ceb96e" + }, + { + "path": "vendor/pr628/interval_kernel.py", + "head": "0768f97d06c623b8211e651543c66135796b62bf", + "source_path": "research/prime-power-cyclic-scan/interval_kernel.py", + "sha256": "9b7bb24640a9a7d3f83c7951dfef483ec933db4c50de6c0130b85f450eeddfbe", + "git_blob": "1182175a55cb871481de0f56ea9ae56e474705fe" + }, + { + "path": "vendor/pr862/PROOF.md", + "head": "57e0659150d323b784580110b36aa64a2dca2a33", + "source_path": "research/cubic-cyclic-inverse/PROOF.md", + "sha256": "bdb0518892c631f8b6ac149535ac5a92270def19fe7778ca737641cd56b7da0b", + "git_blob": "0196499f010857b58ea297611f44721a4b7a0ec6" + }, + { + "path": "vendor/pr862/NOTICE.md", + "head": "57e0659150d323b784580110b36aa64a2dca2a33", + "source_path": "research/cubic-cyclic-inverse/NOTICE.md", + "sha256": "08c25cd6248e8c4dc7008e14e9ea7690f9084e94f927bb602363773637a89921", + "git_blob": "737060bd4d9666a925dfd1e17fc6eaa53c289b8d" + }, + { + "path": "vendor/pr977/PROOF.md", + "head": "2846af720af190cb75b45ebddbb0357dec1121ec", + "source_path": "research/cyclic-stride-effective-depth/PROOF.md", + "sha256": "30c296d4f1947cbcaaeb0fe575c36e3c2308f1583dde6029efb4a162fb7a4b27", + "git_blob": "6019f4d03f2a429c07aae18deba0525d9af36d71" + }, + { + "path": "vendor/pr977/NOTICE.md", + "head": "2846af720af190cb75b45ebddbb0357dec1121ec", + "source_path": "research/cyclic-stride-effective-depth/NOTICE.md", + "sha256": "b6e1bab630faf7eb4ad0952173dd789a7f5d6333bf938b275bcf087474f4f189", + "git_blob": "57939c758daebf9b7c952ce849ccb169d10c35c6" + }, + { + "path": "vendor/pr977/cubic.py", + "head": "2846af720af190cb75b45ebddbb0357dec1121ec", + "source_path": "research/cyclic-stride-effective-depth/cubic.py", + "sha256": "7c6cbeedeb77dee4a167fb32b4e14b33f8bd00d69a560d0d2232ecfca7ee59f8", + "git_blob": "61c213dd255e084805cb3ab22fc9ec5d2e947b66" + } + ] +} diff --git a/research/averaged-cyclotomic-height-validation/VALIDATION.json b/research/averaged-cyclotomic-height-validation/VALIDATION.json new file mode 100644 index 0000000000..0fa37dfe43 --- /dev/null +++ b/research/averaged-cyclotomic-height-validation/VALIDATION.json @@ -0,0 +1,29 @@ +{ + "files": { + "LINUX314-MATH.json.gz": "3050ab8713b13e0b95510f6d2601b254ec4b6a9ce81db8ca3467fc93f24d49f5", + "LINUX314-PACKAGE.json": "2a5c27c854fdcf76ecea15a07f5beccc45ea198728c806882ff36133555dc4ae", + "LINUX314-PLATFORM.json": "b2689b8e145d0fee0df73a85501f012b3ca2a695ee0b2edd4e7584f73fdc24e1", + "LINUX314-TERMINAL.json": "7c8b4ad5ac38c7776a0116039b80084f509dfaa28d645c7215f0270bcc1d0aaa", + "LINUX314.log.txt": "4ea474f1fd25336c73f335dbec30d714e8f6eaa74516196ade64f133c599588d", + "MACOS311-MATH.json.gz": "3050ab8713b13e0b95510f6d2601b254ec4b6a9ce81db8ca3467fc93f24d49f5", + "MACOS311-PACKAGE.json": "2a5c27c854fdcf76ecea15a07f5beccc45ea198728c806882ff36133555dc4ae", + "MACOS311-PLATFORM.json": "7cc8655afa33fa6f9e077cfaad12b6153500e92c2079a80fa4bac2d31087e62b", + "MACOS311-TERMINAL.json": "7c8b4ad5ac38c7776a0116039b80084f509dfaa28d645c7215f0270bcc1d0aaa", + "MACOS311.log.txt": "4ea474f1fd25336c73f335dbec30d714e8f6eaa74516196ade64f133c599588d", + "README.md": "278d3666ac88c5f33d283cfddf9558507c3f5d09f2d3b96210dfd6940c1feff9", + "REPOSITORY-CHECKS.log.txt": "cc79f9351bd035294a41bdc84e4870a2a18c3680df1422679a5e553359f6d398", + "SOURCE-GIT-CHECK.json": "8434f0830f30adad6902cf63d75d6056f85268d00999d7e8cfea24358a79d61e" + }, + "full_decompressed_receipts_byte_equal": true, + "linux_source_read_only": true, + "linux_supervisor_exit": 0, + "manifest_sha256": "7844dd0039723d9a955a2d0961ff1cb0f710f21277c0b2905577ad7b2b5c2f2a", + "math_sha256": "b25ae109654d2e3ac16e6348c982b86d8c07fca80d8cff600205511b9d2617bf", + "package_rejections_per_platform": 11, + "publication_base": "2921874911956718fcaaaf9396fe8267b3cfa9f0", + "read_only_full_replay_per_platform": true, + "selected_kappa": "1661960547713947/1000000000000000000", + "selected_record_checks": true, + "selected_related_tests": 25, + "status": "PASS_TWO_COMPLETE_FROZEN_PLATFORM_REPLAYS" +} diff --git a/research/averaged-cyclotomic-height/EXPECTED.json.gz b/research/averaged-cyclotomic-height/EXPECTED.json.gz new file mode 100644 index 0000000000..35906824df Binary files /dev/null and b/research/averaged-cyclotomic-height/EXPECTED.json.gz differ diff --git a/research/averaged-cyclotomic-height/MANIFEST.json b/research/averaged-cyclotomic-height/MANIFEST.json new file mode 100644 index 0000000000..51a3173dbe --- /dev/null +++ b/research/averaged-cyclotomic-height/MANIFEST.json @@ -0,0 +1,27 @@ +{ + "files": { + "EXPECTED.json.gz": "3050ab8713b13e0b95510f6d2601b254ec4b6a9ce81db8ca3467fc93f24d49f5", + "NOTICE.md": "4a0c8a8c8568ccea7dc4b0d9b455408b806da42d18521732ccc923a8275be2ce", + "PROOF.md": "5f8ec1431faecb7a2503f8c2dd7e398e5a749176d36cd54ae57763b4a4f0d4c4", + "README.md": "b2ca4494c2d057fb61a0cb703c6cac2c36f1b28216a5846024af750a5667e3a0", + "SOURCE-PINS.json": "66c2898770feb2bc8d0691d75efae711023e0c4d1e0006bd9d5257af3f1e55f6", + "budgets.py": "2b2a5ddb2669432c2a7199dc3d7d4ab1ece83166af4b70649e361902db1e551d", + "interval_check.py": "ad6786e9f2db9000a438097f8c4d41f645b54a8df8e70315cc617c19c8a979b1", + "requirements.txt": "47fd19021144e071cc43b6e265aafada0056abe89724ad95bd6e3a8e37995b94", + "resultants.py": "486c4ec2f6723026c50452c67c36c4dfa4ca4e8c90e1249fc77fff73964ff5df", + "test_package.py": "64148d9084b4477b9dcc995afa2a66427716167706910c745c9575c892558c59", + "vendor/pr621/NOTICE.md": "96111c95cfec3c03a6f69c8e02c5d0bceff957d187e638d0534c676d6e3ffd77", + "vendor/pr621/PROOF.md": "2b8056c88e66f692f407450fff0414d41bcd09db8597be22e274a6c3dc20eb9e", + "vendor/pr621/independent_verify.py": "515d60fbbb28c025251b5a2929231b4b6124dabe357b8526fdb93c1456c847ce", + "vendor/pr621/verify.py": "40e5e18cbd98d39ba6d0bb036778ccacc077dff009099a54b9c8f441af5d6a56", + "vendor/pr628/NOTICE.md": "abeacf1ad1491d5797cfcf1f3832799bbf3b24b99597229d7bc884059a51ec68", + "vendor/pr628/PROOF.md": "595893609764c64a90d9b21b9cbd6d9e61980703f3deb43361105cf8c3d1d093", + "vendor/pr628/interval_kernel.py": "9b7bb24640a9a7d3f83c7951dfef483ec933db4c50de6c0130b85f450eeddfbe", + "vendor/pr862/NOTICE.md": "08c25cd6248e8c4dc7008e14e9ea7690f9084e94f927bb602363773637a89921", + "vendor/pr862/PROOF.md": "bdb0518892c631f8b6ac149535ac5a92270def19fe7778ca737641cd56b7da0b", + "vendor/pr977/NOTICE.md": "b6e1bab630faf7eb4ad0952173dd789a7f5d6333bf938b275bcf087474f4f189", + "vendor/pr977/PROOF.md": "30c296d4f1947cbcaaeb0fe575c36e3c2308f1583dde6029efb4a162fb7a4b27", + "vendor/pr977/cubic.py": "7c6cbeedeb77dee4a167fb32b4e14b33f8bd00d69a560d0d2232ecfca7ee59f8", + "verify.py": "8fc79b50d08c55db72ca9a673250b26a5dcb43b749ec8e99383d82b0adbe07ed" + } +} diff --git a/research/averaged-cyclotomic-height/NOTICE.md b/research/averaged-cyclotomic-height/NOTICE.md new file mode 100644 index 0000000000..8ded624012 --- /dev/null +++ b/research/averaged-cyclotomic-height/NOTICE.md @@ -0,0 +1,48 @@ +# Attribution and scope + +The averaged-height estimate and its integration with the explicit +precision budget were prepared by Chafik Boukhalfa (@chafreaky), with +substantial OpenAI Codex assistance. Apache-2.0, as in the repository. +No literature-priority, independent human review, delegated-agent review +or full formal-verification claim is made. + +- Ali Romman (@aliromman), PR621, head + `520774462b19b29af41554b74def31f9d01e997e`: the prime-power ideal + argument, nonzero resultant, cofactor/circle estimate, Fourier inverse + bound and rational field checker. Its proof, notice and two checkers + are retained byte for byte. The new `resultants.py` adapts the independent + SymPy checker's field and Sylvester constructions, and compares a + polynomial resultant with the retained rational-field computation. +- Chafik Boukhalfa, PR628, head + `0768f97d06c623b8211e651543c66135796b62bf`: coefficient preparation, + root-margin framework and rational interval kernel. Its proof, notice + and interval implementation are retained. The new interval checker sets + its documented module precision to 192 bits, and adds outward rational + logarithm and square-root bounds. +- Chafik Boukhalfa, PR862, head + `57e0659150d323b784580110b36aa64a2dca2a33`: the common-operator + complementary-factor bound and explicit cubic precision budgets. + Its proof and notice are retained. +- Chafik Boukhalfa, PR977, head + `2846af720af190cb75b45ebddbb0357dec1121ec`: effective nonzero depth + for the original PR846 stride solver and its cubic-budget integration. + Its proof, notice and budget code are retained. `budgets.py` adapts those + formulas to the new circle exponent. `verify.py` and `test_package.py` + adapt that package's source binding, receipt comparison and relocation + harness. Rohan Guliani's PR846 arbitrary-stride Euclidean solver and + Charles Bethin's PR764 shared-suffix estimate remain credited through + the retained notice; no new solver execution is claimed here. + +The kernel comes from the pinned OpenAI exact-DFT manuscript, with its +classical Newton/q-Pochhammer factorization provenance retained in PR621's +notice. The logarithm Fourier series, geometric sums, Hadamard inequality, +algebraic norm, Mahler-measure argument, approximate factorization and fast +arithmetic remain classical ingredients. The new proof is self-contained +for its averaged-height estimate and does not infer a finite rational-unit +bound from an irrational Sudler-product theorem. + +All retained files have immutable Git-blob and SHA256 pins in +`SOURCE-PINS.json`. Existing notices and licenses are unchanged. This +contribution improves a sufficient precision theorem; it does not resolve +the full-transform, common-label, Clifford, physical hosting or complete +multiplication obligations, and it makes no new kappa claim. diff --git a/research/averaged-cyclotomic-height/PROOF.md b/research/averaged-cyclotomic-height/PROOF.md new file mode 100644 index 0000000000..3215a58a40 --- /dev/null +++ b/research/averaged-cyclotomic-height/PROOF.md @@ -0,0 +1,251 @@ +# Averaged coefficient heights for the prime-power cyclic inverse + +Theorem and proof, 2026-10-13. This is a new derivation on top of +PR621's nonzero resultant and Bezout argument. It is not a new kappa, +a full transform, or a common-label implementation. The finite scripts +check examples and arithmetic; the argument below supplies the universal +claim. No independent human review or formal verification is claimed. + +Let r>=3 be a prime power, n=r-1, D=phi(r), zeta=exp(2 pi i/r), and + + f_k(z) = sum_(j=0)^n a_(k,j) z^j, + a_(k,j) = product_(s=j+1)^n (1-zeta^(ks)), + H_k = sum_j |a_(k,j)|, + +where k ranges over the units modulo r. Thus f_k=r P_k, as in PR621. +All logarithms in the analytic argument are natural. Write t=log r. +We prove + + sum_(k unit mod r) log H_k <= D (4t^2+8t+2). (1) + +The existing proof used H_k<=2^r-1 separately at every embedding. +Using (1) in exactly the same determinant and cofactor argument gives + + |P_k(z)| >= exp[-n D (4t^2+8t+2)] / (2rn), |z|=1. (2) + +Consequently, with ell=ceil(log2 r), + + d = 1+2ell+n D min(r,8ell^2) + +is a valid integer exponent for |P_k(z)|>=2^-d. The minimum retains +PR621's cubic bound at small radices. The new exponent is +O(r phi(r) log^2 r), uniformly in the primitive embedding and circle +point. No average-over-embeddings assumption is imposed on the output. +The original uniform bound and its proof are retained in +[`vendor/pr621/PROOF.md`](vendor/pr621/PROOF.md). + +## The discrete logarithm has small Fourier mass + +Define L(0)=0 and L(s)=log|1-zeta^s| for 1<=s=1) rho^m cos(2 pi m s/r)/m. + +Aliasing into r residues and the triangle inequality show that the +sum of the moduli of its discrete Fourier coefficients is at most +sum_(m>=1) rho^m/m=-log(1-rho)=log r. + +For s!=0, set a_s=|1-zeta^s|. We have + + |1-rho zeta^s|^2/a_s^2 = rho(1+delta^2/(rho a_s^2)). + +By the triangle inequality, -log(1-delta)<=delta/rho, and +log(1+x)<=x for x>=0, this gives + + |L(s)-Lrho(s)| <= delta/(2rho)+delta^2/(2rho a_s^2). + +The difference can have either sign. Pair s with r-s. Concavity of +sine gives a_s>=4 min(s,r-s)/r, so comparison of the reciprocal-square +tail with its integral yields + + sum_(s=1)^(r-1) a_s^-2 + <= (r^2/8) sum_(j>=1) j^-2 <= r^2/4. + +Consequently, since rho>=2/3, + + sum_(s=1)^(r-1) |L(s)-Lrho(s)| + <= (r-1)delta/(2rho)+delta^2 r^2/(8rho) + = 1/2+1/(8rho) <=11/16<1. + +At s=0 the difference is log r. For any sampled function E, normalization gives +sum_h |Ehat(h)|<=sum_s |E(s)|. Applying this to L-Lrho gives + + sum_h |Lhat(h)| <= 2log r+11/16 <=2log r+1. (4) + +The value at zero is essential: silently omitting its correction would +undercharge the Fourier mass. We never evaluate L(0) in a coefficient +product; it is only a convenient finite Fourier extension. + +## Average a geometric-sum bound over units + +Fix h!=0 modulo r and put d0=r/gcd(h,r). For any interval I of +consecutive integers, and any unit k modulo r, + + |sum_(s in I) zeta^(hks)| <= 2/|1-zeta^(hk)|. + +As k ranges over the units modulo r, zeta^(hk) ranges uniformly over +the primitive d0-th roots. This follows from the surjection of the +unit groups for prime-power moduli, followed by multiplication by +h/gcd(h,r), a unit modulo d0. The fibers have equal size. In particular +d0 is a prime power and d0/phi(d0)<=2, including d0=2. + +Pairing j with d0-j and using sin(pi j/d0)>=2j/d0 for +1<=j<=floor(d0/2) gives + + sum_(j=1)^(d0-1) 1/sin(pi j/d0) + <= d0 H_floor(d0/2) <= d0 (1+log d0). + +The middle term is overcounted when d0 is even, which is harmless. +Hence the average over primitive k of the geometric-sum bound is +at most 2(1+log r). This bound holds simultaneously for every I; +the right-hand side for each k does not depend on I. + +Let M_k be the maximum of zero and all logarithms log|a_(k,j)|. +Fourier inversion, (3), and the triangle inequality give the pointwise +upper bound + + M_k <= log r + sum_(h=1)^(r-1) |Lhat(h)| 2/|1-zeta^(hk)|. + +Average this inequality and apply (4). Because H_k<=r exp(M_k), + + average_k log H_k + <= 2log r+2(2log r+1)(1+log r) + = 4t^2+8t+2, + +which is (1). This averages an upper bound on the maximum; it does +not exchange an average and a maximum. + +## Resultant and cofactor cancellation + +Use PR621's Sylvester matrix for f and its conjugate reciprocal f*. +Let R be its determinant in Q(zeta). The prime-power ideal argument +from that proof establishes R!=0. For each embedding k, every +column has Euclidean norm at most H_k, so |R_k|<=H_k^(2n). +The chosen embedding and its complex conjugate have the same H and +the same |R|; they are distinct since r>=3. The nonzero algebraic +integer norm therefore gives + + |R| >= product_(k excluding chosen pair) H_k^(-n). + +The coefficients of the two Bezout polynomials are cofactors. Each +cofactor at the chosen embedding has modulus at most H^(2n-1). +For |z|=1, |f*(z)|=|f(z)|, so + + |P(z)| >= |R|/[2rn H^(2n-1)] + >= H/[2rn product_(all k) H_k^n] + >= 1/[2rn product_(all k) H_k^n]. (5) + +Here H>=1 because f is monic. The local cofactor powers cancel the +two removed embeddings exactly, leaving a favorable numerator H. +Equation (1) now proves (2). No rationality or Galois invariance of R +is assumed; such invariance is false already at r=5. + +## Dyadic exponent and inherited precision budgets + +Since 2/3=2 the second difference is +5ell^2-8ell-3=1+12(ell-2)+5(ell-2)^2>=0. Also +2rn<=2^(1+2ell). These inequalities prove the displayed d. + +PR862's perturbation and partial-inverse estimates, and PR977's +effective-depth stride theorem, use the circle theorem only through +d. Set T=n D min(r,8ell^2) and use their unchanged definitions: + + d=1+2ell+T, a0=2d+r+2, g=d+ell+2r+2, h=a0+2r, + c=ceil(log2(r-1)), + e=max(d+1,a0+1,p+2a0+m+3), b=max((r-1)ell,e+r+3), + J=c+2h+3g+ell+m+5, W=p+J+2, G=m+ell+h+g+8. + +In particular, PR621's Fourier inverse estimate with the unchanged +coefficient bound H=2^r-1 gives ||P(U)^-1||<=2^a0. The bound applies +to every isometry with ||U^j||=1 for all integer j, by the absolutely +convergent Laurent series argument retained in PR862. This includes +arbitrary-stride cyclic unit shifts. The inherited proofs are retained +as [`vendor/pr862/PROOF.md`](vendor/pr862/PROOF.md) and +[`vendor/pr977/PROOF.md`](vendor/pr977/PROOF.md). + +Here p,m>=0, input infinity norm is <=2^m, and target error is +2^-p. Direct substitution gives + + W=p+m+7T+12r+18ell+c+24, + G=m+3T+5r+8ell+15, + b=p+m+4T+3r+8ell+14. + +The last equality follows because p+2a0+m+3 dominates the other e +terms, and its resulting b term exceeds (r-1)ell. For the latter, +d>=n D min(r,8ell^2)>=n ell: D>=1, r>=ell and +8ell^2>=ell. With N=r^2 ell^2, T<=8N and r>=3, ell>=2, +ell<=r, N>=12r, these give convenient universal bounds + + W<=p+m+60N, G<=m+26N, b<=p+m+34N. + +For example, the non-T W terms are <=31r+24<=39r<4N; +the G terms are <=13r+15<=18r<2N; the b terms are +<=11r+14<=16r<2N. All previous cubic bounds remain valid because +d did not increase. The admission W>=2g+8 and the common-error +contraction exponents remain unchanged algebraically. Thus the +existing clean-scratch arbitrary-stride solver has the same 40L +record bound per first-order inverse and an O(r^2 log^2 r) precision +overhead. This statement inherits all phase-oracle, coefficient +preparation, word-size, and clean-workspace charges from PR977; +it is not a new bit-reversible or dirty-array circuit. + +## Evidence and attribution + +`interval_check.py` uses 192-bit outward-rounded rational enclosures +to check 17 prime-power radices through 32. It checks regularization, +Fourier mass, primitive-character fiber multiplicities, geometric +averages, each pointwise maximum bound before averaging, total averaged +height, and dyadic conversion. A separate exact enclosure at r=4096 +proves that the average bound is false if assigned to every embedding +individually. That negative control uses sin(x)<=x and AM-GM, not a +floating-point sample of a large polynomial. + +`resultants.py` independently compares SymPy polynomial resultants and +Sylvester determinants with PR621's rational field arithmetic for +r=3,4,5,7,8,9. It checks all Galois conjugates and norms, and rejects +the rational-resultant shortcut explicitly at r=5. The retained unit-root +and missing-conjugation controls are replayed in all six cases. + +`budgets.py` checks 752 exact integer budgets, including dyadic orders +through 2^128, the dyadic-conversion polynomial identity and a +rational enclosure of log 2. Those large orders test exponent arithmetic; +no enormous polynomial, array or working word is allocated. No actual +inverse execution at the reduced large-radix precision is claimed. + +The full package additionally rejects eleven packaging/receipt faults +and replays from a read-only relocated copy. The finite checks support +specific identities and failure modes. They do not prove the analytic +theorem for all radices; that is the role of the argument above. + +The kernel is from the pinned OpenAI exact-DFT preprint, with its +classical Newton and q-Pochhammer provenance retained in PR621's +NOTICE. The ideal/resultant/cofactor proof is retained from Ali +Romman's PR621. The partial-inverse precision framework is retained +from Chafik's PR862; the arbitrary-stride solver is Rohan Guliani's +PR846, with the effective-depth argument in Chafik's PR977. Classical +ingredients here are the logarithm Fourier series, finite Fourier +inversion, geometric sums, cyclotomic embeddings, Hadamard's +inequality, and the algebraic norm. A search found related Sudler +product literature, including [Bence Borda, arXiv:2104.06716](https://arxiv.org/abs/2104.06716), but the +finite rational-unit average above is derived in full and does not +rely on an irrational-rotation theorem. No priority claim is made. + +The immutable source objects and notices are retained in `vendor/` and +bound by `SOURCE-PINS.json`. Common-label and bit-reversible compilation, +full-transform normalization and traffic, supplier hosting, and the +multiplication reduction remain open. The new averaged-height estimate +does not discharge those obligations. diff --git a/research/averaged-cyclotomic-height/README.md b/research/averaged-cyclotomic-height/README.md new file mode 100644 index 0000000000..79ea64928a --- /dev/null +++ b/research/averaged-cyclotomic-height/README.md @@ -0,0 +1,56 @@ +# Averaged cyclotomic heights + +For every prime-power radix r>=3, average the coefficient heights across +the cyclotomic embeddings before using the algebraic norm. This improves +the uniform circle-separation exponent from O(r^3) to O(r^2 log^2 r). +The same substitution improves the inherited cyclic-inverse precision +budget. No new kappa is claimed. + +Let ell=ceil(log2 r), n=r-1, D=phi(r). The explicit bound is + + |P(z)| >= 2^-d, |z|=1, + d = 1+2ell+n D min(r,8ell^2). + +It holds at every primitive embedding and every point of the unit circle. +The minimum preserves the prior bound at small radices. For example, +at r=4096 the circle exponent decreases from 34,351,349,785 to +9,661,317,145. These are conservative analytic precision bounds, not +executed word sizes or timing measurements. + +With N=r^2 ell^2, input norm <=2^m and target error 2^-p, the retained +PR977 clean-scratch arbitrary-stride construction has fractional working +precision W<=p+m+60N, integer guard G<=m+26N, and factor-preparation +precision b<=p+m+34N. Its inherited record count is unchanged. The theorem +does not supply a new solver, dirty-array circuit, common-label compiler, +complete transform or multiplication exponent. + +## Replay + +Python 3.11 or later and the pinned SymPy dependency are sufficient: + +```sh +python -m pip install -r research/averaged-cyclotomic-height/requirements.txt +python -I -O -B research/averaged-cyclotomic-height/verify.py +python -I -O -B research/averaged-cyclotomic-height/test_package.py +``` + +The verifier checks the source/manifest binding, 17 rational interval +cases, six independent exact resultants and 752 integer budget rows. +Two explicit mathematical controls reject a rational-resultant shortcut +and misuse of the averaged height as a pointwise estimate. The inherited +unit-root and missing-conjugation controls are also replayed. The package +harness rejects eleven packaging faults and runs a complete read-only +relocation, including the mathematical checks. + +`--out /outside/package/result.json` writes a fresh external receipt after +comparison with `EXPECTED.json.gz`. Existing output files are preserved. +`--write` is an explicit authoring mode that skips the expected-receipt +comparison; it is not a verification result and is not used by CI. +No network or private workspace file is needed after installing the +declared dependency. Compressed receipt equality is defined by the full +decompressed canonical payload. + +[PROOF.md](PROOF.md) contains the complete new derivation and the precise +inherited claims. [NOTICE.md](NOTICE.md) identifies contributors and +classical sources. Finite checks are supporting evidence, not a formal +verification of the full multiplication theorem. diff --git a/research/averaged-cyclotomic-height/SOURCE-PINS.json b/research/averaged-cyclotomic-height/SOURCE-PINS.json new file mode 100644 index 0000000000..e775030c9c --- /dev/null +++ b/research/averaged-cyclotomic-height/SOURCE-PINS.json @@ -0,0 +1,90 @@ +{ + "base_commit": "8bddbee377e2f3ce1f1247196c4b290d55767d20", + "repository": "https://github.com/CrocSwap/integer-mult-bounds", + "sources": [ + { + "git_blob": "0c757c37c70fdeb261d73f111ceedd3b233287bf", + "head": "520774462b19b29af41554b74def31f9d01e997e", + "path": "vendor/pr621/PROOF.md", + "sha256": "2b8056c88e66f692f407450fff0414d41bcd09db8597be22e274a6c3dc20eb9e", + "source_path": "research/prime-power-cyclic-inverse/PROOF.md" + }, + { + "git_blob": "a78e84066711e2f4776152d69d480e9629c26961", + "head": "520774462b19b29af41554b74def31f9d01e997e", + "path": "vendor/pr621/NOTICE.md", + "sha256": "96111c95cfec3c03a6f69c8e02c5d0bceff957d187e638d0534c676d6e3ffd77", + "source_path": "research/prime-power-cyclic-inverse/NOTICE.md" + }, + { + "git_blob": "20a069f42ac2e7102d8b1ddac4f568b83e077074", + "head": "520774462b19b29af41554b74def31f9d01e997e", + "path": "vendor/pr621/verify.py", + "sha256": "40e5e18cbd98d39ba6d0bb036778ccacc077dff009099a54b9c8f441af5d6a56", + "source_path": "research/prime-power-cyclic-inverse/verify.py" + }, + { + "git_blob": "813ffd0304c98c6ea4fea89f021a4247f26f9971", + "head": "520774462b19b29af41554b74def31f9d01e997e", + "path": "vendor/pr621/independent_verify.py", + "sha256": "515d60fbbb28c025251b5a2929231b4b6124dabe357b8526fdb93c1456c847ce", + "source_path": "research/prime-power-cyclic-inverse/independent_verify.py" + }, + { + "git_blob": "fb8fe7cb3bd036c69047ae7b4f4009a51b11825b", + "head": "0768f97d06c623b8211e651543c66135796b62bf", + "path": "vendor/pr628/PROOF.md", + "sha256": "595893609764c64a90d9b21b9cbd6d9e61980703f3deb43361105cf8c3d1d093", + "source_path": "research/prime-power-cyclic-scan/PROOF.md" + }, + { + "git_blob": "22fbeb8ef0a28dd6b3feea718492091319ceb96e", + "head": "0768f97d06c623b8211e651543c66135796b62bf", + "path": "vendor/pr628/NOTICE.md", + "sha256": "abeacf1ad1491d5797cfcf1f3832799bbf3b24b99597229d7bc884059a51ec68", + "source_path": "research/prime-power-cyclic-scan/NOTICE.md" + }, + { + "git_blob": "1182175a55cb871481de0f56ea9ae56e474705fe", + "head": "0768f97d06c623b8211e651543c66135796b62bf", + "path": "vendor/pr628/interval_kernel.py", + "sha256": "9b7bb24640a9a7d3f83c7951dfef483ec933db4c50de6c0130b85f450eeddfbe", + "source_path": "research/prime-power-cyclic-scan/interval_kernel.py" + }, + { + "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" + }, + { + "git_blob": "6019f4d03f2a429c07aae18deba0525d9af36d71", + "head": "2846af720af190cb75b45ebddbb0357dec1121ec", + "path": "vendor/pr977/PROOF.md", + "sha256": "30c296d4f1947cbcaaeb0fe575c36e3c2308f1583dde6029efb4a162fb7a4b27", + "source_path": "research/cyclic-stride-effective-depth/PROOF.md" + }, + { + "git_blob": "57939c758daebf9b7c952ce849ccb169d10c35c6", + "head": "2846af720af190cb75b45ebddbb0357dec1121ec", + "path": "vendor/pr977/NOTICE.md", + "sha256": "b6e1bab630faf7eb4ad0952173dd789a7f5d6333bf938b275bcf087474f4f189", + "source_path": "research/cyclic-stride-effective-depth/NOTICE.md" + }, + { + "git_blob": "61c213dd255e084805cb3ab22fc9ec5d2e947b66", + "head": "2846af720af190cb75b45ebddbb0357dec1121ec", + "path": "vendor/pr977/cubic.py", + "sha256": "7c6cbeedeb77dee4a167fb32b4e14b33f8bd00d69a560d0d2232ecfca7ee59f8", + "source_path": "research/cyclic-stride-effective-depth/cubic.py" + } + ] +} diff --git a/research/averaged-cyclotomic-height/budgets.py b/research/averaged-cyclotomic-height/budgets.py new file mode 100644 index 0000000000..f3976e25d6 --- /dev/null +++ b/research/averaged-cyclotomic-height/budgets.py @@ -0,0 +1,64 @@ +"""Exact integer budget checks for the averaged-height bound.""" +from fractions import Fraction as F +import json +from pathlib import Path + + +def need(ok,label): + if not ok: + raise ValueError(label) + + +def plan(r,phi,p,m): + need(all(type(x) is int for x in (r,phi,p,m)) and r>=3 and 1<=phi<=r and p>=0 and m>=0, + 'budget inputs') + ell,c=(r-1).bit_length(),(r-2).bit_length() + T=(r-1)*phi*min(r,8*ell**2) + d=1+2*ell+T + 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) + b=max((r-1)*ell,e+r+3) + J=c+2*h+3*g+ell+m+5 + W=p+J+2 + G=m+ell+h+g+8 + depth=2*g+(W-1).bit_length()+4 + need(W==p+m+7*T+12*r+18*ell+c+24,'width identity') + need(G==m+3*T+5*r+8*ell+15,'guard identity') + need(b==p+m+4*T+3*r+8*ell+14,'preparation identity') + need(W>=2*g+8 and (4*(depth+1)-1).bit_length()<=W-g,'effective-depth admission') + t_exp=c+h+3+3*g-W + need(t_exp<=-1 and 1+t_exp+ell+h+m+1==-p-2,'common-error contraction') + N=r*r*ell*ell + need(W<=p+m+60*N and G<=m+26*N and b<=p+m+34*N,'quasiquadratic bounds') + need(W<=p+m+9*r**3 and G<=m+6*r**3 and b<=p+m+6*r**3,'retained cubic bounds') + old_T=r*(r-1)*phi + old_W=p+m+7*old_T+12*r+18*ell+c+24 + need(W<=old_W,'budget monotonicity') + return dict(r=r,phi=phi,p=p,m=m,ell=ell,d=d,W=W,G=G,b=b, + previous_W=old_W,saved_bits=old_W-W,effective_depth=depth) + + +def main(): + # 2*atanh(1/3) with a positive geometric tail encloses log 2. + lo=2*sum((F(1,3)**(2*j+1)/(2*j+1) for j in range(20)),F(0)) + hi=lo+2*F(1,3)**41/(41*(1-F(1,9))) + need(F(2,3)=0,'nonnegative square root') + s=i.SCALE + n=isqrt(x.numerator*s*s//x.denominator) + lo=F(n,s) + return lo,lo if lo*lo==x else F(n+1,s) + + +def square(a): + low=0 if a[0]<=0<=a[1] else min(a[0]*a[0],a[1]*a[1]) + return i.hull(low,max(a[0]*a[0],a[1]*a[1])) + + +def modulus(a): + squared=i.add(square(a[0]),square(a[1])) + return sqrt_point(squared[0])[0],sqrt_point(squared[1])[1] + + +def atanh_sum(z): + need(0<=z<=F(1,3),'log series argument') + count=80 + lo=2*sum((z**(2*j+1)/(2*j+1) for j in range(count)),F(0)) + hi=lo+2*z**(2*count+1)/((2*count+1)*(1-z*z)) + return i.hull(lo,hi) + + +LOG2=atanh_sum(F(1,3)) + + +@lru_cache(maxsize=None) +def log_point(x): + x=F(x) + need(x>0,'positive logarithm') + k=x.numerator.bit_length()-x.denominator.bit_length() + y=x/F(2)**k + while y<1: + k-=1 + y*=2 + while y>=2: + k+=1 + y/=2 + lo,hi=atanh_sum((y-1)/(y+1)) + return i.add((lo,hi),i.scale(LOG2,k)) + + +def logarithm(a): + return log_point(a[0])[0],log_point(a[1])[1] + + +def cscale(a,b): + return i.mul(a[0],b),i.mul(a[1],b) + + +def total(values): + out=i.point(0) + for value in values: + out=i.add(out,value) + return out + + +def upper_lt_lower(left,right,label): + need(left[1]averaged[1],'reject treating average as pointwise height') + return dict(r=r,j=j,primitive_power=1,log_height_lower=encoded(lower), + average_height_upper=encoded(averaged),pointwise_average_rejected=True) + + +def main(): + rows=[] + for r in [3,4,5,7,8,9,11,13,16,17,19,23,25,27,29,31,32]: + rows.append(case(r)) + print(r,'PASS rational interval enclosures',flush=True) + result={'status':'PASS_RATIONAL_INTERVAL_CASES','bits':i.BITS, + 'source_sha256':hashlib.sha256(SOURCE.read_bytes()).hexdigest(), + 'scope':__doc__,'cases':rows,'pointwise_negative_control':reject_pointwise_average()} + return result + + +if __name__=='__main__': + main() diff --git a/research/averaged-cyclotomic-height/requirements.txt b/research/averaged-cyclotomic-height/requirements.txt new file mode 100644 index 0000000000..de9542d36e --- /dev/null +++ b/research/averaged-cyclotomic-height/requirements.txt @@ -0,0 +1,2 @@ +sympy==1.14.0 +mpmath==1.3.0 diff --git a/research/averaged-cyclotomic-height/resultants.py b/research/averaged-cyclotomic-height/resultants.py new file mode 100644 index 0000000000..39baa6d1d2 --- /dev/null +++ b/research/averaged-cyclotomic-height/resultants.py @@ -0,0 +1,80 @@ +"""Independent SymPy resultant identities and nonrationality counterexample.""" +import importlib.util +import json +from math import gcd +from pathlib import Path +from sympy import Poly, QQ, Symbol, cyclotomic_poly +from sympy.polys.matrices import DomainMatrix + +HERE=Path(__file__).resolve().parent +SOURCE=HERE/'vendor/pr621/verify.py' +spec=importlib.util.spec_from_file_location('retained_pr621',SOURCE) +original=importlib.util.module_from_spec(spec) +spec.loader.exec_module(original) + + +def need(ok,label): + if not ok: + raise ValueError(label) + + +def case(r): + x,z=Symbol('x'),Symbol('z') + field=QQ.alg_field_from_poly(Poly(cyclotomic_poly(r,x),x),alias='u') + u=field([1,0]) + n=r-1 + def embed(a,k): + result=field.zero + for coefficient in a.to_list(): + result=result*u**(k%r)+field(coefficient) + return result + f=[field.one]*r + for j in range(n-1,-1,-1): + f[j]=f[j+1]*(field.one-u**(j+1)) + need(f[0]==field(r),'kernel constant coefficient') + star=[embed(a,-1) for a in reversed(f)] + fp=Poly.from_list(list(reversed(f)),z,domain=field) + gp=Poly.from_list(list(reversed(star)),z,domain=field) + R=field((-1)**n)*fp.rep.resultant(gp.rep) + matrix=[[field.zero]*(2*n) for _ in range(2*n)] + for poly,start in [(f,0),(star,n)]: + for offset in range(n): + for degree,a in enumerate(poly): + matrix[degree+offset][start+offset]=a + need(DomainMatrix(matrix,(2*n,2*n),field).det()==R,'determinant/resultant sign') + need(R!=field.zero and embed(R,-1)==R,'nonzero real resultant') + norm=field.one + embeddings=[] + for k in range(1,r): + if gcd(k,r)!=1: + continue + value=embed(R,k) + norm*=value + embeddings.append([str(c) for c in value.to_list()]) + need(len(norm.to_list())==1 and norm.to_list()[0].denominator==1,'integer norm') + retained=original.case(r,1) + encoded=[str(c) for c in reversed(R.to_list())] + encoded+=['0']*(field.mod.degree()-len(encoded)) + need(encoded==retained['resultant'],'independent exact field agreement') + need(str(norm.to_list()[0])==retained['resultant_norm'],'independent norm agreement') + if r==5: + need(R!=embed(R,2) and len(R.to_list())>1,'reject rational-resultant shortcut') + need(encoded==['98873','0','17859','17859'],'radix-five counterexample') + return dict(r=r,resultant_ascending=encoded,norm=str(norm.to_list()[0]), + embeddings_descending=embeddings,independent_field_agreement=True, + rational_resultant=(len(R.to_list())==1), + inherited_unit_root_control=retained['unit_root_negative_control'], + inherited_missing_conjugation_control=retained['missing_conjugation_negative_control']) + + +def main(): + rows=[] + for r in [3,4,5,7,8,9]: + rows.append(case(r)) + print(r,'PASS independent exact resultant',flush=True) + result={'status':'PASS_INDEPENDENT_EXACT_RESULTANTS','scope':__doc__,'cases':rows} + return result + + +if __name__=='__main__': + main() diff --git a/research/averaged-cyclotomic-height/test_package.py b/research/averaged-cyclotomic-height/test_package.py new file mode 100644 index 0000000000..5ec69c834a --- /dev/null +++ b/research/averaged-cyclotomic-height/test_package.py @@ -0,0 +1,127 @@ +"""Fail-closed package controls and a full read-only optimized relocation.""" +import argparse +import gzip +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +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 run(root, *args, code=None): + command = [sys.executable, '-I', '-O', '-B'] + command += ['-c', code] if code is not None else [str(root/'verify.py'), *map(str, args)] + return subprocess.run(command, cwd=root.parent, text=True, stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, timeout=2400) + + +def rebind(root, name): + path = root/'MANIFEST.json' + record = json.loads(path.read_text()) + record['files'][name] = hashlib.sha256((root/name).read_bytes()).hexdigest() + path.write_text(json.dumps(record, indent=2, sort_keys=True)+'\n') + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--out', type=Path) + args = parser.parse_args() + if args.out: + require(not args.out.exists() and not args.out.resolve().is_relative_to(P), 'fresh external report') + results = [] + with tempfile.TemporaryDirectory(prefix='averaged height package controls ') as temporary: + base = Path(temporary) + def copy(name): + root = Path(shutil.copytree(P, base/name)) + # The supplied package may itself be read-only. Only these + # disposable test fixtures must permit deliberate corruption. + root.chmod(0o755) + for path in root.rglob('*'): + path.chmod(0o755 if path.is_dir() else 0o644) + return root + def rejection(name, mutate, *, full=False, code=None): + root = copy(name) + mutate(root) + output = base/(name+' output.json') + result = run(root, '--out', output, code=code(root) if code else None) if full or code else run(root, '--bindings-only') + require(result.returncode != 0, 'mutation accepted: '+name) + require(not output.exists(), 'failed verification wrote a receipt: '+name) + results.append(dict(name=name, rejected=True, terminal=result.stdout.strip().splitlines()[-1])) + print('PASS package control', name, flush=True) + + rejection('missing manifest', lambda root: (root/'MANIFEST.json').unlink()) + rejection('altered implementation', lambda root: (root/'budgets.py').write_text((root/'budgets.py').read_text()+'\n# altered\n')) + rejection('extra file', lambda root: (root/'undeclared.txt').write_text('unbound\n')) + rejection('missing source', lambda root: (root/'vendor/pr621/PROOF.md').unlink()) + def wrong_source(root): + file = root/'vendor/pr621/PROOF.md' + file.write_text(file.read_text()+'\nchanged\n') + rebind(root, 'vendor/pr621/PROOF.md') + rejection('source hash independent of manifest', wrong_source) + def wrong_blob(root): + file = root/'SOURCE-PINS.json' + value = json.loads(file.read_text()) + value['sources'][0]['git_blob'] = '0'*40 + file.write_text(json.dumps(value)+'\n') + rebind(root, 'SOURCE-PINS.json') + rejection('source Git object independent of manifest', wrong_blob) + rejection('duplicate manifest key', lambda root: (root/'MANIFEST.json').write_text('{"files":{},"files":{}}\n')) + rejection('symlink injection', lambda root: (root/'linked.txt').symlink_to(root/'README.md')) + rejection('preloaded module substitution', lambda root: None, code=lambda root: + "import sys,types,runpy; m=types.ModuleType('budgets'); m.__file__='/not/the/package.py'; " + "sys.modules['budgets']=m; sys.argv=["+repr(str(root/'verify.py'))+"] ; runpy.run_path(sys.argv[0],run_name='__main__')") + def wrong_receipt(root): + file = root/'EXPECTED.json.gz' + value = json.loads(gzip.decompress(file.read_bytes())) + require(value['budgets']['rows'][0]['p'] == 0, 'known zero budget field') + value['budgets']['rows'][0]['p'] = False + file.write_bytes(gzip.compress((json.dumps(value, indent=2, sort_keys=True)+'\n').encode(), mtime=0)) + rebind(root, 'EXPECTED.json.gz') + rejection('false receipt boolean integer confusion', wrong_receipt, full=True) + + root = copy('existing output') + existing = base/'existing.json' + existing.write_bytes(b'preserve this exact output\n') + result = run(root, '--out', existing) + require(result.returncode != 0 and existing.read_bytes() == b'preserve this exact output\n', 'existing output preservation') + results.append(dict(name='existing output preserved', rejected=True)) + print('PASS package control existing output preserved', flush=True) + + root = copy('read only isolated relocation') + for file in root.rglob('*'): + file.chmod(0o555 if file.is_dir() else 0o444) + root.chmod(0o555) + output = base/'relocated receipt.json' + try: + result = run(root, '--out', output) + require(result.returncode == 0, 'full relocated replay failed: '+result.stdout[-2000:]) + require(output.read_bytes() == gzip.decompress((P/'EXPECTED.json.gz').read_bytes()), 'relocated receipt byte equality') + require(run(root, '--bindings-only').returncode == 0, 'read-only package unchanged after replay') + finally: + root.chmod(0o755) + for directory in root.rglob('*'): + if directory.is_dir(): + directory.chmod(0o755) + results.append(dict(name='full read-only isolated optimized relocation', passed=True, + receipt_sha256=hashlib.sha256(output.read_bytes()).hexdigest())) + print('PASS full read-only isolated optimized relocation', flush=True) + report = dict(status='PASS_AVERAGED_HEIGHT_PACKAGE', controls=results, rejected=11, full_readonly_replay=True) + if args.out: + with args.out.open('x') as handle: + handle.write(json.dumps(report, indent=2, sort_keys=True)+'\n') + print('PASS_AVERAGED_HEIGHT_PACKAGE rejected=11 full_readonly_replay=True') + + +if __name__ == '__main__': + main() diff --git a/research/averaged-cyclotomic-height/vendor/pr621/NOTICE.md b/research/averaged-cyclotomic-height/vendor/pr621/NOTICE.md new file mode 100644 index 0000000000..a78e840667 --- /dev/null +++ b/research/averaged-cyclotomic-height/vendor/pr621/NOTICE.md @@ -0,0 +1,21 @@ +# Attribution and assistance + +The kernel definition comes from the OpenAI exact-DFT preprint at +`adc7f1241b42e322a6451854ab7e4b4c146bf78a`, at `loc:newton` and +`loc:fourier-factorization`. Its source has the Apache-2.0 license. +The Newton and q-Pochhammer Fourier factorization is classical; see +Alexey Kuznetsov, [Using q-calculus to study LDLT factorization of a +certain Vandermonde matrix](https://arxiv.org/abs/1507.02959v2). +This source is not presented as a proof of the cyclic conditioning result. + +The proof extends prior unpublished local cyclic inverse and stability +notes from research directed by Ali Romman. The rational field routines +use that work's exact-arithmetic scaffold. The full proof is included +here; no private file is needed for replay. No literature priority is claimed. + +The proof, verifier, and package were prepared with substantial OpenAI +Codex assistance. Separate Codex agents reviewed the proof and checked +it with independent SymPy arithmetic. These are AI-assisted reviews, +not maintainer acceptance or a full Lean multiplication proof. + +This contribution uses the repository's Apache-2.0 license. diff --git a/research/averaged-cyclotomic-height/vendor/pr621/PROOF.md b/research/averaged-cyclotomic-height/vendor/pr621/PROOF.md new file mode 100644 index 0000000000..0c757c37c7 --- /dev/null +++ b/research/averaged-cyclotomic-height/vendor/pr621/PROOF.md @@ -0,0 +1,212 @@ +# Uniform bounds for the prime-power cyclic inverse + +## Result and scope + +Let r=ell^a>=3, where ell is prime and a>=1. Let u be a primitive +r-th root of unity, and put n=r-1 and D=phi(r). Define + + h_j = 1 / product_(s=1)^j (1-u^s), + P(z) = sum_(j=0)^n h_j z^j, + f(z) = r P(z). + +For every such r and u, P has no zero on the complex unit circle. +Put H=2^r-1 and delta_r=1/(2rn H^(nD-1)). For every complex +z with |z|=1, + + |P(z)| >= delta_r. + +This bound does not depend on the order of z. In particular, it holds +at all eigenvalues of a cyclic shift of any length. The old bound from +the algebraic norm of P at a root of unity depends on that root's order. +The new bound removes that dependence. + +There is also an operator bound that does not require root +classification. For any complex scalar tau with |tau|=1, +any cyclic shift Z_L with L>=1, and any integer w, put U=tau Z_L^w. Then + + ||P(U)^-1||_infinity <= delta_r^-1 + 2nH/(r delta_r^2). + +The bound has logarithm O(r^2 phi(r)), hence O(r^3). It is uniform +in L, w, and tau. The induced infinity norm is the maximum absolute +row sum. This bound does not supply a complete O(p polylog p) guard +for growing radix families. Efficient coefficient preparation, rounded +execution, scratch restoration, and a fast fixed-tape circuit remain open. No integer +kappa, complex b, or BIT c changes in this result. + +For an odd prime q, D=n=q-1, so the circle bound becomes + + delta_q = 1/(2q(q-1) (2^q-1)^((q-1)^2-1)). + +The result includes dyadic r>=4. For r=2, P(z)=1+z/2; the geometric +series gives ||P(U)^-1||_infinity<=2. No result for other composite +radices is claimed. The ideal argument below requires a prime power. + +## Integral polynomial and unit roots + +The identity product_(s=1)^(r-1)(1-u^s)=r gives + + f(z) = sum_(j=0)^n a_j z^j, + a_j = product_(s=j+1)^n (1-u^s). + +All a_j are algebraic integers in K=Q(u), and a_n=1. Thus f is +monic. Every root of f is an algebraic integer. + +Take any root alpha and a number field E that contains K and alpha. +The algebraic integer 1-u is not a unit in E, since + + |Norm_(E/Q)(1-u)| = ell^[E:K] > 1. + +Here Norm_(K/Q)(1-u)=Phi_r(1)=ell. The prime-power cyclotomic +polynomial is Phi_r(x)=sum_(j=0)^(ell-1) x^(j r/ell). + +There is a maximal ideal m in the ring of integers of E that contains +1-u. Modulo m, all a_j with j=3, the two embeddings are distinct. Bound the other +D-2 factors by H^(2n). This gives + + 1 <= |Norm_(K/Q)(R)| <= |R|^2 H^(2n(D-2)), + |R| >= H^(-n(D-2)). + +The equation S adj(S) e_0 = R e_0 gives polynomials A and C of +degree below n with + + A(z) f(z) + C(z) f*(z) = R. + +Each coefficient of A and C is a cofactor of S. A cofactor is a +determinant of size 2n-1. Deleting a row and a column cannot +increase the Euclidean norm of any retained column. Therefore each +cofactor has modulus at most H^(2n-1). For |z|=1, + + |A(z)| + |C(z)| <= 2n H^(2n-1), + |f*(z)| = |f(z)|. + +The Bezout identity gives + + |f(z)| >= H^(-n(D-2)) / (2n H^(2n-1)) + = 1 / (2n H^(nD-1)). + +Divide by r to obtain the stated bound for P. Neither this proof +nor its constants use the degree of a root of unity at which P is +evaluated. + +## An inverse bound from Fourier coefficients + +Let g(t)=1/P(exp(it)). The circle bound gives |g(t)|<=delta_r^-1. +The coefficient bound gives + + |P'(exp(it))| <= nH/r, + |g'(t)| <= nH/(r delta_r^2). + +Let c_k be the Fourier coefficients of g, with the average integral +on [0,2 pi] as the normalization. Parseval's identity for g' gives + + sum_k k^2 |c_k|^2 <= (nH/(r delta_r^2))^2. + +The estimate sum_(k!=0) k^-2 <= 4 follows from comparison of the +positive tail with the integral of x^-2 on [1,infinity). By the +Cauchy-Schwarz inequality and |c_0|<=delta_r^-1, + + sum_k |c_k| <= delta_r^-1 + 2nH/(r delta_r^2). + +Thus the Fourier series is absolutely convergent. Its product with +the finite polynomial P(exp(it)) has Fourier coefficients equal to +those of the constant one. For U=tau Z_L^w, every integer power U^k +has infinity norm one. The absolutely convergent matrix series + + sum_(k in Z) c_k U^k + +therefore has norm at most sum_k |c_k|. Multiplication by P(U) gives +the identity matrix, by the same coefficient identities. This proves +the stated inverse bound for all L, w, and unit tau. + +This is a bound for the exact operator. It is not a paid +coefficient-preparation or rounded-program theorem. The infinite +series is used to prove the norm bound, not as a declared algorithm. + +## Products and unit gauges + +For a finite family of such kernels with r_i>=3 on the same cyclic array, put + + C = product_i P_i(tau_i Z_L^(w_i)). + +Each factor is invertible. Submultiplicativity gives + + ||C^-1||_infinity <= product_i [delta_i^-1 + 2n_i H_i/(r_i delta_i^2)]. + +A diagonal conjugation with entries of modulus one preserves this +norm. Thus this bound also applies to a unit-gauged product. Its +logarithm is O(sum_i r_i^2 phi(r_i)). The bound concerns arbitrary +input vectors. It does not give operation counts or a tape schedule. + +## Value, sources, and remaining work + +This result permits inner roots and proves a uniform circle bound for +every primitive root choice. It supplies an explicit all-length inverse +bound for each growing prime-power radix. For an odd prime q and a root of unity xi, a direct algebraic norm +argument in E=Q(u,xi) gives + + |P_q(xi)| >= q^-1 (2^q-1)^(-([E:Q]-1)). + +The degree of E can grow with the order of xi. The new bound uses +Q(u) only and controls every point on the unit circle. The logarithm +of its inverse upper bound still grows polynomially with r. It does +not establish the required combined precision guard or change the +full-array traffic of the literal filter chain. A sharper lower bound +and a paid implementation remain useful next questions. + +The polynomial is from the pinned OpenAI exact-DFT preprint: + +https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-explicit-power-saving-for-the-exact-discrete-Fourier-transform-September-25-2026/build/sections/local.tex + +The unit-ideal argument extends the prior unpublished local note +"Cyclic polynomial stability, norm growth, and rescaling". The prior +local note "Full-output cyclic quotient: exact structure and cost" +supplies the cyclic inverse context. The field arithmetic in the +finite verifier uses the prior local exact-arithmetic scaffold. +The resultant and cofactor estimates use standard algebraic and +linear-algebra facts. Repository and literature novelty checks are +separate from this proof. No priority claim is made here. + +Prepared with OpenAI Codex assistance. Apache-2.0. diff --git a/research/averaged-cyclotomic-height/vendor/pr621/independent_verify.py b/research/averaged-cyclotomic-height/vendor/pr621/independent_verify.py new file mode 100644 index 0000000000..813ffd0304 --- /dev/null +++ b/research/averaged-cyclotomic-height/vendor/pr621/independent_verify.py @@ -0,0 +1,141 @@ +#!/usr/bin/env python3 +"""Check the cyclotomic identities with independent SymPy arithmetic.""" + +import argparse +import json +from math import gcd +from pathlib import Path +from sympy import Poly, QQ, Symbol, cyclotomic_poly +from sympy.polys.matrices import DomainMatrix + + +def require(condition): + if not condition: + raise ValueError('Exact identity check failed') + + +def check(q, power): + x, z = (Symbol('x'), Symbol('z')) + field = QQ.alg_field_from_poly(Poly(cyclotomic_poly(q, x), x), alias='u') + u = field([1, 0]) + n = q - 1 + residue_prime = int(cyclotomic_poly(q, x).subs(x, 1)) + require(residue_prime >= 2) + + def embed(value, exponent): + result = field.zero + root = u ** (exponent % q) + for coefficient in value.to_list(): + result = result * root + field(coefficient) + return result + + def encode(value): + return [str(coefficient) for coefficient in value.to_list()] + + prefix = field.one + f = [] + for j in range(q): + if j: + prefix *= field.one - u ** (power * j % q) + f.append(field(q) / prefix) + require(f[0] == field(q) and f[-1] == field.one) + for j in range(q): + product = field.one + for s in range(j + 1, q): + product *= field.one - u ** (power * s % q) + require(f[j] == product) + coefficients = f[j].to_list() + require(all((coefficient.denominator == 1 for coefficient in coefficients))) + require(int(sum(coefficients)) % residue_prime == (1 if j == n else 0)) + star = [embed(value, -1) for value in reversed(f)] + matrix = [[field.zero] * (2 * n) for _ in range(2 * n)] + for polynomial, start in ((f, 0), (star, n)): + for offset in range(n): + for degree, coefficient in enumerate(polynomial): + matrix[degree + offset][start + offset] = coefficient + dm = DomainMatrix(matrix, (2 * n, 2 * n), field) + determinant = dm.det() + require(determinant != field.zero) + require(embed(determinant, -1) == determinant) + require(all(coefficient.denominator == 1 + for coefficient in determinant.to_list())) + require(int(sum(determinant.to_list())) % residue_prime + == (-1) ** n % residue_prime) + inverse = dm.inv().to_list() + cofactor_column = [row[0] * determinant for row in inverse] + require(all(coefficient.denominator == 1 + for value in cofactor_column for coefficient in value.to_list())) + for row, values in enumerate(matrix): + actual = sum((value * cofactor for value, cofactor in + zip(values, cofactor_column)), field.zero) + require(actual == (determinant if row == 0 else field.zero)) + real_norm = field.one + for exponent in range(1, q // 2 + 1): + if gcd(exponent, q) == 1: + real_norm *= embed(determinant, exponent) + require(len(real_norm.to_list()) == 1) + require(real_norm.to_list()[0].denominator == 1) + require(real_norm != field.zero) + full_norm = field.one + for exponent in range(1, q): + if gcd(exponent, q) == 1: + full_norm *= embed(determinant, exponent) + require(full_norm == real_norm * real_norm) + fp = Poly.from_list(list(reversed(f)), z, domain=field) + gp = Poly.from_list(list(reversed(star)), z, domain=field) + require(fp.gcd(gp).degree() == 0) + require(fp.rep.resultant(gp.rep) == field((-1) ** n) * determinant) + inverse_checks = [] + pp = fp.quo_ground(q) + for length in (1, 2, 4, 8): + modulus = Poly(z ** length - 1, z, domain=field) + reciprocal = pp.invert(modulus) + require((pp * reciprocal).rem(modulus) == Poly(1, z, domain=field)) + inverse_checks.append(length) + unit = Poly(z ** n - 1, z, domain=field) + unit_star = -unit + require(unit.resultant(unit_star) == 0) + missing_conjugation = Poly.from_list(f, z, domain=field) + bad = False + for exponent in range(q): + point = u ** exponent + v = fp.rep.eval(point) + r = missing_conjugation.rep.eval(point) + if v * embed(v, -1) != r * embed(r, -1): + bad = True + break + require(bad) + return { + 'order': q, + 'residue_prime': residue_prime, + 'field_degree': int(field.mod.degree()), + 'primitive_power': power, + 'coefficient_order': 'descending powers of u', + 'resultant': encode(determinant), + 'real_subfield_norm': encode(real_norm)[0], + 'full_field_norm': encode(full_norm)[0], + 'cofactor_identity': True, + 'primitive_ideal_reduction': 'f=z^(order-1), determinant=(-1)^(order-1)', + 'exact_cyclic_inverse_lengths': inverse_checks, + 'unit_root_negative_control': 'zero resultant', + 'missing_conjugation_negative_control': 'different exact squared modulus', + } + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--output', type=Path) + args = parser.parse_args() + cases = [check(radix, power) for radix, power in + ((3, 1), (4, 1), (5, 2), (7, 1), (8, 1), (8, 3), + (9, 1), (11, 1), (11, 4))] + result = { + 'status': 'PASS', + 'scope': 'Exact finite identities. The written proof supplies the uniform theorem.', + 'cases': cases, + } + payload = json.dumps(result, indent=2) + '\n' + if args.output is None: + print(payload, end='') + else: + args.output.write_text(payload) diff --git a/research/averaged-cyclotomic-height/vendor/pr621/verify.py b/research/averaged-cyclotomic-height/vendor/pr621/verify.py new file mode 100644 index 0000000000..20a069f42a --- /dev/null +++ b/research/averaged-cyclotomic-height/vendor/pr621/verify.py @@ -0,0 +1,229 @@ +#!/usr/bin/env python3 +"""Check exact polynomial and resultant identities for prime-power inputs.""" + +from fractions import Fraction as F +from pathlib import Path +import argparse +import json +from math import gcd + + +def require(condition): + if not condition: + raise ValueError("Exact identity check failed") + + +def trim(a): + while len(a) > 1 and a[-1] == 0: + a.pop() + return a + + +def subtract(a, b): + c = [F(0)] * max(len(a), len(b)) + for j, x in enumerate(a): + c[j] += x + for j, x in enumerate(b): + c[j] -= x + return trim(c) + + +def multiply(a, b): + c = [F(0)] * (len(a) + len(b) - 1) + for i, x in enumerate(a): + for j, y in enumerate(b): + c[i + j] += x * y + return trim(c) + + +def divide(a, b): + a = trim(list(a)) + c = [F(0)] * max(1, len(a) - len(b) + 1) + while a != [0] and len(a) >= len(b): + k, x = len(a) - len(b), a[-1] / b[-1] + c[k] += x + for j, y in enumerate(b): + a[k + j] -= x * y + trim(a) + return trim(c), a + + +class Field: + def __init__(self, r): + p = next(j for j in range(2, r + 1) if r % j == 0) + remainder = r + while remainder % p == 0: + remainder //= p + require(r >= 3 and remainder == 1) + step = r // p + self.q, self.n, self.prime = r, (p - 1) * step, p + self.modulus = [F(0)] * (self.n + 1) + for j in range(p): + self.modulus[j * step] = F(1) + self.zero = (F(0),) * self.n + self.one = (F(1),) + (F(0),) * (self.n - 1) + + def reduce(self, a): + a = divide(a, self.modulus)[1] + return tuple(a + [F(0)] * (self.n - len(a))) + + def root(self, j): + return self.reduce([F(0)] * (j % self.q) + [F(1)]) + + def add(self, a, b): + return tuple(x + y for x, y in zip(a, b)) + + def sub(self, a, b): + return tuple(x - y for x, y in zip(a, b)) + + def scale(self, a, x): + return tuple(y * x for y in a) + + def mul(self, a, b): + return self.reduce(multiply(a, b)) + + def inv(self, a): + require(a != self.zero) + r0, r1, s0, s1 = self.modulus, trim(list(a)), [F(0)], [F(1)] + while r1 != [0]: + c, r = divide(r0, r1) + r0, r1 = r1, r + s0, s1 = s1, subtract(s0, multiply(c, s1)) + require(len(r0) == 1 and r0[0] != 0) + return self.reduce([x / r0[0] for x in s0]) + + def embed(self, a, power): + out = self.zero + for j, x in enumerate(a): + out = self.add(out, self.scale(self.root(power * j), x)) + return out + + def conjugate(self, a): + return self.embed(a, -1) + + +def poly_product(k, a, b): + out = [k.zero] * (len(a) + len(b) - 1) + for i, x in enumerate(a): + for j, y in enumerate(b): + out[i + j] = k.add(out[i + j], k.mul(x, y)) + return out + + +def evaluate(k, a, z): + out = k.zero + for x in reversed(a): + out = k.add(k.mul(out, z), x) + return out + + +def sylvester(k, a, b): + n = len(a) - 1 + require(len(b) == n + 1) + out = [[k.zero for _ in range(2 * n)] for _ in range(2 * n)] + for offset, polynomial in ((0, a), (n, b)): + for j in range(n): + for i, x in enumerate(polynomial): + out[i + j][j + offset] = x + return out + + +def eliminate(k, matrix, boundary=None): + a = [list(row) for row in matrix] + b = list(boundary) if boundary is not None else None + determinant = k.one + for col in range(len(a)): + pivot = next((j for j in range(col, len(a)) if a[j][col] != k.zero), None) + if pivot is None: + return k.zero, None + if pivot != col: + a[col], a[pivot] = a[pivot], a[col] + if b is not None: + b[col], b[pivot] = b[pivot], b[col] + determinant = k.scale(determinant, -1) + value = a[col][col] + determinant = k.mul(determinant, value) + reciprocal = k.inv(value) + for j in range(col, len(a)): + a[col][j] = k.mul(a[col][j], reciprocal) + if b is not None: + b[col] = k.mul(b[col], reciprocal) + for row in range(len(a)): + if row == col: + continue + value = a[row][col] + for j in range(col, len(a)): + a[row][j] = k.sub(a[row][j], k.mul(value, a[col][j])) + if b is not None: + b[row] = k.sub(b[row], k.mul(value, b[col])) + return determinant, b + + +def case(r, power): + k, n = Field(r), r - 1 + require(gcd(r, power) == 1) + tail = [k.zero] * r + tail[-1] = k.one + for j in range(n - 1, -1, -1): + tail[j] = k.mul(tail[j + 1], k.sub(k.one, k.root(power * (j + 1)))) + require(tail[0] == k.scale(k.one, r)) + kernel = [k.one] + for j in range(1, r): + kernel.append(k.mul(kernel[-1], k.inv(k.sub(k.one, k.root(power * j))))) + require(tail == [k.scale(x, r) for x in kernel]) + for j in range(r): + require(all(x.denominator == 1 for x in tail[j])) + require(sum(tail[j]) % k.prime == (1 if j == n else 0)) + star = [k.conjugate(x) for x in reversed(tail)] + require([k.conjugate(x) for x in reversed(star)] == tail) + for j in range(r): + require(sum(star[j]) % k.prime == (1 if j == 0 else 0)) + matrix = sylvester(k, tail, star) + boundary = [k.one] + [k.zero] * (2 * n - 1) + resultant, solution = eliminate(k, matrix, boundary) + require(resultant != k.zero) + require(all(x.denominator == 1 for x in resultant)) + residue = (-1) ** n % k.prime + require(sum(resultant) % k.prime == residue) + a, b = solution[:n], solution[n:] + af, bs = poly_product(k, a, tail), poly_product(k, b, star) + require([k.add(x, y) for x, y in zip(af, bs)] == boundary) + norm = k.one + for embedding in range(1, r): + if gcd(embedding, r) == 1: + norm = k.mul(norm, k.embed(resultant, embedding)) + require(all(x == 0 for x in norm[1:]) and norm[0].denominator == 1 and norm[0] != 0) + for j in range(r): + value, reverse = evaluate(k, tail, k.root(j)), evaluate(k, star, k.root(j)) + require(k.mul(value, k.conjugate(value)) == k.mul(reverse, k.conjugate(reverse))) + unit = [k.scale(k.one, -1)] + [k.zero] * (n - 1) + [k.one] + unit_star = [k.conjugate(x) for x in reversed(unit)] + require(eliminate(k, sylvester(k, unit, unit_star))[0] == k.zero) + bad_star = list(reversed(tail)) + require(any(k.mul(evaluate(k, tail, k.root(j)), k.conjugate(evaluate(k, tail, k.root(j)))) != + k.mul(evaluate(k, bad_star, k.root(j)), k.conjugate(evaluate(k, bad_star, k.root(j)))) + for j in range(r))) + return {"radix": r, "prime": k.prime, "field_degree": k.n, + "polynomial_degree": n, "primitive_power": power, + "resultant": [str(x) for x in resultant], "resultant_norm": str(norm[0]), + "bezout_identity": True, "mod_ideal_resultant": residue, + "unit_root_negative_control": "singular", + "missing_conjugation_negative_control": "rejected", + "circle_bound_base": 2 ** r - 1, + "circle_bound_exponent": n * k.n - 1, + "circle_bound_denominator": 2 * r * n} + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path) + args = parser.parse_args() + cases = [case(r, power) for r, power in + ((3, 1), (4, 1), (5, 2), (7, 1), (8, 1), (9, 1), (11, 1), (11, 4))] + result = {"status": "PASS", "cases": cases, + "scope": "Exact finite identities. The written proof supplies the uniform theorem."} + payload = json.dumps(result, indent=2) + "\n" + if args.output is None: + print(payload, end="") + else: + args.output.write_text(payload) diff --git a/research/averaged-cyclotomic-height/vendor/pr628/NOTICE.md b/research/averaged-cyclotomic-height/vendor/pr628/NOTICE.md new file mode 100644 index 0000000000..22fbeb8ef0 --- /dev/null +++ b/research/averaged-cyclotomic-height/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/averaged-cyclotomic-height/vendor/pr628/PROOF.md b/research/averaged-cyclotomic-height/vendor/pr628/PROOF.md new file mode 100644 index 0000000000..fb8fe7cb3b --- /dev/null +++ b/research/averaged-cyclotomic-height/vendor/pr628/PROOF.md @@ -0,0 +1,269 @@ +# Uniform preparation and rounded inversion of a neighboring cyclic kernel + +This note combines PR621's circle lower bound, standard approximate +factorization, and the local two-scan rounding lemma. It concerns a +neighboring cyclic shift with gauge 1 and clean input/output work arrays. +It is not a complete multiplication algorithm, reversible word, arbitrary +stride tape schedule, or new kappa result. The proof uses the cited +factorization theorem; the accompanying numerical nomination program does +not implement that theorem's worst-case algorithm. + +## Statement and model + +Let r>=3 be a prime power, k coprime to r, zeta=exp(2 pi i k/r), and + + P(z)=sum_(j=0)^(r-1) h_j z^j, + h_j=1/product_(s=1)^j(1-zeta^s). + +Let S be either neighboring cyclic shift on L>=1 entries. Given p>=1 +and an exactly supplied dyadic complex vector x with ||x||infinity<=1, +there is an algorithm producing y with + + ||y-P(S)^-1 x||infinity <= 2^-p. + +Coefficient preparation is independent of L. Both the required coefficient +bit lengths and the execution precision are O(p+r^4), including magnitude +bits. The array execution uses O(rL) rounded scalar operations and O(r) +sequential full-array passes. With ordinary near-linear integer arithmetic, +including a conservative exact coefficient-product verification in setup, +the bit-operation bound is + + soft-O((Lr+r^3)(p+r^4)). + +Here soft-O suppresses logarithms in the displayed parameters. Input +fractional precision is assumed at most the execution budget below; +longer exact inputs require their reading/rounding cost and a separately +charged input-error budget. Clean arrays and standard arithmetic scratch +are allowed. The scan layout is sequential for S=Z or Z^-1; this statement +does not assert that an arbitrary modular-stride permutation is free. +The setup bound uses the bit-complexity model of the cited factorization +result. A concrete fixed-tape implementation of its setup is not supplied. + +## Explicit budgets + +Put n=r-1, D=phi(r), ell=ceil(log2 r), and + + d=1+2 ell+r n D, + g=d+ell+2r+2, beta=2^-g, + a=ell+n g, Abar=2^a, + e=max(d+1, a+1, p+2a+3), epsilon=2^-e, + b=max(n ell, e+r+3), + w=max(2g+ceil(log2(14n)), + p+(n+2)g+ceil(log2(28n(r+1)))), u=2^-w. + +All these are computable integer budgets. Their sizes satisfy +d,g=O(r^3) and a,e,b,w=O(p+r^4). No array length occurs in them. +The executable budget checker verifies the integer inequalities used below +for a range of radices and precisions; the algebra proves them generally. + +## Approximate factorization and preparation + +Define f=rP. Its leading coefficient is 1 and its coefficients are + + f_j=product_(s=j+1)^(r-1)(1-zeta^s). + +Thus ||f||_1<=H=2^r-1, and Cauchy's bound places all roots inside +|z|<=1+H<2^(r+1). Its logarithmic root bound is O(r). + +Pan's approximate-factorization theorem, in Theorem 2 and Corollary 1 of +Mehlhorn, Sagraloff and Wang [1], provides dyadics rho_1,...,rho_n with +||f-product_j(z-rho_j)||_1<=2^-b ||f||_1. Its factorization cost is +soft-O(n b+n^2 Gamma), with coefficient-oracle precision O(b+n Gamma), +where Gamma bounds the logarithmic root magnitudes. Repeated roots do not +require a distinct-root count for this factorization step. + +Let Q=(1/r) product_j(z-rho_j). Our choice b>=e+r+3 gives + + ||P-Q||_1 < epsilon/8. + +Only this coefficient error is needed. We do not isolate the true roots, +match approximate roots to true roots, or require simple roots. + +The coefficient oracle is also charged. Compute zeta to the requested +precision, its first r powers, and the backward products defining f_j. +There are O(r) complex operations. Products have magnitude at most 2^r; +guarding by O(r+log r) bits bounds coefficient errors. Fast elementary +function evaluation [2] supplies the required pi, sine and cosine values +with near-linear precision cost up to logarithms. Hence the oracle fits +soft-O(r(p+r^4)). This is an algorithmic preparation argument, not a +complexity claim about the Fraction/Decimal reference scripts. + +An independent certificate can expand the dyadic-root product exactly and +compare it with rigorous coefficient enclosures of total componentwise +error at most epsilon/8. Replacing complex moduli by the sum of absolute +real and imaginary parts costs at most a factor of 2, so the resulting +upper bound is still below epsilon. Exact expansion +of n B-bit roots has O(nB)-bit coefficients; a simple iterative expansion +costs soft-O(n^3 B) bit operations, B=O(p+r^4). This conservative setup +cost is included in the theorem. Faster expansion is unnecessary here. + +## Stability without individual root certification + +PR621 gives |P(z)|>=delta on |z|=1, where + + delta=1/[2rn H^(nD-1)] >= 2^-d. + +The coefficient certificate and e>=d+1 imply |Q(z)|>=delta/2 on the +unit circle. Also ||Q||_1<=H/r+epsilon<=H/r+1<=2^r. + +For any root rho of Q at radial distance t=||rho|-1|<1/2, integrate Q' +along the radial segment to the unit circle. On that segment |z|<2, so + + delta/2 <= t n 2^r 2^(n-1). + +Roots farther than 1/2 already have a fixed gap. Therefore every root of +Q lies at radial distance at least + + eta=min(1/2, delta/[2n 2^r 2^(n-1)]). + +Our g ensures beta<=eta/2. If |rho|>1, b_rho=1/rho has modulus at most +1-beta. If |rho|<1, b_rho=rho has modulus at most 1-beta. These comparisons +can be made exactly on the dyadic rho. Inverting an outer rho produces +an exact rational complex coefficient with O(p+r^4) numerator and +denominator bits; it need not be rounded to a dyadic. + +For each factor, + + (S-rho I)^-1 = -rho^-1 (I-rho^-1 S)^-1 if |rho|>1, + (S-rho I)^-1 = (I-rho S^-1)^-1 S^-1 if |rho|<1. + +Each stable inverse has norm at most beta^-1. Outer scalar factors have +modulus less than 1, while the inner shift has norm 1. Apply the scalar r +to the input first. Exact stage-j values have norm at most r beta^-j. +In particular, ||Q(S)^-1||<=r beta^-n<=Abar, uniformly in L. + +Since epsilon Abar<=1/2, a Neumann perturbation bound gives + + ||P(S)^-1-Q(S)^-1|| + <= Abar^2 epsilon/(1-Abar epsilon) + <= 2 Abar^2 epsilon <= 2^(-p-2). + +This is an operator bound for arbitrary input vectors, not just samples +or a particular Fourier mode. + +## Rounded execution + +Use the two-scan periodic first-order procedure proved in +SCAN-PROOF.md, with grid u and exact rational coefficients. +An inner factor scans in the opposite direction and includes the unit +cyclic shift. An outer factor includes a final rounded multiplication by +-rho^-1. The per-factor error is bounded by + + 7(B+1)u/beta^3 + +for input norm B. The constant 7 includes the outer scalar multiplication; +the original scan constant is 6. Copying and shifting dyadic entries is +exact. Multiplying the original dyadic input by integer r is exact. + +If E_j is the error after j factors, then E_0=0 and + + E_j <= E_(j-1)/beta + +7(r beta^(-(j-1))+E_(j-1)+1)u/beta^3. + +Set T_j=beta^j E_j. Since beta<=1 and j>=1, + + T_j <= (1+7u/beta^2)T_(j-1)+7(r+1)u/beta^2. + +The budget u<=beta^2/(14n) implies +(1+7u/beta^2)^n<=exp(1/2)<2. Consequently + + E_n <= 14n(r+1)u beta^(-(n+2)) <= 2^(-p-1). + +Adding the factorization perturbation yields at most 3*2^(-p-2)<2^-p. +All scan intermediates have O(p+r^4) bits including integer magnitude. +In particular, b_rho^L is accumulated with rounding at every step, so its +representation does not grow with L. The closure denominator stays at +least beta/2, by the single-factor proof. + +Exact rational multiply/add followed by dyadic rounding and the one +closure division use integers of O(p+r^4) bits. Standard fast integer +multiplication and division give the stated scalar bit cost. A bounded +number of sequential passes suffices per factor, including rewinds and +the unit cyclic rotation. Two alternating clean data arrays suffice for +the streaming values. A conservative space allowance is +soft-O((L+r^2)(p+r^4)) bits, including setup and arithmetic scratch. + +## Paid unit phases + +The same factor certificate works for U=tau S when tau is an exactly +supplied rational complex number of modulus 1. In an outer factor, the +scan coefficient becomes tau/rho and the final scalar remains -1/rho. +In an inner factor, it becomes rho/tau; after the backward scan and unit +shift, multiply by tau^-1. Both new coefficients retain the same margin +beta. The inner scalar has modulus 1, so the same constant 7 covers its +rounded multiplication. If tau has T representation bits, scalar +arithmetic costs use O(p+r^4+T)-bit operands; T is not silently free. + +More generally suppose a unit tau has a charged approximation oracle. +Choose a rational unit sigma with |tau-sigma|<=nu, where + + nu <= epsilon/(n 2^r). + +Then ||P(tau S)-Q(sigma S)||<=epsilon+n||Q||_1 nu<=2 epsilon. +Because e>=p+2a+3, we still have 2 epsilon Abar<=1/2 and + + ||P(tau S)^-1-Q(sigma S)^-1|| + <=4 Abar^2 epsilon<=2^(-p-1). + +The same rounded execution budget contributes at most 2^(-p-1), giving +the original target 2^-p. The phase needs O(p+r^4) approximation bits, +in addition to reading whatever representation defines it. + +Here is a constructive way to obtain sigma with exact unit modulus. +Choose C in {1,-1,i,-i} so v=C^-1 tau has Re(v)>=1/2. A coarse enclosure +suffices to choose such a chart: one coordinate of a unit vector has +absolute value at least 1/sqrt(2). Put t=Im(v)/(1+Re(v)). Its denominator +is at least 3/2. Approximate t by a dyadic t0 with |t-t0|<=nu/2 and set + + sigma=C (1-t0^2+2i t0)/(1+t0^2). + +This is exactly rational and unit. The stereographic map's derivative +has modulus 2/(1+t^2)<=2, proving |tau-sigma|<=nu. Obtaining t0 costs +the oracle request plus scalar arithmetic at the stated precision. +For a phase exp(2 pi i h/m), [2] supplies that oracle after the cost of +reading/reducing the integer phase description; a very long h or m is +an extra input cost and is not covered by a bound that omits its length. + +This section treats a single constant unit phase. WEIGHTED-PROOF.md +extends the same bounds to a unit-weighted neighboring shift with an +independent phase at each position. The full transform's collection of +phases still needs its composition and preparation accounting. + +## Scope and finite evidence + +For r bounded by a fixed power of log p, the cost is quasi-linear in p +up to polylogarithmic factors and polynomial dependence on that radix. +There is no extra factor proportional to p in the number of full-array +passes. This removes the repeated-Neumann-pass obstruction for this +neighboring, clean-array inverse primitive. + +The mixed-factor reference certificate at CERTIFICATE-PROOF.md checks +ten kernel/embedding cases through radix 16, including inner roots, exact +rational unit phases, and a certified rational approximation of +exp(2 pi i/7). It uses exact coefficient enclosures, exact factor products, +and an explicit rounding budget. These finite certificates do not implement Pan's +worst-case factorizer or prove its complexity. The uniform argument above +depends on [1], [2], PR621, and the proved scan lemma. + +Remaining work for a multiplication application includes the complete +collection of phase gauges and their paid preparation, the actual strides/layout of every kernel, +composition across the complete transform and recursion, its total +precision guard, input/output normalization, and restoration of dirty +scratch where required. None is inferred from this standalone theorem. + +## Sources and attribution + +[1] K. Mehlhorn, M. Sagraloff, P. Wang, *From Approximate Factorization to +Root Isolation with Application to Cylindrical Algebraic Decomposition*, +Theorem 2 and Corollary 1 (crediting V. Pan), +https://arxiv.org/pdf/1301.4870, PDF page 8. + +[2] R. P. Brent, *Fast multiple-precision evaluation of elementary +functions*, J. ACM 23 (1976), 242-251, +https://maths-people.anu.edu.au/~brent/pub/pub034.html. + +PR621 by aliromman, head 520774462b19b29af41554b74def31f9d01e997e, +supplies the kernel and circle bound. Causal/anticausal filtering and +approximate factorization are standard methods. The explicit budget +composition and reference certificates here were prepared with OpenAI +Codex for chafreaky. No literature-priority claim is made. diff --git a/research/averaged-cyclotomic-height/vendor/pr628/interval_kernel.py b/research/averaged-cyclotomic-height/vendor/pr628/interval_kernel.py new file mode 100644 index 0000000000..1182175a55 --- /dev/null +++ b/research/averaged-cyclotomic-height/vendor/pr628/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=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/averaged-cyclotomic-height/vendor/pr977/NOTICE.md b/research/averaged-cyclotomic-height/vendor/pr977/NOTICE.md new file mode 100644 index 0000000000..57939c758d --- /dev/null +++ b/research/averaged-cyclotomic-height/vendor/pr977/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/averaged-cyclotomic-height/vendor/pr977/PROOF.md b/research/averaged-cyclotomic-height/vendor/pr977/PROOF.md new file mode 100644 index 0000000000..6019f4d03f --- /dev/null +++ b/research/averaged-cyclotomic-height/vendor/pr977/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/averaged-cyclotomic-height/vendor/pr977/cubic.py b/research/averaged-cyclotomic-height/vendor/pr977/cubic.py new file mode 100644 index 0000000000..61c213dd25 --- /dev/null +++ b/research/averaged-cyclotomic-height/vendor/pr977/cubic.py @@ -0,0 +1,62 @@ +"""Exact cubic budgets combining the retained partial-inverse and stride bounds.""" +from fractions import Fraction as F +from math import gcd +from common import need +from uniform import ceil_log2 + + +def plan(r,phi,p,m): + need(all(type(v) is int for v in (r,phi,p,m)) and r>=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/averaged-cyclotomic-height/verify.py b/research/averaged-cyclotomic-height/verify.py new file mode 100644 index 0000000000..e147345331 --- /dev/null +++ b/research/averaged-cyclotomic-height/verify.py @@ -0,0 +1,114 @@ +"""Source-bound averaged-height replay, Python 3.11+ with SymPy 1.14.0.""" +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 = ['budgets', 'interval_check', 'resultants'] + 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_AVERAGED_CYCLOTOMIC_HEIGHT', kappa='unchanged') + for name in ['budgets', 'interval_check', 'resultants']: + result[name] = loaded[name].main() + result['scope'] = ('The written proof supplies an all-prime-power averaged-height circle bound. ' + 'Finite rational enclosures, independent exact resultants and integer budgets ' + 'support its identities and failure modes. The inherited clean-scratch stride ' + 'budget becomes O(r^2 log^2 r); no new solver execution, dirty-array, ' + 'bit-reversible, common-label, full-transform 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_AVERAGED_HEIGHT_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_AVERAGED_CYCLOTOMIC_HEIGHT interval_radices=17 exact_resultants=6 budgets=752 kappa=unchanged') + + +if __name__ == '__main__': + main()