This ledger prevents mathematical results, simulation behavior and cross-domain interpretations from being reported as the same kind of evidence.
| ID | Claim | Status | Evidence |
|---|---|---|---|
| C1 | In the declared common-mode mixture, conditional escape is (E_n=\rho+(1-\rho)(1-q)^n). | Model definition | model.py; DistributedCommons.lean for arbitrary n |
| C2 | For every positive monitor count, perfect effort leaves harmful-finalization probability (b\rho). | Exact theorem | Lean: badFinalizationN_perfect |
| C3 | For arbitrary monitor count and admissible effort, (b\rho) is a lower bound on harmful finalization. | Exact theorem | Lean: badFinalizationN_correlation_floor |
| C4 | For arbitrary monitor count, a target (\varepsilon<b\rho) is unattainable within this architecture. | Exact theorem | Lean: safety_impossible_below_correlation_floor_N |
| C5 | When the target is attainable, the minimum symmetric effort is (1-((\varepsilon/b-\rho)/(1-\rho))^{1/n}). | Exact real-root theorem; machine checked | Lean: safety_iff_sufficientEffortN; Python regression tests |
| C6 | With private objective (b(1-\rho)rq-cq^2/2), selected effort is (b(1-\rho)r/c) before clipping to the feasible interval. | Exact theorem for the unconstrained quadratic | Lean: selectedEffort_global_max |
| C7 | Selected monitoring meets a declared effort requirement iff (cq_{req}\le b(1-\rho)r), for (c>0). | Exact theorem | Lean: selectedEffort_meets_requirement_iff |
| C8 | Higher common-mode correlation can produce lower long-run commons health in the declared adaptive simulation. | Computational result, parameter dependent | Parameter sweep and tests |
| C9 | Verification debt can precede visible commons collapse. | Hypothesis instantiated by one bookkeeping definition | Dynamic model; requires robustness analysis |
| C10 | JAM can be analyzed as distributed maintenance of protocol-valid shared state. | Structural interpretation | docs/JAM_MAPPING.md |
| C11 | Ecological roles can sometimes be represented as positions in distributed feedback loops. | Research hypothesis, not established here | docs/ECOLOGY_MAPPING.md |
| C12 | In the non-trivial attainable region, clipped selected effort is sufficient iff (c\le b(1-\rho)r/q_{suff}). | Exact theorem | Python classifier; Lean: selected_safety_iff_critical_cost |
| C13 | Correlation simultaneously raises required effort and lowers detection-contingent private return in the declared model. | Exact comparative result from the model equations; numerically tested | docs/PHASE_BOUNDARY.md; test_correlation_double_squeeze |
| C14 | In the adaptive producer model, the common-mode detection cap creates an endogenous producer-target floor (m=\sigma((g-\ell(1-\rho))/T)). For partial adjustment (0<\alpha\le1), the attempt rate obeys (b_t\ge m+(1-\alpha)^t(b_0-m)), so (\liminf b_t\ge m); combined with the common-mode floor this gives (\liminf P_{bad,t}\ge\rho m). | Exact finite-time theorem for any antitone producer response; logistic specialization and asymptotic corollary | Lean: EndogenousFloor.lean; Python: producer-floor regression tests |
| C15 | For the declared reduced discrete-time commons map with linear regeneration, positive nonincreasing (P^*(X)), and (0<\gamma\le1), the local multiplier satisfies (M=1-\gamma+\gamma\eta), so ( | M | <1) iff (\eta<1), where (\eta=-(1-X)d\ln P^*/dX). |
| C16 | With reward closure (r(X)=r_0(\kappa+X)), the declared reduced model has a fold and a healthy/collapsed coexistence window for baseline parameters; the window narrows with (\kappa) and disappears near (\kappa_c\approx1.221). | Computational result for declared parameters; reduced model plus finite-adjustment check | closed_loop.py; closed_loop_experiment.py; closed-loop tests |
| C17 | Recovery depends on monitor mobilisation as well as commons health: with detection-funded monitors initialized at their private optimum, quiet histories require substantially more initial commons health to recover than high-attack histories in the reported runs. | Computational result, parameter dependent | docs/CLOSED_LOOP.md §5; basin tests |
| C18 | In the reward-funded closure at (\kappa=0.05), increasing common-mode correlation from 0 to 0.3 lowers the computed fold-damage threshold by about a factor of three. | Computational observation at one parameter slice | docs/CLOSED_LOOP.md §4.2 |
| C19 | The fold and bistability are not specific to reward funding: they also occur in the tested alternative closures where degraded commons health raises checking cost exponentially or raises capture gain. | Computational cross-closure robustness result | docs/CLOSED_LOOP.md §6; alternative-closure tests |
| C20 | In the two-cause heterogeneous-participant model, adding a participant with an independent failure profile changes structural escape from (\rho) to (\rho^2); in the uncapped viability-margin regime this multiplies the margin by (1/\rho). | Exact theorem; machine checked | Lean: ViabilityContribution.lean; Python exact-topology tests |
| C21 | Leave-one-out, Shapley and Harsanyi attribution answer different questions on the same viability-margin set function: Shapley values exhaust the total margin gain by construction, while higher-order Harsanyi terms retain non-additive interactions explicitly. | Established attribution identities instantiated in the model | viability.py; docs/VIABILITY_CONTRIBUTION.md; tests |
| C22 | In the one-loop all-participant structural viability model, adding participants cannot reduce the viability margin: if (S\subseteq T), then (\pi(T)\le\pi(S)) and hence (M(T)\ge M(S)). This monotonicity does not apply automatically when correction access is sampled or capacity-limited. | Exact set-event consequence within the declared all-participant architecture; exhaustively tested on declared examples | viability.py; test_adding_participant_never_reduces_structural_margin; docs/VIABILITY_CONTRIBUTION.md |
| C23 | ELVES converts collateral assumptions into a soundness target: with (C=\nu M/n), rational-adversary soundness requires (1/\varepsilon>n/\nu+1), so the strict boundary is (\varepsilon_*=\nu/(n+\nu)). | External theorem / substrate grounding, not a repository novelty claim | ELVES Corollary 1; jam_elves.py; docs/JAM_GROUNDING.md |
| C24 | In the repository's shared-client extension of ELVES, effective honest escalation is (\lambda_f=(1-\gamma)(1-f)s_\delta), losing supercriticality at (f=1-1/((1-\gamma)s_\delta)). | Exact consequence of declared extension; outside ELVES assumptions | jam_elves.py; tests; docs/JAM_GROUNDING.md |
| C25 | The shared-client extension yields an invertible client-share margin (f_{max}) for a target (\varepsilon). With (s_0=30,s_\delta=2,n=1023,\nu=0.05), the pessimistic bound does not certify the target even at (f=0) at the (\gamma\to1/3) boundary, while (f_{max}\approx0.146) at (\gamma=0.2) and (0.280) at (\gamma=0.05). | Computational specialization of exact branching inversion; extension, not ELVES theorem | jam_elves.py; test_jam_elves.py; docs/JAM_GROUNDING.md |
| C26 | In the neutral two-participant shared-reward game, adding a second participant at frozen incumbent effort has positive direct contribution (bz(1-z)) for (0<z<1), but after symmetric re-equilibration the selected contribution is negative whenever (z^2+4z-4>0). | Exact theorem; machine checked | Lean: SelectedViability.lean; Python tests; docs/SELECTED_VIABILITY.md |
| C27 | The sign reversal occurs at (z_c=2(sqrt2-1)approx0.828427). Equivalently, in target space (x=�arepsilon/b), the two-participant selected system has lower critical-cost tolerance than the one-participant system when (x<(sqrt2-1)^2approx0.171573). | Exact algebraic consequence; polynomial form machine checked, square-root specialization executable | selected_viability.py; docs/SELECTED_VIABILITY.md |
| C28 | In the neutral two-state capacity model, the finite-shock viability condition (V\le X-s+\kappa C) is equivalent to (s\le M(X,C)=X-V+\kappa C). | Exact theorem; machine checked | Lean: CorrectiveCapacity.lean; Python boundary tests; docs/CORRECTIVE_CAPACITY.md |
| C29 | At fixed shared state, higher corrective capacity raises shock margin by exactly (\kappa\Delta C). At the quiet fixed point (X=1), zero-maintenance capacity decay changes the margin by (-\kappa\delta C) while the shared state remains exactly 1. | Exact theorem; machine checked | Lean: CorrectiveCapacity.lean; quiet-capacity tests |
| C30 | Two systems can have identical current shared state and identical local shared-state recovery multiplier but different finite-shock viability because their capacity stocks differ. | Exact consequence of C28-C29; executable counterexample | corrective_capacity.py; docs/CORRECTIVE_CAPACITY.md |
| C31 | If coalition all-disabled probability changes from (\pi_{before}) to (\pi_{after}), expected finite-shock margin changes by exactly (\kappa C(\pi_{before}-\pi_{after})). | Exact theorem; machine checked | Lean: StateDependentContribution.lean; Python tests; docs/STATE_DEPENDENT_CONTRIBUTION.md |
| C32 | In the two-independent-cause example, the independent-profile participant contributes (\kappa C\rho(1-\rho)) through access to stored corrective capacity; this contribution is zero at (C=0) and scales linearly with the capacity state. | Exact theorem and specialization | Lean: independent_profile_capacity_contribution; Python state-scaling tests |
| C33 | Under quiet multiplicative capacity decay, the same topology-based participant contribution shrinks by exactly the surviving capacity fraction ((1-\delta)). | Exact theorem; machine checked | Lean: quiet_decay_scales_access_contribution; Python quiet-decay test |
| C34 | If a participant has positive contribution (a>0) to one declared viability loop and negative contribution (b<0) to another, then positive scalarization weights exist that make the same contribution vector net-positive, and other positive weights make it net-negative. | Exact theorem; machine checked | Lean: VectorContribution.lean; Python witness tests; docs/VECTOR_CONTRIBUTION.md |
| C35 | Therefore a scalar global sign is not intrinsic to a mixed-sign multi-loop contribution vector; any scalar net contribution requires an explicit weighting/aggregation rule. | Exact consequence of C34; interpretation of the vector representation | vector_contribution.py; docs/VECTOR_CONTRIBUTION.md |
| C36 | At a maintenance-dependent viability boundary (V), one-step persistence is equivalent to closing replacement: (V\le(1-\delta)V+e+m\iff \delta V\le e+m). | Exact theorem; machine checked | Lean: BehavioralMaintenance.lean; Python boundary tests; docs/BEHAVIORAL_MAINTENANCE.md |
| C37 | Active participant maintenance is not universally necessary: if passive renewal satisfies (e\ge\delta V), the boundary can persist with (m=0). When (e<\delta V), any boundary-preserving participant maintenance must satisfy (m\ge\delta V-e). | Exact theorem pair; falsifies universal-maintenance claim | Lean: passive_renewal_can_suffice, participant_maintenance_must_close_gap |
| C38 | In the local deficit-correction model, multiplier is (1-\delta-g); if (\delta+g>2), it is below (-1), so increasing corrective gain past this boundary destabilizes rather than improves local maintenance. | Exact theorem; machine checked | Lean: overcorrection_multiplier_lt_neg_one; Python stability sweep |
| C39 | Under symmetric sign-flip signal noise, expected corrective gain is ((2p-1)g); for (g>0,p<1/2), nominal correction reverses sign in expectation. | Exact theorem; machine checked | Lean: low_fidelity_reverses_correction; Python tests |
| C40 | Positive reinforcement of positively signalled processes is not unconditionally beneficial: its sign depends on (hpa-(1-h)(1-p)b), and can be negative when misclassified harm dominates correctly identified benefit. | Exact algebraic condition; harmful region machine checked | Lean: reinforcement_can_be_harmful; Python tests |
| C41 | Repair is conditional: nonnegative repair value is exactly equivalent to (C_R\le r(V-W)). | Exact theorem, reproducing sufficient-alignment repair condition | Lean: repair_nonnegative_iff; docs/BEHAVIORAL_MAINTENANCE.md |
| C42 | In the count-based JAM shared-client extension, moving one otherwise-honest validator from a vulnerable client profile to an independent/correct profile raises effective correction reproduction by exactly (s_\delta/n). | Exact substrate-specific identity; machine checked | Lean: one_validator_diversification_gain; Python fixed-count tests; docs/JAM_MAINTENANCE_OPERATORS.md |
| C43 | In the count-based no-show/scalability model, making one validator-equivalent reliable raises the scalability margin (1-A) by exactly (s_\delta/n). | Exact substrate-specific identity; machine checked | Lean: one_validator_reliability_gain; Python tests |
| C44 | Increasing JAM/ELVES escalation strength (s_\delta) raises correction reproduction when useful honest correctors remain, but lowers the no-show scalability margin when the no-show-prone count is positive. | Exact mixed-sign substrate result; machine checked | Lean: escalation_improves_correction, escalation_harms_scalability; numerical branching-bound experiment |
| C45 | In the declared integer-count slice (n=1023,H=818,B=119,s_0=30,s_\delta=2,\nu=0.05), moving one validator to an independent/correct client changes the pessimistic ELVES-extension safety log margin from about (-0.0132) to (+0.0350), crossing the certification boundary. | Computational specialization of grounded extension; parameter dependent | jam_maintenance.py; tests; docs/JAM_MAINTENANCE_OPERATORS.md |
| C46 | The audited JAM/ELVES maintenance architecture does not co-locate all Experiment-8 operators: sensing/correction are implemented in the core assurance path, while reinforcement/funding, resource reproduction and protocol revision are partly delegated or outside that layer. | Grounded architectural classification, not theorem | docs/JAM_MAINTENANCE_OPERATORS.md; docs/JAM_MAPPING.md; docs/JAM_GROUNDING.md |
| C47 | In the partially identified JAM audit game, actual compute weakly dominates rubber-stamping iff (R_C-R_R+bdL_F\ge c), and weakly dominates no-show iff (R_C-R_N\ge c). | Exact payoff identities; machine checked; reward magnitudes not supplied by JAM core | Lean: compute_dominates_rubber_iff, compute_dominates_noshow_iff; docs/JAM_BEHAVIOR_SELECTION.md |
| C48 | The minimum compute reward advantage over rubber-stamping is (c-bdL_F); lower false-positive exposure probability (d) strictly raises this requirement when (b,L_F>0). | Exact monotonic design-boundary result; machine checked | Lean: lower_exposure_raises_required_advantage; Python tests |
| C49 | If invalid reports are rare, fault punishment may provide little expected deterrence: e.g. (c=1,b=0.001,d=1,L_F=10) still requires (R_C-R_R\ge0.99). | Computational specialization of exact boundary | jam_behavior_selection.py; tests; docs/JAM_BEHAVIOR_SELECTION.md |
| C50 | The current Gray Paper does not numerically close the audit-behavior game: validator rewards are delegated to staking, audit effort is not directly observable on-chain, and the formal validator-statistics tuple does not currently contain a finalized audit-effort statistic. | Grounding/partial-identification result, not theorem | official Gray Paper source checked at commit e5375148...; docs/JAM_BEHAVIOR_SELECTION.md |
| C51 | If effective effort observability is (s) and the higher-layer reward budget is (W), compute is selected against rubber-stamping iff (sW+bdL_F\ge c); for (W>0), the required observability is ((c-bdL_F)/W). | Exact second-order selection boundary; machine checked | Lean: observability_threshold_iff; docs/JAM_EFFORT_OBSERVABILITY.md |
| C52 | Reward without observability cannot selectively reinforce computation: at (s=0), the selection margin is (bdL_F-c), independent of reward budget (W). | Exact falsification result; machine checked | Lean: zero_observability_removes_reward_channel; Python tests |
| C53 | Perfect effort observability can still be insufficient: if (W+bdL_F<c), the compute-selection margin remains negative at (s=1). | Exact falsification result; machine checked | Lean: perfect_observability_insufficient |
| C54 | Lower false-positive exposure raises the effort-observability threshold needed to close the same maintenance return loop. | Exact cross-layer monotonicity theorem; machine checked | Lean: lower_exposure_raises_observability_threshold; Python structural-collapse test |
| C55 | In the fungal-inspired two-route return model, the equal-allocation local multiplier is (M=1-\delta+\delta\beta s); under (0<\delta\le1,\beta,s\ge0), local stability is exactly equivalent to (\beta s<1). | Exact model theorem; machine checked | Lean: fungal_stable_iff_effective_gain_lt_one; Python finite-difference and trajectory tests; docs/FUNGAL_FLOW_MAINTENANCE.md |
| C56 | Unit effective gain (\beta s=1) is locally neutral, while (\beta s>1) makes the symmetric redundant state locally unstable. | Exact model theorem; machine checked | Lean: fungal_neutral_iff_effective_gain_eq_one, fungal_unstable_iff_effective_gain_gt_one |
| C57 | For unit total route allocation, worst-case backup (B(z)=\min(z,1-z)) is maximized at equal redundancy (z=1/2). | Exact theorem; machine checked | Lean: fungal_backup_share_le_half, fungal_backup_share_at_half |
| C58 | The fungal substrate shows that a separate maintenance-observation layer is not structurally necessary: experimentally grounded flow can itself provide local information about a cord's network role while being coupled to future cord growth. | Cross-substrate interpretation grounded in Heaton et al. 2010; not a universal theorem | docs/FUNGAL_FLOW_MAINTENANCE.md; prior-art references |
| C59 | The local unit of distributed maintenance need not be an autonomous individual; in the fungal mapping it can be a cord/hyphal region or local transport/growth process. | Cross-substrate representation result | docs/FUNGAL_FLOW_MAINTENANCE.md |
| C60 | In the grounded JAM branching abstraction, if effective corrective share is (h>0) and failure-amplifying share is (u\ge0), there exists an escalation strength (s>0) with (hs>1) and (us<1) iff (u<h). A constructive feasible choice is (s=2/(h+u)). | Exact cross-substrate synthesis theorem; machine checked | Lean: jam_escalation_feasible_iff_failure_lt_correction; docs/VIABILITY_OUGHT.md |
| C61 | "Viability-conditioned ought" is used only as a conditional interpretation: given a declared viability property, model parameters/policies must lie in its admissible region for that property to persist. It is not a categorical moral theorem. | Conceptual synthesis / scope guard | docs/VIABILITY_OUGHT.md; viability-theory prior art |
| C62 | Under the current Gray Paper verdict rule, with (K=\lfloor2N/3\rfloor+1) and (W=\lfloor N/3\rfloor), a bad verdict can be assembled iff (N-P\ge K), a good verdict iff (P\ge K), and a wonky verdict iff (P\ge W) and (N-P\ge K-W), where (P) is the available positive-judgment population. | Exact consequence of Gray Paper verdict composition rules | Gray Paper text/judgments.tex; docs/JAM_GROUNDING.md; paper 1 |
| C63 | In the correlated-honest-fault extension with adversarial count (A), buggy-positive honest count (B_x), and independently correct count (C_x=N-A-B_x), a bad verdict remains constructible regardless of adversarial voting iff (C_x\ge K). In the large-(N) share form, (\gamma+(1-\gamma)f_x<1/3). | Exact extension of Gray Paper rule; asymptotic share corollary | docs/JAM_GROUNDING.md; paper 1 |
| C64 | For (N=1023), the literal Gray Paper verdict counts are (K=683), (W=341), (K-W=342): bad is possible for (P\le340), wonky for (341\le P\le681), and good for (P\ge683). The (P=682) composition is an explicit specification question. | Exact integer-count observation; interpretation requires author confirmation | docs/JAM_GROUNDING.md; paper 1 |
| C65 | Writing (C_x) for the independently correct validator count, the fault-specific ELVES extension is (\lambda_x=F C_x/N). Holding (F,C_x>0) fixed, adding validators outside (C_x) strictly lowers (\lambda_x), so sampled correction is not structurally monotone under honest-but-correlated additions. | Exact identity in the declared ELVES extension | paper 1; reproduce.py |
| C66 | In the exact-count slice (N=1023,A=205,B_x=164,C_x=654,F=2), adding 200 honest validators in the same fault domain raises the pessimistic branching bound from (4.52\times10^{-4}) to (0.130) with fixed (s_0=30), and to (0.0874) when the Gray Paper's 341 cores are held fixed so (s_0=10N/341). | Computational specialization of C65; parameter dependent | paper 1 reproduce.py |
| C67 | A wonky verdict removes the report but does not, through the current Gray Paper culprit/fault rules, create the ordinary offender records used to populate the punish set. Whether the external staking layer separately penalizes wonky is not specified in the audited layer. | Gray Paper grounding plus explicit scope guard | docs/JAM_GROUNDING.md; paper 1 |
C2-C4 recover the familiar fact that redundancy cannot eliminate a common-cause failure component. C20 is likewise closely related to established common-cause reliability and response-diversity ideas: an independent failure profile can be disproportionately valuable. These are retained as calibration results, not novelty claims. Shapley values and Harsanyi dividends in C21 are established cooperative-game-theory tools. The research contribution must come from how these pieces are tied to a declared viability margin and later to endogenous behavioral and capacity dynamics.
This repository does not claim that consensus establishes external truth, that every species performs a net ecosystem service, that all persistent networks are cooperative, or that the present toy model constitutes a security analysis of JAM.