diff --git a/.github/workflows/carrier-lcm-target.yml b/.github/workflows/carrier-lcm-target.yml new file mode 100644 index 00000000..bea4120e --- /dev/null +++ b/.github/workflows/carrier-lcm-target.yml @@ -0,0 +1,49 @@ +name: carrier-lcm target (Lean) + +# Targeted verifier for the Carrier-LCM proof frontier. +# This intentionally runs the exact pinned-toolchain command requested for +# PR acceptance; a green job means the file type-checks under formal/lean-toolchain, +# while remaining `sorry` leaves still retain their usual no-DEFENDED-status meaning. + +on: + workflow_dispatch: + pull_request: + paths: + - 'formal/**' + - '.github/workflows/carrier-lcm-target.yml' + +jobs: + carrier-lcm: + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@v4 + + - name: Install elan using formal/lean-toolchain + run: | + curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \ + | sh -s -- -y --default-toolchain "$(cat formal/lean-toolchain)" + + - name: Cache Lake packages + uses: actions/cache@v4 + with: + path: formal/.lake + key: carrier-lcm-lake-${{ hashFiles('formal/lean-toolchain', 'formal/lakefile.lean', 'formal/lake-manifest.json') }} + + - name: Build Ucns.CarrierLcm with pinned toolchain + run: | + source $HOME/.elan/env + cd formal + lake build Ucns.CarrierLcm + + - name: Reject admit/axiom in formal Lean files + run: | + if git grep -n -E '\b(admit|axiom)\b' -- 'formal/Ucns/*.lean'; then + echo 'admit/axiom found in formal Lean files' + exit 1 + fi + + - name: Report sorry leaves without certifying them + run: | + echo 'Open executable sorry leaves:' + git grep -n -E '\bsorry\b' -- 'formal/Ucns/*.lean' || true diff --git a/CLAUDE.md b/CLAUDE.md index b4cec7cc..95d54f32 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -31,7 +31,7 @@ experimental UCNS-native cache prototype. | Runtime dependencies | none (stdlib only) | | Optional extras | `dev` | | Keywords | unit-circle, factorization, recursive-algebra, sequence-theory, witness-matrix | -| CI workflows | `ci.yml`, `formal.yml`, `manifest-check.yml`, `python-package.yml` | +| CI workflows | `carrier-lcm-target.yml`, `ci.yml`, `formal.yml`, `manifest-check.yml`, `python-package.yml` | | Top-level directories | `code/` · `docs/` · `examples/` · `formal/` · `pcea-ucns/` · `scripts/` · `tests/` · `ucns/` · `ucns_cache/` · `ucns_recursive/` | Derived from `pyproject.toml` + the repo tree. Unknown fields surface as `hmmm` rather than a guess. diff --git a/formal/Ucns/CarrierLcm.lean b/formal/Ucns/CarrierLcm.lean index 3eaf4c77..0534e26b 100644 --- a/formal/Ucns/CarrierLcm.lean +++ b/formal/Ucns/CarrierLcm.lean @@ -14,9 +14,9 @@ lemmas) are targeted SORRY-FREE. - The Rat denominator leaves (`den_add_dvd_lcm`, `den_amod_dvd`) are discharged against the installed `Std` Rat API. - - Remaining `sorry` leaves are the slice-embedding proofs and the upper-bound - threading proof. A `sorry`-backed lemma confers NO DEFENDED status - (formal/README.md). + - The slice-embedding proofs compile under the pinned Lean/Lake build. + - Remaining `sorry` leaves include the upper-bound threading proof. A + `sorry`-backed lemma confers NO DEFENDED status (formal/README.md). -/ -- === MODULE_BUILD === @@ -37,7 +37,7 @@ -- rollback: remove file and its import from Ucns.lean -- requires: ucns_formal_core_definitions -- since: 2026-06-10 --- unresolved: slice-embedding leaves, upper-bound bind/map threading leaf +-- unresolved: upper-bound bind/map threading leaf -- === END MODULE_BUILD === import Ucns.Core @@ -128,6 +128,19 @@ theorem head_angle_zero_of_complete (A : UCNSObject) (hA : Complete A) c.angle = 0 := hostNormalized_of_complete A hA c hc +/-- A cell returned by `head?` is a member of the same list. + + Local replacement for newer `List.mem_of_mem_head?` API names that are not + present in the pinned Lean 4.7.0/Std version. -/ +theorem mem_of_head?_eq_some {α : Type} {xs : List α} {x : α} + (h : xs.head? = some x) : x ∈ xs := by + cases xs with + | nil => + simp at h + | cons y ys => + simp at h + simp [h] + /-- `Rat.floor` shifts predictably by an integer. Local bridge from the protected `Rat.floor` used by `amod` to Mathlib's @@ -163,6 +176,24 @@ theorem circleFrac_amod4 (a : Rat) : circleFrac (amod4 a) = circleFrac a := by rw [Int.cast_sub, Int.cast_mul] ring +/-- Membership in `angleDenoms` is exactly a cell whose nonzero circle fraction + has the requested denominator. This packages the `map`/`filterMap` shape so + slice proofs can focus on constructing product cells. -/ +theorem mem_angleDenoms_iff (x : Nat) (cs : List (Cell UCNSObject)) : + x ∈ angleDenoms cs ↔ + ∃ c, c ∈ cs ∧ circleFrac c.angle ≠ 0 ∧ (circleFrac c.angle).den = x := by + unfold angleDenoms + simp only [List.mem_filterMap, List.mem_map] + constructor + · rintro ⟨q, ⟨c, hc, rfl⟩, hq⟩ + by_cases hz : circleFrac c.angle = 0 + · simp [hz] at hq + · simp [hz] at hq + exact ⟨c, hc, hz, hq⟩ + · rintro ⟨c, hc, hz, hden⟩ + refine ⟨circleFrac c.angle, ⟨c, hc, rfl⟩, ?_⟩ + simp [hz, hden] + /-! ## Analytic leaves (sorry-stubbed, precise hypotheses) -/ /-- The denominator emitted by `Rat.normalize` divides its input denominator. -/ @@ -252,25 +283,80 @@ theorem den_add_dvd_lcm (a b : Rat) : Repaired domain: use `Complete` operands so the empty-factor counterexample is excluded and host-normalization is supplied by `hostNormalized_of_complete`. - LEAF: list membership through bind/map + amod4 fixpoint under + Discharged by list membership through bind/map + amod4 fixpoint under range normalization. -/ theorem slice_embedding_left (A B : UCNSObject) (d : Nat) (hA : Complete A) (hB : Complete B) : ∀ x ∈ angleDenoms A.cells, x ∈ angleDenoms (multiplyFuel (d + 1) A B).cells := by - sorry + intro x hx + rcases mem_angleDenoms_iff x A.cells |>.mp hx with ⟨ca, hca, hca_ne, hca_den⟩ + rcases exists_head?_of_complete B hB with ⟨cb, hcb_head⟩ + have hcb_mem : cb ∈ B.cells := by + exact mem_of_head?_eq_some hcb_head + have hcb_zero : cb.angle = 0 := head_angle_zero_of_complete B hB hcb_head + refine (mem_angleDenoms_iff x (multiplyFuel (d + 1) A B).cells).mpr ?_ + refine ⟨ + { angle := amod4 (ca.angle + (cb.angle - (match B.cells.head? with + | some c => c.angle + | none => 0))) + face := xor ca.face cb.face + payload := + match ca.payload, cb.payload with + | some p, some q => some (multiplyFuel d p q) + | some p, none => some p + | none, some q => some q + | none, none => none }, + ?_, ?_, ?_⟩ + · cases A with + | mk nda csA => + cases B with + | mk ndb csB => + simp only [cells, multiplyFuel] + exact List.mem_bind.mpr ⟨ca, hca, List.mem_map.mpr ⟨cb, hcb_mem, rfl⟩⟩ + · simp [hcb_head, hcb_zero, circleFrac_amod4, hca_ne] + · simp [hcb_head, hcb_zero, circleFrac_amod4, hca_den] /-- Symmetric embedding for B (the k = 0 slice). Repaired domain: use `Complete` operands so the empty-factor counterexample is - excluded and host-normalization is supplied by `hostNormalized_of_complete`. LEAF. -/ + excluded and host-normalization is supplied by `hostNormalized_of_complete`. + Discharged by the symmetric list-membership witness construction. -/ theorem slice_embedding_right (A B : UCNSObject) (d : Nat) (hA : Complete A) (hB : Complete B) : ∀ x ∈ angleDenoms B.cells, x ∈ angleDenoms (multiplyFuel (d + 1) A B).cells := by - sorry + intro x hx + rcases mem_angleDenoms_iff x B.cells |>.mp hx with ⟨cb, hcb, hcb_ne, hcb_den⟩ + rcases exists_head?_of_complete A hA with ⟨ca, hca_head⟩ + rcases exists_head?_of_complete B hB with ⟨b0, hb0_head⟩ + have hca_mem : ca ∈ A.cells := by + exact mem_of_head?_eq_some hca_head + have hca_zero : ca.angle = 0 := head_angle_zero_of_complete A hA hca_head + have hb0_zero : b0.angle = 0 := head_angle_zero_of_complete B hB hb0_head + refine (mem_angleDenoms_iff x (multiplyFuel (d + 1) A B).cells).mpr ?_ + refine ⟨ + { angle := amod4 (ca.angle + (cb.angle - (match B.cells.head? with + | some c => c.angle + | none => 0))) + face := xor ca.face cb.face + payload := + match ca.payload, cb.payload with + | some p, some q => some (multiplyFuel d p q) + | some p, none => some p + | none, some q => some q + | none, none => none }, + ?_, ?_, ?_⟩ + · cases A with + | mk nda csA => + cases B with + | mk ndb csB => + simp only [cells, multiplyFuel] + exact List.mem_bind.mpr ⟨ca, hca_mem, List.mem_map.mpr ⟨cb, hcb, rfl⟩⟩ + · simp [hb0_head, hca_zero, hb0_zero, circleFrac_amod4, hcb_ne] + · simp [hb0_head, hca_zero, hb0_zero, circleFrac_amod4, hcb_den] /-! ## Bound lemmas and composition (sorry-free modulo leaves) -/