# Unsolved Hard Problems — Lean 4 Statement Stub Plan

**Date:** 2026-06-20  
**Scope:** Turn the RRC survey (`unsolved_hard_problems_rrc_survey.md` + `.json`) into precise, type-correct Lean 4 *statements* with `sorry` skeletons. No proofs are attempted.  
**Claim boundary:** This document is a build/implementation plan. It does not claim any problem is solved or that any stub will soon be provable.

---

## 1. Selection criteria

A problem is a **good stub target** when:

- Its definitions are stable in contemporary mathematics (no interpretational disputes).
- The statement can be written with Mathlib primitives available in the pinned `v4.30.0-rc2` rev.
- It does not depend on unsettled foundational axioms (ZFC extensions, large-cardinal hypotheses, or open-ended physical theories).
- A finite `#eval` witness can be supplied to check small cases without floating-point arithmetic.

A problem is **deferred** when it is formally independent of ZFC, requires choosing an axiom system, or lacks a settled mathematical object to state.

---

## 2. Good stub targets (7 problems)

All modules live under `0-Core-Formalism/lean/Semantics/Semantics/Unsolved/`.  
Shared metadata lives in `Semantics.Unsolved.Metadata` and is imported by every stub.

### 2.1 Shared metadata module

**File:** `Semantics/Unsolved/Metadata.lean`  
**Namespace:** `Semantics.Unsolved.Metadata`

```lean
import Semantics.FixedPoint

namespace Semantics.Unsolved.Metadata

open Semantics.FixedPoint

inductive RRCStatus where
  | candidate
  | hold
  | accept

inductive RRCShape where
  | projectableGeometryTopology
  | cognitiveLoadField
  | logogramProjection
  | burgersRgSolver
  | signalShapedRouteCompiler
  | languageSetManifoldGraph
  | holdForUnlawfulOrUnderspecifiedShape
  | computeKernelReceipt
  | cadForceProbeReceipt
  | erdosBoundConjecture
  | leanTheoremReceipt

structure RRCAxes where
  semanticEntropy        : Q0_16
  geometricMass          : Q0_16
  compressionPressure    : Q0_16
  topologyTorsion        : Q0_16
  residualRisk           : Q0_16
  proofReadiness         : Q0_16
  scaleBandDeclared      : Q0_16
  negativeControlStrength : Q0_16
  projectionDeclared     : Q0_16
  shapeClosure           : Q0_16

structure ProblemMetadata where
  rrcId    : String
  rrcShape : RRCShape
  rrcStatus : RRCStatus
  axes     : RRCAxes

end Semantics.Unsolved.Metadata
```

**Why it is needed:** Keeps the RRC projection data (id, shape, status, 10-axis vector) in one place and lets every problem stub carry its survey identity as a checked Lean value. Axis values are stored as `Q0_16` raw integers, not `Float`.

---

### 2.2 Goldbach conjecture

**File:** `Semantics/Unsolved/Goldbach.lean`  
**Namespace:** `Semantics.Unsolved.Goldbach`

```lean
import Semantics.Unsolved.Metadata
import Mathlib.Data.Nat.Prime
import Mathlib.Data.Nat.Parity

namespace Semantics.Unsolved.Goldbach

open Semantics.Unsolved.Metadata

def metadata : ProblemMetadata where
  rrcId     := "goldbach_conjecture"
  rrcShape  := RRCShape.logogramProjection
  rrcStatus := RRCStatus.candidate
  axes      := {
    semanticEntropy        := Q0_16.ofRawInt 19660  -- 0.60
    geometricMass          := Q0_16.ofRawInt  6553  -- 0.20
    compressionPressure    := Q0_16.ofRawInt 22937  -- 0.70
    topologyTorsion        := Q0_16.ofRawInt  6553  -- 0.20
    residualRisk           := Q0_16.ofRawInt  9830  -- 0.30
    proofReadiness         := Q0_16.ofRawInt  9830  -- 0.30
    scaleBandDeclared      := Q0_16.ofRawInt 27852  -- 0.85
    negativeControlStrength := Q0_16.ofRawInt 22937  -- 0.70
    projectionDeclared     := Q0_16.ofRawInt 31128  -- 0.95
    shapeClosure           := Q0_16.ofRawInt 18022  -- 0.55
  }

def goldbach (n : Nat) : Prop :=
  n > 2 ∧ Even n → ∃ p q, p.Prime ∧ q.Prime ∧ p + q = n

theorem goldbachConjecture :
    ∀ n, goldbach n := by
  sorry -- TODO(lean-port): no known elementary proof; verified computationally to large bounds

-- #eval witness: every even n in (4..10000) is a sum of two primes.
-- Expect: true

end Semantics.Unsolved.Goldbach
```

**Required Mathlib imports:** `Mathlib.Data.Nat.Prime`, `Mathlib.Data.Nat.Parity`.  
**Dependencies:** `Semantics.Unsolved.Metadata`.  
**Why it is a good stub target:** The statement uses only `Nat.Prime` and `Even`; both are stable. A bounded `#eval` witness is immediate.

---

### 2.3 Twin prime conjecture

**File:** `Semantics/Unsolved/TwinPrime.lean`  
**Namespace:** `Semantics.Unsolved.TwinPrime`

```lean
import Semantics.Unsolved.Metadata
import Mathlib.Data.Nat.Prime
import Mathlib.Data.Set.Basic

namespace Semantics.Unsolved.TwinPrime

open Semantics.Unsolved.Metadata

def metadata : ProblemMetadata where
  rrcId     := "twin_prime_conjecture"
  rrcShape  := RRCShape.logogramProjection
  rrcStatus := RRCStatus.candidate
  axes      := {
    semanticEntropy        := Q0_16.ofRawInt 21300  -- 0.65
    geometricMass          := Q0_16.ofRawInt  8191  -- 0.25
    compressionPressure    := Q0_16.ofRawInt 24575  -- 0.75
    topologyTorsion        := Q0_16.ofRawInt  8191  -- 0.25
    residualRisk           := Q0_16.ofRawInt 11468  -- 0.35
    proofReadiness         := Q0_16.ofRawInt  8191  -- 0.25
    scaleBandDeclared      := Q0_16.ofRawInt 26213  -- 0.80
    negativeControlStrength := Q0_16.ofRawInt 21298  -- 0.65
    projectionDeclared     := Q0_16.ofRawInt 29490  -- 0.90
    shapeClosure           := Q0_16.ofRawInt 14745  -- 0.45
  }

def isTwinPrime (p : Nat) : Prop :=
  p.Prime ∧ (p + 2).Prime

theorem twinPrimeConjecture :
    Set.Infinite {p | isTwinPrime p} := by
  sorry -- TODO(lean-port): sieve parity obstruction; verified to large bounds

-- #eval witness: list twin prime pairs below 1000.
-- Expect: a non-empty list ending with (1019, 1021) or similar

end Semantics.Unsolved.TwinPrime
```

**Required Mathlib imports:** `Mathlib.Data.Nat.Prime`, `Mathlib.Data.Set.Basic`.  
**Dependencies:** `Semantics.Unsolved.Metadata`.  
**Why it is a good stub target:** One predicate on `Nat.Prime`; `Set.Infinite` is available. Bounded witnesses are trivial to compute.

---

### 2.4 Collatz conjecture

**File:** `Semantics/Unsolved/Collatz.lean`  
**Namespace:** `Semantics.Unsolved.Collatz`

```lean
import Semantics.Unsolved.Metadata
import Mathlib.Data.Nat.Basic

namespace Semantics.Unsolved.Collatz

open Semantics.Unsolved.Metadata

def metadata : ProblemMetadata where
  rrcId     := "collatz_conjecture"
  rrcShape  := RRCShape.logogramProjection
  rrcStatus := RRCStatus.candidate
  axes      := {
    semanticEntropy        := Q0_16.ofRawInt 18022  -- 0.55
    geometricMass          := Q0_16.ofRawInt 11468  -- 0.35
    compressionPressure    := Q0_16.ofRawInt 22937  -- 0.70
    topologyTorsion        := Q0_16.ofRawInt 14745  -- 0.45
    residualRisk           := Q0_16.ofRawInt 13107  -- 0.40
    proofReadiness         := Q0_16.ofRawInt  6553  -- 0.20
    scaleBandDeclared      := Q0_16.ofRawInt 26213  -- 0.80
    negativeControlStrength := Q0_16.ofRawInt 19660  -- 0.60
    projectionDeclared     := Q0_16.ofRawInt 27852  -- 0.85
    shapeClosure           := Q0_16.ofRawInt 13107  -- 0.40
  }

def collatzNext (n : Nat) : Nat :=
  if n % 2 = 0 then n / 2 else 3 * n + 1

def collatzSeq (n : Nat) : Nat → Nat
  | 0     => n
  | k + 1 => collatzNext (collatzSeq n k)

theorem collatzConjecture :
    ∀ n, n > 0 → ∃ k, collatzSeq n k = 1 := by
  sorry -- TODO(lean-port): no known invariant controls expand/contract dynamics across all scales

-- #eval witness: verify convergence for all seeds 1..10000.
-- Expect: true

end Semantics.Unsolved.Collatz
```

**Required Mathlib imports:** `Mathlib.Data.Nat.Basic`.  
**Dependencies:** `Semantics.Unsolved.Metadata`.  
**Why it is a good stub target:** Pure `Nat` recursion; the statement is a single quantified property. Small-seed verification is an easy `#eval` witness.

---

### 2.5 abc conjecture

**File:** `Semantics/Unsolved/AbcConjecture.lean`  
**Namespace:** `Semantics.Unsolved.AbcConjecture`

```lean
import Semantics.Unsolved.Metadata
import Mathlib.Data.Nat.Prime
import Mathlib.Data.Nat.Factorization
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real

namespace Semantics.Unsolved.AbcConjecture

open Semantics.Unsolved.Metadata

def metadata : ProblemMetadata where
  rrcId     := "abc_conjecture"
  rrcShape  := RRCShape.logogramProjection
  rrcStatus := RRCStatus.candidate
  axes      := {
    semanticEntropy        := Q0_16.ofRawInt 24575  -- 0.75
    geometricMass          := Q0_16.ofRawInt  9830  -- 0.30
    compressionPressure    := Q0_16.ofRawInt 26213  -- 0.80
    topologyTorsion        := Q0_16.ofRawInt 11468  -- 0.35
    residualRisk           := Q0_16.ofRawInt 13107  -- 0.40
    proofReadiness         := Q0_16.ofRawInt  8191  -- 0.25
    scaleBandDeclared      := Q0_16.ofRawInt 24575  -- 0.75
    negativeControlStrength := Q0_16.ofRawInt 19660  -- 0.60
    projectionDeclared     := Q0_16.ofRawInt 29490  -- 0.90
    shapeClosure           := Q0_16.ofRawInt 16383  -- 0.50
  }

/-- Radical of a positive integer: product of distinct prime divisors. -/
def rad (n : Nat) : Nat :=
  n.factorization.prod fun p _ => p

theorem abcConjecture :
    ∀ ε : ℝ, ε > 0 →
      ∃ C : ℝ, C > 0 ∧
        ∀ a b c : Nat,
          a > 0 → b > 0 → c > 0 →
          a + b = c →
          Nat.gcd a b = 1 →
          (c : ℝ) ≤ C * (rad (a * b * c) : ℝ) ^ (1 + ε : ℝ) := by
  sorry -- TODO(lean-port): deep Diophantine machinery; only partial results known

-- #eval witness: for ε = 0.5, check all coprime triples a + b = c ≤ 100.
-- Expect: no counterexample found

end Semantics.Unsolved.AbcConjecture
```

**Required Mathlib imports:** `Mathlib.Data.Nat.Prime`, `Mathlib.Data.Nat.Factorization`, `Mathlib.Data.Real.Basic`, `Mathlib.Analysis.SpecialFunctions.Pow.Real`.  
**Dependencies:** `Semantics.Unsolved.Metadata`.  
**Why it is a good stub target:** `Nat.factorization` and real exponentiation are present in the pinned mathlib. The statement is a single inequality with explicit quantifiers.

---

### 2.6 Beal conjecture

**File:** `Semantics/Unsolved/BealConjecture.lean`  
**Namespace:** `Semantics.Unsolved.BealConjecture`

```lean
import Semantics.Unsolved.Metadata
import Mathlib.Data.Nat.Prime

namespace Semantics.Unsolved.BealConjecture

open Semantics.Unsolved.Metadata

def metadata : ProblemMetadata where
  rrcId     := "beal_conjecture"
  rrcShape  := RRCShape.logogramProjection
  rrcStatus := RRCStatus.candidate
  axes      := {
    semanticEntropy        := Q0_16.ofRawInt 21298  -- 0.65
    geometricMass          := Q0_16.ofRawInt  8191  -- 0.25
    compressionPressure    := Q0_16.ofRawInt 22937  -- 0.70
    topologyTorsion        := Q0_16.ofRawInt  8191  -- 0.25
    residualRisk           := Q0_16.ofRawInt  9830  -- 0.30
    proofReadiness         := Q0_16.ofRawInt  6553  -- 0.20
    scaleBandDeclared      := Q0_16.ofRawInt 24575  -- 0.75
    negativeControlStrength := Q0_16.ofRawInt 18022  -- 0.55
    projectionDeclared     := Q0_16.ofRawInt 27852  -- 0.85
    shapeClosure           := Q0_16.ofRawInt 13107  -- 0.40
  }

def commonPrimeFactor (a b c : Nat) : Prop :=
  ∃ p, p.Prime ∧ p ∣ a ∧ p ∣ b ∧ p ∣ c

theorem bealConjecture :
    ∀ a b c x y z : Nat,
      a > 0 → b > 0 → c > 0 →
      x > 2 → y > 2 → z > 2 →
      a ^ x + b ^ y = c ^ z →
      commonPrimeFactor a b c := by
  sorry -- TODO(lean-port): would follow from abc; special cases and parametric families known

-- #eval witness: check all a^x + b^y = c^z with bases ≤ 20 and exponents ≤ 5.
-- Expect: every solution has a common prime factor

end Semantics.Unsolved.BealConjecture
```

**Required Mathlib imports:** `Mathlib.Data.Nat.Prime`.  
**Dependencies:** `Semantics.Unsolved.Metadata`.  
**Why it is a good stub target:** Purely about `Nat.Prime` and divisibility. The statement is a simple Diophantine implication.

---

### 2.7 Brocard's problem

**File:** `Semantics/Unsolved/Brocard.lean`  
**Namespace:** `Semantics.Unsolved.Brocard`

```lean
import Semantics.Unsolved.Metadata
import Mathlib.Data.Nat.Basic

namespace Semantics.Unsolved.Brocard

open Semantics.Unsolved.Metadata

def metadata : ProblemMetadata where
  rrcId     := "brocards_problem"
  rrcShape  := RRCShape.logogramProjection
  rrcStatus := RRCStatus.candidate
  axes      := {
    semanticEntropy        := Q0_16.ofRawInt 18022  -- 0.55
    geometricMass          := Q0_16.ofRawInt  6553  -- 0.20
    compressionPressure    := Q0_16.ofRawInt 19660  -- 0.60
    topologyTorsion        := Q0_16.ofRawInt  6553  -- 0.20
    residualRisk           := Q0_16.ofRawInt 11468  -- 0.35
    proofReadiness         := Q0_16.ofRawInt  6553  -- 0.20
    scaleBandDeclared      := Q0_16.ofRawInt 22937  -- 0.70
    negativeControlStrength := Q0_16.ofRawInt 18022  -- 0.55
    projectionDeclared     := Q0_16.ofRawInt 27852  -- 0.85
    shapeClosure           := Q0_16.ofRawInt 16383  -- 0.50
  }

def isBrocardSolution (n m : Nat) : Prop :=
  n.factorial + 1 = m ^ 2

theorem brocardProblem :
    {n | ∃ m, isBrocardSolution n m} = {4, 5, 7} := by
  sorry -- TODO(lean-port): expected finite list; only n = 4, 5, 7 are known

-- #eval witness: verify 4!+1 = 5², 5!+1 = 11², 7!+1 = 71².
-- Expect: true

end Semantics.Unsolved.Brocard
```

**Required Mathlib imports:** `Mathlib.Data.Nat.Basic`.  
**Dependencies:** `Semantics.Unsolved.Metadata`.  
**Why it is a good stub target:** Uses only `Nat.factorial` and square equality. The conjectured answer is a finite set, making the statement concrete.

---

### 2.8 Odd perfect numbers

**File:** `Semantics/Unsolved/OddPerfect.lean`  
**Namespace:** `Semantics.Unsolved.OddPerfect`

```lean
import Semantics.Unsolved.Metadata
import Mathlib.Data.Nat.Basic
import Mathlib.Data.Nat.Parity

namespace Semantics.Unsolved.OddPerfect

open Semantics.Unsolved.Metadata

def metadata : ProblemMetadata where
  rrcId     := "perfect_numbers_odd_existence"
  rrcShape  := RRCShape.logogramProjection
  rrcStatus := RRCStatus.candidate
  axes      := {
    semanticEntropy        := Q0_16.ofRawInt 19660  -- 0.60
    geometricMass          := Q0_16.ofRawInt  6553  -- 0.20
    compressionPressure    := Q0_16.ofRawInt 21298  -- 0.65
    topologyTorsion        := Q0_16.ofRawInt  6553  -- 0.20
    residualRisk           := Q0_16.ofRawInt 11468  -- 0.35
    proofReadiness         := Q0_16.ofRawInt  6553  -- 0.20
    scaleBandDeclared      := Q0_16.ofRawInt 26213  -- 0.80
    negativeControlStrength := Q0_16.ofRawInt 19660  -- 0.60
    projectionDeclared     := Q0_16.ofRawInt 27852  -- 0.85
    shapeClosure           := Q0_16.ofRawInt 16383  -- 0.50
  }

/-- n is perfect iff the sum of its proper divisors equals n. -/
def isPerfect (n : Nat) : Prop :=
  n.divisors.sum id = 2 * n

theorem noOddPerfectNumbers :
    ¬∃ n, Odd n ∧ n > 0 ∧ isPerfect n := by
  sorry -- TODO(lean-port): no example or impossibility proof known; many restrictions proven

-- #eval witness: no odd perfect number below 10^5.
-- Expect: true

end Semantics.Unsolved.OddPerfect
```

**Required Mathlib imports:** `Mathlib.Data.Nat.Basic`, `Mathlib.Data.Nat.Parity`.  
**Dependencies:** `Semantics.Unsolved.Metadata`.  
**Why it is a good stub target:** `Nat.divisors.sum` is available; the statement is an existence/impossibility claim with a clean negation.

---

## 3. Deferred poor stub targets (4 problems)

These problems are intentionally excluded from the first stub pass.

### 3.1 Continuum Hypothesis

**Survey id:** `continuum_hypothesis`  
**Why deferred:** Independent of ZFC by Gödel and Cohen. A Lean formalization would require either (a) adopting a specific set-theoretic universe/forcing extension, which is not a settled definition, or (b) proving `ZFC ⊢ CH` or `ZFC ⊢ ¬CH`, both impossible. Stating it as a bare `Prop` gives no useful formal surface.

### 3.2 Consistency of ZFC

**Survey id:** `consistency_of_zfc`  
**Why deferred:** Gödel's second incompleteness theorem shows ZFC cannot prove its own consistency unless inconsistent. Any formal statement would have to be conditional on a stronger metatheory, violating the "stable definitions" criterion.

### 3.3 Hilbert's 6th problem

**Survey id:** `hilbert_sixth_problem`  
**Why deferred:** The problem asks to "axiomatize all of physics." Physics is a collection of effective theories; there is no single agreed-upon object to formalize. The statement is open-ended rather than a well-posed mathematical proposition.

### 3.4 Quantum measurement problem

**Survey id:** `measurement_problem`  
**Why deferred:** It is interpretational. Different solutions (Copenhagen, many-worlds, Bohmian, decoherence-only, etc.) define the measurement process differently. A formal statement would embed an unresolved interpretational choice.

---

## 4. Build strategy

### 4.1 Quarantine the stubs from the default build

Add a dedicated `Unsolved` lean library in `lakefile.toml` and keep it out of `defaultTargets`:

```toml
[[lean_lib]]
name = "Unsolved"
roots = ["Semantics.Unsolved"]
```

Do **not** add `Unsolved` to `defaultTargets`.  
The default `lake build` (which builds `Compiler` + `Semantics`) therefore stays green.  
Developers check stubs with:

```bash
lake build Semantics.Unsolved.Goldbach
lake build Unsolved
```

If the existing `Semantics` lean_lib auto-discovers the same `Semantics.Unsolved.*` modules, narrow `Semantics.roots` during stub development so that `Semantics` no longer traverses `Semantics.Unsolved`.

### 4.2 `sorry` discipline

Every theorem skeleton uses `sorry` with a `TODO(lean-port)` comment that explains the obstruction, per the `lean-proof` skill contract. Example:

```lean
theorem goldbachConjecture : ∀ n, goldbach n := by
  sorry -- TODO(lean-port): no known elementary proof; verified computationally to large bounds
```

No bare `sorry` is allowed.

### 4.3 `#eval` witnesses

Each stub includes at least one `#eval` witness for a finite, computable special case:

| Problem | Witness |
|---------|---------|
| Goldbach | Verify the conjecture for all even `n ≤ 10000`. |
| Twin prime | Enumerate twin prime pairs below 1000. |
| Collatz | Verify convergence for all seeds `1..10000`. |
| abc | For `ε = 0.5`, scan coprime triples `a + b = c ≤ 100`. |
| Beal | Scan `a^x + b^y = c^z` with small bases/exponents. |
| Brocard | Confirm `4!+1 = 5²`, `5!+1 = 11²`, `7!+1 = 71²`. |
| Odd perfect | Confirm no odd perfect number below `10^5`. |

All witnesses use `Nat`/`Int` computation or `Q0_16` axis encoding. No `Float` appears in any compute path.

### 4.4 Start order

1. **First:** `Semantics.Unsolved.Metadata` — defines the shared RRC vocabulary and proves it has no `sorry`.
2. **Second:** `Semantics.Unsolved.Goldbach` and `Semantics.Unsolved.TwinPrime` — simplest definitions, used to validate the build/quarantine setup.
3. **Third:** `Semantics.Unsolved.Collatz` — tests a well-founded recursive definition in the stub namespace.
4. **Fourth:** `Semantics.Unsolved.AbcConjecture`, `Semantics.Unsolved.BealConjecture`, `Semantics.Unsolved.Brocard`, `Semantics.Unsolved.OddPerfect` — number-theory stubs that import prime/divisor/factorial machinery.

### 4.5 Promotion rule

A stub may be promoted into the main `Semantics` library only when its theorem is either fully proved or replaced by an explicit `axiom` that names the model boundary (e.g., `axiom goldbachConjecture`). Until then, `Unsolved` stays quarantined.

---

## 5. Research Stack conventions

- **Fixed-point only:** RRC axis scores are encoded as `Q0_16` raw integers via `Q0_16.ofRawInt`. No `Float` is used in compute paths.
- **Receipt boundary:** The `Unsolved` modules must not emit top-level JSON receipts. If a corpus-wide receipt for the stub collection is ever needed, it must be produced through `Semantics.AVMIsa.Emit`, which is the sole output boundary.
- **No new dependencies:** All definitions rely on the existing mathlib pin (`v4.30.0-rc2`) and the repo's `Semantics.FixedPoint` module.
- **Naming:** Files and namespaces use `PascalCase` per `LEAN_NAMING_CONVENTIONS.md`.
- **No broad staging:** When the stubs are eventually committed, stage only the planned `Unsolved/` files plus `lakefile.toml` changes. Do not use `git add .`.

---

## 6. Open questions

- Should the `Unsolved` library eventually be wired into `RRC.Emit` as a read-only corpus, or kept as a separate formalization target?
- Should the finite `#eval` witnesses be extracted into a single `Unsolved/Witnesses.lean` module to avoid re-running expensive checks during every stub build?
- Should the survey's 30x30 reduction matrix be formalized as a `Finset`-based relation between `ProblemMetadata.rrcId` values before the stubs are expanded beyond these seven?