Distributed Commons Control

How can a network maintain shared state without requiring a central controller or perfectly reliable nodes?

This repository develops a minimal, executable and formally checked theory of distributed control of a commons. Here a commons is not assumed to be external truth or a morally good resource. It is a jointly produced or maintained state whose condition changes the future capabilities of multiple participants.

The initial test case is a small computation protocol:

[ \text{producer} \longrightarrow \text{distributed monitors} \longrightarrow \text{commit to shared state}. ]

A producer can obtain a local benefit from proposing harmful work. Monitoring is costly. Monitors can fail independently or through a correlated blind spot. The network declares a maximum acceptable probability of harmful finalization. This lets us distinguish:

[ \boxed{\text{locally selected control} \neq \text{control sufficient for the commons}}. ]

The project was prompted by the architecture of the Join-Accumulate Machine (JAM) and by the broader Evolution by Emergence programme. It is not an implementation, security audit or official analysis of JAM. JAM is used first as an engineered system in which proposal, checking, availability and commitment are explicit enough to study. Ecological interpretations are treated as hypotheses to be earned after the generic model works.

Baseline exact result: correlated capture floor

Let (b) be the probability that harmful work is attempted, (q) each monitor's detection effort, (n) the number of monitors and (\rho) the probability of a common-mode blind spot. The probability that harmful work escapes all monitors is

[ E_n(q,\rho)=\rho+(1-\rho)(1-q)^n, ]

so the harmful-finalization probability is (P_{\mathrm{bad}}=bE_n(q,\rho)). Even perfect individual effort leaves

[ P_{\mathrm{bad}}(q=1)=b\rho. ]

Therefore a safety target (\varepsilon<b\rho) is structurally unattainable by adding effort or same-mode monitors. The architecture must reduce correlated failure. This is a useful calibration of the model, not a novelty claim: common-cause limits on redundancy are established in reliability engineering and in work on dependent failures in multiversion software. See the prior-art boundary.

The first coupled extension goes one step further. Because the common-mode branch also caps collective detection at (1-\rho), the adaptive producer response cannot drive the harmful-attempt target below

[ m(\rho)=\sigma!\left(\frac{g-\ell(1-\rho)}{T}\right). ]

For producer adjustment (0<\alpha_b\le1),

[ \boxed{b_t\ge m+(1-\alpha_b)^t(b_0-m)} ]

and hence (\liminf P_{\mathrm{bad},t}\ge\rho m). This turns the static floor into an endogenous floor: common-mode weakness changes the producer response that determines the floor itself. The finite-time theorem is machine-checked in formalization/EndogenousFloor.lean.

JAM / ELVES correlated honest failure

The current protocol-facing result of the repository is the technical paper papers/correlated-honest-failure/:

Correlated Honest Failure in JAM/ELVES: Fault-Domain Concentration, Sampling Dilution, and Attribution Boundaries

The paper asks what changes when a validator is honest in the protocol/game-theoretic sense but shares an implementation fault that makes one particular invalid report look valid. The relevant quantity is therefore not raw client count but fault-specific independently corrective capacity.

Three results are kept separate because they rely on different assumptions.

1. Gray Paper verdict-attribution boundary

Let (N) be the validator set used for a verdict and

[ K=\left\lfloor\frac{2N}{3}\right\rfloor+1. ]

For one fault (x), split validators into adversarial (A), otherwise-honest but buggy-positive (B_x), and independently correct (C_x=N-A-B_x). A bad verdict remains constructible regardless of adversarial voting iff

[ \boxed{C_x\ge K.} ]

In large-population share notation, with adversarial share (\gamma) and fault-domain share (f_x) among otherwise-honest validators,

[ \boxed{ \gamma+(1-\gamma)f_x<\frac13. } ]

This is a consequence of the current Gray Paper verdict rules plus the declared correlated-fault scenario; it does not depend on the ELVES adaptive-crash model.

2. Fault-specific ELVES escalation

Extending ELVES so that only independently correct validators contribute useful corrective offspring gives

[ \boxed{ \lambda_x

F\frac{C_x}{N}

F(1-\gamma)(1-f_x). } ]

Supercritical correction requires (\lambda_x>1), hence

[ \boxed{ f_x < 1-\frac{1}{(1-\gamma)F}. } ]

For JAM's current (F=2), the large-population wrong-positive boundaries are

[ \boxed{ \frac13;\text{(robust bad-verdict attribution)} < \frac12;\text{(audit escalation)} < \frac23;\text{(false-good eligibility)}. } ]

The branching result is an extension of ELVES, not an ELVES theorem, and is explicitly presented for review by the ELVES/JAM authors.

3. Sampling dilution

The count form

[ \lambda_x=F\frac{C_x}{N} ]

also shows that sampled correction is not structurally monotone under all honest additions. Holding the independently correct count (C_x) fixed, adding honest validators that share the same fault increases (N) and strictly lowers (\lambda_x). No behavioral response is required.

The paper reports both:

• a fixed initial-sample case, which isolates dilution; and
• a fixed-341-core JAM case, where the expected initial sample grows with the validator population and partly offsets, but does not remove, the effect in the reported parameter slice.

This is why claim C22 is now explicitly scoped to the earlier all-participant structural model rather than sampled/capacity-limited correction.

Economic and engineering boundary

The paper also separates

[ \boxed{ \text{honest stake} \neq \text{independently corrective stake} \neq \text{attacker-attributable stake}. } ]

A shared bug can make honest guarantors or judges sign the wrong result. The Gray Paper can therefore still reject a report while ordinary culprit/fault attribution changes. In particular, a wonky verdict stops the report but does not, through the current culprit/fault paths, create the ordinary offender record. Whether an external staking layer separately penalizes wonky outcomes is intentionally left as an open protocol question.

Guarantor diversity, fault-domain exposure metrics, announcement shortfall, audit-effort observability and load-dependent no-shows are treated as design questions and future tests, not as established fixes.

The protocol-specific assumptions and exact finite-(N) verdict derivation are documented in docs/JAM_GROUNDING.md, and the full claim-status boundary is maintained in CLAIMS.md.

Repository map

Path	Purpose
docs/MODEL.md	Assumptions, equations, phase boundaries and dynamic extension
docs/PHASE_BOUNDARY.md	Complete piecewise phase theorem and critical-cost boundary
docs/PRIOR_ART.md	Prior-art calibration and current novelty boundary
docs/CLOSED_LOOP.md	Experiment 2: closed commons loop, folds, hysteresis and recovery basins
docs/VIABILITY_CONTRIBUTION.md	Experiment 3: neutral participant contribution to a declared viability margin
docs/SELECTED_VIABILITY.md	Experiment 4: direct-positive but selected-negative participant contribution
docs/CORRECTIVE_CAPACITY.md	Experiment 5: current shared state versus slow corrective capacity
docs/STATE_DEPENDENT_CONTRIBUTION.md	Experiment 6: participant contribution to access of stored capacity
docs/VECTOR_CONTRIBUTION.md	Experiment 7: vector-valued contribution across viability loops
docs/BEHAVIORAL_MAINTENANCE.md	Experiment 8: behavioral maintenance operators and falsification boundaries
docs/JAM_MAINTENANCE_OPERATORS.md	Experiment 9: grounded JAM operator audit and viability-vector perturbations
docs/JAM_BEHAVIOR_SELECTION.md	Experiment 10: partially identified compute/rubber-stamp/no-show selection boundaries
docs/JAM_EFFORT_OBSERVABILITY.md	Experiment 11: maintenance observability and return-loop closure
docs/FUNGAL_FLOW_MAINTENANCE.md	Experiment 12: fungal flow-coupled maintenance and redundancy boundary
docs/VIABILITY_OUGHT.md	Cross-substrate synthesis: viability-conditioned ought, prior-art boundary, and falsifiers
papers/correlated-honest-failure/	Technical paper: correlated honest failure, verdict attribution, ELVES escalation and sampling dilution
CLAIMS.md	Claim ledger separating proofs, computations and hypotheses
src/distributed_commons/	Dependency-free executable model
scripts/run_experiment.py	Reproducible parameter sweep
tests/	Numerical and behavioral tests
formalization/	Lean 4 formalization and proof map
docs/JAM_MAPPING.md	Restricted mapping from the generic model to JAM concepts
docs/ECOLOGY_MAPPING.md	Ecological translation and its inferential limits
docs/ROADMAP.md	Staged research programme

Run the model

Python 3.10 or later is sufficient; the model has no runtime dependencies.

python -m pip install -e .
python -m unittest discover -s tests -v
python scripts/run_experiment.py --output results/phase_sweep.csv
python scripts/phase_boundary.py --output results/static_phase_boundary.csv

To compile the formalization:

cd formalization
lake update
lake exe cache get
lake build

The same checks run in GitHub Actions. The real-root formula is now connected end-to-end to actual safety by RootSafety.lean, including construction, uniqueness and leastness; see the verification record.

Complete phase boundary

In the non-trivial attainable region (b\rho\le\varepsilon<b), selected monitoring is sufficient exactly when

[ \frac{b(1-\rho)r}{c} \ge 1-\left(\frac{\varepsilon/b-\rho}{1-\rho}\right)^{1/n}. ]

Equivalently, (c\le c_{crit}=b(1-\rho)r/q_{suff}). Increasing correlation therefore creates a double squeeze: it raises sufficient effort while lowering the private return to supplying it. The full derivation states all boundary cases.

Closed-loop commons control

The next experiment closes the return path that was missing from the original adaptive model: commons condition now changes future control. Under commons-funded monitoring, the reduced equilibrium branch develops a fold and a coexistence region with both a healthy attractor and the clipped collapsed state. The same topology also appears in two alternative closures where degradation raises checking cost or capture gain.

For the declared discrete-time linear-regeneration map, the local equilibrium multiplier can be written

[ M=1-\gamma+\gamma\eta, \qquad \eta=-(1-X)\frac{d\ln P^*}{dX}, ]

so local linear stability is equivalent to (\eta<1). The algebraic equivalence is machine-checked in formalization/ClosedLoopStability.lean; concrete fold locations remain numerical. See Experiment 2.

Participant contribution to viability

Experiment 3 moves from anonymous same-mode monitors to heterogeneous participants with different failure profiles. For a coalition (S), define (pi(S)) as the probability that every participant is disabled, and define the viability margin

[ M(S)=sup{bin[0,1]:bpi(S)le�arepsilon}. ]

The first exact example has two participants sharing failure cause (A) and a third participant vulnerable only to independent cause (B). Adding the third participant changes structural escape from ( ho) to ( ho^2), and in the uncapped regime multiplies the viability margin by (1/ ho). At ( ho=0.05), that is a twentyfold increase.

The model is deliberately substrate-neutral. Leave-one-out contribution, Shapley attribution and higher-order interaction terms are all computed from the same declared margin; no participant is assigned a globally positive or negative role. See Experiment 3.

Scientific boundary

The current model proves conditional statements about a declared toy architecture. It does not establish that consensus equals truth about the external world, every persistent organism benefits its ecosystem, ecosystems optimize a global objective, JAM currently violates a safety or liveness requirement, or economic incentives alone guarantee protocol viability.

Those stronger statements require additional theory or evidence. The purpose of the repository is to make the boundary between result and interpretation inspectable.

Relationship to Evolution by Emergence

This project is an out-of-domain test of the abstractions developed in Evolution by Emergence, especially sufficient alignment, selected-versus-sufficient control and maintenance debt. Its contribution must be more than vocabulary transfer: the distributed-computation substrate must yield new, testable phase structure. The common-mode capture floor is treated as a known calibration result; the endogenous producer-floor result is the first coupled phase constraint produced by the adaptive model. The repository does not yet claim literature priority for that theorem.

Licensing

Code and Lean sources are licensed under Apache-2.0. Research text and documentation are licensed under CC BY 4.0; see LICENSES.md.