Formalize recurrent and dynamic corrective resilience in JAM/ELVES

[albertjanvanhoek]

Summary

This PR extends the correlated-honest-failure JAM/ELVES analysis from an event-level audit model into a two-timescale resilience model.

The central distinction is now:

• within-audit corrective reproduction: lambda_x = F(1-gamma)(1-f_x);
• cross-audit maintenance reproduction: whether the capacities supporting independent correction remain above replacement;
• finite-horizon corrective resilience: whether those slow dynamics keep future lambda_x,t above the audit threshold.

Result 4 — correction reproduction is not maintenance reproduction

formalization/JamRecurrentMaintenance.lean machine-checks:

• the declared C -> O -> R -> C maintenance replacement inequality;
• a witness where current correction is supercritical but slow maintenance is subcritical;
• a witness where slow maintenance is viable but fault-specific current correction is subcritical;
• both non-implications;
• all four cells of the resulting two-threshold phase structure.

The maintenance threshold is explicitly orthogonal to the existing 1/3 < 1/2 < 2/3 event-level sequence.

Result 5 — dynamic corrective resilience

formalization/JamResilienceDynamics.lean couples the slow corrective-capacity state back to the next audit:

C_(t+1) = r_C C_t + k_RC R_t

with lambda_t = F C_t, yielding the exact bridge

lambda_(t+1) = r_C lambda_t + F k_RC R_t.

At current criticality lambda_t = 1, Lean proves

lambda_(t+1) >= 1 <-> F k_RC R_t >= 1-r_C.

The reduced model additionally proves that every finite initial reproduction number eventually becomes subcritical for 0 <= m < 1, and supplies a matched-current-state counterexample: the same current lambda_0 = 3/2 can imply opposite five-step threshold status under different cross-audit maintenance multipliers.

Full-state persistence theorem

formalization/JamMaintenancePersistence.lean removes the remaining gap between the static maintenance threshold and the time-indexed audit result.

For the canonical slow state

• C* = (1-r_O)(1-r_R)
• O* = k_CO(1-r_R)
• R* = k_CO k_OR

it proves:

1. the exact canonical three-cycle replacement condition
   (1-r_C)(1-r_O)(1-r_R) <= k_CO k_OR k_RC;
2. under nonnegative coefficients, the coordinatewise cone above (C*,O*,R*) is forward invariant;
3. if F C* > 1, then the canonical maintenance trajectory remains fast-audit-supercritical at every future cross-audit time;
4. deleting the immediate R -> C return edge with r_C < 1 makes positive corrective capacity decline in the next slow update.

This gives both sides of the resilience question: an explicit erosion mechanism and an explicit invariant region of persistent correction.

Literature / novelty boundary

The paper now positions the result against several adjacent literatures rather than claiming the underlying mathematics:

• classical coincident-failure / multiversion-software work;
• software aging, rejuvenation and environmental diversity;
• proactive Byzantine recovery and reconfiguration, where recovery must prevent faults from accumulating beyond a tolerated bound;
• blockchain incentive-compliance and participation/decentralization dynamics;
• client-diversity measurement and diversity-aware rewards.

The narrower proposed contribution is different in the object being maintained. Proactive BFT maintains enough nonfaulty replicas relative to a fault bound. This JAM/ELVES extension instead tracks the fault-specific independently corrective capacity entering a sampled-audit reproduction number, including honest validators sharing a common implementation fault, and makes preservation of that capacity endogenous through maintenance observability/attribution and resource return.

The contribution is therefore the composition of:

• fault-specific sampled-audit corrective reproduction;
• correlated honest failure;
• a separately maintained corrective-capacity state;
• an exact maintenance-return boundary;
• a full-state invariant region preserving future audit supercriticality; and
• counterexamples showing why present audit success alone does not identify future corrective resilience.

No novelty is claimed for positive-systems, Perron–Frobenius/reproduction-number, proactive-recovery, or geometric-decay mathematics themselves.

Scope

The slow-state variables and coefficients are declared model parameters, not claimed Gray Paper variables or calibrated JAM estimates. The full-state theorem is a conditional forward-invariance theorem, not a convergence or global-stability theorem. External review by the ELVES/JAM authors and empirical grounding on a testnet/deployment remain necessary before interpreting the maintenance-return margin as a measured JAM quantity.