# Proof Spec: statistease
<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->

**Repo Path**: `/var/mnt/eclipse/repos/statistease`
**Tier**: T2 — High
**Total Theorems**: 4
**Primary Prover(s)**: Agda (all)
**Existing Proof Coverage**: 3 Agda files: TropicalSemiring.agda, RankIdentities.agda, Inequalities.agda

## Status Tracker

| # | Theorem | Prover | Status | Verified |
|---|---------|--------|--------|----------|
| 1 | SE1 Tropical semiring correctness | Ag | [x] Specified | — |
| 2 | SE2 Rank identities | Ag | [x] Specified | — |
| 3 | SE3 Statistical inequalities | Ag | [x] Specified | — |
| 4 | SE4 NaN/infinity screening completeness | Ag | [ ] Pending | — |

## Context

Neurosymbolic stats assistant. All computation via verified Julia (17 modules). Zero statistical inference in neural path.

### Key files
- `src/stats/descriptive.jl`
- `src/stats/inferential.jl`
- `src/stats/effect_sizes.jl`
- `src/stats/bayesian.jl`
- `src/stats/assumptions.jl`

## Theorems to Prove

### SE1/SE2/SE3: Verify existing Agda proofs

**Target**: Existing files
**Priority**: P0

**Obligations**:
- [ ] `agda --safe` each existing file
- [ ] Confirm 0 postulates

---

### SE4: NaN/infinity screening completeness

**Target**: `proofs/StatistEase/NaNInfScreen.agda` (NEW)
**Priority**: P1

**Statement**: Input validation rejects all NaN and infinity values before computation.

**Obligations**:
- [ ] Enumerate input types
- [ ] Prove screening completeness

---

## Verification Commands

```bash
cd /var/mnt/eclipse/repos/statistease
agda --safe proofs/StatistEase/*.agda
```

## Handoff Checklist

- [ ] All 4 theorems proven
- [ ] Commit: `proof: complete statistease proofs (4/4)`
