Skip to content

Commit 12de6ab

Browse files
denisecasedenisecase
committed
reference and ref validation
1 parent 296ba49 commit 12de6ab

16 files changed

Lines changed: 1085 additions & 19 deletions

‎CHANGELOG.md‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,30 @@ All notable changes to this project will be documented in this file.
77
The format is based on **[Keep a Changelog](https://keepachangelog.com/en/1.1.0/)**
88
and this project adheres to **[Semantic Versioning](https://semver.org/spec/v2.0.0.html)**.
99

10+
---
11+
1012
## [Unreleased]
1113

14+
### Added
15+
16+
- Added `reference/` artifacts for the Neutral Substrate public theory surface.
17+
- Added `reference/index.toml` to declare machine-readable reference artifacts.
18+
- Added reference validation for:
19+
- `reference/index.toml` structure.
20+
- declared artifact paths.
21+
- declared artifact formats.
22+
- Lean public surface coverage.
23+
- Added `lean_surface.py` to mirror the exported symbols from `NeutralSubstrate/Surface.lean`.
24+
- Added `paths.py` for repository path helpers used by reference validation.
25+
- Added `proof-registry.json` as the planned Lean-generated proof metadata artifact.
26+
27+
### Changed
28+
29+
- Extended repository validation to include the `reference/` artifact surface.
30+
- Updated validation output to show each reference validation step explicitly.
31+
32+
---
33+
1234
## [0.4.0] - 2026-05-01
1335

1436
### Added

‎reference/dependency-registry.toml‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
# ============================================================
2+
# Dependency Registry
3+
# se-theory-neutral-substrate
4+
# ============================================================
5+
6+
schema = "se-dependency-registry-1"
7+
repo = "se-theory-neutral-substrate"
8+
9+
[dependency.se_manifest_schema]
10+
id = "se-manifest-schema"
11+
target_repo = "se-manifest-schema"
12+
dependency_kind = "schema"
13+
required = true
14+
description = "Neutral substrate repo declares conformance through the shared SE manifest schema."
15+
16+
[dependency.no_identity_regimes_dependency]
17+
id = "no-identity-regimes-dependency"
18+
target_repo = "se-theory-identity-regimes"
19+
dependency_kind = "forbidden-formal-theory-dependency"
20+
required = false
21+
allowed = false
22+
description = "Neutral substrate must not depend on identity regimes; regimes build on the neutral substrate, not the reverse."
23+
24+
[dependency.no_structural_explainability_dependency]
25+
id = "no-structural-explainability-dependency"
26+
target_repo = "se-theory-structural-explainability"
27+
dependency_kind = "forbidden-formal-theory-dependency"
28+
required = false
29+
allowed = false
30+
description = "Neutral substrate must not depend on structural explainability integration theory."

‎reference/index.toml‎

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
# ============================================================
2+
# Reference Artifact Index
3+
# se-theory-neutral-substrate
4+
# ============================================================
5+
6+
schema = "se-reference-index-1"
7+
repo = "se-theory-neutral-substrate"
8+
ref_kind = "formal-theory-reference"
9+
surface_module = "NeutralSubstrate.Surface"
10+
11+
[[artifact]]
12+
id = "substrate-types"
13+
path = "reference/substrate-types.toml"
14+
kind = "substrate-type-registry"
15+
format = "toml"
16+
generated = false
17+
required = true
18+
19+
[[artifact]]
20+
id = "substrate-predicates"
21+
path = "reference/substrate-predicates.toml"
22+
kind = "substrate-predicate-registry"
23+
format = "toml"
24+
generated = false
25+
required = true
26+
27+
[[artifact]]
28+
id = "substrate-axioms"
29+
path = "reference/substrate-axioms.toml"
30+
kind = "substrate-axiom-registry"
31+
format = "toml"
32+
generated = false
33+
required = true
34+
35+
[[artifact]]
36+
id = "substrate-theorems"
37+
path = "reference/substrate-theorems.toml"
38+
kind = "substrate-theorem-registry"
39+
format = "toml"
40+
generated = false
41+
required = true
42+
43+
[[artifact]]
44+
id = "proof-registry"
45+
path = "reference/proof-registry.json"
46+
kind = "proof-registry"
47+
format = "json"
48+
generated = true
49+
generator = "lean4"
50+
required = true
51+
52+
[[artifact]]
53+
id = "dependency-registry"
54+
path = "reference/dependency-registry.toml"
55+
kind = "dependency-registry"
56+
format = "toml"
57+
generated = false
58+
required = true
59+
60+
[[artifact]]
61+
id = "traceability-registry"
62+
path = "reference/traceability-registry.toml"
63+
kind = "traceability-registry"
64+
format = "toml"
65+
generated = false
66+
required = true

‎reference/proof-registry.json‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
{
2+
"schema": "se-proof-registry-1",
3+
"repo": "se-theory-neutral-substrate",
4+
"surface_module": "NeutralSubstrate.Surface",
5+
"namespace": "SE.NeutralSubstrate",
6+
"proof_system": "lean4",
7+
"proofs": [
8+
{
9+
"id": "proof_not_neutral_if_causal_or_normative",
10+
"theorem_id": "not_neutral_if_causal_or_normative",
11+
"cite_id": "NS.THEOREM.not_neutral_if_causal_or_normative",
12+
"status": "proved",
13+
"lean_symbol": "not_neutral_if_causal_or_normative",
14+
"source_module": "NeutralSubstrate.Core"
15+
},
16+
{
17+
"id": "proof_neutral_if_only_neutral",
18+
"theorem_id": "neutral_if_only_neutral",
19+
"cite_id": "NS.THEOREM.neutral_if_only_neutral",
20+
"status": "proved",
21+
"lean_symbol": "neutral_if_only_neutral",
22+
"source_module": "NeutralSubstrate.Core"
23+
},
24+
{
25+
"id": "proof_ontological_neutrality_theorem",
26+
"theorem_id": "ontological_neutrality_theorem",
27+
"cite_id": "NS.THEOREM.ontological_neutrality_theorem",
28+
"status": "proved",
29+
"lean_symbol": "ontological_neutrality_theorem",
30+
"source_module": "NeutralSubstrate.Core"
31+
},
32+
{
33+
"id": "proof_only_neutral_primitives_implies_INC",
34+
"theorem_id": "only_neutral_primitives_implies_INC",
35+
"cite_id": "NS.THEOREM.only_neutral_primitives_implies_INC",
36+
"status": "proved",
37+
"lean_symbol": "only_neutral_primitives_implies_INC",
38+
"source_module": "NeutralSubstrate.Core"
39+
},
40+
{
41+
"id": "proof_framework_contestability_lemma",
42+
"theorem_id": "framework_contestability_lemma",
43+
"cite_id": "NS.THEOREM.framework_contestability_lemma",
44+
"status": "proved",
45+
"lean_symbol": "framework_contestability_lemma",
46+
"source_module": "NeutralSubstrate.Core"
47+
},
48+
{
49+
"id": "proof_separate_stability",
50+
"theorem_id": "separate_stability",
51+
"cite_id": "NS.THEOREM.separate_stability",
52+
"status": "proved",
53+
"lean_symbol": "separate_stability",
54+
"source_module": "NeutralSubstrate.Core"
55+
}
56+
]
57+
}

‎reference/substrate-axioms.toml‎

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
1+
# ============================================================
2+
# Neutral Substrate Axioms
3+
# se-theory-neutral-substrate
4+
# ============================================================
5+
6+
schema = "se-substrate-axiom-registry-1"
7+
repo = "se-theory-neutral-substrate"
8+
surface_module = "NeutralSubstrate.Surface"
9+
namespace = "SE.NeutralSubstrate"
10+
11+
[axiom.framework_relativity]
12+
id = "framework_relativity"
13+
cite_id = "NS.AXIOM.framework_relativity"
14+
name = "Framework relativity"
15+
lean_symbol = "framework_relativity"
16+
source_module = "NeutralSubstrate.Core"
17+
description = "Axiom expressing that relevant neutrality or interpretation claims may be relative to a framework."
18+
19+
[axiom.neutral_primitives_undisputed]
20+
id = "neutral_primitives_undisputed"
21+
cite_id = "NS.AXIOM.neutral_primitives_undisputed"
22+
name = "Neutral primitives undisputed"
23+
lean_symbol = "neutral_primitives_undisputed"
24+
source_module = "NeutralSubstrate.Core"
25+
description = "Axiom asserting the availability or undisputed status of neutral primitives."
26+
27+
[axiom.causal_normative_affirmed]
28+
id = "causal_normative_affirmed"
29+
cite_id = "NS.AXIOM.causal_normative_affirmed"
30+
name = "Causal or normative affirmed"
31+
lean_symbol = "causal_normative_affirmed"
32+
source_module = "NeutralSubstrate.Core"
33+
description = "Axiom identifying when causal or normative commitment is affirmed."

‎reference/substrate-predicates.toml‎

Lines changed: 73 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,73 @@
1+
# ============================================================
2+
# Neutral Substrate Predicates
3+
# se-theory-neutral-substrate
4+
# ============================================================
5+
6+
schema = "se-substrate-predicate-registry-1"
7+
repo = "se-theory-neutral-substrate"
8+
surface_module = "NeutralSubstrate.Surface"
9+
namespace = "SE.NeutralSubstrate"
10+
11+
[predicate.Admissible]
12+
id = "Admissible"
13+
cite_id = "NS.DEF.Admissible"
14+
name = "Admissible"
15+
lean_symbol = "Admissible"
16+
source_module = "NeutralSubstrate.Core"
17+
description = "Predicate indicating that a framework or substrate satisfies the conditions required for downstream regime reasoning."
18+
19+
[predicate.containsCausalOrNormative]
20+
id = "containsCausalOrNormative"
21+
cite_id = "NS.DEF.containsCausalOrNormative"
22+
name = "Contains causal or normative commitment"
23+
lean_symbol = "containsCausalOrNormative"
24+
source_module = "NeutralSubstrate.Core"
25+
description = "Predicate indicating that an ontology or framework contains causal or normative commitments."
26+
27+
[predicate.extensionInconsistent]
28+
id = "extensionInconsistent"
29+
cite_id = "NS.DEF.extensionInconsistent"
30+
name = "Extension inconsistent"
31+
lean_symbol = "extensionInconsistent"
32+
source_module = "NeutralSubstrate.Core"
33+
description = "Predicate indicating inconsistency under extension."
34+
35+
[predicate.ExtensionStable]
36+
id = "ExtensionStable"
37+
cite_id = "NS.DEF.ExtensionStable"
38+
name = "Extension stable"
39+
lean_symbol = "ExtensionStable"
40+
source_module = "NeutralSubstrate.Core"
41+
description = "Predicate indicating stability under extension."
42+
43+
[predicate.Neutral]
44+
id = "Neutral"
45+
cite_id = "NS.DEF.Neutral"
46+
name = "Neutral"
47+
lean_symbol = "Neutral"
48+
source_module = "NeutralSubstrate.Core"
49+
description = "Predicate indicating that the substrate or framework remains neutral with respect to causal, normative, or domain-specific interpretive commitments."
50+
51+
[predicate.FrameworkVariant]
52+
id = "FrameworkVariant"
53+
cite_id = "NS.DEF.FrameworkVariant"
54+
name = "Framework variant"
55+
lean_symbol = "FrameworkVariant"
56+
source_module = "NeutralSubstrate.Core"
57+
description = "Predicate or relation identifying a framework variant."
58+
59+
[predicate.FrameworksContradict]
60+
id = "FrameworksContradict"
61+
cite_id = "NS.DEF.FrameworksContradict"
62+
name = "Frameworks contradict"
63+
lean_symbol = "FrameworksContradict"
64+
source_module = "NeutralSubstrate.Core"
65+
description = "Predicate indicating contradiction between frameworks."
66+
67+
[predicate.InterpretivelyNonCommitted]
68+
id = "InterpretivelyNonCommitted"
69+
cite_id = "NS.DEF.InterpretivelyNonCommitted"
70+
name = "Interpretively non-committed"
71+
lean_symbol = "InterpretivelyNonCommitted"
72+
source_module = "NeutralSubstrate.Core"
73+
description = "Predicate indicating absence of interpretive commitment beyond the neutral structural substrate."

‎reference/substrate-theorems.toml‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
# ============================================================
2+
# Neutral Substrate Theorems
3+
# se-theory-neutral-substrate
4+
# ============================================================
5+
6+
schema = "se-substrate-theorem-registry-1"
7+
repo = "se-theory-neutral-substrate"
8+
surface_module = "NeutralSubstrate.Surface"
9+
namespace = "SE.NeutralSubstrate"
10+
11+
[theorem.not_neutral_if_causal_or_normative]
12+
id = "not_neutral_if_causal_or_normative"
13+
cite_id = "NS.THEOREM.not_neutral_if_causal_or_normative"
14+
name = "Not neutral if causal or normative"
15+
lean_symbol = "not_neutral_if_causal_or_normative"
16+
source_module = "NeutralSubstrate.Core"
17+
status = "proved"
18+
description = "If causal or normative commitment is present, the relevant substrate or framework is not neutral."
19+
20+
[theorem.neutral_if_only_neutral]
21+
id = "neutral_if_only_neutral"
22+
cite_id = "NS.THEOREM.neutral_if_only_neutral"
23+
name = "Neutral if only neutral"
24+
lean_symbol = "neutral_if_only_neutral"
25+
source_module = "NeutralSubstrate.Core"
26+
status = "proved"
27+
description = "If only neutral primitives or commitments are present, the relevant substrate or framework is neutral."
28+
29+
[theorem.ontological_neutrality_theorem]
30+
id = "ontological_neutrality_theorem"
31+
cite_id = "NS.THEOREM.ontological_neutrality_theorem"
32+
name = "Ontological neutrality theorem"
33+
lean_symbol = "ontological_neutrality_theorem"
34+
source_module = "NeutralSubstrate.Core"
35+
status = "proved"
36+
description = "Main theorem establishing ontological neutrality under the required neutral-substrate conditions."
37+
38+
[theorem.only_neutral_primitives_implies_INC]
39+
id = "only_neutral_primitives_implies_INC"
40+
cite_id = "NS.THEOREM.only_neutral_primitives_implies_INC"
41+
name = "Only neutral primitives implies interpretive non-commitment"
42+
lean_symbol = "only_neutral_primitives_implies_INC"
43+
source_module = "NeutralSubstrate.Core"
44+
status = "proved"
45+
description = "If only neutral primitives are present, interpretive non-commitment follows."
46+
47+
[theorem.framework_contestability_lemma]
48+
id = "framework_contestability_lemma"
49+
cite_id = "NS.THEOREM.framework_contestability_lemma"
50+
name = "Framework contestability lemma"
51+
lean_symbol = "framework_contestability_lemma"
52+
source_module = "NeutralSubstrate.Core"
53+
status = "proved"
54+
description = "Lemma supporting contestability or relativity among frameworks."
55+
56+
[theorem.separate_stability]
57+
id = "separate_stability"
58+
cite_id = "NS.THEOREM.separate_stability"
59+
name = "Separate stability"
60+
lean_symbol = "separate_stability"
61+
source_module = "NeutralSubstrate.Core"
62+
status = "proved"
63+
description = "Theorem or lemma establishing separate stability under the relevant neutral-substrate conditions."

0 commit comments

Comments
 (0)