Release 0.4.0

Author: denisecase

CHANGELOG.md

@@ -9,7 +9,33 @@ and this project adheres to **[Semantic Versioning](https://semver.org/spec/v2.0
 
 ## [Unreleased]
 
----
+## [0.4.0] - 2026-05-01
+
+### Added
+
+- `InterpretivelyNonCommitted` predicate; no primitive in the substrate
+  is framework-variant; the second neutrality requirement (INC) from
+  Case (2025) alongside extension stability (EXT)
+- `only_neutral_primitives_implies_INC` theorem; only-neutral substrates
+  satisfy INC under existing axioms; no additional axiom required
+- `NS.DEF.INTERPRETIVELY_NON_COMMITTED` citation ID
+- `NS.THEOREM.ONLY_NEUTRAL_IMPLIES_INC` citation ID
+
+### Changed
+
+- `Neutral` updated from EXT alone to the full `EXT ∧ INC` conjunction.
+
+  **Breaking change**: all proofs unfolding `Neutral` updated accordingly.
+
+- `framework_contestability_lemma` now proves both EXT and INC violations;
+- "deferred to 0.4.0" note removed
+- `NeutralSubstrate.lean` Section 2.2 updated with `InterpretivelyNonCommitted`
+- `NeutralSubstrate.lean` Section 2.4 updated with `only_neutral_primitives_implies_INC`
+
+### Exports Added
+
+- `InterpretivelyNonCommitted`
+- `only_neutral_primitives_implies_INC`
 
 ## [0.3.0] - 2026-05-01
 
@@ -132,6 +158,7 @@ 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.3.0...HEAD
+[Unreleased]: https://github.com/structural-explainability/se-theory-neutral-substrate/compare/v0.4.0...HEAD
+[0.4.0]: https://github.com/structural-explainability/se-theory-neutral-substrate/compare/v0.3.0...v0.4.0
 [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,7 +9,7 @@ cff-version: "1.2.0"
 type: software
 
 title: "SE Theory: Neutral Substrate"
-version: "0.3.0"
+version: "0.4.0"
 date-released: "2026-05-01"
 
 authors:

NeutralSubstrate.lean

@@ -36,13 +36,14 @@ internal and may change without notice.
 
 ### 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
+- `Neutral`                    extension stability and interpretive non-commitment holds
+- `Admissible`                 framework is internally consistent
+- `ExtensionStable`            EXT:no admissible framework causes inconsistency
+- `InterpretivelyNonCommitted` INC: no primitive in the substrate is framework-variant
+- `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
 
@@ -52,11 +53,18 @@ internal and may change without notice.
 
 ### 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
+- `ontological_neutrality_theorem`     biconditional under both axioms
+- `not_neutral_if_causal_or_normative` lower bound; requires only
+                                         `framework_relativity`
+- `neutral_if_only_neutral`            upper bound; requires also
+                                         `neutral_primitives_undisputed`
+- `only_neutral_primitives_implies_INC` only-neutral substrates satisfy INC;
+                                          no additional axiom required
+- `framework_contestability_lemma`     framework-variant primitives cannot
+                                         appear in neutral substrates;
+                                         proves both EXT and INC violations
+- `separate_stability`                 a neutral substrate is separately
+                                         consistent with each of two mutually
                                          contradicting frameworks
 
 ### 2.5.  Asymmetry Note (Normative)

NeutralSubstrate/Core.lean

@@ -111,17 +111,6 @@ def extensionInconsistent (S : Ontology) (F : Framework) : Prop :=
 def ExtensionStable (S : Ontology) : Prop :=
   ∀ F : Framework, Admissible F → ¬extensionInconsistent S F
 
-/-- Neutrality is extension stability.
-
-    An ontology is neutral iff it can be extended by any admissible framework
-    without revision or contradiction.
-
-    OBS: The paper also specifies INC (interpretive non-commitment).
-    This formalization focuses on EXT (extension stability) as the
-    mechanically sufficient condition for the main theorem.
-    INC will be formalized in a future version alongside EXT. -/
-def Neutral (S : Ontology) : Prop := ExtensionStable S
-
 /-- A primitive is framework-variant if admissible frameworks disagree about it:
     some affirm it, some deny it.
 
@@ -136,6 +125,37 @@ def FrameworkVariant (p : Primitive) : Prop :=
   ∃ F1 F2 : Framework, Admissible F1 ∧ Admissible F2 ∧
     F1.affirms p = true ∧ F2.denies p = true
 
+/-- Interpretive non-commitment: no primitive in the substrate is framework-variant.
+
+    A substrate satisfies INC when every primitive it contains has truth
+    conditions that are framework-invariant — no admissible framework
+    affirms it while another denies it.
+
+    WHY: INC is the second neutrality requirement from Case (2025) alongside
+    EXT (extension stability). Together they constitute full neutrality.
+    A substrate satisfying INC makes no interpretive commitments at the
+    foundational layer: it does not assert propositions whose truth depends
+    on the conclusions of any particular interpretive framework.
+
+    OBS: For substrates where containsCausalOrNormative S = false,
+    INC follows from neutral_primitives_undisputed alone —
+    see only_neutral_primitives_implies_INC.
+    No additional axiom is required. -/
+def InterpretivelyNonCommitted (S : Ontology) : Prop :=
+  ∀ p ∈ S, ¬FrameworkVariant p
+
+/-- Neutrality is extension stability and interpretive non-commitment.
+
+    An ontology is neutral iff it can be extended by any admissible framework
+    without revision or contradiction (EXT), and it does not assert any
+    framework-variant proposition at the substrate layer (INC).
+
+    WHY: Both requirements are necessary. EXT alone is sufficient for the
+    lower bound but the full paper theorem requires INC alongside EXT.
+    See ontological_neutrality_theorem for the biconditional result. -/
+def Neutral (S : Ontology) : Prop :=
+  ExtensionStable S ∧ InterpretivelyNonCommitted S
+
 /-- Two frameworks mutually contradict when one affirms what the other denies.
 
     Note: mutual contradiction does not affect admissibility.
@@ -264,6 +284,36 @@ theorem any_false_implies_none {α : Type} (l : List α) (pred : α → Bool) :
 -- REQ.CORE.THEOREMS
 --   The main results. Each theorem cites its proof strategy.
 
+/-- THEOREM: Only-neutral substrate satisfies INC.
+
+    If an ontology contains only neutral primitives, it satisfies
+    interpretive non-commitment.
+
+    WHY: Establishes that INC follows from neutral_primitives_undisputed
+    alone, without requiring a new axiom. Used as a helper in the
+    updated neutral_if_only_neutral proof.
+
+    Proof strategy:
+    1. Take any p ∈ S and assume FrameworkVariant p for contradiction
+    2. Extract F2 from FrameworkVariant — the framework that denies p
+    3. any_false_implies_none shows p.kind = neutral
+    4. neutral_primitives_undisputed shows F2 cannot deny p
+    5. Contradiction with F2.denies p = true -/
+theorem only_neutral_primitives_implies_INC :
+    ∀ S : Ontology, containsCausalOrNormative S = false →
+    InterpretivelyNonCommitted S := by
+  intro S h_only_neutral
+  unfold InterpretivelyNonCommitted FrameworkVariant
+  intro p hp_in_S
+  intro ⟨_F1, F2, _hF1_adm, hF2_adm, _hF1_affirms, hF2_denies⟩
+  have h_all_neutral := any_false_implies_none S _ h_only_neutral
+  have hp_neutral_kind : (p.kind != PrimitiveKind.neutral) = false :=
+    h_all_neutral p hp_in_S
+  simp at hp_neutral_kind
+  have h_not_denied := neutral_primitives_undisputed p hp_neutral_kind F2 hF2_adm
+  rw [h_not_denied] at hF2_denies
+  contradiction
+
 /-- THEOREM: If an ontology contains causal or normative primitives, it is not neutral.
 
     This is the lower bound of the main theorem.
@@ -272,24 +322,26 @@ theorem any_false_implies_none {α : Type} (l : List α) (pred : α → Bool) :
     are contested across admissible frameworks.
 
     Proof strategy:
-    1. Assume neutrality for contradiction
-    2. Extract witness primitive p via any_true_implies_exists
-    3. Show p.kind ≠ neutral from the boolean witness
-    4. Apply framework_relativity to get F that denies p
-    5. Neutrality of S says F cannot cause inconsistency
-    6. But p ∈ S and F.denies p = true is exactly inconsistency
-    7. Contradiction -/
+    1. Assume neutrality (EXT ∧ INC) for contradiction
+    2. Extract EXT conjunct from h_neutral
+    3. Extract witness primitive p via any_true_implies_exists
+    4. Show p.kind ≠ neutral from the boolean witness
+    5. Apply framework_relativity to get F that denies p
+    6. EXT of S says F cannot cause inconsistency
+    7. But p ∈ S and F.denies p = true is exactly inconsistency
+    8. Contradiction -/
 theorem not_neutral_if_causal_or_normative :
     ∀ S : Ontology, containsCausalOrNormative S = true → ¬Neutral S := by
   intro S h_contains h_neutral
+  have h_ext := h_neutral.1
   have h_exists := any_true_implies_exists S _ h_contains
   match h_exists with
   | ⟨p, hp_in_S, hp_kind⟩ =>
     have hp_not_neutral : p.kind ≠ PrimitiveKind.neutral := by
       intro h_eq
       simp [h_eq] at hp_kind
     have ⟨F, hF_adm, hF_denies⟩ := framework_relativity p hp_not_neutral
-    have h_no_inconsist := h_neutral F hF_adm
+    have h_no_inconsist := h_ext F hF_adm
     apply h_no_inconsist
     exact ⟨p, hp_in_S, hF_denies⟩
 
@@ -301,32 +353,34 @@ theorem not_neutral_if_causal_or_normative :
     themselves contested across admissible frameworks.
 
     Proof strategy:
-    1. Unfold Neutral and ExtensionStable to expose the goal
-    2. Take any admissible framework F
-    3. Assume inconsistency for contradiction: ∃ p ∈ S, F.denies p = true
-    4. any_false_implies_none shows every p ∈ S has kind = neutral
-    5. neutral_primitives_undisputed shows F cannot deny that p
-    6. Contradiction with the denial assumption -/
+    1. Split Neutral into EXT ∧ INC and prove each conjunct
+    2. EXT: unfold and proceed as before using neutral_primitives_undisputed
+    3. INC: apply only_neutral_primitives_implies_INC directly -/
 theorem neutral_if_only_neutral :
     ∀ S : Ontology, containsCausalOrNormative S = false → Neutral S := by
   intro S h_only_neutral
-  unfold Neutral ExtensionStable extensionInconsistent
-  intro F hF_adm
-  intro ⟨p, hp_in_S, hF_denies⟩
-  have h_all_neutral := any_false_implies_none S _ h_only_neutral
-  have hp_neutral_kind : (p.kind != PrimitiveKind.neutral) = false :=
-    h_all_neutral p hp_in_S
-  simp at hp_neutral_kind
-  have h_not_denied := neutral_primitives_undisputed p hp_neutral_kind F hF_adm
-  rw [h_not_denied] at hF_denies
-  contradiction
+  constructor
+  · -- EXT: extension stability
+    unfold ExtensionStable extensionInconsistent
+    intro F hF_adm
+    intro ⟨p, hp_in_S, hF_denies⟩
+    have h_all_neutral := any_false_implies_none S _ h_only_neutral
+    have hp_neutral_kind : (p.kind != PrimitiveKind.neutral) = false :=
+      h_all_neutral p hp_in_S
+    simp at hp_neutral_kind
+    have h_not_denied := neutral_primitives_undisputed p hp_neutral_kind F hF_adm
+    rw [h_not_denied] at hF_denies
+    contradiction
+  · -- INC: interpretive non-commitment
+    exact only_neutral_primitives_implies_INC S h_only_neutral
 
 /-- THEOREM: Ontological Neutrality (biconditional)
 
     An ontology is neutral if and only if it contains no causal or normative primitives.
 
     This is the main result from Case (2025).
     It holds given framework_relativity and neutral_primitives_undisputed.
+    Neutrality is now the full EXT ∧ INC conjunction.
 
     NOTE: The two directions have different epistemic status.
     - Only-if (lower bound): follows from framework_relativity alone.
@@ -361,50 +415,51 @@ theorem ontological_neutrality_theorem :
     Formalizes the paper's Framework-Contestability Lemma (Case 2025, §4.2):
     a proposition whose truth conditions depend on interpretive framework
     conclusions cannot be a substrate commitment without violating
-    extension stability.
+    either EXT or INC.
 
-    NOTE: The paper states two conclusions from contestability:
-    (1) EXT violated - formalized here
-    (2) INC violated - deferred to 0.4.0 when INC is formalized
+    Both violations are now formalized:
+    (1) EXT violated: F2 denies p, but p ∈ S, producing inconsistency
+    (2) INC violated: p is framework-variant, but S contains p
 
     Proof strategy:
-    1. Extract F2 from FrameworkVariant - the framework that denies p
-    2. Apply h_neutral to F2 to get no-inconsistency claim
-    3. Construct extensionInconsistent S F2 from p ∈ S and F2.denies p
-    4. Contradiction -/
+    1. Assume Neutral S (EXT ∧ INC) for contradiction
+    2. EXT violation: extract h_ext, apply framework_relativity pattern
+       via F2 from FrameworkVariant, construct extensionInconsistent
+    3. INC violation: extract h_inc, apply to p and hp_in_S,
+       apply h_variant directly for contradiction
+    Note: either violation suffices; we use INC as it is most direct. -/
 theorem framework_contestability_lemma :
     ∀ p : Primitive, FrameworkVariant p →
     ∀ S : Ontology, p ∈ S → ¬Neutral S := by
   intro p h_variant S hp_in_S h_neutral
-  obtain ⟨_F1, F2, _hF1_adm, hF2_adm, _hF1_affirms, hF2_denies⟩ := h_variant
-  exact h_neutral F2 hF2_adm ⟨p, hp_in_S, hF2_denies⟩
+  have h_inc := h_neutral.2
+  exact h_inc p hp_in_S h_variant
 
 /-- THEOREM: Separate Stability
 
     A neutral substrate is separately consistent with each of two mutually
     contradicting frameworks.
 
     Formalizes the paper's key observation (Case 2025, §4.1) that a neutral
-    substrate need not reconcile contradicting frameworks - it must only
+    substrate need not reconcile contradicting frameworks — it must only
     avoid assertions that either framework rejects. The substrate's role
     is common-ground provision, not arbitration.
 
     NOTE: FrameworksContradict is not used in the proof body.
-    Neutrality implies stability under ALL admissible frameworks, which
-    subsumes the two-framework case. The hypothesis is retained for
-    fidelity to the paper's framing and to make the theorem applicable
-    to the incident example pattern.
+    The EXT conjunct of Neutral implies stability under ALL admissible
+    frameworks, which subsumes the two-framework case. The hypothesis
+    is retained for fidelity to the paper's framing.
 
     Proof strategy:
-    Neutrality of S directly implies ¬extensionInconsistent S F for any
-    admissible F. Apply twice, once for F1 and once for F2. -/
+    Extract EXT conjunct from Neutral S.
+    Apply twice, once for F1 and once for F2. -/
 theorem separate_stability :
     ∀ S : Ontology, Neutral S →
     ∀ F1 F2 : Framework, Admissible F1 → Admissible F2 →
     FrameworksContradict F1 F2 →
     ¬extensionInconsistent S F1 ∧ ¬extensionInconsistent S F2 := by
   intro S h_neutral F1 F2 hF1_adm hF2_adm _h_contradict
-  exact ⟨h_neutral F1 hF1_adm, h_neutral F2 hF2_adm⟩
+  exact ⟨h_neutral.1 F1 hF1_adm, h_neutral.1 F2 hF2_adm⟩
 
 
 -- ============================================================
@@ -428,9 +483,16 @@ theorem separate_stability :
 #check @FrameworkVariant
 -- Primitive → Prop
 
+#check @InterpretivelyNonCommitted
+-- Ontology → Prop
+
 #check @FrameworksContradict
 -- Framework → Framework → Prop
 
+#check @only_neutral_primitives_implies_INC
+-- ∀ (S : Ontology), containsCausalOrNormative S = false →
+--   InterpretivelyNonCommitted S
+
 #check @framework_contestability_lemma
 -- ∀ (p : Primitive), FrameworkVariant p → ∀ (S : Ontology), p ∈ S → ¬Neutral S
 

NeutralSubstrate/Spec.lean

@@ -74,6 +74,10 @@ def NS_ID_DEF_FRAMEWORK_VARIANT : String :=
 def NS_ID_DEF_FRAMEWORKS_CONTRADICT : String :=
   "NS.DEF.FRAMEWORKS_CONTRADICT"
 
+/-- Cite when a regime depends on the definition of InterpretivelyNonCommitted. -/
+def NS_ID_DEF_INTERPRETIVELY_NON_COMMITTED : String :=
+  "NS.DEF.INTERPRETIVELY_NON_COMMITTED"
+
 
 -- ============================================================
 -- AXIOMS
@@ -131,5 +135,10 @@ def NS_ID_THEOREM_FRAMEWORK_CONTESTABILITY : String :=
 def NS_ID_THEOREM_SEPARATE_STABILITY : String :=
   "NS.THEOREM.SEPARATE_STABILITY"
 
+/-- Cite when a regime depends on the result that only-neutral substrates satisfy INC.
+    This theorem confirms no new axiom is needed for the INC direction. -/
+def NS_ID_THEOREM_ONLY_NEUTRAL_IMPLIES_INC : String :=
+  "NS.THEOREM.ONLY_NEUTRAL_IMPLIES_INC"
+
 
 end SE.NeutralSubstrate.Spec