Formal Theory: Structural Assurability

Lean 4 formalization of Structural Explainability's Structural Assurability theory.

For full documentation, see docs/en/index.md.

Candidate Structural Properties

Four candidate properties have dimension-specific, profile-grounded separating constructions: observability, evidence coverage, traceability, and reconstructability. These do not independently establish capability-profile non-equivalence or claim resolution.

Independence, integrity, and controllability do not yet have corresponding dimension-specific constructions.

For independence and integrity, establishing the assurance significance of a profile difference requires additional assumptions concerning evidence provenance, admissibility, and trust.

For controllability, connecting interventions to claim resolution requires representing how the evaluator's observations depend on permitted interventions and applicable resource constraints. The current claim-resolution model does not represent those interactions.

See Candidate Structural Properties.

Claim-Relative Assurance Limitation

If two admissible worlds disagree on a claim but produce identical observations under a specified observation model, that observation model cannot resolve the claim.

The approximation-transfer theorems establish conditions for transferring claim-resolution results between abstract and concrete models.

Applying a resolution-failure result to an operational system requires independent justification that the relevant worlds are realizable and that the modeled observations faithfully represent what the evaluator can observe.

Authority

Lean source files are authoritative for formal definitions, predicates, axioms, theorems, proof obligations, and reference rules.

Reference artifacts under reference/ declare the repository-owned classification, traceability, and export intent for the Lean public surface.

Generated artifacts under data/*/ are outputs. They do not define theory semantics independently of Lean or the reference artifacts.

The reusable se-theory-reference-kit owns the generic validation, cataloging, inspection, and export machinery. This repository owns its Lean source, reference declarations, and generated artifacts.

Repository Organization

SE/                     Lean authoritative theory
SETest/                 Lean verification surface
reference/              declared formal/reference intent
data/                    generated outputs, if/when needed
docs/en/                 human-readable theory documentation

Theory Layers

10  Foundation
20  Semantics
30  Core
40  Order
50  Candidate structural properties
60  General theorems
90  Representative examples

Example modules should declare the lower-level theory they directly depend on rather than assuming transitive imports.

Import

Downstream Lean projects should import the public surface:

import SE

Dependencies

The Structural Assurability formalization currently has no required cross-repository Lean theory dependencies.

Repository reference validation and export tooling is provided by se-theory-reference-kit.

Reference Configuration

The theory-reference workflow is configured by:

reference/theory-reference.toml

That file declares this repository's Lean public modules, reference artifact layout, export targets, and validation commands. Public symbols are declared in the reference artifacts.

Map

Paper concept                         Theory repo destination

Assurance context                     Layer10_Foundation / Context
System + claim                        Layer10_Foundation
Evidence                              Layer10_Foundation
Claim materiality                     Layer20_Semantics
Obtainable evidence                   Layer20_Semantics
Evidentiary capability Γ_C            Layer30_Core
Assurability A(S,C,K,B)               Layer30_Core
Evidence-capability preorder          Layer40_Order
Equivalence                           Layer40_Order
Dominance / incomparability           Layer40_Order
Candidate structural properties       Layer50_Properties
Access/resource propositions          Layer60_Theorems
Separating constructions              Layer60_Theorems
Architectural cases                   Layer90_Examples

Lean Formal Objects

Formal objects are either:

• API names whose implementations should remain hidden, defined with public def
• mathematical definitions whose bodies are part of the public theory, defined with public abbrev, such as: WorldSpace.unrestricted, indistinguishable, claimDisagreement, admissiblyIndistinguishable, claimResolvedBy, feasibleEvidence, accessibleEvidence, obtainableEvidence, claimMaterialEvidence, isSufficient, capabilities, systemCapabilities, profile, and structuralAssurability.

This distinction is intentional. Downstream theorem layers may unfold mathematical definitions, while implementation details of ordinary API definitions remain encapsulated.

Examples

Three examples come directly from the associated paper's application section:

• unauthorized consequential action → strict dominance
• externally observable output property → equivalence
• internal visibility versus independent evidence → incomparability

Case 1: strict dominance
        S_R ≻q S_A ≻q S_O

Case 2: equivalence
        S_O ~q S_A ~q S_R

Case 3: incomparability
        S_V ∥q S_N

and the indistinguishability result:

two admissible worlds
+ same obtainable observation
+ different claim truth
→ claim not resolvable

Note: For an existential/counterexample-style theorem, explicit witnesses may be better and more readable than asking elaboration to infer them.

Additional Examples

Two-sided approximation transfer

ApproximationTransfer.lean establishes conditions for transferring resolution and resolution-failure results between abstract and concrete models.

Witness-level realization requires exhibiting only one concrete resolution-failure witness rather than specifying a global mapping.

Under the current definitions, a global failure transfer can also be constructed classically from one realized witness. Neither construction independently establishes a faithful correspondence with an operational system.

Precinct vintage

PrecinctVintage.lean demonstrates why a self-reported vintage label cannot establish dataset currency when inaccurate labels are admissible. It formalizes the conditions under which labels and independent reference checks can resolve that claim, including explicit counterexamples when assumptions are dropped.

Deployment shift

DeploymentShift.lean provides an independent example. Offline accuracy metrics, drift monitoring and partial production labeling can all leave a deployment-accuracy claim unresolved. It also establishes resolution under specified coverage or representativeness assumptions.

Note: Global failure transfer supplies a witness-level realization, but we have not formally established that the witness-level condition is strictly weaker.

Adversarial Experiments (Python)

src/se_theory_structural_assurability/ contains finite-model experiments written in Python, not Lean. They stress-test candidate distinctions, e.g., whether a property is an evidence gap or a trust gap, against small, explicitly constructed worlds before such distinctions may be formalized.

These experiments are not part of the Lean theory. A result that survives here is a candidate for formalization, not a proof. See Authority.

An ObservationModel-style Channel declares which fields of a world it may read; its implementation receives only those fields, so it cannot read a hidden field or the claim itself. resolved() and witnesses() mirror the Lean theory's claimResolvedBy and ResolutionFailureWitness: worlds are grouped by what a set of channels observes, and a claim is unresolved wherever two worlds in the same group disagree on it.

Each scenario is self-contained: its own world type, its own claim, its own channels, and its own admissibility assumptions. Scenarios are added independently and do not compose or share structure with one another.

Motivation and Initial Findings

The experiments challenge candidate structural distinctions before committing them to the formal theory.

The initial scenarios distinguish an observability gap that can be resolved by additional evidence from integrity and independence cases in which additional observations may remain insufficient without appropriate trust or failure assumptions.

The integrity experiments show that detection can resolve a claim under specified conditions but can fail under lossy tampering or channel compromise. The independence experiments demonstrate that even agreeing reports can leave a claim unresolved when collusion is admissible.

These are constructive finite-model results, not general claims about operational systems or proofs that the candidate structural properties are independent.

See Adversarial Experiments for the research questions, experimental method, results, limitations, and next steps.

Running

uv run python -m se_theory_structural_assurability.run_experiment
uv run python -m pytest

run_experiment.py runs the current scenarios and prints, for each, which channel sets resolve the claim and a witness pair where they don't.

The tests/ suite asserts specific claims the experiments have established so far; a failing assertion means a scenario's result changed and any conclusion drawn from it should be re-checked before reuse elsewhere in the repository.

Developer

• Maintain lakefile.toml and lean-toolchain.

Command Reference

Show command reference

In a machine terminal

Open a machine terminal where you want the project:

git clone https://github.com/structural-explainability/se-theory-structural-assurability

cd se-theory-structural-assurability
code .

In a VS Code terminal

Use VS Code Menu: View / Command Palette / Developer: Reload Window to refresh.

.\rel.ps1

# save progress
git add -A
git commit -m "update"
git push -u origin main

Inspect Theory-Reference Commands

uv run --locked se-theory-reference --help
uv run --locked se-theory-reference validate --help
uv run --locked se-theory-reference export --help
uv run --locked se-theory-reference catalog --help
uv run --locked se-theory-reference inspect --help

Repair Dependency State

Use only when the normal update and build commands cannot repair the workspace:

Remove-Item -Recurse -Force .\.lake\packages\mathlib `
    -ErrorAction SilentlyContinue

Remove-Item -Force .\lake-manifest.json `
    -ErrorAction SilentlyContinue

lake update
lake exe cache get

Citation

CITATION.cff

License

MIT

Repository Manifest

SE_MANIFEST.toml