GnosisMath dependency graph (Init-only)

Parent: README.md
Math sandbox policy: MATH_SANDBOX.md

Directed edges mean imports (arrow points from importer → importee).

flowchart TB
  Init[Init]
  P[GnosisMathPrelude]
  L[GnosisMath.ListNat]
  F[GnosisMath.Fibonacci]
  B[GnosisMath.Basic]
  H[Hyperoperations]
  MS[MathSandbox]
  Init --> P
  P --> L
  Init --> F
  Init --> D[DiscreteFiniteInfo]
  P --> B
  L --> B
  F --> B
  B --> H
  B --> MS
  H --> MS
  D --> MS
  K[KraftInequality] --> MS
  GP[GeneralizedParity] --> MS
  BT[BaseTenConsequence] --> MS
  LC[LeibnizCalculemus] --> MS
  GL[GreekLogicCanon.DiscreteBoundary] --> MS

Arrows point into the importer: e.g. KraftInequality --> MathSandbox means MathSandbox imports KraftInequality.

Module	Imports	Role
`GnosisMathPrelude.lean`	`Init`	`powNat`, base `Nat` lemmas
`GnosisMath/ListNat.lean`	`GnosisMathPrelude`	`powNat_mul_distrib`, list length lemmas
`GnosisMath/Fibonacci.lean`	`Init`	`fibZ` tower (same equations as `ZeckendorfFST.F`, Init-only)
`DiscreteFiniteInfo.lean`	`Init`	`finSum`, `MassVec`, `ratFinSum`, `probRat` (Init-only thermo-shaped discrete layer)
`GnosisMath/Basic.lean`	`GnosisMathPrelude`, `ListNat`, `Fibonacci`	StructuralErrorgle barrel `import` for sandbox consumers
`Hyperoperations.lean`	`GnosisMath.Basic`	Hyperoperation hierarchy (`hyperop`, `powNat`)
`MathSandbox.lean`	`GnosisMath.Basic`, `DiscreteFiniteInfo`, Kraft / parity / …, `GreekLogicCanon.DiscreteBoundary`	CI-visible Init-first hub
`ZeckendorfFST.lean`	`Init`	Standalone Zeckendorf / Pisot–Vickrey FST substrate (`F`, `decode`, `smooth`, …); not imported by `MathSandbox`

Rule: Init-only sandbox roots (see init-only-import-closure.json) must not transitively import Mathlib (enforced by scripts/validate-init-only-import-closure.mjs; pnpm run validate:lean-minimal runs the Lake package + this check).

forkjoin-ai/gnosis

GnosisMath dependency graph (Init-only)

GnosisMath dependency graph (Init-only)