sov-kernel-monster / haskell /INTEGRATION_GUIDE.md

SNAPKITTYWEST

chore: push full sov-kernel-monster content from local build

9425aed verified 5 days ago

preview code

Raw

History Blame Contribute Delete

9.69 kB

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

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

Inputs:

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

Outputs:

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:

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:

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:

#[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.

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.

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.

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.

-- 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.)

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:

# 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)

✅ Cherry-pick modules (DONE)
✅ Create entry point (DONE)
⏳ Fix Bug #1 (translate scope)
⏳ Fix Bug #2 (countBranches factorization)
⏳ Fix Bug #3 (monomialDiff sign)
⏳ Fix Bug #4 (complete singularity search)
⏳ Add Lean FFI bindings
⏳ Add Fortran bridge
⏳ Wire to WORM ledger
⏳ 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