// SPDX-License-Identifier: CC-BY-SA-4.0
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
# Machine Verification Guide

> **STATUS 2026-07-07 (PR #100), reconciled 2026-11-01:** This guide's *method*
> still applies, but its illustrative pass/fail examples below are historical.
> The *active* stack — Agda (`--safe --without-K`, zero postulates) + Z3 bounded
> checks + the Idris 2 ABI — verifies clean; run `proofs/verify-active-provers.sh`
> for `ACTIVE-PROVERS-GREEN`. Coq/Lean 4/Isabelle/Mizar are archived under
> `archive/proofs/`. See `PROOF-STATUS.adoc` for the canonical active-vs-archived
> proof-status table. Treat the counts in the examples that follow as pedagogical,
> not current.

## Current Status: PARTIAL VERIFICATION (historical example)

### What Will Pass ✅
- Phase 1 core proofs (composition theorems in Coq and Lean 4)
- Basic CNO definitions
- Syntactically correct frameworks

### What Will Fail ❌
- Any theorem marked `Admitted` (Coq)
- Any theorem marked `sorry` (Lean 4)
- Complex arithmetic in StatMech.v, QuantumCNO.v
- Some category theory edge cases

## Step-by-Step Machine Verification

### Step 1: Build Container

```bash
cd /home/user/absolute-zero

# Using Podman (recommended)
podman build -t absolute-zero .

# Or using Docker
docker build -t absolute-zero .
```

**Expected time**: 10-30 minutes (downloads dependencies)

### Step 2: Run Verification Script

```bash
# Podman
podman run --rm absolute-zero ./verify-proofs.sh

# Docker
docker run --rm absolute-zero ./verify-proofs.sh
```

**Expected output**:
```
Checking for proof tools...
✓ coqc found
✓ z3 found
✓ lean found
...

Verifying Coq proofs...
[PASS] proofs/coq/common/CNO.v (with 1 admitted)
[FAIL] proofs/coq/physics/StatMech.v (12 admitted)
[FAIL] proofs/coq/category/CNOCategory.v (8 admitted)
...
```

### Step 3: Interpret Results

**Admitted/Sorry Count**:
Run this to count incomplete proofs:

```bash
# Count Coq admits
find proofs/coq -name "*.v" -exec grep -c "Admitted" {} + | awk -F: '{sum += $2} END {print "Coq Admitted:", sum}'

# Count Lean 4 sorries
find proofs/lean4 -name "*.lean" -exec grep -c "sorry" {} + | awk -F: '{sum += $2} END {print "Lean sorry:", sum}'
```

### Step 4: Address Failures

**Option A: Complete Proofs** (Hard)
- Fill in all `Admitted`/`sorry` with actual proofs
- Requires deep expertise in each domain
- Estimated: Weeks to months of work

**Option B: Honest Documentation** (Recommended)
- Update VERIFICATION.md with exact pass/fail counts
- Clearly state: "Frameworks complete, many proofs incomplete"
- Be transparent about axiomatization

**Option C: Extract Verified Core** (Pragmatic)
- Separate fully-verified Phase 1 from incomplete Phase 2-4
- Publish Phase 1 as "verified"
- Publish Phase 2-4 as "formalization in progress"

## Honest Expectations

Based on my analysis:
- **Phase 1**: ~90% will verify (only 1-2 edge cases admitted)
- **Phase 2 (StatMech)**: ~40% will verify (many axioms)
- **Phase 3 (Category/Lambda)**: ~60% will verify (some edge cases)
- **Phase 4 (Quantum/Filesystem)**: ~50% will verify (complex arithmetic incomplete)

## What to Report

**Academic Honesty Requires**:
1. Exact count of admitted/sorry statements
2. Distinction between "axiomatized" and "proven"
3. Clear statement: "Formal frameworks with partial proofs"
4. Not: "Fully verified across 6 proof systems" (this is false)

## Next Steps After Verification

1. **If verification rate > 80%**: Can claim "substantial verification"
2. **If verification rate 50-80%**: Claim "formal framework with proof sketches"
3. **If verification rate < 50%**: Claim "formalization in progress"

Currently, I estimate: **~60% overall verification rate**