Prove sharp read savings for encoded Gaussian inverse setup (no κ)

research/gaussian-inverse-settled-columns/PROOF.md

@@ -0,0 +1,111 @@
+# Exact inverse refinement and its resource boundary
+
+This scoped proof and implementation were produced by Nick Petalas.
+The Gauss-Jordan algorithm and its identity-column invariant are classical.
+Jose Manuel / jmbarrancoml, PR3851, supplies the exact encoded implementation
+to which this refinement applies. Its Gaussian construction is a cited
+premise, not a result audited here. New work is Apache-2.0.
+
+## Contract
+
+Take a positive-dimensional square exact rational `Matrix` accepted by the
+retained no-pivot inverse. Each successive pivot must be positive. Matrix
+entries are canonical reduced rational records. Numerical payloads and
+indices use the retained encoded tape operations; fixture construction and
+final checking are separate host boundaries. Sufficient scratch leases for
+the stated extra counts are required; a pool sized only for the original
+peak is not promised to suffice.
+
+The candidate starts from the same `[A | I]`, uses the same normalization
+and elimination arithmetic, checks each pivot at the same point, and copies
+the same final right block. It changes only the column iterator in the two
+row-operation loops from `[0,2n)` to `[k,2n)` at pivot `k`.
+
+## Equality of states and accepted domain
+
+Before pivot `k`, the first `k` columns of the augmented matrix equal the
+first `k` columns of `I`. This holds vacuously at zero. In particular every
+entry `(k,j)` with `j<k` is exactly zero.
+
+Normalization in the retained implementation reads these entries, tests
+zero, and skips them. The candidate omits exactly those reads. In every
+other row, elimination first captures its factor from column `k`. For
+`j<k` the source entry in row `k` is zero, so the retained implementation
+again reads it and skips every multiplication and write. The candidate
+omits exactly those source reads. Both implementations perform identical
+arithmetic and writes for every `j>=k`, in identical order. Column `k`
+becomes the `k`th identity column. Induction proves both the invariant and
+bit-identical augmented matrix contents after every completed pivot.
+
+The next pivot is therefore identical, including its sign and reduced
+representation. A nonpositive pivot rejects in both implementations. A
+nonsquare matrix rejects before augmentation in both. The iterator's
+extra order guard always holds, since `0<=k<n<2n`. The accepted numerical
+domain is unchanged. After the last pivot, both return the same encoded
+inverse matrix. Suppressing reads of known zeros cannot change borrowed
+input data or exterior state. The cursor owns and closes its two added
+`Count` values; the retained augmented matrix remains closed in `finally`.
+
+## Exact matrix-read reduction
+
+Let `m_k` be the number of nonzero off-diagonal elimination factors at
+pivot `k`. Both algorithms have the same `m_k` by the state induction.
+Normalization omits `k` matrix reads. Each of those `m_k` row eliminations
+omits another `k` source reads. All remaining matrix reads and all matrix
+writes agree, including augmentation and result construction. Thus
+
+```text
+saved Matrix.get calls = sum(k * (1 + m_k), k=0,...,n-1).
+```
+
+Since `0<=m_k<=n-1`, the sharp general interval is
+
+```text
+n(n-1)/2 <= saved reads <= n^2(n-1)/2.
+```
+
+An identity matrix attains the lower bound. For the upper bound use
+`A=nI+J`, where `J` is the all-ones matrix. After eliminating `k` columns,
+the unprocessed Schur block has the form `nI+c_k J` with `c_k>0`, because
+eliminating one pivot changes `c` to `nc/(n+c)>0`. The already processed
+rows have the same nonzero coefficient on every unprocessed column;
+their common coefficient begins positive and updates by multiplication
+by `n/(n+c)>0`. Thus every off-diagonal factor is nonzero and `m_k=n-1`.
+Every pivot is positive. This proves attainment in every dimension.
+
+For `n=4`, this is the literal fixture `4I+J`. The physical checker measures
+236 versus 212 matrix reads and 80 writes on each side. Its separate
+rational trace derives the 24 omitted reads rather than assuming density.
+
+## Costs not hidden by the read count
+
+The suffix iterator additionally owns a cursor and a length while the
+retained iterator owns its own index and remaining counter. These are
+encoded `O(log n)`-bit counts, closed after each finite traversal. The
+candidate does not claim a universal reduction in every tape operation,
+wall time or scratch capacity.
+
+For the complete `4I+J` fixture, including input construction, decoding,
+and final pool cleanup, the retained pool's own meters report
+
+```text
+                 baseline   candidate
+record reads       947301      922401
+record writes      187399      182739
+unit head moves    869032      846336
+peak pool leases       34          36
+```
+
+These are actual finite pooled-record-tape counters. They are not a
+complete machine instruction count or a supplier invoice. In particular
+the two extra peak leases are paid explicitly. Both runs execute under
+`sealed_constructors` and disallow host payload decoding during inversion.
+All returned source records agree and all pool tapes are blank at return.
+
+Cold-process measurements include source hash authentication, extraction,
+imports, input construction, inversion, output consumption and cleanup.
+They do not establish a runtime improvement. The written theorem is the
+all-dimension semantics and matrix-read refinement; finite checks alone
+do not prove it universally. Native all-column validity, numerical
+Gaussian admission, production pages and a complete multiplication caller
+remain outside this result.

research/gaussian-inverse-settled-columns/README.md

@@ -0,0 +1,135 @@
+# Skip settled columns in encoded Gaussian inverse setup
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped semantics/resource proof with exact finite corroboration.
+The exact positive-pivot inverse of Jose Manuel's
+[PR3851](https://github.com/CrocSwap/integer-mult-bounds/pull/3851)
+can omit reads of its completed identity columns. At pivot k, with m_k
+nonzero off-diagonal elimination factors, the exact saving is
+
+```text
+sum k(1+m_k) matrix reads,
+between n(n-1)/2 and n^2(n-1)/2, both sharp.
+```
+
+The candidate performs identical rational arithmetic and matrix writes,
+returns identical encoded output and preserves the positive-pivot numerical
+domain. It requires additional scratch. [PROOF.md](PROOF.md) gives the
+all-dimension invariant, sharp examples and resource boundary. No new kappa
+or selected-frontier change is claimed.
+
+For the literal physical 4-by-4 matrix `4I+J`, where J is all ones:
+
+| Measured complete finite workload | Retained inverse | Candidate |
+| --- | ---: | ---: |
+| Matrix reads during inversion | 236 | 212 |
+| Matrix writes during inversion | 80 | 80 |
+| Pooled tape reads | 947301 | 922401 |
+| Pooled tape writes | 187399 | 182739 |
+| Pooled unit head moves | 869032 | 846336 |
+| Peak pool leases | 34 | 36 |
+
+The pooled counters include input construction, output decoding and final
+cleanup. They include the suffix iterator's extra scratch operations. They
+are finite record-tape counters, not a complete machine instruction count
+or recursive supplier invoice. A pool sized only for the original peak
+need not suffice. The first checked improvement is shipped without further
+optimization.
+
+## Evidence and reproduction
+
+The new checker executes ten paired physical fixtures, checks every output
+against a separate rational trace and both inverse products, and confirms
+the exact read reduction and unchanged writes. Eight executions reject
+nonsquare, singular, zero-pivot and negative-pivot inputs with the same
+messages and cleanup. Another 81 rational matrices corroborate the identity
+invariant. All checks use explicit exceptions and survive optimized Python.
+The inversion itself runs under sealed constructors and a host-decoding ban.
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gaussian-inverse-settled-columns/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/gaussian-inverse-settled-columns/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gaussian-inverse-settled-columns
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gaussian-inverse-settled-columns --check-source-history --check-modes
+```
+
+Other hosts may substitute their CPython 3.12 path. The direct checker writes
+no files and prints a generated receipt bound to every package file. It
+authenticates all five live inputs before importing the retained physical
+runtime. An official package export includes those inputs and supports a
+Git-free replay; full history is needed only for the repository provenance
+checks. No predecessor scientific verifier is imported or replayed.
+
+## Cold runtime limit
+
+Run the separate benchmark with
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gaussian-inverse-settled-columns/benchmark.py --pairs 9
+```
+
+Nine alternating fresh-process pairs on macOS arm64, CPython 3.12.15,
+give medians 0.928621375 seconds retained and 0.922816875 seconds candidate.
+Their ranges are 0.917676334 to 1.030556625 seconds and 0.909664875 to
+0.998733333 seconds. All eighteen complete output byte strings agree and
+there are zero errors. This comparison is inconclusive: the median gap is
+smaller than the observed variation. No wall-time speedup is claimed.
+
+The timed region includes authentication, nested export extraction, imports,
+fixture construction, inversion, literal output checking and cleanup. A
+separate profile of the same 4-by-4 workload places the retained inversion
+at 0.703 of 1.532 profiled seconds; `Matrix.get` accounts for 0.189 seconds. Authentication and
+extraction dominate this tiny cold workload. The host has eighteen logical
+CPUs, and other processes were active. Alternating sides limits drift but
+does not remove contention. Neither side uses result caching or a changed
+fixture. Timing is not a CI acceptance threshold.
+
+## Open next questions
+
+The structured questions and blockers are in [TASK.json](TASK.json).
+
+1. Can one exact streamed row update reduce complete tape work without
+   increasing peak scratch? First specify every borrowed record, scan and
+   cleanup operation. No such primitive or cost proof is supplied here.
+2. Does this inverse improve a complete reached Gaussian preparation?
+   First compare an actual preparation page, its full output bytes,
+   ownership and pooled meters. Production pages and a full caller
+   benchmark were not run.
+
+## Credit, scope and implementation limits
+
+Jose Manuel / jmbarrancoml retains PR3851's physical Gaussian setup,
+positive-pivot rational inverse, encoded tape operations and word-product
+lineage. Chafik Boukhalfa, RaD/hipotures, Mason Hale, Dugongue and the
+retained arithmetic, Gaussian and multiplication contributors retain their
+source credit. Existing files and attribution are unchanged. Gauss-Jordan
+elimination and its identity-column argument are classical; the new result
+is their checked physical read-count refinement in this exact implementation.
+
+The canonical base is `a5bff3bf133e482541c09eba4e773884bdb2b1b7`, priority
+revision 8. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19279747)
+and [TASK.json](TASK.json) record the original question and bounded overlap
+coverage. Direct live PR/Discussion and main-tree searches supplement the
+helper's incomplete sparse local coverage. Unpublished work and arbitrary
+historical code diffs are outside that search.
+
+The source Gaussian theorem is cited rather than audited. Native all-column,
+numerical Gaussian admission, production preparation, precision/tape/stock,
+complete caller and all five selected framework assumptions remain open.
+No selected scientific cold replay, Lean or Docker run was performed.
+Independent human and formal proof-kernel review are unclaimed.
+
+Power of Ten inspection covers the five new Python files. Functions are
+under sixty lines; numerical loops are bounded by matrix dimension and
+fixtures by width four. The 81-matrix host domain and at most fifteen
+benchmark pairs are explicit. Subprocesses have sixty-second timeouts.
+Source files are capped at 128 MiB and the manifest at 64 KiB and sixteen
+rows. Recursion and runtime code generation are absent from new code.
+Managed Python allocation is a rule-3 deviation; inherited tape buffers
+also allocate dynamically, so no fixed-storage implementation is claimed.
+The two engine choices, source loader, fixture constructor and temporary
+instrumentation are bounded indirect calls, a rule-9 deviation. Strict
+warnings and normal/optimized replays are the available local diagnostics.

research/gaussian-inverse-settled-columns/SOURCES.json

@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7",
+  "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/physical-gaussian-core/gaussian_matrix.py",
+      "usage": "input",
+      "git_blob": "fc41183a42f5e1af5ea2294c295a0519abbcdb6c",
+      "sha256": "5bb982c6f36083b646bd5a5ab2ea4059c203fa0cc824e9f28132c0f323824bac"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_rationals.py",
+      "usage": "input",
+      "git_blob": "053404d91c1bef0d4bb0f6647491847bf5879aaf",
+      "sha256": "6f9a380c8c7b4233c3bc338a6206d65cc85bee2e4f5625c2a212065f04f4b73d"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_sources.py",
+      "usage": "input",
+      "git_blob": "ce521f91997775e189f984ba7dd68a15bf9ecd9b",
+      "sha256": "c5889a97a11a9c6c6c44deb8a2042498ddc3f55703de15269132b8f198e24b15"
+    },
+    {
+      "path": "research/physical-gaussian-core/inputs/branchfree-source.tar",
+      "usage": "input",
+      "git_blob": "48dc77f5145d649bfed6745e38ab18b11772d597",
+      "sha256": "e6cdacd59a067189a99bfe03f4448913bb8d518ed4a9b1d981a68c5c666529c7"
+    },
+    {
+      "path": "research/physical-gaussian-core/inputs/word-export.tar",
+      "usage": "input",
+      "git_blob": "885794cf3328941209034ee2d946ed76dbea8ce3",
+      "sha256": "d428e8b6aef4d348fa2e922ca64c4cfd634bbb2f0c150033273e65fcf4600b49"
+    }
+  ]
+}

research/gaussian-inverse-settled-columns/TASK.json

@@ -0,0 +1,80 @@
+{
+  "schema_version": 1,
+  "task_id": "replay-runtime",
+  "priority_revision": 8,
+  "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7",
+  "original_card": {
+    "id": "replay-runtime",
+    "question": "Can one measured replay bottleneck be sped up without dropping coverage?",
+    "starting_points": [
+      "scripts/run_isolated_tests.py",
+      "scripts/verify_replay_coverage.py",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Profile one isolated replay and optimize the measured bottleneck.",
+      "Design source-bound reuse with explicit dependency invalidation and negative controls."
+    ],
+    "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.",
+    "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.",
+    "allowed_variations": [
+      "Profile one stage or design one source-bound cache boundary."
+    ],
+    "scope_change_triggers": [
+      "Skipping coverage or comparing different fixtures to claim speedup."
+    ],
+    "overlap_terms": [
+      "replay runtime",
+      "cache invalidation",
+      "isolated tests"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Skip settled leading identity columns in the exact encoded Gaussian inverse; prove the read-count saving and test the complete finite physical boundary.",
+  "scope_change_reason": "This is an encoded preparation component used by Gaussian replays. Cold runtime measurements are reported even when inconclusive; the proved improvement is matrix-read count.",
+  "bottleneck_link": "Fewer exact setup scans can reduce preparation work for physical Gaussian experiments. This component does not alter the recursive paid invoice or supply a new kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first exact read-count improvement, with the full scratch tradeoff and measured cold-command limits; do not extend the optimizer.",
+  "outcome": "completed",
+  "evidence": "Written all-dimension read-count refinement; ten paired physical fixtures, 81 rational matrices and eight rejecting executions. Dense dimension four saves 24 of 236 matrix reads and reduces each pooled-tape meter at a two-lease peak cost. Cold runtime comparison is inconclusive.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a row-streaming inverse reduce complete tape work without increasing peak scratch?",
+      "why_it_matters": "The present suffix cursor saves reads but uses two extra peak leases.",
+      "first_step": "Specify one exact batched row update and charge every stream scan and cleanup.",
+      "blocked_by": "No such physical update or complete cost proof is supplied."
+    },
+    {
+      "question": "Does replacing the setup inverse improve a complete Gaussian preparation on a reached caller?",
+      "why_it_matters": "Source authentication dominates the cold tiny inversion command; a component improvement is not an end-to-end speedup.",
+      "first_step": "Pin one actual preparation page and compare complete bytes, ownership and pooled meters.",
+      "blocked_by": "No production-size preparation or full caller benchmark was run."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19279747",
+  "source_predecessor": {
+    "pr": 3851,
+    "author": "jmbarrancoml",
+    "role": "Exact encoded positive-pivot inverse and physical Gaussian setup; cited construction, not audited."
+  },
+  "freshness": {
+    "canonical_main": "a5bff3bf133e482541c09eba4e773884bdb2b1b7",
+    "priority_revision": 8,
+    "selected_kappa": "0.003125804",
+    "orientation": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+    "overlap_limits": "Cached snapshot covers 338 open PRs and 5959 Discussion records; sparse local coverage is incomplete. Direct live PR/Discussion and main README searches supplement it. Unpublished work and arbitrary historical diffs are not covered."
+  }
+}