From 9004eb1b185803ba2f3101b8955e6e8d0dc12ed4 Mon Sep 17 00:00:00 2001 From: zxv Date: Sat, 24 Oct 2026 12:01:14 -0400 Subject: [PATCH] Prove exact precision and recovery-history frontiers for native recoding --- .../precision-state-frontier/FIXTURE.json | 918 ++++++++++++++++++ .../precision-state-frontier/MUTATIONS.json | 110 +++ .../precision-state-frontier/OVERLAP.json | 160 +++ .../precision-state-frontier/PORTABLE.json | 18 + research/precision-state-frontier/PROOF.md | 339 +++++++ research/precision-state-frontier/README.md | 159 +++ research/precision-state-frontier/RESULT.json | 235 +++++ .../precision-state-frontier/SOURCES.json | 56 ++ .../precision-state-frontier/VALIDATION.json | 95 ++ research/precision-state-frontier/frontier.py | 229 +++++ research/precision-state-frontier/history.py | 47 + .../mutation_check.py | 62 ++ .../precision-state-frontier/source/kernel.py | 152 +++ .../precision-state-frontier/test_package.py | 76 ++ research/precision-state-frontier/verify.py | 275 ++++++ 15 files changed, 2931 insertions(+) create mode 100644 research/precision-state-frontier/FIXTURE.json create mode 100644 research/precision-state-frontier/MUTATIONS.json create mode 100644 research/precision-state-frontier/OVERLAP.json create mode 100644 research/precision-state-frontier/PORTABLE.json create mode 100644 research/precision-state-frontier/PROOF.md create mode 100644 research/precision-state-frontier/README.md create mode 100644 research/precision-state-frontier/RESULT.json create mode 100644 research/precision-state-frontier/SOURCES.json create mode 100644 research/precision-state-frontier/VALIDATION.json create mode 100644 research/precision-state-frontier/frontier.py create mode 100644 research/precision-state-frontier/history.py create mode 100644 research/precision-state-frontier/mutation_check.py create mode 100644 research/precision-state-frontier/source/kernel.py create mode 100644 research/precision-state-frontier/test_package.py create mode 100644 research/precision-state-frontier/verify.py diff --git a/research/precision-state-frontier/FIXTURE.json b/research/precision-state-frontier/FIXTURE.json new file mode 100644 index 0000000000..0aa9f78163 --- /dev/null +++ b/research/precision-state-frontier/FIXTURE.json @@ -0,0 +1,918 @@ +{ + "schema": "literal-eight-mode-columns-v1", + "source_path": "research/coded-native-caller/NORMALIZERS.json", + "mode_columns": [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + -1, + 1, + -1, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + 1, + 1, + -1, + -1, + -1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + -1, + 1, + -1, + 1, + 1, + 1, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + -1, + 1, + -1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + -1, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + -1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + -1, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + -1, + 1, + 0, + 0, + -1, + 1, + 1, + 1, + 0, + -1, + -1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + -1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0 + ], + [ + 1, + 0, + 1, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 1, + 1, + 1, + 1, + 0, + 1, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 1, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 1, + 1, + 1, + 0, + 1, + 0, + 0, + 0, + 1, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 1, + 1, + 1, + 0, + 0 + ], + [ + 1, + 0, + 0, + 1, + 1, + 1, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + 0, + -1, + -1, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + -1, + -1, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 0, + 1, + 0, + 1, + -1, + 0, + 0, + 0, + 1, + 0, + 1, + 1, + 0, + 0, + 0, + 1, + 0, + 0, + -1, + -1, + -1, + 1, + 1, + 0, + 0, + 0, + 0, + -1, + -1, + -1, + -1, + -1, + -1, + 0, + 0 + ], + [ + 0, + 1, + 1, + 0, + 1, + 1, + -1, + 0, + 0, + 1, + 0, + 0, + 0, + -1, + 0, + 0, + 1, + 0, + -1, + -1, + 1, + 1, + 0, + 0, + -1, + -1, + 0, + 0, + -1, + 0, + 0, + 0, + -1, + 0, + 0, + 1, + -1, + -1, + 0, + 1, + 1, + 0, + 0, + -1, + -1, + -1, + -1, + -1, + 1, + 0, + 0, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 0, + 0, + -1, + 0, + 0, + 1, + 1, + 0, + 0, + -1, + -1, + 0, + 0, + -1, + 0, + 0, + -1, + 0, + 0, + 1, + -1, + 0, + 0, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 0, + 0, + 0, + -1, + 1, + 0, + -1, + -1, + -1, + -1, + 0, + -1, + -1, + 0, + 1, + 0, + 0, + 1, + 0, + 0, + 1, + 1 + ], + [ + 0, + 1, + 0, + 1, + 0, + 0, + -1, + 0, + -1, + 0, + 1, + 1, + -1, + 0, + -1, + -1, + 0, + -1, + 0, + 0, + -1, + -1, + 0, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + -1, + -1, + 1, + 0, + 0, + -1, + -1, + 0, + 0, + -1, + -1, + -1, + -1, + 0, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + 0, + -1, + 0, + 0, + 0, + -1, + -1, + 0, + 0, + 1, + -1, + 0, + 0, + -1, + -1, + 0, + 0, + 0, + 1, + 0, + 1, + 0, + 0, + -1, + 0, + -1, + 0, + 0, + 1, + 1, + 0, + 1, + 0, + 1, + 1, + 0, + -1, + 0, + -1, + 0, + 0, + -1, + 0, + -1, + 0, + 0, + -1, + 0, + 1, + 1, + -1, + 0, + 0, + -1, + -1 + ], + [ + 0, + 0, + 1, + 1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 1, + 1, + 0, + 0, + 1, + -1, + 0, + 0, + 1, + 1, + -1, + -1, + 0, + -1, + -1, + 0, + 0, + -1, + -1, + -1, + 0, + -1, + -1, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + -1, + -1, + 0, + 1, + 1, + -1, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + 1, + -1, + -1, + 0, + 0, + -1, + 1, + -1, + 1, + 0, + 0, + 1, + 1, + 0, + 0, + 0, + -1, + -1, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + -1, + -1, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 1, + 1, + -1, + -1 + ], + [ + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 0, + 0, + -1, + 1, + 0, + 0, + 1, + -1, + 0, + 0, + -1, + 1, + 1, + -1, + -1, + 1, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + 0, + 0, + 1, + -1, + 0, + -1, + 1, + 0, + 1, + -1, + -1, + 1, + 0, + 0, + 0, + 1, + -1, + 0, + -1, + 1, + 0, + -1, + 1, + -1, + 1, + 0, + 0, + 0, + -1, + 1, + 0, + 1, + -1, + -1, + 1, + 0, + 0, + -1, + 1, + -1, + 1, + 0, + -1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + 0, + 0, + 0, + 0, + -1, + 1, + 0, + 0, + 0, + -1, + 1, + 0, + 0, + -1, + 1, + 0, + -1, + 1, + 1, + -1 + ] + ] +} diff --git a/research/precision-state-frontier/MUTATIONS.json b/research/precision-state-frontier/MUTATIONS.json new file mode 100644 index 0000000000..337f9c9e7b --- /dev/null +++ b/research/precision-state-frontier/MUTATIONS.json @@ -0,0 +1,110 @@ +{ + "mutants": [ + { + "file": "frontier.py", + "modes": [ + { + "exit_code": 1, + "optimized": false, + "rejection": "ValueError: scalar fiber ceiling" + }, + { + "exit_code": 1, + "optimized": true, + "rejection": "ValueError: scalar fiber ceiling" + } + ], + "name": "half-ties-toward-zero", + "original_sha256": "3f623f3e64890905a50c64514bd13e353ed31a26d498f91bb1201a629e6fb8f7", + "replacement": { + "after": "(abs(value)+25)//52", + "before": "(abs(value)+26)//52" + } + }, + { + "file": "frontier.py", + "modes": [ + { + "exit_code": 1, + "optimized": false, + "rejection": "ValueError: source precision/state ceiling" + }, + { + "exit_code": 1, + "optimized": true, + "rejection": "ValueError: source precision/state ceiling" + } + ], + "name": "ignore-binary-coset", + "original_sha256": "3f623f3e64890905a50c64514bd13e353ed31a26d498f91bb1201a629e6fb8f7", + "replacement": { + "after": "patterns = list(range(256))", + "before": "patterns = self.signatures.get(signature, [])" + } + }, + { + "file": "frontier.py", + "modes": [ + { + "exit_code": 1, + "optimized": false, + "rejection": "ValueError: exact source reconstruction" + }, + { + "exit_code": 1, + "optimized": true, + "rejection": "ValueError: exact source reconstruction" + } + ], + "name": "forget-relative-input-scale", + "original_sha256": "3f623f3e64890905a50c64514bd13e353ed31a26d498f91bb1201a629e6fb8f7", + "replacement": { + "after": "q = [round52(t) for t in self.transpose(x)]", + "before": "q = [round52(scale*t) for t in self.transpose(x)]" + } + }, + { + "file": "frontier.py", + "modes": [ + { + "exit_code": 1, + "optimized": false, + "rejection": "ValueError: source precision/state ceiling" + }, + { + "exit_code": 1, + "optimized": true, + "rejection": "ValueError: source precision/state ceiling" + } + ], + "name": "omit-weight-four-words", + "original_sha256": "3f623f3e64890905a50c64514bd13e353ed31a26d498f91bb1201a629e6fb8f7", + "replacement": { + "after": "for z in self.dual if z.bit_count() != 4)", + "before": "for z in self.dual)" + } + }, + { + "file": "history.py", + "modes": [ + { + "exit_code": 1, + "optimized": false, + "rejection": "ValueError: sharp history alphabet" + }, + { + "exit_code": 1, + "optimized": true, + "rejection": "ValueError: sharp history alphabet" + } + ], + "name": "reuse-history-after-every-round", + "original_sha256": "9537b305fe48918e1e1404a3fda6615de8e7456dfb118d37da0a0d14ea749892", + "replacement": { + "after": "exponent = 8*components", + "before": "exponent = 8*rounds*components" + } + } + ], + "status": "PASS_SEMANTIC_MUTATION_CONTROLS" +} diff --git a/research/precision-state-frontier/OVERLAP.json b/research/precision-state-frontier/OVERLAP.json new file mode 100644 index 0000000000..098709e3aa --- /dev/null +++ b/research/precision-state-frontier/OVERLAP.json @@ -0,0 +1,160 @@ +{ + "additional_local_overlap": { + "path": "research/rounded-borrowing-contract/README.md", + "relationship": "Classifies rounded safe-translation lattices and saved residues at a different borrowed-child contract. Read as overlap; no claim that generic lattice or recovery counting is new." + }, + "canonical_base": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "canonical_committed_note_search": { + "command": "git grep -in -e '51008161' -e '362401' -e 'history accumulation' -e 'repeated recoding' -e 'precision.state frontier' -e 'coset weight enumerator' HEAD -- 'research/*/README.md' 'research/*/PROOF.md'", + "exit_code": 1, + "head": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "matches": 0, + "scope": "All committed matching README/PROOF paths, including omitted sparse-checkout files; exact terms only." + }, + "limits": [ + "Remote query searches PR bodies and Discussions, not all code or proofs.", + "Cached local note corpus was at a8e0467c60fc851f7a94b1ad5524fd562f5922bd; canonical exact-term Git search supplements it.", + "No match is not evidence of global priority; closed and outside work are not exhaustively surveyed.", + "No new Discussion post, shared-ledger update or selected-frontier update. The scoped contribution is prepared for authorized PR publication." + ], + "nearest_work": [ + { + "role": "Direct predecessor, sharp same-grid recovery; not claimed new.", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5323" + }, + { + "role": "Actual finite kernel, half-away rounding, destructive owned cleanup.", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5035" + }, + { + "role": "Actual physical matrix and access contract.", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4933" + }, + { + "role": "Native code geometry.", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4929" + }, + { + "role": "Cheaper unchanged kernel arithmetic; does not price the new codec.", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5321" + }, + { + "role": "Physical residual precision; absolute guards are not relative refinement.", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5333" + }, + { + "role": "Proposed selected-caller exact grids; mathematical comparison, not source dependency.", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5438" + } + ], + "novelty_scope": "Exact relative-precision frontier and constructive coset codec for this source; sharp arbitrary fixed unimodular changing-frame history law. Classical coding duality and volume counting are explicitly credited.", + "refresh_utc": "2026-10-24T15:28:52.588764+00:00", + "remote_search_reports": [ + { + "coverage": { + "discussions": { + "complete_pagination": true, + "fetched_at": "2026-10-24T14:46:22.157856+00:00", + "records": 4711 + }, + "local": { + "complete_head_inventory": true, + "head": "a8e0467c60fc851f7a94b1ad5524fd562f5922bd", + "head_records": 7377, + "records": 7377, + "unsearched_head_paths": [] + }, + "open_prs": { + "complete_pagination": true, + "fetched_at": "2026-10-24T14:45:17.279544+00:00", + "records": 313 + } + }, + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. Local coverage compares searched working-tree notes with regular note paths at coverage.local.head; it does not certify HEAD contents or historical coverage. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "matches_total": 1632, + "searched_at": "2026-10-24T14:46:22.687355+00:00", + "terms": [ + "recovery tags", + "guard bits", + "Construction A", + "weight enumerator", + "fiber size" + ], + "warnings": [] + }, + { + "coverage": { + "discussions": { + "complete_pagination": true, + "fetched_at": "2026-10-24T14:55:18.516259+00:00", + "records": 4711 + }, + "local": { + "complete_head_inventory": true, + "head": "a8e0467c60fc851f7a94b1ad5524fd562f5922bd", + "head_records": 7377, + "records": 7377, + "unsearched_head_paths": [] + }, + "open_prs": { + "complete_pagination": true, + "fetched_at": "2026-10-24T14:54:17.174399+00:00", + "records": 314 + } + }, + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. Local coverage compares searched working-tree notes with regular note paths at coverage.local.head; it does not certify HEAD contents or historical coverage. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "matches_total": 3, + "searched_at": "2026-10-24T14:55:18.874163+00:00", + "terms": [ + "relative precision", + "five guard", + "51008161", + "362401", + "history growth", + "recovery tags" + ], + "warnings": [] + } + ], + "specific_matches": [ + { + "excerpt": "# Exact recovery tags with a sharp state bound for the rounded inverse code\n\nFINDING \u2014 the rounded inverse-code kernel has a sharp recovery-state bound: 13^8 states, or 30 packed bits, per real scalar coordinate of its 112 owners. Eight separate four-bit quotient tags give a simple 32-bit implementation of the injective output interface. This answers part of the ownership question left by [PR #5035](https://github.com/CrocSwap/integer-mult-bounds/pull/5035); it is not a reversible circuit, a fre", + "kind": "local-readme", + "matched_terms": [ + "recovery tags" + ], + "path": "research/inverse-code-recovery-tags/README.md", + "score": 1, + "sha256": "928ec760364dc290624c9226355c2bcd701abdcef5863c9da35956f02460642e", + "title": "research/inverse-code-recovery-tags/README.md" + }, + { + "excerpt": " T^2 < 2^200014 < 2^210000` (precision), and\n `2T + 18 < 2^100003 < 2^210000` (tape).\n\nThus those five guards cannot fail alone while the stated hypotheses hold. `verify.py`\nchecks each maximal integer bound exactly. The inequalities are monotone over the stated\nnonnegative domain, which supplies the quantified implication rather than merely sampling it.\nFor the honest geometry, `M < 73S` follows from\n`rank_mass = 73 * live - 5120`, `physical = live + helpers + 10`, and positive helpers.\n**Non", + "kind": "local-readme", + "matched_terms": [ + "five guard" + ], + "path": "research/t16-invoice-boundary-audit/README.md", + "score": 1, + "sha256": "57eab1eb200b416f6d103819636b2952736370ec62bfee424a66ebc904386148", + "title": "research/t16-invoice-boundary-audit/README.md" + }, + { + "excerpt": "589231b23e12ceef3e4bad129\"\n }\n ]\n },\n \"scope_status\": \"refined\",\n \"actual_scope\": \"Exact recovery tags with a sharp state bound for the rounded inverse code\",\n \"scope_change_reason\": \"Publish the completed, scoped Discussion result as a source-bound proof and replay package. The local interface or error obligation is separate from the complete physical caller.\",\n \"bottleneck_link\": \"The physical construction needs funded precision and owned state. This result supplies one exact loca", + "kind": "local-task", + "matched_terms": [ + "recovery tags" + ], + "path": "research/inverse-code-recovery-tags/TASK.json", + "score": 1, + "sha256": "e5f8191937c4ddbc4aee7e14928d72ee815ea941375b62770d9ff0fca631fdaa", + "title": "research/inverse-code-recovery-tags/TASK.json" + } + ], + "status": "LOCAL_DRAFT_OVERLAP_REVIEW_NOT_A_NOVELTY_CERTIFICATE", + "submission_refresh": { + "canonical_main": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "checked_utc": "2026-10-24T16:00:44.326486+00:00", + "unchanged_from_base": true + } +} diff --git a/research/precision-state-frontier/PORTABLE.json b/research/precision-state-frontier/PORTABLE.json new file mode 100644 index 0000000000..c30735c463 --- /dev/null +++ b/research/precision-state-frontier/PORTABLE.json @@ -0,0 +1,18 @@ +{ + "cli_rejections": 3, + "cli_roundtrips": [ + { + "relative_bits": 4, + "states": 16 + }, + { + "relative_bits": 5, + "states": 1 + } + ], + "empty_path": true, + "history_cli_bits": 533, + "normal_and_optimized_receipt_sha256": "77e707e013c8656146436ade8f561ebff0f553d5b66dc9c43f692f1fca18ae38", + "read_only_package": true, + "status": "PASS_PORTABLE_PRECISION_STATE_PACKAGE" +} diff --git a/research/precision-state-frontier/PROOF.md b/research/precision-state-frontier/PROOF.md new file mode 100644 index 0000000000..79090050d4 --- /dev/null +++ b/research/precision-state-frontier/PROOF.md @@ -0,0 +1,339 @@ +# Exact recovery across precision changes and repeated native recoding + +**Status:** proposed scoped theorem with a constructive integer codec and finite +calibration. The argument below supplies the all-input implications; the probes +do not constitute independent proof review or a complete multiplication theorem. + +The source matrix and finite kernel are pinned in [SOURCES.json](SOURCES.json). +The same-grid `13^8` result belongs to [Ali Romman](https://github.com/aliromman), +[PR #5323](https://github.com/CrocSwap/integer-mult-bounds/pull/5323). +The additions here are the exact relative-precision frontier, its code-coset +decoder, and the sharp composition law under changing integer frames. + +## 1. General rounded low-rank maps + +Let `M` be an integer `n × r` matrix of full column rank, `β` a positive +integer, and `R` componentwise nearest rounding with half ties away from zero. +Write + +```text +K(z) = z − M R(Mᵀz/β), H = MᵀM − βI. +``` + +Inputs lie in `B Z^n`, where `B` is a nonsingular integer matrix. The input +coordinate is `x`, the actual fine-grid input is `z=Bx`, and the output is `y`. +Set `s=Mᵀy`. + +**Fiber theorem.** Preimages of `y` correspond bijectively to integer vectors +`q` satisfying + +```text +y + Mq ∈ B Z^n, +R((s + MᵀMq)/β) = q. (1) +``` + +Reconstruction is `x=B⁻¹(y+Mq)`. The second condition is equivalently +`−β/2 ≤ s+Hq ≤ β/2` componentwise, with the following endpoint rules: +at residual `−β/2` the corresponding `q_j` must be at least one; at residual +`+β/2` it must be at most minus one. + +*Proof.* A forward input has `z=y+Mq`, hence (1). Conversely (1) gives an +integer `x` whose defining rounded quotient is exactly `q`. Distinct `q` +give distinct inputs because `M` has full column rank. The endpoint rules +follow directly by rounding `q_j±1/2` away from zero. ∎ + +**Finite-state dichotomy.** A fixed finite alphabet suffices to recover every +input from its output and a retained tag if and only if `H` is nonsingular. +When `H` is nonsingular, every fiber lies in a translated parallelotope and +has at most + +```text +∏_j ( floor(β · ||row_j(H⁻¹)||₁) + 1 ) (2) +``` + +points. If `H` is singular, choose a nonzero integer kernel vector `u`. +Then `K(kMu)=0` for every integer `k`. Multiplication by `det(B)` puts these +inputs in `B Z^n`, since `B adj(B)=det(B)I`, and preserves their distinctness. +Thus that fiber is infinite. In the nonsingular case, the coordinate widths +of the parallelotope give (2). + +The exact minimum tag alphabet is the maximum fiber size: a tag must separate +inputs in the same fiber; conversely, order the finitely many candidates in +each fiber and retain their index. This is an effective finite enumeration for +rational data. Its running time can grow exponentially with rank; no general +efficient reversible synthesis follows from this existence statement. + +## 2. The pinned 112-owner matrix + +For the literal matrix in [FIXTURE.json](FIXTURE.json), + +```text +n=112, r=8, β=52, MᵀM=56I, H=4I, +A=I−MMᵀ/4, L=A⁻¹=I−MMᵀ/52. +``` + +Each row has four signs in `{−1,+1}`. Consequently `K(z)=Lz+e(z)` with +`||e(z)||∞≤2`; the physical error is at most two output-grid units. This is +the map implemented by [Brian](https://github.com/JoyboyBrian)'s unchanged +[PR #5035](https://github.com/CrocSwap/integer-mult-bounds/pull/5035) kernel. +Its owned zero-writing is classical destructive cleanup. + +Let `C` be the binary span of the rows of `M`. Direct finite source identities, +checked in `source_facts` and printed in [RESULT.json](RESULT.json), give + +```text +C=C⊥, |C|=16, W_C(a,b)=a^8+14a^4b^4+b^8. (3) +``` + +There is also, for each `j`, a pair of actual signed rows whose sum is `2e_j`. +Their row indices and signs are in the receipt. These facts give the complete +integer row lattice + +```text +row_Z(M) = {v ∈ Z^8 : v mod 2 ∈ C}. (4) +``` + +Indeed reduction modulo two gives one inclusion. For the reverse inclusion, +lift a binary row combination with the desired parity and correct its even +coordinate differences using the eight `2e_j` witnesses. + +It follows for every `g≥1` that + +```text +Mq = 0 mod 2^g + ⇔ q=2^(g−1)v with v mod 2 ∈ C⊥=C. (5) +``` + +Necessity of the divisibility of `q` follows by applying the `2e_j` row +combinations. After division, the remaining condition is exactly binary +orthogonality to all rows. This proves (5) at every precision, rather than +only those tested. + +## 3. Exact relative-precision frontier + +The coarse input is `x∈Z^112` and the fine output is + +```text +y = K(2^g x), δ_out = δ_in / 2^g. (6) +``` + +The integer `g≥0` is fixed known **relative** refinement. Increasing both +absolute precisions together leaves `g` unchanged. + +**Theorem.** The exact maximum fiber sizes and minimum fixed-length recovery +tags for (6) are: + +| Relative bits `g` | Maximum states `F_g` | Packed bits | Sufficient coarse bound `||x||∞≤H` to attain it | +|---:|---:|---:|---:| +| 0 | 815,730,721 = `13^8` | 30 | 24 | +| 1 | 51,008,161 | 26 | 12 | +| 2 | 362,401 | 19 | 6 | +| 3 | 4,096 | 12 | 16 | +| 4 | 16 | 4 | 14 | +| ≥5 | 1 | 0 | 0 | + +Thus five relative bits are necessary and sufficient for tag-free +injectivity on the unbounded coarse lattice. The displayed bounds on `H` +are sufficient witnesses, not claimed minimal range thresholds. + +### Upper bound + +For each mode, with `s=Mᵀy`, (1) gives the consecutive candidates + +```text +ceil((-26−s_j)/4) ≤ q_j ≤ floor((26−s_j)/4), +R((s_j+56q_j)/52) = q_j. (7) +``` + +The closed interval can have fourteen integers only when both boundary +residuals occur. Its lower endpoint would require `q_j≥1` while its upper +endpoint would require `q_j≤−1`; they cannot both survive. Removing invalid +boundary endpoints leaves at most thirteen consecutive integers. For `g=0`, +the modes are independent, giving `13^8` as in the predecessor result. + +For `g≥1`, two solutions to the coarse-lattice condition `y+Mq=0 mod 2^g` +differ by (5). Thus each coordinate has a fixed residue modulo +`d=2^(g−1)`. Its candidates in (7), divided by `d`, are at most +`ceil(13/d)` consecutive integers. Splitting by parity gives a preferred +parity with at most `a` choices and the other with at most `b` choices, where + +```text +(a,b) = (7,6), (4,3), (2,2), (1,1), (1,0) + for g=1,2,3,4,≥5, respectively. (8) +``` + +The remaining parity condition is one coset of `C`. Allowing every coordinate +its maximal counts bounds the fiber by a coset weight enumerator. For every +binary linear code and `a≥b≥0`, the zero coset maximizes this enumerator: + +```text +Σ_{c∈C+z} a^(8−wt(c)) b^wt(c) + = |C|/2^8 · Σ_{u∈C⊥} (−1)^(u·z) + (a+b)^(8−wt(u)) (a−b)^wt(u) + ≤ Σ_{c∈C} a^(8−wt(c)) b^wt(c). (9) +``` + +This is the elementary character-sum form of the classical MacWilliams +identity; all coefficients on the right of the middle expression are +nonnegative. Coordinatewise preferred parities simply change the coset `z`. +Equations (3), (8), and (9) give the table. For `g≥5` the upper bound is one; +an input supplies a nonempty fiber, so the map is injective. + +### Attaining fibers + +For `g=0,1,2`, use `y=0` and `q∈{−6,…,6}^8`, subject to (5). +For `g=1`, even/odd counts are `(7,6)`. For `g=2`, write `q=2v` with +`v∈{−3,…,3}^8`; its preferred parity is the all-one word, which belongs +to `C`, so the count is `W_C(4,3)`. Reconstruct `x=Mq/2^g`. +The four-term rows give the first three displayed bounds on `H`. + +For `g=3`, set `y=−M(2·1)`, where `1` is the eight-mode all-one vector. +Now `s=−112·1`, and (7) includes the thirteen integers centered at `28`. +The coarse congruence requires `q−2·1` in the kernel modulo eight, so +each `q_j` is in `{22,26,30,34}`. There are two choices of each residual +parity per coordinate and sixteen allowed parity words: `16·2^8=4096`. +The reconstruction `x=M(q−2·1)/8` has norm at most sixteen. + +For `g=4`, use `y=−M(4·1)`. The scalar interval is centered at `56`; +the coarse congruence leaves `q_j∈{52,60}`. Equation (5) selects exactly +sixteen parity words. Here `x=M(q−4·1)/16` has norm at most fourteen. +All these candidates have residual strictly inside the half-tie endpoints. +Finally the zero input attains the singleton bound for every `g≥5`. + +### Constructive codec + +[frontier.py](frontier.py) implements (7) without enumerating the enormous +fibers. The `2e_j` witnesses determine `q` modulo `2^(g−1)`. The remaining +112-bit parity syndrome determines at most sixteen binary code-coset words. +For each word the admissible quotients form a Cartesian product of eight +lists. A block offset plus mixed-radix rank indexes all candidates exactly. +Decoding unpacks that rank, computes `(y+Mq)/2^g`, and checks the defining +forward relation. The codec therefore attains the minimal state alphabet. + +The implementation accepts `0≤g≤16`; this is an operational resource limit, +while the proof covers all nonnegative `g`. It uses arbitrary-precision +Python integers, with no bit-operation/tape price or reversible cleanup claim. +The source identity, relative precision, output, and tag must belong to the +same invocation. Packet metadata is a validation interface; fixed source and +precision data are not a hidden variable recovery channel. + +For `N` independent real coordinates the exact maximum is `F_g^N` and the +minimum packed tag uses `ceil(log₂(F_g^N))` bits. With differing fixed +relative precisions the maximum is the product of their `F_g` values. + +## 4. Sharp history accumulation under changing frames + +Put `F=13^8`. Let each step be + +```text +f_i = V_i ◦ K ◦ U_i, U_i,V_i ∈ GL_112(Z), +``` + +where the frame changes are fixed and known independently of the input. +Only the final 112-owner output and retained history are available for exact +recovery; additional observations must be counted separately. + +**Theorem.** The exact maximum fiber of `f_t◦…◦f_1` on `Z^112` is `F^t`. +Thus the minimal retained-history alphabet has `13^(8t)` states and needs +`ceil(8t log₂13)` packed bits. Commutation of the frames is unnecessary. + +*Upper bound.* Each step has maximum fiber `F`, since integer unimodular +pre/post changes are bijections. Induction bounds each composite fiber by +`F^t`. Retaining each step's tag allows reconstruction in reverse order, +attaining an alphabet of this size. + +*Lower bound.* The matrix `L` has eigenvalue `−1/13` on the eight-dimensional +column space of `M` and eigenvalue one on its complement. Hence +`|det L|=1/F`. Each step is a bounded perturbation of `V_iLU_i`, and a finite +composition remains a bounded perturbation of its matrix product. Its +determinant magnitude is `F^(−t)`. Apply the following counting lemma. ∎ + +**Lattice-volume lemma.** If `f:Z^n→Z^n`, `L` is nonsingular, and +`||f(x)−Lx||∞≤E` uniformly in `x`, the maximum fiber is at least +`ceil(1/|det L|)` (or is infinite). + +*Proof.* The number of lattice points `Lx` in `[-R,R]^n` is +`(2R)^n/|det L|+O(R^(n−1))`. This follows by tiling with the fundamental +parallelotopes `L(x+[-1/2,1/2]^n)`; their boundary thickness is bounded +independently of `R`. Their corresponding outputs lie in +`[-R−E,R+E]^n`, containing at most `(2R+2E+1)^n` integer points. +If all fibers have size at most `m`, divide the resulting counting inequality +by `(2R)^n` and let `R` increase. This forces `m≥1/|det L|`. ∎ + +The conclusion concerns the unbounded integer domain, and therefore some +sufficiently large finite input range. It need not hold in a prescribed small +range. The two-dimensional noncommuting controls in `verify.py` exhibit this: +one finite window reaches only sixty of the eventual sixty-four states. + +For stationary frames there is an explicit sufficient range. On `x=Mv`, + +```text +K(Mv) = −M R(v/13). +``` + +The identity uses `56/52=1+1/13`; for integer `v`, denominator thirteen +excludes half ties, making integer translation of nearest rounding legitimate. +All vectors with `|v_j|≤(13^t−1)/2` reach zero after `t` steps. Induct on +the radius recurrence `R_t=13R_(t−1)+6`. These distinct inputs give +`13^(8t)` preimages and obey `||x||∞≤2(13^t−1)`. + +For `N` independent real coordinates, replace `K` by its direct product and +allow arbitrary fixed unimodular mixing of all `112N` integer fields between +steps. The same proof gives `13^(8Nt)` states. At eighteen steps and `N=1`, +packing all history together needs **533 bits**, rather than the 540 bits +from eighteen separately padded thirty-bit records. + +## 5. Precision and side information conservation + +Suppose step `i` instead uses `K(2^(g_i)z)`, with fixed known `g_i≥0`, +and let `G=Σ_i g_i`. For `N` real coordinates, `n=112N`. The final integer +map is a bounded perturbation of a matrix of determinant magnitude + +```text +2^(112NG) / 13^(8Nt). +``` + +If a retained side observation has at most `S` possible values and the history +has at most `T`, injective recovery requires + +```text +T S ≥ ceil(13^(8Nt) / 2^(112NG)), +T ≥ ceil(13^(8Nt) / (2^(112NG) S)), +b + log₂S + 112NG ≥ 8Nt log₂13 when T≤2^b. (10) +``` + +Apply the same counting proof with at most `TS` states above each final output. +The lower bound on `T` is at least one. These are necessary bounds; sharpness +is asserted only for `G=0,S=1`. In particular the exact one-step table is +strictly stronger than the volume relaxation at positive `g`. + +Nonuniform fixed diagonal refinements have the same volume argument with +`112NG` replaced by the sum of their added fractional bit positions. Other +nonunimodular maps require their determinant and actual lattice covolume. +Input-dependent frame/precision choices require counting their recoverable +control data among the retained observations or history. + +This excludes indefinitely many recodings with bounded cumulative refinement, +bounded history, and bounded side information when every initial input on +growing ranges must remain recoverable. Rereading the original input, keeping +another output, changing the map, or admitting irreversible disposal changes +that contract. The result imposes no paid-query, average-entropy, or physical +thermodynamic lower bound. + +## 6. Classical input, source novelty, and proof limits + +Weight-enumerator duality is classical: see MacWilliams, +[A Theorem on the Distribution of Weights in a Systematic Code](https://doi.org/10.1002/j.1538-7305.1963.tb04003.x), +and Forney, +[Codes on graphs: Duality and MacWilliams identities](https://arxiv.org/abs/0911.5508). +The pigeonhole and lattice-volume arguments are elementary, and are proved +here rather than claimed as new general mathematics. The proposed repository +contribution is their exact application to this native code, including +attainment, the codec, and arbitrary changing-frame composition. + +The unchanged selected record at the source pin has conditional +`κ=0.003027288235`. This package changes no selected result. Mathematical +injectivity at five relative bits does not make the retained destructive kernel +a reversible program. Source access, wrappers, output magnitude, carry widths, +codec cost, variable control, additional observations, and eventual restoration +still need a complete caller-bound implementation and invoice. diff --git a/research/precision-state-frontier/README.md b/research/precision-state-frontier/README.md new file mode 100644 index 0000000000..9c21dc65e5 --- /dev/null +++ b/research/precision-state-frontier/README.md @@ -0,0 +1,159 @@ +# Where rounded native codes keep their history + +**Scoped theorem and constructive codec; author-checked evidence. No new κ.** + +This package determines the exact recovery information lost by the actual +112-owner rounded inverse as its output grid changes. It also proves that +the worst-case history cost multiplies under repeated same-grid recoding, +even through noncommuting changes of integer coordinates. + +The coarse input is `x∈Z^112`; the output is +`y=2^g x−M round_away(2^g Mᵀx/52)`, where the pinned source has +`MᵀM=56I`. The fixed parameter `g` measures output precision **relative to +the actual input lattice**. It is not an absolute working-precision allowance. + +| Relative bits `g` | Exact worst-case recovery states | Packed tag bits | Added fractional slots + tag bits¹ | +|---:|---:|---:|---:| +| 0 | 815,730,721 | 30 | 30 | +| 1 | 51,008,161 | 26 | 138 | +| 2 | 362,401 | 19 | 243 | +| 3 | 4,096 | 12 | 348 | +| 4 | 16 | 4 | 452 | +| 5 | 1 | 0 | 560 | + +¹One real scalar coordinate across all 112 owners, with uniform fixed-width +fractional fields: `112g+ceil(log₂ F_g)`. This comparison excludes magnitude +bits, scratch, movement, and execution costs. Every `g≥5` is injective. +Increasing input and output precision together preserves the same-grid loss. + +The `g=0` result is [Ali Romman](https://github.com/aliromman)'s +[PR #5323](https://github.com/CrocSwap/integer-mult-bounds/pull/5323). +The positive-precision rows and the composition theorem extend that work. + +## Significance for researchers + +Recovery tags, precision, and repeated recoding can now be compared using an +exact interface theorem. Five relative bits permit a tag-free mathematical +decoder; they add 560 fractional bit positions if all 112 output fields are +uniformly widened. That route is most attractive when the finer output grid +is already needed. On the same grid, integer frame changes cannot keep the +recovery history bounded through indefinitely many recodings on growing input +ranges. A proposal must retain history, introduce relative refinement or other +recoverable information, change the map, or accept irreversible disposal. + +## The broader theorem + +For full-column-rank integer `M`, positive integer `β`, and inputs in `B Z^n`, +the fibers of `z−M round(Mᵀz/β)` are exactly the integer quotients in a +translated residual parallelotope satisfying the input-lattice congruence. +Uniform finite recovery tags exist exactly when `MᵀM−βI` is nonsingular. +This supplies a reusable test and a finite enumeration method, with no general +efficient synthesis claim. + +For this source, `N` real coordinates and `t` same-grid recodings require +exactly `13^(8Nt)` worst-case history states. Fixed known unimodular pre/post +maps may mix all `112N` fields and need not commute. Packed history needs +`ceil(8Nt log₂13)` bits; for `N=1,t=18`, that is **533 bits**. + +With total uniform relative refinement `G`, side information of at most `S` +states, and a `b`-bit retained history, the necessary conservation inequality is + +```text +b + log₂S + 112NG ≥ 8Nt log₂13. +``` + +Sharpness is proved for same-grid history with no extra observation. The +refined/side-information inequality is a necessary volume bound; the one-step +table is stronger. These history claims require the unbounded lattice, or a +sufficiently large finite range. Stationary frames have an explicit sufficient +input bound `||x||∞≤2(13^t−1)`. A fixed small range need not attain the bound. + +See [PROOF.md](PROOF.md) for all hypotheses, the source binary code's weight +enumerator `a^8+14a^4b^4+b^8`, attaining fibers, and the volume argument. + +## Nearest overlapping work and useful seams + +| Work | Existing contribution | New use or unresolved seam | +|---|---|---| +| [PR #4933](https://github.com/CrocSwap/integer-mult-bounds/pull/4933), [Dillon Amburgey](https://github.com/dillona); [PR #4929](https://github.com/CrocSwap/integer-mult-bounds/pull/4929), [David Ganz](https://github.com/Dugongue) | Physical normalizers and native code geometry | Bind the coarse lattice and actual common-coordinate access before using the table. | +| [PR #5035](https://github.com/CrocSwap/integer-mult-bounds/pull/5035), [Brian](https://github.com/JoyboyBrian) | Finite bitwise rounded kernel and sharp output error | Its byte-exact kernel is calibrated here; destructive zero-writing still needs a separate reversible implementation. | +| [PR #5323](https://github.com/CrocSwap/integer-mult-bounds/pull/5323), [Ali Romman](https://github.com/aliromman) | Sharp same-grid `13^8` states | Direct predecessor; this package adds relative precision, code-coset ranking, and changing-frame composition. | +| [PR #5321](https://github.com/CrocSwap/integer-mult-bounds/pull/5321), [Ali Romman](https://github.com/aliromman) | Cheaper kernel arithmetic | Recovery-codec cost must join its bill; the information theorem supplies no priced implementation. | +| [PR #5333](https://github.com/CrocSwap/integer-mult-bounds/pull/5333), [Ali Romman](https://github.com/aliromman) | All-site physical pair residual budget | Extract actual input/output grids before identifying any relative bits. | +| [PR #5438](https://github.com/CrocSwap/integer-mult-bounds/pull/5438), [Mark](https://github.com/Matarener) | Proposed exact selected-caller grids | Its absolute grid requirement does not by itself establish five relative bits for this inverse map. | + +Classical outside input is MacWilliams' +[weight-enumerator theorem](https://doi.org/10.1002/j.1538-7305.1963.tb04003.x) +and Forney's [Fourier/duality treatment](https://arxiv.org/abs/0911.5508). +The new claim is the exact source application and its composition consequences; +general code duality and volume counting retain their classical status. +[OVERLAP.json](OVERLAP.json) records search coverage and its limits. + +## Reproduction and interfaces + +Python 3.10+ and the standard library suffice. From the repository root: + +```sh +python3 -B research/precision-state-frontier/verify.py +python3 -B research/precision-state-frontier/test_package.py +python3 -B research/precision-state-frontier/mutation_check.py +``` + +The first prints [RESULT.json](RESULT.json); `--source-root .` additionally +checks six exact canonical source hashes and equality of the literal matrix. +The default is self-contained and Git/network-free. The second repeats both +normal and optimized verification from a read-only portable copy with an empty +`PATH`, then exercises the public JSON interfaces and rejection controls. +The third tests five semantic changes in both Python modes on private copies. +[VALIDATION.json](VALIDATION.json) records commands, hashes, environment, and +unrun obligations. This standalone package is not registered in the shared +replay catalogue. + +```sh +python3 -B research/precision-state-frontier/frontier.py table +python3 -B research/precision-state-frontier/frontier.py encode input.json > encoded.json +python3 -B research/precision-state-frontier/frontier.py decode encoded.json +python3 -B research/precision-state-frontier/history.py budget.json +``` + +Encoding input has exactly `{"g":4,"x":[112 exact integer entries]}`. +The output includes the fine integer output, rank tag, source identity, and +fiber/state metadata. `budget.json` may be `{"rounds":18}`; optional fields +are `components`, `total_relative_guard_bits`, and `side_states`. +The codec supports `0≤g≤16`; excessive guard/exponent requests fail with +“no decision” rather than silently truncating the mathematical domain. + +Finite checks cover all 64 Gram entries, 2,016 dyadic congruence cases, 1,280 +coset counts, 321 scalar intervals, 97 attaining-fiber roundtrips, 36 other +input roundtrips, 24 unchanged source-kernel calls, three source-sized changing +frame chains, and noncommuting toy windows totaling 345,859 inputs. +Large fibers are counted by the proof and factored codec, not enumerated. + +## Risks, tradeoffs, and remaining obligations + +| Boundary | Consequence | +|---|---| +| Relative versus absolute precision | Widening both grids leaves `g=0`; existing absolute guards cannot be reused as an injectivity proof. | +| Interface versus reversible machine | The injective output/tag map still needs legal computation, storage, routing, and eventual restoration. | +| Uniform precision cost | Eliminating a thirty-bit tag can add 560 fractional positions; output range and scratch may add more. | +| Lattice and observation contract | Nonunimodular maps, extra outputs, rereads, and variable control change the information bill. | +| Input range and repetition | The exact repeated bound is asymptotic in available input range; it does not force 533 bits in every bounded eighteen-step caller. | +| Validation status | Written scoped proof and author calibration; independent mathematical review and caller admission remain open. | + +## Open next questions + +| Direction | Opportunity and first discriminating step | Main risk / stop rule | +|---|---|---| +| Actual pair/caller lattice | At one named inverse call, derive the input lattice and output grid using the physical and exact-grid work above. | Stop applying this frontier if the matrix or access contract differs. | +| Paid reversible codec | Compile one `g=0` or `g=4` rank/unrank path with explicit scratch and restoration; compare the complete bill to retained-input replay. | The information optimum may cost more to compute than a simpler thirty-two-bit quotient layout. | +| Unequal precision | Optimize per-owner grid additions using the actual congruence lattice, rather than widening all 112 fields. | Determinant volume alone is not an attainable decoder; avoid claiming an optimum from that relaxation. | +| Mixed refined chains | Compute a sharp two-step fiber with one relative bit and a noncommuting integer frame. | One-step maxima need not multiply after refinement; the current conservation inequality may be loose. | +| Wider native-code family | Derive the row lattice and coset enumerator of one other admitted low-rank code, then compare complete recovery cost. | A favorable determinant or binary code does not establish physical access or a useful full invoice. | +| Finite-range frontier | Determine the smallest `H` attaining a chosen row or repeated-frame bound, using exact branch-and-bound. | Fixed-range enumeration grows rapidly; stop after a certified threshold or explicit useful gap. | + +Source pin: canonical main `32890bc5de034ab8fc93ac88ead7279a6a416d04`, +priority revision seven. Its selected conditional `κ=0.003027288235` is +unchanged. [zxv](https://github.com/zxv), with substantial OpenAI Codex +assistance. Apache-2.0. The retained source kernel keeps its original notice; +all native, controller, precision, compiler, and recovery predecessors retain +their attribution. diff --git a/research/precision-state-frontier/RESULT.json b/research/precision-state-frontier/RESULT.json new file mode 100644 index 0000000000..b3b919fb66 --- /dev/null +++ b/research/precision-state-frontier/RESULT.json @@ -0,0 +1,235 @@ +{ + "histories": { + "budget_cases": 72, + "changing_frame_roundtrips": 3, + "eighteen_same_grid_rounds": { + "components": 1, + "large_input_range_required": true, + "minimum_history_states": 25576595330541451188765832638549849298314373520153608786670906139957572402372141367568937940553448343243684988004734396737936160930207489715389784190815069636161, + "minimum_packed_bits": 533, + "new_fractional_slots": 0, + "rounds": 18, + "scope": "Fixed known unimodular frames, bounded rounding residuals, all initial inputs recoverable. Refined/side-information bounds are necessary, not claimed attainable.", + "side_states": 1, + "status": "SHARP_SAME_GRID_HISTORY" + }, + "stationary": [ + { + "packed_bits": 30, + "rounds": 1, + "sufficient_input_bound": 24, + "zero_fiber_states": 815730721 + }, + { + "packed_bits": 60, + "rounds": 2, + "sufficient_input_bound": 336, + "zero_fiber_states": 665416609183179841 + }, + { + "packed_bits": 89, + "rounds": 3, + "sufficient_input_bound": 4392, + "zero_fiber_states": 542800770374370512771595361 + }, + { + "packed_bits": 119, + "rounds": 4, + "sufficient_input_bound": 57120, + "zero_fiber_states": 442779263776840698304313192148785281 + }, + { + "packed_bits": 149, + "rounds": 5, + "sufficient_input_bound": 742584, + "zero_fiber_states": 361188648084531445929920877641340156544317601 + }, + { + "packed_bits": 178, + "rounds": 6, + "sufficient_input_bound": 9653616, + "zero_fiber_states": 294632676319010105335586872991323185304149065116720321 + } + ] + }, + "noncommuting_volume_controls": [ + { + "frames": [ + 0, + 1 + ], + "input_bound": 64, + "inputs": 16641, + "maximum_fiber_in_window": 60, + "unbounded_maximum": 64 + }, + { + "frames": [ + 0, + 1 + ], + "input_bound": 128, + "inputs": 66049, + "maximum_fiber_in_window": 64, + "unbounded_maximum": 64 + }, + { + "frames": [ + 0, + 1, + 0 + ], + "input_bound": 256, + "inputs": 263169, + "maximum_fiber_in_window": 512, + "unbounded_maximum": 512 + } + ], + "recovery": { + "attaining_fiber_roundtrips": 97, + "frontier": [ + { + "attaining_input_bound": 24, + "fractional_slots_plus_tag": 30, + "maximum_fiber": 815730721, + "packed_bits": 30, + "relative_guard": 0, + "sampled_tags": 20 + }, + { + "attaining_input_bound": 12, + "fractional_slots_plus_tag": 138, + "maximum_fiber": 51008161, + "packed_bits": 26, + "relative_guard": 1, + "sampled_tags": 20 + }, + { + "attaining_input_bound": 6, + "fractional_slots_plus_tag": 243, + "maximum_fiber": 362401, + "packed_bits": 19, + "relative_guard": 2, + "sampled_tags": 20 + }, + { + "attaining_input_bound": 16, + "fractional_slots_plus_tag": 348, + "maximum_fiber": 4096, + "packed_bits": 12, + "relative_guard": 3, + "sampled_tags": 20 + }, + { + "attaining_input_bound": 14, + "fractional_slots_plus_tag": 452, + "maximum_fiber": 16, + "packed_bits": 4, + "relative_guard": 4, + "sampled_tags": 16 + }, + { + "attaining_input_bound": 0, + "fractional_slots_plus_tag": 560, + "maximum_fiber": 1, + "packed_bits": 0, + "relative_guard": 5, + "sampled_tags": 1 + } + ], + "other_input_roundtrips": 36 + }, + "rejections": [ + "wrong-source", + "wrong-fiber", + "wrong-bound", + "wrong-bits", + "negative-tag", + "out-of-fiber-tag", + "boolean-guard", + "float-output", + "missing-owner", + "absolute-guard-is-not-relative-refinement" + ], + "scalar_intervals": 321, + "source_facts": { + "binary_codewords": [ + 0, + 15, + 51, + 60, + 85, + 90, + 102, + 105, + 150, + 153, + 165, + 170, + 195, + 204, + 240, + 255 + ], + "coset_enumerator_cases": 1280, + "dyadic_congruence_cases": 2016, + "gram_entries": 64, + "two_unit_witnesses": [ + [ + 0, + 1, + 92, + -1 + ], + [ + 0, + 1, + 87, + -1 + ], + [ + 0, + 1, + 81, + 1 + ], + [ + 0, + 1, + 76, + -1 + ], + [ + 1, + 1, + 75, + -1 + ], + [ + 1, + 1, + 82, + -1 + ], + [ + 2, + 1, + 89, + -1 + ], + [ + 4, + 1, + 5, + -1 + ] + ], + "weight_enumerator": { + "0": 1, + "4": 14, + "8": 1 + } + }, + "status": "PASS_PRECISION_STATE_FRONTIER", + "unchanged_kernel_calls": 24 +} diff --git a/research/precision-state-frontier/SOURCES.json b/research/precision-state-frontier/SOURCES.json new file mode 100644 index 0000000000..aa892a4cb3 --- /dev/null +++ b/research/precision-state-frontier/SOURCES.json @@ -0,0 +1,56 @@ +{ + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903", + "usage": "provenance" + }, + { + "path": "research/coded-native-caller/NORMALIZERS.json", + "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f", + "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da", + "usage": "provenance" + }, + { + "path": "research/coded-native-caller/PHYSICAL.md", + "git_blob": "da8837ba67423ef08ef1afb8e8297a8032aafe9f", + "sha256": "4321b159ff8d3fe705419adaaa1beef75606e869e34341bda553f17d598a6078", + "usage": "provenance" + }, + { + "path": "research/coded-inverse-fixed-grid/kernel.py", + "git_blob": "70b5d65cae9a8f19cfda4a862c7ecc0bdc42c89b", + "sha256": "bc0e9f705665d6981c0f9176dad0f2d71471735e866c44643cb6835423435303", + "usage": "provenance" + }, + { + "path": "research/coded-inverse-fixed-grid/PROOF.md", + "git_blob": "a465ed5ce6b0bd7ac03bc79e72003380a839d7f4", + "sha256": "2bf523cf4f4b3e6bd90805e86f2cbf5d1d85142c16e751e72f09480bcdbee5cd", + "usage": "provenance" + }, + { + "path": "research/inverse-code-recovery-tags/PROOF.md", + "git_blob": "94dcc7307656ec1fee672187f5c97e4fbe9821dd", + "sha256": "0a10d518a071af52de0300dd6f43f610a3aa6096bd470897611aa3d3e5cba46b", + "usage": "provenance" + } + ], + "fixture_sha256": "2ca4d7550fcae5b757ec500f87aee1d2ef9f64b59e4abe2bda93319521304af8", + "vendored_kernel_sha256": "bc0e9f705665d6981c0f9176dad0f2d71471735e866c44643cb6835423435303", + "literature": [ + { + "title": "A Theorem on the Distribution of Weights in a Systematic Code", + "url": "https://doi.org/10.1002/j.1538-7305.1963.tb04003.x", + "role": "Classical weight-enumerator/Fourier duality, not claimed new." + }, + { + "title": "Codes on graphs: Duality and MacWilliams identities", + "url": "https://arxiv.org/abs/0911.5508", + "role": "Classical code-coset Fourier framework; the source precision/state frontier is the proposed application." + } + ], + "scope": "Local proof, exact source geometry, constructive tag codec and bounded calls to the unchanged finite kernel. No full caller, reversible implementation or new kappa." +} diff --git a/research/precision-state-frontier/VALIDATION.json b/research/precision-state-frontier/VALIDATION.json new file mode 100644 index 0000000000..4b75b6bb71 --- /dev/null +++ b/research/precision-state-frontier/VALIDATION.json @@ -0,0 +1,95 @@ +{ + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "commands": [ + { + "command": "python3 -B research/precision-state-frontier/verify.py --source-root .", + "receipt": "RESULT.json", + "result": "PASS_PRECISION_STATE_FRONTIER", + "source_checks": "Six canonical source SHA256 pins plus literal matrix equality." + }, + { + "command": "python3 -B research/precision-state-frontier/test_package.py", + "receipt": "PORTABLE.json", + "result": "PASS_PORTABLE_PRECISION_STATE_PACKAGE", + "scope": "Both normal and optimized self-contained replays match RESULT.json byte-for-byte, empty PATH, read-only package, fresh unused pycache path; two JSON codec roundtrips, history CLI, three CLI rejections." + }, + { + "command": "python3 -B research/precision-state-frontier/mutation_check.py", + "receipt": "MUTATIONS.json", + "result": "PASS_SEMANTIC_MUTATION_CONTROLS", + "scope": "Five semantic mutations rejected with explicit ValueError in both normal and optimized modes on private copies." + } + ], + "coverage": { + "attaining_fiber_roundtrips": 97, + "binary_code_size": 16, + "binary_coset_counts": 1280, + "cli_rejections": 3, + "dyadic_congruence_cases": 2016, + "gram_entries": 64, + "history_budget_cases": 72, + "integer_two_unit_row_witnesses": 8, + "literal_source_kernel_calls": 24, + "noncommuting_two_dimensional_inputs": 345859, + "other_input_roundtrips": 36, + "packet_rejections": 10, + "scalar_intervals": 321, + "semantic_mutants_in_each_mode": 5, + "source_sized_changing_frame_round_counts": [ + 2, + 4, + 6 + ], + "stationary_history_round_counts": [ + 1, + 2, + 3, + 4, + 5, + 6 + ] + }, + "environment": { + "executable": "/opt/homebrew/opt/python@3.14/bin/python3.14", + "libraries": "Python standard library only", + "machine": "arm64", + "platform": "macOS-26.5.1-arm64-arm-64bit-Mach-O", + "python": "3.14.5 (main, May 10 2026, 10:21:34) [Clang 21.0.0 (clang-2100.0.123.102)]" + }, + "not_run": [ + "Independent mathematical review", + "Lean or other proof assistant", + "Full physical caller, native/compiler, or selected-result replay", + "Shared registered research-package CI (this standalone package is not registered)" + ], + "publication_checks": { + "result_receipt": "External submission receipt, checked after creating the publication commit.", + "scientific_replay": "Existing executable and fixture hashes are unchanged; no historical suites rerun for metadata-only submission edits.", + "scope": "Exact raw Git blob comparison for every published package file, source-pin blob/SHA256 checks, and base ancestry. Standalone package has no VERIFY.json; the shared registered-package preflight does not apply." + }, + "recorded_utc": "2026-10-24T16:00:44.329224+00:00", + "scientific_limits": [ + "Finite source identities and the written proof establish the asserted all-input result; probes are calibration rather than independent review.", + "Large fibers and 13^(8Nt) states are counted by the proof, not exhaustively enumerated.", + "Positive-refinement/side-information volume bounds are necessary and not asserted sharp.", + "Repeated sharp history requires the unbounded lattice or a sufficiently large finite range.", + "Source kernel is destructive; the new mathematical codec has no reversible or paid arithmetic/tape implementation." + ], + "sha256": { + "FIXTURE.json": "2ca4d7550fcae5b757ec500f87aee1d2ef9f64b59e4abe2bda93319521304af8", + "MUTATIONS.json": "d472944656eb5a58369ad5336db81b43877be8bf1b6b078de9dce2415f2b7cc3", + "OVERLAP.json": "ba0ba62f5631a169bb3a29eb124cfc96dc2dccff91de2355d847f3443cd0d1b2", + "PORTABLE.json": "5be105899480ce29998f5b26092c8389442cbfa7c979e2266845eae17f0de5db", + "PROOF.md": "f7e4d410cc108bc8b148ed8641c09be20c4c864fbc3908c533fa889b59dae341", + "README.md": "0a62a71cea7e8ec40cf1a175b84b2d42cd81a3d94c7ab106ea7d6c765d75d8d2", + "RESULT.json": "77e707e013c8656146436ade8f561ebff0f553d5b66dc9c43f692f1fca18ae38", + "SOURCES.json": "6128e8f85672e7156658bf97805a91d7f9f00607c5690390fc57b4923f6c59e0", + "frontier.py": "3f623f3e64890905a50c64514bd13e353ed31a26d498f91bb1201a629e6fb8f7", + "history.py": "9537b305fe48918e1e1404a3fda6615de8e7456dfb118d37da0a0d14ea749892", + "mutation_check.py": "36cce52c7404d5ca6f7cced01fca5d2142e4156e0eca548017713744e7589afe", + "source/kernel.py": "bc0e9f705665d6981c0f9176dad0f2d71471735e866c44643cb6835423435303", + "test_package.py": "a3e9f04e428e318b7178b1fc6f56884d311a0675eff87a5e50d0d9cb8a0e4c46", + "verify.py": "1245fd3f3fa6391a202fae35abe56375d0977c286d537ac9e1b7ccaaa4b9e537" + }, + "status": "AUTHOR_CHECKED_SCOPED_PROOF_AND_CALIBRATION" +} diff --git a/research/precision-state-frontier/frontier.py b/research/precision-state-frontier/frontier.py new file mode 100644 index 0000000000..ccfe9a2573 --- /dev/null +++ b/research/precision-state-frontier/frontier.py @@ -0,0 +1,229 @@ +#!/usr/bin/env python3 +"""Exact precision/recovery-state codec for the pinned 112-owner inverse. + +Apache-2.0; substantial OpenAI Codex assistance. Not a priced reversible +circuit. Source arithmetic and same-grid recovery retain predecessor credit. +""" +from pathlib import Path +from itertools import product +import argparse +import hashlib +import json + +ROOT = Path(__file__).resolve().parent + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load(path): + def unique(pairs): + result = {} + for k, v in pairs: + need(k not in result, 'duplicate JSON key') + result[k] = v + return result + with open(path, encoding='utf-8') as f: + return json.load(f, object_pairs_hook=unique) + + +def round52(value): + need(type(value) is int, 'integer numerator required') + return (1 if value >= 0 else -1)*((abs(value)+26)//52) + + +def ceildiv(a, b): + return -((-a)//b) + + +def intvector(values, size): + need(isinstance(values, list) and len(values) == size and all(type(x) is int for x in values), + 'exact integer vector required') + return list(values) + + +class Geometry: + def __init__(self): + sources = load(ROOT/'SOURCES.json') + raw = (ROOT/'FIXTURE.json').read_bytes() + need(hashlib.sha256(raw).hexdigest() == sources['fixture_sha256'], 'literal source fixture hash') + fixture = load(ROOT/'FIXTURE.json') + columns = fixture['mode_columns'] + need(len(columns) == 8 and all(len(v) == 112 for v in columns), 'eight source columns') + self.m = list(map(list, zip(*columns))) + need(all(type(x) is int and x in (-1, 0, 1) for row in self.m for x in row), 'source signs') + self.fingerprint = sources['fixture_sha256'] + self.binary = [sum((a & 1) << j for j, a in enumerate(row)) for row in self.m] + self.dual = [z for z in range(256) if all((z & row).bit_count() % 2 == 0 for row in self.binary)] + need(len(self.dual) == 16, 'source dual dimension') + self.signatures = {} + for z in range(256): + sig = sum(((z & row).bit_count() % 2) << i for i, row in enumerate(self.binary)) + self.signatures.setdefault(sig, []).append(z) + self.pairs = [None]*8 + for i, a in enumerate(self.m): + for k in range(i+1, len(self.m)): + b = self.m[k] + for ca, cb in product((-1, 1), repeat=2): + value = [ca*x+cb*y for x, y in zip(a, b)] + support = [j for j, x in enumerate(value) if x] + if len(support) == 1 and value[support[0]] == 2: + j = support[0] + if self.pairs[j] is None: + self.pairs[j] = (i, ca, k, cb) + need(all(p is not None for p in self.pairs), 'source two-unit lattice witnesses') + + def mul(self, q): + return [sum(a*b for a, b in zip(row, q)) for row in self.m] + + def transpose(self, x): + return [sum(row[j]*a for row, a in zip(self.m, x)) for j in range(8)] + + @staticmethod + def guard(g): + need(type(g) is int and g >= 0, 'nonnegative integer relative guard required') + need(g <= 16, 'guard budget exceeded: no decision') + + def maximum(self, g): + self.guard(g) + if g == 0: + return 13**8 + step = 1 << (g-1) + length = ceildiv(13, step) + a, b = (length+1)//2, length//2 + return sum(a**(8-z.bit_count())*b**z.bit_count() for z in self.dual) + + def forward(self, x, g): + self.guard(g) + x = intvector(x, 112) + scale = 1 << g + q = [round52(scale*t) for t in self.transpose(x)] + correction = self.mul(q) + return [scale*a-b for a, b in zip(x, correction)], q + + def choices(self, y): + s = self.transpose(y) + choices = [] + for value in s: + low, high = ceildiv(-26-value, 4), (26-value)//4 + allowed = [q for q in range(low, high+1) if round52(value+56*q) == q] + need(len(allowed) <= 13, 'scalar fiber ceiling') + choices.append(allowed) + return choices + + def blocks(self, y, g): + self.guard(g) + y = intvector(y, 112) + choices = self.choices(y) + if g == 0: + patterns = [None] + base, step = [0]*8, 0 + else: + step = 1 << (g-1) + base = [] + for i, ca, k, cb in self.pairs: + rhs = -ca*y[i]-cb*y[k] + if rhs % 2: + return [] + base.append((rhs//2) % step) + mb = self.mul(base) + residual = [-a-b for a, b in zip(y, mb)] + if any(a % step for a in residual): + return [] + signature = sum(((a//step) & 1) << i for i, a in enumerate(residual)) + patterns = self.signatures.get(signature, []) + blocks = [] + for pattern in patterns: + if g == 0: + lists = choices + else: + residues = [base[j]+step*((pattern >> j) & 1) for j in range(8)] + modulus = 1 << g + lists = [[q for q in values if q % modulus == residue] + for values, residue in zip(choices, residues)] + count = 1 + for values in lists: + count *= len(values) + if count: + blocks.append((lists, count)) + need(sum(count for _, count in blocks) <= self.maximum(g), 'source precision/state ceiling') + return blocks + + def encode(self, x, g): + y, q = self.forward(x, g) + blocks = self.blocks(y, g) + offset = 0 + for lists, count in blocks: + if all(v in values for v, values in zip(q, lists)): + rank = 0 + for v, values in zip(q, lists): + rank = rank*len(values)+values.index(v) + maximum = self.maximum(g) + return {'source_sha256': self.fingerprint, 'g': g, 'y': y, 'tag': offset+rank, + 'fiber_states': sum(n for _, n in blocks), 'worst_case_states': maximum, + 'tag_bits': (maximum-1).bit_length()} + offset += count + raise ValueError('true quotient missing from exact fiber') + + def recover(self, y, g, tag): + need(type(tag) is int and tag >= 0, 'nonnegative integer tag required') + blocks = self.blocks(y, g) + for lists, count in blocks: + if tag < count: + q = [0]*8 + for j in range(7, -1, -1): + q[j] = lists[j][tag % len(lists[j])] + tag //= len(lists[j]) + correction = self.mul(q) + numerator = [a+b for a, b in zip(y, correction)] + scale = 1 << g + need(all(v % scale == 0 for v in numerator), 'coarse input lattice') + x = [v//scale for v in numerator] + output, original_q = self.forward(x, g) + need(output == y and original_q == q, 'exact source reconstruction') + return x + tag -= count + raise ValueError('tag outside this output fiber') + + def decode(self, packet): + need(isinstance(packet, dict) and set(packet) == {'source_sha256', 'g', 'y', 'tag', + 'fiber_states', 'worst_case_states', 'tag_bits'}, 'exact encoding fields required') + need(packet['source_sha256'] == self.fingerprint, 'source binding') + g = packet['g']; self.guard(g) + blocks = self.blocks(packet['y'], g) + maximum = self.maximum(g) + need(type(packet['fiber_states']) is int and packet['fiber_states'] == sum(n for _, n in blocks), + 'fiber count binding') + need(type(packet['worst_case_states']) is int and packet['worst_case_states'] == maximum, + 'worst-case count binding') + need(type(packet['tag_bits']) is int and packet['tag_bits'] == (maximum-1).bit_length(), + 'tag bit binding') + return self.recover(packet['y'], g, packet['tag']) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('mode', choices=('encode', 'decode', 'table')) + parser.add_argument('file', nargs='?') + args = parser.parse_args() + geometry = Geometry() + if args.mode == 'table': + result = [{'relative_guard_bits': g, 'states': geometry.maximum(g), + 'tag_bits': (geometry.maximum(g)-1).bit_length(), + 'fractional_slots_plus_tag': 112*g+(geometry.maximum(g)-1).bit_length()} + for g in range(6)] + else: + need(args.file is not None, 'input file required') + packet = load(args.file) + if args.mode == 'encode': + need(isinstance(packet, dict) and set(packet) == {'g', 'x'}, 'encode input fields') + result = geometry.encode(packet['x'], packet['g']) + else: + result = {'status': 'RECOVERED_EXACT_INPUT', 'x': geometry.decode(packet)} + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main() diff --git a/research/precision-state-frontier/history.py b/research/precision-state-frontier/history.py new file mode 100644 index 0000000000..e3344cfbb3 --- /dev/null +++ b/research/precision-state-frontier/history.py @@ -0,0 +1,47 @@ +#!/usr/bin/env python3 +"""Necessary state/precision budgets; exact for the declared same-grid chain. + +Apache-2.0; substantial OpenAI Codex assistance. Unbounded integer-domain +theorem, or sufficiently large input ranges; not a paid-query lower bound. +""" +import argparse +import json +from frontier import load, need + + +def budget(rounds, components=1, total_relative_guard_bits=0, side_states=1): + need(type(rounds) is int and rounds >= 1, 'positive round count') + need(type(components) is int and components >= 1, 'positive component count') + need(type(total_relative_guard_bits) is int and total_relative_guard_bits >= 0, + 'nonnegative total relative refinement') + need(type(side_states) is int and side_states >= 1, 'positive side alphabet') + exponent = 8*rounds*components + need(exponent <= 10000, 'integer budget exceeded: no decision') + numerator = 13**exponent + fractional_slots = 112*components*total_relative_guard_bits + if fractional_slots >= numerator.bit_length(): + minimum = 1 + else: + denominator = (1 << fractional_slots)*side_states + minimum = (numerator+denominator-1)//denominator + sharp = total_relative_guard_bits == 0 and side_states == 1 + return {'status': 'SHARP_SAME_GRID_HISTORY' if sharp else 'NECESSARY_HISTORY_BOUND', + 'rounds': rounds, 'components': components, + 'minimum_history_states': minimum, 'minimum_packed_bits': (minimum-1).bit_length(), + 'new_fractional_slots': fractional_slots, 'side_states': side_states, + 'large_input_range_required': True, + 'scope': 'Fixed known unimodular frames, bounded rounding residuals, all initial inputs recoverable. Refined/side-information bounds are necessary, not claimed attainable.'} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('file') + args = parser.parse_args() + data = load(args.file) + need(isinstance(data, dict) and set(data) <= {'rounds', 'components', + 'total_relative_guard_bits', 'side_states'} and 'rounds' in data, 'budget fields') + print(json.dumps(budget(**data), sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main() diff --git a/research/precision-state-frontier/mutation_check.py b/research/precision-state-frontier/mutation_check.py new file mode 100644 index 0000000000..4968c21618 --- /dev/null +++ b/research/precision-state-frontier/mutation_check.py @@ -0,0 +1,62 @@ +#!/usr/bin/env python3 +"""Bounded semantic controls against private copies, never source edits. + +Apache-2.0; substantial OpenAI Codex assistance. +""" +from pathlib import Path +import hashlib +import json +import os +import shutil +import subprocess +import sys +import tempfile + +ROOT = Path(__file__).resolve().parent + +MUTANTS = ( + ('half-ties-toward-zero', 'frontier.py', + '(abs(value)+26)//52', '(abs(value)+25)//52'), + ('ignore-binary-coset', 'frontier.py', + 'patterns = self.signatures.get(signature, [])', 'patterns = list(range(256))'), + ('forget-relative-input-scale', 'frontier.py', + 'q = [round52(scale*t) for t in self.transpose(x)]', + 'q = [round52(t) for t in self.transpose(x)]'), + ('omit-weight-four-words', 'frontier.py', + 'for z in self.dual)', 'for z in self.dual if z.bit_count() != 4)'), + ('reuse-history-after-every-round', 'history.py', + 'exponent = 8*rounds*components', 'exponent = 8*components'), +) + + +def main(): + results = [] + with tempfile.TemporaryDirectory(prefix='precision-state-mutations-') as temporary: + for name, filename, before, after in MUTANTS: + target = Path(temporary)/name + shutil.copytree(ROOT, target, ignore=shutil.ignore_patterns('__pycache__')) + path = target/filename + original = path.read_text() + if original.count(before) != 1: + raise ValueError('mutation anchor is not unique: '+name) + path.write_text(original.replace(before, after)) + modes = [] + for optimized in (False, True): + command = [sys.executable, '-B']+(['-O'] if optimized else [])+[str(target/'verify.py')] + result = subprocess.run(command, cwd=temporary, capture_output=True, text=True, + timeout=30, env={**os.environ, 'PYTHONDONTWRITEBYTECODE':'1'}) + if result.returncode == 0 or 'PASS_PRECISION_STATE_FRONTIER' in result.stdout: + raise ValueError('semantic mutant survived: '+name) + lines = result.stderr.strip().splitlines() + if not lines or not lines[-1].startswith('ValueError:'): + raise ValueError('mutant failed outside a semantic check: '+name) + modes.append({'optimized':optimized, 'exit_code':result.returncode, + 'rejection':lines[-1]}) + results.append({'name':name, 'file':filename, + 'original_sha256':hashlib.sha256(original.encode()).hexdigest(), + 'replacement':{'before':before, 'after':after}, 'modes':modes}) + print(json.dumps({'status':'PASS_SEMANTIC_MUTATION_CONTROLS', 'mutants':results}, + sort_keys=True, indent=2)) + + +if __name__ == '__main__':main() diff --git a/research/precision-state-frontier/source/kernel.py b/research/precision-state-frontier/source/kernel.py new file mode 100644 index 0000000000..70b5d65cae --- /dev/null +++ b/research/precision-state-frontier/source/kernel.py @@ -0,0 +1,152 @@ +"""Bounded bit-word implementation of the pinned eight-mode inverse code. + +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. +""" + + +def word_width(bound): + if type(bound) is not int or bound < 0: + raise ValueError("bound must be a nonnegative integer") + return (56 * bound + 2).bit_length() + 1 + + +def encode(value, width): + if not -(1 << (width - 1)) <= value < (1 << (width - 1)): + raise ValueError("signed input does not fit") + return [(value >> bit) & 1 for bit in range(width)] + + +def decode(word): + return sum(bit << index for index, bit in enumerate(word[:-1])) - (word[-1] << (len(word) - 1)) + + +def check_word(word, width): + if len(word) != width or any(type(bit) is not int or bit not in (0, 1) for bit in word): + raise ValueError("expected a fixed-width binary word") + + +def add_into(target, source, sign): + """Ripple ADD/SUB modulo 2^W; the invocation range proof excludes overflow.""" + carry = int(sign == -1) + flip = carry + for index, source_bit in enumerate(source): + total = target[index] + (source_bit ^ flip) + carry + target[index] = total & 1 + carry = total >> 1 + + +def negate_if(word, negative): + carry = negative + for index, bit in enumerate(word): + total = (bit ^ negative) + carry + word[index] = total & 1 + carry = total >> 1 + + +def clear(word): + for index in range(len(word)): + word[index] = 0 + + +def within_bound(word, limit, work): + for index, bit in enumerate(word): + work[index] = bit + negate_if(work, word[-1]) + comparison = 0 + for index in range(len(word) - 1, -1, -1): + if comparison == 0 and work[index] != limit[index]: + comparison = 1 if work[index] > limit[index] else -1 + clear(work) + return comparison <= 0 + + +def round52_into(word, work): + """Nearest integer to signed word/52; exact ties go away from zero. + + The only division loop has 13 remainder states and consumes one bit. + No integer division or remainder instruction is used. + """ + negative = word[-1] + for index, bit in enumerate(word): + work[index] = bit + negate_if(work, negative) + low = work[0] + 2 * work[1] + clear(word) + remainder = 0 + for index in range(len(work) - 1, 1, -1): + trial = 2 * remainder + work[index] + digit = int(trial >= 13) + remainder = trial - 13 * digit + word[index - 2] = digit + carry = int(4 * remainder + low >= 26) + for index, bit in enumerate(word): + total = bit + carry + word[index] = total & 1 + carry = total >> 1 + negate_if(word, negative) + clear(work) + + +def tape_invoice(width, components=1): + """Constructive upper bounds in the explicitly described fixed multitape ABI.""" + if type(width) is not int or width < 3 or type(components) is not int or components < 0: + raise ValueError("invalid tape geometry") + return { + "components_per_owner": components, + "word_bits": width, + "signed_adds": 896 * components, + "round52_calls": 8 * components, + "range_checks": 112 * components, + "external_clear_scans": 9 + 8 * components, + "internal_divider_clear_scans": 16 * components, + "internal_range_clear_scans": 112 * components, + "recursive_calls": 0, + "owned_word_slots": 9, + "owned_cells": 9 * (width + 1), + "owner_cells": 112 * (components * (width + 1) + 1), + "readonly_bound_cells": width + 1, + "transition_upper": components * (2898 * width + 5922) + 18 * width + 100, + "head_moves_upper": 122 * (components * (2898 * width + 5922) + 18 * width + 100), + } + + +def recode(owner_words, mode_columns, bound, scratch): + """Mutate 112 owner words, returning every one of the nine owned words clean. + + Input/output words use the same grid 2^-P; P is a representation parameter. + Borrowed helper tapes are absent from this arithmetic interface. + """ + width = word_width(bound) + if len(owner_words) != 112 or len(mode_columns) != 8 or len(scratch) != 9: + raise ValueError("expected 112 owners, eight modes and nine owned words") + all_words = owner_words + scratch + if len({id(word) for word in all_words}) != len(all_words): + raise ValueError("owner and scratch words must be physically distinct") + for word in all_words: + check_word(word, width) + if any(len(column) != 112 or any(type(c) is not int or c not in (-1, 0, 1) for c in column) + for column in mode_columns): + raise ValueError("invalid mode coefficients") + if any(sum(c != 0 for c in column) != 56 for column in mode_columns) or any( + sum(column[index] != 0 for column in mode_columns) != 4 for index in range(112)): + raise ValueError("mode incidence does not satisfy the numerical ABI") + for word in scratch: + clear(word) + modes, work = scratch[:8], scratch[8] + limit = encode(bound, width) + for word in owner_words: + if not within_bound(word, limit, work): + raise ValueError("input exceeds the numerical ABI") + for column, target in zip(mode_columns, modes): + for source, sign in zip(owner_words, column): + if sign: + add_into(target, source, sign) + for mode in modes: + round52_into(mode, work) + for index, target in enumerate(owner_words): + for mode, column in zip(modes, mode_columns): + if column[index]: + add_into(target, mode, -column[index]) + for word in modes: + clear(word) + return tape_invoice(width) diff --git a/research/precision-state-frontier/test_package.py b/research/precision-state-frontier/test_package.py new file mode 100644 index 0000000000..fdd46a1510 --- /dev/null +++ b/research/precision-state-frontier/test_package.py @@ -0,0 +1,76 @@ +#!/usr/bin/env python3 +"""Read-only portable replay and CLI controls; Python 3.10+, standard library. + +Apache-2.0; substantial OpenAI Codex assistance. +""" +from pathlib import Path +import hashlib +import json +import os +import shutil +import subprocess +import sys +import tempfile + +from frontier import Geometry, ROOT, need + + +def main(): + geo = Geometry() + expected = (ROOT/'RESULT.json').read_bytes() + with tempfile.TemporaryDirectory(prefix='precision-state-portable-') as temporary: + outer = Path(temporary) + package = outer/'package' + shutil.copytree(ROOT, package, ignore=shutil.ignore_patterns('__pycache__')) + for path in package.rglob('*'): + path.chmod(0o555 if path.is_dir() else 0o444) + package.chmod(0o555) + environment = {key:value for key,value in os.environ.items() if not key.startswith('PYTHON')} + environment.update(PATH='', PYTHONDONTWRITEBYTECODE='1', + PYTHONPYCACHEPREFIX=str(outer/'fresh-pycache')) + def run(script, arguments=(), optimized=False, success=True): + command = [sys.executable, '-B']+(['-O'] if optimized else [])+[str(package/script), *arguments] + result = subprocess.run(command, cwd=outer, env=environment, capture_output=True, timeout=30) + need((result.returncode == 0) == success, 'portable CLI exit: '+script) + if success:need(not result.stderr, 'portable warnings or stderr: '+script) + return result.stdout + for optimized in (False, True): + need(run('verify.py', optimized=optimized) == expected, 'portable exact receipt') + # Exercise the published JSON interfaces with a nontrivial 16-state + # fiber and with a tag-free relative-five-bit input. + cli_roundtrips = [] + for g in (4, 5): + y = [-v for v in geo.mul([4]*8)] + x = geo.recover(y, g, 15) if g == 4 else [i-56 for i in range(112)] + source = outer/('input-'+str(g)+'.json') + source.write_text(json.dumps({'g':g, 'x':x})) + encoded = run('frontier.py', ('encode', str(source))) + packet = json.loads(encoded) + need(packet['worst_case_states'] == (16 if g == 4 else 1), 'CLI frontier state bound') + encoded_file = outer/('encoded-'+str(g)+'.json');encoded_file.write_bytes(encoded) + recovered = json.loads(run('frontier.py', ('decode', str(encoded_file)), optimized=True)) + need(recovered['x'] == x, 'CLI exact recovery') + cli_roundtrips.append({'relative_bits':g, 'states':packet['worst_case_states']}) + budget_file = outer/'budget.json' + budget_file.write_text(json.dumps({'rounds':18})) + result = json.loads(run('history.py', (str(budget_file),))) + need(result['minimum_packed_bits'] == 533, 'CLI history budget') + duplicate = outer/'duplicate.json';duplicate.write_text('{"g":0,"g":1,"x":[]}') + run('frontier.py', ('encode', str(duplicate)), success=False) + forged = json.loads(encoded);forged['tag']=1 + forged_file=outer/'forged.json';forged_file.write_text(json.dumps(forged)) + run('frontier.py', ('decode', str(forged_file)), optimized=True, success=False) + invalid_budget=outer/'invalid-budget.json';invalid_budget.write_text('{"rounds":true}') + run('history.py', (str(invalid_budget),), success=False) + need(not (outer/'fresh-pycache').exists(), 'no package-side or external bytecode writes') + # Restore write permission only to clean this temporary export. + for path in package.rglob('*'): + path.chmod(0o755 if path.is_dir() else 0o644) + package.chmod(0o755) + print(json.dumps({'status':'PASS_PORTABLE_PRECISION_STATE_PACKAGE', + 'normal_and_optimized_receipt_sha256':hashlib.sha256(expected).hexdigest(), + 'empty_path':True, 'read_only_package':True, 'cli_roundtrips':cli_roundtrips, + 'history_cli_bits':533, 'cli_rejections':3}, sort_keys=True, indent=2)) + + +if __name__ == '__main__':main() diff --git a/research/precision-state-frontier/verify.py b/research/precision-state-frontier/verify.py new file mode 100644 index 0000000000..23e25cad83 --- /dev/null +++ b/research/precision-state-frontier/verify.py @@ -0,0 +1,275 @@ +#!/usr/bin/env python3 +"""Exact finite calibration of the proof and constructive source codec. + +Apache-2.0; substantial OpenAI Codex assistance. No full physical caller. +""" +from collections import Counter +from copy import deepcopy +from fractions import Fraction +from itertools import product +from pathlib import Path +import argparse +import hashlib +import importlib.util +import json +import random + +from frontier import Geometry, ROOT, load, need +from history import budget + + +def source_facts(geo): + m = geo.m + gram = [[sum(row[i]*row[j] for row in m) for j in range(8)] for i in range(8)] + need(gram == [[56*int(i == j) for j in range(8)] for i in range(8)], 'full source Gram') + need(all(sum(v != 0 for v in row) == 4 for row in m), 'source row support') + code = {0} + for row in geo.binary: + code |= {x ^ row for x in list(code)} + need(code == set(geo.dual) and len(code) == 16, 'source self-dual binary code') + need(Counter(v.bit_count() for v in code) == {0: 1, 4: 14, 8: 1}, 'weight enumerator') + need(all((a & b).bit_count() % 2 == 0 for a in code for b in code), 'complete self-orthogonality') + for j, (i, ca, k, cb) in enumerate(geo.pairs): + need([ca*a+cb*b for a, b in zip(m[i], m[k])] == [2*int(j == h) for h in range(8)], + 'integer two-unit row combination') + congruences = 0 + rng = random.Random(20261024) + for g in range(1, 8): + step = 1 << (g-1) + vectors = [[step*((mask >> j) & 1) for j in range(8)] for mask in range(256)] + vectors += [[rng.randrange(-65, 66) for _ in range(8)] for _ in range(32)] + for q in vectors: + direct = all(v % (1 << g) == 0 for v in geo.mul(q)) + predicted = all(v % step == 0 for v in q) and sum(((q[j]//step) & 1) << j for j in range(8)) in code + need(direct == predicted, 'dyadic source lattice classification') + congruences += 1 + cosets = 0 + for a, b in ((7, 6), (4, 3), (2, 2), (1, 1), (1, 0)): + counts = [sum(a**(8-(v ^ z).bit_count())*b**(v ^ z).bit_count() for v in code) for z in range(256)] + need(max(counts) == counts[0], 'coset enumerator upper bound') + cosets += len(counts) + return {'gram_entries': 64, 'binary_codewords': sorted(code), + 'weight_enumerator': {'0': 1, '4': 14, '8': 1}, + 'two_unit_witnesses': [list(x) for x in geo.pairs], + 'dyadic_congruence_cases': congruences, 'coset_enumerator_cases': cosets} + + +def scalar_candidates(geo): + cases = 0 + # Independent Fraction nearest rounding, including both exact tie signs. + def independent(t): + value = Fraction(t, 52) + whole = abs(value.numerator)//value.denominator + fraction = abs(value)-whole + answer = whole+int(fraction >= Fraction(1, 2)) + return answer if value >= 0 else -answer + for s in range(-160, 161): + candidates = [q for q in range(-100, 101) if independent(s+56*q) == q] + low = -((26+s)//4) + high = (26-s)//4 + # Recover the mode list through a separately evaluated interval rule. + interval = [q for q in range(low, high+1) if independent(s+56*q) == q] + need(candidates == interval and len(interval) <= 13, 'complete scalar fiber interval') + if interval: + need(interval == list(range(min(interval), max(interval)+1)), 'contiguous scalar fiber') + cases += 1 + return cases + + +def frontier_suite(geo): + rng = random.Random(53) + expected = [815730721, 51008161, 362401, 4096, 16, 1] + h_bound = [24, 12, 6, 16, 14, 0] + rows, inverse_cases = [], 0 + for g, maximum in enumerate(expected): + a = 2 if g == 3 else 4 if g == 4 else 0 + y = [-v for v in geo.mul([a]*8)] + count = sum(n for _, n in geo.blocks(y, g)) + need(count == maximum == geo.maximum(g), 'attaining worst-case fiber') + tags = set(range(count)) if count <= 16 else {0, count-1, count//2} | {rng.randrange(count) for _ in range(17)} + seen = set() + for tag in sorted(tags): + x = geo.recover(y, g, tag) + packet = geo.encode(x, g) + need(packet['tag'] == tag and packet['y'] == y and geo.decode(packet) == x, + 'rank/unrank attaining fiber') + need(max(map(abs, x)) <= h_bound[g], 'explicit finite input range') + seen.add(tuple(x)); inverse_cases += 1 + need(len(seen) == len(tags), 'distinct preimages') + rows.append({'relative_guard': g, 'maximum_fiber': maximum, + 'packed_bits': (maximum-1).bit_length(), 'attaining_input_bound': h_bound[g], + 'sampled_tags': len(tags), 'fractional_slots_plus_tag':112*g+(maximum-1).bit_length()}) + random_cases = 0 + for g in range(9): + for magnitude in (0, 1, 26, 10**6): + x = [rng.randrange(-magnitude, magnitude+1) for _ in range(112)] + packet = geo.encode(x, g) + need(geo.decode(packet) == x, 'arbitrary-input exact codec') + need(packet['fiber_states'] <= geo.maximum(g), 'per-output fiber cap') + if g >= 5: + need(packet['tag'] == 0 and packet['fiber_states'] == 1, 'relative-five-bit injectivity') + random_cases += 1 + return {'frontier': rows, 'attaining_fiber_roundtrips': inverse_cases, + 'other_input_roundtrips': random_cases} + + +def source_kernel(geo): + sources = load(ROOT/'SOURCES.json') + kernel_path = ROOT/'source/kernel.py' + need(hashlib.sha256(kernel_path.read_bytes()).hexdigest() == sources['vendored_kernel_sha256'], + 'unchanged finite-kernel bytes') + spec = importlib.util.spec_from_file_location('pinned_inverse_kernel', kernel_path) + module = importlib.util.module_from_spec(spec); spec.loader.exec_module(module) + rng = random.Random(13) + cases = 0 + for g in range(6): + fixtures = [[0]*112, [26 if i == 0 else 0 for i in range(112)], + [-26 if i == 0 else 0 for i in range(112)], + [rng.randrange(-40, 41) for _ in range(112)]] + for x in fixtures: + scaled = [(1 << g)*a for a in x] + bound = max(map(abs, scaled)) + width = module.word_width(bound) + words = [module.encode(a, width) for a in scaled] + scratch = [module.encode(1 if i % 2 else -1, width) for i in range(9)] + module.recode(words, list(map(list, zip(*geo.m))), bound, scratch) + output = [module.decode(w) for w in words] + want, _ = geo.forward(x, g) + need(output == want and all(not any(w) for w in scratch), 'literal source kernel and owned return') + # Compare to exact linear A^-1, not a falsely linear rounded map. + t = geo.transpose(scaled) + exact = [Fraction(a)-sum(Fraction(c*b, 52) for c, b in zip(row, t)) + for a, row in zip(scaled, geo.m)] + need(max(abs(Fraction(a)-b) for a, b in zip(output, exact)) <= 2, 'source error in output-grid units') + cases += 1 + return cases + + +def histories(geo): + rng = random.Random(197) + stationary = [] + for rounds in range(1, 7): + radius = (13**rounds-1)//2 + for _ in range(8): + modes = [rng.randrange(-radius, radius+1) for _ in range(8)] + x = geo.mul(modes) + z = x + for _ in range(rounds): + z, _ = geo.forward(z, 0) + need(not any(z) and max(map(abs, x)) <= 2*(13**rounds-1), 'stationary growing zero fiber') + x = geo.mul([radius]*8) + z = x + for _ in range(rounds-1):z, _ = geo.forward(z, 0) + need(any(z), 'history depth discriminator') + b = budget(rounds) + need(b['minimum_history_states'] == 13**(8*rounds), 'sharp history alphabet') + stationary.append({'rounds': rounds, 'zero_fiber_states':13**(8*rounds), + 'sufficient_input_bound':2*(13**rounds-1), + 'packed_bits':b['minimum_packed_bits']}) + # Source-sized changing signed-permutation frames: retain only each tag, + # reconstructing each earlier output from the final state while reversing. + framed = 0 + for rounds in (2, 4, 6): + original = [rng.randrange(-1000, 1001) for _ in range(112)] + z = list(original); log = [] + for _ in range(rounds): + permutation = list(range(112)); rng.shuffle(permutation) + signs = [rng.choice((-1, 1)) for _ in range(112)] + u = [s*z[j] for s, j in zip(signs, permutation)] + packet = geo.encode(u, 0) + out = [0]*112 + for i, j in enumerate(permutation):out[j]=signs[i]*packet['y'][i] + z = out; log.append((permutation, signs, packet['tag'])) + for permutation, signs, tag in reversed(log): + out = [s*z[j] for s, j in zip(signs, permutation)] + u = geo.recover(out, 0, tag) + z = [0]*112 + for i, j in enumerate(permutation):z[j]=signs[i]*u[i] + need(z == original, 'changing-frame reverse recovery') + framed += 1 + for t in range(1, 9): + for g in range(3): + for side in (1, 3, 13**4): + got = budget(t, 1, g, side) + num, den = 13**(8*t), (1 << (112*g))*side + need(got['minimum_history_states'] == (num+den-1)//den, 'precision/side-state conservation arithmetic') + return {'stationary':stationary,'changing_frame_roundtrips':framed, + 'budget_cases':72,'eighteen_same_grid_rounds':budget(18)} + + +def noncommuting_volume_controls(): + def nearest(v, b): + return (1 if v >= 0 else -1)*((2*abs(v)+b)//(2*b)) + def step(z, frame): + a, b = z + if frame == 0:a += b + else:b += a + a, b = a-3*nearest(a, 2), b-5*nearest(b, 4) + if frame == 0:a -= b + else:b -= a + return a, b + results = [] + for bound, frames in ((64, (0, 1)), (128, (0, 1)), (256, (0, 1, 0))): + counts = Counter() + for a in range(-bound, bound+1): + for b in range(-bound, bound+1): + z = a, b + for frame in frames:z = step(z, frame) + counts[z] += 1 + maximum = max(counts.values()) + expected = 60 if bound == 64 else 8**len(frames) + need(maximum == expected, 'finite-window noncommuting volume control') + results.append({'input_bound':bound,'frames':list(frames),'inputs':(2*bound+1)**2, + 'maximum_fiber_in_window':maximum,'unbounded_maximum':8**len(frames)}) + return results + + +def rejections(geo): + good = geo.encode([13 if i == 0 else 0 for i in range(112)], 1) + cases = [] + def reject(name, packet): + try:geo.decode(packet) + except (ValueError, TypeError):cases.append(name) + else:raise ValueError('invalid packet accepted: '+name) + for name, key, value in (('wrong-source','source_sha256','0'*64), + ('wrong-fiber','fiber_states',-1), + ('wrong-bound','worst_case_states',1), + ('wrong-bits','tag_bits',0), + ('negative-tag','tag',-1), + ('out-of-fiber-tag','tag',good['fiber_states']), + ('boolean-guard','g',True)): + packet=deepcopy(good);packet[key]=value;reject(name,packet) + packet=deepcopy(good);packet['y'][0]=0.5;reject('float-output',packet) + packet=deepcopy(good);packet['y'].pop();reject('missing-owner',packet) + # Changing precision on an existing same-grid packet is not refinement. + packet=geo.encode([13 if i==0 else 0 for i in range(112)],0);packet['g']=5 + reject('absolute-guard-is-not-relative-refinement',packet) + return cases + + +def authenticate_source(root): + sources=load(ROOT/'SOURCES.json') + for row in sources['files']: + need(hashlib.sha256((Path(root)/row['path']).read_bytes()).hexdigest()==row['sha256'], + 'canonical source hash: '+row['path']) + normal=load(Path(root)/'research/coded-native-caller/NORMALIZERS.json') + need(normal['mode_columns']==load(ROOT/'FIXTURE.json')['mode_columns'], 'literal source columns') + + +def main(): + parser=argparse.ArgumentParser(description=__doc__) + parser.add_argument('--source-root') + parser.add_argument('--suite',choices=('all','core'),default='all') + args=parser.parse_args();geo=Geometry() + result={'status':'PASS_PRECISION_STATE_FRONTIER','source_facts':source_facts(geo), + 'scalar_intervals':scalar_candidates(geo),'recovery':frontier_suite(geo), + 'rejections':rejections(geo)} + if args.suite=='all': + result['unchanged_kernel_calls']=source_kernel(geo) + result['histories']=histories(geo) + result['noncommuting_volume_controls']=noncommuting_volume_controls() + if args.source_root:authenticate_source(args.source_root) + print(json.dumps(result,sort_keys=True,indent=2)) + + +if __name__=='__main__':main()