Seismic stress toy (Gnosis TypeScript + Lean)

Parent index: ./README.md
Formal ledger rows: ../THEOREM_LEDGER.md (THM-PLANETARY-SEISMIC-*)
Broader physics hub (Mathlib classical / thermo): ./PHYSICS_SANDBOX.md

This page ties together the executable discrete-time toy in TypeScript and the small Lean sketches that formalize fragments of the same story. It is not a substitute for continuum seismology or elastodynamics.

What this is (and is not)

Is: deterministic updates for load → threshold → slip on one or more patches; optional θ-aging with a linear effective critical stress (rate–state-shaped hooks, not full Dieterich–Ruina ODEs); a two-node symmetric stress exchange relaxTwoPatch with coupling κ ∈ [0, 1] before independent slip on each patch.

Is not: Green’s functions, finite-source rupture dynamics, or verified rate-and-state friction laws on a continuum fault.

TypeScript module

Source: ../src/seismic-stress-toy.ts
Package export: @a0n/gnosis/seismic-stress-toy
Disclaimer constant: SEISMIC_STRESS_TOY_DISCLAIMER (use in manifests or UIs when surfacing outputs)

API surface (grouped)

Group	Functions
StructuralErrorgle patch, fixed threshold	`normalizeStructuralErrorgleAsperityParams`, `slipAfterLoaded`, `stepStructuralErrorgleAsperity`, `simulateStructuralErrorgleAsperity`
Multi-patch (independent steps)	`stepMultiAsperity`
Two-patch relax (no slip)	`relaxTwoPatch` — total of loaded stresses conserved for all `κ`
Two-patch coupled (fixed threshold)	`stepCoupledTwoPatch`, `simulateCoupledTwoPatch`
Rate–state-shaped single patch	`normalizeRateStateAsperityParams`, `rateStateThetaAging`, `effectiveCriticalLinear`, `stepStructuralErrorgleAsperityRateState`, `simulateStructuralErrorgleAsperityRateState`, optional `thetaOnRupture`
Two-patch coupled + rate state	`stepCoupledTwoPatchRateState`, `simulateCoupledTwoPatchRateState`

Fork / race / fold reading (informal)

Fork: stepMultiAsperity applies one step per patch in parallel loading semantics; rupture order is deterministic by index.
Race: not used here — there is no competing winner selection; slips are patch-local after a shared relax when coupled.
Fold: relaxTwoPatch redistributes loaded stress between two nodes before slip; total loaded stress is unchanged by the relax map.

Lean mirrors

Lean module	Role
`SeismicStressToySketch.lean`	Discrete `ℕ` `stepStress` / `stepStressSubtract` + lemmas
`SeismicRelaxRealSketch.lean`	`relax_two_patch_real_conserves`, nonnegative parts for `κ ∈ [0,1]`
Hub: `PlanetaryHomologySandbox.lean`	Imports the sketches; build the library target below

Ledger IDs (canonical names)

ID	Maps to
`THM-PLANETARY-SEISMIC-DISC-STEP`	Discrete rupture iff loaded stress reaches critical
`THM-PLANETARY-SEISMIC-DISC-SUB`	Subtract slip: post-rupture stress `max residual (loaded − drop)`
`THM-PLANETARY-SEISMIC-RELAX-REAL`	Two-patch exchange on `ℝ` conserves total loaded stress
`THM-PLANETARY-SEISMIC-RELAX-NONNEG`	Nonnegative loads and `κ ∈ [0,1]` ⇒ nonnegative relaxed stresses

Validation

From open-source/gnosis:

pnpm run validate:seismic-stress-toy

Runs lake build PlanetaryHomologySandbox and the Jest-equivalent test file src/__tests__/seismic-stress-toy.test.ts.

One-shot demo (stdout)

node ./bin/gnode.js run src/seismic-stress-toy-demo.ts --export main

Prints a few labeled lines and terminal stresses from a fixed-parameter coupled run (deterministic). The script is shaped for gnode run’s TS bridge (simple console.log + explicit return).

forkjoin-ai/gnosis