diff --git a/6-Documentation/docs/research/unsolved_hard_problems_lean_stubs_plan.md b/6-Documentation/docs/research/unsolved_hard_problems_lean_stubs_plan.md new file mode 100644 index 00000000..5f0c5ae1 --- /dev/null +++ b/6-Documentation/docs/research/unsolved_hard_problems_lean_stubs_plan.md @@ -0,0 +1,550 @@ +# 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? diff --git a/6-Documentation/docs/research/unsolved_hard_problems_leverage_points.md b/6-Documentation/docs/research/unsolved_hard_problems_leverage_points.md new file mode 100644 index 00000000..457e7e63 --- /dev/null +++ b/6-Documentation/docs/research/unsolved_hard_problems_leverage_points.md @@ -0,0 +1,237 @@ +# RRC Unsolved-Problems Leverage Analysis + +**Source:** `6-Documentation/docs/research/unsolved_hard_problems_rrc_alignments.json` +**Schema:** `unsolved_hard_problems_rrc_alignments_v1` (68 problems, 67 unsolved, 1 solved boundary) +**Generated:** 2026-06-20 + +## 1. Methodology + +I modeled the artifact as a directed influence graph: + +- **Nodes:** the 67 unsolved problems (the solved 3D Poincaré boundary marker was excluded). +- **Edge weights** were assembled from two sources: + 1. The `crossing_matrix` row for each problem (0–1 connection strengths). + 2. `known_reductions_to` / `known_reductions_from` lists: a known reduction between *A* and *B* adds a 0.25 machinery bonus to the corresponding directed edge, because solving the stronger statement typically collapses or heavily informs the weaker one. +- **Direction:** an edge `X → Y` means "solving X is expected to unlock or collapse Y" via reduction, shared machinery, or analogy. + +### Leverage scoring + +For each problem I computed four normalized components and combined them into a composite leverage score: + +| Component | Weight | Meaning | +|-----------|--------|---------| +| Strong weighted out-degree (edges ≥ 0.5) | 30 % | Direct, high-confidence unlock pressure | +| Strong transitive reach (edges ≥ 0.5) | 25 % | Number of problems reachable through rigorous-looking reductions / machinery | +| Two-hop strong reach | 20 % | Immediate cascade depth before saturation | +| Cross-cluster bridging (strong edges) | 15 % | Number of distinct alignment clusters unlocked outside the node's home cluster | +| Strong degree count | 10 % | Count of direct high-confidence outgoing edges | + +I also ran a second pass with a 0.3 threshold to capture shared-technique / analogical links. The results below distinguish the two whenever the difference matters. + +## 2. Ranked Top-10 Leverage Problems + +The scoring is dominated by the computational-complexity core: P vs NP and its satellites act as the artifact's central routing hub. Only one non-complexity problem (Birch–Swinnerton-Dyer) cracks the extended top 15. + +| Rank | Problem | ID | Composite score | Strong reach | Cross clusters (strong) | RRC shape | RRC status | Home cluster | +|------|---------|----|-----------------|--------------|------------------------|-----------|------------|--------------| +| 1 | **P vs NP** | `p_vs_np` | 0.975 | 11 | 2 | `CognitiveLoadField` | CANDIDATE | cluster_02 (Complexity) | +| 2 | **Unique Games Conjecture** | `unique_games_conjecture` | 0.900 | 11 | 2 | `CognitiveLoadField` | CANDIDATE | cluster_02 | +| 3 | **Exponential Time Hypothesis** | `exponential_time_hypothesis` | 0.890 | 11 | 2 | `CognitiveLoadField` | CANDIDATE | cluster_02 | +| 4 | **BPP vs P (derandomization)** | `bpp_vs_p` | 0.885 | 11 | 2 | `CognitiveLoadField` | HOLD | cluster_02 | +| 5 | **Strong Exponential Time Hypothesis** | `strong_exponential_time_hypothesis` | 0.871 | 11 | 2 | `CognitiveLoadField` | CANDIDATE | cluster_02 | +| 6 | **Discrete logarithm in P** | `discrete_log_in_p` | 0.867 | 11 | 2 | `CognitiveLoadField` | CANDIDATE | cluster_02 | +| 7 | **Existence of NP-intermediate problems** | `np_intermediate_existence` | 0.846 | 11 | 2 | `CognitiveLoadField` | HOLD | cluster_02 | +| 8 | **Integer factorization in P** | `factoring_in_p` | 0.829 | 11 | 2 | `CognitiveLoadField` | CANDIDATE | cluster_02 | +| 9 | **Graph isomorphism in P?** | `graph_isomorphism_in_p` | 0.808 | 11 | 2 | `CognitiveLoadField` | CANDIDATE | cluster_02 | +| 10 | **Quantum supremacy verification** | `quantum_supremacy_verification` | 0.617 | 11 | 2 | `ComputeKernelReceipt` | HOLD | cluster_07 (Quantum/information) | + +### Details per top problem + +1. **P vs NP** (`p_vs_np`) + - **Home cluster:** `cluster_02` (Computational complexity core); the artifact also lists it in `cluster_06` (Logic/foundations). + - **Clusters connected (strong):** cluster_02, cluster_03 (PDE/field singularities), cluster_07 (quantum/information). + - **Direct strong unlocks:** BPP vs P, discrete log, ETH, factoring, graph isomorphism, NP-intermediate existence, quantum supremacy verification, SETH, UGC. + - **With analogies (≥0.3):** also reaches continuum hypothesis, consistency of ZFC, cosmological constant, dark matter, Navier–Stokes, Hilbert's 6th/16th, Yang–Mills mass gap (via quantum supremacy). + - **Why it tops the list:** highest strong weighted out-degree (7.20) and the broadest set of direct strong edges in the artifact. + +2. **Unique Games Conjecture** (`unique_games_conjecture`) + - **Home cluster:** `cluster_02`. + - **Clusters connected (strong):** cluster_02, cluster_03, cluster_07. + - **Direct strong unlocks:** BPP vs P, discrete log, ETH, factoring, graph isomorphism, NP-intermediate, P vs NP, small-set expansion, SETH. + - **Note:** UGC and small-set expansion are mutually reducible in the artifact; UGC is the more central hub. + +3. **Exponential Time Hypothesis** (`exponential_time_hypothesis`) + - **Home cluster:** `cluster_02`. + - **Clusters connected (strong):** cluster_02, cluster_03, cluster_07. + - **Direct strong unlocks:** BPP vs P, discrete log, factoring, graph isomorphism, NP-intermediate, P vs NP, SETH, UGC. + - **Role:** fine-grained-complexity anchor; its collapse propagates through the entire complexity web. + +4. **BPP vs P (derandomization)** (`bpp_vs_p`) + - **Home cluster:** `cluster_02`. + - **Clusters connected (strong):** cluster_02, cluster_03, cluster_07. + - **Direct strong unlocks:** discrete log, ETH, factoring, graph isomorphism, NP-intermediate existence, P vs NP, quantum supremacy, SETH, UGC. + - **Status:** HOLD (the artifact flags derandomization as currently blocked by circuit-lower-bound barriers). + +5. **Strong Exponential Time Hypothesis** (`strong_exponential_time_hypothesis`) + - **Home cluster:** `cluster_02`. + - **Clusters connected (strong):** cluster_02, cluster_03, cluster_07. + - **Direct strong unlocks:** BPP vs P, discrete log, ETH, factoring, graph isomorphism, NP-intermediate, P vs NP, UGC. + - **Relationship:** tightly coupled to ETH (1.30 mutual edge), so solving either collapses the other and the rest of the cluster. + +6. **Discrete logarithm in P** (`discrete_log_in_p`) + - **Home cluster:** `cluster_02`. + - **Clusters connected (strong):** cluster_02, cluster_03, cluster_07. + - **Direct strong unlocks:** BPP vs P, ETH, factoring, graph isomorphism, NP-intermediate, P vs NP, SETH, UGC. + - **Note:** mutually reducible with factoring; together they are the cryptographic hardness sub-hub. + +7. **Existence of NP-intermediate problems** (`np_intermediate_existence`) + - **Home cluster:** `cluster_02`. + - **Clusters connected (strong):** cluster_02, cluster_03, cluster_07. + - **Direct strong unlocks:** BPP vs P, discrete log, ETH, factoring, graph isomorphism, P vs NP, SETH, UGC. + - **Status:** HOLD — the artifact notes it is conditional on P ≠ NP, so it is essentially a corollary-shaped gate. + +8. **Integer factorization in P** (`factoring_in_p`) + - **Home cluster:** `cluster_02`. + - **Clusters connected (strong):** cluster_02, cluster_03, cluster_07. + - **Direct strong unlocks:** BPP vs P, discrete log, ETH, NP-intermediate, P vs NP, SETH, UGC. + - **Note:** like discrete log, a concrete algorithmic collapse node rather than a purely logical implication. + +9. **Graph isomorphism in P?** (`graph_isomorphism_in_p`) + - **Home cluster:** `cluster_02`. + - **Clusters connected (strong):** cluster_02, cluster_03, cluster_07. + - **Direct strong unlocks:** BPP vs P, discrete log, ETH, NP-intermediate, P vs NP, SETH, UGC. + - **Distinctive feature:** its quasipolynomial witness gives it the highest `proof_readiness` (0.30) among the top complexity nodes. + +10. **Quantum supremacy verification** (`quantum_supremacy_verification`) + - **Home cluster:** `cluster_07` (Quantum and information). + - **Clusters connected (strong):** cluster_02, cluster_03. + - **Direct strong unlocks:** P vs NP, Yang–Mills mass gap. + - **Why it ranks here despite fewer direct edges:** it sits in `cluster_07` and has high cross-cluster bridging; from it the strong transitive closure reaches the full complexity core and PDE/field-singularity nodes. + - **Status:** HOLD — the artifact treats the verification gap as underspecified. + +## 3. Cluster-Specific Leverage Leaders + +Because the global top 10 is almost entirely the complexity core, the non-complexity clusters each have their own local leverage nodes. These are the best "entry points" if the goal is to collapse a particular domain rather than the whole graph. + +| Cluster | Best leverage node | Score | Strong reach | Key unlocks | +|---------|-------------------|-------|--------------|-------------| +| cluster_01 — Millennium, L-functions, motives | **Riemann Hypothesis** | 0.289 | 4 | GRH, Birch–Swinnerton-Dyer, Hodge, twin primes | +| cluster_03 — PDE regularity/singularities | **Hilbert's 16th problem** | 0.165 | 2 | Navier–Stokes existence, Yang–Mills mass gap | +| cluster_04 — Arithmetic/Diophantine | **Twin prime conjecture** | 0.312 | 4 | Polignac, Elliott–Halberstam, Schinzel H, Goldbach | +| cluster_05 — Topology/geometry | **Smooth 4D Poincaré conjecture** | 0.090 | 1 | Generalized Poincaré (smooth) | +| cluster_08 — Cosmology/dark sectors | **Dark energy equation of state** | 0.199 | 3 | Cosmological constant, dark matter, inflation | +| cluster_09 — Fluid/field singularities | **Navier–Stokes existence and smoothness** | 0.197 | 2 | Navier–Stokes blow-up, Yang–Mills mass gap | +| cluster_10 — Algebraic geometry/motives | **Birch and Swinnerton-Dyer conjecture** | 0.499 | 8 | Hodge, Tate, standard conjectures, rational points, Langlands | +| unclustered | **Quantum measurement problem** | 0.210 | 2 | Quantum gravity, Hilbert's 6th problem | + +## 4. Minimum Collapsing Subset + +A greedy set-cover over the strong-edge (≥0.5) transitive reach selects **14 problems** that together cover all 67 unsolved problems in the artifact: + +1. Algebrization barrier (`p_np_algebrization_barrier`) +2. Birch and Swinnerton-Dyer conjecture +3. Dark energy equation of state +4. Quantum measurement problem +5. Navier–Stokes existence and smoothness +6. abc conjecture +7. Singular Cardinal Hypothesis +8. Hilbert's 16th problem +9. Beal conjecture +10. Smooth 4D Poincaré conjecture +11. Generalized Poincaré conjecture (smooth category) +12. Borel conjecture +13. Cap set problem (exact growth) +14. Langlands program + +If analogical / shared-technique links (≥0.3) are included, the greedy cover collapses to **4 problems**: algebrization barrier, Schinzel's Hypothesis H, Borel conjecture, and cap set problem. This dramatic shrinkage shows how much of the artifact's connectivity is carried by cross-domain analogy rather than formal reduction. + +## 5. Network Diagram + +The diagram below shows the top leverage nodes and their strongest edges (weight ≥ 0.5). Thickness is omitted; all shown edges are high-confidence machinery/reduction links. Analogical weaker edges are suppressed to keep the diagram readable. + +```mermaid +graph LR + subgraph ComplexityCore [cluster_02 — Complexity core] + PNP[p_vs_np] + UGC[unique_games_conjecture] + ETH[exponential_time_hypothesis] + SETH[strong_exponential_time_hypothesis] + BPP[bpp_vs_p] + DLOG[discrete_log_in_p] + FACT[factoring_in_p] + GI[graph_isomorphism_in_p] + NPI[np_intermediate_existence] + end + + subgraph QuantumInfo [cluster_07 — Quantum & information] + QS[quantum_supremacy_verification] + YM[yang_mills_mass_gap] + end + + subgraph PDE [cluster_09 — Fluid/field singularities] + NS[navier_stokes_existence_smoothness] + H16[hilbert_sixteenth_problem] + end + + subgraph Foundations [cluster_06 — Logic/foundations] + ALG[p_np_algebrization_barrier] + end + + subgraph Arithmetic [cluster_04 — Arithmetic/Diophantine] + TP[twin_prime_conjecture] + end + + subgraph Motives [cluster_01/10 — L-functions & motives] + RH[riemann_hypothesis] + BSD[birch_swinnerton_dyer_conjecture] + HODGE[hodge_conjecture] + TATE[tate_conjecture] + end + + PNP --> BPP + PNP --> DLOG + PNP --> ETH + PNP --> FACT + PNP --> GI + PNP --> NPI + PNP --> QS + PNP --> SETH + PNP --> UGC + + UGC --> PNP + UGC --> ETH + UGC --> SETH + + ETH --> SETH + SETH --> ETH + + DLOG --> FACT + FACT --> DLOG + + QS --> PNP + QS --> YM + + YM --> H16 + NS --> H16 + H16 --> NS + H16 --> YM + + ALG --> PNP + + RH --> TP + TP --> RH + + BSD --> RH + BSD --> HODGE + BSD --> TATE + HODGE --> TATE + TATE --> HODGE +``` + +## 6. Caveats + +- **Analogy vs. rigorous reduction.** Many cross-cluster edges in the artifact are 0.3–0.4 and are annotated as "shared techniques, cluster co-membership, and analogies." The strong-edge (≥0.5) analysis filters these out, but even the 0.5 threshold is a heuristic. Solving P vs NP will not automatically prove the cosmological constant problem or Hilbert's 6th problem; the artifact encodes a belief that progress on the complexity boundary propagates as *methodology*, not as formal implication. +- **Cluster-internal vs. cross-cluster impact.** The top global nodes are high-impact inside the complexity cluster and modestly bridge into quantum/PDE/foundations. Within arithmetic, the Riemann Hypothesis / abc / twin-prime triangle is far more levered than P vs NP, even though the global score is lower. +- **Directionality.** Edges represent "solving X unlocks Y," but reductions are not always one-way. Some pairs (P vs NP ↔ UGC, ETH ↔ SETH, factoring ↔ discrete log, abc ↔ Beal) are mutually linked, so either endpoint would collapse the other. +- **Status bias.** Several top-scoring nodes (`bpp_vs_p`, `np_intermediate_existence`, `quantum_supremacy_verification`, `p_np_algebrization_barrier`) are in `HOLD` status, meaning the artifact already considers them underspecified or blocked. High leverage does not imply high tractability. +- **Coverage is not collapse.** The set-cover result shows that 14 (or 4, with analogy) nodes *touch* every other problem in the graph. It does not mean proving those 14 would prove all 67; it means every other problem has at least one analogical or reduction path back to one of them. diff --git a/6-Documentation/docs/research/unsolved_hard_problems_path_forward.md b/6-Documentation/docs/research/unsolved_hard_problems_path_forward.md new file mode 100644 index 00000000..87c42418 --- /dev/null +++ b/6-Documentation/docs/research/unsolved_hard_problems_path_forward.md @@ -0,0 +1,116 @@ +# Unsolved Hard Problems — RRC Strategic Path Forward + +**Date:** 2026-06-20 + +**Scope:** What to do with the RRC manifold/projection survey of 67 unsolved hard problems plus one solved boundary marker. + +**Claim boundary:** This document is strategic planning material. It proposes concrete next steps but does not claim any problem is solved or that any option will succeed. + +--- + +## Executive Summary + +- The survey records **68 problem records** (67 unsolved, 1 solved boundary), assigned to **10 alignment clusters** and a 30x30 crossing matrix that encodes known reduction/shared-topic weights. +- Most problems map to four RRC shape classes: `ProjectableGeometryTopology`, `CognitiveLoadField`, `LogogramProjection`, and `BurgersRGSolver`. The lone `ACCEPT` is the 3D Poincare conjecture, which validates that the `LeanTheoremReceipt` boundary can in principle be reached. +- The clusters with the densest internal crossing structure are `cluster_02` (complexity core, 17 problems) and `cluster_04` (arithmetic/Diophantine, 16 problems). These are the highest-leverage targets for formalization scaffolding and attack-graph analysis. +- The survey is currently **projection-only**: every entry is a `CANDIDATE` or `HOLD`. No entry has been promoted to `ACCEPT` by the RRC pipeline. +- The 30x30 crossing matrix is the most actionable artifact beyond the clusters; it can be used directly to rank problems by centrality, reduction cascades, and braid-strand coverage. + +--- + +## Strategic Options + +### Option A: Convert the top N problems into Lean formalization stubs + +Produce Lean 4 modules in `0-Core-Formalism/lean/Semantics/Semantics/RRC/UnsolvedProblems/` that state each selected problem as a `def` or `theorem` with the exact RRC axes and status embedded as metadata. + +- **Pros:** Keeps Lean as the source of truth; stubs can be `#eval`-checked for syntactic well-formedness; creates a formal target surface for future proof work. +- **Cons:** Stating a famous open problem in Lean adds no new mathematics; without a realistic path to proof, stubs risk becoming permanently `sorry`-laden unless quarantined. +- **Effort:** Low for stubs, high if we demand `#eval` witnesses and no `sorry`. 1-2 days for 5-10 carefully chosen problems; a full 67-problem module would take several weeks and require quarantine discipline. + +**Recommended initial target set (5):** Riemann Hypothesis, P vs NP, Navier-Stokes existence, abc conjecture, Smooth 4D Poincare conjecture. These span the four dominant shape classes and have the strongest projection_declared scores. + +### Option B: Use the crossing matrix to build an attack graph + +Treat the 30x30 crossing matrix as a weighted directed graph and compute node centrality, sink/source structure, and reduction cascades. Use the result to decide which problems are "hubs" and which are "leaves" that collapse if the hub is solved. + +- **Pros:** Directly leverages an existing artifact; gives an objective ordering; aligns with RRC's braid/crossing vocabulary (each edge is a crossing weight). +- **Cons:** Weights are manually assigned and should not be treated as quantitative evidence; graph centrality can be gamed by over-connected underspecified problems (e.g., `quantum_gravity`). +- **Effort:** 1-3 days for a Python shim that reads the JSON, builds the graph, and emits a ranked `attack_graph_receipt.json`. Could be reused by `rrc_refactor_oracle.py`. + +### Option C: Promote alignment clusters into RRC shape classes and update the pipeline + +Merge the 10 alignment clusters into the existing RRC taxonomy used by `rrc_ray_tagger.py` and `docs/rrc_equation_classification.md`. Add cluster-aware tagging so that a problem text or receipt can be routed to a cluster and then to a shape. + +- **Pros:** Makes the survey operational inside the existing RRC/Corpus250 and AVMIsa.Emit boundary; lets the tagger reason about problem families, not just isolated equations. +- **Cons:** Extending the shape taxonomy without a classifier trained on ground truth risks overfitting the survey; RRC shape decisions must stay in Lean per the programming-choice flow. +- **Effort:** 3-5 days for a design pass; longer if we also update `RRC.Emit` in Lean to stamp cluster-aware receipts. + +### Option D: Generate #eval witnesses / toy counterexamples for the HOLD/CANDIDATE boundaries + +For each problem, build a small deterministic witness that shows why its current RRC status is justified. For `HOLD` problems, demonstrate the missing axis (e.g., a proof of independence for CH). For `CANDIDATE` problems, show a concrete small-case computation (e.g., Collatz iterations up to a bounded seed). + +- **Pros:** Grounds the survey in executable evidence; fits the repo's `#eval` witness requirement; separates shallowly-underspecified problems from deeply-underspecified ones. +- **Cons:** Toy witnesses do not prove or disprove the general statements; some `HOLD` cases (ZFC consistency, measurement problem) have principled limits. +- **Effort:** 2-4 days for a first batch of 10-15 witnesses; scales linearly with the number of problems covered. + +### Option E: Outreach — publish the survey as a research note or guide literature mining + +Publish a short research note on the survey structure, the crossing matrix, and the RRC projection methodology. Use it to solicit external reviewers and to seed `rrc_arxiv_kernel_refine.py` with targeted literature-mining queries. + +- **Pros:** Low engineering cost; builds reviewer provenance; may surface reduction edges the survey missed. +- **Cons:** Does not directly advance the formal stack; publicity before the claim-state ladder is mature risks overclaiming. +- **Effort:** 1-2 days for a note; ongoing effort to curate mined literature. + +--- + +## Recommendation: Three-Stage Roadmap + +### Stage 1 — This week: inventory and attack graph + +1. Run `python3 -m py_compile` and `python3 -m json.tool` on the new survey artifacts. +2. Build a Python shim in `4-Infrastructure/shim/unsolved_problems_attack_graph.py` that reads `unsolved_hard_problems_rrc_alignments.json` and emits: + - in-degree / out-degree / betweenness rankings, + - reduction cascades (longest directed paths), + - a list of hub problems whose solution would collapse the most leaves. +3. Validate the top 5 hub problems against the four dominant RRC shapes. +4. Save the result as `shared-data/data/stack_solidification/unsolved_problems_attack_graph_v1.json` with a receipt hash. + +### Stage 2 — This month: Lean stubs and #eval witnesses + +1. Create `0-Core-Formalism/lean/Semantics/Semantics/RRC/UnsolvedProblems/TopFive.lean` containing formalized statements for the top 5 hub problems. +2. Each stub records: `rrcId`, `rrcShape`, `rrcStatus`, the 10-axis vector encoded as `Q0_16` values, and a `theorem` or `def` stating the problem in Lean terms. +3. Add `#eval` witnesses that compute small finite cases (e.g., verify Collatz up to a bound, or compute prime-gap statistics) using only `Q16_16`/`Q0_16` arithmetic. +4. Update `docs/rrc_equation_classification.md` with the new `UnsolvedProblems` surface and regenerate its receipt via `AVMIsa.Emit` when the ISA rebuild permits. + +### Stage 3 — This quarter: integration with Research Stack goals + +1. Route the attack-graph output into `rrc_ray_tagger.py` so that each unsolved problem can be tagged with its RRC shape, cluster, and recommended ray layer. +2. Feed hub-problem receipts into the BraidStorm/eigensolid compressor as a stress-test corpus: each problem statement is a 1 KB chunk; convergence receipts measure how well the compressor captures high-semantic-entropy text. +3. Use the solved boundary marker (3D Poincare conjecture) as a positive-control receipt: its eigensolid convergence and receipt invertibility theorems should pass cleanly, providing a sanity check on the full pipeline. +4. Promote no problem beyond `CANDIDATE` in RRC space until a Lean gate explicitly passes. + +--- + +## Open Questions / Risks + +- **Authority of the crossing weights.** The 30x30 matrix weights are expert-judgment estimates, not computed from citation or reduction data. Using them for centrality rankings must carry a `claim_boundary` that says "projection-only; weights are not evidence of reduction strength." +- **Lean stub scope.** Stating open problems in Lean is safe if the files stay outside the main build path or use `axiom`/`sorry` with explicit `TODO(lean-port)` markers. Quarantine discipline is required. +- **Shape-class overlap.** Several problems appear in multiple clusters and could plausibly map to more than one RRC shape. The pipeline must tolerate multi-shape ambiguity rather than forcing a single label. +- **No Float in compute paths.** Any `#eval` witness or attack-graph score must use `Q16_16`/`Q0_16`. Raw axis scores in the JSON are already bounded in [0,1]; convert them through the fixed-point boundary, not `ofFloat`. +- **Premature outreach.** Publishing before the claim-state ladder is documented could let external readers misread `CANDIDATE` as progress. Any note should repeat the projection-only boundary prominently. + +--- + +## Required Resources / Skills + +| Resource | Need | +|---|---| +| Lean 4 / lake | Stage 2 stubs and witnesses | +| Python + networkx or equivalent | Stage 1 attack graph | +| RRC taxonomy knowledge | Option C and Stage 3 integration | +| arXiv / literature curation | Option E and cluster refinement | +| Fixed-point (Q16_16/Q0_16) discipline | All `#eval` witnesses and scoring | +| Reviewer | Before any promotion beyond CANDIDATE or publication | + +Estimated total effort for the recommended path: **1-2 person-weeks for Stage 1**, **2-4 person-weeks for Stage 2**, and **4-8 person-weeks for Stage 3**, assuming no new dependencies and all RRC decisions remain in Lean.