diff --git a/.github/workflows/build-jam-researcher-brief.yml b/.github/workflows/build-jam-researcher-brief.yml new file mode 100644 index 0000000..ce4b8b5 --- /dev/null +++ b/.github/workflows/build-jam-researcher-brief.yml @@ -0,0 +1,58 @@ +name: Build JAM researcher brief PDF + +on: + push: + paths: + - "docs/JAM_RESEARCHER_BRIEF.tex" + - ".github/workflows/build-jam-researcher-brief.yml" + workflow_dispatch: + +permissions: + contents: write + +concurrency: + group: jam-researcher-brief-${{ github.ref }} + cancel-in-progress: true + +jobs: + build-pdf: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v7 + with: + ref: ${{ github.ref_name }} + fetch-depth: 0 + + - name: Install LaTeX + run: | + sudo apt-get update + sudo apt-get install -y --no-install-recommends \ + latexmk \ + lmodern \ + texlive-latex-base \ + texlive-latex-recommended \ + texlive-latex-extra \ + texlive-fonts-recommended \ + texlive-pictures + + - name: Compile researcher brief + run: | + mkdir -p build/jam-researcher-brief + latexmk -pdf -interaction=nonstopmode -halt-on-error \ + -output-directory=build/jam-researcher-brief \ + docs/JAM_RESEARCHER_BRIEF.tex + cp build/jam-researcher-brief/JAM_RESEARCHER_BRIEF.pdf \ + docs/JAM_RESEARCHER_BRIEF.pdf + + - name: Commit generated PDF when changed + run: | + if git ls-files --error-unmatch docs/JAM_RESEARCHER_BRIEF.pdf >/dev/null 2>&1 \ + && git diff --quiet -- docs/JAM_RESEARCHER_BRIEF.pdf; then + echo "Generated PDF is unchanged." + exit 0 + fi + git config user.name "github-actions[bot]" + git config user.email "41898282+github-actions[bot]@users.noreply.github.com" + git add docs/JAM_RESEARCHER_BRIEF.pdf + git commit -m "Regenerate JAM researcher brief PDF" + git push origin HEAD:${{ github.ref_name }} diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d82c120..d01c6e7 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -5,16 +5,24 @@ on: branches: - main pull_request: + paths-ignore: + - "docs/JAM_RESEARCHER_BRIEF.pdf" permissions: contents: read +# Keep only the newest run for a PR/ref. Rapid proof-development commits were +# otherwise leaving several expensive Lean/mathlib jobs running in parallel. +concurrency: + group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: true + jobs: python: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v4 - - uses: actions/setup-python@v5 + - uses: actions/checkout@v7 + - uses: actions/setup-python@v7 with: python-version: "3.12" - name: Install package @@ -55,18 +63,15 @@ jobs: lean: runs-on: ubuntu-latest - defaults: - run: - working-directory: formalization steps: - - uses: actions/checkout@v4 - - name: Install elan - run: | - curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y - echo "$HOME/.elan/bin" >> "$GITHUB_PATH" - - name: Update dependencies - run: $HOME/.elan/bin/lake update - - name: Fetch Mathlib cache - run: $HOME/.elan/bin/lake exe cache get - - name: Compile proofs - run: $HOME/.elan/bin/lake build + - uses: actions/checkout@v7 + - name: Build Lean formalization + uses: leanprover/lean-action@v1 + with: + lake-package-directory: formalization + auto-config: false + build: true + test: false + lint: false + use-mathlib-cache: true + use-github-cache: true diff --git a/docs/JAM_RESEARCHER_BRIEF.pdf b/docs/JAM_RESEARCHER_BRIEF.pdf new file mode 100644 index 0000000..9e0a10b Binary files /dev/null and b/docs/JAM_RESEARCHER_BRIEF.pdf differ diff --git a/docs/JAM_RESEARCHER_BRIEF.tex b/docs/JAM_RESEARCHER_BRIEF.tex new file mode 100644 index 0000000..035d1f4 --- /dev/null +++ b/docs/JAM_RESEARCHER_BRIEF.tex @@ -0,0 +1,183 @@ +% Source for the committed researcher-brief PDF. +\documentclass[10pt,a4paper]{article} + +\usepackage[margin=16mm]{geometry} +\usepackage[T1]{fontenc} +\usepackage[utf8]{inputenc} +\usepackage{lmodern} +\usepackage{microtype} +\usepackage{amsmath,amssymb} +\usepackage{booktabs} +\usepackage{enumitem} +\usepackage{xcolor} +\usepackage{tikz} +\usetikzlibrary{arrows.meta,positioning,fit} +\usepackage[colorlinks=true,linkcolor=black,urlcolor=blue!55!black,citecolor=black]{hyperref} +\usepackage{parskip} +\usepackage{titlesec} + +\definecolor{ink}{HTML}{17202A} +\definecolor{muted}{HTML}{5D6D7E} +\definecolor{accent}{HTML}{185FA5} +\definecolor{pale}{HTML}{EEF5FB} +\definecolor{warn}{HTML}{FFF7E6} +\definecolor{line}{HTML}{CCD6E0} + +\color{ink} +\setlength{\parindent}{0pt} +\setlength{\parskip}{4.5pt} +\setlist[itemize]{leftmargin=4.5mm,itemsep=1.5pt,topsep=2pt} +\setlist[enumerate]{leftmargin=5.5mm,itemsep=2pt,topsep=2pt} +\titleformat{\section}{\large\bfseries\color{accent}}{}{0pt}{} +\titlespacing*{\section}{0pt}{8pt}{3pt} +\titleformat{\subsection}{\normalsize\bfseries}{}{0pt}{} +\titlespacing*{\subsection}{0pt}{6pt}{2pt} + +\newcommand{\callout}[2]{% + \noindent\fcolorbox{line}{#1}{% + \begin{minipage}{0.955\linewidth} + #2 + \end{minipage}} +} + +\begin{document} +\pagestyle{empty} + +{\small\bfseries\color{accent} JAM RESEARCHER BRIEF}\par +\vspace{2pt} +{\LARGE\bfseries Does JAM maintain its capacity to correct shared implementation faults?}\par +\vspace{4pt} +{\small\color{muted} A narrow question for expert review of the JAM/ELVES security model. The aim is not to propose a replacement protocol model, but to test whether a residual failure mode has been identified or whether JAM already closes it elsewhere.}\par +\vspace{5pt} +\hrule + +\section{The question} + +Fix one invalid report and one fault family $x$. Some validators may be adversarial. A second group may be honest in the ordinary sense but share an implementation fault that makes this particular invalid report look valid. A third group independently detects the fault. + +\callout{pale}{\textbf{Core distinction.} Validator honesty and implementation independence are different security resources. A validator can be honest yet fail to provide independent corrective capacity for a particular fault family.} + +Let $A$ be adversarial validators, $B_x$ otherwise-honest validators sharing fault $x$, and $C_x$ validators that independently judge the report invalid, with $N=A+B_x+C_x$. + +At the Gray-Paper verdict layer, the relevant arithmetic can be stated directly: if $K=\lfloor 2N/3\rfloor+1$, then independently correct negative judgments can construct a bad verdict against adversarial positive voting exactly when $C_x\ge K$ in the declared fault partition. + +For the ELVES-style escalation model, let $F$ be the tranche/escalation factor, $\gamma=A/N$, and $f_x=B_x/(N-A)$. Replacing the generic honest share by the fault-specific independently correct share gives the declared reproduction mean +\[ +\boxed{\lambda_x=F\frac{C_x}{N}=F(1-\gamma)(1-f_x),\qquad \lambda_x>1\ \text{supercritical}.} +\] +This substitution is a model extension, not a theorem attributed to the original ELVES analysis. + +\subsection{A minimal counterexample} + +Take the same validator count, the same adversarial share $\gamma=0.20$, and the same illustrative escalation factor $F=2$. + +\begin{center} +\small +\begin{tabular}{@{}lccc@{}} +\toprule + & shared-fault share $f_x$ & independently correct share & $\lambda_x$ \\ +\midrule +Population 1 & $0.10$ & $0.80\times0.90=0.72$ & $1.44$ \\ +Population 2 & $0.50$ & $0.80\times0.50=0.40$ & $0.80$ \\ +\bottomrule +\end{tabular} +\end{center} + +Both populations are 80\% non-adversarial. Under this declared audit model, one is above the independent-correction threshold and the other below it. Ordinary validator counts and honest fractions therefore do not determine fault-specific corrective capacity. + +\begin{center} +\begin{tikzpicture}[ + node distance=6mm and 11mm, + box/.style={draw=line,rounded corners=2pt,fill=white,inner sep=5pt,align=center,font=\small}, + good/.style={box,fill=pale}, + bad/.style={box,fill=warn}, + arr/.style={-{Latex[length=2.2mm]},draw=muted,thick} +] +\node[box] (same) {same current validator count\\same adversarial share}; +\node[good,below left=of same] (ind) {low correlated exposure\\large $C_x$}; +\node[bad,below right=of same] (corr) {shared fault $x$\\small $C_x$}; +\node[good,below=of ind] (sup) {$\lambda_x>1$\\correction reproduces}; +\node[bad,below=of corr] (sub) {$\lambda_x<1$\\correction can die out}; +\draw[arr] (same) -- (ind); +\draw[arr] (same) -- (corr); +\draw[arr] (ind) -- (sup); +\draw[arr] (corr) -- (sub); +\end{tikzpicture} +\end{center} + +\section{The second question: what maintains correction over time?} + +Even if $\lambda_x>1$ today, the ecosystem can lose the independent implementations, operators, effort, observability, or resources that supplied that margin. We therefore introduced the smallest explicit slow-state model we could use to separate \emph{current correction} from \emph{maintenance of future correction}. + +Let $C_t$ denote normalized independently corrective capacity, $O_t$ maintenance observability/attribution, and $R_t$ returned-resource capacity. The declared slow loop is $C\rightarrow O\rightarrow R\rightarrow C$. Coupling the next slow update back to the audit layer gives +\[ +\boxed{\lambda_{x,t+1}=r_C\lambda_{x,t}+F k_{RC}R_t.} +\] +At current criticality, $\lambda_{x,t}=1$, Lean verifies the exact one-step boundary +\[ +\boxed{\lambda_{x,t+1}\ge1\quad\Longleftrightarrow\quad Fk_{RC}R_t\ge1-r_C.} +\] +Interpretation: return into corrective capacity must at least replace its attrition if a critical system is not to cross below the threshold on the next slow update. + +\newpage + +{\small\bfseries\color{accent} JAM RESEARCHER BRIEF \hfill PAGE 2}\par +\vspace{3pt}\hrule + +\section{Why a snapshot is not enough} + +The distinction does not depend on accepting the full three-variable maintenance model. In the reduced path $\lambda_t=m^t\lambda_0$, two systems can start at the same current value $\lambda_0=3/2$ but have opposite five-step status: with $m=1$ the value remains $3/2$; with $m=0.9$ it falls to approximately $0.886$. + +\callout{pale}{\centering\textbf{Present agreement $\neq$ present corrective capacity $\neq$ maintained corrective capacity $\neq$ future corrective resilience.}} + +The full-state Lean result goes one step further. For the declared $C\rightarrow O\rightarrow R\rightarrow C$ dynamics, it identifies a canonical replacement condition and proves a coordinatewise forward-invariant region in which fast audit correction stays supercritical at every future cross-audit time. It also proves the complementary erosion mechanism: remove the immediate $R\rightarrow C$ return edge while $r_C<1$, and positive corrective capacity declines at the next slow update. + +\section{What is proved, and what is not claimed} + +\begin{minipage}[t]{0.48\linewidth} +\textbf{Machine-checked in Lean} +\begin{itemize} + \item separation of current audit correction from slow maintenance viability; + \item witnesses for all four cells of the two-threshold phase structure; + \item the one-step bridge from slow state to next-audit reproduction; + \item eventual erosion in the reduced model when $0\le m<1$; + \item the full-state forward-invariance persistence theorem; + \item decline after deleting the immediate resource-return edge. +\end{itemize} +\end{minipage}\hfill +\begin{minipage}[t]{0.48\linewidth} +\textbf{Deliberately not claimed} +\begin{itemize} + \item that $C_t,O_t,R_t$ are Gray-Paper state variables; + \item that the coefficients are calibrated JAM quantities; + \item that positive-systems, branching, or geometric-decay mathematics is novel; + \item that the full slow system globally converges; + \item that current JAM deployments have any particular correlated-fault rate. +\end{itemize} +\end{minipage} + +\section{Three questions for JAM/ELVES reviewers} + +\begin{enumerate} +\item \textbf{Coverage.} Is correlated honest implementation failure already covered by a JAM/ELVES assumption, verdict rule, sampling mechanism, or recovery mechanism that this analysis has missed? +\item \textbf{Security object.} If not, is \emph{fault-specific independently corrective capacity} a meaningful quantity for reasoning about JAM execution auditing, or is there a better protocol-native object? +\item \textbf{Measurement.} If the distinction is meaningful, which observable testnet/deployment quantities would best estimate whether independent corrective capacity persists across audits---client/fault-family exposure, independent re-execution effort, operator diversity, attribution, resource flows, or something else? +\end{enumerate} + +\callout{warn}{\textbf{The requested expert judgment is intentionally narrow:} are we modelling a real residual failure mode of JAM, or has the protocol already closed this loop somewhere we have missed? If the latter, identifying that mechanism would directly falsify or substantially narrow the JAM-specific interpretation.} + +\section{Where to inspect the full argument} + +The maintained source of truth is the \href{https://github.com/albertjanvanhoek/Distributed-Commons-Control/tree/main}{\texttt{main} branch of Distributed-Commons-Control}. The most relevant entry points are: +\begin{itemize} + \item \href{https://github.com/albertjanvanhoek/Distributed-Commons-Control/tree/main/papers/correlated-honest-failure}{\texttt{papers/correlated-honest-failure/}} --- manuscript and claim ledger; + \item \href{https://github.com/albertjanvanhoek/Distributed-Commons-Control/blob/main/formalization/JamRecurrentMaintenance.lean}{\texttt{formalization/JamRecurrentMaintenance.lean}}; + \item \href{https://github.com/albertjanvanhoek/Distributed-Commons-Control/blob/main/formalization/JamResilienceDynamics.lean}{\texttt{formalization/JamResilienceDynamics.lean}}; + \item \href{https://github.com/albertjanvanhoek/Distributed-Commons-Control/blob/main/formalization/JamMaintenancePersistence.lean}{\texttt{formalization/JamMaintenancePersistence.lean}}. +\end{itemize} +The complete development history for this integration remains available in \href{https://github.com/albertjanvanhoek/Distributed-Commons-Control/pull/22}{PR \#22}. + +\vfill +{\footnotesize\color{muted} Researcher brief, September 2026. This document is an interface to the formal work, not an additional layer of claims. The declared model is intentionally small so that protocol experts can reject, replace, or operationalize its assumptions.} + +\end{document} diff --git a/docs/RECURRENT_CORRECTIVE_CAPACITY.md b/docs/RECURRENT_CORRECTIVE_CAPACITY.md new file mode 100644 index 0000000..364133c --- /dev/null +++ b/docs/RECURRENT_CORRECTIVE_CAPACITY.md @@ -0,0 +1,160 @@ +# Recurrent corrective capacity in JAM/ELVES + +## Purpose + +The JAM/ELVES analysis now distinguishes three questions: + +1. **Within-audit corrective reproduction**: does independently correct checking reproduce during the current dispute process? +2. **Cross-audit maintenance reproduction**: does the surrounding architecture preserve the capacities required to remain independently corrective? +3. **Finite-horizon corrective resilience**: can current supercritical correction persist under the measured replenishment and attrition dynamics? + +These are not the same condition. + +## Event-level condition + +Under the correlated-honest-failure extension, + +\[ +\lambda_x = F(1-\gamma)(1-f_x). +\] + +The current audit is supercritical for independently correct checking when + +\[ +\lambda_x>1. +\] + +## Slow maintenance condition + +Introduce a declared slow three-process loop: + +- `C`: independently corrective capacity; +- `O`: observability/attribution of genuine maintenance; +- `R`: resources returned to preserve future corrective capacity. + +The canonical directed loop is + +\[ +C\rightarrow O\rightarrow R\rightarrow C. +\] + +With retention factors `r_C,r_O,r_R` and coupling gains `k_CO,k_OR,k_RC`, the declared replacement condition is + +\[ +k_{CO}k_{OR}k_{RC}\ge(1-r_C)(1-r_O)(1-r_R). +\] + +This is a model extension. The coefficients are not claimed to be current Gray Paper state variables. The underlying product/spectral threshold structure is classical; the research contribution is the explicit separation of this condition from the ELVES event-level correction threshold. + +## Machine-checked separation + +`formalization/JamRecurrentMaintenance.lean` proves explicit witnesses for all four cells: + +| Current correction | Slow maintenance | Interpretation | +|---|---|---| +| supercritical | viable | current correction works and modeled corrective capacity is maintained | +| supercritical | subcritical | correctable now, modeled capacity erodes across time | +| subcritical | viable | ecosystem persists but is insufficiently independently corrective for fault `x` | +| subcritical | subcritical | neither condition holds | + +The two key non-implications are therefore machine checked: + +\[ +\lambda_x>1\not\Rightarrow \text{maintenance viability}, +\] + +and + +\[ +\text{maintenance viability}\not\Rightarrow\lambda_x>1. +\] + +## Dynamic bridge to the next audit + +`formalization/JamResilienceDynamics.lean` adds an explicit slow state + +\[ +X_t=(C_t,O_t,R_t) +\] + +with update + +\[ +C_{t+1}=r_CC_t+k_{RC}R_t, +\] +\[ +O_{t+1}=r_OO_t+k_{CO}C_t, +\] +\[ +R_{t+1}=r_RR_t+k_{OR}O_t. +\] + +The fast audit reproduction supplied by this state is + +\[ +\lambda_{x,t}=FC_t. +\] + +Hence + +\[ +\lambda_{x,t+1}=r_C\lambda_{x,t}+Fk_{RC}R_t. +\] + +At current criticality, `lambda_x,t = 1`, Lean verifies the exact maintenance-return boundary + +\[ +\boxed{\lambda_{x,t+1}\ge1\iff Fk_{RC}R_t\ge1-r_C.} +\] + +This motivates the local return margin + +\[ +M_t=Fk_{RC}R_t-(1-r_C). +\] + +- `M_t < 0`: a currently critical system crosses below the audit threshold on the next slow update; +- `M_t = 0`: replacement exactly closes the local corrective-capacity gap; +- `M_t > 0`: a currently critical system moves above the audit threshold. + +This is a one-step boundary, not a general stability theorem for the full slow system. + +## Why current audit success is not enough + +For a reduced effective cross-audit multiplier `m`, define + +\[ +\lambda_t=m^t\lambda_0. +\] + +The correction margin `mu_t=lambda_t-1` obeys + +\[ +\mu_{t+1}=m\mu_t-(1-m). +\] + +A machine-checked counterexample starts two systems at the same current value `lambda_0=3/2`: + +- with `m=1`, the system is still at `3/2` after five steps; +- with `m=9/10`, it is below one after five steps. + +Thus a snapshot of current `lambda_x` does not identify finite-horizon resilience in the declared dynamic model. The reduced multiplier is a diagnostic abstraction, not a calibrated JAM parameter and not the same object as the three-process loop ratio. + +## Empirical grounding needed next + +A protocol-facing resilience assessment would need measurable proxies for: + +- the current fault-specific independently corrective share `C_x,t`; +- rates at which independent implementations/operators enter, exit, converge, or become correlated; +- real audit effort versus nominal participation; +- observability/attribution of useful independent maintenance; +- economic and development resources returned to independently corrective implementations/operators; +- the time scale on which those returns affect future corrective capacity; +- the current maintenance-return margin and its uncertainty; +- horizon forecasts under plausible ranges rather than a single point estimate. + +Client identity or diversity proofs can help make part of this state observable, but observability alone does not establish that the return loop closes. The operational target is stronger: estimate whether the processes that produce independent correction are themselves above replacement before the current audit margin is exhausted. + +A concrete testnet/deployment question is therefore: + +> Can JAM estimate both the current fault-specific audit reproduction margin and a separate cross-audit maintenance-return margin, and detect a projected threshold crossing before event-level correction becomes subcritical? diff --git a/formalization/JamMaintenancePersistence.lean b/formalization/JamMaintenancePersistence.lean new file mode 100644 index 0000000..20e801c --- /dev/null +++ b/formalization/JamMaintenancePersistence.lean @@ -0,0 +1,218 @@ +import JamResilienceDynamics + +namespace DistributedCommons + +/-! +# JAM: persistent corrective resilience from a closed maintenance loop + +`JamRecurrentMaintenance.lean` gives the static three-process replacement +threshold, while `JamResilienceDynamics.lean` couples slow corrective capacity +to the fast audit reproduction number. This module closes the remaining gap: +it proves directly on the full C -> O -> R -> C state dynamics that the cone +above a canonical maintenance witness is forward invariant when the closed-loop +product meets replacement. + +Consequently, if the canonical corrective coordinate is already sufficient to +make the fast audit reproduction number supercritical, then every future point +on the canonical slow trajectory remains audit-supercritical. + +The mathematics is the finite directed-three-cycle specialization of standard +positive-systems / reproduction-number reasoning. The JAM-facing contribution +is the explicit bridge from a closed cross-audit maintenance loop to persistent +within-audit corrective reproduction. +-/ + +/-- Canonical corrective coordinate for the C -> O -> R -> C witness. -/ +noncomputable def jamCanonicalCorrective (rO rR : ℝ) : ℝ := + (1 - rO) * (1 - rR) + +/-- Canonical observability coordinate. -/ +noncomputable def jamCanonicalObservability (kCO rR : ℝ) : ℝ := + kCO * (1 - rR) + +/-- Canonical returned-resource coordinate. -/ +noncomputable def jamCanonicalResources (kCO kOR : ℝ) : ℝ := + kCO * kOR + +/-- Canonical state exposing the exact three-cycle maintenance threshold. -/ +noncomputable def jamCanonicalMaintenanceState + (rO rR kCO kOR : ℝ) : JamCorrectiveState := + { corrective := jamCanonicalCorrective rO rR + observability := jamCanonicalObservability kCO rR + resources := jamCanonicalResources kCO kOR } + +/-- Coordinatewise order above the canonical maintenance witness. -/ +def jamAtOrAboveCanonical + (rO rR kCO kOR : ℝ) + (x : JamCorrectiveState) : Prop := + jamCanonicalCorrective rO rR ≤ x.corrective ∧ + jamCanonicalObservability kCO rR ≤ x.observability ∧ + jamCanonicalResources kCO kOR ≤ x.resources + +/-- Exact canonical-state form of the slow replacement threshold. O and R are +exactly replaced at the witness; C is at least replaced iff the cycle-gain +product covers the product of autonomous deficits. -/ +theorem jam_canonical_threshold_iff + (rC rO rR kCO kOR kRC : ℝ) : + let x := jamCanonicalMaintenanceState rO rR kCO kOR + (x.corrective ≤ + (jamCorrectiveStateStep rC rO rR kCO kOR kRC x).corrective ∧ + x.observability = + (jamCorrectiveStateStep rC rO rR kCO kOR kRC x).observability ∧ + x.resources = + (jamCorrectiveStateStep rC rO rR kCO kOR kRC x).resources) + ↔ + (1 - rC) * (1 - rO) * (1 - rR) ≤ kCO * kOR * kRC := by + dsimp [jamCanonicalMaintenanceState, jamCanonicalCorrective, + jamCanonicalObservability, jamCanonicalResources, + jamCorrectiveStateStep] + constructor + · rintro ⟨hC, hO, hR⟩ + nlinarith + · intro h + constructor + · nlinarith + constructor <;> ring + +/-- The cone above the canonical witness is forward invariant for nonnegative +retention/coupling coefficients when the closed maintenance loop meets the +replacement threshold. -/ +theorem jam_step_preserves_canonical_lower_bound + {rC rO rR kCO kOR kRC : ℝ} + (hrC : 0 ≤ rC) (hrO : 0 ≤ rO) (hrR : 0 ≤ rR) + (hkCO : 0 ≤ kCO) (hkOR : 0 ≤ kOR) (hkRC : 0 ≤ kRC) + (hloop : + (1 - rC) * (1 - rO) * (1 - rR) ≤ kCO * kOR * kRC) + {x : JamCorrectiveState} + (hx : jamAtOrAboveCanonical rO rR kCO kOR x) : + jamAtOrAboveCanonical rO rR kCO kOR + (jamCorrectiveStateStep rC rO rR kCO kOR kRC x) := by + rcases hx with ⟨hxC, hxO, hxR⟩ + have hcanon := + (jam_canonical_threshold_iff rC rO rR kCO kOR kRC).2 hloop + change + jamCanonicalCorrective rO rR ≤ + rC * x.corrective + kRC * x.resources ∧ + jamCanonicalObservability kCO rR ≤ + rO * x.observability + kCO * x.corrective ∧ + jamCanonicalResources kCO kOR ≤ + rR * x.resources + kOR * x.observability + constructor + · have hCself := mul_le_mul_of_nonneg_left hxC hrC + have hCreturn := mul_le_mul_of_nonneg_left hxR hkRC + have hmono : + rC * jamCanonicalCorrective rO rR + + kRC * jamCanonicalResources kCO kOR + ≤ rC * x.corrective + kRC * x.resources := by + linarith + exact le_trans hcanon.1 hmono + constructor + · have hOself := mul_le_mul_of_nonneg_left hxO hrO + have hOcross := mul_le_mul_of_nonneg_left hxC hkCO + have hmono : + rO * jamCanonicalObservability kCO rR + + kCO * jamCanonicalCorrective rO rR + ≤ rO * x.observability + kCO * x.corrective := by + linarith + exact le_trans (le_of_eq hcanon.2.1) hmono + · have hRself := mul_le_mul_of_nonneg_left hxR hrR + have hRcross := mul_le_mul_of_nonneg_left hxO hkOR + have hmono : + rR * jamCanonicalResources kCO kOR + + kOR * jamCanonicalObservability kCO rR + ≤ rR * x.resources + kOR * x.observability := by + linarith + exact le_trans (le_of_eq hcanon.2.2) hmono + +/-- Deterministic slow trajectory initialized at the canonical witness. -/ +noncomputable def jamCanonicalMaintenanceTrajectory + (rC rO rR kCO kOR kRC : ℝ) : ℕ → JamCorrectiveState + | 0 => jamCanonicalMaintenanceState rO rR kCO kOR + | n + 1 => + jamCorrectiveStateStep rC rO rR kCO kOR kRC + (jamCanonicalMaintenanceTrajectory rC rO rR kCO kOR kRC n) + +/-- Every point of the canonical trajectory remains at or above the canonical +witness when the slow loop meets replacement. -/ +theorem jam_canonical_trajectory_stays_above_witness + {rC rO rR kCO kOR kRC : ℝ} + (hrC : 0 ≤ rC) (hrO : 0 ≤ rO) (hrR : 0 ≤ rR) + (hkCO : 0 ≤ kCO) (hkOR : 0 ≤ kOR) (hkRC : 0 ≤ kRC) + (hloop : + (1 - rC) * (1 - rO) * (1 - rR) ≤ kCO * kOR * kRC) : + ∀ n : ℕ, + jamAtOrAboveCanonical rO rR kCO kOR + (jamCanonicalMaintenanceTrajectory rC rO rR kCO kOR kRC n) := by + intro n + induction n with + | zero => + exact ⟨le_rfl, le_rfl, le_rfl⟩ + | succ n ih => + change jamAtOrAboveCanonical rO rR kCO kOR + (jamCorrectiveStateStep rC rO rR kCO kOR kRC + (jamCanonicalMaintenanceTrajectory rC rO rR kCO kOR kRC n)) + exact jam_step_preserves_canonical_lower_bound + hrC hrO hrR hkCO hkOR hkRC hloop ih + +/-- **Persistent corrective-resilience theorem.** If the closed slow +maintenance loop meets replacement and the canonical corrective coordinate is +already sufficient for fast audit supercriticality, then every future point on +the canonical slow trajectory remains audit-supercritical. + +This directly links the Result-4 maintenance threshold to the Result-5 fast +audit threshold without introducing the reduced multiplier `m`. -/ +theorem jam_closed_maintenance_loop_preserves_supercritical_correction + {F rC rO rR kCO kOR kRC : ℝ} + (hF : 0 ≤ F) + (hrC : 0 ≤ rC) (hrO : 0 ≤ rO) (hrR : 0 ≤ rR) + (hkCO : 0 ≤ kCO) (hkOR : 0 ≤ kOR) (hkRC : 0 ≤ kRC) + (hloop : + (1 - rC) * (1 - rO) * (1 - rR) ≤ kCO * kOR * kRC) + (hfast : 1 < F * jamCanonicalCorrective rO rR) : + ∀ n : ℕ, + jamStateCorrectionSupercritical F + (jamCanonicalMaintenanceTrajectory rC rO rR kCO kOR kRC n) := by + intro n + have habove := jam_canonical_trajectory_stays_above_witness + hrC hrO hrR hkCO hkOR hkRC hloop n + have hC : + jamCanonicalCorrective rO rR ≤ + (jamCanonicalMaintenanceTrajectory rC rO rR kCO kOR kRC n).corrective := + habove.1 + have hmul : + F * jamCanonicalCorrective rO rR ≤ + F * (jamCanonicalMaintenanceTrajectory rC rO rR kCO kOR kRC n).corrective := + mul_le_mul_of_nonneg_left hC hF + unfold jamStateCorrectionSupercritical jamStateCorrectionReproduction + exact lt_of_lt_of_le hfast hmul + +/-- Under positive O and R deficits and positive C->O and O->R gains, the +canonical corrective coordinate is strictly positive. -/ +theorem jam_canonical_corrective_positive + {rO rR : ℝ} + (hdO : 0 < 1 - rO) + (hdR : 0 < 1 - rR) : + 0 < jamCanonicalCorrective rO rR := by + unfold jamCanonicalCorrective + exact mul_pos hdO hdR + +/-- Deleting the immediate R->C return edge makes any positive corrective +coordinate with subunit autonomous retention strictly decline on the next +cross-audit update. -/ +theorem jam_deleting_return_edge_makes_corrective_capacity_decline + {rC rO rR kCO kOR : ℝ} + {x : JamCorrectiveState} + (hrC : rC < 1) + (hxC : 0 < x.corrective) : + (jamCorrectiveStateStep rC rO rR kCO kOR 0 x).corrective < x.corrective := by + simp [jamCorrectiveStateStep] + nlinarith + +#print axioms jam_canonical_threshold_iff +#print axioms jam_step_preserves_canonical_lower_bound +#print axioms jam_canonical_trajectory_stays_above_witness +#print axioms jam_closed_maintenance_loop_preserves_supercritical_correction +#print axioms jam_canonical_corrective_positive +#print axioms jam_deleting_return_edge_makes_corrective_capacity_decline + +end DistributedCommons diff --git a/formalization/JamRecurrentMaintenance.lean b/formalization/JamRecurrentMaintenance.lean new file mode 100644 index 0000000..c926985 --- /dev/null +++ b/formalization/JamRecurrentMaintenance.lean @@ -0,0 +1,156 @@ +import JamEffortObservability + +namespace DistributedCommons + +/-! +# JAM: corrective reproduction versus recurrent maintenance + +This module separates two timescales that are easy to conflate. + +* `jamFaultCorrectionReproduction` is the within-audit reproduction mean of + independently correct checking under the correlated-honest-failure + extension of ELVES. +* `jamMaintenanceLoopGain` and `jamMaintenanceDeficitProduct` describe a + slower three-process return loop that maintains the capacity to keep doing + useful correction across audits. + +The three slow processes are intentionally abstract: + + C = independently corrective capacity + O = capacity to observe/attribute genuine maintenance + R = resources returned to maintain future corrective capacity + +with the canonical directed loop + + C -> O -> R -> C. + +The product threshold used here is the finite three-cycle replacement +condition. The underlying nonnegative-matrix / reproduction-number mathematics +is classical; the contribution of this module is the explicit separation from +the ELVES event-level correction threshold and the machine-checked independence +witnesses below. +-/ + +/-- Fault-specific within-audit corrective reproduction. -/ +noncomputable def jamFaultCorrectionReproduction + (F gamma f : ℝ) : ℝ := + F * (1 - gamma) * (1 - f) + +/-- Autonomous maintenance deficit of one slow maintenance process. -/ +noncomputable def jamMaintenanceDeficit (r : ℝ) : ℝ := + 1 - r + +/-- Product of the three autonomous maintenance deficits. -/ +noncomputable def jamMaintenanceDeficitProduct + (rC rO rR : ℝ) : ℝ := + jamMaintenanceDeficit rC * + jamMaintenanceDeficit rO * + jamMaintenanceDeficit rR + +/-- Closed-loop gain of the C -> O -> R -> C maintenance cycle. -/ +noncomputable def jamMaintenanceLoopGain + (kCO kOR kRC : ℝ) : ℝ := + kCO * kOR * kRC + +/-- The canonical slow maintenance loop meets replacement when its closed-loop +product covers the product of its autonomous deficits. -/ +def jamMaintenanceViable + (rC rO rR kCO kOR kRC : ℝ) : Prop := + jamMaintenanceDeficitProduct rC rO rR ≤ + jamMaintenanceLoopGain kCO kOR kRC + +/-- Event-level correction is supercritical exactly when its reproduction mean +exceeds one. This is kept as a named predicate so the two timescales can be +combined without identifying them. -/ +def jamCorrectionSupercritical (F gamma f : ℝ) : Prop := + 1 < jamFaultCorrectionReproduction F gamma f + +/-- Exact substitution of the independently-correct share into the ELVES-style +fault-specific reproduction mean. -/ +theorem jamFaultCorrectionReproduction_eq + (F gamma f : ℝ) : + jamFaultCorrectionReproduction F gamma f = + F * (1 - gamma) * (1 - f) := by + rfl + +/-- The slow maintenance threshold depends only on the maintenance-loop +parameters, not on the current ELVES fault-specific reproduction parameters. -/ +theorem jamMaintenanceViable_iff + (rC rO rR kCO kOR kRC : ℝ) : + jamMaintenanceViable rC rO rR kCO kOR kRC ↔ + (1 - rC) * (1 - rO) * (1 - rR) ≤ kCO * kOR * kRC := by + rfl + +/-- Separation witness 1: current correction can be strongly supercritical +while the slow maintenance return loop is subcritical. + +Here the audit reproduction mean is 2, but three zero-retention maintenance +processes coupled by gains 1/2 have loop gain 1/8 against deficit product 1. -/ +theorem correction_supercritical_maintenance_subcritical_witness : + jamCorrectionSupercritical 2 0 0 ∧ + ¬ jamMaintenanceViable 0 0 0 (1 / 2) (1 / 2) (1 / 2) := by + constructor + · norm_num [jamCorrectionSupercritical, jamFaultCorrectionReproduction] + · norm_num [jamMaintenanceViable, jamMaintenanceDeficitProduct, + jamMaintenanceDeficit, jamMaintenanceLoopGain] + +/-- Separation witness 2: a strongly viable slow maintenance loop does not +imply fault-specific correction is supercritical for the current audit. + +Here the slow loop has unit gain against deficit product 1/8, while a fault +shared by 3/4 of otherwise-honest validators leaves the event-level correction +mean at 1/2 for F=2. -/ +theorem maintenance_viable_correction_subcritical_witness : + jamMaintenanceViable (1 / 2) (1 / 2) (1 / 2) 1 1 1 ∧ + ¬ jamCorrectionSupercritical 2 0 (3 / 4) := by + constructor + · norm_num [jamMaintenanceViable, jamMaintenanceDeficitProduct, + jamMaintenanceDeficit, jamMaintenanceLoopGain] + · norm_num [jamCorrectionSupercritical, jamFaultCorrectionReproduction] + +/-- Therefore within-audit corrective reproduction does not logically imply +cross-audit maintenance viability in this declared two-timescale model. -/ +theorem correction_supercritical_does_not_imply_maintenance_viable : + ¬ (∀ F gamma f rC rO rR kCO kOR kRC : ℝ, + jamCorrectionSupercritical F gamma f → + jamMaintenanceViable rC rO rR kCO kOR kRC) := by + intro h + have hbad := h 2 0 0 0 0 0 (1 / 2) (1 / 2) (1 / 2) + correction_supercritical_maintenance_subcritical_witness.1 + exact correction_supercritical_maintenance_subcritical_witness.2 hbad + +/-- Conversely, a viable slow maintenance loop does not logically imply that +independent correction for a particular current fault is supercritical. -/ +theorem maintenance_viable_does_not_imply_correction_supercritical : + ¬ (∀ F gamma f rC rO rR kCO kOR kRC : ℝ, + jamMaintenanceViable rC rO rR kCO kOR kRC → + jamCorrectionSupercritical F gamma f) := by + intro h + have hbad := h 2 0 (3 / 4) (1 / 2) (1 / 2) (1 / 2) 1 1 1 + maintenance_viable_correction_subcritical_witness.1 + exact maintenance_viable_correction_subcritical_witness.2 hbad + +/-- The two predicates therefore generate four logically distinct phase cells; +this witness inhabits the jointly viable cell. -/ +theorem both_reproduction_conditions_can_hold : + jamCorrectionSupercritical 2 0 0 ∧ + jamMaintenanceViable (1 / 2) (1 / 2) (1 / 2) 1 1 1 := by + constructor + · exact correction_supercritical_maintenance_subcritical_witness.1 + · exact maintenance_viable_correction_subcritical_witness.1 + +/-- This witness inhabits the jointly non-viable cell. -/ +theorem neither_reproduction_condition_need_hold : + ¬ jamCorrectionSupercritical 2 0 (3 / 4) ∧ + ¬ jamMaintenanceViable 0 0 0 (1 / 2) (1 / 2) (1 / 2) := by + exact ⟨maintenance_viable_correction_subcritical_witness.2, + correction_supercritical_maintenance_subcritical_witness.2⟩ + +#print axioms correction_supercritical_maintenance_subcritical_witness +#print axioms maintenance_viable_correction_subcritical_witness +#print axioms correction_supercritical_does_not_imply_maintenance_viable +#print axioms maintenance_viable_does_not_imply_correction_supercritical +#print axioms both_reproduction_conditions_can_hold +#print axioms neither_reproduction_condition_need_hold + +end DistributedCommons diff --git a/formalization/JamResilienceDynamics.lean b/formalization/JamResilienceDynamics.lean new file mode 100644 index 0000000..8d18394 --- /dev/null +++ b/formalization/JamResilienceDynamics.lean @@ -0,0 +1,243 @@ +import JamRecurrentMaintenance +import Mathlib.Analysis.SpecificLimits.Basic + +namespace DistributedCommons + +/-! +# JAM: dynamic corrective resilience + +`JamRecurrentMaintenance.lean` separates within-audit corrective reproduction +from cross-audit maintenance viability. This module couples the two timescales. + +The slow state has three coordinates: + +* `corrective` -- the normalized, fault-specific independently-correct share + that feeds the next audit's corrective reproduction number; +* `observability` -- capacity to observe or attribute genuine maintenance; +* `resources` -- resources returned to preserve future corrective capacity. + +The declared linear update is + + C' = rC C + kRC R + O' = rO O + kCO C + R' = rR R + kOR O. + +For a fixed audit escalation factor `F`, the next audit's fast reproduction +number is `F * C`. The main exact bridge proved here is therefore local and +measurable: at the fast critical boundary `F*C = 1`, the next audit remains at +or above criticality exactly when returned resources close the current +corrective-capacity replacement gap. + +A reduced one-parameter path is also used to prove an identification result: +the same current reproduction number can imply different finite-horizon +resilience depending on the cross-audit maintenance multiplier. This is a +model theorem, not a claim that JAM currently has any particular slow-state +coefficients or multiplier. +-/ + +/-- Slow state supporting future independently-correct auditing. `corrective` +is normalized to the validator population relevant to the fast audit model. -/ +structure JamCorrectiveState where + corrective : ℝ + observability : ℝ + resources : ℝ + +/-- One cross-audit update of corrective capacity, maintenance observability, +and returned resources. -/ +def jamCorrectiveStateStep + (rC rO rR kCO kOR kRC : ℝ) + (x : JamCorrectiveState) : JamCorrectiveState := + { corrective := rC * x.corrective + kRC * x.resources + observability := rO * x.observability + kCO * x.corrective + resources := rR * x.resources + kOR * x.observability } + +/-- Fast, fault-specific audit reproduction generated by the current slow +corrective-capacity coordinate. -/ +noncomputable def jamStateCorrectionReproduction + (F : ℝ) (x : JamCorrectiveState) : ℝ := + F * x.corrective + +/-- Fast supercriticality of the current state. -/ +def jamStateCorrectionSupercritical + (F : ℝ) (x : JamCorrectiveState) : Prop := + 1 < jamStateCorrectionReproduction F x + +/-- Exact bridge from the slow state update to the next audit reproduction +number. The observability and resource equations matter for later rounds, but +the immediate next-audit bridge enters through the returned-resource term in +`C'`. -/ +theorem jam_next_reproduction_identity + (F rC rO rR kCO kOR kRC : ℝ) + (x : JamCorrectiveState) : + jamStateCorrectionReproduction F + (jamCorrectiveStateStep rC rO rR kCO kOR kRC x) + = + rC * jamStateCorrectionReproduction F x + + F * kRC * x.resources := by + unfold jamStateCorrectionReproduction jamCorrectiveStateStep + ring + +/-- **Maintenance-return boundary.** If the current fast audit is exactly at +criticality, then the next audit stays at or above criticality iff returned +resources close the autonomous loss of corrective capacity. + +The right-hand side is intentionally written without division, so it remains +meaningful even when `F` or `kRC` is zero. -/ +theorem jam_critical_return_boundary + {F rC rO rR kCO kOR kRC : ℝ} + {x : JamCorrectiveState} + (hcrit : jamStateCorrectionReproduction F x = 1) : + 1 ≤ jamStateCorrectionReproduction F + (jamCorrectiveStateStep rC rO rR kCO kOR kRC x) + ↔ + 1 - rC ≤ F * kRC * x.resources := by + rw [jam_next_reproduction_identity, hcrit] + constructor <;> intro h <;> nlinarith + +/-- At current criticality, a strict shortfall in the returned-resource term +forces the next audit below the fast correction threshold. -/ +theorem jam_return_shortfall_makes_next_audit_subcritical + {F rC rO rR kCO kOR kRC : ℝ} + {x : JamCorrectiveState} + (hcrit : jamStateCorrectionReproduction F x = 1) + (hshort : F * kRC * x.resources < 1 - rC) : + jamStateCorrectionReproduction F + (jamCorrectiveStateStep rC rO rR kCO kOR kRC x) < 1 := by + rw [jam_next_reproduction_identity, hcrit] + nlinarith + +/-- Conversely, a strict returned-resource surplus above the replacement gap +makes the next audit supercritical when the current audit is exactly critical. -/ +theorem jam_return_surplus_makes_next_audit_supercritical + {F rC rO rR kCO kOR kRC : ℝ} + {x : JamCorrectiveState} + (hcrit : jamStateCorrectionReproduction F x = 1) + (hsurplus : 1 - rC < F * kRC * x.resources) : + 1 < jamStateCorrectionReproduction F + (jamCorrectiveStateStep rC rO rR kCO kOR kRC x) := by + rw [jam_next_reproduction_identity, hcrit] + nlinarith + +/-- Reduced cross-audit trajectory for the fast correction reproduction number. +`m` is a net maintenance multiplier for this reduced coordinate; it is not the +same object as the three-process loop ratio from `JamRecurrentMaintenance`. -/ +noncomputable def jamReducedCorrectionPath + (lambda0 m : ℝ) (n : ℕ) : ℝ := + m ^ n * lambda0 + +/-- The reduced path starts at the observed current reproduction number. -/ +theorem jamReducedCorrectionPath_zero + (lambda0 m : ℝ) : + jamReducedCorrectionPath lambda0 m 0 = lambda0 := by + simp [jamReducedCorrectionPath] + +/-- Exact one-step recurrence of the reduced cross-audit path. -/ +theorem jamReducedCorrectionPath_succ + (lambda0 m : ℝ) (n : ℕ) : + jamReducedCorrectionPath lambda0 m (n + 1) + = m * jamReducedCorrectionPath lambda0 m n := by + simp [jamReducedCorrectionPath, pow_succ] + ring + +/-- Margin above the fast ELVES-style critical boundary. -/ +noncomputable def jamCorrectionMargin (lambda : ℝ) : ℝ := + lambda - 1 + +/-- Exact margin recursion. Because the fast threshold remains fixed at one, +a maintenance multiplier below one creates both multiplicative shrinkage of +existing margin and an additive replacement drag. -/ +theorem jamCorrectionMargin_step + (lambda m : ℝ) : + jamCorrectionMargin (m * lambda) + = m * jamCorrectionMargin lambda - (1 - m) := by + unfold jamCorrectionMargin + ring + +/-- Any positive reproduction number strictly declines in one reduced step +when the maintenance multiplier lies below one. -/ +theorem jamReducedCorrection_strictly_declines + {lambda m : ℝ} + (hlambda : 0 < lambda) + (hm : m < 1) : + m * lambda < lambda := by + have hgap : 0 < (1 - m) * lambda := + mul_pos (sub_pos.mpr hm) hlambda + nlinarith + +/-- A nonnegative subunit reduced maintenance multiplier drives every finite +initial reproduction number to zero, hence eventually below the fast critical +threshold. This is the general reduced-model erosion theorem behind the finite +counterexample below. -/ +theorem jamReducedCorrection_eventually_subcritical + {lambda0 m : ℝ} + (hm0 : 0 ≤ m) + (hm1 : m < 1) : + ∀ᶠ n : ℕ in Filter.atTop, + jamReducedCorrectionPath lambda0 m n < 1 := by + have hpow : + Filter.Tendsto (fun n : ℕ => m ^ n) Filter.atTop (nhds 0) := + tendsto_pow_atTop_nhds_zero_of_lt_one hm0 hm1 + have hpath : + Filter.Tendsto + (fun n : ℕ => jamReducedCorrectionPath lambda0 m n) + Filter.atTop (nhds 0) := by + simpa [jamReducedCorrectionPath] using hpow.mul_const lambda0 + exact (tendsto_order.1 hpath).2 1 (by norm_num) + +/-- In particular, some finite cross-audit horizon lies below criticality for +any nonnegative reduced multiplier strictly below one. -/ +theorem jamReducedCorrection_eventually_crosses_threshold + {lambda0 m : ℝ} + (hm0 : 0 ≤ m) + (hm1 : m < 1) : + ∃ n : ℕ, jamReducedCorrectionPath lambda0 m n < 1 := by + exact (jamReducedCorrection_eventually_subcritical hm0 hm1).exists + +/-- Finite-horizon resilience in the reduced path. -/ +def jamHorizonSupercritical + (lambda0 m : ℝ) (T : ℕ) : Prop := + 1 < jamReducedCorrectionPath lambda0 m T + +/-- **Current audit success is not a sufficient statistic for horizon +resilience.** Two systems can have exactly the same current supercritical +reproduction number and different five-step status solely because their +cross-audit maintenance multipliers differ. + +The numbers are a transparent counterexample, not calibrated JAM estimates: +`lambda0 = 3/2`; perfect replacement keeps it at `3/2`, while multiplier +`9/10` yields `(9/10)^5 * (3/2) < 1`. -/ +theorem event_level_success_not_sufficient_statistic_for_five_step_resilience : + ∃ lambda0 mStable mErode : ℝ, + 1 < lambda0 ∧ + jamReducedCorrectionPath lambda0 mStable 0 = + jamReducedCorrectionPath lambda0 mErode 0 ∧ + jamHorizonSupercritical lambda0 mStable 5 ∧ + ¬ jamHorizonSupercritical lambda0 mErode 5 := by + refine ⟨3 / 2, 1, 9 / 10, ?_⟩ + norm_num [jamReducedCorrectionPath, jamHorizonSupercritical] + +/-- Concrete full-state witness of latent loss: current correction is +supercritical, but with no returned-resource contribution and only half of the +corrective coordinate retained, the next audit becomes subcritical. -/ +theorem current_supercritical_can_cross_subcritical_next_round : + let x : JamCorrectiveState := + { corrective := 3 / 4, observability := 1, resources := 1 } + jamStateCorrectionSupercritical 2 x ∧ + ¬ jamStateCorrectionSupercritical 2 + (jamCorrectiveStateStep (1 / 2) 1 1 1 1 0 x) := by + norm_num [jamStateCorrectionSupercritical, jamStateCorrectionReproduction, + jamCorrectiveStateStep] + +#print axioms jam_next_reproduction_identity +#print axioms jam_critical_return_boundary +#print axioms jam_return_shortfall_makes_next_audit_subcritical +#print axioms jam_return_surplus_makes_next_audit_supercritical +#print axioms jamReducedCorrectionPath_succ +#print axioms jamCorrectionMargin_step +#print axioms jamReducedCorrection_strictly_declines +#print axioms jamReducedCorrection_eventually_subcritical +#print axioms jamReducedCorrection_eventually_crosses_threshold +#print axioms event_level_success_not_sufficient_statistic_for_five_step_resilience +#print axioms current_supercritical_can_cross_subcritical_next_round + +end DistributedCommons diff --git a/formalization/README.md b/formalization/README.md index d8d4475..f1e6661 100644 --- a/formalization/README.md +++ b/formalization/README.md @@ -64,6 +64,24 @@ The Lean source checks only the algebraic core of the declared model. It does no | Perfect observability may still be insufficient | `perfect_observability_insufficient` | | More effort observability improves selection | `higher_observability_improves_selection` | | Lower exposure raises observability requirement | `lower_exposure_raises_observability_threshold` | +| Current correction can be supercritical while slow maintenance is subcritical | `correction_supercritical_maintenance_subcritical_witness` | +| Slow maintenance can be viable while fault-specific correction is subcritical | `maintenance_viable_correction_subcritical_witness` | +| Event-level correction does not imply maintenance viability | `correction_supercritical_does_not_imply_maintenance_viable` | +| Maintenance viability does not imply event-level correction | `maintenance_viable_does_not_imply_correction_supercritical` | +| Jointly viable and jointly non-viable phase cells are inhabited | `both_reproduction_conditions_can_hold`; `neither_reproduction_condition_need_hold` | +| Next audit reproduction from slow-state update | `jam_next_reproduction_identity` | +| Exact return boundary at current criticality | `jam_critical_return_boundary` | +| Return shortfall/surplus determines next-step threshold direction | `jam_return_shortfall_makes_next_audit_subcritical`; `jam_return_surplus_makes_next_audit_supercritical` | +| Reduced cross-audit recurrence | `jamReducedCorrectionPath_succ` | +| Exact correction-margin recursion | `jamCorrectionMargin_step` | +| Subunit maintenance multiplier strictly erodes positive reproduction | `jamReducedCorrection_strictly_declines` | +| Subunit nonnegative multiplier eventually becomes subcritical | `jamReducedCorrection_eventually_subcritical`; `jamReducedCorrection_eventually_crosses_threshold` | +| Same current reproduction can imply opposite five-step resilience | `event_level_success_not_sufficient_statistic_for_five_step_resilience` | +| Current supercritical state can cross below threshold next round | `current_supercritical_can_cross_subcritical_next_round` | +| Canonical full-state maintenance threshold | `jam_canonical_threshold_iff` | +| Canonical maintenance cone is forward invariant | `jam_step_preserves_canonical_lower_bound`; `jam_canonical_trajectory_stays_above_witness` | +| Closed maintenance loop preserves fast audit supercriticality | `jam_closed_maintenance_loop_preserves_supercritical_correction` | +| Deleting the return edge makes positive corrective capacity decline | `jam_deleting_return_edge_makes_corrective_capacity_decline` | | Fungal redundant-state stability iff effective gain < 1 | `fungal_stable_iff_effective_gain_lt_one` | | Unit fungal effective gain is neutral | `fungal_neutral_iff_effective_gain_eq_one` | | Superunit fungal effective gain is unstable | `fungal_unstable_iff_effective_gain_gt_one` | @@ -84,12 +102,7 @@ The toolchain and Mathlib commit match the current formalization convention used ## End-to-end real-root proof -`RootSafety.lean` is a default Lake build target. It adds 11 declarations covering -root construction, its power identity, uniqueness, monotonicity, residual bounds, -threshold feasibility, exact target attainment, least sufficient effort and the -selected-safety/critical-cost equivalence. Every declaration prints its axioms. -See `docs/PHASE_BOUNDARY.md` for the exact claim map. No root existence or -leastness hypothesis remains assumed in `selected_safety_iff_critical_cost`. +`RootSafety.lean` is a default Lake build target. It adds 11 declarations covering root construction, its power identity, uniqueness, monotonicity, residual bounds, threshold feasibility, exact target attainment, least sufficient effort and the selected-safety/critical-cost equivalence. Every declaration prints its axioms. See `docs/PHASE_BOUNDARY.md` for the exact claim map. No root existence or leastness hypothesis remains assumed in `selected_safety_iff_critical_cost`. ## Endogenous producer floor @@ -135,6 +148,18 @@ leastness hypothesis remains assumed in `selected_safety_iff_critical_cost`. `JamEffortObservability.lean` formalizes Experiment 11's second-order maintenance channel. It proves that selective reinforcement depends jointly on effort observability and returned reward, and that structural loss of false-positive exposure raises the observability burden needed to select real computation. +## JAM recurrent corrective capacity + +`JamRecurrentMaintenance.lean` adds a second timescale to the JAM analysis. It keeps the ELVES-style fault-specific reproduction mean `lambda_x` separate from a declared slow `C -> O -> R -> C` maintenance loop linking independently corrective capacity, maintenance observability/attribution and returned resources. The file machine-checks explicit witnesses showing that event-level supercritical correction and slow maintenance viability imply neither one another, and it inhabits all four phase cells. The slow-loop coefficients are model parameters rather than claimed Gray Paper variables; no novelty is claimed for the underlying positive-systems/reproduction-number threshold mathematics. + +## JAM dynamic corrective resilience + +`JamResilienceDynamics.lean` couples the slow corrective-capacity coordinate back to the next audit. For the declared state update `C' = r_C C + k_RC R` and `lambda = F C`, it proves the exact identity `lambda' = r_C lambda + F k_RC R`. At current criticality it proves the one-step maintenance-return boundary `lambda' >= 1` iff `F k_RC R >= 1-r_C`, including strict shortfall and surplus corollaries. The reduced cross-audit model proves both a concrete matched-current-state counterexample and the general result that every finite initial reproduction number eventually becomes subcritical when `0 <= m < 1`. These are dynamic model implications, not calibrated JAM forecasts. + +## JAM persistent corrective resilience + +`JamMaintenancePersistence.lean` closes the gap between the static three-process replacement threshold and the time-indexed audit model. It constructs the canonical slow state `C*=(1-r_O)(1-r_R)`, `O*=k_CO(1-r_R)`, `R*=k_CO k_OR`; proves that the cone above this state is forward invariant under nonnegative coefficients when the three-cycle product threshold is met; and then proves that, whenever `F C* > 1`, the canonical trajectory remains fast-audit-supercritical at every future cross-audit time. It also proves one-step corrective-capacity decline when the immediate `R -> C` return edge is deleted and `r_C < 1`. The result is a conditional invariant-region theorem, not a convergence, global-stability, or calibrated long-run JAM theorem. + ## Fungal flow-coupled maintenance `FungalFlowMaintenance.lean` formalizes Experiment 12's two-route local stability boundary. The nonlinear flow-reinforcement rule is a falsification model extension motivated by empirical fungal flow/cord-growth coupling; the file does not claim that this exact power-law is fungal physiology. diff --git a/formalization/lake-manifest.json b/formalization/lake-manifest.json new file mode 100644 index 0000000..3b270b3 --- /dev/null +++ b/formalization/lake-manifest.json @@ -0,0 +1 @@ +{"version":"1.2.0","packagesDir":".lake/packages","packages":[{"url":"https://github.com/leanprover-community/mathlib4.git","type":"git","subDir":null,"scope":"","rev":"db584cd6d46c92f209a44c0f1c829460d327499d","name":"mathlib","manifestFile":"lake-manifest.json","inputRev":"db584cd6d46c92f209a44c0f1c829460d327499d","inherited":false,"configFile":"lakefile.lean"},{"url":"https://github.com/leanprover-community/plausible","type":"git","subDir":null,"scope":"leanprover-community","rev":"b7eb3304aeae834b12dda98993a37f6a41f6f0bb","name":"plausible","manifestFile":"lake-manifest.json","inputRev":"main","inherited":true,"configFile":"lakefile.toml"},{"url":"https://github.com/leanprover-community/LeanSearchClient","type":"git","subDir":null,"scope":"leanprover-community","rev":"5f4d51b81cbd3f6b32b156bfad9056621a040404","name":"LeanSearchClient","manifestFile":"lake-manifest.json","inputRev":"main","inherited":true,"configFile":"lakefile.toml"},{"url":"https://github.com/leanprover-community/import-graph","type":"git","subDir":null,"scope":"leanprover-community","rev":"16f02aa7642864af59f1ff0e384a015994db9118","name":"importGraph","manifestFile":"lake-manifest.json","inputRev":"main","inherited":true,"configFile":"lakefile.toml"},{"url":"https://github.com/leanprover-community/ProofWidgets4","type":"git","subDir":null,"scope":"leanprover-community","rev":"4be2e3d5087eeb272cf5a8853b8f9dd025ef5957","name":"proofwidgets","manifestFile":"lake-manifest.json","inputRev":"main","inherited":true,"configFile":"lakefile.lean"},{"url":"https://github.com/leanprover-community/aesop","type":"git","subDir":null,"scope":"leanprover-community","rev":"3448c0bcc5ce01b2d1546e483ec3620e32df3d0e","name":"aesop","manifestFile":"lake-manifest.json","inputRev":"master","inherited":true,"configFile":"lakefile.toml"},{"url":"https://github.com/leanprover-community/quote4","type":"git","subDir":null,"scope":"leanprover-community","rev":"92c15be17b7caf78c2ad767ec40f89052d908d81","name":"Qq","manifestFile":"lake-manifest.json","inputRev":"master","inherited":true,"configFile":"lakefile.toml"},{"url":"https://github.com/leanprover-community/batteries","type":"git","subDir":null,"scope":"leanprover-community","rev":"4488d40d070b9700d4d5a6aa342f0d40c31b2a2d","name":"batteries","manifestFile":"lake-manifest.json","inputRev":"main","inherited":true,"configFile":"lakefile.toml"},{"url":"https://github.com/leanprover/lean4-cli","type":"git","subDir":null,"scope":"leanprover","rev":"6130a47896ce867c6a4a55373441e59e565bad0f","name":"Cli","manifestFile":"lake-manifest.json","inputRev":"v4.33.0","inherited":true,"configFile":"lakefile.toml"}],"name":"distributed_commons_control","lakeDir":".lake","fixedToolchain":false} diff --git a/formalization/lakefile.toml b/formalization/lakefile.toml index b7b98e9..796c2ed 100644 --- a/formalization/lakefile.toml +++ b/formalization/lakefile.toml @@ -1,6 +1,6 @@ name = "distributed_commons_control" version = "0.1.0" -defaultTargets = ["DistributedCommons", "RootSafety", "DynamicSafety", "EndogenousFloor", "ClosedLoopStability", "ViabilityContribution", "SelectedViability", "CorrectiveCapacity", "StateDependentContribution", "VectorContribution", "BehavioralMaintenance", "JamMaintenance", "JamBehaviorSelection", "JamEffortObservability", "FungalFlowMaintenance", "ViabilityOught"] +defaultTargets = ["DistributedCommons", "RootSafety", "DynamicSafety", "EndogenousFloor", "ClosedLoopStability", "ViabilityContribution", "SelectedViability", "CorrectiveCapacity", "StateDependentContribution", "VectorContribution", "BehavioralMaintenance", "JamMaintenance", "JamBehaviorSelection", "JamEffortObservability", "JamRecurrentMaintenance", "JamResilienceDynamics", "JamMaintenancePersistence", "FungalFlowMaintenance", "ViabilityOught"] [[require]] name = "mathlib" @@ -49,6 +49,15 @@ name = "JamBehaviorSelection" [[lean_lib]] name = "JamEffortObservability" +[[lean_lib]] +name = "JamRecurrentMaintenance" + +[[lean_lib]] +name = "JamResilienceDynamics" + +[[lean_lib]] +name = "JamMaintenancePersistence" + [[lean_lib]] name = "FungalFlowMaintenance" diff --git a/papers/correlated-honest-failure/CLAIMS.md b/papers/correlated-honest-failure/CLAIMS.md index dbfaa88..9137219 100644 --- a/papers/correlated-honest-failure/CLAIMS.md +++ b/papers/correlated-honest-failure/CLAIMS.md @@ -16,6 +16,21 @@ | D1 | Slashable collateral need not equal attacker-attributable collateral when honest buggy guarantors sign the invalid report. | Economic mapping observation | Does not prove attacker has zero cost. | | D2 | Wonky has no ordinary Gray Paper culprit/fault offender record. | Gray Paper rule interpretation | Staking layer may add consequences; requires author confirmation. | | D3 | Guarantor diversity, announcement monitoring, effort proofs and load-feedback controls are design hypotheses. | Future work | No protocol recommendation is claimed. | +| E1 | The slow three-process model `C -> O -> R -> C` meets its canonical replacement condition when `k_CO k_OR k_RC >= (1-r_C)(1-r_O)(1-r_R)`. | Declared maintenance-loop model; algebraic threshold | The variables and couplings are not claimed to be current Gray Paper state variables. General product/spectral threshold mathematics is prior art. | +| E2 | Event-level supercritical correction (`lambda_x > 1`) does not imply slow maintenance viability. | Machine-checked separation witness | Witness uses `F=2, gamma=f=0` and a subcritical slow loop. | +| E3 | Slow maintenance viability does not imply event-level supercritical correction for a particular fault. | Machine-checked separation witness | Witness uses a strong slow loop but `f=3/4`, giving `lambda_x=1/2` at `F=2, gamma=0`. | +| E4 | All four cells of the two-threshold phase structure are jointly inhabitable in the declared model. | Machine-checked witnesses | This is logical/model non-equivalence, not an empirical statement about JAM deployment. | +| E5 | A system can therefore be correctable in the current audit while the modeled capacity supporting future correction is below replacement, or operationally persistent while fault-specific correction is subcritical. | Interpretation of E2–E4 | Requires empirical/protocol mapping before any claim about actual JAM long-run dynamics. | +| F1 | Under the declared state update `C' = r_C C + k_RC R` and fast coupling `lambda = F C`, next reproduction satisfies `lambda' = r_C lambda + F k_RC R`. | Machine-checked exact identity | `C`, `R`, and their update coefficients are declared slow-state variables, not Gray Paper variables. | +| F2 | At current criticality `lambda=1`, next reproduction is at least critical iff `F k_RC R >= 1-r_C`. | Machine-checked exact equivalence | Local one-step maintenance-return boundary; not a general stability theorem for the full three-dimensional loop. | +| F3 | At current criticality, strict return shortfall makes the next audit subcritical; strict return surplus makes it supercritical. | Machine-checked corollaries of F2 | Same declared state model. | +| F4 | In the reduced path `lambda_t=m^t lambda_0`, the correction margin obeys `mu_{t+1}=m mu_t-(1-m)`. | Machine-checked identity | `m` is a reduced net cross-audit multiplier and is not identified with the three-process loop ratio `R_M`. | +| F5 | The same current supercritical reproduction number can correspond to different finite-horizon threshold status: with `lambda_0=3/2`, `m=1` remains supercritical at step 5 whereas `m=9/10` is subcritical. | Machine-checked counterexample | Numerical witness demonstrates non-identifiability; it is not a calibrated JAM forecast. | +| F6 | Current `lambda_x` is therefore not a sufficient statistic for finite-horizon corrective resilience in the declared dynamic model. | Interpretation of F4–F5 | Forecasting actual JAM resilience requires empirical identification of slow-state dynamics. | +| F7 | For the full three-state dynamics, the canonical witness `C*=(1-r_O)(1-r_R)`, `O*=k_CO(1-r_R)`, `R*=k_CO k_OR` is componentwise nondecreasing after one update iff the three-cycle product threshold is met, with `O*` and `R*` exactly at replacement. | Machine-checked exact finite-cycle theorem | Finite three-cycle result; no novelty claim for general positive-systems or Perron–Frobenius theory. | +| F8 | Under nonnegative retention and coupling coefficients and the product threshold, the coordinatewise cone above the canonical witness is forward invariant. | Machine-checked dynamic theorem | Applies to the declared linear slow-state model. It is not a global stability or convergence theorem. | +| F9 | If the canonical corrective coordinate already satisfies `F C* > 1`, then every point of the canonical maintenance trajectory remains audit-supercritical for all future cross-audit times. | Machine-checked persistent-resilience theorem | Conditional on the declared slow dynamics, nonnegative coefficients and canonical initial state. | +| F10 | Deleting the immediate `R -> C` return edge with `r_C<1` makes any positive corrective coordinate decline in the next slow update. | Machine-checked return-edge theorem | One-step erosion result; later system behavior may depend on other mechanisms not represented here. | ## Explicit non-claims @@ -25,4 +40,11 @@ The paper does not claim: - that the attacker can freely choose a favorable core assignment; - that a wonky verdict is economically cost-free in a production staking layer; - that client count equals fault-domain diversity; -- that F=2 is incorrectly chosen without a complete re-optimization under the revised threat model. +- that F=2 is incorrectly chosen without a complete re-optimization under the revised threat model; +- that the Gray Paper already specifies numerical coefficients for the slow `C -> O -> R -> C` maintenance loop; +- that `lambda_x > 1` guarantees preservation of corrective capacity across future audits; +- that persistence of a validator/economic ecosystem guarantees independent correction for every correlated fault; +- that the reduced multiplier `m=9/10` or any other numerical slow-dynamics parameter is an estimate for JAM; +- that a single current observation of `lambda_x` is sufficient to estimate a future failure probability; +- that the full three-state forward-invariance result establishes convergence, global stability, or calibrated long-run JAM behavior; +- novelty for the underlying positive-systems, spectral-radius, reproduction-number, software-rejuvenation, or geometric-decay mathematics used in the declared slow models. diff --git a/papers/correlated-honest-failure/README.md b/papers/correlated-honest-failure/README.md index a6c3fb4..4732d48 100644 --- a/papers/correlated-honest-failure/README.md +++ b/papers/correlated-honest-failure/README.md @@ -7,6 +7,42 @@ Repo-ready LaTeX package for the technical companion paper. 1. **Verdict attribution boundary** from the current Gray Paper rules. 2. **Fault-specific ELVES escalation** under correlated honest failure. 3. **Sampling dilution** showing that honest-but-correlated validator additions can lower corrective reproduction. +4. **Recurrent corrective capacity** separating within-audit corrective reproduction from cross-audit maintenance of the capacity required to remain corrective. +5. **Dynamic corrective resilience** coupling slow corrective capacity back to the next audit and proving both erosion and a full-state persistence region. + +Result 4 introduces a declared slow `C -> O -> R -> C` loop linking independently corrective capacity, observability/attribution of genuine maintenance, and resources returned to preserve future corrective capacity. Machine-checked witnesses show that the event-level condition `lambda_x > 1` and the slow maintenance replacement condition imply neither one another. The maintenance threshold is therefore an orthogonal timescale, not a fourth nested point on the verdict/audit threshold sequence. + +Result 5 adds a slow state update and the bridge `lambda_x,t = F C_t`. At current criticality, Lean verifies the exact one-step condition + +\[ +\lambda_{x,t+1}\ge1 +\iff +F k_{RC}R_t\ge1-r_C. +\] + +The reduced model proves that any finite initial correction reproduction eventually becomes subcritical when `0 <= m < 1`, and gives two systems with identical current `lambda_0 = 3/2` but opposite five-step threshold status under different maintenance multipliers. + +The full three-state formalization then closes the positive side. For + +\[ +C^*=(1-r_O)(1-r_R),\qquad +O^*=k_{CO}(1-r_R),\qquad +R^*=k_{CO}k_{OR}, +\] + +the exact product condition + +\[ +(1-r_C)(1-r_O)(1-r_R)\le k_{CO}k_{OR}k_{RC} +\] + +makes the coordinatewise cone above `(C*,O*,R*)` forward invariant under nonnegative coefficients. If `F C* > 1`, the canonical trajectory therefore remains audit-supercritical at every future cross-audit time. The model thus contains both a formal erosion mechanism and a formal persistence region. + +## Literature boundary + +The paper does **not** claim novelty for the general idea that resilience must be replenished over time. Proactive Byzantine recovery and reconfiguration already maintain enough nonfaulty replicas so accumulated faults do not exceed a tolerated bound. Nor does the paper claim novelty for client diversity, diversity-aware rewards, positive-systems thresholds, or geometric decay. + +The narrower proposed contribution is different in the object being maintained: **fault-specific independently corrective capacity inside a sampled audit process**, including honest validators sharing a common implementation fault. The paper connects that fast audit quantity to a separately maintained slow state, makes observability/attribution and resource return part of the maintenance loop, derives an exact return-gap boundary, and proves when the resulting full-state dynamics preserve fast audit supercriticality. ## Files @@ -16,6 +52,9 @@ Repo-ready LaTeX package for the technical companion paper. - `references.bib` — bibliography. - `CLAIMS.md` — claim-status ledger. - `reproduce.py` — dependency-free reproduction of numerical tables. +- `../../formalization/JamRecurrentMaintenance.lean` — machine-checked two-timescale separation witnesses. +- `../../formalization/JamResilienceDynamics.lean` — machine-checked slow-to-fast bridge, maintenance-return boundary and erosion/non-identifiability results. +- `../../formalization/JamMaintenancePersistence.lean` — canonical full-state threshold, forward-invariant maintenance cone and persistent-supercriticality theorem. ## Build @@ -34,4 +73,4 @@ python reproduce.py ## Scope -This is not a JAM security audit and does not claim an observed vulnerability. Result 1 derives from the Gray Paper verdict rules under a declared correlated-fault scenario. Results 2-3 extend ELVES and therefore require review by the ELVES authors. +This is not a JAM security audit and does not claim an observed vulnerability. Result 1 derives from the Gray Paper verdict rules under a declared correlated-fault scenario. Results 2-3 extend ELVES and therefore require review by the ELVES authors. Results 4-5 add declared slow-timescale systems dynamics motivated by the repository's grounded JAM maintenance analysis. Their coefficients and reduced multipliers are not claimed to be current Gray Paper parameters or calibrated JAM estimates. The full-state result is a conditional invariant-region theorem, not a convergence, global-stability, or empirical long-run JAM theorem. diff --git a/papers/correlated-honest-failure/main.tex b/papers/correlated-honest-failure/main.tex index 7e4bd87..a51127e 100644 --- a/papers/correlated-honest-failure/main.tex +++ b/papers/correlated-honest-failure/main.tex @@ -24,7 +24,7 @@ \newcommand{\ceil}[1]{\left\lceil #1\right\rceil} \title{\textbf{Correlated Honest Failure in JAM/ELVES}\\ -\large Fault-Domain Concentration, Sampling Dilution, and Attribution Boundaries} +\large Fault-Domain Concentration, Sampling Dilution, and Dynamic Corrective Resilience} \author{Albert Jan van Hoek} \date{Draft --- September 2026} @@ -32,7 +32,7 @@ \maketitle \begin{abstract} -Execution-auditing protocols distinguish adversarial validators from honest validators, but implementation faults create a third class: validators that follow the protocol and nevertheless return the same wrong judgment on a particular crafted input. We extend the ELVES/JAM auditing model to this \emph{correlated honest failure} case and separate three consequences that arise at different protocol layers. +Execution-auditing protocols distinguish adversarial validators from honest validators, but implementation faults create a third class: validators that follow the protocol and nevertheless return the same wrong judgment on a particular crafted input. We extend the ELVES/JAM auditing model to this \emph{correlated honest failure} case and separate consequences that arise at different protocol layers and timescales. First, the current JAM dispute rules imply an attribution boundary that does not depend on the ELVES adaptive-crash model. If a fraction \(\gamma\) of validators is adversarial and a fraction \(f\) of the otherwise-honest validators shares a fault that makes one invalid report appear valid, then the maximum wrong-positive share is \(p_x=\gamma+(1-\gamma)f\). A bad verdict---and therefore the Gray Paper's ordinary culprit/fault attribution path---remains available regardless of adversarial voting only while the independently correct share is at least the verdict quorum. Asymptotically this requires \(p_x<1/3\). At \(\gamma=0.2\), this corresponds to \(f<1/6\approx16.7\%\), well below the point at which audit escalation itself becomes subcritical. @@ -44,7 +44,27 @@ Third, sampled correction breaks a monotonicity property that holds when every participant supplies an independent blocking route. Writing \(C_x\) for the number of independently correct validators in a population of size \(N\), \(\lambda_x=FC_x/N\). Adding honest validators outside \(C_x\) lowers \(\lambda_x\) even with no behavioral change. In an exact-count illustration based on \(N=1023\), \(205\) adversarial validators and \(164\) honest validators sharing one fault, adding 200 further honest validators with the same fault raises the pessimistic acceptance bound from \(4.5\times10^{-4}\) to \(0.13\) when the initial committee is held at 30; if JAM's 341 cores remain fixed so the initial sample grows with \(N\), the same bound still rises to \(0.087\). -These are model extensions, not claims about an observed JAM vulnerability. The attribution result follows from the current Gray Paper verdict rules; the branching and dilution results inherit ELVES assumptions. We identify several design questions rather than prescriptions: whether staking acts on wonky verdicts, whether fault-domain exposure should be measured across shared components, whether guarantor diversity can restore attacker-attributable collateral, and how audit effort and no-show rates behave under load. The purpose is to make the additional assumptions required by correlated honest failure explicit and reviewable by the ELVES and JAM authors. +Fourth, event-level corrective reproduction is distinct from reproduction of the capacity to remain corrective across future audits. We introduce a minimal slow return-loop model linking independently corrective capacity, observability or attribution of genuine maintenance, and resources returned to preserve that capacity. Its canonical three-cycle replacement boundary is +\[ +k_{CO}k_{OR}k_{RC}\ge(1-r_C)(1-r_O)(1-r_R). +\] +Machine-checked witnesses show that \(\lambda_x>1\) does not imply this maintenance condition and that maintenance viability does not imply \(\lambda_x>1\). The two thresholds therefore define a genuine two-timescale phase structure. + +Fifth, coupling the slow corrective-capacity coordinate to the next audit yields an exact local maintenance-return boundary. With +\[ +C_{t+1}=r_CC_t+k_{RC}R_t, +\qquad +\lambda_{x,t}=FC_t, +\] +current criticality \(\lambda_{x,t}=1\) implies +\[ +\lambda_{x,t+1}\ge1 +\quad\Longleftrightarrow\quad +Fk_{RC}R_t\ge1-r_C. +\] +A separate machine-checked finite-horizon witness gives two systems with the same current \(\lambda_0=3/2\) but opposite five-step threshold status under different cross-audit maintenance multipliers. Thus current audit reproduction is not, within the declared dynamic model, a sufficient statistic for future corrective resilience. + +These are model extensions, not claims about an observed JAM vulnerability. The attribution result follows from the current Gray Paper verdict rules; the branching, dilution, recurrent-maintenance and dynamic results inherit declared modeling assumptions. The purpose is to expose which quantities must remain above replacement if a sampled decentralized auditing system is to preserve its capacity for independent correction over time. \end{abstract} \input{sections/01_introduction.tex} @@ -52,6 +72,8 @@ \input{sections/03_attribution.tex} \input{sections/04_escalation.tex} \input{sections/05_sampling.tex} +\input{sections/06_recurrent_maintenance.tex} +\input{sections/06b_resilience_dynamics.tex} \input{sections/06_implications.tex} \input{sections/07_limitations.tex} \input{sections/08_conclusion.tex} diff --git a/papers/correlated-honest-failure/references.bib b/papers/correlated-honest-failure/references.bib index 3af6a82..1d2a9b1 100644 --- a/papers/correlated-honest-failure/references.bib +++ b/papers/correlated-honest-failure/references.bib @@ -43,3 +43,73 @@ @inproceedings{luu2015 year = {2015}, doi = {10.1145/2810103.2813659} } + +@inproceedings{sousa2007, + author = {Sousa, Paulo and Bessani, Alysson Neves and Correia, Miguel and Neves, Nuno Ferreira and Verissimo, Paulo}, + title = {Resilient Intrusion Tolerance through Proactive and Reactive Recovery}, + booktitle = {Proceedings of the 13th Pacific Rim International Symposium on Dependable Computing}, + pages = {373--380}, + year = {2007}, + doi = {10.1109/PRDC.2007.59} +} + +@inproceedings{karakostas2023, + author = {Karakostas, Dimitris and Kiayias, Aggelos and Zacharias, Thomas}, + title = {Blockchain Nash Dynamics and the Pursuit of Compliance}, + booktitle = {Proceedings of the 4th ACM Conference on Advances in Financial Technologies}, + pages = {281--293}, + publisher = {ACM}, + year = {2023}, + doi = {10.1145/3558535.3559781} +} + +@inproceedings{tran2023, + author = {Tran, Tuan and Nawab, Faisal and Alvaro, Peter and Arden, Owen}, + title = {Unstick Yourself: Recoverable Byzantine Fault Tolerant Services}, + booktitle = {2023 IEEE International Conference on Blockchain and Cryptocurrency (ICBC)}, + year = {2023}, + doi = {10.1109/ICBC56567.2023.10174886} +} + +@inproceedings{kiayias2024, + author = {Kiayias, Aggelos and Koutsoupias, Elias and Marmolejo-Coss{\'i}o, Francisco and Stouka, Aikaterini-Panagiota}, + title = {Balancing Participation and Decentralization in Proof-of-Stake Cryptocurrencies}, + booktitle = {Algorithmic Game Theory: SAGT 2024}, + series = {Lecture Notes in Computer Science}, + volume = {15156}, + pages = {333--350}, + publisher = {Springer}, + year = {2024}, + doi = {10.1007/978-3-031-71033-9_19} +} + +@article{trivedi2024, + author = {Trivedi, Kishor S. and Grottke, Michael and Lopez, Javier Alonso}, + title = {Rethinking Software Fault Tolerance}, + journal = {IEEE Transactions on Reliability}, + volume = {73}, + number = {1}, + pages = {67--72}, + year = {2024}, + doi = {10.1109/TR.2023.3330787} +} + +@article{ron2026, + author = {Ron, Javier and He, Zheyuan and Monperrus, Martin}, + title = {Proving and Rewarding Client Diversity to Strengthen Resilience of Blockchain Networks}, + journal = {Distributed Ledger Technologies: Research and Practice}, + volume = {5}, + year = {2026}, + doi = {10.1145/3773288}, + note = {Published online before the 2026 volume assignment} +} + +@misc{grandjean2023, + author = {Grandjean, Dominic and Heimbach, Lioba and Wattenhofer, Roger}, + title = {Ethereum Proof-of-Stake Consensus Layer: Participation and Decentralization}, + year = {2023}, + eprint = {2306.10777}, + archivePrefix = {arXiv}, + primaryClass = {cs.CR}, + doi = {10.48550/arXiv.2306.10777} +} diff --git a/papers/correlated-honest-failure/sections/01_introduction.tex b/papers/correlated-honest-failure/sections/01_introduction.tex index b9b0ee9..df6c5b2 100644 --- a/papers/correlated-honest-failure/sections/01_introduction.tex +++ b/papers/correlated-honest-failure/sections/01_introduction.tex @@ -6,7 +6,9 @@ \section{Introduction} The usual honest/adversarial partition hides one important failure mode. A validator can be honest in the game-theoretic and protocol sense---it executes the assigned software, announces when selected, and publishes the result it obtains---yet still be wrong because several validators share the same implementation defect. This is a classical concern in multiversion software: independently developed implementations can exhibit coincident failures on the same inputs, and nominal redundancy does not by itself imply independent failure \citep{eckhardt1985,littlewood1989}. -JAM explicitly encourages implementation diversity, but the question studied here is narrower: +Client diversity is already recognized as a resilience mechanism in blockchain systems. Longitudinal measurements of Ethereum PoS have documented both client concentration and participation disruptions associated with major clients or service operators \citep{grandjean2023}. More recently, verifiable client identification and diversity-aware rewards have been proposed as a direct way to make minority implementations economically selectable \citep{ron2026}. The present question is therefore not whether diversity matters, nor whether it can be rewarded. It is whether a sampled auditing protocol can distinguish \emph{current corrective success} from the \emph{maintenance of the capacity that makes future correction possible}. + +JAM explicitly encourages implementation diversity, but the starting question studied here is narrower: \begin{quote} \textbf{What changes in the JAM/ELVES security bookkeeping when some otherwise-honest validators share a fault that makes one crafted invalid report appear valid?} @@ -14,15 +16,19 @@ \section{Introduction} We call this \emph{correlated honest failure}. The phrase is fault-specific. A validator class can be correct for almost all reports and correlated only on one input family. Consequently the relevant quantity is not the number of clients but the size of a \emph{fault domain}: the set of validators that would produce the same erroneous judgment for the same fault. -This paper separates three layers that should not be conflated. +Following that fault-specific analysis one further question becomes unavoidable: even if independently correct checking is sufficient today, what maintains the independently corrective population, the observability of useful maintenance, and the resources that allow those capacities to persist tomorrow? + +This paper separates five questions that should not be conflated. \begin{enumerate}[label=\textbf{R\arabic*.},leftmargin=*] \item \textbf{Verdict attribution.} Given the current Gray Paper dispute rules, how large can the combined adversarial-plus-buggy-positive bloc become before a bad verdict, and therefore ordinary offender attribution, can no longer be guaranteed? \item \textbf{Audit escalation.} Under ELVES's pessimistic adaptive-crash branching model, how does a shared fault change the reproduction number of independent correction? \item \textbf{Sampling dilution.} When only a sample audits, can adding honest-but-correlated validators reduce structural safety even before incentives or behavior change? +\item \textbf{Recurrent corrective capacity.} Does event-level supercritical correction imply that the capacities supporting independent correction are themselves maintained across audits? +\item \textbf{Dynamic resilience.} Can the system remain supercritical now while its corrective margin is already on a trajectory toward future subcriticality, and what return condition prevents that crossing at the critical boundary? \end{enumerate} -The first result is the strongest because it depends only on the current JAM verdict rules plus the correlated-fault thought experiment. The second and third results are extensions of ELVES and inherit its modeling assumptions. +R1 follows from the current JAM verdict rules plus the declared correlated-fault scenario. R2--R5 are model extensions of increasing scope: R2--R3 extend the ELVES branching bookkeeping, while R4--R5 add an explicitly declared cross-audit maintenance layer. The latter variables are not claimed to be existing Gray Paper state variables. \subsection{Main results} @@ -71,14 +77,36 @@ \subsection{Main results} \] The ordering is illustrated in \Cref{fig:thresholds}. -Finally, with \(C_x\) fixed, +With \(C_x\) fixed, \[ \lambda_x(N)=F\frac{C_x}{N} \] is strictly decreasing in \(N\). Hence adding honest validators that belong to the same fault domain can reduce the corrective reproduction number without any behavioral response. The effect remains in a JAM-specific fixed-core variant in which the expected initial sample grows with validator count, although the larger sample partly offsets the dilution. +R4 then separates this event-level condition from a slower maintenance condition. In a minimal declared cycle linking corrective capacity \(C\), maintenance observability \(O\), and returned resources \(R\), the canonical replacement condition is +\[ +\boxed{ +k_{CO}k_{OR}k_{RC}\ge(1-r_C)(1-r_O)(1-r_R). +} +\] +Machine-checked counterexamples show that this condition and \(\lambda_x>1\) imply neither one another. + +R5 adds time. Let the normalized independently corrective coordinate evolve as +\[ +C_{t+1}=r_C C_t+k_{RC}R_t, +\qquad +\lambda_{x,t}=F C_t. +\] +At the fast critical boundary \(\lambda_{x,t}=1\), the next audit remains at or above criticality exactly when +\[ +\boxed{ +F k_{RC}R_t\ge 1-r_C. +} +\] +This gives a maintenance-return boundary in the same units as the current audit threshold. A separate machine-checked finite-horizon witness shows that two systems can have the same current supercritical value \(\lambda_0=3/2\) yet lie on opposite sides of the threshold five rounds later when their cross-audit maintenance multipliers differ. Current audit reproduction is therefore not, within the declared dynamic model, a sufficient statistic for horizon resilience. + \subsection{Scope} -Nothing in this paper establishes that JAM currently violates a security requirement or that a particular correlated client bug exists. The model deliberately asks what follows \emph{if} a crafted report lies inside a shared fault domain. The results are therefore best read as assumption audits and design margins. +Nothing in this paper establishes that JAM currently violates a security requirement or that a particular correlated client bug exists. The model deliberately asks what follows \emph{if} a crafted report lies inside a shared fault domain and, for R4--R5, what follows under explicitly declared maintenance dynamics. The results are therefore best read as assumption audits, phase boundaries and candidate resilience margins. The paper also distinguishes accidental failure from strategic exploitation. For an accidental bug, assignment probabilities determine how often a bad report is produced and how often independently correct auditors see it. For a strategic attacker who knows the bug, opportunity can be concentrated on favorable assignments. We quantify the frequency of such assignments but do not assume the attacker can route arbitrary work to a chosen core unless that ability is established separately. diff --git a/papers/correlated-honest-failure/sections/02_protocol_and_model.tex b/papers/correlated-honest-failure/sections/02_protocol_and_model.tex index 0dbde2f..458d929 100644 --- a/papers/correlated-honest-failure/sections/02_protocol_and_model.tex +++ b/papers/correlated-honest-failure/sections/02_protocol_and_model.tex @@ -1,115 +1,106 @@ -\section{Protocol elements and model} +\section{Protocol and model} \label{sec:model} -\subsection{JAM auditing and disputes} +\subsection{JAM/ELVES audit structure} -The current Gray Paper states that JAM's auditing and judging system is theoretically equivalent to ELVES \citep{wood2026,burdges2024}. Each validator initially audits a random deterministic selection of up to ten active cores. If an announced auditor fails to produce a positive judgment, later tranches recruit additional auditors. The Gray Paper sets the audit bias factor to +The present paper treats ELVES as the execution-auditing abstraction and the JAM Gray Paper as the protocol-facing specialization. The key architectural feature is sampled re-execution with escalation: a small initial set checks a report, and unresolved disagreement recruits further checking capacity. The exact JAM verdict layer then aggregates judgments into good, bad or wonky outcomes. + +We keep three levels separate throughout: +\begin{enumerate}[leftmargin=*] +\item the \emph{verdict rule}: which collections of judgments permit a good, bad or wonky verdict; +\item the \emph{audit branching model}: how independently correct checking reproduces during escalation; +\item the \emph{cross-audit maintenance model}: how the capacity supplying independent correction is retained, observed and resourced across time. +\end{enumerate} + +Only the first is a direct Gray Paper rule. The second is inherited from ELVES and extended by a correlated-fault partition. The third is introduced in Results 4--5 as a declared systems model. + +\subsection{Fault-specific validator classes} + +Fix one invalid report and one fault family $x$. Partition the validator set into: +\begin{itemize} +\item $A$: adversarial validators; +\item $B_x$: otherwise-honest validators whose shared fault causes the report to be judged valid; +\item $C_x$: validators that independently judge the report invalid. +\end{itemize} +Thus \[ -F=2, +N=A+B_x+C_x. \] -meaning that one unmatched announcement induces an expected two additional auditors in the next tranche. A negative judgment instead causes broad re-auditing and opens the dispute path. +The adjective \emph{independently correct} is fault-specific. It does not imply globally independent software, nor does membership in $B_x$ imply that a validator is generally unreliable. -The dispute rules are central to our first result. Let +Define \[ -K=\floor{\frac{2N}{3}}+1 +\gamma=\frac{A}{N}, +\qquad +f_x=\frac{B_x}{N-A}, +\qquad +h_x=\frac{C_x}{N}=(1-\gamma)(1-f_x), \] -be the number of judgments carried by a verdict and +and \[ -W=\floor{\frac{N}{3}} +p_x=1-h_x=\gamma+(1-\gamma)f_x. \] -the number of positive judgments required for a wonky verdict. Under the current Gray Paper rule, a verdict is: -\begin{itemize} -\item \textbf{good} if all \(K\) included judgments are positive; -\item \textbf{bad} if all \(K\) included judgments are negative; -\item \textbf{wonky} if exactly \(W\) of the \(K\) judgments are positive. -\end{itemize} - -Bad and wonky verdicts remove the availability assignment. The Gray Paper's ordinary offense paths are tied to good or bad reports: guarantors of a bad report can be included as culprits, and judges contradicting an established good/bad verdict can be included as faults. A wonky report is recorded in the wonky set, but the current specification does not place its guarantors or judges in the punish set through those culprit/fault rules \citep{wood2026}. +Here $p_x$ is the maximum share that can return a wrong positive judgment for the declared report if adversarial validators coordinate with the shared fault. -This paper therefore uses the precise phrase \emph{protocol-defined offender attribution path} rather than equating a wonky verdict with zero economic consequences. A staking subsystem could in principle react to the wonky record; the Gray Paper leaves validator rewards and much of the higher-level economics outside the JAM chain itself. +\subsection{Verdict threshold} -\subsection{ELVES branching quantities} - -ELVES models the audit-tranche process with a pessimistic adaptive-crash adversary. Let \(s_0\) be the expected initial audit committee and let \(F\) be the expected number of auditors recruited per unmatched prior auditor. If a fraction \(\gamma\) of the validator population is adversarial, the mean number of useful honest offspring in the branching approximation is -\[ -\lambda=(1-\gamma)F. -\] -If \(q\) is the extinction probability of the corresponding Poisson Galton--Watson process, then +For verdict-set size $N$, write \[ -q=\exp[-\lambda(1-q)], +K=\floor{\frac{2N}{3}}+1. \] -and the ELVES soundness analysis yields the pessimistic acceptance bound +The analysis uses the Gray Paper verdict composition rules exactly as stated in the protocol snapshot cited in this repository. A bad verdict requires a qualifying set containing no positive judgments. Therefore independently correct negative judgments can construct a bad verdict against adversarial positive voting iff \[ -\boxed{ -P_{\rm accept}\le q^{s_0/F}. -} +C_x\ge K. \] -Useful escalation requires \(\lambda>1\). +This result is independent of the ELVES branching approximation. + +\subsection{Fault-specific audit reproduction} -The same architecture has a no-show/scalability side. If \(u\) is the fraction represented in the no-show/fault-amplification term, the reproduction number is \(uF\), so the static expected-final-committee bound has the form +For the ELVES-style escalation extension, let $F$ denote the tranche/escalation factor. Replacing the independently honest share by the fault-specific independently correct share yields the declared reproduction mean \[ -\boxed{ - s_f\le\frac{s_0}{1-uF}, - \qquad uF<1. -} +\lambda_x=Fh_x=F\frac{C_x}{N}=F(1-\gamma)(1-f_x). \] -ELVES reports a continuous-model optimum near \(F=2.0794\) under its stated assumptions; the Gray Paper uses \(F=2\). - -\subsection{Correlated honest fault domain} - -For one crafted invalid report and one fault class \(x\), partition the verdict population into: -\begin{align*} -A &: \text{adversarial validators},\\ -B_x &: \text{otherwise-honest validators that judge the invalid report as valid},\\ -C_x &: \text{otherwise-honest validators that independently judge it as invalid}. -\end{align*} -Thus +The supercritical condition is \[ -N=A+B_x+C_x. +\lambda_x>1. \] +This substitution is a model extension and is not presented as a theorem from the original ELVES paper. + +\subsection{Slow corrective-capacity state} -The central distinction is: +Results 4--5 add a separate cross-audit state. To avoid confusing a count with a normalized state variable, write \[ -\boxed{ -\text{honest validator count} -\neq -\text{fault-specific independently corrective validator count}. -} +c_{x,t}\in\mathbb R \] +for the model's normalized fault-specific independently corrective coordinate at slow time $t$. In the simplest mapping to the static partition, $c_{x,t}$ corresponds to an effective independently correct share like $C_{x,t}/N_t$, but the dynamic model leaves empirical construction of this quantity open. -When convenient we write +The remaining coordinates are \[ -\gamma=\frac{A}{N}, +o_t=\text{maintenance observability/attribution capacity}, \qquad -f_x=\frac{B_x}{N-A}, +r_t=\text{returned-resource capacity}. \] -so +For readability, the later dynamic sections denote these three coordinates by capital letters $(C_t,O_t,R_t)$; there $C_t$ is a normalized slow-state coordinate, not the earlier validator count $C_x$. + +The declared linear update is +\begin{align} +C_{t+1}&=r_C C_t+k_{RC}R_t,\\ +O_{t+1}&=r_O O_t+k_{CO}C_t,\\ +R_{t+1}&=r_R R_t+k_{OR}O_t. +\end{align} +Coupling the slow corrective coordinate to the next audit gives \[ -\frac{C_x}{N}=(1-\gamma)(1-f_x). +\lambda_{x,t}=F C_t. \] -The parameter \(f_x\) should not be interpreted as a universal client market share. It is the exposure of honest validators to fault \(x\). A client implementation is one possible fault domain, but shared libraries, compilers, virtual machines, cryptographic code, erasure-coding implementations, or copied specification logic can couple nominally distinct clients. - -\subsection{Claim-status map} - -\begin{table}[htbp] -\centering -\small -\caption{Status of the main claims. Extension means derived after changing an ELVES/JAM assumption; it is not attributed to the original authors.} -\label{tab:claims} -\begin{tabularx}{\textwidth}{@{}p{0.05\textwidth}X p{0.23\textwidth}@{}} -\toprule -ID & Claim & Status \\ -\midrule -A1 & A bad verdict remains constructible against adversarial positive voting iff \(C_x\ge K\). & Exact consequence of Gray Paper verdict rule + declared fault model \\ -A2 & A good verdict becomes constructible if \(A+B_x\ge K\). & Exact consequence of Gray Paper verdict rule + declared fault model \\ -A3 & For large \(N\), robust bad-verdict attribution requires \(\gamma+(1-\gamma)f_x<1/3\). & Asymptotic form of A1 \\ -B1 & Correlated honest failure changes the ELVES corrective mean to \(\lambda_x=F C_x/N\). & ELVES extension \\ -B2 & Supercritical correction requires \(f_x<1-1/[(1-\gamma)F]\). & Exact consequence of B1 \\ -B3 & Increasing \(F\) raises fault-domain tolerance while worsening the static no-show committee bound. & ELVES extension / comparative result \\ -C1 & Holding \(C_x\) fixed, adding validators outside the independently correct set strictly lowers \(\lambda_x=FC_x/N\). & Exact sampling identity \\ -C2 & In the declared baseline, the pessimistic acceptance bound worsens under such additions both for fixed \(s_0=30\) and fixed 341 cores. & Computational specialization \\ -D1 & Slashable collateral need not be attacker-attributable collateral under an honest shared bug. & Economic mapping observation; not a theorem of JAM \\ -D2 & Guarantor diversity, effort proofs, announcement monitoring and load feedback are design questions, not established fixes. & Hypotheses / future work \\ -\bottomrule -\end{tabularx} -\end{table} +No claim is made that the Gray Paper already contains these state variables or linear coefficients. They are introduced to expose which additional empirical quantities are required if current audit correction is to be translated into a claim about persistence of correction. + +\subsection{Claim hierarchy} + +The model therefore has an explicit hierarchy: +\begin{enumerate}[leftmargin=*] +\item exact verdict arithmetic under the Gray Paper rules and declared fault partition; +\item ELVES-style branching consequences under the substitution $h_x=C_x/N$; +\item slow maintenance replacement consequences under declared $C\to O\to R\to C$ dynamics; +\item finite-horizon implications after coupling $C_t$ back to $\lambda_{x,t}$. +\end{enumerate} +The claim ledger records these levels separately so that a failure of a higher-level mapping does not invalidate lower-level protocol arithmetic. diff --git a/papers/correlated-honest-failure/sections/06_implications.tex b/papers/correlated-honest-failure/sections/06_implications.tex index 14d9898..3332afe 100644 --- a/papers/correlated-honest-failure/sections/06_implications.tex +++ b/papers/correlated-honest-failure/sections/06_implications.tex @@ -1,86 +1,65 @@ -\section{Corollaries and design questions} -\label{sec:implications} +\section{Implications and design questions} -The three main results are analytical. The following items are consequences or engineering questions, not recommendations established by the model. +The results above do not identify a single protocol fix. They identify distinct interfaces at which correlated honest failure and long-run corrective-capacity loss can enter the system. Keeping those interfaces separate avoids turning a structural analysis into an unsupported prescription. -\subsection{Slashable collateral is not necessarily attacker-attributable collateral} +\subsection{Slashable collateral and attacker-attributable collateral} -ELVES's rational-adversary argument makes invalid acceptance prohibitively expensive by charging collateral to the attack path \citep{burdges2024}. In a conventional attack, the parties signing or backing an invalid result can be economically aligned with the attacker. +If honest guarantors share a bug and sign an invalid report because they genuinely compute the same wrong result, their stake may be slashable under a higher-layer mechanism without being attacker-controlled collateral. These are different economic objects. A security argument that counts all slashable stake as attacker cost therefore requires an explicit attribution mechanism when correlated honest failure is in scope. -A shared implementation bug changes that mapping. If otherwise-honest guarantors compute the same wrong result and sign it, a later bad verdict can place \emph{their} signatures in the culprit path. The protocol may destroy collateral, yet the actor that selected the crafted input may not bear that loss. +The paper does not claim that honest buggy guarantors are unpunished. It claims only that punishment of a mistaken participant is not automatically equivalent to economic loss borne by the adversary who found or exploited the shared bug. -The distinction is: -\[ -\boxed{ -\text{slashable collateral} -\neq -\text{attacker-attributable collateral}. -} -\] +\subsection{Wonky outcomes and attribution gaps} -This does not prove that exploiting the bug is cost-free. It means that the specific expected-profit argument needs an additional mapping from protocol offender to economic beneficiary when honest common-mode faults are admitted. +Under the Gray Paper verdict interpretation used here, a wonky verdict does not create the ordinary culprit/fault offender record. Whether a production staking layer attaches additional consequences is a separate question and should be confirmed with the JAM authors. If wonky outcomes are intentionally an uncertainty state, correlated honest failure gives a concrete reason that such a state may occur without Byzantine equivocation. -The wonky region strengthens the issue: the current Gray Paper does not create ordinary culprit/fault offender records for wonky reports. Whether the staking layer imposes a cost on a wonky report is therefore a first-order question for the protocol authors. +\subsection{Fault-domain exposure rather than client count} -\subsection{Guarantor diversity as a design hypothesis} +The analysis suggests tracking exposure to common components rather than only counting nominal clients. Candidate dimensions include implementation family, version, execution engine, shared libraries, compiler/toolchain, operating system, cloud/operator concentration and common specification interpretations. None is individually equivalent to a fault domain; together they can provide a conservative exposure map. -Every active core has three assigned guarantors and a guarantee carries two or three credentials. If a single fault domain occupies population share \(r\), the probability that at least two of three randomly assigned guarantors belong to that domain is -\[ -\Prb(\ge2)=3r^2(1-r)+r^3. -\] -At \(r=0.2\), this is \(0.104\). Across 341 cores, the expectation is approximately 35.5 core assignments per rotation with at least two guarantors from that domain. +Existing work proposes making client implementation verifiable and using that information to reward minority clients \citep{ron2026}. That can improve one important layer of diversity management. The present analysis adds a stricter criterion: a diversity mechanism matters for audit resilience only insofar as it preserves or increases fault-specific independently corrective capacity. -This number does \emph{not} establish that an attacker can route a crafted package to one of those cores. It quantifies the frequency of favorable assignments if exploitation opportunities can be targeted or waited for. +\subsection{Guarantor diversity} -One possible mitigation is to require the credential set for a guarantee to span declared implementation/fault-domain classes. This could prevent a single honest client bug from supplying both signatures. But the idea has unresolved issues: -\begin{itemize} -\item implementation identity may be self-declared and therefore gameable; -\item nominally distinct clients can share deeper components; -\item diversity constraints may reduce liveness when one implementation class is unavailable; -\item an adversarial validator can lie about identity, although doing so may force its own signature onto the report. -\end{itemize} -Hence guarantor diversity is a hypothesis to analyse, not a proposed protocol change in this paper. +If guarantors for a work report are drawn from different fault domains, a shared implementation defect is less likely to produce unanimous or near-unanimous false support. This is a design hypothesis, not a recommendation established by the present paper. Enforcing diversity can add assignment constraints, latency, implementation-identification requirements and new strategic surfaces. -\subsection{Fault-domain exposure metrics} +\subsection{Announcement and effort observability} -The quantity that matters for an unknown future bug cannot be measured directly: by definition we do not know which validators will be wrong on an input not yet discovered. +The repository's earlier JAM experiments separate nominal participation from useful independent computation. A validator can announce availability yet still contribute little independent corrective information if it rubber-stamps, reuses a correlated result, or relies on the same faulty implementation path. Effort observability therefore affects whether rewards can selectively maintain real checking capacity. -What can be measured is \emph{exposure} to shared components. Examples include validator share by: -\begin{itemize} -\item client implementation; -\item execution VM; -\item compiler/toolchain; -\item cryptographic or erasure-coding library; -\item major shared dependencies; -\item copied or common code paths. -\end{itemize} +This becomes more important in the dynamic model. The slow return loop requires not merely that corrective work exists, but that useful maintenance can be observed well enough for resources to return to the capacities that generated it. Weak maintenance observability can therefore convert an apparently adequate current audit layer into a long-run replacement shortfall. + +\subsection{A maintenance-return margin} + +Result 5 suggests a concrete candidate diagnostic near the current fast threshold. Under the declared coupling, +\[ +M_t=Fk_{RC}R_t-(1-r_C). +\] +At $\lambda_{x,t}=1$, the sign of $M_t$ exactly determines whether the next slow update lies below, at, or above the current audit threshold. -These are upper bounds or proxies for possible fault-domain concentration, not measurements of \(f_x\) for an unknown bug. A useful operational question is therefore whether the largest identifiable shared-component exposure leaves adequate margin below the attribution and escalation boundaries. +The value is not that this particular expression should be hard-coded into JAM. The value is methodological: a protocol can expose a current safety/correction threshold while leaving the replenishment process that maintains the state variable behind that threshold unmeasured. Once the replenishment state is explicit, a replacement-gap diagnostic becomes possible. -\subsection{Announcement shortfall as an early-warning statistic} +A deployment-facing analogue of $M_t$ would require measurable estimates of attrition and return. Possible observables include independent client/operator entry and exit, version concentration, economically sustained minority implementations, audit effort that can be independently verified, and development or operator resources returned to those implementations. Estimation uncertainty should be reported rather than hidden inside a point parameter. -JAM's later tranches respond to unmatched announcements. A validator that is offline before announcing is different: it simply reduces the number of initial auditors that appear. +\subsection{Early warning rather than post-failure diagnosis} -Aggregate announcement counts per report can therefore serve as a statistical early-warning signal for loss of available corrective capacity. The expected count is known from validator count and active-core configuration. A sustained shortfall can indicate that the online population is smaller than the nominal population. +The strongest practical consequence of the dynamic result is temporal. If current $\lambda_x$ is above one but declining because maintenance is below replacement, waiting for $\lambda_x\le1$ detects the problem only after the structural correction condition has already been lost. Monitoring the maintenance-return process creates the possibility of detecting erosion earlier. -This is not a deterministic fault detector. Audit assignment is random, observations are local before information propagates, and the current formal validator-statistics tuple does not directly expose a finalized audit-count metric. The proposal is simply to monitor the discrepancy between expected and observed audit participation. +This reframes resilience as a two-signal problem: +\[ +\text{current corrective margin} +\quad+\quad +\text{maintenance-return margin}. +\] +The first asks whether correction is sufficient now. The second asks whether the processes supplying that correction are being reproduced. A strong implementation of the idea would estimate both through time and test whether deterioration in the second predicts deterioration in the first. -\subsection{Rubber-stamping remains an open interface} +\subsection{Load-dependent no-shows and feedback} -The Gray Paper notes that auditing activity is difficult to track directly and delegates validator rewards to a staking subsystem; peer voting on impressions of validator effort is described as the available oracle mechanism \citep{wood2026}. +The existing ELVES trade-off between larger escalation factor $F$ and no-show growth becomes more complicated if no-show probability itself depends on audit load. The present paper does not solve that endogenous-load problem. It does show why the direction matters: stronger escalation can improve event-level corrective reproduction while simultaneously increasing resource demand, and long-run capacity may respond to that demand. -That leaves a classic verifier's-dilemma-style question \citep{luu2015}: how strongly does the reward signal discriminate actual re-execution from a validator that produces the expected positive judgment without paying the full computation cost? +A future extension should therefore treat validator availability, maintenance cost, observability and returned resources as jointly dynamic rather than independent constants. Such an extension should be attempted only after the simpler state variables can be tied to measurable JAM quantities. -The present paper does not claim that rubber-stamping is selected in JAM. The reward function and effort-observability mechanism are not sufficiently specified to close that game numerically. Candidate approaches such as verifiable execution artifacts, occasional test reports, or other proof-of-effort mechanisms should therefore be evaluated only after the actual staking design is specified. +\subsection{What should be tested next} -\subsection{Load-dependent no-shows are a separate future model} +The most informative next test is not another static client-diversity count. It is a longitudinal test of the proposed separation. On a JAM testnet or sufficiently instrumented deployment, estimate a time series for current fault-domain corrective capacity and independent proxies for maintenance return. Then ask whether maintenance shortfall predicts subsequent loss of corrective margin after controlling for validator-set size and audit load. -ELVES treats the no-show/fault share used in its committee-size analysis as exogenous. In a real implementation, no-show probability could rise with audit load. If -\[ -u=u(L), -\] -and load \(L\) grows with the final committee size, then -\[ - s_f\approx\frac{s_0}{1-Fu(s_f)} -\] -becomes a feedback equation. This could amplify load under stress, but no claim of a JAM overload transition is made without empirical measurements of \(u(L)\). A testnet stress experiment measuring deadline misses against concurrent audit load would be the appropriate next step. +A failure of that prediction would be scientifically useful: it would indicate that the declared $C\!\to O\!\to R\!\to C$ abstraction misses an important replenishment pathway. A successful prediction would turn recurrent corrective capacity from a conceptual distinction into an operational resilience quantity. diff --git a/papers/correlated-honest-failure/sections/06_recurrent_maintenance.tex b/papers/correlated-honest-failure/sections/06_recurrent_maintenance.tex new file mode 100644 index 0000000..cfd0309 --- /dev/null +++ b/papers/correlated-honest-failure/sections/06_recurrent_maintenance.tex @@ -0,0 +1,135 @@ +\section{Result 4: correction reproduction is not maintenance reproduction} +\label{sec:recurrent-maintenance} + +The preceding results concern what happens \emph{within} an audit or dispute episode. A distinct question is whether the system preserves the capacity required to remain corrective across future episodes. The two questions should not be identified. + +\subsection{Two timescales} + +For a fault $x$, the event-level corrective reproduction mean in the correlated-honest-failure extension is +\[ +\lambda_x=F(1-\gamma)(1-f_x). +\] +The condition +\[ +\lambda_x>1 +\] +means that independently correct checking is supercritical for the declared audit process. It does not state that the resources, observability or implementation diversity required for such checking will persist across time. + +To make that second problem explicit, introduce three slow capacities: +\[ +C_t=\text{independently corrective capacity}, +\] +\[ +O_t=\text{capacity to observe or attribute genuine maintenance}, +\] +\[ +R_t=\text{resources returned to preserve future corrective capacity}. +\] +These variables are a model extension rather than Gray Paper state variables. The simplest directed return loop is +\[ +C\longrightarrow O\longrightarrow R\longrightarrow C. +\] +Write $r_C,r_O,r_R$ for autonomous one-step retention factors and $k_{CO},k_{OR},k_{RC}$ for the three directed coupling gains. The canonical finite-cycle replacement condition is +\[ +\boxed{ + k_{CO}k_{OR}k_{RC} + \ge + (1-r_C)(1-r_O)(1-r_R). +} +\] +For convenience define the dimensionless loop ratio +\[ +\mathcal R_M += +\frac{k_{CO}k_{OR}k_{RC}} +{(1-r_C)(1-r_O)(1-r_R)} +\] +when the denominator is positive. Then the canonical replacement boundary is $\mathcal R_M\ge1$. + +The underlying product/spectral threshold mathematics is standard positive-systems and reproduction-number structure; no novelty is claimed for that mathematics. The point here is the separation of this slower maintenance threshold from the ELVES event-level reproduction threshold. + +\subsection{The thresholds are logically independent} + +The repository now machine-checks explicit witnesses in Lean. + +First, current correction may be supercritical while recurrent maintenance is subcritical. Set +\[ +F=2,\qquad \gamma=0,\qquad f_x=0. +\] +Then +\[ +\lambda_x=2>1. +\] +But if +\[ +r_C=r_O=r_R=0, +\qquad +k_{CO}=k_{OR}=k_{RC}=\frac12, +\] +then the maintenance deficit product is $1$ while the loop gain is $1/8$. Hence the slow loop is below replacement. + +Second, a viable maintenance loop does not imply fault-specific correction for the current audit. Set +\[ +r_C=r_O=r_R=\frac12, +\qquad +k_{CO}=k_{OR}=k_{RC}=1. +\] +Then the maintenance loop gain is $1$ against deficit product $1/8$, so it is above the canonical replacement boundary. But with +\[ +F=2,\qquad \gamma=0,\qquad f_x=\frac34, +\] +we obtain +\[ +\lambda_x=\frac12<1. +\] +Thus an economically and operationally persistent validator ecosystem can still be insufficiently independently corrective for a particular correlated fault. + +These two counterexamples establish +\[ +\boxed{ +\lambda_x>1 +\not\Rightarrow +\mathcal R_M\ge1, +} +\] +and +\[ +\boxed{ +\mathcal R_M\ge1 +\not\Rightarrow +\lambda_x>1. +} +The Lean module also explicitly inhabits the jointly viable and jointly non-viable cells, so the two predicates form a genuine two-dimensional phase structure in this declared model. + +\subsection{Two-timescale phase structure} + +The resulting interpretation is: + +\begin{center} +\begin{tabularx}{\textwidth}{lXX} +\toprule +& recurrent maintenance above replacement & recurrent maintenance below replacement \\ +\midrule +$\lambda_x>1$ & current correction is supercritical and the modeled maintenance loop is viable & current correction is supercritical now, but the modeled capacity that supports future correction is eroding \\ +$\lambda_x\le1$ & maintenance resources/processes persist, but independent correction is insufficient for fault $x$ & neither condition is met \\ +\bottomrule +\end{tabularx} +\end{center} + +The upper-right cell is the main systems question opened by this separation. A protocol can satisfy its current audit-reproduction condition while selecting against, failing to observe, or failing to resource the costly capacities on which that condition depends in the future. Result 5 turns this qualitative statement into an explicit cross-audit state update and asks when the fast threshold is actually crossed. + +The lower-left cell is the complementary failure mode. Persistence of validators, rewards and monitoring infrastructure is not equivalent to preservation of fault-specific independent correction. A homogeneous but well-funded implementation ecosystem can remain operational while losing the diversity needed for one shared fault. + +\subsection{Relation to the Gray Paper and ELVES} + +This result does not claim that JAM currently has a closed $C\!\to O\!\to R\!\to C$ loop with known coefficients. Rather, the Gray Paper and the preceding repository experiments expose interfaces corresponding to the three functions: + +\begin{itemize} +\item useful audit computation supplies independently corrective capacity; +\item effort and judgment information can make maintenance observable or attributable; +\item staking, operator economics and implementation ecosystems determine whether resources are returned to preserve that capacity. +\end{itemize} + +Some of these mechanisms are explicitly delegated outside the audited assurance layer. That delegation is precisely why event-level correction and cross-time maintenance should be represented by different conditions rather than by one reproduction number. + +The falsifiable design question is therefore not merely whether $\lambda_x>1$ today. It is whether the surrounding protocol, staking and client ecosystem jointly close a return loop that keeps independently corrective capacity available across future audits. Result 5 derives the corresponding one-step replacement condition at the fast critical boundary. diff --git a/papers/correlated-honest-failure/sections/06b_resilience_dynamics.tex b/papers/correlated-honest-failure/sections/06b_resilience_dynamics.tex new file mode 100644 index 0000000..7fdec8d --- /dev/null +++ b/papers/correlated-honest-failure/sections/06b_resilience_dynamics.tex @@ -0,0 +1,161 @@ +\section{Result 5: current correction is not a sufficient statistic for future resilience} +\label{sec:resilience-dynamics} + +Result 4 separates two reproduction conditions. The next question is dynamic: can a system remain on the supercritical side of the current audit condition while the capacity supporting future correction is already eroding? + +\subsection{Coupling slow capacity to fast audit reproduction} + +Let the slow maintenance state at cross-audit time $t$ be +\[ +X_t=(C_t,O_t,R_t), +\] +where $C_t$ is a normalized fault-specific independently corrective share/capacity, $O_t$ is maintenance observability or attribution capacity, and $R_t$ is returned-resource capacity. The notation $C_t$ in this section is a normalized slow-state coordinate; it is not the earlier validator count $C_x$. + +Consider the declared linear update +\begin{align} +C_{t+1}&=r_C C_t+k_{RC}R_t,\\ +O_{t+1}&=r_O O_t+k_{CO}C_t,\\ +R_{t+1}&=r_R R_t+k_{OR}O_t. +\end{align} +The variables and coefficients remain model quantities rather than Gray Paper state variables. + +For fixed audit escalation factor $F$, couple the fast fault-specific reproduction number directly to the corrective coordinate: +\[ +\lambda_{x,t}=F C_t. +\] +It follows exactly that +\[ +\lambda_{x,t+1} +=r_C\lambda_{x,t}+F k_{RC}R_t. +\] +This identity is machine checked in the repository. + +\subsection{An exact maintenance-return boundary} + +The most useful local case is the fast critical boundary. Suppose +\[ +\lambda_{x,t}=1. +\] +Then +\[ +\lambda_{x,t+1}=r_C+F k_{RC}R_t, +\] +and therefore +\[ +\boxed{ +\lambda_{x,t+1}\ge1 +\quad\Longleftrightarrow\quad +F k_{RC}R_t\ge1-r_C. +} +\] +Thus the quantity +\[ +\boxed{ +M_t=F k_{RC}R_t-(1-r_C) +} +\] +acts as a local maintenance-return margin at the audit critical boundary. A negative margin implies that a system sitting exactly at current criticality crosses below it on the next cross-audit update; a positive margin moves it above criticality. + +This one-step boundary is deliberately local. Its advantage is interpretability: the left side is the familiar event-level audit threshold, while the right side states exactly how much effective returned resource is required to replace attrition in the corrective coordinate. + +\subsection{From the closed maintenance threshold to persistent correction} + +The static product threshold from Result 4 can also be connected directly to the full slow dynamics, without introducing a reduced multiplier. Define the canonical maintenance state +\begin{align} +C^*&=(1-r_O)(1-r_R),\\ +O^*&=k_{CO}(1-r_R),\\ +R^*&=k_{CO}k_{OR}. +\end{align} +At this state, the $O$ and $R$ coordinates are exactly at replacement. The $C$ coordinate is at or above replacement exactly when +\[ +\boxed{ +(1-r_C)(1-r_O)(1-r_R) +\le +k_{CO}k_{OR}k_{RC}. +} +\] +This is the same three-process maintenance threshold used in Result 4, now expressed on the time-indexed state system. + +Under nonnegative retention and coupling coefficients, the Lean formalization proves a stronger statement: the entire coordinatewise cone above $(C^*,O^*,R^*)$ is forward invariant whenever the product threshold is met. A trajectory initialized at the canonical state therefore remains at or above that state at every future cross-audit time. + +This yields the direct persistence theorem. If +\[ +F C^*>1, +\] +then +\[ +\boxed{ +\lambda_{x,t}>1\quad\text{for every }t\ge0 +} +\] +for the canonical maintenance trajectory. Thus the slow maintenance threshold is not merely a static feasibility condition: together with a sufficiently large canonical corrective coordinate, it supplies an explicit invariant region that preserves fast audit supercriticality indefinitely in the declared model. + +The converse failure mechanism is equally transparent. Deleting the immediate return edge $R\to C$ sets $k_{RC}=0$. If $r_C<1$ and $C_t>0$, then +\[ +C_{t+1}=r_C C_t1$. If only half of $C_t$ is retained and the immediate returned-resource contribution to $C_{t+1}$ is zero, the next reproduction number is $3/4<1$. Current supercriticality alone therefore supplies no invariant preventing a future threshold crossing. + +\subsection{Relation to prior resilience and incentive dynamics} + +None of the individual ingredients above is claimed to be new in isolation. Software fault-tolerance research has long studied design diversity, environmental diversity, proactive recovery and rejuvenation as ways to prevent present operation from degrading into future failure \citep{trivedi2024}. Proactive Byzantine-fault-tolerance work goes closer still: recovery and reconfiguration are used to stop faulty replicas from accumulating beyond a tolerated bound over the lifetime of a system \citep{sousa2007,tran2023}. Blockchain research has likewise studied dynamic incentive compliance \citep{karakostas2023}, payment schemes that balance participation and decentralization \citep{kiayias2024}, longitudinal validator concentration \citep{grandjean2023}, and mechanisms that identify and reward minority client implementations \citep{ron2026}. + +The narrower contribution proposed here is different in the object that must be reproduced. Classical proactive BFT maintains enough nonfaulty replicas relative to a fault bound. The present JAM/ELVES extension instead tracks the \emph{fault-specific independently corrective capacity} that enters a sampled audit reproduction number, including honest validators that may share the same implementation error. It then makes maintenance of that capacity endogenous through observability/attribution and resource return. The model derives an exact return-gap boundary for the next audit and proves both a full-state persistence region and counterexamples in which the same current audit reproduction implies different future resilience. The positive-systems, recovery and geometric-decay mathematics is prior art; the proposed contribution is this composition at the sampled-audit/common-mode-failure interface. + +\subsection{What would make this operational?} + +The formal result shifts the empirical question. Measuring current client shares or current audit success is not enough to estimate persistence of correction. A deployment would need evidence about at least: +\begin{itemize} +\item the rate at which independently corrective implementations/operators enter, leave, converge, or become correlated; +\item whether useful independent audit effort can be distinguished from nominal participation; +\item whether rewards, operator revenue, tooling and development resources return preferentially to capacities that preserve independent correction; +\item whether those return flows close the measured replacement gap before the fast margin is exhausted. +\end{itemize} + +Mechanisms that prove client identity and reward minority implementations \citep{ron2026} can instantiate part of the $O\to R$ pathway. The present model asks the additional systems question: whether the resulting return loop is strong enough, relative to attrition, to preserve the fault-specific corrective capacity on which the audit process relies. + +Longitudinal measurements are therefore central. Ethereum evidence already shows that validator participation and concentration are time-dependent and can be affected by major clients and operators \citep{grandjean2023}. For JAM, the corresponding resilience object would be a time-dependent pair: the current fault-specific audit reproduction margin together with an empirically grounded maintenance-return margin. diff --git a/papers/correlated-honest-failure/sections/07_limitations.tex b/papers/correlated-honest-failure/sections/07_limitations.tex index b8326e9..6961f2c 100644 --- a/papers/correlated-honest-failure/sections/07_limitations.tex +++ b/papers/correlated-honest-failure/sections/07_limitations.tex @@ -1,53 +1,44 @@ -\section{Limitations and questions for the ELVES/JAM authors} -\label{sec:limitations} +\section{Limitations and claim boundaries} -The purpose of this paper is to expose assumptions, not to claim a complete security analysis. Several issues require author or implementation review. +This paper combines one direct protocol-rule derivation with several declared model extensions. The distinction is essential. -\subsection{Correlated honest failure is outside the ELVES proof model} +\paragraph{Correlated fault domains are hypothetical inputs, not observed JAM failures.} +The paper does not establish that a currently deployed or planned JAM client contains a fault shared by any particular validator fraction. The fault-domain model asks what follows if such a dependency exists. -The branching extension assumes that a buggy honest auditor behaves like an auditor that cannot produce a useful negative judgment for fault \(x\). This is a natural substitution in the reproduction mean, but it is not proved by ELVES. The exact coupling to adaptive crashes, tranche timing, and the paper's stronger committee-size concentration bounds should be checked by the ELVES authors. +\paragraph{The ELVES branching substitution is an extension.} +Replacing the original independently honest corrective share by the fault-specific independently correct share $h_x$ is analytically transparent, but it is outside the assumptions under which the published ELVES result was derived. Its interpretation therefore requires review by the ELVES authors. -\subsection{The verdict analysis assumes enough judgments become available} +\paragraph{The pessimistic branching process is not an exact protocol simulator.} +The reproduction number and extinction expressions are inherited from a branching approximation. They identify structural thresholds under that approximation; they do not constitute an exact JAM attack probability. -The finite-population verdict conditions in \Cref{sec:attribution} concern which signed judgment compositions can be assembled. If too many validators are offline, a verdict may fail to reach \(K\) total judgments at all. That is a distinct liveness failure. +\paragraph{Fault domains are not equivalent to client labels.} +Two validators running the same nominal client may differ in version, dependencies, configuration, hardware, or execution environment. Conversely, nominally different clients may share libraries, compilers, specifications, or conceptual defects. The relevant object is fault-specific correlated response, not a client-name count. -\subsection{What does the staking layer do with wonky?} +\paragraph{The slow maintenance state is declared rather than protocol-native.} +The variables $C_t$, $O_t$, and $R_t$ and coefficients $r_C,r_O,r_R,k_{CO},k_{OR},k_{RC}$ are analytical state variables introduced to expose a cross-audit maintenance question. They are not claimed to be Gray Paper state variables, and the paper does not currently estimate them from a JAM deployment or testnet. -This is the highest-priority clarification. +\paragraph{The recurrent product threshold is not claimed as new mathematics.} +The three-process replacement inequality is a finite positive-systems/reproduction-number structure. The contribution claimed here is its explicit separation from the event-level ELVES correction condition and the resulting JAM-facing systems question, not the product threshold itself. -The Gray Paper records wonky reports in a dedicated set and removes non-positive reports from the availability path. Its ordinary culprit/fault rules refer to good or bad reports, and its punish set is populated by those offense extrinsics. However, the chain's validator rewards and higher-level economic policy are delegated. +\paragraph{The dynamic return theorem is local.} +The equivalence +\[ +\lambda_{t+1}\ge1 +\iff +Fk_{RC}R_t\ge1-r_C +\] +is proved at current criticality under the declared one-step state update. It is not a general stability theorem for the full three-dimensional maintenance system, nor does it establish that the system converges to a particular equilibrium. -Therefore the paper's narrow claim is: -\begin{quote} -A wonky verdict does not create the ordinary Gray-Paper culprit/fault offender record. -\end{quote} -It does \emph{not} follow that a production staking system must impose zero cost. If the staking layer explicitly penalizes guarantors or judges associated with wonky, the economic attribution gap narrows. +\paragraph{The reduced multiplier is diagnostic, not calibrated.} +The reduced path $\lambda_t=m^t\lambda_0$ is used to prove that current reproduction alone does not identify finite-horizon resilience. The witness $m=9/10$ is deliberately transparent and is not an estimate of JAM attrition, client turnover, or any protocol parameter. A deployment forecast would require empirical identification of the slow dynamics and uncertainty around them. -\subsection{The one-vote finite-population gap} +\paragraph{Current supercriticality is not equivalent to guaranteed audit success.} +The condition $\lambda_x>1$ is a supercritical branching condition in the declared ELVES extension. The paper does not equate it with certainty of correct resolution for a particular audit, and the dynamic sections therefore discuss preservation of the reproduction condition rather than guaranteed outcomes. -At \(N=1023\), a global composition of 682 positive and 341 negative judgments does not appear to contain a valid 683-judgment subset with any of the three permitted positive counts \(683\), \(341\), or \(0\). This may be resolved elsewhere in the intended protocol semantics, or it may be an unreachable/irrelevant edge case under assumptions not represented in our abstraction. It should be confirmed rather than silently approximated by the continuous \(2/3\) boundary. +\paragraph{Client-diversity incentives do not automatically close the maintenance loop.} +Existing work shows that client identity can in principle be made verifiable and minority implementations can be differentially rewarded. Such mechanisms may instantiate part of the observability/resource-return pathway, but this paper does not assume that they are sufficient to maintain fault-specific independent corrective capacity. That sufficiency is itself an empirical systems question. -\subsection{Strategic entry is not established} +\paragraph{Protocol and ecosystem boundaries remain partly delegated.} +Operator economics, staking consequences, implementation development, software maintenance and deployment choices span layers beyond execution auditing. The model deliberately exposes this boundary rather than attributing every slow-loop coefficient to the JAM protocol itself. -The probability that at least two of three guarantors share a fault does not imply an attacker can freely choose such a core. Strategic exploitation requires a mapping from attacker-controlled work submission to core assignment and timing. The manuscript therefore separates: -\begin{itemize} -\item \emph{accidental correlated failure}, where assignment probabilities enter the event probability; and -\item \emph{strategic exploitation}, where an attacker conditions on known favorable assignments only if the protocol gives it sufficient choice. -\end{itemize} - -\subsection{Client identity is not fault identity} - -A client-diversity rule can miss shared dependencies and can be gamed when identity is self-declared. Conversely, two versions of the same client might not share a particular bug. The model's fundamental variable is fault-domain membership, which is generally latent until a fault is discovered. - -\subsection{Questions to send with the paper} - -We would ask the ELVES and JAM authors five concrete questions: -\begin{enumerate}[label=Q\arabic*.] -\item Is replacing the honest offspring share \((1-\gamma)\) by a fault-specific independently correct share \(h_x\) valid under the ELVES adaptive-crash proof, or does another part of the proof change? -\item Under the current JAM dispute semantics, is our reading correct that a wonky verdict creates no culprit/fault offender records? Does the intended staking layer nevertheless act on the wonky set? -\item Is the \(N=1023\), 682-positive/341-negative verdict composition handled by another rule, or is the literal three-count verdict restriction intentional? -\item When validator count changes while the 341-core constant remains fixed, is the expected initial audit count per report intended to scale as \(10N/341\) once all cores are active? -\item Are implementation/fault-domain diversity constraints considered anywhere in guarantor assignment, validator selection, or staking beyond the ecosystem-level encouragement of multiple clients? -\end{enumerate} - -A negative answer to any of these can change the conclusions. That is precisely why the results are presented as a reviewable extension rather than a vulnerability claim. +These limitations are not secondary caveats. They define the intended claim hierarchy: direct Gray Paper verdict arithmetic first; ELVES-based fault-domain extension second; recurrent-maintenance and dynamic-resilience models third; empirical grounding and protocol design conclusions only after those mappings survive expert review and measurement. diff --git a/papers/correlated-honest-failure/sections/08_conclusion.tex b/papers/correlated-honest-failure/sections/08_conclusion.tex index e2b2581..6c3e769 100644 --- a/papers/correlated-honest-failure/sections/08_conclusion.tex +++ b/papers/correlated-honest-failure/sections/08_conclusion.tex @@ -1,8 +1,8 @@ \section{Discussion and conclusion} -The standard honest/adversarial partition is sufficient only when “honest” also means “independently correct for the fault being exploited.” Correlated implementation failure separates those concepts. +The standard honest/adversarial partition is sufficient only when ``honest'' also means ``independently correct for the fault being exploited.'' Correlated implementation failure separates those concepts. -The resulting JAM/ELVES analysis has three nested boundaries. +The resulting JAM/ELVES analysis has three nested event-level boundaries, an orthogonal cross-time maintenance condition, and a dynamic bridge between them. First, the dispute layer has an attribution boundary. If the combined adversarial-plus-buggy-positive bloc exceeds roughly one third of the validator population, independently correct validators no longer suffice by themselves to construct a bad verdict. The report can still be stopped through a wonky outcome, but the ordinary Gray Paper offender-attribution path changes. This is a protocol-rule result, not a branching-model result. @@ -18,19 +18,75 @@ \section{Discussion and conclusion} \] validator growth can reduce corrective reproduction when new validators do not increase the independently correct set for the relevant fault. This can occur even if every entrant is honest and the adversarial fraction falls. -Together these results suggest that a useful security variable is not raw validator count or raw client count but fault-specific independent corrective capacity. Because future faults are unknown, operators cannot observe that capacity directly. They can only monitor exposure to plausible common components and preserve diversity margins across multiple layers. +Fourth, event-level correction is not the same as preserving the capacity to remain corrective across future audits. The declared slow maintenance model separates independently corrective capacity, maintenance observability or attribution, and returned resources. Its canonical three-cycle threshold is +\[ +k_{CO}k_{OR}k_{RC}\ge(1-r_C)(1-r_O)(1-r_R). +\] +Machine-checked counterexamples show that this maintenance condition and \(\lambda_x>1\) imply neither one another. The maintenance condition should therefore not be read as a fourth point on the earlier one-third/one-half/two-thirds sequence. It is an orthogonal timescale. -The most concise summary is therefore: +Fifth, once the slow corrective-capacity state is allowed to feed the next audit, the separation becomes a dynamic resilience condition. Under +\[ +C_{t+1}=r_CC_t+k_{RC}R_t, +\qquad +\lambda_{x,t}=FC_t, +\] +we obtain +\[ +\lambda_{x,t+1}=r_C\lambda_{x,t}+Fk_{RC}R_t. +\] +At current criticality this gives the exact machine-checked boundary +\[ +\boxed{ +\lambda_{x,t+1}\ge1 +\quad\Longleftrightarrow\quad +Fk_{RC}R_t\ge1-r_C. +} +\] +The difference +\[ +M_t=Fk_{RC}R_t-(1-r_C) +\] +is therefore a candidate local maintenance-return margin: its sign tells whether a currently critical corrective state crosses below, stays at, or moves above the fast audit threshold on the next slow update. + +The full-state result is stronger than this local boundary. For the canonical maintenance state +\[ +C^*=(1-r_O)(1-r_R),\qquad +O^*=k_{CO}(1-r_R),\qquad +R^*=k_{CO}k_{OR}, +\] +the same product threshold makes the coordinatewise cone above $(C^*,O^*,R^*)$ forward invariant under nonnegative retention and coupling coefficients. Hence, if +\[ +FC^*>1, +\] +then the canonical slow trajectory remains audit-supercritical at every future cross-audit time. The model therefore contains both an erosion mechanism and an explicit persistence region: insufficient return can push correction below threshold, while a sufficiently closed maintenance loop can preserve correction indefinitely. + +This dynamic bridge exposes a stronger failure mode than static insufficiency. A system can remain on the supercritical side of its current audit condition while its corrective margin is decaying toward subcriticality. The Lean formalization demonstrates this by constructing two systems with the same current \(\lambda_0=3/2\) but opposite five-step threshold status under different reduced maintenance multipliers; it also proves generally that any nonnegative reduced multiplier below one eventually crosses the fast threshold. Current audit reproduction is therefore not, within the declared model, a sufficient statistic for finite-horizon corrective resilience. + +Together these results suggest that the relevant security object is not raw validator count, raw client count, or even current \(\lambda_x\) alone. It is a pair consisting of fault-specific independent corrective capacity and the maintenance dynamics that replenish or erode that capacity. Because future faults are unknown, this object cannot be observed perfectly. But implementation exposure, useful audit effort, client/operator turnover, diversity-aware rewards, development resources and other return flows can in principle provide measurable proxies. + +The most concise hierarchy is therefore: \[ \boxed{ \text{honest stake} \neq \text{independently corrective stake} \neq -\text{attacker-attributable stake}. +\text{attacker-attributable stake}, } \] +followed by +\[ +\boxed{ +\text{corrective reproduction now} +\neq +\text{reproduction of corrective capacity over time} +\neq +\text{finite-horizon corrective resilience}. +} +\] + +The first distinction matters for auditing and economics. The second separates an event-level success condition from a cross-time maintenance condition. The third makes that maintenance condition operational by asking whether the observed return flows are sufficient to keep the fast corrective threshold from being crossed in the future. -The first inequality matters for auditing. The second matters for economics. The Gray Paper and ELVES already provide a strong framework for reasoning about adversarial and availability failures; correlated honest failure asks where shared implementation dependencies enter that framework. +This also clarifies the relationship to existing client-diversity and resilience work. Dynamic compliance, decentralization incentives, software rejuvenation and diversity-aware rewards all address parts of the broader problem. The narrower contribution here is to connect fault-specific sampled-audit reproduction to a separately maintained corrective-capacity state, derive the exact return-gap boundary, and prove both loss and persistence of fast correction under declared slow dynamics. -The immediate next step is not another model extension. It is review by the ELVES and JAM authors, especially on the wonky-verdict economics and the substitution of \(h_x\) into the branching proof. If those mappings are accepted, fault-domain exposure becomes a quantitatively defined protocol margin rather than only a qualitative argument for client diversity. If they are rejected, the reasons will identify exactly which additional mechanism closes the gap. +External review by the ELVES and JAM authors remains essential, especially on the wonky-verdict economics, the substitution of \(h_x\) into the branching proof, and the mapping from protocol/ecosystem mechanisms to the declared slow state. The strongest next empirical test is correspondingly concrete: determine whether a JAM deployment or testnet can estimate both a current fault-domain correction margin and an independent maintenance-return margin, then test whether the latter predicts changes in the former before event-level correction becomes subcritical.