# Theorem 3 Crack: Integration into sov-kernel-monster

## Overview

The Jacobian Conjecture crack (Theorem 3: constant Jacobian ⟹ genus-0 curve) has been cherry-picked into `haskell/` for polyglot integration.

**Location:** `sov-kernel-monster/haskell/LiquidLean/Jacobian/`

**Status:** Phase 1 integration (code as-is, bugs documented for Phase 2)

---

## Module Structure

```
haskell/LiquidLean/Jacobian/
├── Theorem3Kernel.hs           [SOURCE: Theorem3 core types, Polynomial ops]
├── MoraLocal.hs                [SOURCE: Mora standard basis algorithm]
├── SingularityAnalysis.hs       [SOURCE: Milnor number + δ-invariant computation]
├── CrackTheorem3.hs            [SOURCE: Main orchestration (genus-0 forcing)]
└── Theorem3Entry.hs            [NEW: Kernel integration point]
```

### Module Responsibilities

| Module | Purpose | Lines | Dependencies |
|--------|---------|-------|--------------|
| **Theorem3Kernel** | Polynomial type, Rational/Z literals, Energy monad, Thermal type, Obstruction errors | 169 | GHC.TypeLits, Data.Map, Data.Ratio, Control.Monad.State |
| **MoraLocal** | Mora weak normal form, divisibility, Gröbner basis algorithm | 82 | Theorem3Kernel, Data.Map |
| **SingularityAnalysis** | Polynomial translation, lowest-degree part extraction, branch counting, Plücker genus formula | 93 | Theorem3Kernel, MoraLocal |
| **CrackTheorem3** | Main algorithm: singularity → δ-invariants → genus formula → decision | 101 | Theorem3Kernel, MoraLocal, SingularityAnalysis |
| **Theorem3Entry** | Kernel-facing interface, Theorem3Status/Evidence types, energy accounting wrapper | 150 | All of the above |

---

## Entry Point

```haskell
theorem3EnforceGenusZero :: Polynomial -> Integer -> Either Obstruction Theorem3Evidence
```

**Inputs:**
- `Polynomial` — The implicit curve h(u,x) ∈ ℚ[u,x]
- `Integer` — Energy budget (φ⁻¹ discretized as integer tokens)

**Outputs:**
```haskell
Either Obstruction Theorem3Evidence

data Theorem3Status
  = GenusZeroProved Polynomial        -- Theorem 3 holds ✓
  | CounterexampleFound Polynomial Int -- Higher genus (potential counter to Conjecture)
  | AnalysisBlocked Obstruction        -- Hit an obstruction

data Theorem3Evidence
  { evPolynomial :: Polynomial         -- Input poly
  , evDegree :: Int                   -- Degree
  , evGenusBound :: Int               -- Genus from Plücker
  , evEnergySpent :: Integer          -- Energy consumed
  , evEnergyBudget :: Integer         -- Initial budget
  , evStatus :: Theorem3Status        -- Result
  }
```

---

## Integration with Kernel

### 1. Lean FFI Bindings (New)

Add to `lean/SovMonster.lean`:

```lean
namespace Theorem3

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

### 2. Fortran Bridge (New)

Add to `src/theorem3_gateway.f90`:

```fortran
subroutine theorem3_enforce_genus_zero( &
    poly_ptr, poly_bytes, budget, status_ptr) bind(C, name='theorem3_enforce_genus_zero')
  use iso_c_binding
  use bob_kinds
  implicit none
  
  integer(c_int64_t), value :: poly_ptr, poly_bytes, budget
  integer(c_int64_t) :: status_ptr
  
  ! Call Haskell: Theorem3Entry.theorem3EnforceGenusZero
  ! [Requires Haskell RTS + foreign imports]
end subroutine
```

### 3. Rust WASM Bridge (Optional)

If running in `wasm/`, implement thin wrapper:

```rust
#[wasm_bindgen]
pub extern "C" fn theorem3_prove_genus_zero(
    poly_bytes: &[u8],
    budget: u64,
) -> String {
    // Call Haskell via FFI or as subprocess
    // Return JSON: {"status": "GenusZeroProved", "energy": 42}
}
```

---

## WORM Ledger Interface

Energy tokens emitted by `theorem3_enforce_genus_zero` flow into the WORM chain:

```
Entry structure:
  {
    "kernel_id": "theorem3_entry",
    "event": "forceGenusZero",
    "polynomial_degree": <int>,
    "energy_token": <integer>,
    "timestamp": <quantum_state>,
    "prior_entry_hash": <Blake3>
  }

Sealed with:
  signature := Ed25519(entry ‖ prior_entry_hash, sk_node)
  receipt := (Blake3_hash, Ed25519_sig)
```

See: `src/bob_worm.f90` for chain mechanics.

---

## Known Bugs (Phase 1: NOT FIXED)

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

**File:** `SingularityAnalysis.hs`, lines 32-44

**Issue:** Variables `u'` and `x'` are used in the `coeff` function but not properly bound.

```haskell
translate (Poly f) (u0, x0) = Poly $ Map.fromListWith (+)
  [ ((u'-a, x'-b), c * coeff a b u0 x0)  -- u', x' undefined here!
  | ((a,b), c) <- Map.toList f
  , u' <- [0..a], x' <- [0..b]
  ]
  where
    coeff a b u0 x0 =
      fromIntegral (choose a (a-u') * choose b (b-x'))  -- u', x' not in scope
      * (u0 ^ (a - u')) * (x0 ^ (b - x'))
```

**Symptoms:** Compilation failure or runtime crash on `analyseSingularity`.

**Fix (Phase 2):** Refactor `coeff` to accept `u'` and `x'` as parameters or use a curried lambda.

---

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

**File:** `SingularityAnalysis.hs`, lines 56-61

**Issue:** Polynomial factorization is stubbed out. Returns `degree + 1` as a placeholder.

```haskell
countBranches h0 =
  let (initForm, _) = lowestDegreePart h0
      -- Placeholder: actual factorization deferred
      degree = totalDegree initForm
  in if degree >= 0 then degree + 1 else 1
```

**Symptoms:** δ-invariant is under-counted. Genus bound may be incorrect.

**Fix (Phase 2):** Implement polynomial factorization over ℚ using resultant or Hensel lifting.

---

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

**File:** `MoraLocal.hs`, lines 44-45

**Issue:** The monomial difference is computed backwards.

```haskell
monomialDiff (LM u1 x1) (LM u2 x2) = (u1 - u2, x1 - x2)  -- Should be (u2-u1, x2-x1)
```

**Symptoms:** Mora reduction computes incorrect quotient monomials.

**Fix (Phase 2):** Swap the subtraction order: `(u2 - u1, x2 - x1)`.

---

### Bug #4: CrackTheorem3.forceGenusZero() — Single Singularity Check

**File:** `CrackTheorem3.hs`, lines 49-51

**Issue:** Only checks singularity at origin. Missing all other critical singular points.

```haskell
-- Step 2: Analyze singularities (simplified: check origin)
-- In full version: would find all singular points via resultant
singData <- analyseSingularity hPoly (0, 0)
```

**Symptoms:** δ-invariant computation is incomplete. Genus bound is wrong.

**Fix (Phase 2):** Compute singular locus: { (u,x) : h=0, ∂h/∂u=0, ∂h/∂x=0 } via resultant.

---

### Bug #5: Theorem3Kernel.translate() — Undefined Variables

**File:** `Theorem3Kernel.hs`, line 128-130

**Issue:** Arity check only handles 2-variable polynomials. (Design limitation, not a bug.)

```haskell
evaluate (Poly f) [u,x] = sum [ c * (u^u') * (x^x')
                               | ((u',x'),c) <- Map.toList f ]
evaluate _ _ = error "evaluate: wrong arity"
```

**Impact:** No immediate problem, but limits to univariate/bivariate.

---

## Build Instructions (Future)

When ready to build the polyglot kernel with Haskell:

```bash
# 1. Build just Theorem 3
cd sov-kernel-monster/haskell
ghc -XStrictData -O2 \
  LiquidLean/Jacobian/Theorem3Kernel.hs \
  LiquidLean/Jacobian/MoraLocal.hs \
  LiquidLean/Jacobian/SingularityAnalysis.hs \
  LiquidLean/Jacobian/CrackTheorem3.hs \
  LiquidLean/Jacobian/Theorem3Entry.hs \
  -shared -dynamic -fPIC

# 2. Link with Fortran kernel
cd ..
make theorem3_bridge

# 3. Verify Lean FFI compiles
lake build
```

---

## Proof Map

```
Input: h(u,x) with det(J_F) = const
         ↓
         ├─→ [Find singularities] → set S of (u_i, x_i)
         │
         ├─→ [For each P ∈ S]:
         │     ├─→ Translate to origin: h₀ = h(u+u_P, x+x_P)
         │     ├─→ Jacobian ideal: ⟨∂h₀/∂u, ∂h₀/∂x⟩
         │     ├─→ Mora basis: GB
         │     ├─→ Standard monomials: μ = |{LT(GB)}|
         │     ├─→ Branches: r = factor multiplicity
         │     └─→ δ_P = (μ + r - 1) / 2   [Milnor-Jung]
         │
         ├─→ [Plücker Genus Formula]:
         │     g = (d-1)(d-2)/2 - Σ δ_P
         │
         └─→ [Decision]:
              ├─ If g = 0 → GenusZeroProved ✓
              ├─ If g > 0 → CounterexampleFound (genus > 0!)
              └─ Else → AnalysisBlocked (error)

Output: Either Obstruction Theorem3Evidence
```

---

## Related Files

- **Source (liquidlean-transmutation):** `../liquidlean-transmutation/src/LiquidLean/Jacobian/`
- **Formal spec (jacobian-formal):** `/tmp/jacobian-formal/lean/Jacobian/MainConjecture.lean`
- **WORM attestation:** `src/bob_worm.f90`
- **Quantum boundary:** `src/sov_monster_kernel.f90` (Blake3 + Ed25519)
- **Lean FFI spec:** `lean/SovMonster.lean`

---

## Next Steps (Phase 2)

1. ✅ Cherry-pick modules (DONE)
2. ✅ Create entry point (DONE)
3. ⏳ Fix Bug #1 (translate scope)
4. ⏳ Fix Bug #2 (countBranches factorization)
5. ⏳ Fix Bug #3 (monomialDiff sign)
6. ⏳ Fix Bug #4 (complete singularity search)
7. ⏳ Add Lean FFI bindings
8. ⏳ Add Fortran bridge
9. ⏳ Wire to WORM ledger
10. ⏳ Test end-to-end

---

**Integration Date:** 2026-07-20  
**Phase:** 1 (cherry-pick, no fixes)  
**Bugs:** 5 documented for Phase 2  
**Status:** Ready for formalization review