Add Python CI + Theorem N (Lean) formalization scaffold

.github/workflows/ci.yml

@@ -2,51 +2,34 @@ name: CI
 
 on:
   push:
-    branches: [main]
+    paths:
+      - 'ucns/**'
+      - 'ucns_recursive/**'
+      - 'tests/**'
+      - 'pyproject.toml'
+      - '.github/workflows/ci.yml'
   pull_request:
-    branches: [main]
-  workflow_dispatch:
+    paths:
+      - 'ucns/**'
+      - 'ucns_recursive/**'
+      - 'tests/**'
+      - 'pyproject.toml'
+      - '.github/workflows/ci.yml'
 
 jobs:
-  tests:
+  test:
     runs-on: ubuntu-latest
-    strategy:
-      fail-fast: false
-      matrix:
-        python-version: ["3.8", "3.10", "3.12"]
-
     steps:
-      - uses: actions/checkout@v4
+      - name: Checkout
+        uses: actions/checkout@v4
 
-      - name: Set up Python ${{ matrix.python-version }}
+      - name: Set up Python 3.11
         uses: actions/setup-python@v5
         with:
-          python-version: ${{ matrix.python-version }}
-
-      - name: Install package
-        run: pip install -e .
+          python-version: '3.11'
 
-      - name: Import check (stdlib-only)
-        run: python -c "import ucns_recursive; print('OK, stdlib-only')"
+      - name: Install package (with dev extras)
+        run: python -m pip install -e .[dev]
 
-      - name: Run tests
+      - name: Run ucns_recursive unittest suite
         run: python -m unittest discover ucns_recursive/tests/ -v
-
-  verification-scripts:
-    runs-on: ubuntu-latest
-    needs: tests
-
-    steps:
-      - uses: actions/checkout@v4
-
-      - name: Set up Python 3.12
-        uses: actions/setup-python@v5
-        with:
-          python-version: "3.12"
-
-      - name: Install package
-        run: pip install -e .
-
-      - name: Run depth-3 sweep
-        timeout-minutes: 5
-        run: python code/sweeps/depth3_sweep.py

formal/README.md

@@ -0,0 +1,55 @@
+# UCNS Formal — Lean 4 scaffold for Theorem N
+
+This directory is a **Lean 4 scaffold** for machine-checking the UCNS
+completeness results, principally the Theorem N family described in
+[`../ucns-theorem-n.md`](../ucns-theorem-n.md).
+
+## Status: FRONTIER / awaiting external formal review
+
+This is exploratory scaffolding. **The theorem statements here are stubbed
+with `sorry` and prove nothing yet.** Lean will accept the file (a `sorry`
+closes any goal) but each `sorry` is an unverified hole — no proof obligation
+has been discharged. The statements themselves may also be imprecise
+transcriptions of the informal claims and are subject to revision during
+formal review.
+
+The informal, prose-level argument for Theorem N (and its instances Lemma 7
+and the depth-3 results) lives in [`../ucns-theorem-n.md`](../ucns-theorem-n.md).
+That document is the source of truth for the *claims*; this directory is an
+attempt to restate those claims in a form a proof assistant could eventually
+check.
+
+## Proof-status non-transfer discipline
+
+**A `sorry`-backed statement confers no `DEFENDED` status to any consumer
+repository.** Concretely:
+
+- A `theorem ... := sorry` in this directory is *not* a proof. It is a
+  placeholder for a proof that does not yet exist.
+- No downstream repository, package, or claim may cite this scaffold as
+  evidence that any UCNS result is formally verified.
+- A result graduates from FRONTIER only when every `sorry` in its statement
+  (and its transitive dependencies) has been removed and replaced by a
+  complete, type-checked proof term, and that has been confirmed by external
+  formal review.
+
+Until then, treat everything here as a specification draft, not a guarantee.
+
+## Layout
+
+- `lean-toolchain` — pins the Lean 4 toolchain version.
+- `lakefile.lean` — minimal Lake package definition (`Ucns`).
+- `Ucns/TheoremN.lean` — stub statements (all `sorry`) for:
+  - depth-1 restricted completeness,
+  - the depth-2 oracle result (Lemma 7),
+  - catalogue-sufficient completeness (Theorem N).
+
+## Building (once Lean is installed)
+
+```sh
+# from this directory, with elan/lake installed
+lake build
+```
+
+A successful `lake build` here means only that the *statements* type-check
+with their `sorry` placeholders — it does **not** mean the theorems are proven.

formal/Ucns/TheoremN.lean

@@ -0,0 +1,113 @@
+/-
+  Ucns.TheoremN
+  =============
+
+  Lean 4 scaffold for the UCNS Theorem N family.
+
+  SOURCE OF TRUTH FOR THE CLAIMS: ../../ucns-theorem-n.md
+
+  STATUS: FRONTIER / awaiting external formal review.
+
+  Every statement in this file is closed with `sorry`. A `sorry` is an
+  UNVERIFIED HOLE: Lean accepts the file, but nothing here is proven. These
+  are statement stubs, not proofs. Per the proof-status non-transfer
+  discipline (see README.md), a `sorry`-backed statement confers NO DEFENDED
+  status to any consumer repository.
+
+  The abstract objects below (UCNSObject, multiply, catalogues, the search
+  procedure factor_search_v08) are modelled as opaque placeholders so the
+  statements can be written down. Faithful definitions are future work and
+  are themselves part of what external formal review must check.
+-/
+
+namespace Ucns
+
+/-- A UCNS object. Placeholder carrier; the real structure is the recursive
+    `(angle, payload)` sequence object of `ucns-spec.md` / `ucns-theorem-n.md`
+    §1.1. Opaque here so the Theorem N statements can be stated. -/
+opaque UCNSObject : Type
+
+/-- The recursive product `multiply(A, B)` of `ucns-theorem-n.md` §1.1.
+    Placeholder. -/
+opaque multiply : UCNSObject → UCNSObject → UCNSObject
+
+/-- The recursion depth of a UCNS object (depth-1 = atomic payloads, etc.),
+    as used throughout `ucns-theorem-n.md`. Placeholder. -/
+opaque depth : UCNSObject → Nat
+
+/-- Number of top-level `A_plus` cells of an object (`|A.A_plus|`). -/
+opaque width : UCNSObject → Nat
+
+/-- A catalogue `C`: a candidate set of payloads (`UCNSObject | None`), modelled
+    here as a list of objects. See §1.2. Placeholder. -/
+abbrev Catalogue : Type := List UCNSObject
+
+/-- `ContainsPayloads C X` holds when the catalogue `C` contains every payload
+    appearing recursively in `X` (including the identity). This is the single
+    hypothesis of Theorem N ("the catalogue contains the necessary payloads").
+    Placeholder predicate. -/
+opaque ContainsPayloads : Catalogue → UCNSObject → Prop
+
+/-- `FindsFactorization P C` holds when `factor_search_v08(P, C)` returns a pair
+    `(A', B')` with `multiply A' B' = P`. Models the success of the depth-agnostic
+    search procedure of §1.3. Placeholder predicate. -/
+opaque FindsFactorization : UCNSObject → Catalogue → Prop
+
+/--
+  **Depth-1 restricted completeness (stub).**
+
+  Informal claim: for depth-1 factors `A`, `B` whose (atomic) payloads are all
+  present in the catalogue `C`, the search procedure recovers a factorization of
+  `P = multiply A B`. This is the base/restricted case underneath the depth-2
+  oracle result and Theorem N (cf. `ucns-theorem-n.md` §4).
+
+  STUB: proves nothing — closed by `sorry`.
+-/
+theorem depth1_restricted_completeness
+    (A B : UCNSObject) (C : Catalogue)
+    (hA : depth A ≤ 1) (hB : depth B ≤ 1)
+    (hwA : 1 ≤ width A) (hwB : 1 ≤ width B)
+    (hCA : ContainsPayloads C A) (hCB : ContainsPayloads C B) :
+    FindsFactorization (multiply A B) C := by
+  sorry
+
+/--
+  **Lemma 7 — depth-2 oracle completeness (stub).**
+
+  Informal claim (`ucns-theorem-n.md` §4.1): for `A, B` in the depth-2 oracle
+  class `D'_oracle` (depth ≤ 2), every payload of `A` and `B` is a depth-1
+  oracle atom and so lies in the generated payload catalogue `C`; the search
+  procedure is therefore complete. Presented in §2/§4 as an instance of
+  Theorem N rather than an independent result.
+
+  STUB: proves nothing — closed by `sorry`.
+-/
+theorem lemma7_depth2_oracle_completeness
+    (A B : UCNSObject) (C : Catalogue)
+    (hA : depth A ≤ 2) (hB : depth B ≤ 2)
+    (hwA : 1 ≤ width A) (hwB : 1 ≤ width B)
+    (hCA : ContainsPayloads C A) (hCB : ContainsPayloads C B) :
+    FindsFactorization (multiply A B) C := by
+  sorry
+
+/--
+  **Theorem N — catalogue-sufficient factorization (stub).**
+
+  Informal claim (`ucns-theorem-n.md` §2): let `A`, `B` be UCNS objects with
+  `|A.A_plus|, |B.A_plus| ≥ 1`, and let `C` be a catalogue containing every
+  payload appearing recursively in `A` or `B` (including the identity). Define
+  `P = multiply A B`. Then `factor_search_v08(P, C)` returns `(A', B')` with
+  `multiply A' B' = P`. There is NO depth parameter and NO oracle-class
+  predicate; the only hypothesis is that the catalogue contains the necessary
+  payloads. Lemma 7 and the depth-1 case above are instances.
+
+  STUB: proves nothing — closed by `sorry`.
+-/
+theorem theoremN_catalogue_sufficient_completeness
+    (A B : UCNSObject) (C : Catalogue)
+    (hwA : 1 ≤ width A) (hwB : 1 ≤ width B)
+    (hCA : ContainsPayloads C A) (hCB : ContainsPayloads C B) :
+    FindsFactorization (multiply A B) C := by
+  sorry
+
+end Ucns

formal/lakefile.lean

@@ -0,0 +1,11 @@
+import Lake
+open Lake DSL
+
+package «Ucns» where
+  -- Minimal Lake package for the UCNS Theorem N formalization scaffold.
+  -- See README.md: every statement here is currently `sorry`-backed and
+  -- proves nothing. This package exists so the stubs type-check.
+
+@[default_target]
+lean_lib «Ucns» where
+  -- Library root: Ucns/TheoremN.lean

formal/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.7.0