Math sandbox (Gnosis Lean — Mathlib reduction)

Parent README: ../README.md
Formal index: ../FORMAL_LEDGER.md
Physics sandbox (contrast — Mathlib showcase): ./PHYSICS_SANDBOX.md
Dependency graph (Init-only): ./GNOSIS_MATH_DEPENDENCY_GRAPH.md
Contributing: ./MATH_SANDBOX_CONTRIBUTING.md
Vs Mathlib / Std: ./MATH_SANDBOX_VS_MATHLIB.md
Init-first replacement roadmap (what to peel vs keep): ./INIT_FIRST_MATHLIB_REPLACEMENT_ROADMAP.md

This document maps the Init-first “math sandbox” in open-source/gnosis/lean/Lean/ and records what is proved in the hub, what Mathlib debt exists elsewhere, and fork / refactor targets for the next integration phase.

Policy (vs physics sandbox)

Long term, Mathlib is replaced by an internally consistent, provable reduced layer. The math sandbox hub imports no Mathlib; any import Mathlib elsewhere is technical debt to peel or replace with Gnosis-local lemmas (and eventually a curated internal prelude, not a second Mathlib).

Status: lake build MathSandbox’s import closure is free of Mathlib (including Mathlib.Tactic — former tactic-only imports in [GnosisMathPrelude], [GnosisMath/ListNat], [Hyperoperations], etc. were removed in favor of import Init / structural imports). scripts/validate-init-only-import-closure.mjs passes for the MathSandbox root.

Entry point

MathSandbox.lean — import-only hub; build with lake build MathSandbox (see lakefile.lean lean_lib MathSandbox).

Layers in the hub (zero Mathlib in this graph)

Layer	Lean module	Role	Gaps
Prelude	`GnosisMathPrelude.lean` / `GnosisMath.Basic`	`powNat`, `mul_pow`-style `powNat_mul_distrib`, list length lemmas in `ListNat`	Expand with lemma-by-lemma ports; no wholesale Mathlib
Discrete masses (Init-only)	`DiscreteFiniteInfo.lean`	`finSum`, [`vadd`], [`finSum_vadd`]; [`Rat`] `ratFinSum`; [`MassVec.probRat`], [`ratFinSum_probRat_eq_one`]; [`MassVec.rawMassLog2Weight`] (`∑ m·log₂ m` on `Nat` masses); zero Mathlib	Shannon/KL with `Real.log`, `PMF` — Mathlib lane ([`ThermoPMFKLFintype`], …)
Coding / discrete	`KraftInequality.lean`	Kraft-style prefix-free / address-space model	Full analytic Kraft over ℝ, infinite codes
Growth / parity	`GeneralizedParity.lean`	Bounded multi-pair “parity” checks	Universal quantification over all growth pairs
Base ten / F–T	`BaseTenConsequence.lean`	Fork/race/fold narrative + Fibonacci vs triangular structure	Broader “base ten necessity” claims outside the proved fragment
Logic fragment	`LeibnizCalculemus.lean`	Finite signs, assignments, truth-table agreement	Completeness of a universal language, full Leibniz program
Hyperoperations	`Hyperoperations.lean`	`hyperop` hierarchy + `powNat` bridge (no deep `native_decide` on huge towers)	General closed forms beyond the proved slices
Fibonacci weights	`GnosisMath/Fibonacci.lean`	`fibZ` same equations as `ZeckendorfFST.F` / `PisotVickreyTable.F` for Init-only consumers	Keep narrative alignment across hubs
GreekLogicCanon (Init seed)	`GreekLogicCanon/DiscreteBoundary.lean`	Placeholder for finite combinatorial / paradox fragments before the monolith splits	Expand with real peeled sections

Optional hub (compatibility)

MathSandboxExtras.lean — lake build MathSandboxExtras; re-exports MathSandbox.lean for backward compatibility and future extras not yet listed in the main hub.

Corpus modules excluded from the hub (explicit debt or peel)

Module	Reason
`ZeckendorfFST.lean`	Init-only (no Mathlib imports); not re-exported from `MathSandbox` by default — see ZECKENDORF_FST_PEEL.md.
`PisotVickreyTable.lean`	Companion Pisot/Vickrey lattice file; `Mathlib.Tactic.Ring` removed, still uses `Linarith`, `Nat.Log`, `IntervalCases` — PISOT_VICKREY_PEEL.md.

Next-phase integration: fork `GreekLogicCanon.lean`

GreekLogicCanon.lean is not imported by MathSandbox: it uses import Mathlib and pulls a wide Gnosis chain (BuleyeanProbability, VoidWalking, EnvelopeConvergence, CombinatorialBruteForce, PhilosophicalAllegories, …).

Refactor / fork plan (prep for Mathlib-reduction integration):

Split by paradox / section into submodules under e.g. ForkRaceFoldTheorems/GreekLogicCanon/ with explicit imports, so Zeno / Achilles / Sorites slices can be linked independently.
Peel Mathlib: replace wholesale import Mathlib with minimal Mathlib.Analysis.* (or local analysis lemmas) per slice; move Buleyean-heavy sections behind an optional import or a later hub.
Promote Init-first cores where possible (mirror LeibnizCalculemus-style discipline for finite combinatorial fragments).
Only then add a chosen slice to MathSandbox.lean (preferred) or stage it under MathSandboxExtras.lean with documented Mathlib boundaries.

Until that fork lands, treat GreekLogicCanon as narrative-adjacent formal glue: valuable, but not part of the reduced hub contract.

Axiom discipline

Same as physics sandbox: named opaque / axiom blocks with documented interfaces — no anonymous sorry on promoted surfaces.

TypeScript lane

src/math-sandbox.ts exposes Lean module anchors and optional deterministic numeric toys; it is not proof-checked against Lean (see disclaimer string in that module).

CI / build

Default: lake build still targets ForkRaceFoldTheorems (full corpus).
Focused math hub: pnpm run validate:lean-minimal (or validate:math-sandbox, same pipeline) from open-source/gnosis — lean-minimal lake build + scripts/validate-init-only-import-closure.mjs / config init-only-import-closure.json (fails if any configured Init-only root closure imports Mathlib). Roots include MathSandbox, DiscreteFiniteInfo, LaplaceDemon, EntropyBridge.LayerC, etc.
GitHub Actions: .github/workflows/gnosis-math-sandbox.yml runs on pushes/PRs that touch the math sandbox Lean paths.

forkjoin-ai/gnosis