chore

Author: denisecase

Main.lean

@@ -12,7 +12,5 @@ import NeutralSubstrate
 --   This file must remain trivial and stable.
 --   Any failure here indicates a broken proof or import graph.
 
-
-
 def main : IO Unit :=
-  IO.println "Structural Explainability: package verified."
+  IO.println "Success: package verified."

NeutralSubstrate.lean

@@ -2,11 +2,17 @@ import NeutralSubstrate.Conformance
 import NeutralSubstrate.Core
 import NeutralSubstrate.Spec
 
--- REQ.LIBRARY.ROOT:
---   Public library root for this package.
--- OBS:
---   Imports must appear before this comment (Lean requirement).
---   This file is intentionally thin: it only re-exports submodules.
+/-!
+REQ.PUBLIC.SURFACE:
+  Canonical public import surface for this package.
+  Do not add any declarations here.
+  Do not add empty namespaces.
 
-namespace StructuralExplainability.NeutralSubstrate
-end StructuralExplainability.NeutralSubstrate
+WHY:
+  Downstream projects should have exactly one stable import path for this repo.
+
+OBS:
+  - This module re-exports the intended public modules by importing them.
+  - It must not define placeholder namespaces.
+  - All exported declarations live in imported modules.
+-/

SE_MANIFEST.toml

@@ -22,7 +22,8 @@ optional = []
 artifacts = [
   "ANNOTATIONS.md",
   "CITATION.cff",
-  "README.md"
+  "README.md",
+  "SE_MANIFEST.toml"
 ]
 
 [scope]