How the Ecological OS is built.

How the Ecological OS is built · snapshot 2026-09-20

An operating system for the repair of living systems.

Every number a customer sees traces to an admitted kernel; every kernel traces to a DOI and a kernel-checked theorem; every decision records the foundation’s applicability and stops at a stated boundary. This page is generated from the same registries the runtime reads.

Decision kernels, runnable

17

Blocked, awaiting warrant

1

Held proposals

6

Kernel candidates in canon

26

Working-corpus records

176

Canon Lean records

203

Empirical validation status on every admitted kernel today: NOT_VALIDATED. Authority: automatic kernel activation false · automatic certification false · automatic ledger mutation false.

Six layers

1. L5GovernanceKernel admission (VRS-VIRIDISOS-KERNEL-PACKAGE-1), product warrant chain, human publish gate. No automatic activation, certification or ledger mutation.
2. L4SurfacesPublic site · free decision workspace · reviewed analysis (quoted) · agent API + MCP · public recompute receipts · research library.
3. L3The loopQualify → Bind evidence → Route → Compute & verify → Review → Deliver → Learn. Every step has a gate and three outcomes, one of which is a refusal.
4. L2Decision familiesFour families, each naming its customer question and its decision boundary.
5. L1Admitted kernelsModules with a DOI, kernel-checked Lean theorem, closed schema, units, deterministic runner and recompute receipt.
6. L0FoundationIntelligence Bound (P0), bounded-memory dissipation, biosphere erasure bound, thermodynamic economics. Applicability is recorded on every decision; a numerical result is withheld.

The loop

Seven stages; each has a gate and three outcomes, one of which is a refusal.

Four decision families, 18 kernels

24 theorem functions

A Lean theorem is “hypotheses ⇒ conclusion”. Each of these takes your values, reports which hypotheses hold and the conclusion that follows, with a receipt. Callable unsigned previews; not admitted to reviewed analyses; empirical validation NOT_VALIDATED.

• Biosphere erasure floor — total erasure cost is at least N·ε_L
  Checks that when every bit of biosphere order costs at least the Landauer quantum to erase, the total cost of erasing N bits is at least N times that quantum.
  callablebiosphere_erasure_floor · BiosphereErasureBound.leanRun
• Bounded-memory learning — erasure dissipation floor
  Checks that a learner with finite memory that acquired more bits than it can store must dissipate at least ε·(acquired − memory) as heat.
  callableerasure_dissipation_floor · BoundedMemoryLearning.leanRun
• The Conjunctive Audit Stewardship Theorem: Why Evidence Portfolios Reward Bundles Rather Than Scattered Greedy Checks
  For one independent conjunctive claim with equal audit costs, auditing the k smallest component-validity probabilities maximizes post-audit claim credibility.
  referenceconjunctive_chain_weakest_first · series/CAST/ViridisRun120.leanRun
• The Corridor Overlap Duality Certificate: An exact synchrony-diversification tradeoff for two shared habitat paths
  For two finite fixed paths under independent physical-edge survival, Q_A Q_B equals Q_union Q_intersection.
  referencesynchrony_dividend_identity · series/CODC/ViridisRun133.leanRun
• Decoherent selection — ambiguity cost is at most ln N
  Checks that the Shannon entropy (ambiguity cost, in nats) of a decision distribution over N options never exceeds ln N.
  callableambiguity_cost_le_lnN · DecoherentSelection.leanRun
• The D-Score Weight-Charter Certificate: A sharp rank-stability bound for precommitted composite indicators
  For simplex weights w and w0 and finite-dimensional contrast z, absolute score drift is at most total variation times range(z); the corollary is dimension-free within these assumptions.
  referencetv_range_certificate · series/DSWC/ViridisRun132.leanRun
• Effortless equilibrium — Intelligence Bound floor on forcing time
  Checks that steering a system with I bits of control information at a rate within the Intelligence Bound takes at least I·k_B·T·ln 2/(P·D) time.
  callablesteersman_ib_floors_forcing_time · EffortlessEquilibrium.leanRun
• The Gaian Alignment Cone Certificate: When Local Directional Bounds Survive Aggregation
  Nonnegative weighted subsystem residuals obey the aggregate residual budget.
  referenceaggregate_residual_bound · series/GACC/ViridisRun138.leanRun
• Geodesic saturation — forcing excess splits into speed and path excess
  Checks that the excess dissipation of a finite-time protocol above the geodesic minimum splits exactly into a non-negative speed-variation part and a non-negative path-length part.
  callableforcing_decomposition_nonneg · GeodesicSaturation.leanRun
• A Free-Energy Floor for Habitable-State Concentration: A Coarse-Grained Relative-Entropy Audit for Gaian Models
  KL decomposes exactly into the binary H versus H-complement divergence plus two conditional divergences.
  referencekl_chain_rule_habitable_partition · series/HCF/ViridisRun123.leanRun
• HDFM — corridor width is monotone in Strahler order
  Checks that in a dendritic (HDFM) corridor network with widths W_min·α^(order−1) and α ≥ 1, a higher-order corridor is never narrower than a lower-order one.
  callablestrahler_monotone_width · P2_HDFM_POC.leanRun
• Information Symbiosis Balance: A Conditional-Dependence Criterion for Cooperative Learning
  For every finite joint distribution, B = I(Y;X1,X2)-I(Y;X1)-I(Y;X2) equals I(X1;X2|Y)-I(X1;X2).
  referenceinformation_symbiosis_chain_rule · series/ISB/ViridisRun121.leanRun
• Conservation feasibility — corrigibility rate ceiling under the Intelligence Bound
  Checks that if correcting an agent at rate Δ costs Δ·k_B·T·ln 2 of power and that fits in the available power P, then the correction rate cannot exceed P/(k_B·T·ln 2).
  callablecorrigibility_under_IB · P3_Impossibility.leanRun
• Mutualistic attestation — attester throughput speed limit
  Checks that an attester whose per-attestation cost is κ·H cannot attest faster than P·D/(κ·H) when its power budget covers the work.
  callableattester_ib_throughput_speed_limit · MutualisticAttestation.leanRun
• Pivotal Corridor Stewardship: Exact Reliability Gradients and a Failure-Aware Priority Rule
  For independent edge states, the partial derivative of two-terminal reliability with respect to an edge survival probability equals that edge's pivotal probability.
  referencereliability_derivative_eq_pivotal_probability · series/PCS/ViridisRun124.leanRun
• Perennial corridor — holding power grows with decay rate
  Checks that holding a corridor against faster decay never takes less standing power (holding power δ·ε is monotone in the decay rate δ).
  callableholding_power_mono_in_decay · PerennialCorridor.leanRun
• Plasma N-fixation — information-rate bound structure
  Checks that any information rate within the solar-powered system's bound P/(k_B·T·ln 2) consumes no more than the available power P.
  callabletheorem10_info_bound_structure · P7_PlasmaNFix/Integration.leanRun
• The Symbiotic Accounting Certificate: Complementarity Does Not Create Thermodynamic Capacity
  Any conjunctive task rate obeys R <= P/(epsilon sum_i w_i/d_i) under the frozen component and shared-budget inequalities.
  referenceconjunctive_rate_upper_bound · series/SAC/ViridisRun137.leanRun
• The Sufficient Sanitization Certificate: Task Information, Data Minimization, and an Ideal Erasure Gap
  For finite X,Y and deterministic S=f(X), I(Y;X)=I(Y;S)+I(Y;X|S).
  referencerelevance_chain_identity · series/SSC/ViridisRun135.leanRun
• Stewardship setpoint — which way to move capacity toward D*
  Given regeneration rate ρ, carrying capacity K, discount r and current capacity D, reports the sustainable setpoint D* = (K/2)(1 − r/ρ) and checks that the marginal signal points toward it (raise capacity below D*, lower it above).
  callableorar_extremum_seeking_converges_to_Dstar · StewardshipSetpoint.leanRun
• Thermodynamic attention — slower modes are filled first
  Checks that under attention water-filling, a mode with larger variance (slower, closer to a tipping point) never receives less attention capacity than a faster one.
  callableslow_modes_filled_first · ThermodynamicAttention.leanRun
• Thermodynamic economics — production cannot exceed P·D/(k_B·T·ln 2)
  Checks that thermodynamic production η·P·D/(k_B·T·ln 2) never exceeds the ceiling P·D/(k_B·T·ln 2) when efficiency and data richness are fractions.
  callablethermodynamic_production_bound · P4_ThermodynamicEconomics.leanRun
• Universal water-filling — the equimarginal split is optimal
  For two concave-quadratic uses of a budget R, reports the water-filling split x* and shadow price λ*, checks both marginals equal λ*, and checks that your proposed split x does no better than x*.
  callableuwmt_concave_optimum_is_waterfilling · UniversalWaterfilling.leanRun
• The Zeno Alignment Budget: Uniform Projective Steps and a Noise-Limited Measurement Count
  For fixed N and endpoint angle in the stated two-level geodesic model, equal angular increments uniquely maximize successful-branch probability.
  referenceuniform_zeno_schedule_maximizes_success · series/ZAB/ViridisRun122.leanRun

Compiled from the canon v10.2.0-os.2 · commit 85505cf · catalog 6d992e8efe77

What is queued behind the gate

Held proposals are kernel-verified but not wired; each names the gate that would admit it. Research intake: 37 backlog no wrapper · 7 certification ready · 1 kernel implementation ready.

1. P1Delay-coherence budgetHOLD_FIXTURE_VALIDATIONdoi:10.5281/zenodo.21855724

   Next gate: Run real D-Score timestamps and component weights through frozen fixtures and review the refusal threshold.

2. P2Effective-resistance stewardship allocatorHOLD_CASE_STUDY_AND_SCOPEdoi:10.5281/zenodo.20777069

   Next gate: Remove IB/Landauer claims, narrow the deferred general sensitivity theorem, and pass a Circuitscape case-study fixture.

3. P3Firebreak circuit-rank plannerHOLD_CANON_AND_EMPIRICAL_VALIDATIONdoi:10.5281/zenodo.21708530

   Next gate: Create a Canon-linked exact proof object and validate the fire-spread claim with FARSITE, FlamMap, or a real landscape.

4. P4Gaming-resistant D-Score weightsHOLD_EMPIRICAL_CALIBRATIONdoi:10.5281/zenodo.21609945

   Next gate: Estimate at least one real elasticity vector, generalize the proof beyond three named channels, and freeze calibration provenance.

5. P5Fragmentation-hysteresis restoration budgetHOLD_INDEPENDENT_Q_CALIBRATIONdoi:10.5281/zenodo.21609938

   Next gate: Estimate q independently from an offset registry and remove circular calibration and thermodynamic-law language.

6. P6Early-warning observability windowHOLD_EMPIRICAL_AND_FORMAL_RECONCILIATIONdoi:10.5281/zenodo.21327070

   Next gate: Reconcile the paper and Lean statistic, prove a maximum rather than a stationary point, and test published lake or coral series.