streamline

Author: denisecase

CITATION.cff

@@ -0,0 +1,25 @@
+cff-version: "1.2.0"
+type: software
+
+title: "Structural Explainability: Neutral Substrate"
+version: "0.1.0"
+date-released: "2025-12-23"
+
+authors:
+  - family-names: Case
+    given-names: Denise M.
+    orcid: "https://orcid.org/0000-0001-6165-7389"
+
+repository-code: "https://github.com/civic-interconnect/NeutralSubstrate"
+license: MIT
+
+keywords:
+  - structural-explainability
+  - accountability
+  - ontological-neutrality
+  - formal-ontology
+  - formal-verification
+  - theorem-proving
+  - lean4
+
+message: "If you use this software, please cite it as described in this file."

Main.lean

@@ -1,7 +1,16 @@
---- Main.lean executable ---
---- REQ: Main entry point for the application ---
+-- REQ.EXEC.MAIN:
+--   Main entry point for this package.
+--
+-- WHY:
+--   This executable exists solely to ensure that the full
+--   formalization compiles end-to-end under CI and local builds.
+--
+-- OBS:
+--   No definitions, theorems, or logic belong here.
+--   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: Ontological Neutrality Theorem verified."
---- End of Main.lean ---
+  IO.println "Structural Explainability: package verified."

README.md

@@ -4,50 +4,36 @@
 ![Build Status](https://github.com/civic-interconnect/NeutralSubstrate/actions/workflows/ci.yml/badge.svg)
 [![Check Links](https://github.com/civic-interconnect/NeutralSubstrate/actions/workflows/links.yml/badge.svg)](https://github.com/civic-interconnect/NeutralSubstrate/actions/workflows/links.yml)
 
-> Lean 4 formalization of the Ontological Neutrality Theorem.
+> Lean 4 formalization of foundational constraints required for ontological substrates
+> intended to support accountability under persistent interpretive disagreement.
 
-## Theorem
+## Context
 
-An ontology is neutral if and only if it contains no causal or normative primitives.
+Part of the Structural Explainability framework.
 
-```lean
-∀ S : Ontology, Neutral S ↔ containsCausalOrNormative S = false
-```
-
-## Domain Scope
-
-This formalization applies to substrates optimized for:
-
-- Stability under durable interpretive disagreement
-- Accountability across jurisdictions
-- Interoperability without semantic consensus
+## Scope
 
-## Paper (Submitted)
+This repository formalizes structural constraints on ontological substrates that are intended to remain stable across incompatible interpretations, legal regimes, and analytic frameworks.
 
-Case, D. M. (2025). "The Ontological Neutrality Theorem: Why Neutral Ontological Substrates Must Be Pre-Causal and Pre-Normative."
+It does not define a concrete ontology or protocol.
+It establishes conditions that any such system must satisfy at the substrate level.
 
-## Verify
+## Build and Run
 
 ```bash
 lake update
 lake build
-lake exe neutralsubstrate
+lake exe verify
 ```
 
 ## Documentation
 
 - [Paper to Lean Mapping](./docs/MAPPING.md)
 - [Lean 4 Quick Reference](./docs/LEAN.md)
 
-## Project Structure
+## Citation
 
-| Item         | Value                                            |
-| ------------ | ------------------------------------------------ |
-| Project name | `NeutralSubstrate`                               |
-| Namespace    | `StructuralExplainability`                       |
-| Library      | `StructuralExplainability`                       |
-| Executable   | `neutralsubstrate`                               |
-| Main proof   | `StructuralExplainability/NeutralSubstrate.lean` |
+See [CITATION.cff](./CITATION.cff)
 
 ## License
 

StructuralExplainability.lean

@@ -1,3 +1,14 @@
---- StructuralExplainability.lean ---
---- REQ: Library root, imports all modules ---
+-- REQ.LIBRARY.ROOT:
+--   Public library root for this package.
+--
+-- WHY:
+--   Downstream users import this module to obtain the package's
+--   entire verified surface through a single stable entry point.
+--
+-- OBS:
+--   Imports MUST appear at the beginning of the file (Lean requirement).
+--   This file remains thin: it only re-exports submodules.
+--   No definitions or theorems belong here.
+
 import StructuralExplainability.NeutralSubstrate
+

lakefile.toml

@@ -1,12 +1,57 @@
+# REQ.FILE.PROJECT.IDENTITY
+#   Declares the externally visible identity and build surface of this package.
+#   Sections marked CUSTOM are expected to vary by repository.
+
+# ============================================================
+# REQUIRED PROJECT IDENTITY (stable structure, custom values)
+# ============================================================
+
+# REQ.PROJECT.NAME
+#   Canonical package name.
+#   CUSTOM: Must match repository naming.
 name = "NeutralSubstrate"
+
+# REQ.PROJECT.VERSION
+#   Semantic version.
+#   Increment only for externally visible logical changes.
 version = "0.1.0"
-defaultTargets = ["StructuralExplainability"]
-keywords = ["ontology", "formal-verification", "structural-explainability"]
+
+# REQ.PROJECT.LICENSE
+#   Open license permitting reuse of formal artifacts.
 license = "MIT"
 
+# REQ.PROJECT.KEYWORDS
+#   Discovery metadata for Lean, GitHub, and academic indexing.
+#   CUSTOM: Adjust to reflect repository scope.
+keywords = [
+  "structural-explainability",
+  "accountability",
+  "ontological-neutrality",
+  "formal-ontology",
+  "formal-verification",
+  "theorem-proving",
+  "lean4"
+]
+
+# ============================================================
+# REQUIRED BUILD SURFACE (invariant across repos)
+# ============================================================
+
+# REQ.BUILD.DEFAULT_TARGETS
+#   Default build surface.
+#   MUST include the public library root.
+defaultTargets = ["StructuralExplainability"]
+
+# REQ.LIB.PUBLIC
+#   Public Lean library exported by this package.
+#   Downstream projects import this by name.
 [[lean_lib]]
 name = "StructuralExplainability"
 
+# REQ.EXEC.VERIFICATION
+#   Minimal executable used to verify that the
+#   formalization compiles end-to-end under CI and local builds.
+#   Executable MUST remain trivial.
 [[lean_exe]]
-name = "neutralsubstrate"
-root = "Main"
+name = "verify"
+root = "Main"