ReBaseGuard

Stopping-selected recursive re-baselining in repeated sequential monitoring.

Research status: LEVEL-4-CLOSED · 16/16 mandatory requirements passed

“Level 4” is an internally frozen research-program closure criterion, not an external academic certification. The terminal ledger contains 17 PASS, 1 PARTIAL, 0 FAIL, and 0 OPEN; the sole partial item, L4R-13, is nonmandatory. See the final closure report and mechanical decision.

Why this problem exists

A repeated monitoring system can feed its own stopping decision into its next cycle:

If observations that participated in an alarm are reused to estimate the next reference, neither the reused window nor its terminal observation is an ordinary sample: both were selected by the stopping rule. The updated reference then changes the distribution and stopping behavior of the next cycle. ReBaseGuard isolates this feedback mechanism rather than treating it as generic drift detection.

Core result

Let (e) be the current reference error, (m) the reuse-window length, (\rho) the reuse fraction, and (F_{\rho,m}(e)) the deterministic conditional mean of the next reference error. Under the frozen Track-1B random-window convention,

[ F'_{\rho,m}(0)=\rho\left(1-\widetilde{\Gamma}_m\right). ]

For the frozen Gaussian CUSUM with (m=1), Lean checks the stopped-likelihood differentiation spine and outward-rounded Arb arithmetic independently certifies (\Gamma_{\mathrm{CUSUM}}\in[3.9243482,27.8493821]). The human theorem bridge therefore makes zero locally linearly repelling at full reuse. This is a local result for the deterministic conditional-mean map, not a claim of global instability of the monitoring process.

Main findings

• The frozen CUSUM stopped-selection derivative identity is supported by a human theorem and a Lean-checked differentiation spine.
• Arb certifies (\Gamma_{\mathrm{CUSUM}}>2), establishing local repulsion at zero for the full-reuse deterministic map.
• A separate rigorous numerical certificate establishes a locally attracting period-two orbit of the deterministic conditional-mean skeleton; it does not establish period-two behavior for the noisy stochastic chain.
• The random-window (m>1) theorem includes the exact short-cycle correction and yields a protocol-specific (m)-(\rho) local-stability boundary.
• The symmetric two-chart SR derivative theorem is closed. Its (\Gamma_{\mathrm{SR}}>2) result is confirmatory numerical evidence; the corresponding rigorous Arb certificate remains open.
• The derivative form extends to regular common-support location families under explicit analytic hypotheses; L4R-13 non-Gaussian robustness remains nonmandatory partial.
• A frozen stability-aware P3 policy passed its primary scoped criteria, while historical failures and unfavorable P2 comparisons remain part of the record.
• Semi-real tasks support the scoped package in three tasks against two required, while a pre-specified study found no corresponding operational transition at the mathematical crossing under the frozen protocol.

The main theorem architecture and dependency graph separate these conclusions and their assumptions.

Evidence map

Result	Evidence	Authoritative entry point
CUSUM derivative spine	Human theorem + Lean-checked	Lean verification
(\Gamma_{\mathrm{CUSUM}}>2)	Arb-certified	Arb certificate report
Period-two skeleton	Rigorous numerical certificate	Stage-B report
Random-window (m>1) derivative	Human theorem + conditional Lean-checked spine	Track-1B theorem
D4 (m)-(\rho) boundary	Theorem consequence + confirmatory numerical	D4 report
SR derivative	Human theorem + conditional Lean-checked spine	SR report
(\Gamma_{\mathrm{SR}}>2)	Confirmatory numerical; Arb certificate open	SR precision attempt
Location-family derivative	Human theorem + conditional Lean-checked spine	Location-family theorem
External validation	Semi-real empirical	Cross-campaign aggregation
Operational crossing	Negative result	L4R-12 report

Evidence labels are descriptive rather than cumulative. See the evidence hierarchy for exactly what each layer does and does not establish.

Stability-aware reuse policy

The frozen P3 method uses 80% of the simultaneous lower-95% D4 boundary, clipped at one:

[ \rho_{\mathrm{P3}}(m)=\min\left(1,;0.8,\rho_{c,L95}(m)\right). ]

At (m=1,20,70,100), P3 uses reuse fractions (0.053642), (0.245418), (0.781994), and (1). In active regimes it improved the frozen reference-MSE and false-alert-burden contrasts against P1. At (m=100), P3 saturates at P1; P2 retains descriptive advantages at (m=70) and (m=100), and two secondary (\epsilon=0.05) conditions fail. The result is scoped to the frozen policy protocol.

External validation

The external-validation package retains every semi-real/public sequential task without pooling samples: Stage E is 0/3, V2 is 1/3, and V3 is 2/2. That is three supporting tasks against two required. Unsuccessful tasks remain visible, and P2 safety is regime-dependent. These results are not production deployment evidence.

Negative result

The D4 mathematical local-stability boundary brackets the full-reuse crossing at (m\in[70,72]). Under the frozen Stage-D protocol, 0/4 preselected operational metrics peaked at the crossing and 4/4 were monotone in (\log m). The study therefore detected no corresponding operational transition. This conclusion is limited to the frozen Gaussian CUSUM protocol, grid, shifts, and monitored metrics.

Reproduce

From a normal Git clone on a Unix-like system with Bash, Python 3, Git, the repository’s Python environments, Lean/Lake, and FLINT/Arb available as documented, run the authoritative offline terminal reproducer:

bash level4/final_level4_closure/reproduce.sh

It verifies protected hashes, frozen decisions, the requirement ledger, adversarial claim checks, and recorded reproduction state without starting new science. Useful component checks are:

bash scripts/verify_level_4.sh
python3 docs/research_synthesis/verify_synthesis.py --no-diff-check
level4/.venv/bin/python scripts/generate_final_figures.py

Figure hashes and exact evidence paths are recorded in figures/final/README.md.

Repository map

Topic	Entry point
Terminal closure	level4/final_level4_closure/
Reviewer synthesis	docs/research_synthesis/
Complete evidence routing	REPOSITORY_MAP.md
Lean formalization	rebaseguard-lean/
Arb CUSUM certificate	rebaseguard-proof/proofs/certificate.json
Random-window (m>1) theorem	m_gt_1_track1b/
D4 local-stability map	d4_phase_map/
SR theorem and evidence boundary	sr_derivative/
Location-family theorem	location_family_track3ab/
P3 policy	l4r06_policy/
External validation	external_validation_v3/
Novelty audit	novelty_verification/
Final figures	figures/final/

Limitations

• L4R-13, the stronger non-Gaussian robustness requirement, remains PARTIAL and nonmandatory.
• The rigorous SR local-instability Arb certificate remains OPEN; (\Gamma_{\mathrm{SR}}>2) is numerical evidence only.
• The D4 boundary is a deterministic local-stability map, not an operational phase-transition theorem.
• Empirical policy safety is regime-dependent; the project does not establish a universally safe or universally optimal reuse rule.
• Semi-real tasks do not establish production readiness.
• Within the documented N2 search scope, no identified work combines the same alarm-stopped next-reference mechanism with the reported derivative and stability results. This is a scoped literature-audit position, not a priority claim or exhaustive search.

See limitations and open items for the full boundary.

Citation

No paper DOI or release DOI is assigned. Cite the repository by its title, release tag rebaseguard-level4-closed, resolved commit, repository URL, and access date. A CITATION.cff is intentionally not supplied because complete author metadata is not established in repository-authoritative records.

License

No explicit license is currently included. Copyright defaults therefore apply; do not assume permission to reuse, modify, or redistribute beyond applicable law.