ReBaseGuard studies how repeated monitoring changes when observations selected by an alarm stopping time are reused to update the next reference state.
Drift monitoring is often repeated: a system raises an alarm, updates its reference, and starts monitoring again. If that update reuses observations that helped trigger the alarm, the reference data were selected through a data-dependent stopping event rather than sampled afresh. ReBaseGuard studies the recursive feedback created by this reuse. It develops mathematical descriptions of the resulting reference dynamics, with rigorous local instability results for frozen CUSUM and symmetric two-chart Shiryaev-Roberts settings. It also evaluates a stability-aware reuse policy on simulated and semi-real streams. The policy receives scoped support in the tested regimes, while a pre-specified operational-transition hypothesis produces a negative result. The project keeps theorem, formal proof, certified numerics, empirical evidence, and limitations distinct.
The cycle is monitor -> alarm at a data-dependent stopping time -> reuse alarm-participating observations -> update the next reference -> monitor again. Because the alarm selected the reused observations, they need not behave like fresh reference data; the resulting update then changes later monitoring cycles.
Strongest rigorous core. For the frozen two-sided Gaussian CUSUM with (m=1,\rho=1,k=1/2,h=5), a human theorem connects the reference-map derivative to the stopped gain; Lean kernel-checks the differentiation and moment spine; and an independent outward-rounded Arb certificate proves (\Gamma_{\mathrm{CUSUM}}>2). Together—not Lean or Arb alone—these establish that zero is locally repelling for the deterministic conditional-mean map.
| Result | Evidence type | Current status |
|---|---|---|
| CUSUM stopped-selection derivative | Human bridge + Lean-checked spine | Proved for the frozen model |
| (\Gamma_{\mathrm{CUSUM}}>2) | Arb interval certificate | Certified |
| Symmetric two-chart SR local instability | Human/conditional Lean spine + separate Arb certificate | SR-GAMMA-CERTIFIED |
| Deterministic period-two skeleton | Human theorem + rigorous numerical certificate | Certified within the stated interval |
| Finite-window (m>1) derivative | Human theorem + conditional Lean spine | Closed for the Track-1B convention |
| Stability-aware P3 policy | Frozen numerical + semi-real evidence | Scoped empirical support |
| Operational crossing hypothesis | Frozen operational evaluation | Negative result under the tested protocol |
For reuse fraction (\rho), reference error (e), and stopped gain (\Gamma), the frozen (m=1) derivative is
[ F'_\rho(0)=\rho(1-\Gamma). ]
Arb certifies (\Gamma_{\mathrm{CUSUM}}\in[3.9243482,27.8493821]). The later, separate symmetric two-chart SR upgrade certifies (\Gamma_{\mathrm{SR}}\in[5.800391799508442,28.781285803081492]), whose lower endpoint exceeds two by (3.800391799508442). These are local deterministic results, not global or operational instability theorems for noisy chains.
| Evidence layer | What it checks | Status | Entry point |
|---|---|---|---|
| Human mathematics | Model bridge, assumptions, and theorem interpretation | Proved within stated scope | Theorem map |
| Numerical correspondence | Frozen simulations and consistency checks | Confirmatory, not proof | Evidence hierarchy |
| Lean | Stopped-likelihood derivative and moment proof spine | Kernel-checked | Lean audit guide |
| Arb | Outward-rounded gain enclosures | Certified | CUSUM certificate |
Lean does not certify either numerical interval; Arb does not prove differentiation under the expectation. The human theorem supplies the bridge.
(cd rebaseguard-lean && lake build)
(cd rebaseguard-proof && .venv/bin/python -m rebaseguard_certify.audit proofs/certificate.json)The first command checks the primary Lean library. The second replays the CUSUM
certificate. For frozen release snapshots, use the separate
terminal closure snapshot and
SR-GAMMA-CERTIFIED
instructions. Current presentation checks are:
python3 scripts/verify_academic_presentation.py --no-diff-check
python3 docs/research_synthesis/verify_synthesis.py --no-diff-check| Reader question | Entry point |
|---|---|
| What exactly does Lean verify? | Lean audit guide |
| What is the complete scientific narrative? | Research synthesis |
| Where are theorem dependencies and evidence boundaries? | Theorem architecture and evidence hierarchy |
| Where is the short academic overview? | Four-page Research Brief |
| Where are frozen artifacts by topic? | Reviewer-first repository map |
| What wording and limitations are authoritative? | Claim catalog and limitations register |
- Historical Stage-D D2.3 and Track 1A remain failed. The later Track 1B theorem is a separate result under its own random-window convention.
- L4R-13 non-Gaussian robustness remains
PARTIALand nonmandatory. - Results concern frozen CUSUM and one symmetric two-chart SR model; they are neither detector-independent nor distribution-free.
- Deterministic local multipliers do not establish stochastic invariant laws or an operational phase transition. Under the frozen crossing study, 0/4 metrics peaked at the crossing and 4/4 were monotone in (\log m).
- Policy and semi-real evidence are regime-scoped, not production validation; the novelty position is scoped to the documented search.
LEVEL-4-CLOSED is an internal project-closure designation: 17 PASS, 1
PARTIAL, 0 FAIL, 0 OPEN, with 16/16 satisfied mandatory requirements. It is
not an external academic standard, certification, endorsement, or peer-review
result. At the original Level-4 closure, the optional SR Arb certificate
remained open and was closed later as SR-GAMMA-CERTIFIED; future work is
limited to new scoped extensions such as the remaining non-Gaussian question.
Jingzhe Su (苏靖哲) · School of Information and Software Engineering · University of Electronic Science and Technology of China · suzhea0226@gmail.com
Use CITATION.cff and the relevant immutable release tag when citing a snapshot. Citation is scholarly practice, not a condition of the Apache License 2.0. No institutional endorsement is implied.
Original ReBaseGuard software, formalizations, proof and certificate implementations, documentation, and figures are licensed under the Apache License 2.0 only to the extent owned by the licensor. Third-party dependencies, datasets, bibliographic records, and source-derived portions retain their respective terms and are excluded from that grant. See THIRD_PARTY_NOTICES.md for the audited boundaries.