# Theoria validation

Theoria owns its validation corpus. External tools such as Lean consume this corpus, but they do not decide which examples, theorem modules, or reduction checks matter.

Run native validation with:

```bash
mix theoria.validate
```

Check a downstream theorem module with:

```bash
mix theoria.theorems MyApp.Proofs
```

To narrow the corpus while developing:

```bash
mix theoria.validate --only bool
mix theoria.validate --only nat,list
mix theoria.validate --only defeq
mix theoria.validate --only inductives
mix theoria.validate --axioms
```

## What is validated

`Theoria.Validation.Corpus` currently contains three kinds of checks:

| Check | Source | Native checker |
|---|---|---|
| Theorem modules | `Theoria.Library.*.Theorems` via `Theoria.Validation.TheoremModuleCheck` | `Theoria.Validation.Checkable` / `Theoria.Theorem.check_all/2` |
| Definitional equality | `%Theoria.Validation.DefeqCheck{}` | `Theoria.Validation.Checkable` / `Theoria.Normalize.defeq?/3` |
| Inductive specs | `%Theoria.Validation.InductiveCheck{}` | `Theoria.Validation.Checkable` / `Theoria.Inductive.check_spec/2` and `Theoria.Inductive.verify_env/2` |
| Explicit indexed matcher spec | Internal Vec matcher validation | `Theoria.Validation.IndexedMatchers` / `Theoria.Equation.Matcher.Indexed.Package` |

The default corpus covers Logic, Equality, Bool, Nat, List, and Vec theorem modules, built-in reduction checks, deterministic small normalized Bool/Nat/List/Vec terms, the built-in inductive specs, equation metadata, generated equation theorem realization, matcher equation realization, one explicit indexed Vec matcher spec, indexed matcher equation metadata, checked statement types, metadata-only lemmas, and validation-only theorem realization. The indexed matcher validation constructs and admits the matcher inside validation only; it is not installed by `Prelude.env/0`. Indexed matcher equations can be exercised through `Theoria.Library.Vec.env_with_indexed_matcher/1`; passing `install_equations: true` also installs the realized indexed equation theorems into that opt-in environment. Prelude still does not install them, and rewrite/simp still exclude indexed matcher equations until simplification policy is finalized.

## Defeq checks

Defeq checks are first-class Theoria values:

```elixir
%Theoria.Validation.DefeqCheck{
  category: :nat,
  name: "nat_add_one_zero",
  left: left,
  right: right
}
```

They are checked by Theoria before any external oracle sees them:

```elixir
Theoria.Validation.DefeqCheck.check(env, check)
```

Use these for kernel reduction behavior such as beta, zeta, recursor iota, indexed iota, and small deterministic normalized examples.

## Lean oracle boundary

Lean validation is optional contributor hardening:

```bash
mix theoria.lean.check
```

It translates the Theoria validation corpus into Lean source and asks Lean to check the same proof and defeq claims. It also emits Lean `#check` type checks for the indexed Vec matcher equation statement shapes. Lean is not Theoria's source of truth and is not required for normal use.

## Adding new checks

Prefer adding validation data close to the Theoria feature it exercises. Library validation metadata lives under modules such as `Theoria.Library.Bool.Validation`, `Theoria.Library.Nat.Validation`, `Theoria.Library.List.Validation`, and `Theoria.Library.Vec.Validation`.

Guidelines:

| Need | Put it in |
|---|---|
| Reusable proposition proof | `Theoria.Library.*.Theorems` |
| Reduction/iota/defeq behavior | `Theoria.Library.*.Validation` as `%Theoria.Validation.DefeqCheck{}` |
| Inductive declaration invariant | `Theoria.Library.*.Validation` as `%Theoria.Validation.InductiveCheck{}` |
| Shared validation term helper | `Theoria.Validation.Terms` |
| External oracle mapping issue | `Theoria.Lean.Encode.*` |

1. Add a theorem to the appropriate `Theoria.Library.*.Theorems` module when it is a reusable library fact.
2. Add a `%Theoria.Validation.DefeqCheck{}` in the owning library validation module when the point is definitional equality or reduction behavior.
3. Add an inductive check in the owning library validation module when a built-in spec/declaration shape needs to stay validated.

## Downstream theorem example

```elixir
defmodule MyApp.Proofs do
  use Theoria.DSL

  theorem :identity do
    type do
      term do
        forall :p, prop() do
          p ~> p
        end
      end
    end

    proof do
      term do
        lam :p, prop() do
          lam :hp, p do
            hp
          end
        end
      end
    end
  end
end

{:ok, env} = Theoria.Prelude.env()
Theoria.Theorem.check_all(MyApp.Proofs, env)
```

From Mix:

```bash
mix theoria.theorems MyApp.Proofs
```

## Kernel differential reports

Use `mix theoria.kernel.check` for production/reference kernel assurance. It covers curated infer/check/normalize/defeq cases, rejection cases, theorem modules, generated artifacts, indexed artifacts, reference replay of the Prelude environment, replay of theorem-module-installed environments, and replay of environments extended with generated and indexed artifacts.

Coverage, explanation, and JSON modes are intended for CI and tooling:

```bash
mix theoria.kernel.check --coverage
mix theoria.kernel.check --explain
mix theoria.kernel.check --json --coverage
```

The JSON output is encoded through Jason encoders and includes structured artifact replay counts and skip entries. A skipped artifact means it was not replayed as an installed declaration in that environment; it is not silently treated as checked. Rewrite/simp remain untrusted search even when these reports pass—the trusted boundary is still the final kernel-checked artifact or theorem declaration.

After adding checks, run:

```bash
mix theoria.validate
mix theoria.lean.check
```