Contributing to the Gnosis math sandbox

• Policy: MATH_SANDBOX.md
• Dependency graph: GNOSIS_MATH_DEPENDENCY_GRAPH.md

What belongs in MathSandbox

• Init-first: modules that build without import Mathlib (use GnosisMathPrelude for shared Nat/List helpers).
• Named axioms: follow the same discipline as the physics sandbox — no anonymous sorry on promoted surfaces.

What belongs elsewhere

• Heavy Mathlib: keep in ForkRaceFoldTheorems until peeled; document debt in MATH_SANDBOX.md.
• GreekLogicCanon split: new Init-only slices go under ForkRaceFoldTheorems/GreekLogicCanon/; promote stable slices with import lines in MathSandbox.lean (see DiscreteBoundary). Use MathSandboxExtras only for transitional or experimental wiring.

Verification

cd open-source/gnosis && pnpm run validate:lean-minimal

This runs lean-minimal lake build and node scripts/validate-init-only-import-closure.mjs (see init-only-import-closure.json).