diff --git a/research/sliding-window-inverse/.gitignore b/research/sliding-window-inverse/.gitignore new file mode 100644 index 0000000000..3673a99c42 --- /dev/null +++ b/research/sliding-window-inverse/.gitignore @@ -0,0 +1,2 @@ +__pycache__/ +*.pyc diff --git a/research/sliding-window-inverse/INPUTS.json b/research/sliding-window-inverse/INPUTS.json new file mode 100644 index 0000000000..c8a9d21e05 --- /dev/null +++ b/research/sliding-window-inverse/INPUTS.json @@ -0,0 +1,3 @@ +{ + "inputs/gaussian_check_setup.py": "46e234fbadbbf934cb02f609d7aa14355789c42f82e384cf624d31e57bd05a3a" +} diff --git a/research/sliding-window-inverse/LIBRARY-BRIDGES.json b/research/sliding-window-inverse/LIBRARY-BRIDGES.json new file mode 100644 index 0000000000..b07809bad9 --- /dev/null +++ b/research/sliding-window-inverse/LIBRARY-BRIDGES.json @@ -0,0 +1,109 @@ +{ + "schema_version": 1, + "concepts": [ + { + "id": "schur-elimination", + "source": "Mathproof/LinearAlgebra/SchurBlockElimination.lean", + "sha256": "b865c41950e67c86d3e2961e5a5682d0cbf1a49ad9e11612730e0c198c16ddb3", + "declarations": [ + "schur_block_system_iff" + ], + "role": "Deletion and reattachment of one coordinate; requires the actual two-sided inverse hypotheses.", + "catalog_status": "ARTIFACT_PRESENT", + "catalog_hash_matches_current": true, + "evidence": "Current source read; no new kernel audit of this combined informal application." + }, + { + "id": "robust-frames", + "source": "Mathproof/Meta/RobustRealTIFrames20261006.lean", + "sha256": "47a7f3586e6b1be6497e237df7cd37c73fae5107b69f7242e5e128a2eb7e918b", + "declarations": [ + "Frame.norm_apply", + "relative_frame_error" + ], + "role": "Permutation-frame transport. Positive diagonal weights are separately justified by a pullback norm, not treated as orthogonal.", + "catalog_status": "ARTIFACT_PRESENT", + "catalog_hash_matches_current": true, + "evidence": "Current source read; no new kernel audit of this combined informal application." + }, + { + "id": "tensor-packing", + "source": "Mathproof/Meta/RobustRealTIRecovery20261006.lean", + "sha256": "bffdfcd0b61f4f116c2f7e24566cbbef608fe127f2215fb3d225ad1218ce73d6", + "declarations": [ + "pack_norm", + "pack_sub" + ], + "role": "Finite tensor layouts preserve squared energy; real/imaginary and correlated payload columns share one exact map.", + "catalog_status": "ARTIFACT_PRESENT", + "catalog_hash_matches_current": true, + "evidence": "Current source read; no new kernel audit of this combined informal application." + }, + { + "id": "block-energy", + "source": "Mathproof/Computability/IntegerTensorBlockNorm20261015.lean", + "sha256": "52a61d4d8ed0897f097001b9aac1d1ea46b57a0deec5598734b6badae134c420", + "declarations": [ + "block_energy_prefix", + "total_energy_bound" + ], + "role": "Maximum local depth controls a direct sum without an independence premise; inverse gaps yield explicit local factors.", + "catalog_status": "NOT_FOUND", + "catalog_hash_matches_current": false, + "evidence": "Current source read; no new kernel audit of this combined informal application." + }, + { + "id": "word-embedding", + "source": "Mathproof/LiGuanCNOTFallout20260905.lean", + "sha256": "1b6b13e220370fee7a233ba1ee6b66b7eb9d981e8daa9042da2342eb982972da", + "declarations": [ + "word_map", + "within_embedding_iff" + ], + "role": "The generic monoid portion transports an unchanged finite word through fixed injective ports; no characteristic-two recorder theorem is used over rationals.", + "catalog_status": "ARTIFACT_PRESENT", + "catalog_hash_matches_current": true, + "evidence": "Current source read; no new kernel audit of this combined informal application." + }, + { + "id": "footprint-frame", + "source": "Mathproof/Computability/MultitapeFrameRule20261014.lean", + "sha256": "e5aa9ec056340c67bc6e382eee0a859e6903d9944d3a0e021f2a24a12459cb66", + "declarations": [ + "FootprintedRuns.frame" + ], + "role": "Arbitrary exterior preservation is a design precedent; the finite-memory API is proved directly, not claimed as a Lean multitape instance.", + "catalog_status": "ARTIFACT_PRESENT", + "catalog_hash_matches_current": true, + "evidence": "Current source read; no new kernel audit of this combined informal application." + }, + { + "id": "locality", + "source": "Mathproof/Computability/MultitapeLocality20261014.lean", + "sha256": "4e5df1bdd9764d335424acb2a3aad8364f647892e632d8b09aec85e45cfb5b31", + "declarations": [], + "role": "Local scanned-region dependence motivates the exact immutable-source/port contract; not a new tape execution theorem.", + "catalog_status": "ARTIFACT_PRESENT", + "catalog_hash_matches_current": true, + "evidence": "Current source read; no new kernel audit of this combined informal application." + }, + { + "id": "woodbury", + "source": "research/woodbury-reactor-20260920/Woodbury.lean", + "sha256": "8f269e268a026bc659e33f85e8873713b325f618ef0dae9f7d469e911730b27d", + "declarations": [ + "woodbury_two_sided" + ], + "role": "Two-sided inverse of the 2x2 core gives the exact full rank-two replacement.", + "evidence": "Historical typed DAG operation exists; current source read. Not a fresh audit of this new result.", + "dag_snapshot": "5cafc7e755c67429021b07c755ddd70e5fef81e1f478c9e6d14f298cca131835", + "dag_type_node": "837a84e5d279c06003451565aefc1517bec1e6667bba5fc0a71ce315fc9002ed", + "historical_axioms": [ + "propext", + "Classical.choice", + "Quot.sound" + ] + } + ], + "scope": "Discovery provenance, exact hypotheses checked against written application. Source presence or historical artifacts are not a fresh kernel proof." +} diff --git a/research/sliding-window-inverse/LIBRARY-BRIDGES.md b/research/sliding-window-inverse/LIBRARY-BRIDGES.md new file mode 100644 index 0000000000..36856c2d4f --- /dev/null +++ b/research/sliding-window-inverse/LIBRARY-BRIDGES.md @@ -0,0 +1,60 @@ +# Eight shared-library bridges and nine mathematical concepts + +These are actual source statements or explicitly labelled design precedents. +The new sufficient proofs are fully written in PROOF.md; none relies on an +unavailable spectral oracle or an assumed unknown circuit. Exact current source +hashes and historical evidence distinctions are in LIBRARY-BRIDGES.json. + +| Shared source | Reusable fact or concept | Concrete use here | Limit | +| --- | --- | --- | --- | +| SchurBlockElimination | two-sided Schur system elimination | principal inverse deletion and bordering | Already used in PR3851; no novelty claim for Schur. | +| woodbury-reactor / typed DAG | `woodbury_two_sided` | a two-column/two-row update and 2×2 inverse replace a dense inverse | Historical audited algebra; combined cache is informal. | +| RobustRealTIFrames | `relative_frame_error`, exact orthogonal frames | source-label permutations transport inverse/error without changing norm | Arbitrary positive D is NOT orthogonal. | +| RobustRealTIRecovery | `pack_norm`, coordinate bijection | tensor/column flattening preserves squared energy | Does not prove spectral recovery or supply frames. | +| IntegerTensorBlockNorm | `block_energy_prefix`, `total_energy_bound` | correlated blocks use maximum local amplification, not total unrelated work | Separate inverse applications, not an unbounded product. | +| LiGuanCNOTFallout | generic `word_map` and injective word transport | fixed caller-port embedding preserves the same local-map sequence | Uses only generic monoid lemmas, not F₂-only recorder algebra. | +| MultitapeFrameRule | `FootprintedRuns.frame` | direct finite-memory exterior-frame proof and dirty-value controls | This API is not a new Lean multitape program. | +| MultitapeLocality | finite-region observational dependence | immutable old-H and injective finite port contract | Design precedent, not an instantiated new execution certificate. | + +The additional numerical concept is an actual residual-to-recovery certificate: +check the full rational residual against the exact weighted old-H matrix before +asserting a numerical tolerance. It follows the shared robust-recovery practice +of checking the returned object itself; the inverse-specific proof is new here. +The exact coefficient-height/minor argument and diagonal similarity cancellation +are retained from the Gaussian predecessor, not advertised as unused inventions. + +The submitted cache, two-sided residual check, weighted rounding, port-map +implementation and tensor/block controls instantiate the first six algebraic +patterns and a direct finite-memory frame. The two multitape sources remain +explicit design precedents; their Lean execution theorems are not newly applied +to this host-language algorithm. We do not inflate that boundary into a formal +tape result merely to increase the source count. + +## Search coverage and unused status + +The existing authoritative source catalogue contains 401,769 registered modules. +Twenty broad source queries retrieved at most 100 hits each, with bounded +MathProof-specific follow-ups; twelve typed-DAG/symbol queries and six indexed +note searches were also performed. Sources include the federated project, +downloaded libraries and registered archive notes. This is broad retrieval, +not a complete inspection or semantic search of every registered statement. +The first unrestricted ranked source query was bounded after slow common-term +search; the bounded indexed replacement preserved explicit limits. + +Actual source inspection then followed the eight bridges above, the local +Woodbury mission/proof, current Gaussian source and precise predecessor APIs. +The private search packets retain indexed paths, revisions, snapshots and misses. +Only the sanitized provenance needed for review is published here. + +Schur, weights, minors and Neumann reasoning are demonstrably already present +in PR3851. The scoped Woodbury sliding-cache application, its weighted residual +and fixed-port/block contracts were not located in the inspected project sources +or the 575-open-PR body scan. That is a bounded overlap finding, not a guarantee +that nobody has applied any of these standard ideas anywhere in the project. + +A later actual-source comparison found that RaD's retained +`review-reusable-banded-inverse.md` already uses Woodbury for a circular wrap +correction and shares setup across right-hand sides. That predecessor is +explicitly credited. It does not describe the one-index principal-set deletion/ +bordering cache checked here. Our claim is this scoped composition, not first +use of Woodbury, residuals, setup reuse or weighted Gaussian inverses. diff --git a/research/sliding-window-inverse/NOTICE b/research/sliding-window-inverse/NOTICE new file mode 100644 index 0000000000..399859aeb9 --- /dev/null +++ b/research/sliding-window-inverse/NOTICE @@ -0,0 +1,25 @@ +Apache-2.0. New composition, exact host algorithm, proof and checks by Dugongue, +with substantial OpenAI Codex assistance. No independent human review claimed. + +Unmodified vendored source: +research/physical-gaussian-core/gaussian_check_setup.py from Jose Manuel +(jmbarrancoml), PR3851 at 7ab67b4a84d28cd562b9711aa315ca5b47822b37. +Only its literal exact rational setup fixture is consumed by AST parsing. +Its physical implementation and native dependencies are not imported or rerun. + +Retain the predecessor's attribution: Chafik Boukhalfa's PR489 local inverse +and PR481/486 boundary/halo work; the RaD project (hipotures) Gaussian, +phase-cell, microbox and reusable-banded-inverse reports; PR3787 word multiplier +at 9b5474f47b0ea9a3c76bb5b1b577fb36704815e0 including corrected PR3709; +Mason Hale's interval reference; Dugongue's scalar ABI precedent; Harvey and +van der Hoeven, the OpenAI manuscript and Douglas Colkitt's framework. +These source notices are retained credit, not a fresh validation of their full +physical/analytic claims. PR3763's chirp caller is a separate future integration +interface, not implemented or re-audited here. + +The shared MathProof Schur, Woodbury, robust-TI frames/recovery, block norm, +CNOT/TI word, locality and frame sources retain their existing authorship and +provenance, identified by exact source hashes in LIBRARY-BRIDGES.json. +The matrix identities and elementary norm facts are standard mathematics. +Woodbury already appears in RaD's reviewed circular-wrap correction; this work +claims a moving-principal-window cache application, not its first project use. diff --git a/research/sliding-window-inverse/OVERLAP.md b/research/sliding-window-inverse/OVERLAP.md new file mode 100644 index 0000000000..e48958bf5e --- /dev/null +++ b/research/sliding-window-inverse/OVERLAP.md @@ -0,0 +1,34 @@ +# Current source and overlap + +Canonical main fetched at entry and at the final research checkpoint: +`20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority revision 6. +Current AGENTS.md, autoresearch.md and CONTRIBUTING.md were refreshed and compared +with the same previously read source revision. PR3851's current head remained +`7ab67b4a84d28cd562b9711aa315ca5b47822b37`. Its actual PROOF, setup fixture, +window/axis/matrix/production source, README and source manifest were inspected. + +The original uniform-transfer-audit card is retained verbatim; the changed scope +and its actual sufficient conclusion are explicit in TASK.json. The selected +baseline bindings were checked in the preceding same-main campaign; no new +selected cold replay is claimed for this unrelated component. + +A fully paginated REST snapshot scanned 575 open PR titles/bodies. No body match +for the scoped sliding principal-inverse cache was located. The repository +find_overlap.py also searched the snapshot and available local package notes. +Latest all-state updated records were scanned at entry and a final 30-record +checkpoint through PR3871. Start-here and handoff Discussion HTML was read, with +partial possible reply coverage and no complete GraphQL Discussion cache. +No exhaustive historical closed-PR, arbitrary-diff or unpublished coverage claim. + +Actual-source comparison found a crucial existing use: RaD's retained +review-reusable-banded-inverse.md already uses Woodbury for circular-wrap repair, +plus setup sharing, rounded row residuals, inverse bounds and coefficient heights. +Its phase-cell report and PR3851 already use Schur and exact similarity weights. +Those tools are predecessors, not newly introduced mechanisms. The new delta is +one-index changes of the principal index set, with exact cache update, source- +label contracts, weighted residual recovery and a finite-memory port/energy API. +Neither new broad mathematical novelty nor first project use of the standard +identities is asserted. The scoped application was not found in the compared +sources. LIBRARY-BRIDGES.md records the broad DAG/source/note search and limits. + +No exact new kappa, selected-frontier change, hosted CI or human review claimed. diff --git a/research/sliding-window-inverse/PROOF.md b/research/sliding-window-inverse/PROOF.md new file mode 100644 index 0000000000..c95bef030b --- /dev/null +++ b/research/sliding-window-inverse/PROOF.md @@ -0,0 +1,234 @@ +# Exact sliding-window preparation with certified weighted recovery + +## Root theorem and actual contribution + +Let H be a fixed N×N rational matrix, N ≥ 2, and D a fixed positive rational +diagonal matrix. Suppose G = D^−1 H D has real positive diagonal entries and + + δ = min_i (G_ii − Σ_(j≠i) |G_ij|) > 0. + +Let 1 ≤ m ≤ N. Begin with an ordered list J of m distinct source indices; +each slide removes the first index and appends an index absent from the retained +list. The incoming index may equal the outgoing index. Then both algorithms +below construct exactly `H[J,J]^−1` after every slide. After one dense initial +inverse, T slides use `O(m³ + T m²)` rational field operations and `O(m²)` live +cache storage, in addition to access/storage for the unchanged global H,D. +The output stream, if retained, has its separate output-storage cost. +All final reduced inverse entries have bit height polynomial in m and the fixed +input coefficient height, independent of T. The weighted residual tests below +supply sufficient numerical error and integer-recovery guarantees. + +This is an exact arithmetic preparation component, not a finite-tape compiler, +a revised online page format, a runtime benchmark, or a new κ. The mathematical +identities are classical and found in the shared library. The contribution is a +source-bound composition, two exact algorithms, explicit safety/precision/height +conditions and a checked reuse target for the current Gaussian preparation. + +## 1. Every principal window and every pivot exists + +Every principal restriction G_J has diagonal-dominance gap at least δ. +For nonzero z, choose i with |z_i| = ||z||_∞. The reverse triangle inequality +on row i gives + + ||G_J z||_∞ ≥ δ ||z||_∞. + +Thus G_J is injective, hence invertible in finite dimension, and +`||G_J^−1||_∞ ≤ 1/δ`. Similarity by the positive diagonal restriction D_J +makes H_J invertible as well. This holds for all principal subwindows and +permutations, not merely the finitely tested windows. No spectral oracle is +required. Empty retained windows at m = 1 use the empty block convention. + +## 2. Schur deletion and bordering + +Move the outgoing coordinate to the end by the same row/column permutation. +Write the old matrix and its inverse as + + M = [ B u ; v d ], M^−1 = [ E f ; g h ]. + +When m > 1, B is an invertible principal matrix. Let +`σ_old = d − v B^−1 u`. The block factorization + + M = [ I 0 ; v B^−1 1 ] [ B 0 ; 0 σ_old ] [ I B^−1 u ; 0 1 ] + +shows σ_old ≠ 0, and multiplication of the inverses gives +`h = σ_old^−1 ≠ 0` and + + B^−1 = E − f h^−1 g. (2.1) + +This is the deletion step. For the incoming source index, read its column u', +row v' and diagonal d' from the SAME global H. Compute + + w = B^−1 u', z = v' B^−1, σ = d' − v' w. + +The new principal matrix is invertible by section 1, so σ ≠ 0. Its inverse is + + [ B^−1 + w σ^−1 z −w σ^−1 ; + −σ^−1 z σ^−1 ]. (2.2) + +Multiplying on either side verifies every block entry, proving the new inverse. +The empty case m = 1 simply returns `1/d'`. Formula (2.1) is the specialization +of two-sided Schur elimination; assuming a one-sided formula in an arbitrary +ring without the required inverse conditions would not justify both directions. + +## 3. Complementary rank-two Woodbury update + +Keep the same outgoing-last order. The replacement changes only the final +row and column. Let c be the entire new-minus-old final column, e the final +standard basis vector, and r the new-minus-old final row with its last entry +SET TO ZERO. Then + + Δ = c eᵀ + e r, U = [ c e ], V = [ eᵀ ; r ]. + +The diagonal change occurs in c exactly once; counting it again in r is wrong +when the two source diagonals differ. Let Q = M^−1 and C = (I_2+VQU)^−1. +The inverse exists: if `(I+VQU)t=0`, then `(M+UV)QUt = U(I+VQU)t = 0`; +invertibility of M+UV implies Ut = 0, and the original equality then gives +t = 0. In finite dimension the core is invertible. The two-sided Woodbury +identity from the shared DAG gives + + (M+UV)^−1 = Q − QU C VQ. (3.1) + +For completeness, put A=QU and B=V. The DAG identity says +`(I+AB)(I−ACB) = (I−ACB)(I+AB) = I` whenever C is a two-sided inverse of +I+BA. Since M+UV = M(I+QUV), right multiplication by Q yields (3.1). +This proof fixes the multiplication orientation even for nonsymmetric H. +The core has size 2 regardless of m. The implementation evaluates its inverse +by its exact determinant. At small widths the extra core work need not beat +fresh elimination; the quadratic bound is asymptotic field arithmetic only. + +## 4. Operation and coefficient-height bounds + +Deletion (2.1) is one scaled outer product. Bordering (2.2) is two matrix-vector +products and one outer product. Thus each costs O(m²) field operations. +The Woodbury route uses products with two-column/two-row factors and a 2×2 +inverse, hence also O(m²). The initial dense inverse costs O(m³). +The tested deterministic width-8 instance uses 414 field operations for a +Schur slide, 869 for Woodbury, and 1,920 for the retained fresh Gauss–Jordan +algorithm. These exact counters count rational additions/subtractions/products/ +divisions equally. They exclude source generation, bit costs, checking, page +emission and tape scans; they are not timings or an end-to-end speedup claim. + +Suppose each source numerator and positive denominator has at most B bits, +B ≥ 1. Clear denominators separately in each m-row principal matrix. The row +multiplier is at most 2^(mB), and resulting integer entries have magnitude at +most 2^((m+1)B). Expanding a k×k minor bounds its magnitude by +`k! 2^(k(m+1)B)`. Cramer's rule for `A^−1 = adj(Z) diag(row_multipliers)/det(Z)` +therefore bounds each numerator and denominator by bit height at most + + L = m(m+1)B + m ceil(log2(max(m,2))) + 3. + +Reduction cannot increase that bound. Every cache checkpoint is the inverse +of a principal submatrix of the fixed source, so this L is independent of T. +The retained inverse after deletion has the analogous bound at width m−1. +Each formula forms at most O(m)-term sums of products of a fixed number of +bounded-height rationals; even using the product of denominators as a common +denominator bounds temporary bit height polynomially in m,B. Reduce after +each operation, as `Fraction` does. Ordinary integer arithmetic and gcd hence +give a polynomial bit-cost per slide, rather than an unproved constant-cost +or repeated-unreduced-fraction claim. No fast multitape implementation follows +solely from the rational operation count. + +## 5. Frames, exact weights and residual certificates + +A source-label permutation P is an exact orthogonal frame change: +`(PᵀAP)^−1 = PᵀA^−1P`. Permuting coordinates preserves both ∞ norm and +squared Euclidean norm; this is the finite coordinate use of the robust-frame +and tensor-packing precedents. Positive diagonal D is generally NOT orthogonal. +For it define the pullback norm `||x||_D = ||D^−1x||_∞`; then +`||A||_D = ||D^−1 A D||_∞` by substitution. This is a separate weighted-norm +argument, not an application of an orthogonal-frame theorem to arbitrary D. +It is essential when similarity weights have large ratios. + +For a candidate inverse Z of the weighted principal G_J, compute the exact +rational residual `ρ = ||I−G_J Z||_∞`. If ρ < 1, the Neumann series gives + + ||G_J^−1||_∞ ≤ ||Z||_∞/(1−ρ). + +Indeed `G_J Z = I−R` is invertible and its inverse has norm at most 1/(1−ρ). +Using the independent dominance bound from section 1 gives the sharper +solution-error certificate needed here: + + ||Z−G_J^−1||_∞ = ||G_J^−1(G_J Z−I)||_∞ ≤ ρ/δ_J, + +where δ_J is the computed principal gap, at least δ. Thus for an input with +`||D_J^−1 b||_∞ ≤ B_0` and an additional weighted application error η, + + ||D_J^−1(y−H_J^−1b)||_∞ ≤ B_0 ρ/δ_J + η. (5.1) + +If each entry of the exact weighted inverse is rounded with absolute error +at most ε, the weighted operator error is at most mε. Rounding in weighted +coordinates avoids a spurious `max(D)/min(D)` multiplier. Restoring physical +coordinates multiplies the error bound by max_i D_ii, exactly once. +If the exact solution is known independently to be integral and this physical +bound is STRICTLY below 1/2, nearest-integer recovery is unique. Integrality is +an explicit application premise; a Gaussian inverse output is not generally +integral. At the 1/2 boundary uniqueness cannot be asserted. The finite tests +choose b = H_J z for literal integer z, so that premise is actually discharged. + +## 6. Tensor payloads, correlations and block-local precision + +Packing a finite tensor into a vector is a coordinate bijection and preserves +the sum of squared coordinates. Applying the same inverse separately to its +columns, or to real and imaginary components, needs no statistical independence. +For block ℓ of width m_ℓ and weighted gap δ_ℓ, the elementary ∞-to-2 comparison +and section 1 give + + ||x_ℓ||_2² ≤ (m_ℓ/δ_ℓ²) ||b_ℓ||_2². + +Here x,b are in the weighted coordinates. Consequently the sum of output +energies is at most `max_ℓ(m_ℓ/δ_ℓ²)` times the sum of input energies, even +for identical or otherwise correlated inputs. Choosing c_ℓ with +`m_ℓ/δ_ℓ² ≤ 4^c_ℓ` specializes the shared DAG's block-energy accounting. +It uses the maximum block depth, not the total number of unrelated blocks. +These are separate applications of an inverse to given payloads, not a claim +that a sequential product of inverses has this bound. Cache coefficients reset +to the exact current inverse after every slide; their uniform bound likewise +depends on δ and m, not on the number of prior windows. + +## 7. Injective ports and arbitrary dirty exterior + +For any injective list of caller ports p_1,…,p_m, lift a local linear map T by +reading those values, applying T, writing the m results to those same ports, +and preserving every other memory value. A coordinate check proves + + lift(T_2 T_1) = lift(T_2) ∘ lift(T_1), lift(I) = I. + +Thus the generic injective word-transport theorem from the shared CNOT/TI +library applies to the SAME sequence of local maps. It does not enlarge the +generator alphabet or claim a new shortest-word/tape-time bound. For every +outside port, its arbitrary initial value is invariant, by cases on membership +in the finite port image. This is the locality/frame principle made explicit +by the shared footprint proofs, here proved directly for the finite-memory +API. The interpreter tests unstructured dirty exterior values and noncontiguous +ports. We have not built a program in that Lean multitape semantics or proved +its tape heads, halt state, restoration or primitive transition count. + +## 8. Current-source relevance and evidence boundary + +PR3851 prepares exact old-H principal/interior/Schur matrices, then publishes +rounded factor pages. Its producer already preserves one global rounded H; +its dense local q-model is a different matrix and cannot replace it. +This contribution freezes that boundary and supplies a reuse component for +streams of one-index-shift principal windows from the same H. Schur elimination, +weights and coefficient/minor reasoning already occur in that predecessor; +we do not claim to introduce them to the project. The newly assembled piece +is the two-sided sliding inverse cache with weighted residual and port/energy +contracts. Producing the existing protected page layout from these cached +inverses, transporting the cache through encoded tapes and pricing the complete +outer catalogue remain future integration work. + +The immutable 3×3 fixture is extracted without executing upstream code from +Jose Manuel's PR3851 `gaussian_check_setup.py`. It is a rational setup fixture, +not a production Gaussian window. The 13×13 weighted cyclic band fixture is +new and synthetic. Both are labelled in RESULT.json. Across 244 slides both +routes agree with a separate forward-elimination/back-substitution solver, +satisfy both inverse identities and recover the deliberately integral payloads. +The written arguments give the universal sufficient statements; finite tests +are implementation evidence. The combined result is not newly kernel checked. + +RaD's retained reusable-banded-inverse review already proves a circular-wrap +Woodbury correction and reused per-axis setup. The present delta is a changing +principal index set, not a new wrap solver. A nontrivial positive diagonal must +pass the weighted gap test itself; in the predecessor's stated ordinary +row-dominant domain D = I is admissible. No unconditional claim about every +choice of its Gaussian similarity weights is made. diff --git a/research/sliding-window-inverse/README.md b/research/sliding-window-inverse/README.md new file mode 100644 index 0000000000..cca049dfc1 --- /dev/null +++ b/research/sliding-window-inverse/README.md @@ -0,0 +1,86 @@ +# Reuse exact principal-window inverses from one global source + +This provides an exact preparation component for streams of overlapping windows: +after one dense initialization, each one-index slide updates the inverse in +**O(m²) rational field operations**, rather than starting another O(m³) dense +inverse. Both Schur deletion/bordering and a rank-two Woodbury route are supplied. +All coefficients and source labels remain bound to the same old-H matrix. + +The result combines eight shared-library bridges: Schur, two-sided Woodbury, +robust frames, tensor packing, block-local energy, injective word transport, +footprint frames and locality. [LIBRARY-BRIDGES.md](LIBRARY-BRIDGES.md) explains +what is actually used and which tape theorems remain design precedents. +[PROOF.md](PROOF.md) gives complete sufficient conditions and proofs for the +cache, rounding/residual recovery, polynomial coefficient heights and dirty +exterior. No assumed unknown gadget or oracle replaces those proofs. + +**Current relevance:** Jose Manuel's pending PR3851 constructs exact old-H +principal/Schur preparation pages and pays setup separately. This package supplies +a reuse target for that exact matrix boundary; it does not modify his code or +substitute the dense local q-model. Existing protected-page emission, encoded-tape +porting and the complete outer/setup budget still need integration. No new κ, +new physical supplier or end-to-end runtime speedup is claimed. + +## Evidence + +- 244 exact slides on the immutable upstream 3×3 setup fixture and a separately + labelled synthetic weighted 13×13 cyclic band matrix; both routes match a + separate exact solver and satisfy both inverse identities. +- Weighted rounded inverses pass full residual checks and recover deliberately + integral payloads; correlated/scaled payload columns are included. +- Twelve source-label permutation cases also pass a separate cofactor oracle. + Controls reject stale sources, aliasing, bad residuals and malformed domains; + semantic controls expose diagonal double-counting and the wrong old-H model. +- Finite output-port interpretation preserves arbitrary dirty exterior, word + composition and correlated block/tensor energy bounds. +- Width 8 counts: fresh Gauss–Jordan **1,920** rational field operations; + Schur slide **414**; Woodbury slide **869**. These are exact instrumented + arithmetic counts, not wall-clock, bit-cost or multitape measurements. + +The universal proofs are informal. A historical typed-DAG Woodbury proof is +identified precisely; it is not a new kernel audit of the combined result. +No production Gaussian domain, native compiler or selected cold replay is claimed. + +## Reproduce + +Python 3.12 and its standard library, from the repository root: + +```sh +python3.12 -B research/sliding-window-inverse/verify.py +python3.12 -B research/sliding-window-inverse/test_cache.py +python3.12 -O -B research/sliding-window-inverse/test_cache.py +python3.12 -B scripts/research_package.py --package research/sliding-window-inverse +``` + +Ordinary verification is read-only and works without Git. It authenticates the +upstream fixture source before AST-only extraction, regenerates every exact +receipt field and compares it with RESULT.json. The upstream module is never +imported or executed. The independent reference solver imports no cache code. +A frozen source object and explicit digest prevent silently switching matrices. + +## Open next questions + +1. Wire the cache into a separately priced stream of actual PR3851 overlapping + windows. First freeze its global H, window index sequence and output-page + interface; retain all setup scans and output storage. This host algorithm + alone does not prove fixed-tape complexity or preserve that page layout. +2. Is updating the source's banded factor pages cheaper than emitting them from + a cached inverse? First price one real shift including coefficient creation, + factor rounding and protected-page ownership, then compare the complete bill. +3. For source-certified positive weights, test whether weighted-coordinate + rounding reduces a concrete guard without repaying the gain in scaling work. + Certify weighted dominance afresh; arbitrary diagonal similarity need not + preserve ordinary row dominance. + +## Credit + +Jose Manuel (`jmbarrancoml`), PR3851 at +`7ab67b4a84d28cd562b9711aa315ca5b47822b37`, supplies the exact old-H preparation +contract and the immutable rational setup fixture. His retained line includes +Chafik Boukhalfa/PR489, RaD's phase-cell/microbox construction and PR3787's word +multiplier. Their complete algorithm and physical cost claims are not re-audited +here. Shared MathProof source hashes, declarations and evidence are retained in +LIBRARY-BRIDGES.json. The underlying matrix identities are standard; no exclusive +invention or global absence-of-prior-use claim is made. + +Dugongue, with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/sliding-window-inverse/RESULT.json b/research/sliding-window-inverse/RESULT.json new file mode 100644 index 0000000000..c3fd8e6a23 --- /dev/null +++ b/research/sliding-window-inverse/RESULT.json @@ -0,0 +1,177 @@ +{ + "schema_version": 1, + "status": "PASS_SLIDING_WINDOW_INVERSE", + "slides": 244, + "integer_recoveries": 244, + "rows": [ + { + "fixture": "upstream-setup-3", + "width": 1, + "method": "schur", + "slides": 6, + "fresh_dense_field_ops": 2, + "update_field_ops_min": 2, + "update_field_ops_max": 2, + "maximum_weighted_residual": "1/65536", + "maximum_actual_physical_error": "3/65536", + "maximum_reduced_inverse_bit_length": 3 + }, + { + "fixture": "upstream-setup-3", + "width": 1, + "method": "woodbury", + "slides": 6, + "fresh_dense_field_ops": 2, + "update_field_ops_min": 29, + "update_field_ops_max": 29, + "maximum_weighted_residual": "1/65536", + "maximum_actual_physical_error": "3/65536", + "maximum_reduced_inverse_bit_length": 3 + }, + { + "fixture": "upstream-setup-3", + "width": 2, + "method": "schur", + "slides": 6, + "fresh_dense_field_ops": 24, + "update_field_ops_min": 12, + "update_field_ops_max": 12, + "maximum_weighted_residual": "13/131072", + "maximum_actual_physical_error": "19/131072", + "maximum_reduced_inverse_bit_length": 7 + }, + { + "fixture": "upstream-setup-3", + "width": 2, + "method": "woodbury", + "slides": 6, + "fresh_dense_field_ops": 24, + "update_field_ops_min": 77, + "update_field_ops_max": 77, + "maximum_weighted_residual": "13/131072", + "maximum_actual_physical_error": "19/131072", + "maximum_reduced_inverse_bit_length": 7 + }, + { + "fixture": "upstream-setup-3", + "width": 3, + "method": "schur", + "slides": 6, + "fresh_dense_field_ops": 90, + "update_field_ops_min": 39, + "update_field_ops_max": 39, + "maximum_weighted_residual": "9/65536", + "maximum_actual_physical_error": "9/32768", + "maximum_reduced_inverse_bit_length": 10 + }, + { + "fixture": "upstream-setup-3", + "width": 3, + "method": "woodbury", + "slides": 6, + "fresh_dense_field_ops": 90, + "update_field_ops_min": 149, + "update_field_ops_max": 149, + "maximum_weighted_residual": "9/65536", + "maximum_actual_physical_error": "9/32768", + "maximum_reduced_inverse_bit_length": 10 + }, + { + "fixture": "weighted-cyclic-13", + "width": 1, + "method": "schur", + "slides": 26, + "fresh_dense_field_ops": 2, + "update_field_ops_min": 2, + "update_field_ops_max": 2, + "maximum_weighted_residual": "0", + "maximum_actual_physical_error": "0", + "maximum_reduced_inverse_bit_length": 1 + }, + { + "fixture": "weighted-cyclic-13", + "width": 1, + "method": "woodbury", + "slides": 26, + "fresh_dense_field_ops": 2, + "update_field_ops_min": 29, + "update_field_ops_max": 29, + "maximum_weighted_residual": "0", + "maximum_actual_physical_error": "0", + "maximum_reduced_inverse_bit_length": 1 + }, + { + "fixture": "weighted-cyclic-13", + "width": 2, + "method": "schur", + "slides": 26, + "fresh_dense_field_ops": 24, + "update_field_ops_min": 12, + "update_field_ops_max": 12, + "maximum_weighted_residual": "1/1048576", + "maximum_actual_physical_error": "13/1048576", + "maximum_reduced_inverse_bit_length": 11 + }, + { + "fixture": "weighted-cyclic-13", + "width": 2, + "method": "woodbury", + "slides": 26, + "fresh_dense_field_ops": 24, + "update_field_ops_min": 77, + "update_field_ops_max": 77, + "maximum_weighted_residual": "1/1048576", + "maximum_actual_physical_error": "13/1048576", + "maximum_reduced_inverse_bit_length": 11 + }, + { + "fixture": "weighted-cyclic-13", + "width": 4, + "method": "schur", + "slides": 26, + "fresh_dense_field_ops": 224, + "update_field_ops_min": 82, + "update_field_ops_max": 82, + "maximum_weighted_residual": "1/131072", + "maximum_actual_physical_error": "211/1048576", + "maximum_reduced_inverse_bit_length": 20 + }, + { + "fixture": "weighted-cyclic-13", + "width": 4, + "method": "woodbury", + "slides": 26, + "fresh_dense_field_ops": 224, + "update_field_ops_min": 245, + "update_field_ops_max": 245, + "maximum_weighted_residual": "1/131072", + "maximum_actual_physical_error": "211/1048576", + "maximum_reduced_inverse_bit_length": 20 + }, + { + "fixture": "weighted-cyclic-13", + "width": 8, + "method": "schur", + "slides": 26, + "fresh_dense_field_ops": 1920, + "update_field_ops_min": 414, + "update_field_ops_max": 414, + "maximum_weighted_residual": "15/1048576", + "maximum_actual_physical_error": "425/1048576", + "maximum_reduced_inverse_bit_length": 40 + }, + { + "fixture": "weighted-cyclic-13", + "width": 8, + "method": "woodbury", + "slides": 26, + "fresh_dense_field_ops": 1920, + "update_field_ops_min": 869, + "update_field_ops_max": 869, + "maximum_weighted_residual": "15/1048576", + "maximum_actual_physical_error": "425/1048576", + "maximum_reduced_inverse_bit_length": 40 + } + ], + "scope": "Exact arithmetic preparation and sufficient residual recovery; no physical compiler, wall-time speedup or kappa claim." +} diff --git a/research/sliding-window-inverse/SOURCES.json b/research/sliding-window-inverse/SOURCES.json new file mode 100644 index 0000000000..20a39794d2 --- /dev/null +++ b/research/sliding-window-inverse/SOURCES.json @@ -0,0 +1,39 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "references/semantic-bulk/rad20/reports/review-reusable-banded-inverse.md", + "usage": "provenance", + "git_blob": "de7a916369cc36737fd96b9b0172e2ef453c6b03", + "sha256": "801359569c92f9d5ddd128b694993a5ac22a468e87bfea478cecc0ee413d058b" + }, + { + "path": "references/semantic-bulk/rad20/reports/downstream-phase-cell-inverse.md", + "usage": "provenance", + "git_blob": "d72345a0aa748443c4efcddf87aa10d524664841", + "sha256": "3cdf492bcb719db4295658604dc202d6a2c5a008b87de43ec54f0107c64db730" + } + ], + "external_public_input": { + "local_path": "inputs/gaussian_check_setup.py", + "source_pr": 3851, + "source_head": "7ab67b4a84d28cd562b9711aa315ca5b47822b37", + "source_path": "research/physical-gaussian-core/gaussian_check_setup.py", + "sha256": "46e234fbadbbf934cb02f609d7aa14355789c42f82e384cf624d31e57bd05a3a", + "coverage": "Unmodified public source; vendored and hash-checked; AST literal fixture only, no foreign Git object or physical modules required." + }, + "local_library_provenance": "LIBRARY-BRIDGES.json; source/hash/declaration references are discovery evidence, not new Lean runtime dependencies or new kernel certification." +} diff --git a/research/sliding-window-inverse/TASK.json b/research/sliding-window-inverse/TASK.json new file mode 100644 index 0000000000..49d3476c5e --- /dev/null +++ b/research/sliding-window-inverse/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?", + "starting_points": [ + "certificates/selected-result.json", + "docs/audit.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected review scope and choose one exact all-size or precision implication.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "Choose one tape, precision, hosting or restoration lemma." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision" + ] + }, + "scope_status": "changed", + "scope_change_reason": "The donor explicitly requests extensive shared DAG/Lean-tree reuse. Current PR3851 exposes exact old-H preparation with separately charged setup; this scope supplies a universal cached principal-window preparation and residual-to-recovery contract using eight inspected shared-library bridges. It is not a selected supplier cold replay or a new physical tape implementation.", + "actual_scope": "Exact all-window inverse reuse with explicit weighted precision, height, frame and correlation-safe sufficient bounds.", + "bottleneck_link": "Overlapping windows can reuse exact global-matrix preparation; a complete caller must still pay its page/tape/setup schedule.", + "budget_minutes": 25, + "author": "Dugongue", + "ai_assistance": "Substantial OpenAI Codex assistance in retrieval, mathematical synthesis, code, proof review and verification; no independent human review.", + "outcome": "completed", + "evidence": "Complete informal universal proof and exact host implementation; 244 slides, independent solver and cofactor checks, weighted residual/integer recovery, dirty exterior and correlation controls. No new formal proof or kappa.", + "stop_rule": "Finish one positive source-bound reuse component and its complete sufficient proof. Stop before native page integration or a new frontier claim.", + "upstream_checkpoint": { + "utc": "2026-10-19T00:03:57.036Z", + "main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "priority_revision": 6, + "predecessor_head": "7ab67b4a84d28cd562b9711aa315ca5b47822b37" + }, + "open_questions": [ + { + "question": "Can a real stream of overlapping PR3851 windows consume the cache through the existing protected page ABI?", + "why_it_matters": "Would turn the arithmetic component into a priced physical preparation improvement.", + "first_step": "Freeze actual old H, index stream and page fields; include complete coefficient, output and tape scan costs.", + "blocked_by": "The host cache does not implement encoded page emission or fixed-tape transitions." + }, + { + "question": "Would direct banded-factor updates be cheaper than cached inverse-to-page emission?", + "why_it_matters": "Avoids assuming the new arithmetic count automatically improves the complete current construction.", + "first_step": "Price one literal shift in both representations at the same frozen source and precision.", + "blocked_by": "No production tape implementation comparison is claimed." + }, + { + "question": "Can certified weighted-coordinate rounding reduce one current guard after scaling costs are charged?", + "why_it_matters": "The norm contract may avoid multiplying large similarity ratios unnecessarily.", + "first_step": "Certify the actual weighted dominance gap and full returned residual before changing any guard.", + "blocked_by": "Arbitrary diagonal similarity need not preserve row dominance." + } + ] +} diff --git a/research/sliding-window-inverse/VALIDATION.json b/research/sliding-window-inverse/VALIDATION.json new file mode 100644 index 0000000000..988222cbdd --- /dev/null +++ b/research/sliding-window-inverse/VALIDATION.json @@ -0,0 +1,28 @@ +{ + "status": "PASS", + "python": "3.12.10", + "registered_command": "python3.12 -B scripts/research_package.py --package research/sliding-window-inverse", + "coverage": [ + "244 exact sliding updates, both Schur and rank-two Woodbury routes", + "Separate forward-elimination/back-substitution solver and both inverse identities", + "12 label permutation cases with a separate cofactor oracle", + "Weighted inverse residual, uniform height guards and actual integral-target recovery", + "Source identity, aliases, zero candidate residual, strict 1/2 boundary and malformed-domain rejects", + "Real diagonal-overlap and nonsymmetric-model semantic controls", + "Fixed-port word embedding, arbitrary dirty exterior, tensor flattening and correlated block-energy controls", + "Actual read-only Git-free CLI with immutable source and result corruption rejects", + "All guards and controls repeated under Python -O" + ], + "measured_field_operations_width_8": { + "fresh_dense": 1920, + "schur_slide": 414, + "woodbury_slide": 869 + }, + "not_claimed": [ + "Combined Lean/kernel audit", + "Production Gaussian domain replay", + "Encoded-tape or protected-page implementation", + "Bit-operation, wall-clock or end-to-end speedup", + "New kappa, selected-frontier change, independent human review" + ] +} diff --git a/research/sliding-window-inverse/VERIFY.json b/research/sliding-window-inverse/VERIFY.json new file mode 100644 index 0000000000..962708579c --- /dev/null +++ b/research/sliding-window-inverse/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "All 244 exact slides, two independent update routes, residuals, explicit recovery premises, polynomial height guard and field operation counts." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_cache.py" + ], + "timeout_seconds": 60, + "checks": "Separate cofactor/permutation, malformed source/alias/residual, semantic diagonal/model, port word/frame, correlated energy, strict-boundary and actual CLI controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/test_cache.py" + ], + "timeout_seconds": 60, + "checks": "The same safeguards and controls with Python assertions disabled." + } + ] +} diff --git a/research/sliding-window-inverse/cache.py b/research/sliding-window-inverse/cache.py new file mode 100644 index 0000000000..db4c97557e --- /dev/null +++ b/research/sliding-window-inverse/cache.py @@ -0,0 +1,158 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Exact rational principal-window inverse updates, not a physical tape compiler. +Dugongue, with substantial OpenAI Codex assistance. See PROOF.md. +""" +from fractions import Fraction as F +from hashlib import sha256 +import json + +def need(ok,message): + if not ok:raise ValueError(message) + +class Arithmetic: + def __init__(self):self.counts={'add':0,'sub':0,'mul':0,'div':0} + def add(self,a,b):self.counts['add']+=1;return a+b + def sub(self,a,b):self.counts['sub']+=1;return a-b + def mul(self,a,b):self.counts['mul']+=1;return a*b + def div(self,a,b): + need(b!=0,'nonzero exact pivot');self.counts['div']+=1;return a/b + def total(self):return sum(self.counts.values()) + def dot(self,a,b): + need(len(a)==len(b),'dot dimensions') + if not a:return F(0) + z=self.mul(a[0],b[0]) + for x,y in zip(a[1:],b[1:]):z=self.add(z,self.mul(x,y)) + return z + def mm(self,A,B): + if not A:return [] + return [[self.dot(row,[B[k][j] for k in range(len(B))]) for j in range(len(B[0]))] for row in A] + +def identity(n):return [[F(i==j) for j in range(n)] for i in range(n)] + +def dense_inverse(A,ops=None): + o=Arithmetic() if ops is None else ops;n=len(A) + need(n>0 and all(len(r)==n for r in A),'nonempty square inverse') + M=[list(map(F,row))+identity(n)[i] for i,row in enumerate(A)] + for k in range(n): + pivot=next((i for i in range(k,n) if M[i][k]),None) + need(pivot is not None,'nonsingular matrix') + M[k],M[pivot]=M[pivot],M[k];d=M[k][k] + M[k]=[o.div(v,d) for v in M[k]] + for i in range(n): + if i==k:continue + c=M[i][k] + M[i]=[o.sub(v,o.mul(c,w)) for v,w in zip(M[i],M[k])] + return [r[n:] for r in M] + +def freeze(H): + n=len(H);need(n>1 and all(len(row)==n for row in H),'square global source') + need(all(type(v) in (int,F) for row in H for v in row),'exact rational entries') + return tuple(tuple(F(v) for v in row) for row in H) + +def fingerprint(H):return sha256(json.dumps([[str(v) for v in row] for row in H],separators=(',',':')).encode()).hexdigest() +def principal(H,labels):return [[H[i][j] for j in labels] for i in labels] + +def weighted(H,weights): + need(len(weights)==len(H) and all(type(v) in (int,F) and v>0 for v in weights),'positive rational weights') + return [[F(H[i][j])*F(weights[j])/F(weights[i]) for j in range(len(H))] for i in range(len(H))] + +def norm_inf(A):return max((sum(abs(v) for v in row) for row in A),default=F(0)) +def dominance_gap(G):return min(G[i][i]-sum(abs(v) for j,v in enumerate(G[i]) if i!=j) for i in range(len(G))) + +class WindowCache: + """Frozen source and read-only inverse view. Trusted methods preserve its invariant.""" + def __init__(self,H,labels,weights=None): + self._source=freeze(H);self.source_digest=fingerprint(self._source) + self.weights=tuple(F(v) for v in (weights if weights is not None else [1]*len(H))) + self.gap=dominance_gap(weighted(self._source,self.weights));need(self.gap>0,'weighted strict diagonal dominance') + need(len(labels)>0 and len(set(labels))==len(labels) and all(type(i) is int and 0<=i=0,'dyadic precision');S=1<0 and rho<1,'sufficient inverse residual') + return {'residual':str(rho),'gap':str(gap),'inverse_error_bound':str(rho/gap), + 'neumann_inverse_bound':str(norm_inf(Z)/(1-rho))} + + +def publish_owned(memory,ports,values): + need(len(ports)==len(values) and len(set(ports))==len(ports),'injective output port map') + result=dict(memory) + for port,value in zip(ports,values):result[port]=value + return result + +def round_nearest_integer(value): + value=F(value)+F(1,2) + return value.numerator//value.denominator + + +def apply_owned(cache,memory,ports): + need(len(ports)==len(cache.labels) and len(set(ports))==len(ports),'injective caller ports') + return publish_owned(memory,ports,cache.apply([memory[i] for i in ports])) + +def block_energy_factor(width,gap): + need(type(width) is int and width>0 and gap>0,'block bound inputs') + needed=F(width)/(gap*gap);depth=0 + while F(4)**depth=3,'synthetic cyclic dimension') + D=[F(2)**(i%4-1) for i in range(size)] + G=[[F(i==j)+(F(1,32) if (i-j)%size in (1,size-1) else 0) for j in range(size)] for i in range(size)] + H=[[D[i]*G[i][j]/D[j] for j in range(size)] for i in range(size)] + return H,D diff --git a/research/sliding-window-inverse/inputs/gaussian_check_setup.py b/research/sliding-window-inverse/inputs/gaussian_check_setup.py new file mode 100644 index 0000000000..529c2e7fe3 --- /dev/null +++ b/research/sliding-window-inverse/inputs/gaussian_check_setup.py @@ -0,0 +1,146 @@ +"""Independent exact identities for reduced rationals, matrix setup and rows.""" +from fractions import Fraction +from math import gcd +from gaussian_sources import require + + +def run(): + from cardinal_counts import Count + from check_support import no_decode + from compact_counts import write_fixed + from gaussian_matrix import Matrix, inverse, lu + from gaussian_rationals import Rational, read_rational, write_rational + from gaussian_rows import reverse_records + from records import Tape + from ring_check_words import body, decode + from ring_words import Signed + from router_metadata import owned + from scratch_pool import ScratchPool + from session import OuterScope, borrowed_tape, erase_marker, sealed_constructors + from words import BLANK + + def make(value): + value = Fraction(value) + return Rational(Signed(Count.literal(abs(value.numerator)), value < 0), + Count.literal(value.denominator)) + + def number(value): + n, d = decode(value.numerator.magnitude), decode(value.denominator) + require(gcd(n, d) == 1 and d > 0, "reduced physical rational") + return Fraction(-n if value.numerator.negative else n, d) + + def snapshot(value): + tape = borrowed_tape(value.tape) + return bytes(tape.cells), tape.head + + def matrix_values(matrix): + result = [] + for i in range(decode(matrix.rows)): + row = [] + for j in range(decode(matrix.columns)): + with owned(Count.literal(i), Count.literal(j)) as (a, b): + with owned(matrix.get(a, b)) as (value,): + row.append(number(value)) + result.append(row) + return result + + pool = ScratchPool(256) + scope = OuterScope(pool) + cases = 0 + values = (Fraction(0), Fraction(1), Fraction(-1), Fraction(17, 23), Fraction(-5, 7)) + with sealed_constructors(), scope.installed(): + try: + for a in values: + for b in values: + with owned(make(a), make(b), Count.literal(7)) as (left, right, precision): + saved = tuple(snapshot(x) for x in + (left.numerator.magnitude, left.denominator, + right.numerator.magnitude, right.denominator)) + for operation, expected in (("plus", a+b), ("minus", a-b), ("times", a*b)): + with no_decode(): + result = getattr(left, operation)(right) + with owned(result): + require(number(result) == expected, "exact encoded rational operation") + if b: + with no_decode(): + result = left.over(right) + with owned(result): + require(number(result) == a/b, "exact encoded rational quotient") + with no_decode(): + truncated = left.rounded(precision) + floor = left.integer_part() + ceil = left.integer_part(True) + with owned(truncated, floor, ceil): + def signed(x): + return (-1 if x.negative else 1)*decode(x.magnitude) + require(signed(truncated) == int(a*128), "signed dyadic truncation") + require(signed(floor) == a.__floor__() and signed(ceil) == a.__ceil__(), + "signed floor and ceiling") + require(saved == tuple(snapshot(x) for x in + (left.numerator.magnitude, left.denominator, + right.numerator.magnitude, right.denominator)), + "rational setup preserves input carriers") + cases += 1 + with owned(Count.literal(3)) as (dimension,): + source = [[Fraction(4), Fraction(-1), Fraction(0)], + [Fraction(1, 3), Fraction(5), Fraction(-1, 2)], + [Fraction(0), Fraction(1, 4), Fraction(3)]] + # Host lookup creates this boundary fixture only. All matrix + # elimination and its numerical indices use encoded tapes. + matrix = Matrix(dimension, dimension, pool, + lambda i, j: make(source[decode(i)][decode(j)])) + inv = lower = upper = None + try: + with no_decode(): + inv = inverse(matrix) + lower, upper = lu(matrix) + actual, low, high = (matrix_values(x) for x in (inv, lower, upper)) + for i in range(3): + for j in range(3): + require(sum(source[i][k]*actual[k][j] for k in range(3)) == int(i == j), + "exact inverse identity against independent rationals") + require(sum(low[i][k]*high[k][j] for k in range(3)) == source[i][j], + "exact LU identity against independent rationals") + require(matrix_values(matrix) == source, "matrix setup preserves source") + finally: + for value in (inv, lower, upper, matrix): + if value is not None: + value.close() + with owned(Count.literal(4), Count.literal(3)) as (length, width): + source, result, restored = pool.acquire(), pool.acquire(), pool.acquire() + try: + for value in (0, 3, 5, 7): + with owned(Count.literal(value)) as (word,): + write_fixed(word, source, width) + original = body(borrowed_tape(source)) + with no_decode(): + reverse_records(source, result, length, width) + reverse_records(result, restored, length, width) + require(body(borrowed_tape(result)) == b"".join( + original[offset:offset+3] for offset in (9, 6, 3, 0)), + "record reversal preserves each record bit order") + require(body(borrowed_tape(restored)) == original + and body(borrowed_tape(source)) == original, "reversal involution and input preservation") + finally: + for value in (source, result, restored): + value.clear() + with owned(make(Fraction(-17, 23))) as (value,): + tape = pool.acquire() + try: + with no_decode(): + write_rational(value, tape) + tape.rewind() + restored = read_rational(tape) + with owned(restored): + require(number(restored) == Fraction(-17, 23) and tape.read() == BLANK, + "canonical exact rational record") + finally: + tape.clear() + finally: + pool.empty() + require(not pool.live, "closed setup scratch pool") + for tape in pool.tapes: + erase_marker(tape) + require(tape.head == 1 and all(v == BLANK for v in tape.cells), "setup scratch restoration") + return {"rational_pairs": cases, "matrix_dimension": 3, "matrix_identities": 18, + "record_reversal": [4, 3], "pool_peak": pool.peak} diff --git a/research/sliding-window-inverse/reference.py b/research/sliding-window-inverse/reference.py new file mode 100644 index 0000000000..0ae85f1457 --- /dev/null +++ b/research/sliding-window-inverse/reference.py @@ -0,0 +1,22 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Separate forward-elimination/back-substitution oracle, no cache imports.""" +from fractions import Fraction as F + +def solve(A,b): + n=len(A);M=[list(map(F,row))+[F(b[i])] for i,row in enumerate(A)] + for k in range(n): + pivot=next(i for i in range(k,n) if M[i][k]);M[k],M[pivot]=M[pivot],M[k] + for i in range(k+1,n): + f=M[i][k]/M[k][k] + for j in range(k,n+1):M[i][j]-=f*M[k][j] + x=[F(0)]*n + for i in range(n-1,-1,-1):x[i]=(M[i][n]-sum((M[i][j]*x[j] for j in range(i+1,n)),F(0)))/M[i][i] + return x + +def inverse(A): + n=len(A);cols=[solve(A,[F(i==j) for i in range(n)]) for j in range(n)] + return [[cols[j][i] for j in range(n)] for i in range(n)] + +def determinant(A): + if not A:return F(1) + return sum(((-1)**j*A[0][j]*determinant([r[:j]+r[j+1:] for r in A[1:]]) for j in range(len(A))),F(0)) diff --git a/research/sliding-window-inverse/test_cache.py b/research/sliding-window-inverse/test_cache.py new file mode 100644 index 0000000000..7c48d234f3 --- /dev/null +++ b/research/sliding-window-inverse/test_cache.py @@ -0,0 +1,79 @@ +# SPDX-License-Identifier: Apache-2.0 +from fractions import Fraction as F +from pathlib import Path +from itertools import permutations +import tempfile,shutil,subprocess,sys,json +from cache import * +from fixtures import source_fixture,cyclic_fixture +from reference import inverse as oracle_inverse,determinant +ROOT=Path(__file__).resolve().parent + +def reject(fn): + try:fn() + except (ValueError,ZeroDivisionError):return + raise RuntimeError('invalid operation accepted') + +def main(): + H=source_fixture();checks=0 + # All label permutations, both orientations, and a nonconstant incoming diagonal. + for labels in permutations(range(3),2): + incoming=next(i for i in range(3) if i not in labels) + for method in ('schur','woodbury'): + cache=WindowCache(H,labels);cache.slide(incoming,method=method) + A=principal(H,cache.labels);Q=cache.inverse + need(Q==tuple(map(tuple,oracle_inverse(A))),'permuted source order') + det=determinant(A) + for i in range(2): + for j in range(2): + cofactor=(-1)**(i+j)*determinant([[A[r][c] for c in range(2) if c!=i] for r in range(2) if r!=j]) + need(Q[i][j]==cofactor/det,'separate cofactor identity') + checks+=1 + cache=WindowCache(H,[0,1]);saved=cache.inverse,cache.labels + reject(lambda:cache.slide(2,'wrong-source')) + need((cache.inverse,cache.labels)==saved,'rejected source preserves checkpoint') + reject(lambda:cache.slide(1));reject(lambda:cache.slide(-1));reject(lambda:cache.slide(2,method='other')) + reject(lambda:WindowCache(H,[0,0]));reject(lambda:WindowCache([[1,2],[2,1]],[0,1])) + reject(lambda:WindowCache(H,[0,1],[1,0,1]));reject(lambda:residual_certificate(H,[0,1],[1,1,1],[[0,0],[0,0]])) + # Omitting diagonal overlap correction is a real semantic error on the upstream fixture. + old=principal(H,[1,0]);new=principal(H,[1,2]);delta=[[new[i][j]-old[i][j] for j in range(2)] for i in range(2)] + naive=[[delta[i][1]*F(j==1)+F(i==1)*delta[1][j] for j in range(2)] for i in range(2)] + need(naive!=delta and delta[1][1]!=0,'double-counted diagonal mutant exposed') + # Do not replace the old nonsymmetric global model by a transposed or dense local model. + wrong=[list(r) for r in zip(*H)] + need(oracle_inverse(principal(wrong,[0,1]))!=oracle_inverse(principal(H,[0,1])),'wrong old-H model exposed') + # Arbitrary dirty exterior is preserved by injective finite output ports. + memory={i:('dirty',i,i*i) for i in range(-8,25)};ports=[2,7] + value=publish_owned(memory,ports,[F(5),F(-2)]) + need(all(value[i]==memory[i] for i in memory if i not in ports),'exterior frame') + need(memory[2]==('dirty',2,4),'input memory immutable') + reject(lambda:publish_owned(memory,[2,2],[1,2])) + cache=WindowCache(H,[0,1]);memory[2]=F(3);memory[7]=F(-4) + once=apply_owned(cache,memory,ports);twice=apply_owned(cache,once,ports) + vector=cache.apply(cache.apply([memory[i] for i in ports])) + need([twice[i] for i in ports]==list(vector),'fixed-port word embedding') + need(all(twice[i]==memory[i] for i in memory if i not in ports),'word exterior frame') + # Correlated blocks have no statistical-independence premise. + blocks=[(cache,[F(3),F(-4)]),(cache,[F(6),F(-8)])] + before=after=F(0);factor=F(0) + for item,vector in blocks: + depth,bound=block_energy_factor(len(item.labels),item.gap);factor=max(factor,bound) + before+=sum(v*v for v in vector);after+=sum(v*v for v in item.apply(vector)) + need(after<=factor*before,'direct-sum block energy bound') + # Tensor flattening is a permutation, so correlated squared energy is invariant. + tensor=[[[F(i+2*j-3*k) for k in range(3)] for j in range(2)] for i in range(2)] + first=[tensor[i][j][k] for i in range(2) for j in range(2) for k in range(3)] + second=[tensor[i][j][k] for k in range(3) for i in range(2) for j in range(2)] + need(sum(v*v for v in first)==sum(v*v for v in second),'pack norm and frame invariance') + reject(lambda:recover_known_integer([F(1,2)],F(1,2))) + reject(lambda:recover_known_integer([F(0)],F(-1))) + # Actual export/CLI must reject changed immutable sources and changed claims. + with tempfile.TemporaryDirectory() as temporary: + target=Path(temporary)/'package';shutil.copytree(ROOT,target,ignore=shutil.ignore_patterns('__pycache__')) + command=[sys.executable,'-B',str(target/'verify.py')] + need(subprocess.run(command,capture_output=True,timeout=60).returncode==0,'export positive') + file=target/'inputs/gaussian_check_setup.py';raw=file.read_bytes();file.write_bytes(raw+b' ') + need(subprocess.run(command,capture_output=True,timeout=60).returncode!=0,'source drift accepted');file.write_bytes(raw) + file=target/'RESULT.json';data=json.loads(file.read_text());data['slides']+=1;file.write_text(json.dumps(data)) + need(subprocess.run(command,capture_output=True,timeout=60).returncode!=0,'false receipt accepted') + print('PASS_WINDOW_CONTROLS',checks,'permuted independent/cofactor cases; source, alias, residual, diagonal, model, exterior, tensor and CLI controls') +if __name__=='__main__':main() diff --git a/research/sliding-window-inverse/verify.py b/research/sliding-window-inverse/verify.py new file mode 100644 index 0000000000..398f216c68 --- /dev/null +++ b/research/sliding-window-inverse/verify.py @@ -0,0 +1,64 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Bounded exact reuse/rounding replay; ordinary execution never rewrites receipts.""" +from pathlib import Path +from fractions import Fraction as F +import hashlib,json +from cache import (Arithmetic,WindowCache,dense_inverse,principal,need, + rounded_weighted_inverse,residual_certificate,round_nearest_integer,recover_known_integer,inverse_height_bound) +from fixtures import source_fixture,cyclic_fixture +from reference import inverse as independent_inverse +ROOT=Path(__file__).resolve().parent + +def result(): + for name,digest in json.loads((ROOT/'INPUTS.json').read_text()).items(): + need(hashlib.sha256((ROOT/name).read_bytes()).hexdigest()==digest,'source hash '+name) + cases=[('upstream-setup-3',source_fixture(),[F(1)]*3,[1,2,3])] + H,D=cyclic_fixture();cases.append(('weighted-cyclic-13',H,D,[1,2,4,8])) + rows=[];total=0;restored=0 + for name,H,D,widths in cases: + for width in widths: + for method in ('schur','woodbury'): + cache=WindowCache(H,list(range(width)),D);source=cache._source + costs=[];max_residual=F(0);max_error=F(0);max_height=0 + baseline=Arithmetic();dense_inverse(principal(H,range(width)),baseline) + for t in range(2*len(H)): + incoming=(width+t)%len(H) + costs.append(cache.slide(incoming,cache.source_digest,method)) + A=principal(H,cache.labels);Q=independent_inverse(A) + need(cache.inverse==tuple(map(tuple,Q)),'independent exact inverse') + n=len(A) + for side in (0,1): + for i in range(n): + for j in range(n): + value=sum(((A[i][k]*cache.inverse[k][j] if side==0 else cache.inverse[i][k]*A[k][j]) for k in range(n)),F(0)) + need(value==F(i==j),'two-sided exact inverse') + # Correlated payloads: duplicate/scaled columns do not require independence. + x=[F((-1)**i*(i+1)) for i in cache.labels] + b=[sum((A[i][j]*x[j] for j in range(n)),F(0)) for i in range(n)] + need(cache.apply(b)==tuple(x),'exact integer-valued solve') + Z=rounded_weighted_inverse(cache,16) + cert=residual_certificate(H,cache.labels,D,Z);rho=F(cert['residual']) + dw=[D[i] for i in cache.labels];bw=[b[i]/dw[i] for i in range(n)] + approximate=[dw[i]*sum((Z[i][j]*bw[j] for j in range(n)),F(0)) for i in range(n)] + error=max(abs(a-e) for a,e in zip(approximate,x)) + bound=max(dw)*F(cert['inverse_error_bound'])*max(abs(v) for v in bw) + need(error<=bound