forgo.cloud
Sign in
Repo workspace

forkjoin-ai/gnosis

Socio-technical sandbox (Lean)

docs/SOCIO_TECHNICAL_SANDBOX.md
forkjoin-ai/gnosis
Repo overview Open in workbench

Socio-technical sandbox (Lean)

Focused Lean library SocioTechnicalSandbox (see lakefile.lean): discrete toy dynamics for backlog / arousal / repair cap and discrete rollback triggers.

Build

Recommended (no Mathlib): lean-minimal target ArenaSocioMinimal — same sources, fast PR/CI gate.

cd open-source/gnosis && node scripts/prepare-lean-minimal.mjs && cd lean-minimal && lake build ArenaSocioMinimal

Heritage package (Mathlib present in the workspace; optional):

cd open-source/gnosis/lean && lake build SocioTechnicalSandbox

Lean-only (socio sandbox, no TS tests): from open-source/gnosis,

pnpm run validate:socio-sandbox

Full arena slice (Lean + TS gates + tests): from open-source/gnosis,

pnpm run validate:arena-stack

Includes verification bundle CLI, ecology snapshot CLI, and gnode tests for merge gate + ecology snapshot (see ARENA_MERGE_GATE.md).

TS-only (skip Lean build): pnpm run validate:arena-stack-ts.

Modules

Module Content
SocioTechnicalSandbox/CoupledDynamics.lean STState, repairCap, repairCap_antitone, servedRepair, stepX
SocioTechnicalSandbox/RollbackToy.lean integralDeficit, allBelow, rollbackTrigger, small lemmas
SocioTechnicalSandbox.lean Import hub

Expository docs for the full socio-technical control story: THREE_ARENAS_SYNTHESIS.md, TOPO_COGNITIVE_EVENT_HORIZON.md, AUTONOMOUS_MUTATION_ZERO_TRUST.md.