Architecture and namespaces

The repository is a small Lean library with an intentionally stable public surface.

Layout

• TheoremLibrary/ — reusable theorem modules.
• TheoremLibrary.lean — top-level import surface.
• INDEX.md — stable identifiers and human-readable statements.
• PUBLIC_CORE.md — exported module inventory.
• NAMESPACE.md — namespace and contribution boundary.
• scripts/ — bootstrap and independent validation checks.
• lakefile.lean, lake-manifest.json, lean-toolchain — pinned build environment.

Namespace rule

Reusable public mathematics lives under TheoremLibrary.*. Temporary research scaffolding or private proof exploration should not leak into the public namespace merely to make a local experiment compile.

Dependency shape

Modules are organized so foundational calculus/geometry results support higher-level consequences. Avoid circular “convenience imports” that make theorem provenance difficult to inspect.

Stable identifiers

Stable LIB-* and FRM-* identifiers decouple research references from module paths. Source organization can improve without forcing every notebook or ledger entry to change its conceptual identifier.