From 2a0cd8ccfb32ac834bfc4bcedd364a5a8c36ac8a Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 15:10:44 +0000 Subject: [PATCH] feat(research): add shared-denominator principal-window cache --- .../shared-denominator-window-cache/PROOF.md | 182 ++++++++++++++++ .../shared-denominator-window-cache/README.md | 97 +++++++++ .../SOURCES.json | 36 ++++ .../shared-denominator-window-cache/TASK.json | 144 +++++++++++++ .../VERIFY.json | 38 ++++ .../shared-denominator-window-cache/cache.py | 157 ++++++++++++++ .../shared-denominator-window-cache/verify.py | 196 ++++++++++++++++++ 7 files changed, 850 insertions(+) create mode 100644 research/shared-denominator-window-cache/PROOF.md create mode 100644 research/shared-denominator-window-cache/README.md create mode 100644 research/shared-denominator-window-cache/SOURCES.json create mode 100644 research/shared-denominator-window-cache/TASK.json create mode 100644 research/shared-denominator-window-cache/VERIFY.json create mode 100644 research/shared-denominator-window-cache/cache.py create mode 100644 research/shared-denominator-window-cache/verify.py diff --git a/research/shared-denominator-window-cache/PROOF.md b/research/shared-denominator-window-cache/PROOF.md new file mode 100644 index 0000000000..4e155d0ebb --- /dev/null +++ b/research/shared-denominator-window-cache/PROOF.md @@ -0,0 +1,182 @@ +# Shared-denominator principal-window cache + +This is a scoped written construction, produced by Nick Petalas. Finite tests +corroborate the implementation. Independent human and formal proof-kernel review +are unclaimed. No multiplication theorem or new kappa follows. + +## Boundary and theorem + +Let H be one fixed rational N by N source. For every row i, choose a positive +integer q_i clearing every denominator in that row, and put Z=diag(q) H. These +scales and the integer source Z are prepared once and retained separately. A +window J is an ordered list of m distinct source labels. An update removes its +first label and appends a label not in the retained list. The appended label may +equal the removed one. + +Assume the old principal window Z[J,J], the retained principal window B, and +the incoming principal window are nonsingular. The empty retained matrix at m=1 +has determinant one. The predecessor's weighted strict diagonal dominance is +one sufficient all-window premise. We cite that premise without replaying its +scientific checks; this construction also applies outside that class whenever +these exact nonsingularity conditions hold. + +After one exact initialization, the cache stores + + d = det Z[J,J], A = adj Z[J,J]. + +Its inverse output is represented exactly by + + H[J,J]^-1 = A diag(q_J) / d. (1) + +A slide updates d,A with integer additions, multiplications and exactly +2(m-1)^2 exact integer divisions. It uses O(m^2) arithmetic operations and +O(m^2) live integer fields. The inverse coefficient state contains m^2 integer +cofactors and one signed common determinant. It therefore removes m^2-1 +per-entry denominator fields compared with m^2 individually stored rationals. +This count excludes labels, source storage, row scales, initialization scratch +and materialized outputs. It counts representation fields, not distinct heap +objects. Common cofactors can be larger than individually reduced numerators; +no total-bit-space or runtime improvement is asserted. + +Equation (1) follows from Z_J=diag(q_J) H_J. The row scales occur on the RIGHT +of the inverse, so they multiply columns of A. A left multiplication here would +be wrong for a nonsymmetric source. + +## Delete the outgoing coordinate + +Simultaneously permute rows and columns to move the outgoing coordinate last. +This does not change the determinant. Write the correspondingly permuted cache +and source as + + adj M = [ E f ; g b ], M = [ B u0 ; v0 a0 ], + d = det M, b = det B. + +The last equality is the bottom-right cofactor identity. Since M and B are +nonsingular, the Schur inverse identity yields + + B^-1 = E/d - (f/d)(d/b)(g/d). + +Multiplication by b gives the deletion formula + + C = adj B = (b E - f g) / d. (2) + +All quotients in (2) are integers because the left side is an adjugate of an +integer matrix. The implementation uses divmod and rejects a nonzero remainder, +rather than truncating. It performs (m-1)^2 such divisions. Negative d is legal. +For m=1, A=[1], b=1 and C is empty, so (2) needs no division. + +## Border the retained matrix + +Read the incoming column u, row v and diagonal a from the SAME integer source. +Let + + p = C u, r = v C, e = a b - v p. + +The determinant formula for a bordered matrix gives + + e = det [ B u ; v a ]. + +The Schur inverse formula, multiplied by e, gives its adjugate + + A_new = [ (e C + p r)/b -p ; + -r b ], d_new=e. (3) + +In detail, B^-1=C/b and the Schur complement is e/b. The inverse top-left +block is C/b + p r/(b e); the other blocks are -p/e, -r/e and b/e. Thus (3) +holds entry by entry over the rationals. Its top-left block is integral because +it is part of an integer adjugate. There are another (m-1)^2 exact divisions. +For m=1, e=a and A_new=[1], including negative nonzero a. + +Equations (2) and (3) prove the state invariant by induction over every finite +sequence of legal slides. The induction does not retain an expanding product +of historic denominators. Both row and column order are part of the invariant. +Incoming singularity or a zero deletion pivot is rejected before publication +of a new state. The old immutable cache remains available after every failure. + +These are classical Schur and determinantal-condensation identities. The new +contribution is their composition as a shared-denominator sliding cache with +an explicit persistent state, rational-source orientation and bounded integer +implementation. It does not claim invention of the underlying identities. + +## Heights do not grow with the number of slides + +Put C0=max(1,max_ij |Z_ij|), Q=max_i q_i, k=m-1, and + + L = m! C0^m. + +Leibniz expansion bounds every stored determinant by L and every stored +cofactor by (m-1)! C0^(m-1), hence also by L. Retained determinants and cofactors +satisfy the same common bound. These estimates depend on the fixed source and +window width, not on the number of preceding slides. + +A deletion numerator has magnitude at most 2 L^2. Each component of p or r +has magnitude at most k L C0. During evaluation of e, the absolute sum is at +most L C0 + k^2 L C0^2. Once e is formed it is a determinant and has magnitude +at most L. A bordering numerator is at most + + L^2 (1 + k^2 C0^2). + +These bounds also cover partial sums by the triangle inequality. The integer +numerators in (1) have magnitude at most L Q. Thus stored and temporary bit +heights are polynomial in m, log C0 and log Q, uniformly over the slide count. +The quotient and remainder do not require an unbounded denominator chain. + +If every input numerator and denominator has magnitude less than 2^B, row-wise +least-common-multiple clearing gives q_i <= 2^(NB) and +C0 <= 2^((N+1)B). Initial clearing is global-source work, not free per-window +normalization. Row scaling can substantially enlarge integers. Bit arithmetic, +source access, output formation and exact initialization must all be charged. + +## Implementation and finite evidence + +`initialize` validates the bounded rational source and distinct ordered labels. +It uses classical pivoted Bareiss determinant elimination and one dense rational +inverse to obtain the integer adjugate. No Fraction survives in the cache. This +adds a separately paid determinant computation to dense initialization. The +constructor also clears N^2 source entries, using row-wise denominator lcms; +the subsequent dense initialization is O(m^3) rational/integer arithmetic. +No faster setup is claimed. +The mathematical update accepts any exact initial adjugate/determinant pair. + +`slide`, `delete_first` and `border` contain only integer arithmetic. They build +a new immutable cache and share the original source and row scales. The explicit +`materialize` adapter creates reduced Fractions only when requested; it is not +called by a slide. Storing its output reinstates per-entry denominators and its +additional output storage is payable. The integer numerator adapter costs +m^2 multiplications and leaves the shared determinant intact. + +The implementation supports 1<=N<=32, 1<=m<=min(N,16), and at most 256 bits +per reduced input numerator/denominator. The written formulas hold for arbitrary +finite dimensions. New evidence enumerates its own sources and slides rather +than rerunning PR3872's scientific suite. A separate Leibniz/cofactor oracle +imports neither initialization nor slide arithmetic. It checks complete ordered +windows, signed nonsymmetric rational streams, both division pivots and the +source-row orientation. The verifier emits the enumerated counts and SHA256 +bindings; no receipt is handwritten. + +Power-of-Ten inspection: all loops are bounded by the validated dimensions, +fixed census domains or explicit 48/64-step streams, and no function recurses. +Every function is below 60 lines. Invalid source/label/pivot/quotient checks use +ValueError and remain active under -O. Frozen cache values confine mutation to +local construction. Returned quotient/remainder and pivot searches are checked. +There is no dynamic code execution or callback registration. Standard dataclass +construction is the only generated method mechanism. + +Managed-runtime deviation to rule 3: CPython integers, Fractions during +initialization/materialization, tuples and temporary lists allocate dynamically. +The bounded dimensions and the height bounds above bound live arithmetic state; +a slide retains only a constant number of O(m^2) arrays. The caller must account +for any old cache states or materialized outputs it retains. Follow-up physical +integration must provide its own fixed storage allocator and include conversion, +allocation, erasure and routing costs. No such program is supplied here. +Warning-strict normal and optimized runs are registered; external static type +or lint tooling is not required by the repository replay contract. + +## Remaining obligations + +This is an arithmetic preparation component. It does not implement the actual +protected factor pages, a rounded Gaussian producer, a fixed-tape integer +arithmetic routine, dirty-helper operations, supplier admission or any of the +five retained framework assumptions. Production nonsingularity, initialization, +source row clearing, bit costs, page emission, input/output ownership, storage, +precision, movement and cleanup must be bound to an actual caller separately. diff --git a/research/shared-denominator-window-cache/README.md b/research/shared-denominator-window-cache/README.md new file mode 100644 index 0000000000..a3671b8416 --- /dev/null +++ b/research/shared-denominator-window-cache/README.md @@ -0,0 +1,97 @@ +# Shared-denominator sliding principal inverses + +A new exact cache stores each principal-window inverse using one signed +determinant and an integer adjugate. Every one-index slide uses integer +arithmetic with exact divisions. The inverse coefficient state removes m^2-1 +per-entry denominator fields at width m. Stored and temporary bit heights are +bounded independently of the number of slides. + +This contribution was produced by Nick Petalas. Claim type: scoped written +construction with finite exact corroboration. No new kappa or selected-frontier +change. The representation count is not a total-bit-space or runtime guarantee; +common cofactors can exceed individually reduced numerators. + +[PROOF.md](PROOF.md) states the arbitrary finite-dimension theorem, full +rational-source contract, both update identities, height bounds and limitations. +`cache.py` implements a bounded reusable constructor and slide API. `verify.py` +uses independent literal determinants and cofactors, including signed nonsymmetric +sources and rational row scaling. It produces a hash-bound JSON receipt on stdout +and writes no files. + +## Reproduce + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error research/shared-denominator-window-cache/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error research/shared-denominator-window-cache/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/shared-denominator-window-cache +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/shared-denominator-window-cache --check-source-history +``` + +Any CPython 3.12 interpreter may replace that local path. The direct status is +`PASS_SHARED_DENOMINATOR_WINDOW_CACHE`; the registered hook reports +`PASS_REGISTERED_RESEARCH_PACKAGE`. + +## New step and predecessor credit + +David Ganz / Dugongue's [PR3872](https://github.com/CrocSwap/integer-mult-bounds/pull/3872) +supplies the fixed-global-source, ordered principal-window preparation interface +and rational Schur cache. Its page-integration question motivates the smaller +cache-representation subproblem here. Its scientific results and counts are +cited, not audited or replayed. The new code imports no predecessor code. + +Credit Jose Manuel / jmbarrancoml's PR3851 for the exact old-H preparation +boundary, Chafik Boukhalfa, RaD and the retained Gaussian/FFT lineage. Adjugates, +Schur complements, Bareiss elimination and determinantal condensation are +classical. This package claims the concrete shared-denominator sliding +construction and contract, without a global literature-priority claim. +Apache-2.0. Every predecessor source and credit line remains unchanged. + +The earlier PR5119 comparison barrier concerns residual error bounds on the same +preparation family. It does not supply this integer cache representation and is +not a mathematical dependency here. + +## Scope and costs + +The cache first clears each GLOBAL source row once. Thereafter it retains the +integer source, the row scales, ordered labels, m^2 cofactors and one determinant. +It supports N<=32, m<=16 and 256-bit reduced input coefficients. Its mathematical +identities hold in all finite dimensions with the stated nonsingular principal +blocks. Returning the outgoing index is permitted. A zero retained or incoming +determinant fails without changing the previous state. + +Dense initialization, global source storage/scaling, integer bit arithmetic, +optional inverse materialization and retained output storage remain payable. +Materialization creates ordinary Fractions and reinstates their per-entry +denominators. Physical protected-page production, precision/tapes/stock, +ownership/restoration, native implementation, complete invoices and all five +framework assumptions remain open. Independent human and formal proof-kernel +review are unclaimed. + +## Overlap and scope change + +The supplier-boundary-audit card is retained verbatim in TASK.json. Its scope +changes from admission auditing to this constructive arithmetic preparation +subproblem. The selected binding-only first example passed. Main and merged PR +searches covered sliding inverses, adjugate caches, shared denominators and the +general fraction-free form. Live handoffs, active Discussions, open PRs, recent +account submissions and local reservations were checked before the advance +[CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19376727). +PR3872 is the question source and main predecessor. This is not a claim of +exhaustive novelty; sparse notes, arbitrary historical diffs and unpublished work +remain coverage limits. The broad cached report covered 598 open PRs and 6,677 +Discussion records with complete remote pagination. The local corpus searched +136 of 8,917 HEAD notes. Exact freshness and coverage limits are in TASK.json. + +## Open next questions + +1. Can one actual protected factor-page consumer use the integer numerator/common + denominator stream without materializing every rational inverse entry? + Freeze its matrix, page format and access sequence, then price normalization, + coefficient creation, output ownership and cleanup. No physical adapter is + supplied by this arithmetic cache. +2. When does row-cleared adjugate storage use fewer total bits than separately + reduced entries for a production source family? Begin with one authenticated + source and charge initialization plus every output conversion. The field-count + improvement alone does not answer that question. diff --git a/research/shared-denominator-window-cache/SOURCES.json b/research/shared-denominator-window-cache/SOURCES.json new file mode 100644 index 0000000000..53ea689791 --- /dev/null +++ b/research/shared-denominator-window-cache/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/sliding-window-inverse/PROOF.md", + "usage": "input", + "git_blob": "c95bef030bf13ee7ee836a9f81e38e26f720907d", + "sha256": "e087c64dee82b541cf563245a5c59dc5bd5236072fc96b094ead15ee848bfb3e" + }, + { + "path": "research/sliding-window-inverse/README.md", + "usage": "input", + "git_blob": "cca049dfc1981fd92f53715a067d52ee6345eb18", + "sha256": "846561df84d5dd049fa174d6b25fde8964216cdac5fb9cf6988b02e3c9c2e375" + }, + { + "path": "research/sliding-window-inverse/cache.py", + "usage": "input", + "git_blob": "db4c97557e72540be912ca1b8a4b7643afb03e5e", + "sha256": "678830c2a0d26294489fd23ddb839123b528c2c725cce8cc7ca6ac8d5b9b469a" + } + ] +} diff --git a/research/shared-denominator-window-cache/TASK.json b/research/shared-denominator-window-cache/TASK.json new file mode 100644 index 0000000000..af2c48c4cb --- /dev/null +++ b/research/shared-denominator-window-cache/TASK.json @@ -0,0 +1,144 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one changed supplier have complete source-bound native, caller, ordinary and outer admission coverage?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one latest uncovered candidate and build a delta coverage map against the selected review. For P104, #5717 changes owned-lifetime assumptions and #5719 covers exact #5713 causal premises; neither automatically transfers to #5718. For BIT, #5679/#5708 need component admission and compatible outer use. Check controls and exact source identity before reuse; stop with one resolved gap or explicit remaining obligation. A heavy full replay requires a separate serial resource budget.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "supplier admission", + "5717", + "5719", + "5708", + "owned lifetime" + ], + "existing_checks": [ + { + "scope": "PR #4088: author-checked local words, native receipts, owner/phase fill and exact moment.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Rebind and validate ordinary/outer admission with all four providers; full mixed release not established.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3801: successor scatter-boundary decision package.", + "evidence": "research/scatter-boundary-decision/README.md", + "remaining": "Consult its exact acceptance scope before any new exporter audit; not proof of a selected failure.", + "status": "author-checked", + "source_commit": "911f8800ba7a4b03603ef62c5ffc6240e53cb5fd", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Construct exact integer adjugate/determinant updates for fixed-source principal-window inverses, removing per-entry cache denominator fields.", + "scope_change_reason": "The donor requests original constructive research, not admission auditing. PR3872 page-preparation directions motivate this smaller arithmetic cache-representation subproblem; physical integration is not claimed.", + "bottleneck_link": "Arithmetic preparation side result for the retained global Gaussian source interface. It removes denominator fields in the exact cache without claiming a favorable complete native, caller or outer invoice.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved shared-denominator construction with exact finite corroboration; leave actual physical page use and bit-space comparisons as open questions.", + "outcome": "completed", + "evidence": "PROOF.md proves the exact-division update and horizon-independent heights. verify.py enumerates 729 integer sources, 19683 slides, 480 signed rational slides, 64 width-sixteen slides and explicit failure controls against independent determinant/cofactor oracles.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a protected factor-page consumer use the shared-denominator stream directly?", + "why_it_matters": "Materialization restores per-entry denominator fields and may consume the representation benefit.", + "first_step": "Bind one source/page/access sequence and price coefficient conversion, output ownership and cleanup.", + "blocked_by": "No actual physical page adapter or complete caller cost is supplied." + }, + { + "question": "When are total stored bits lower than separately reduced inverse entries?", + "why_it_matters": "Fewer denominator fields does not imply a total-bit-space improvement.", + "first_step": "Measure exact coefficient heights on one authenticated production source and include source row clearing and initialization.", + "blocked_by": "No production source-family bit-cost comparison is supplied." + } + ], + "source_question": { + "source": "PR #3872", + "author": "Dugongue", + "predecessor_author": "Dugongue", + "retained_head": "bf7d82ac703660854d1aa843d322b7518f305b70" + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19376727", + "environment": { + "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "standard library only" + }, + "claim_type": "scoped written construction with finite exact corroboration", + "unrun_obligations": [ + "Production protected factor-page adapter and complete cost", + "Physical initialization, row clearing, integer arithmetic, output conversion, storage, ownership and cleanup", + "Native supplier and five inherited framework assumptions", + "Independent human or formal proof-kernel review" + ], + "overlap": { + "canonical_main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "priority_revision": 8, + "open_prs": { + "records": 598, + "complete_pagination": true, + "fetched_at": "2026-11-03T15:02:15.720226+00:00" + }, + "discussions": { + "records": 6677, + "complete_pagination": true, + "fetched_at": "2026-11-03T15:03:34.141458+00:00" + }, + "recent_account_prs": 471, + "recent_account_since": "2026-10-27", + "local_notes": { + "records": 136, + "head_records": 8917, + "complete_head_inventory": false + }, + "targeted_terms": [ + "sliding inverse", + "adjugate cache", + "shared denominator", + "fraction-free window" + ], + "limits": "Targeted main-tree and merged body searches supplement a sparse local corpus. Arbitrary historical diffs and unpublished work are not exhaustively searched." + } +} diff --git a/research/shared-denominator-window-cache/VERIFY.json b/research/shared-denominator-window-cache/VERIFY.json new file mode 100644 index 0000000000..8023ffd813 --- /dev/null +++ b/research/shared-denominator-window-cache/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/sliding-window-inverse/PROOF.md", + "research/sliding-window-inverse/README.md", + "research/sliding-window-inverse/cache.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Independent literal determinant/cofactor census, rational source orientation, signed wide boundary cases and input/singularity/corrupted-state controls" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete scientific evidence with assertions disabled" + } + ] +} diff --git a/research/shared-denominator-window-cache/cache.py b/research/shared-denominator-window-cache/cache.py new file mode 100644 index 0000000000..6253348ffd --- /dev/null +++ b/research/shared-denominator-window-cache/cache.py @@ -0,0 +1,157 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Integer-only principal-window slides after one rational initialization.""" +from dataclasses import dataclass +from fractions import Fraction +from math import lcm + +MAX_SOURCE = 32 +MAX_WIDTH = 16 +MAX_INPUT_BITS = 256 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def exact_div(numerator, denominator): + require(denominator != 0, "zero exact-division pivot") + quotient, remainder = divmod(numerator, denominator) + require(remainder == 0, "nonintegral determinantal quotient") + return quotient + + +def validate_labels(labels, size): + labels = tuple(labels) + require(1 <= len(labels) <= min(size, MAX_WIDTH), "window width") + require(all(type(i) is int and 0 <= i < size for i in labels), "source label") + require(len(set(labels)) == len(labels), "duplicate source label") + return labels + + +def normalize_source(matrix): + size = len(matrix) + require(1 <= size <= MAX_SOURCE, "source dimension") + require(all(len(row) == size for row in matrix), "square source") + require(all(type(x) in (int, Fraction) for row in matrix for x in row), + "exact rational source entries") + rational = tuple(tuple(Fraction(x) for x in row) for row in matrix) + require(all(max(abs(x.numerator).bit_length(), x.denominator.bit_length()) + <= MAX_INPUT_BITS for row in rational for x in row), "source bit limit") + scales = tuple(lcm(*(x.denominator for x in row)) for row in rational) + integral = tuple(tuple(exact_div(x.numerator * scale, x.denominator) for x in row) + for row, scale in zip(rational, scales)) + return integral, scales + + +def integer_determinant(matrix): + """Bareiss elimination with row pivoting; used only during initialization.""" + size = len(matrix) + require(1 <= size <= MAX_WIDTH and all(len(row) == size for row in matrix), + "determinant shape") + work = [list(row) for row in matrix] + previous, sign = 1, 1 + for column in range(size - 1): + pivot_row = next((i for i in range(column, size) if work[i][column]), None) + if pivot_row is None: + return 0 + if pivot_row != column: + work[column], work[pivot_row] = work[pivot_row], work[column] + sign = -sign + pivot = work[column][column] + for i in range(column + 1, size): + for j in range(column + 1, size): + work[i][j] = exact_div(pivot * work[i][j] + - work[i][column] * work[column][j], previous) + work[i][column] = 0 + previous = pivot + return sign * work[-1][-1] + + +def initial_adjugate(matrix, determinant): + """One dense rational initialization; no Fraction is retained in the cache.""" + size = len(matrix) + work = [[Fraction(x) for x in row] + + [Fraction(i == j) for j in range(size)] for i, row in enumerate(matrix)] + for column in range(size): + pivot_row = next((i for i in range(column, size) if work[i][column]), None) + require(pivot_row is not None, "singular initial window") + work[column], work[pivot_row] = work[pivot_row], work[column] + pivot = work[column][column] + work[column] = [x / pivot for x in work[column]] + for i in range(size): + if i != column: + multiplier = work[i][column] + work[i] = [x - multiplier * y for x, y in zip(work[i], work[column])] + adjugate = [[x * determinant for x in row[size:]] for row in work] + require(all(x.denominator == 1 for row in adjugate for x in row), + "integral initial adjugate") + return tuple(tuple(x.numerator for x in row) for row in adjugate) + + +def delete_first(adjugate, determinant): + size = len(adjugate) + order = tuple(range(1, size)) + (0,) + moved = tuple(tuple(adjugate[i][j] for j in order) for i in order) + retained_determinant = moved[-1][-1] + require(retained_determinant != 0, "singular retained principal window") + retained = tuple(tuple(exact_div(retained_determinant * moved[i][j] + - moved[i][-1] * moved[-1][j], determinant) + for j in range(size - 1)) for i in range(size - 1)) + return retained, retained_determinant + + +def border(retained, determinant, column, row, diagonal): + size = len(retained) + left = tuple(sum(retained[i][j] * column[j] for j in range(size)) + for i in range(size)) + right = tuple(sum(row[i] * retained[i][j] for i in range(size)) + for j in range(size)) + new_determinant = diagonal * determinant - sum(row[i] * left[i] for i in range(size)) + require(new_determinant != 0, "singular incoming principal window") + new_adjugate = tuple(tuple(exact_div(new_determinant * retained[i][j] + + left[i] * right[j], determinant) + for j in range(size)) + (-left[i],) for i in range(size)) + new_adjugate += (tuple(-x for x in right) + (determinant,),) + return new_adjugate, new_determinant + + +@dataclass(frozen=True) +class WindowCache: + """Construct through initialize; serialized/forged states are not an input API.""" + source: tuple[tuple[int, ...], ...] + row_scales: tuple[int, ...] + labels: tuple[int, ...] + adjugate: tuple[tuple[int, ...], ...] + determinant: int + + def slide(self, incoming): + require(type(incoming) is int and 0 <= incoming < len(self.source), + "incoming source label") + require(incoming not in self.labels[1:], "incoming aliases retained label") + retained, divisor = delete_first(self.adjugate, self.determinant) + labels = self.labels[1:] + (incoming,) + column = tuple(self.source[i][incoming] for i in labels[:-1]) + row = tuple(self.source[incoming][i] for i in labels[:-1]) + adjugate, determinant = border(retained, divisor, column, row, + self.source[incoming][incoming]) + return WindowCache(self.source, self.row_scales, labels, adjugate, determinant) + + def numerators(self): + """H[J,J] inverse is this integer matrix divided by determinant.""" + return tuple(tuple(x * self.row_scales[self.labels[j]] for j, x in enumerate(row)) + for row in self.adjugate) + + def materialize(self): + return tuple(tuple(Fraction(x, self.determinant) for x in row) + for row in self.numerators()) + + +def initialize(matrix, labels): + source, scales = normalize_source(matrix) + labels = validate_labels(labels, len(source)) + principal = tuple(tuple(source[i][j] for j in labels) for i in labels) + determinant = integer_determinant(principal) + require(determinant != 0, "singular initial window") + adjugate = initial_adjugate(principal, determinant) + return WindowCache(source, scales, labels, adjugate, determinant) diff --git a/research/shared-denominator-window-cache/verify.py b/research/shared-denominator-window-cache/verify.py new file mode 100644 index 0000000000..ef078ba57f --- /dev/null +++ b/research/shared-denominator-window-cache/verify.py @@ -0,0 +1,196 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Bounded independent cofactor oracle and generated hash-bound evidence.""" +import hashlib +import itertools +import json +from dataclasses import replace +from fractions import Fraction +from pathlib import Path +import sys + +PACKAGE = Path(__file__).resolve().parent +sys.path.insert(0, str(PACKAGE)) +from cache import exact_div, initialize, require # noqa: E402 + + +def literal_determinant(matrix): + """Leibniz formula, independent of both initialization and slide algorithms.""" + size = len(matrix) + require(size <= 5, "bounded permutation oracle") + result = 0 + for order in itertools.permutations(range(size)): + inversions = sum(order[i] > order[j] for i in range(size) for j in range(i + 1, size)) + term = (-1) ** inversions + for i in range(size): + term *= matrix[i][order[i]] + result += term + return result + + +def literal_adjugate(matrix): + size = len(matrix) + return tuple(tuple((-1) ** (i + j) * literal_determinant( + [[matrix[r][c] for c in range(size) if c != i] + for r in range(size) if r != j]) for j in range(size)) for i in range(size)) + + +def check_state(state, original): + labels = state.labels + matrix = tuple(tuple(state.source[i][j] for j in labels) for i in labels) + require(state.determinant == literal_determinant(matrix), "oracle determinant") + require(state.adjugate == literal_adjugate(matrix), "oracle adjugate") + require(type(state.determinant) is int + and all(type(x) is int for row in state.adjugate for x in row), "integer state") + actual = state.materialize() + principal = tuple(tuple(Fraction(original[i][j]) for j in labels) for i in labels) + determinant = literal_determinant(principal) + adjugate = literal_adjugate(principal) + expected = tuple(tuple(x / determinant for x in row) for row in adjugate) + require(actual == expected, "rational-source inverse orientation") + + +def initialization_census(): + nonsingular = singular = 0 + for entries in itertools.product(range(-2, 3), repeat=4): + matrix = (entries[:2], entries[2:]) + if literal_determinant(matrix): + check_state(initialize(matrix, (0, 1)), matrix) + nonsingular += 1 + else: + expect_rejection(lambda: initialize(matrix, (0, 1))) + singular += 1 + return {"nonsingular": nonsingular, "singular_rejected": singular} + + +def exhaustive_integer(): + initial_states = slides = 0 + positions = tuple((i, j) for i in range(3) for j in range(3) if i != j) + for values in itertools.product((-1, 0, 1), repeat=6): + source = [[0] * 3 for _ in range(3)] + for i in range(3): + source[i][i] = 4 + i + for (i, j), value in zip(positions, values): + source[i][j] = value + for width in range(1, 4): + for labels in itertools.permutations(range(3), width): + state = initialize(source, labels) + check_state(state, source) + initial_states += 1 + for incoming in range(3): + if incoming not in labels[1:]: + following = state.slide(incoming) + check_state(following, source) + require(following.source is state.source, "fixed global integer source") + require(state.labels == labels, "immutable predecessor state") + slides += 1 + return {"sources": 3 ** 6, "initial_states": initial_states, "slides": slides} + + +def rational_streams(): + slides = 0 + for sign_pattern in range(2): + source = [[Fraction(20 + i) if i == j else Fraction((3*i + 5*j) % 7 - 3, i+j+2) + for j in range(5)] for i in range(5)] + if sign_pattern: + source = [[(-1) ** i * x for x in row] for i, row in enumerate(source)] + for width in range(1, 6): + state = initialize(source, tuple(range(width))) + check_state(state, source) + for step in range(48): + available = tuple(i for i in range(5) if i not in state.labels[1:]) + state = state.slide(available[(7 * step + width) % len(available)]) + check_state(state, source) + slides += 1 + return {"sources": 2, "initial_states": 10, "slides": slides, + "maximum_stream_length": 48} + + +def diagonal_boundaries(): + source = [[(i + 1) * (-1) ** i if i == j else 0 for j in range(17)] for i in range(17)] + state = initialize(source, tuple(range(16))) + for step in range(65): + if step: + incoming = next(i for i in range(17) if i not in state.labels) + state = state.slide(incoming) + determinant = 1 + for label in state.labels: + determinant *= source[label][label] + require(state.determinant == determinant, "width-sixteen diagonal determinant") + require(state.materialize() == tuple(tuple( + Fraction(1, source[label][label]) if i == j else Fraction(0) + for j in range(16)) for i, label in enumerate(state.labels)), "wide diagonal inverse") + max_source = [[int(i == j) for j in range(32)] for i in range(32)] + require(initialize(max_source, (31,)).slide(0).materialize() == ((Fraction(1),),), + "maximum source dimension") + return {"width": 16, "slides": 64, "source_limit": 32} + + +def expect_rejection(action): + try: + action() + except ValueError: + return + raise ValueError("expected rejection did not occur") + + +def controls(): + invalid = [([], (0,)), ([[1, 0], [0]], (0,)), ([[True]], (0,)), + ([[1.0]], (0,)), ([[1 << 257]], (0,)), ([[1]], (True,)), + ([[1]], (1,)), ([[1, 0], [0, 1]], (0, 0)), + ([[1, 1], [1, 1]], (0, 1)), + ([[int(i == j) for j in range(33)] for i in range(33)], (0,)), + ([[int(i == j) for j in range(17)] for i in range(17)], tuple(range(17)))] + for matrix, labels in invalid: + expect_rejection(lambda: initialize(matrix, labels)) + source = [[4, -1, 2], [1, 5, -2], [0, 1, 3]] + state = initialize(source, (0, 1)) + for incoming in (True, -1, 3, 1): + expect_rejection(lambda: state.slide(incoming)) + expect_rejection(lambda: exact_div(1, 2)) + expect_rejection(lambda: exact_div(1, 0)) + expect_rejection(lambda: initialize([[0, 1], [1, 0]], (0, 1)).slide(0)) + bad = [[1, 0, 0], [0, 1, 1], [0, 1, 1]] + expect_rejection(lambda: initialize(bad, (0, 1)).slide(2)) + following = state.slide(2) + for corrupted in (replace(following, determinant=-following.determinant), + replace(following, adjugate=((3, -2), (-1, 5))), + replace(following, row_scales=(1, 2, 1)), + replace(following, labels=(2, 1))): + expect_rejection(lambda: check_state(corrupted, source)) + require(state.labels == (0, 1) and state.determinant == 21, "failure leaves state intact") + # A singular first scalar pivot is legal when the retained block is invertible. + pivoted = [[0, 1], [1, 1]] + check_state(initialize(pivoted, (0, 1)).slide(0), pivoted) + return {"invalid_inputs": len(invalid) + 4, "division_or_singular_controls": 4, + "corrupted_state_controls": 4, "row_pivot_positive_control": 1} + + +def source_hashes(): + names = ("cache.py", "verify.py", "README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json") + hashes = {name: hashlib.sha256((PACKAGE / name).read_bytes()).hexdigest() for name in names} + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + root = PACKAGE.parents[1] + require(len(manifest["files"]) <= 8, "bounded source manifest") + inputs = {} + for entry in manifest["files"]: + if entry["usage"] == "input": + actual = hashlib.sha256((root / entry["path"]).read_bytes()).hexdigest() + require(actual == entry["sha256"], "changed predecessor contract bytes") + inputs[entry["path"]] = actual + return {"package": hashes, "contract_inputs": inputs} + + +def main(): + hashes_before = source_hashes() + report = {"status": "PASS_SHARED_DENOMINATOR_WINDOW_CACHE", + "claim_type": "scoped written construction with finite exact corroboration", + "initialization_census": initialization_census(), + "integer_census": exhaustive_integer(), "rational_streams": rational_streams(), + "boundary_cases": diagonal_boundaries(), "controls": controls()} + require(source_hashes() == hashes_before, "source stability during verification") + report["sha256"] = hashes_before + print(json.dumps(report, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()