From 439b7c9b1bada7a3cb4c4d41347e236c32615dcb Mon Sep 17 00:00:00 2001
From: Nick Petalas <webmasternikos@gmail.com>
Date: Tue, 27 Oct 2026 22:04:32 +0000
Subject: [PATCH] feat(research): prove chronological helper repair tariff

---
 research/chronological-helper-repair/PROOF.md | 195 ++++++++++++
 .../chronological-helper-repair/README.md     | 132 ++++++++
 .../chronological-helper-repair/SOURCES.json  |  36 +++
 .../chronological-helper-repair/TASK.json     |  92 ++++++
 .../chronological-helper-repair/VERIFY.json   |  34 ++
 .../chronological-helper-repair/verify.py     | 291 ++++++++++++++++++
 6 files changed, 780 insertions(+)
 create mode 100644 research/chronological-helper-repair/PROOF.md
 create mode 100644 research/chronological-helper-repair/README.md
 create mode 100644 research/chronological-helper-repair/SOURCES.json
 create mode 100644 research/chronological-helper-repair/TASK.json
 create mode 100644 research/chronological-helper-repair/VERIFY.json
 create mode 100644 research/chronological-helper-repair/verify.py

diff --git a/research/chronological-helper-repair/PROOF.md b/research/chronological-helper-repair/PROOF.md
new file mode 100644
index 0000000000..56eacea14b
--- /dev/null
+++ b/research/chronological-helper-repair/PROOF.md
@@ -0,0 +1,195 @@
+# Chronological helper spill and sharp boundary repair
+
+This is a scoped all-field linear-algebra proof. It gives no native price,
+physical supplier or multiplication exponent. The contribution was produced
+by Nick Petalas. Apache-2.0.
+
+## The fixed replacement model
+
+Let F be any field and let h in F^k be k arbitrary initial helper values.
+An invertible scalar word returns h unchanged. It can have any number of
+invertible events. Fix k ordered cuts. At cut i the original prefix is P_i.
+Choose a cut row a_i and column b_i such that a_i b_i=1. Define
+
+```text
+c_i = a_i P_i,       d_i = P_i^-1 b_i,
+C   = matrix with rows c_i,
+D   = matrix with columns d_i.
+```
+
+Assume C is invertible. No invertibility assumption is made on D or CD.
+The choice of cuts, rows and columns is fixed before seeing any data.
+There are k further arbitrary independent inputs z_1,...,z_k, all public
+from the start. At cut i return t_i=a_i x, retain that output, and replace
+the live state by
+
+```text
+x <- x + b_i (z_i - t_i).
+```
+
+This is an invertible replacement, not an erasure. Since a_i b_i=1,
+decompose x=b_i(a_i x)+(x-b_i a_i x). The event swaps the first coordinate
+with z_i and preserves the second. The old coordinate t_i remains an
+output. Any realization by local bases still has to pay for those bases.
+
+This is the independent-input replacement semantics of Ali Romman's
+[PR #5599](https://github.com/CrocSwap/integer-mult-bounds/pull/5599),
+applied to several fixed cuts of one identity helper word. Its physical
+common-chart hypotheses are additional requirements, not consequences
+of the scalar model here. Main fields, owned lifetimes and nonidentity
+helper endpoints are outside this theorem unless a separate reduction
+to this identity block is supplied.
+
+Write the pairing matrix as
+
+```text
+K = CD = I + L + U,
+```
+
+where L is strictly lower triangular and U is strictly upper triangular.
+The diagonal is one because c_i d_i=a_i b_i=1. Let f denote the final live
+helper vector, after the original word's terminal identity has completed.
+
+## The complete causal map
+
+The following identities hold for every h,z over every field:
+
+```text
+(I+L)t = Ch + Lz,
+Cf     = (I+U)z - Ut.                         (1)
+```
+
+To prove them, pull the current live state back through the original prefix.
+If u is this boundary-coordinate state, replacement i changes it by
+d_i(z_i-t_i). The original scalar events between cuts do not change u.
+Consequently,
+
+```text
+t_i = c_i h + sum_(j<i) K_ij (z_j-t_j),
+f   = h + D(z-t).
+```
+
+The first equation gives the first line of (1). Multiplying the second by
+C and substituting Ch=(I+L)t-Lz gives the second line. No simultaneous-cut
+commutation, joint basis or pairwise-independence premise was used.
+
+Let A=(I+L)^-1, which exists because L is nilpotent. The two cross-input
+coefficient maps have exact ranks
+
+```text
+rank(z -> t, holding h fixed) = rank(AL) = rank(L),
+rank(h -> f, holding z fixed) = rank(-C^-1 UAC) = rank(U).       (2)
+```
+
+Both statements are invariant under separate invertible changes of basis
+within the early-output bank and within the final-helper bank.
+
+Thus individual equations c_i d_i=1 do not certify independent splits.
+The early outputs depend only on old inputs exactly when L=0. The final
+helpers depend only on new inputs exactly when U=0. Both requirements hold
+without communication between the two output banks exactly when CD=I.
+Here independence means the prescribed old/new input partition; allowing
+a new input basis that mixes h and z changes the contract.
+
+## Exact repair tariff when the early targets are already valid
+
+Suppose L=0. The early bank is then t=Ch and can remain untouched. Define
+r=rank(U). Grant free invertible linear operations confined to either bank.
+A cross-bank update adds B times one bank to the other and costs rank(B).
+Rank-one updates therefore cost one unit. Coefficients and local basis
+operations are unrestricted over F. This is a relaxation of physical
+delivery, not a native rank tariff.
+
+The least total cross-bank cost that makes all final helpers independent
+of h, preserves the early outputs, and restores every auxiliary field is
+exactly r. Any finite clean or dirty workspace is permitted on either side
+of a fixed bank partition. Auxiliary fields must return to their original
+values. Cross-bank updates in either direction are allowed.
+
+For the lower bound, fix z and every auxiliary input, and vary h. The
+coefficient of h in all live-side fields initially has rank r by (2).
+Adjoining fixed clean or dirty workspace only appends zero rows. An
+invertible operation confined to the live side preserves this rank.
+An operation confined to the early side leaves it unchanged. A cross-bank
+update into the live side with matrix B changes the coefficient matrix
+by rank at most rank(B). The inequality
+
+```text
+|rank(M+E)-rank(M)| <= rank(E)
+```
+
+therefore forces total charge at least r before that coefficient can be
+zero. At the desired endpoint every final helper and every restored
+live-side auxiliary is independent of h. Updates into the early side
+cannot reduce this lower bound. The proof uses neither a workspace limit
+nor a sign, characteristic or nonzero-state assumption.
+
+For attainment, take any rank factorization
+U=sum_(s=1)^r v_s w_s^T. Execute
+
+```text
+f <- f + (C^-1 v_s)(w_s^T t),       s=1,...,r.
+```
+
+These are r rank-one updates from the retained early bank. Equation (1)
+then gives Cf=(I+U)z. The live-side normalizer (I+U)^-1 C returns f=z.
+The early bank remains t=Ch; no workspace is needed. This proves both
+the exact cross-bank charge and a constructive endpoint decoder.
+
+If the early outputs are physically unavailable for later reading, this
+attainment is unavailable. The rank lower bound still applies to any
+implementation in the stated larger relaxation. Similarly, free local
+bases in this tariff must receive their actual scalar, native, routing,
+precision and storage charges before use in a supplier invoice.
+
+## A sharp obstruction of arbitrary size
+
+For every k>=2 choose C=I and D=I+N, where N has ones on the first
+superdiagonal and zeros elsewhere. Then L=0 and U=N has rank k-1.
+Every individual replacement is normalized, and every early output is
+exactly t_i=h_i. Nevertheless,
+
+```text
+f_i = z_i + z_(i+1) - h_(i+1)       for 1<=i<k,
+f_k = z_k.
+```
+
+The final helpers retain k-1 independent old-input directions. They need
+exactly k-1 cross-bank rank units to repair. In particular, counting k
+individually valid cuts as k independent target splits misses a deficit
+of arbitrary size in this fixed-direction model.
+
+An explicit scalar repair adds t_(i+1) to f_i for all i<k. Processing
+i=k-1,...,1, subtract the already normalized f_(i+1) from f_i. This word
+uses k-1 cross-bank additions and k-1 within-bank additions, returns
+f=z, and preserves every early output. Optimality is claimed for the
+cross-bank rank charge only, not the total scalar addition count.
+
+## Evidence and scope
+
+`verify.py` builds an explicit identity source word with changing invertible
+prefixes, performs the literal cut replacements on all input coefficients,
+and compares its endpoint with (1). It checks (2), the full reversible
+endpoint and the attaining rank-factor repair. Finite-field and rational
+domains are bounded and enumerated in its output. A separate binary
+outer-product enumeration rejects every one-unit repair of a rank-two
+sharp-family defect. Incorrect diagonal, basis and field fixtures fail.
+
+The universal result rests on this written proof. The finite replay is
+corroboration, not proof-kernel or independent human acceptance. Causal
+elimination, nilpotent triangular inverses, rank factorization and rank-cut
+lower bounds are classical. The proposed new contribution is their exact
+chronological helper-replacement application, with both leakage ranks,
+the sharp repair tariff and the explicit family. No general literature
+priority is claimed.
+
+Ali Romman's #5599 supplies the single-cut replacement contract and its
+retained P104 lineage. His [#5615](https://github.com/CrocSwap/integer-mult-bounds/pull/5615)
+supplies the dyadic single-cut pairing context. This theorem does not
+compute a dyadic module capacity or recheck either predecessor.
+
+No actual P104 cut is constructed here. Distinct output charts, physical
+availability of retained early outputs, restricted coefficient alphabets,
+native operators, dirty-state physical restoration, the complete signed
+moment, compiler and outer transfer remain separate obligations. The
+selected frontier and all five selected framework assumptions are unchanged.
diff --git a/research/chronological-helper-repair/README.md b/research/chronological-helper-repair/README.md
new file mode 100644
index 0000000000..71288f4e9f
--- /dev/null
+++ b/research/chronological-helper-repair/README.md
@@ -0,0 +1,132 @@
+# Chronological helper spill has an exact repair rank
+
+This scoped written proof determines how multiple individually normalized
+helper replacements interfere. The contribution was produced by Nick Petalas.
+It does not change kappa or the selected frontier.
+
+For a scalar identity helper word, transport the row and column at ordered
+cut i to the input boundary as c_i,d_i, with c_i d_i=1. Assume the k rows
+form an invertible helper basis C, and put the columns in D. Write
+CD=I+L+U, with strictly lower L and strictly upper U. For arbitrary old
+inputs h, independent replacement inputs z, early outputs t and final
+helpers f, the complete map is
+
+```text
+(I+L)t = Ch + Lz,
+Cf     = (I+U)z - Ut.
+```
+
+The early outputs have new-input leakage rank exactly rank(L). Final
+helpers have old-input leakage rank exactly rank(U). Both banks are
+independent under the prescribed old/new input partition without repair
+exactly when CD=I. Separate invertible basis changes within either bank
+cannot remove these leakage ranks.
+
+When L=0, exactly rank(U) cross-bank rank units suffice and are necessary
+to repair the final helpers. This allows arbitrary finite restored clean
+or dirty workspace and grants free invertible operations within either
+bank. It is an optimistic linear communication tariff, not a physical
+Gaussian rank tariff. For every k>=2 an explicit family has k individually
+valid cuts, already independent early outputs, and repair cost k-1.
+
+[PROOF.md](PROOF.md) contains the all-field derivation, workspace-robust
+lower bound and attaining decoder. Classical elimination and rank-cut
+methods are credited as methods. The new contribution is this precise
+chronological helper-replacement application. No general literature
+priority is claimed.
+
+## Reproduce
+
+From the repository root, using standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/chronological-helper-repair/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/chronological-helper-repair/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/chronological-helper-repair
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/chronological-helper-repair --check-source-history --check-modes
+```
+
+Another CPython 3.12 executable can replace the absolute interpreter path.
+The direct commands print `PASS_CHRONOLOGICAL_HELPER_REPAIR` and a generated
+SHA256 receipt covering all six package files. The registered replay also
+prints `PASS_REGISTERED_RESEARCH_PACKAGE`.
+
+The verifier replays changing original prefixes and literal cut events
+on every input coefficient. It compares this direct endpoint with the
+closed form, checks both leakage ranks and full reversibility, and emits
+minimal rank-factor repairs when L=0. Its finite domains are:
+
+- All 10,752 pairs of an invertible binary 3-by-3 C and a unit-diagonal
+  binary 3-by-3 K, and all 729 ternary unit-diagonal 3-by-3 K with C=I.
+- All 25 quinary unit-diagonal 2-by-2 K with C=I, and 72 rational fixtures
+  through k=6, including nontrivial dyadic C and nonzero L and U.
+- Twenty-five sharp-family cases over Q, F2, F3, F5 and F7 through k=6.
+  An independent enumeration rejects all 64 binary outer products as
+  one-unit repairs of a rank-two defect.
+- Eight invalid-domain fixtures and four semantic controls, including
+  reversed chronological pairing and the biorthogonal positive control.
+
+The three finite-field domains contain 1,376 cases with L=0. The
+rational domain contains 43. Every such case checks the attaining repair;
+the sharp-family checks are additional fixtures and can overlap those
+domains. Counts are enumerated by the verifier, not extrapolated.
+
+## Scope and predecessor credit
+
+The target was an original causal-composition question under the current
+`coverage-law-change` card, not a follow-up question taken from another
+package. It changes the single-cut premise to multiple prescribed cuts.
+The task and exact provenance are in [TASK.json](TASK.json) and
+[SOURCES.json](SOURCES.json), based on canonical main
+`19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8.
+
+Ali Romman's [#5599](https://github.com/CrocSwap/integer-mult-bounds/pull/5599)
+supplies the independent-input replacement contract and the retained
+Pierre-Loic Doulcet, Cinna Davis, Jacob Alan Sussman and P104 lineage.
+His [#5615](https://github.com/CrocSwap/integer-mult-bounds/pull/5615)
+supplies the dyadic single-cut pairing context. They are cited premises,
+not audit or scientific-replay deliverables of this package. Historical
+multi-cut response-kernel work concerns a different replacement operation.
+
+The result is a written proof with exact finite corroboration. It is not
+a finite search failure, native certificate, complete multiplier theorem
+or independently accepted formal proof. Physical cut eligibility, common
+charts, availability of retained early outputs, scalar bases, coefficient
+restrictions, native alignment, ownership, precision, stock, complete
+signed moment, compiler and outer funding remain payable. All five
+selected framework assumptions remain. No selected supplier cold replay,
+Lean or Docker run is performed.
+
+Independent human and formal proof-kernel review are unclaimed.
+Apache-2.0.
+
+## Open next questions
+
+1. Does one changed P104 word contain a full or separately justified
+   partial family of eligible cuts with zero lower pairing and nonzero
+   upper pairing? Extract exact transported rows and columns from a named
+   word. The blocker is physical eligibility and chart compatibility,
+   not the scalar formula.
+2. Can a real consumer deliver the necessary early-output reads within
+   a favorable complete signed moment? Start with a rank factorization
+   of that actual U and charge every read, basis operation and restore.
+   The tariff here grants free operations that a physical caller must pay.
+
+## Verification design
+
+The kept code has no recursion, dynamic code execution or external
+scientific dependency. Functions are at most 33 lines. Matrices have at
+most 12 rows and columns; input helper dimension is at most six. Scientific
+domains and all loop counts are fixed by the enumerations above. Runtime
+checks remain enabled under `-O` and enforce dimensions, unit diagonal,
+invertibility, coefficient bounds and exact residuals. Warnings are errors
+in both registered commands. The only filesystem reads in the scientific
+replay generate the six-file receipt, each bounded to one MiB.
+
+Power-of-Ten rule 3 has a managed-runtime deviation in `verify.py`. Python
+integers, lists and Fractions allocate during arithmetic. The scope is the
+fixed finite replay only. The compensating controls are bounded dimensions,
+fixed coefficient grids, streamed cases, no retained case history and the
+receipt size limit. Normal and optimized replays check the same domains.
+An embedded implementation would need fixed-capacity integer storage and
+a separate bit-capacity analysis; this verifier is not such an implementation.
diff --git a/research/chronological-helper-repair/SOURCES.json b/research/chronological-helper-repair/SOURCES.json
new file mode 100644
index 0000000000..9b0d8dde0a
--- /dev/null
+++ b/research/chronological-helper-repair/SOURCES.json
@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/p104-helper-subspace-splits/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "ca979984444a431b02b62da7094a3b23d5341742",
+      "sha256": "f4c68acf9373e34d88e14e1a7791b4b739c8b5297a1ae4c0121f579a02fde04e"
+    },
+    {
+      "path": "research/dyadic-helper-channel-capacity/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "c97a6edce3070414c81f0ef6e6c099ebb17f3a90",
+      "sha256": "b258a217f2cd0fc48461285fe8ae24de26b0c5963668d9d8f0955fc6e759e929"
+    },
+    {
+      "path": "docs/research/current-priorities.md",
+      "usage": "provenance",
+      "git_blob": "6f5d40d13d8f3bdc12ce7954c8c3eb4ab1f8be91",
+      "sha256": "70f61c8d140ae6e892f2b8f065bba4eae3e76f7a8f55f632fd4e2f9f34039bdc"
+    }
+  ]
+}
diff --git a/research/chronological-helper-repair/TASK.json b/research/chronological-helper-repair/TASK.json
new file mode 100644
index 0000000000..352a0042e0
--- /dev/null
+++ b/research/chronological-helper-repair/TASK.json
@@ -0,0 +1,92 @@
+{
+  "schema_version": 1,
+  "task_id": "coverage-law-change",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "original_card": {
+    "id": "coverage-law-change",
+    "question": "Can a completed call earn more independent productive target credit without an offsetting paid bill?",
+    "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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "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": "Use #5599 as a completed positive control, then choose one uncovered cut/module beyond an applicable frozen exclusion. Derive independence, saturation and chronological availability rather than counting rational rank alone. Price target credits and all new jobs together, then check compiler and actual caller compatibility. Stop on a nonphysical credit or an unfavorable complete relaxation.",
+    "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": [
+      "target credit",
+      "helper split",
+      "coverage law"
+    ],
+    "existing_checks": [
+      {
+        "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": "Exact chronological helper-replacement leakage ranks and the sharp final-bank repair tariff for a full helper basis.",
+  "scope_change_reason": "Replace the single-cut premise by multiple fixed cuts in a scalar identity helper block; isolate a causal obstruction and repair lower bound before any physical construction.",
+  "bottleneck_link": "Current helper-target splitting requires independent inputs and outputs at actual causal cuts. Individual unit pairings alone omit chronological spill and any paid repair it requires.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first all-field scoped result with direct finite corroboration; do not search actual P104 words or extend the construction.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves the causal map, both leakage ranks, the sharp rank(U) repair tariff when L=0, and an arbitrary-size sharp family. verify.py replays all input coefficients, checks leakage ranks and attaining repairs, and rejects invalid and semantically incorrect controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can eligible cuts of a named changed P104 word realize zero lower and nonzero upper pairing?",
+      "why_it_matters": "Determines whether the obstruction or repair tariff applies to a proposed target split.",
+      "first_step": "Extract transported cut rows and columns and every physical eligibility condition.",
+      "blocked_by": "No actual cut family or partial-basis reduction is constructed here."
+    },
+    {
+      "question": "Can an actual consumer pay for all early-output reads and basis operations with a favorable complete signed moment?",
+      "why_it_matters": "A scalar repair tariff is not a native supplier invoice.",
+      "first_step": "Factor the actual upper pairing and price its complete physical delivery and restoration.",
+      "blocked_by": "Early-output availability, common charts, native alignment, precision, compiler and complete invoice."
+    }
+  ],
+  "claim_type": "scoped proof with exact finite corroboration",
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228439",
+  "upstream_checkpoint": {
+    "commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+    "priority_revision": 8,
+    "checked_at": "2026-10-27T22:03:56.100819+00:00"
+  },
+  "environment": {
+    "python": "CPython 3.12.15",
+    "os": "macOS 27.0.1",
+    "architecture": "arm64",
+    "dependencies": "standard library only"
+  }
+}
diff --git a/research/chronological-helper-repair/VERIFY.json b/research/chronological-helper-repair/VERIFY.json
new file mode 100644
index 0000000000..8d8d1c1f35
--- /dev/null
+++ b/research/chronological-helper-repair/VERIFY.json
@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Direct complete cut-event replay versus the causal formula, exact leakage ranks, minimal rank-factor repairs, sharp-family and rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Repeat every mathematical and rejection check with assertions disabled."
+    }
+  ]
+}
diff --git a/research/chronological-helper-repair/verify.py b/research/chronological-helper-repair/verify.py
new file mode 100644
index 0000000000..20a949530b
--- /dev/null
+++ b/research/chronological-helper-repair/verify.py
@@ -0,0 +1,291 @@
+#!/usr/bin/env python3
+"""Exact finite corroboration; the all-field proof is in PROOF.md.
+
+Produced by Nick Petalas. Apache-2.0.
+"""
+from fractions import Fraction
+from hashlib import sha256
+from itertools import product
+import json
+from pathlib import Path
+
+MAX_DIM = 6
+MAX_SIDE = 2 * MAX_DIM
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def scalar(value, prime):
+    return Fraction(value) if prime == 0 else value % prime
+
+
+def identity(size):
+    require(1 <= size <= MAX_SIDE, "identity size")
+    return [[int(i == j) for j in range(size)] for i in range(size)]
+
+
+def transpose(matrix):
+    return [list(row) for row in zip(*matrix, strict=True)]
+
+
+def multiply(left, right, prime):
+    require(1 <= len(left) <= MAX_SIDE, "left size")
+    require(len(left[0]) == len(right), "product shape")
+    require(1 <= len(right[0]) <= MAX_SIDE, "right size")
+    columns = transpose(right)
+    return [[scalar(sum(x * y for x, y in zip(row, col, strict=True)), prime)
+             for col in columns] for row in left]
+
+
+def combine(left, right, prime, sign=1):
+    require(len(left) == len(right), "sum shape")
+    return [[scalar(x + sign * y, prime) for x, y in zip(a, b, strict=True)]
+            for a, b in zip(left, right, strict=True)]
+
+
+def rref(matrix, prime):
+    require(1 <= len(matrix) <= MAX_SIDE, "row count")
+    width = len(matrix[0])
+    require(1 <= width <= MAX_SIDE, "column count")
+    require(all(len(row) == width for row in matrix), "ragged matrix")
+    result = [[scalar(x, prime) for x in row] for row in matrix]
+    pivots = []
+    for col in range(width):
+        choices = [i for i in range(len(pivots), len(result)) if result[i][col]]
+        if not choices:
+            continue
+        pivot = len(pivots)
+        other = choices[0]
+        result[pivot], result[other] = result[other], result[pivot]
+        value = result[pivot][col]
+        reciprocal = 1 / value if prime == 0 else pow(value, -1, prime)
+        result[pivot] = [scalar(x * reciprocal, prime) for x in result[pivot]]
+        for row in range(len(result)):
+            if row != pivot:
+                value = result[row][col]
+                result[row] = [scalar(x - value * y, prime) for x, y in
+                               zip(result[row], result[pivot], strict=True)]
+        pivots.append(col)
+        if len(pivots) == len(result):
+            break
+    return result, pivots
+
+
+def rank(matrix, prime):
+    _, pivots = rref(matrix, prime)
+    return len(pivots)
+
+
+def inverse(matrix, prime):
+    size = len(matrix)
+    require(size <= MAX_DIM and all(len(row) == size for row in matrix), "inverse shape")
+    augmented = [row + unit for row, unit in zip(matrix, identity(size), strict=True)]
+    reduced, pivots = rref(augmented, prime)
+    require(pivots == list(range(size)), "singular matrix")
+    result = [row[size:] for row in reduced]
+    require(multiply(matrix, result, prime) == identity(size), "inverse residual")
+    return result
+
+
+def validate_case(c, k, prime):
+    require(prime in (0, 2, 3, 5, 7), "field")
+    size = len(c)
+    require(1 <= size <= MAX_DIM and len(k) == size, "case size")
+    require(all(len(row) == size for row in c + k), "case shape")
+    require(all(type(x) in (int, Fraction) for row in c + k for x in row), "coefficient type")
+    require(all(abs(Fraction(x).numerator).bit_length() <= 32 and
+                Fraction(x).denominator.bit_length() <= 32 for row in c + k for x in row),
+            "coefficient bound")
+    require(prime == 0 or all(type(x) is int for row in c + k for x in row),
+            "finite-field coefficients")
+    require(all(scalar(k[i][i], prime) == 1 for i in range(size)), "unit diagonal")
+    return inverse(c, prime)
+
+
+def direct_replay(c, d, prime):
+    """Execute changing live charts and literal extract/replace events."""
+    size = len(c)
+    state = [row + [0] * size for row in identity(size)]
+    prefix = identity(size)
+    early = []
+    for cut in range(size):
+        segment = identity(size)
+        if size > 1:
+            segment[cut][(cut + 1) % size] = cut + 1
+        prefix = multiply(segment, prefix, prime)
+        state = multiply(segment, state, prime)
+        a = multiply([c[cut]], inverse(prefix, prime), prime)
+        b = multiply(prefix, [[row[cut]] for row in d], prime)
+        require(multiply(a, b, prime) == [[1]], "literal cut normalization")
+        returned = multiply(a, state, prime)[0]
+        incoming = [int(j == size + cut) for j in range(2 * size)]
+        delta = [scalar(x - y, prime) for x, y in zip(incoming, returned, strict=True)]
+        for row in range(size):
+            state[row] = [scalar(x + b[row][0] * y, prime)
+                          for x, y in zip(state[row], delta, strict=True)]
+        early.append(returned)
+    return early, multiply(inverse(prefix, prime), state, prime)
+
+
+def rank_one_factors(matrix, prime):
+    """Return a minimal outer-product decomposition, with a residual check."""
+    _, columns = rref(matrix, prime)
+    if not columns:
+        return []
+    basis = [[row[j] for j in columns] for row in matrix]
+    _, rows = rref(transpose(basis), prime)
+    minor = [basis[i] for i in rows]
+    weights = multiply(inverse(minor, prime), [matrix[i] for i in rows], prime)
+    factors = list(zip(transpose(basis), weights, strict=True))
+    reconstructed = [[0] * len(matrix) for _ in matrix]
+    for column, row in factors:
+        term = [[scalar(x * y, prime) for y in row] for x in column]
+        reconstructed = combine(reconstructed, term, prime)
+    require(reconstructed == matrix, "rank factorization residual")
+    return factors
+
+
+def check_case(c, k, prime):
+    cinv = validate_case(c, k, prime)
+    size = len(c)
+    lower = [[scalar(k[i][j], prime) if j < i else 0
+              for j in range(size)] for i in range(size)]
+    upper = [[scalar(k[i][j], prime) if i < j else 0
+              for j in range(size)] for i in range(size)]
+    d = multiply(cinv, k, prime)
+    early, final = direct_replay(c, d, prime)
+    a = inverse(combine(identity(size), lower, prime), prime)
+    expected_early = multiply(a, [x + y for x, y in zip(c, lower, strict=True)], prime)
+    incoming = [[0] * size + row for row in identity(size)]
+    expected_final = multiply(cinv, combine(
+        multiply(combine(identity(size), upper, prime), incoming, prime),
+        multiply(upper, early, prime), prime, -1), prime)
+    require(early == expected_early and final == expected_final, "causal formula")
+    require(rank([row[size:] for row in early], prime) == rank(lower, prime),
+            "early new-input rank")
+    require(rank([row[:size] for row in final], prime) == rank(upper, prime),
+            "final old-input rank")
+    require(rank(early + final, prime) == 2 * size, "complete reversible endpoint")
+    if rank(lower, prime) == 0:
+        require(early == [row + [0] * size for row in c], "independent early targets")
+        factors = rank_one_factors(upper, prime)
+        for column, row in factors:
+            delivered = multiply([row], early, prime)[0]
+            vector = multiply(cinv, [[x] for x in column], prime)
+            correction = [[scalar(x[0] * y, prime) for y in delivered] for x in vector]
+            final = combine(final, correction, prime)
+        normalizer = multiply(inverse(combine(identity(size), upper, prime), prime), c, prime)
+        require(multiply(normalizer, final, prime) == incoming, "attaining repair")
+        require(len(factors) == rank(upper, prime), "repair rank units")
+    return int(rank(lower, prime) == 0)
+
+
+def unit_diagonal_cases(size, prime):
+    positions = [(i, j) for i in range(size) for j in range(size) if i != j]
+    for values in product(range(prime), repeat=len(positions)):
+        matrix = identity(size)
+        for (i, j), value in zip(positions, values, strict=True):
+            matrix[i][j] = value
+        yield matrix
+
+
+def finite_checks():
+    counts = {"binary_basis_pairings": 0, "ternary_pairings": 0,
+              "quinary_pairings": 0, "independent_early_repairs": 0}
+    for entries in product(range(2), repeat=9):
+        c = [list(entries[3 * i:3 * i + 3]) for i in range(3)]
+        if rank(c, 2) != 3:
+            continue
+        for k in unit_diagonal_cases(3, 2):
+            counts["independent_early_repairs"] += check_case(c, k, 2)
+            counts["binary_basis_pairings"] += 1
+    for prime, size, label in ((3, 3, "ternary_pairings"), (5, 2, "quinary_pairings")):
+        for k in unit_diagonal_cases(size, prime):
+            counts["independent_early_repairs"] += check_case(identity(size), k, prime)
+            counts[label] += 1
+    return counts
+
+
+def rational_checks():
+    cases = repairs = 0
+    for size in range(1, MAX_DIM + 1):
+        c = identity(size)
+        for i in range(size - 1):
+            c[i][i + 1] = Fraction(i + 1, 2)
+        for seed in range(12):
+            k = [[Fraction(1) if i == j else Fraction(
+                ((i + 2) * (j + 3) + seed) % 7 - 3, 2 ** (seed % 3))
+                  for j in range(size)] for i in range(size)]
+            if seed % 2 == 0:
+                k = [[0 if j < i else x for j, x in enumerate(row)]
+                     for i, row in enumerate(k)]
+            repairs += check_case(c, k, 0)
+            cases += 1
+    return {"rational_cases": cases, "rational_repairs": repairs}
+
+
+def sharp_family_checks():
+    cases = 0
+    for prime in (0, 2, 3, 5, 7):
+        for size in range(2, MAX_DIM + 1):
+            k = identity(size)
+            for i in range(size - 1):
+                k[i][i + 1] = 1
+            require(check_case(identity(size), k, prime) == 1, "sharp family")
+            _, final = direct_replay(identity(size), k, prime)
+            require(rank([row[:size] for row in final], prime) == size - 1,
+                    "sharp spill k-1")
+            cases += 1
+    target = [[0, 1, 0], [0, 0, 1], [0, 0, 0]]
+    rejected = 0
+    for v in product(range(2), repeat=3):
+        for w in product(range(2), repeat=3):
+            require([[x * y for y in w] for x in v] != target, "one-unit false repair")
+            rejected += 1
+    return {"sharp_family_cases": cases, "rank_one_repairs_rejected": rejected}
+
+
+def rejection_checks():
+    invalid = [([], [], 0), ([[1]], [[0]], 0), ([[0]], [[1]], 0),
+               ([[1]], [[1]], 4), ([[1, 0]], [[1]], 0),
+               ([[1]], [[1], [1]], 0), ([[1]], [[Fraction(1)]], 2),
+               ([[1]], [[2 ** 40]], 0)]
+    for c, k, prime in invalid:
+        try:
+            validate_case(c, k, prime)
+        except ValueError:
+            continue
+        raise ValueError("invalid fixture accepted")
+    c = identity(3)
+    k = [[1, 2, 0], [3, 1, 1], [1, 4, 1]]
+    early, final = direct_replay(c, k, 0)
+    old_only = [row + [0] * 3 for row in c]
+    incoming = [[0] * 3 + row for row in c]
+    require(early != old_only, "lower spill control")
+    require(final != incoming, "upper spill control")
+    reversed_early, reversed_final = direct_replay(c, transpose(k), 0)
+    require(early != reversed_early and final != reversed_final, "time order control")
+    require(direct_replay(c, c, 0) == (old_only, incoming), "biorthogonal control")
+    return {"invalid_cases_rejected": len(invalid), "semantic_controls": 4}
+
+
+def main():
+    counts = {}
+    for report in (finite_checks(), rational_checks(), sharp_family_checks(), rejection_checks()):
+        counts.update(report)
+    package = Path(__file__).resolve().parent
+    names = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py")
+    hashes = {}
+    for name in names:
+        path = package / name
+        require(path.stat().st_size <= 1024 * 1024, "receipt file size")
+        hashes[name] = sha256(path.read_bytes()).hexdigest()
+    print("PASS_CHRONOLOGICAL_HELPER_REPAIR " + json.dumps(counts, sort_keys=True))
+    print(json.dumps({"schema": "chronological-helper-repair/v1", "sha256": hashes}, sort_keys=True))
+
+
+if __name__ == "__main__":
+    main()