folders

Author: denisecase

CITATION.cff

@@ -18,6 +18,7 @@ keywords:
   - structural-explainability
   - accountability
   - ontological-neutrality
+  - neutral-substrate
   - formal-ontology
   - formal-verification
   - theorem-proving

Main.lean

@@ -1,3 +1,5 @@
+import NeutralSubstrate
+
 -- REQ.EXEC.MAIN:
 --   Main entry point for this package.
 --
@@ -10,7 +12,7 @@
 --   This file must remain trivial and stable.
 --   Any failure here indicates a broken proof or import graph.
 
-import StructuralExplainability
+
 
 def main : IO Unit :=
   IO.println "Structural Explainability: package verified."

NeutralSubstrate.lean

@@ -0,0 +1,12 @@
+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.
+
+namespace StructuralExplainability.NeutralSubstrate
+end StructuralExplainability.NeutralSubstrate

NeutralSubstrate/Conformance.lean

@@ -0,0 +1,20 @@
+import NeutralSubstrate.Core
+import NeutralSubstrate.Spec
+
+/-!
+Neutral Substrate (NS) conformance: identifier-to-theorem trace surface.
+-/
+
+namespace StructuralExplainability.NeutralSubstrate.Conformance
+
+open StructuralExplainability
+open StructuralExplainability.NeutralSubstrate.Spec
+
+structure ConformanceEvidence where
+  neutrality_no_causal_or_normative :
+    ∀ S : Ontology, Req_NS_NEUTRALITY_NO_CAUSAL_OR_NORMATIVE S ↔ Neutral S
+
+  extension_stability_is_neutrality :
+    ∀ S : Ontology, Req_NS_NEUTRALITY_EXTENSION_STABILITY S ↔ Neutral S
+
+end StructuralExplainability.NeutralSubstrate.Conformance

…uralExplainability/NeutralSubstrate.lean NeutralSubstrate/Core.leanStructuralExplainability/NeutralSubstrate.lean renamed to NeutralSubstrate/Core.lean StructuralExplainability/NeutralSubstrate.lean renamed to NeutralSubstrate/Core.lean

@@ -0,0 +1,24 @@
+import NeutralSubstrate.Core
+
+/-!
+Neutral Substrate (NS) spec surface: identifiers and requirement shapes.
+-/
+
+namespace StructuralExplainability.NeutralSubstrate.Spec
+
+
+def NS_NEUTRALITY_NO_CAUSAL_OR_NORMATIVE : String :=
+  "NS.NEUTRALITY.NO_CAUSAL_OR_NORMATIVE"
+
+def NS_NEUTRALITY_EXTENSION_STABILITY : String :=
+  "NS.NEUTRALITY.EXTENSION_STABILITY"
+
+/-- REQ: NS.NEUTRALITY.NO_CAUSAL_OR_NORMATIVE -/
+def Req_NS_NEUTRALITY_NO_CAUSAL_OR_NORMATIVE (S : StructuralExplainability.Ontology) : Prop :=
+  StructuralExplainability.containsCausalOrNormative S = false
+
+/-- REQ: NS.NEUTRALITY.EXTENSION_STABILITY -/
+def Req_NS_NEUTRALITY_EXTENSION_STABILITY (S : StructuralExplainability.Ontology) : Prop :=
+  StructuralExplainability.ExtensionStable S
+
+end StructuralExplainability.NeutralSubstrate.Spec

NeutralSubstrate/Spec.lean

@@ -0,0 +1,50 @@
+schema = "se-manifest-1"
+
+[repo]
+name   = "NeutralSubstrate"
+org    = "structural-explainability"
+kind   = "formalization"
+status = "reference"
+since  = "2025"
+summary = "Lean formalization of the ontological neutrality theorem for representational substrates."
+
+[layer]
+space = "SE"
+role  = "foundation"
+
+[depends]
+required = [
+  "structural-explainability/spec-se@v1"
+]
+optional = []
+
+[provides]
+artifacts = [
+  "ANNOTATIONS.md",
+  "CITATION.cff",
+  "README.md"
+]
+
+[scope]
+includes = [
+  "ontological neutrality theorem",
+  "extension stability under disagreement",
+  "formal definitions of neutrality",
+  "axioms bounding domain applicability"
+]
+excludes = [
+  "identity regime definitions",
+  "entity kinds",
+  "domain semantics",
+  "explanations or interpretive claims",
+  "causal or normative primitives",
+  "governance or enforcement logic"
+]
+
+[citation]
+cff = "CITATION.cff"
+preferred = "repo"
+bib_hint = "case2025-lean-ns"
+
+[traceability]
+identifier_map = "none"

SE_MANIFEST.toml

@@ -126,9 +126,9 @@ Type backslash + shortcut, then space:
 
 | Command | Purpose |
 |---------|---------|
-| `lake build` | Compile the project. |
 | `lake clean` | Remove build artifacts. |
-| `lake exe <name>` | Run an executable. |
+| `lake build` | Compile the project. |
+| `lake exe verify` | Run verification executable. |
 
 ---
 

StructuralExplainability.lean

@@ -5,7 +5,10 @@ This document maps definitions and theorems from the paper to their Lean formali
 **Paper**: "The Ontological Neutrality Theorem:
 Why Neutral Ontological Substrates Must Be Pre-Causal and Pre-Normative" (Case, 2025)
 
-**Formalization**: `StructuralExplainability/NeutralSubstrate.lean`
+**Formalization**:
+
+- `NeutralSubstrate/NeutralSubstrate/*.lean`
+
 
 ## Domain Scope
 
@@ -59,8 +62,9 @@ Such positions do not contradict these results; they are outside the scope of th
 To verify the formalization (and optionally, run it):
 
 ```bash
+lake update
 lake build
-lake exe neutralsubstrate
+lake exe verify
 ```
 
 All theorems compile without `sorry`, confirming the proofs are complete.