Skip to content

Commit 5ff73a7

Browse files
denisecasedenisecase
committed
folders
1 parent de825fb commit 5ff73a7

16 files changed

Lines changed: 305 additions & 108 deletions

‎AccountableEntities.lean‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
import AccountableEntities.Conformance
2+
import AccountableEntities.Core
3+
import AccountableEntities.Spec
4+
5+
6+
/-!
7+
REQ.PUBLIC.SURFACE:
8+
Canonical public import surface for this package.
9+
Do not add any declarations here.
10+
Do not add empty namespaces.
11+
12+
WHY:
13+
Downstream projects should have exactly one stable import path for this repo.
14+
15+
OBS:
16+
- This module re-exports the intended public modules by importing them.
17+
- It must not define placeholder namespaces.
18+
- All exported declarations live in imported modules.
19+
-/

StructuralExplainability/AccountableEntities/Spec/Conformance.lean renamed to AccountableEntities/Conformance.lean

Lines changed: 65 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -1,44 +1,52 @@
1-
import StructuralExplainability.AccountableEntities.Spec.Kind
2-
import StructuralExplainability.AccountableEntities.Spec.KindNames
1+
import AccountableEntities.Spec.Kind
2+
import AccountableEntities.Spec.KindNames
33

4-
namespace StructuralExplainability.AccountableEntities.Spec
4+
namespace AccountableEntities.Conformance
55

66
/-!
7-
Accountable Entities (AE) -- Conformance Predicate (v1, named kinds)
8-
9-
This file keeps the internal Kind constructors as K1..K6 for stability,
10-
and introduces named kind requirements at the specification layer.
11-
12-
Names are mapped to K1..K6 using abbrev declarations in:
13-
- AccountableEntities/Spec/KindNames.lean
14-
15-
Conformance evidence fields and requirement names align with AE SPEC.md
16-
identifiers (AE.KIND.ACTOR, AE.KIND.LOCUS, etc.).
7+
# Accountable Entities (AE) Conformance Predicate Surface (v1)
8+
9+
REQ:
10+
Provide a single, deterministic, identifier-aligned conformance surface for AE v1.
11+
12+
WHY:
13+
AE identifiers are the sole normative references across prose, schema, and proof.
14+
Lean conformance evidence must therefore be keyed to the canonical identifiers,
15+
not to human-friendly names that may change.
16+
17+
OBS:
18+
- The canonical AE kind constructors are `Kind.K1 .. Kind.K6`.
19+
- Human-readable kind names (Actor/Locus/...) are definitional abbreviations only,
20+
defined in `AccountableEntities/Spec/KindNames.lean`.
21+
- Canonical AE v1 kind identifiers are `AE.KIND.K1 .. AE.KIND.K6`.
22+
- This file does not assign domain semantics; it only provides structural shapes.
1723
-/
1824

25+
1926
/-- Conjunction of a list of propositions. -/
2027
def AndList : List Prop -> Prop
2128
| [] => True
2229
| p :: ps => p ∧ AndList ps
2330

2431
section
2532

26-
/- Placeholder wiring: integrate with SE later. -/
27-
variable {SEEvidence : Type}
28-
29-
/- Placeholder: "this artifact conforms to SE". Replace with SE.Conforms. -/
30-
variable (SEConforms : SEEvidence -> Prop)
31-
3233
/- Abstract identity regime type (left uninterpreted at this layer). -/
3334
variable (Regime : Type)
3435

3536
/- Kind-to-regime mapping. -/
3637
variable (kindToRegime : Kind -> Regime)
3738

3839
/-
39-
AE v1 requirements as stable propositions.
40+
REQ.AE.CONFORMANCE.EVIDENCE:
41+
AE v1 requirements as stable propositions.
42+
43+
WHY:
44+
Fields are the Lean-level mirror of identifiers. This supports:
45+
- deterministic "exactly once" traceability, and
46+
- stable referencing from other Lean modules without relying on prose order.
4047
41-
Fields are alphabetized by identifier name to reduce editorial discretion.
48+
OBS:
49+
Fields are alphabetized by canonical identifier name to reduce editorial discretion.
4250
-/
4351
structure ConformanceEvidence where
4452
AE_CONFORMANCE_SE_REQUIRED : Prop
@@ -48,38 +56,53 @@ structure ConformanceEvidence where
4856
AE_IDENTITY_REGIME_MAPPING : Prop
4957
AE_KIND_CLOSED_SET_V1 : Prop
5058
AE_KIND_EXACT_COUNT_V1 : Prop
59+
AE_KIND_K1 : Prop
60+
AE_KIND_K2 : Prop
61+
AE_KIND_K3 : Prop
62+
AE_KIND_K4 : Prop
63+
AE_KIND_K5 : Prop
64+
AE_KIND_K6 : Prop
65+
AE_SCOPE_EXCLUSIONS : Prop
5166

52-
AE_KIND_ACTOR : Prop
53-
AE_KIND_EVENT : Prop
54-
AE_KIND_INSTRUMENT : Prop
55-
AE_KIND_LOCUS : Prop
56-
AE_KIND_OBSERVATION : Prop
57-
AE_KIND_SCOPE : Prop
67+
/-
68+
REQ.AE.CONFORMANCE.REQUIREMENTS_LIST:
5869
59-
AE_SCOPE_EXCLUSIONS : Prop
70+
WHY:
71+
Conformance is defined as conjunction over this list.
72+
The list must preserve the same canonical, alphabetical order used everywhere else.
6073
74+
OBS:
75+
Alphabetical order here is by identifier string, not by KindNames.
76+
-/
6177
/-- Alphabetized requirements list for AE v1. -/
6278
def requirements (e : ConformanceEvidence) : List Prop :=
6379
[ e.AE_CONFORMANCE_SE_REQUIRED
6480
, e.AE_DEFINITION_CORE
6581
, e.AE_EXTENSION_ADMISSIBILITY
6682
, e.AE_EXTENSION_VERSIONED_ONLY
6783
, e.AE_IDENTITY_REGIME_MAPPING
68-
, e.AE_KIND_ACTOR
6984
, e.AE_KIND_CLOSED_SET_V1
70-
, e.AE_KIND_EVENT
7185
, e.AE_KIND_EXACT_COUNT_V1
72-
, e.AE_KIND_INSTRUMENT
73-
, e.AE_KIND_LOCUS
74-
, e.AE_KIND_OBSERVATION
75-
, e.AE_KIND_SCOPE
86+
, e.AE_KIND_K1
87+
, e.AE_KIND_K2
88+
, e.AE_KIND_K3
89+
, e.AE_KIND_K4
90+
, e.AE_KIND_K5
91+
, e.AE_KIND_K6
7692
, e.AE_SCOPE_EXCLUSIONS
7793
]
7894

7995
/-- AE conformance predicate: all AE requirements hold. -/
8096
def Conforms (e : ConformanceEvidence) : Prop :=
8197
AndList (requirements e)
8298

99+
/-
100+
REQ.AE.CONFORMANCE.EXTRACTOR:
101+
102+
WHY:
103+
Conformance evidence is often consumed indirectly.
104+
This lemma provides a stable way to extract any required proposition from Conforms.
105+
-/
83106
/- If `AndList ps` holds, then every member of `ps` holds. -/
84107
theorem andList_of_mem {ps : List Prop} {p : Prop} :
85108
p ∈ ps -> AndList ps -> p := by
@@ -105,14 +128,20 @@ theorem andList_of_mem {ps : List Prop} {p : Prop} :
105128
theorem conforms_of_mem (e : ConformanceEvidence) (p : Prop) :
106129
p ∈ requirements e -> Conforms e -> p := by
107130
intro hmem hconf
108-
-- unfold Conforms to get AndList (requirements e)
109131
unfold Conforms at hconf
110132
exact andList_of_mem (ps := requirements e) (p := p) hmem hconf
111133

134+
/-
135+
REQ.AE.IDENTITY.REGIME.MAPPING.INJECTIVE:
136+
137+
WHY:
138+
AE requires distinct kinds to correspond to distinct identity regimes.
139+
This is one structurally checkable formulation of that requirement.
140+
-/
112141
/-- Injectivity of kind->regime (distinct kinds correspond to distinct regimes). -/
113142
def kindToRegimeInjective : Prop :=
114143
Function.Injective kindToRegime
115144

116145
end
117146

118-
end StructuralExplainability.AccountableEntities.Spec
147+
end AccountableEntities.Conformance

‎AccountableEntities/Core.lean‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
import AccountableEntities.Core.Coverage
2+
import AccountableEntities.Core.EntityKinds
3+
import AccountableEntities.Core.MappingJustification
4+
import AccountableEntities.Core.RegimeMapping
5+
6+
/-!
7+
REQ.PUBLIC.SURFACE:
8+
Canonical public import surface for this layer.
9+
Do not add any declarations here.
10+
Do not add empty namespaces.
11+
12+
WHY:
13+
Downstream layers should have exactly one stable import path for this layer.
14+
15+
OBS:
16+
- This module re-exports the intended public modules by importing them.
17+
- It must not define placeholder namespaces.
18+
- All exported declarations live in imported modules.
19+
-/

StructuralExplainability/AccountableEntities/Coverage.lean renamed to AccountableEntities/Core/Coverage.lean

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
1-
-- StructuralExplainability/AccountableEntities/Coverage.lean
1+
import AccountableEntities.Core.RegimeMapping
2+
23
/-
34
Completeness and correctness proofs for the entity-kind -> identity-regime mapping.
45
@@ -12,9 +13,7 @@ Reminders:
1213
- A function is bijective if it is both injective and surjective.
1314
-/
1415

15-
import StructuralExplainability.AccountableEntities.RegimeMapping
16-
17-
namespace StructuralExplainability.AccountableEntities
16+
namespace AccountableEntities.Core
1817

1918
open NamedEntityKind
2019
open IdentityRegime
@@ -112,4 +111,4 @@ theorem regimeInstances_unique_length :
112111
intro r
113112
cases r <;> rfl
114113

115-
end StructuralExplainability.AccountableEntities
114+
end AccountableEntities.Core

StructuralExplainability/AccountableEntities/EntityKinds.lean renamed to AccountableEntities/Core/EntityKinds.lean

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,4 @@
1-
-- StructuralExplainability/AccountableEntities/EntityKinds.lean
2-
3-
namespace StructuralExplainability.AccountableEntities
1+
namespace AccountableEntities.Core
42

53
/--
64
Core named entity kinds derived from common entity recognition taxonomies
@@ -15,4 +13,4 @@ inductive NamedEntityKind where
1513
| Observation
1614
deriving Repr, BEq, DecidableEq
1715

18-
end StructuralExplainability.AccountableEntities
16+
end AccountableEntities.Core

StructuralExplainability/AccountableEntities/MappingJustification.lean renamed to AccountableEntities/Core/MappingJustification.lean

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,11 @@
1-
-- StructuralExplainability/AccountableEntities/MappingJustification.lean
1+
import AccountableEntities.Core.RegimeMapping
2+
23
/-
34
Semantic justification for entity-to-regime mappings.
45
Formalizes the rationale for why each entity kind maps to its assigned regime.
56
-/
67

7-
import StructuralExplainability.AccountableEntities.RegimeMapping
8-
9-
namespace StructuralExplainability.AccountableEntities
8+
namespace AccountableEntities.Core
109

1110
/--
1211
An entity is appropriately ActorBound when it exhibits agency and persistent identity.
@@ -174,4 +173,4 @@ theorem dataset_is_observation_bound : IsObservationBound datasetObservationJust
174173
unfold IsObservationBound datasetObservationJustification
175174
simp
176175

177-
end StructuralExplainability.AccountableEntities
176+
end AccountableEntities.Core

StructuralExplainability/AccountableEntities/RegimeMapping.lean renamed to AccountableEntities/Core/RegimeMapping.lean

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
1-
-- StructuralExplainability/AccountableEntities/RegimeMapping.lean
1+
import AccountableEntities.Core.EntityKinds
22

3-
import StructuralExplainability.AccountableEntities.EntityKinds
4-
5-
namespace StructuralExplainability.AccountableEntities
3+
namespace AccountableEntities.Core
64

75
/--
86
The six necessary and sufficient identity regimes from the proof series.
@@ -48,4 +46,4 @@ def regimeInstances (r : IdentityRegime) : List NamedEntityKind :=
4846
| .ScopeBound => [.Scope]
4947
| .ObservationBound => [.Observation]
5048

51-
end StructuralExplainability.AccountableEntities
49+
end AccountableEntities.Core

‎AccountableEntities/Spec.lean‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
import AccountableEntities.Spec.IdentifierMap
2+
import AccountableEntities.Spec.Kind
3+
import AccountableEntities.Spec.KindNames
4+
5+
/-!
6+
REQ.PUBLIC.SURFACE:
7+
Canonical public import surface for this layer.
8+
Do not add any declarations here.
9+
Do not add empty namespaces.
10+
11+
WHY:
12+
Downstream layers should have exactly one stable import path for this layer.
13+
14+
OBS:
15+
- This module re-exports the intended public modules by importing them.
16+
- It must not define placeholder namespaces.
17+
- All exported declarations live in imported modules.
18+
-/

0 commit comments

Comments
 (0)