add theory

Author: denisecase

.pre-commit-config.yaml

@@ -36,6 +36,7 @@ exclude: |
     build/|
     coverage\.xml|
     dist/|
+    external/se-formal-contract/|
     htmlcov/|
     lake-packages/|
     node_modules/|
@@ -65,9 +66,9 @@ repos:
       # === PRE-COMMIT: CHECK DATA FILE FORMATS ===
 
       - id: check-json
-        name: B1) Validate JSON syntax (except .vscode/)
-        # WHY: VSCode settings may include comments, which are non-standard JSON.
-        exclude: ^\.vscode/.*\.json$
+        name: B1) Validate JSON syntax (except .vscode/ and external/)
+        # WHY: VSCode settings may include comments; external/ contains submodules not owned by this repo.
+        exclude: ^(\.vscode/.*\.json|external/.*\.json)$
 
       - id: check-toml
         name: B2) Validate TOML syntax

CHANGELOG.md

@@ -1,12 +1,43 @@
 # Changelog
 
+<!-- markdownlint-disable MD024 -->
+
 All notable changes to this project will be documented in this file.
 
 The format is based on **[Keep a Changelog](https://keepachangelog.com/en/1.1.0/)**
 and this project adheres to **[Semantic Versioning](https://semver.org/spec/v2.0.0.html)**.
 
 ## [Unreleased]
 
+### Added
+
+New repository class:
+
+- `theory` — Lean 4 theorem-development repositories for Structural Explainability theory
+
+Naming pattern support for `theory`:
+
+- `se-theory-{focus}`
+
+Dependency rules:
+
+- `theory` may depend on `formal_contract`
+- `theory` does not introduce upstream dependencies into the foundation layer
+
+Repository requirements for `theory`:
+
+- Lean 4 project structure (`lean-toolchain`, `lakefile.toml`)
+- Lean module root (e.g., `SETheory`)
+- documentation (`docs/`)
+- no required data export directories
+
+Design clarification:
+
+- separation of concerns between:
+  - theory repos (proof development)
+  - formal contract (stable exported surface)
+  - constitution (operational validation)
+
 ---
 
 ## [0.1.1] - 2026-04-27
@@ -22,7 +53,8 @@ Naming pattern support for `govsrc`:
 
 - `se-govsrc-{jurisdiction}`
 - `se-govsrc-{jurisdiction}-{focus}`
-- Clarified that `{jurisdiction}` may include subdivision (e.g., `us-missouri`) and is treated as a single logical token
+- Clarified that `{jurisdiction}` may include
+  subdivision (e.g., `us-missouri`) and is treated as a single logical token
 
 Dependency rules for new classes:
 

CITATION.cff

@@ -9,8 +9,8 @@ cff-version: "1.2.0"
 type: software
 
 title: "Structural Explainability Constitution"
-version: "0.1.0"
-date-released: "2026-04-22"
+version: "0.1.1"
+date-released: "2026-04-27"
 
 authors:
   - family-names: Case

README.md

@@ -33,12 +33,10 @@ se-admin
 
 ### In a machine terminal
 
-After you get a copy of this repo in your own GitHub account,
-open a machine terminal in `Repos` or where you want the project:
+Open a machine terminal where you want the project:
 
 ```shell
-# Replace username with YOUR GitHub username.
-git clone https://github.com/username/se-constitution
+git clone https://github.com/structural-explainability/se-constitution
 
 cd se-constitution
 code .
@@ -51,6 +49,8 @@ uv self update
 uv python pin 3.15
 uv sync --extra dev --extra docs --upgrade
 
+git submodule update --init --recursive
+
 uvx pre-commit install
 
 git add -A

data/class/class-registry.toml

@@ -8,6 +8,14 @@ version = "0.1.0"
 status = "draft"
 title = "SE Constitution Class Registry"
 
+[class.formal_contract]
+label = "Formal Contract"
+description = "Lean 4-verified formal contract exporting invariants, regimes, relations, and proof status to operational SE repositories."
+
+[class.theory]
+label = "Theory"
+description = "Lean 4 theorem-development repositories for Structural Explainability theory."
+
 [class.constitution]
 summary = "Architectural law and governing definitions for the SE ecosystem."
 stable = true

data/dependency/dependency-rules.toml

@@ -12,13 +12,24 @@ status = "draft"
 title = "SE Constitution Dependency Rules"
 
 [principle]
+formal_contract_is_root = true
 no_cycles = true
 no_reverse_foundation_dependencies = true
 constitution_is_foundational = true
 
-[dependency.constitution]
+[dependency.formal_contract]
 allowed = []
 
+[dependency.theory]
+allowed = [
+    "formal_contract",
+]
+
+[dependency.constitution]
+allowed = [
+    "formal_contract",
+]
+
 [dependency.admin]
 allowed = [
     "adapter",

data/manifest/manifest-schema.toml

@@ -34,84 +34,59 @@ schema_url_required = true
 required = true
 description = "Non-normative contextual information about the manifest and framework."
 allowed_fields = [
-  "framework",
-  "framework_url",
-  "framework_note",
-  "description",
-  "purpose"
+    "framework",
+    "framework_url",
+    "framework_note",
+    "description",
+    "purpose",
 ]
 
 [section.repo]
 required = true
 description = "Stable repository identity and declared class."
-allowed_fields = [
-  "name",
-  "org",
-  "class",
-  "kind",
-  "status",
-  "since",
-  "summary"
-]
+allowed_fields = ["name", "org", "class", "kind", "status", "since", "summary"]
 
 [section.layer]
 required = true
 description = "Declared epistemic position."
-allowed_fields = [
-  "space",
-  "role"
-]
+allowed_fields = ["space", "role"]
 
 [section.depends]
 required = true
 description = "Declared upstream dependencies."
-allowed_fields = [
-  "required",
-  "optional"
-]
+allowed_fields = ["required", "optional"]
 
 [section.provides]
 required = true
 description = "Artifacts intentionally provided and maintained."
-allowed_fields = [
-  "artifacts"
-]
+allowed_fields = ["artifacts"]
 
 [section.scope]
 required = true
 description = "Explicit semantic boundary."
-allowed_fields = [
-  "includes",
-  "excludes"
-]
+allowed_fields = ["includes", "excludes"]
 
 [section.compatibility]
 required = false
 description = "Declared compatibility with constitutional and ecosystem components."
 allowed_fields = [
-  "constitution",
-  "kernel",
-  "mapspec",
-  "schema",
-  "profile",
-  "rules"
+    "constitution",
+    "kernel",
+    "mapspec",
+    "schema",
+    "profile",
+    "rules",
 ]
 
 [section.citation]
 required = true
 description = "Citation pointer metadata."
-allowed_fields = [
-  "cff",
-  "preferred",
-  "bib_hint"
-]
+allowed_fields = ["cff", "preferred", "bib_hint"]
 
 [section.traceability]
 required = true
 description = "Identifier resolution and traceability strategy."
-allowed_fields = [
-  "identifier_map"
-]
+allowed_fields = ["identifier_map"]
 
 # ------------------------------------------------------------
 # Field definitions
@@ -226,6 +201,18 @@ required = true
 # Class-specific requirements
 # ------------------------------------------------------------
 
+[class.formal_contract]
+required_repo_name_patterns = ["se-formal-contract"]
+required_layer_roles = ["formal-contract"]
+forbidden_sections = []
+required_compatibility_fields = []
+
+[class.theory]
+required_repo_name_patterns = ["se-theory-{focus}"]
+required_layer_roles = ["theory"]
+forbidden_sections = []
+required_compatibility_fields = []
+
 [class.constitution]
 required_repo_name_patterns = ["se-constitution"]
 required_layer_roles = ["constitution"]
@@ -275,7 +262,10 @@ forbidden_sections = []
 required_compatibility_fields = ["constitution", "kernel"]
 
 [class.profile]
-required_repo_name_patterns = ["se-profile-{jurisdiction}", "se-profile-{jurisdiction}-{focus}"]
+required_repo_name_patterns = [
+    "se-profile-{jurisdiction}",
+    "se-profile-{jurisdiction}-{focus}",
+]
 required_layer_roles = ["profile"]
 forbidden_sections = []
 required_compatibility_fields = ["constitution", "kernel", "schema"]
@@ -286,10 +276,19 @@ optional_sections = ["validation", "naming", "governance", "traceability"]
 
 [class.govsrc]
 required_sections = ["meta", "repo", "provides", "scope", "citation"]
-optional_sections = ["depends", "validation", "naming", "governance", "traceability"]
+optional_sections = [
+    "depends",
+    "validation",
+    "naming",
+    "governance",
+    "traceability",
+]
 
 [class.rules]
-required_repo_name_patterns = ["se-rules-{jurisdiction}", "se-rules-{jurisdiction}-{focus}"]
+required_repo_name_patterns = [
+    "se-rules-{jurisdiction}",
+    "se-rules-{jurisdiction}-{focus}",
+]
 required_layer_roles = ["rules"]
 forbidden_sections = []
 required_compatibility_fields = ["constitution", "kernel", "schema"]
@@ -330,10 +329,10 @@ empty_required_lists_allowed = true
 [notes]
 manifest_role = "Declares repository intent, scope, role, and compatibility under constitutional law."
 non_goals = [
-  "build configuration",
-  "deployment configuration",
-  "runtime secrets",
-  "replace README documentation",
-  "replace CITATION.cff",
-  "duplicate constitutional law tables"
+    "build configuration",
+    "deployment configuration",
+    "runtime secrets",
+    "replace README documentation",
+    "replace CITATION.cff",
+    "duplicate constitutional law tables",
 ]

data/naming/naming-patterns.toml

@@ -24,6 +24,15 @@ domain_pattern = "[a-z0-9]+(?:-[a-z0-9]+)*"
 focus_pattern = "[a-z0-9]+(?:-[a-z0-9]+)*"
 standard_pattern = "[a-z0-9]+(?:-[a-z0-9]+)*"
 
+[pattern.formal_contract]
+class = "formal_contract"
+format = "se-formal-contract"
+
+[pattern.theory]
+class = "theory"
+format = "se-theory-{focus}"
+required_tokens = ["focus"]
+
 [pattern.constitution]
 class = "constitution"
 format = "se-constitution"

data/repo/repo-requirements.toml

@@ -57,6 +57,50 @@ schema = "se-manifest-2"
 require_ci = true
 require_manifest_validation = true
 
+# ------------------------------------------------------------
+# Formal Contract
+# ------------------------------------------------------------
+
+[repo.formal_contract]
+summary = "Lean 4-verified formal contract exporting invariants, regimes, relations, and proof status to operational SE repositories."
+
+required_files = [
+  "SE_MANIFEST.toml",
+  "README.md",
+  "CHANGELOG.md",
+  "CITATION.cff",
+  "lean-toolchain",
+  "lakefile.toml",
+]
+
+required_directories = [
+  "SEFormalContract",
+  "data/contract",
+  "docs",
+]
+
+# ------------------------------------------------------------
+# Theory
+# ------------------------------------------------------------
+
+[repo.theory]
+summary = "Lean 4 theorem development repositories for Structural Explainability theory."
+
+required_files = [
+  "SE_MANIFEST.toml",
+  "README.md",
+  "CHANGELOG.md",
+  "CITATION.cff",
+  "lean-toolchain",
+  "lakefile.toml",
+]
+
+required_directories = [
+  "SETheory",
+  "docs",
+]
+
+
 # ------------------------------------------------------------
 # Constitution
 # ------------------------------------------------------------