# Theorem 3 Integration: Quick Reference

**Status:** Phase 1 Complete (2026-07-20)  
**Location:** `sov-kernel-monster/haskell/LiquidLean/Jacobian/`  
**Entry Point:** `theorem3EnforceGenusZero :: Polynomial -> Integer -> Either Obstruction Theorem3Evidence`

---

## Module Map

| Module | Purpose | Lines | Status |
|--------|---------|-------|--------|
| `Theorem3Kernel.hs` | Polynomial types, Energy monad, Obstruction errors | 169 | ✅ Cherry-picked |
| `MoraLocal.hs` | Mora standard basis algorithm | 82 | ✅ Cherry-picked |
| `SingularityAnalysis.hs` | Milnor number, δ-invariants, Plücker genus | 93 | ✅ Cherry-picked |
| `CrackTheorem3.hs` | Main orchestration: singularity → genus decision | 101 | ✅ Cherry-picked |
| `Theorem3Entry.hs` | Kernel integration wrapper + WORM bridge | 150 | ✅ NEW |

---

## Quick Start

### Using the Entry Point

```haskell
import LiquidLean.Jacobian.Theorem3Entry

-- Example: test polynomial h = u*x - 1
let h = fromTerms [(1,1,1), (0,0,-1)] :: Polynomial
let result = theorem3EnforceGenusZero h 1000

-- Returns: Either Obstruction Theorem3Evidence
case result of
  Left obs -> putStrLn $ "Error: " ++ show obs
  Right ev -> putStrLn $ "Genus: " ++ show (evGenusBound ev)
```

### Signature

```haskell
theorem3EnforceGenusZero 
  :: Polynomial     -- Input polynomial h(u,x)
  -> Integer        -- Energy budget (φ⁻¹ tokens)
  -> Either Obstruction Theorem3Evidence

data Theorem3Status
  = GenusZeroProved Polynomial        -- Theorem 3 holds ✓
  | CounterexampleFound Polynomial Int -- Higher genus
  | AnalysisBlocked Obstruction        -- Hit obstruction

data Theorem3Evidence = Theorem3Evidence
  { evPolynomial :: Polynomial        -- Input polynomial
  , evDegree :: Int                   -- Total degree
  , evGenusBound :: Int               -- Genus from Plücker
  , evEnergySpent :: Integer          -- Energy consumed
  , evEnergyBudget :: Integer         -- Initial budget
  , evStatus :: Theorem3Status        -- Final status
  }
```

---

## Known Bugs (Phase 2 Deferred)

### Bug #1: SingularityAnalysis.translate() — Variable Scope

**File:** `SingularityAnalysis.hs:32-44`  
**Severity:** HIGH  
**Issue:** Variables `u'`, `x'` undefined in `coeff` function scope.  
**Impact:** Crashes on `analyseSingularity` calls with non-origin singularities.  
**Fix:** Refactor `coeff` to accept u', x' as parameters.

### Bug #2: SingularityAnalysis.countBranches() — Incomplete Factorization

**File:** `SingularityAnalysis.hs:56-61`  
**Severity:** MEDIUM  
**Issue:** Returns `degree + 1` placeholder; actual factorization not implemented.  
**Impact:** δ-invariant under-counted; genus bound incorrect.  
**Fix:** Implement polynomial factorization over ℚ (resultant or Hensel lifting).

### Bug #3: MoraLocal.monomialDiff() — Inverted Arithmetic

**File:** `MoraLocal.hs:44-45`  
**Severity:** MEDIUM  
**Issue:** Computes `(u1-u2, x1-x2)` instead of `(u2-u1, x2-x1)`.  
**Impact:** Mora reduction computes wrong quotient monomials.  
**Fix:** Swap subtraction order.

### Bug #4: CrackTheorem3.forceGenusZero() — Incomplete Singularity Search

**File:** `CrackTheorem3.hs:49-51`  
**Severity:** HIGH  
**Issue:** Only checks singularity at origin (0,0); misses all others.  
**Impact:** δ-invariant computation incomplete; genus formula wrong.  
**Fix:** Compute full singular locus via resultant algorithm.

### Bug #5: Theorem3Kernel.evaluate() — Arity Limitation

**File:** `Theorem3Kernel.hs:127-130`  
**Severity:** LOW  
**Issue:** Only handles 2-variable polynomials (design limitation).  
**Impact:** Can't evaluate with other arities.  
**Fix:** Generalize to n variables (optional).

---

## Proof Pipeline

```
Input: h(u,x) [polynomial]
  ↓
[Step 1: Find singularities]
  → Singular locus S = { (u,x) : h=0 ∧ ∂h/∂u=0 ∧ ∂h/∂x=0 }
  ⚠️  BUG #4: Currently only checks (0,0)
  ↓
[Step 2: For each singularity P ∈ S]
  → Translate: h₀ = h(u+u_P, x+x_P)
  ⚠️  BUG #1: Fails on non-origin translation
  ↓
  → Jacobian ideal: ⟨∂h₀/∂u, ∂h₀/∂x⟩
  → Mora basis: GB via groebnerBasisLocal
  ⚠️  BUG #3: Mora reduction may have arithmetic error
  ↓
  → Standard monomials: μ = countStandardMonomials GB
  → Branches: r = countBranches h₀
  ⚠️  BUG #2: countBranches is stub (returns degree+1)
  ↓
  → Milnor-Jung: δ = (μ + r - 1) / 2
  ↓
[Step 3: Plücker Genus Formula]
  g = (d-1)(d-2)/2 - Σ δ_P
  ↓
[Step 4: Decision]
  If g = 0 → GenusZeroProved ✓
  If g > 0 → CounterexampleFound (genus contradiction!)
  Else → AnalysisBlocked (error)
```

---

## Integration with sov-kernel-monster

### WORM Ledger

Each `theorem3EnforceGenusZero` call emits energy tokens:

```json
{
  "kernel_id": "theorem3_entry",
  "event": "forceGenusZero",
  "polynomial_degree": 6,
  "energy_token": 42,
  "prior_entry_hash": "Blake3(previous_entry)"
}
```

Sealed with Ed25519 at quantum boundary (`sov_monster_kernel.f90`).

### Lean FFI Binding (Template)

```lean
@[extern "theorem3_enforce_genus_zero"]
opaque enforceGenusZero 
    (polyPtr : CPtr) (budget : Int64)
    (statusPtr : CPtr) : Unit
```

See `INTEGRATION_GUIDE.md` for full Fortran + WASM templates.

---

## Build

```bash
cd sov-kernel-monster/haskell

# Stack (recommended)
stack build

# Or with Cabal
cabal build

# Or with ghc directly
ghc -XStrictData -O2 \
  LiquidLean/Jacobian/Theorem3Kernel.hs \
  LiquidLean/Jacobian/MoraLocal.hs \
  LiquidLean/Jacobian/SingularityAnalysis.hs \
  LiquidLean/Jacobian/CrackTheorem3.hs \
  LiquidLean/Jacobian/Theorem3Entry.hs
```

---

## References

- **Full architecture:** `INTEGRATION_GUIDE.md` (330 lines)
- **Phase 1 summary:** `PHASE_1_INTEGRATION_SUMMARY.md` (427 lines)
- **Formal spec:** `/tmp/jacobian-formal/lean/Jacobian/MainConjecture.lean`
- **Source repo:** `liquidlean-transmutation/src/LiquidLean/Jacobian/`

---

## Phase 2 Roadmap

- ⏳ Fix 5 bugs (critical path: #1, #4, #2)
- ⏳ Lean FFI bindings
- ⏳ Fortran bridge + Haskell RTS
- ⏳ WORM ledger wiring
- ⏳ Quantum boundary verification
- ⏳ Test suite
- ⏳ Performance profiling

**Next step:** Fix Bug #1 and #4 to enable full singularity analysis.

---

**Last updated:** 2026-07-20  
**Phase:** 1 (Cherry-pick Complete, No Fixes)  
**Bugs:** 5 documented, all deferred to Phase 2