Release 0.3.0

Author: denisecase

.github/workflows/ci-python-zensical.yml

@@ -32,8 +32,7 @@ env:
   PYTHONIOENCODING: "utf-8" # WHY: Consistent encoding across platforms.
   PYTHON_VERSION: "3.15"
   UV_PYTHON: "3.15"
-  DOC_SECTIONS: "Basic,Structure,Admissibility,Separation,Invariants,Theorems,Witness"
-   # WHY: Enforce critical docs sections for theory repositories.
+  DOC_SECTIONS: "Core, Spec, Surface"   # WHY: Enforce critical docs sections for theory repositories.
    # OBS: This is a comma-separated list of required section headers in docs/en/index.md.
   MODULE_PREFIX: "NeutralSubstrate/"
 

CHANGELOG.md

@@ -11,6 +11,40 @@ and this project adheres to **[Semantic Versioning](https://semver.org/spec/v2.0
 
 ---
 
+## [0.3.0] - 2026-05-01
+
+### Added
+
+- `FrameworkVariant` predicate - a primitive is framework-variant if
+  admissible frameworks disagree about it
+- `FrameworksContradict` predicate - one framework affirms what another denies
+- `causal_normative_affirmed` axiom - companion to `framework_relativity`;
+  establishes that non-neutral primitives are affirmed by some admissible framework
+- `framework_contestability_lemma` theorem - framework-variant primitives
+  cannot appear in neutral substrates; proves the extension stability
+  violation; the interpretive non-commitment violation is deferred to 0.4.0
+  when interpretive non-commitment (INC) is formalized
+- `separate_stability` theorem - a neutral substrate is separately consistent
+  with each of two mutually contradicting frameworks
+- Incident substrate example in `TestRegime` instantiating `separate_stability`
+  on the 2026 NS paper Section 4.3 engineering/legal framework pair
+- `NS.THEOREM.LOWER_BOUND_ONLY` citation ID for domains where only the
+  lower bound applies
+
+### Changed
+
+- Namespace changed to SE.NeutralSubstrate
+- Split into Core / Spec / Surface / entry point
+- ISO-structured doc block on NeutralSubstrate.lean
+- Test library with TestBasic and TestRegime
+- lakefile.toml with separate Test lib target
+- `neutral_primitives_undisputed` doc strengthened with upper-bound warning
+- `ontological_neutrality_theorem` doc updated with asymmetry note on
+  differing axiom dependencies of the two directions
+- `NeutralSubstrate.lean` Section 2.5 added normative asymmetry note to public surface
+
+---
+
 ## [0.1.0] - 2026-04-28
 
 ### Added
@@ -44,7 +78,8 @@ Follow these steps exactly when creating a new release.
 ### Task 1. Update release metadata (manual edits)
 
 1.1. CITATION.cff: update version and date-released
-1.2. CHANGELOG.md: add section, move unreleased entries, update links
+1.2. lakefile.toml: update version
+1.3. CHANGELOG.md: add section, move unreleased entries, update links
 
 ### Task 2. Sync
 
@@ -97,5 +132,6 @@ git tag -d vX.Z.Y
 git push origin :refs/tags/vX.Z.Y
 ```
 
-[Unreleased]: https://github.com/structural-explainability/se-theory-neutral-substrate/compare/v0.1.1...HEAD
+[Unreleased]: https://github.com/structural-explainability/se-theory-neutral-substrate/compare/v0.3.0...HEAD
+[0.3.0]: https://github.com/structural-explainability/se-theory-neutral-substrate/compare/v0.1.0...v0.3.0
 [0.1.0]: https://github.com/structural-explainability/se-theory-neutral-substrate/releases/tag/v0.1.0

CITATION.cff

@@ -9,8 +9,8 @@ cff-version: "1.2.0"
 type: software
 
 title: "SE Theory: Neutral Substrate"
-version: "0.1.0"
-date-released: "2026-04-30"
+version: "0.3.0"
+date-released: "2026-05-01"
 
 authors:
   - family-names: Case

NeutralSubstrate.lean

@@ -1,16 +1,96 @@
-import NeutralSubstrate.Basic
-import NeutralSubstrate.Structure
-import NeutralSubstrate.Admissibility
-import NeutralSubstrate.Separation
-import NeutralSubstrate.Invariants
-import NeutralSubstrate.Theorems
-import NeutralSubstrate.Witness
+import NeutralSubstrate.Core
+import NeutralSubstrate.Spec
+import NeutralSubstrate.Surface
 
 /-!
-File: NeutralSubstrate.lean
+# Neutral Substrate (NS)
 
-Notes:
+Lean 4 formalization of the Neutral Substrate specification from
+Structural Explainability (SE) theory.
+Defines the necessary and sufficient conditions for
+ontological neutrality under durable interpretive disagreement.
 
-- This is the single import surface for downstream users.
-- Must remain thin: imports only, no logic.
+## 1.  Scope (Informative)
+
+Applies to substrates optimized for stability across disagreeing
+interpretive frameworks.
+Does not apply to substrates optimized for other objectives.
+
+This library does not encode identity regimes, persistence behavior,
+domain semantics, or operational validation.
+
+## 2.  Public Surface (Normative)
+
+The following names constitute the normative public surface of this library.
+They are stable across patch versions.
+Breaking changes require a minor version increment.
+Names in `NeutralSubstrate.Core` not listed here are
+internal and may change without notice.
+
+### 2.1.  Types
+
+- `PrimitiveKind`  the three primitive classifications
+- `Primitive`      basic unit of ontological commitment
+- `Ontology`       a finite list of primitives
+- `Framework`      an interpretive stance over primitives
+
+### 2.2.  Predicates
+
+- `Neutral`                   extension stability holds
+- `Admissible`                framework is internally consistent
+- `ExtensionStable`           no admissible framework causes inconsistency
+- `containsCausalOrNormative` boolean test for non-neutral content
+- `extensionInconsistent`     a framework denies a substrate primitive
+- `FrameworkVariant`          admissible frameworks disagree about a primitive
+- `FrameworksContradict`      one framework affirms what another denies
+
+### 2.3.  Axioms
+
+- `framework_relativity`          causal/normative primitives are contested
+- `neutral_primitives_undisputed` neutral primitives are framework-invariant
+- `causal_normative_affirmed`     causal/normative primitives are affirmed
+
+### 2.4  Theorems
+
+- `ontological_neutrality_theorem`     main biconditional result
+- `not_neutral_if_causal_or_normative` only-if direction
+- `neutral_if_only_neutral`            if direction
+- `framework_contestability_lemma`     framework-variant primitives cannot appear in NS
+- `separate_stability`                 an NS is separately consistent with each of two mutually
+                                         contradicting frameworks
+
+### 2.5.  Asymmetry Note (Normative)
+
+The two directions of `ontological_neutrality_theorem` have different
+epistemic status and different axiom dependencies.
+
+The lower bound (`not_neutral_if_causal_or_normative`) follows from
+`framework_relativity` alone.
+It holds structurally in any domain where causal and normative
+primitives are contested across admissible frameworks.
+
+The upper bound (`neutral_if_only_neutral`) additionally requires
+`neutral_primitives_undisputed`.
+It holds only in domains where identity conditions are not themselves contested.
+In domains where identity is contested, only the lower bound applies.
+Cite `NS.THEOREM.LOWER_BOUND_ONLY` when documenting this restriction.
+
+## 3.  Usage (Informative)
+
+```lean
+import NeutralSubstrate
+open SE.NeutralSubstrate        -- types, predicates, axioms, theorems
+open SE.NeutralSubstrate.Spec   -- citation IDs (optional)
+```
+
+## 4.  Metadata (Informative)
+
+Version, authorship, and release date: see `CITATION.cff`.
+Scope, layer, and governance: see `SE_MANIFEST.toml`.
+
+## 5.  File Notes (Informative)
+
+- This file must remain thin: imports only, no logic.
+- Downstream regime libraries depend on this file as their sole NS import.
+- Internal structure (Core, Spec, Surface) is not part of the public contract.
 -/