From 0330f19ec77552ea1ce4a8cf985eb5fbfaca947d Mon Sep 17 00:00:00 2001 From: Erin Spencer Date: Wed, 1 Jul 2026 16:31:08 -0700 Subject: [PATCH 1/3] add pinned Carrier-LCM Lean verifier --- .github/workflows/carrier-lcm-target.yml | 49 +++++ README.md | 4 +- REVIEW_PACKET.md | 23 +- formal/Ucns/CarrierLcm.lean | 261 +++++++++++++++++++++-- formal/Ucns/Core.lean | 8 +- formal/lake-manifest.json | 54 +++++ 6 files changed, 358 insertions(+), 41 deletions(-) create mode 100644 .github/workflows/carrier-lcm-target.yml 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/README.md b/README.md index 51689616..0ee7a618 100644 --- a/README.md +++ b/README.md @@ -57,7 +57,7 @@ Start here: - Collaboration issue: https://github.com/The-Interdependency/ucns/issues/7 - Starter task: define one UCNS term in standard mathematical language, with notation, example, non-example, and relationship to existing concepts. -The ask is bounded: help separate definitions, implemented algorithms, empirical results, proof sketches, conjectures, limitations, and counterexamples. +The ask is bounded: help separate definitions, implemented algorithms, empirical results, proof sketches, conjectures, limitations, and counterexamples. The current formal frontier is partially verified in Lean, with remaining proof leaves under active discharge. Cancellativity is not claimed globally; the valid target is the restricted `Complete` plus common-depth domain unless the live formalization proves a stronger restricted theorem. GPT generated; context, prompt Erin Spencer. @@ -76,7 +76,7 @@ Status vocabulary (from `docs/ucns-spec-status-addendum-2026-05-16.md`): | Depth-2 oracle (Lemma 7) | `DEFENDED` + `ORACLE-COMPLETE` | | Full frozen depth-2 domain | `IMPLEMENTED` + `TEST-BACKED` (not yet `DEFENDED` at spec level) | | Depth-3 asymmetric (Theorem 9) | `TEST-BACKED` (6/6 empirical) | -| **Catalogue-sufficient completeness — all depths (Theorem N)** | **`DEFENDED` — proof drafted, awaiting external formal review** | +| **Catalogue-sufficient completeness — all depths (Theorem N)** | **`FRONTIER` — partially verified in Lean; remaining proof leaves under active discharge** | | Tractable sub-catalogues | `FRONTIER` | | Carrier widening | `FRONTIER` / out of v1.0 scope | | General recursive primality outside defended-complete domains | out of v1.0 scope | diff --git a/REVIEW_PACKET.md b/REVIEW_PACKET.md index b578cb37..9f145403 100644 --- a/REVIEW_PACKET.md +++ b/REVIEW_PACKET.md @@ -43,13 +43,12 @@ doesn't. **Read first:** - `ucns-v06-completeness-proof.md` — the proof. Eight lemmas, theorem, - corollary. Depends on cancellativity (proven by induction sketch in - `ucns_v0_5_1_boundary.md`) and on already-frozen v0.3 / v0.4 results. + corollary. Depends on a restricted cancellativity target, not global cancellativity; the current formal frontier is partially verified in Lean, with remaining proof leaves under active discharge. **Reference (read as needed):** - `ucns-spec.md` — complete consolidated spec defining the objects, - the product, sequence equivalence, and the cancellativity sketch the + the product, sequence equivalence, and the restricted cancellativity frontier the completeness proof depends on. **Implementation (run if you want to check):** @@ -80,12 +79,7 @@ The completeness proof takes these as given: structurally and by tests. 2. **v0.4 None-as-unit normalization (Guard 1, E1.5).** Verified in the E6 oracle regression. -3. **E10.4 cancellativity.** Proven by induction sketch in the spec. - Empirically verified across 11,016 product pairs at depths 0 and 1 - (0 violations). The sketch is loose — promoting it to a fully written - induction is a known open task and would close the last methodological - loop. **If you want to challenge the proof's foundation, this is where - I'd look first.** +3. **E10.4 cancellativity.** Not claimed globally: `multiply_left_cancellative` is false in general. The surviving target is the restricted `Complete` plus common-depth domain unless the live Lean formalization proves a stronger restricted theorem. Empirical counterexample searches inform that domain, but empirical success does not imply proof completion. **If you want to challenge the proof's foundation, this is where I'd look first.** --- @@ -94,8 +88,8 @@ The completeness proof takes these as given: - The eight lemmas reduce to: host-data recovery is direct (Lemmas 2, 3), payload work is q independent recursive sub-problems (Lemma 4), recursion strictly decreases depth and bottoms out at `S^A_0 = None` (Lemmas 5, 6, - 7), each sub-call returns the unique correct value by induction + - cancellativity (Lemma 8). Theorem composes them. + 7), each sub-call returns the unique correct value only under the restricted + cancellativity hypotheses (Lemma 8). Theorem composes them. - Lemma 7's termination bound (`1 + d(A)` stack frames) is verified tight by `code/proof_trace.py` — observed depth equals predicted depth at d=1 and d=2. @@ -106,13 +100,10 @@ The completeness proof takes these as given: ## What I think is genuinely weak -- Cancellativity itself is on a sketch + extensive empirical, not on a - full written induction. The sketch is straightforward but not yet - prose-complete. +- Cancellativity is not global. The current formal frontier is partially verified in Lean, with remaining proof leaves under active discharge; the valid target is the restricted `Complete` plus common-depth domain unless the live formalization proves more. - `right_quotient` completeness is claimed by structural symmetry but the dual proof isn't written. Empirically verified on the same 900 cases. -- Verification beyond depth 2 is one-trace empirical (depth-2 oracle) plus - the proof's structural argument. No depth ≥ 3 examples have been run. +- Verification beyond depth 2 is empirical/frontier evidence plus the proof's structural argument. Empirical tests do not imply proof completion. If any of these matter to you, that's a real comment to leave. diff --git a/formal/Ucns/CarrierLcm.lean b/formal/Ucns/CarrierLcm.lean index b584542c..3f8129fe 100644 --- a/formal/Ucns/CarrierLcm.lean +++ b/formal/Ucns/CarrierLcm.lean @@ -12,10 +12,12 @@ - The lcm fold engine (`dvd_foldl_lcm`, `foldl_lcm_dvd`, `foldl_lcm_pos`) and the composition layer (`carrier_lcm_law'` from the two bound lemmas) are targeted SORRY-FREE. - - The analytic leaves (`denEngine` group: amod/denominator behavior over - Rat; `embedding` group: slice membership under host normalization) - remain `sorry`-stubbed with precise hypotheses. A `sorry`-backed - lemma confers NO DEFENDED status (formal/README.md). + - The Rat denominator leaves (`den_add_dvd_lcm`, `den_amod_dvd`) are + discharged against the installed `Std` Rat API. + - The slice-embedding proofs are structurally proposed in this file, but + require the pinned Lean/Lake build before being cited as discharged. + - Remaining `sorry` leaves include the upper-bound threading proof. A + `sorry`-backed lemma confers NO DEFENDED status (formal/README.md). -/ -- === MODULE_BUILD === @@ -36,12 +38,15 @@ -- rollback: remove file and its import from Ucns.lean -- requires: ucns_formal_core_definitions -- since: 2026-06-10 --- unresolved: denominator-of-sum leaf, amod-denominator leaf, slice-embedding leaf +-- unresolved: slice-embedding leaves, upper-bound bind/map threading leaf -- === END MODULE_BUILD === import Ucns.Core import Std.Data.Nat.Gcd +import Std.Data.Rat.Lemmas import Std.Data.List.Lemmas +import Mathlib.Data.Rat.Floor +import Mathlib.Tactic.Ring namespace Ucns namespace UCNSObject @@ -91,50 +96,268 @@ theorem nMin_dvd_of_denoms_subset (fun x hx => dvd_foldl_lcm x _ (h x hx) 1) 1 (Nat.one_dvd _) + +/-- A `Complete` object is host-normalized at the top level. -/ +theorem hostNormalized_of_complete (A : UCNSObject) (hA : Complete A) : + HostNormalized A := by + cases A with + | mk nd cs => + simp [Complete, HostNormalized, HostNormalizedRec] at hA ⊢ + exact hA.2.1.1 + +/-- A `Complete` object has a nonempty top-level cell list. -/ +theorem cells_ne_nil_of_complete (A : UCNSObject) (hA : Complete A) : + A.cells ≠ [] := by + cases A with + | mk nd cs => + simp [Complete, NonemptyRec] at hA ⊢ + exact hA.1.1 + +/-- A `Complete` object has a top-level head cell. -/ +theorem exists_head?_of_complete (A : UCNSObject) (hA : Complete A) : + ∃ c, A.cells.head? = some c := by + cases A with + | mk nd cs => + rcases List.exists_cons_of_ne_nil (cells_ne_nil_of_complete (UCNSObject.mk nd cs) hA) with + ⟨c, rest, hcs⟩ + subst hcs + exact ⟨c, rfl⟩ + +/-- The head cell of a `Complete` object has zero angle. -/ +theorem head_angle_zero_of_complete (A : UCNSObject) (hA : Complete A) + {c : Cell UCNSObject} (hc : A.cells.head? = some c) : + c.angle = 0 := + hostNormalized_of_complete A hA c hc + +/-- `Rat.floor` shifts predictably by an integer. + + Local bridge from the protected `Rat.floor` used by `amod` to Mathlib's + floor-ring notation/API. -/ +theorem rat_floor_sub_int (a : Rat) (z : Int) : + Rat.floor (a - (z : Rat)) = Rat.floor a - z := by + change ⌊a - (z : Rat)⌋ = ⌊a⌋ - z + exact Int.floor_sub_int a z + +/-- Taking the circle fraction after reducing modulo 4 is the same as taking + the circle fraction directly: the extra reduction only subtracts an even + integer before the final modulo-2 quotient. -/ +theorem circleFrac_amod4 (a : Rat) : circleFrac (amod4 a) = circleFrac a := by + unfold circleFrac amod4 amod + let z4 : Int := Rat.floor (a / (4 : Rat)) + let z2 : Int := Rat.floor (a / (2 : Rat)) + have hdiv : + (a - (4 : Rat) * (z4 : Rat)) / (2 : Rat) = + a / (2 : Rat) - ((z4 * 2 : Int) : Rat) := by + rw [Int.cast_mul] + ring + have hfloor : + Rat.floor ((a - (4 : Rat) * (z4 : Rat)) / (2 : Rat)) = z2 - z4 * 2 := by + rw [hdiv] + dsimp [z2] + exact rat_floor_sub_int (a / (2 : Rat)) (z4 * 2) + change + (a - (4 : Rat) * (z4 : Rat) - + (2 : Rat) * (Rat.floor ((a - (4 : Rat) * (z4 : Rat)) / (2 : Rat)) : Int)) / + (2 : Rat) = + (a - (2 : Rat) * (z2 : Rat)) / (2 : Rat) + rw [hfloor] + 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. -/ +theorem den_normalize_dvd (num : Int) (den : Nat) (h : den ≠ 0) : + (Rat.normalize num den h).den ∣ den := by + rcases Rat.normalize_num_den' num den h with ⟨d, _, _, hden⟩ + exact ⟨d, hden⟩ + +/-- The product of a natural-number rational and an integer rational is integral, + hence has denominator one. -/ +theorem den_mul_nat_int_cast_eq_one (n : Nat) (z : Int) : + ((n : Rat) * (z : Rat)).den = 1 := by + have hdiv : ((n : Rat) * (z : Rat)).den ∣ 1 := by + rw [Rat.mul_def] + have hraw : + (Rat.normalize ((n : Rat).num * (z : Rat).num) + ((n : Rat).den * (z : Rat).den) + (Nat.mul_ne_zero (n : Rat).den_nz (z : Rat).den_nz)).den ∣ + (n : Rat).den * (z : Rat).den := + den_normalize_dvd _ _ _ + simpa only [Rat.ofNat_den, Rat.intCast_den, Nat.mul_one] using hraw + exact Nat.eq_one_of_dvd_one hdiv + /-- amod never enlarges a denominator. LEAF: Rat arithmetic. -/ -theorem den_amod_dvd (a : Rat) (n : Nat) (hn : 0 < n) : +theorem den_amod_dvd (a : Rat) (n : Nat) (_hn : 0 < n) : (amod a n).den ∣ a.den := by - sorry + unfold amod + let z : Int := (a / (n : Rat)).floor + have hmul : ((n : Rat) * (z : Rat)).den = 1 := + den_mul_nat_int_cast_eq_one n z + rw [Rat.sub_def] + have hnorm : + (Rat.normalize + (a.num * ((n : Rat) * (z : Rat)).den - + ((n : Rat) * (z : Rat)).num * a.den) + (a.den * ((n : Rat) * (z : Rat)).den) + (Nat.mul_ne_zero a.den_nz ((n : Rat) * (z : Rat)).den_nz)).den ∣ + a.den * ((n : Rat) * (z : Rat)).den := + den_normalize_dvd _ _ _ + have hprod : a.den * ((n : Rat) * (z : Rat)).den ∣ a.den := by + rw [hmul, Nat.mul_one] + exact Nat.dvd_trans hnorm hprod + +/-- The denominator emitted by `Rat.maybeNormalize` divides its input + denominator whenever the normalizing gcd divides that denominator. -/ +theorem den_maybeNormalize_dvd_of_dvd (num : Int) (den g : Nat) + (den_nz : den / g ≠ 0) (reduced : (num.div g).natAbs.Coprime (den / g)) + (hg : g ∣ den) : + (Rat.maybeNormalize num den g den_nz reduced).den ∣ den := by + unfold Rat.maybeNormalize + by_cases h : g = 1 + · simp [h] + · simp [h] + exact ⟨g, (Nat.div_mul_cancel hg).symm⟩ /-- The denominator of a sum divides the lcm of the denominators. LEAF: Rat arithmetic. -/ theorem den_add_dvd_lcm (a b : Rat) : (a + b).den ∣ Nat.lcm a.den b.den := by - sorry + change (Rat.add a b).den ∣ Nat.lcm a.den b.den + unfold Rat.add + dsimp only + by_cases hg : Nat.gcd a.den b.den = 1 + · simp [hg, Nat.lcm] + · simp [hg] + let g := Nat.gcd a.den b.den + let den := (a.den / g) * b.den + let num := a.num * ↑(b.den / g) + b.num * ↑(a.den / g) + let g1 := num.natAbs.gcd g + have hden_dvd_lcm : den ∣ Nat.lcm a.den b.den := by + have hden_eq : den = Nat.lcm a.den b.den := by + simp [den, g, Nat.lcm] + rw [Nat.mul_comm (a.den / Nat.gcd a.den b.den) b.den, + ← Nat.mul_div_assoc b.den (Nat.gcd_dvd_left a.den b.den), + Nat.mul_comm b.den a.den] + rw [hden_eq] + have hg1den : g1 ∣ den := by + have e : g1 = num.natAbs.gcd den := Rat.add.aux a b rfl rfl rfl + rw [e] + exact Nat.gcd_dvd_right _ _ + have hnormden : den / g1 ∣ den := ⟨g1, (Nat.div_mul_cancel hg1den).symm⟩ + exact Nat.dvd_trans hnormden hden_dvd_lcm /-- Host-normalized objects keep their angle list pointwise inside the product's angle list (the j = 0 slice for A). - LEAF: list membership through bind/map + amod4 fixpoint under - range normalization. -/ + + Repaired domain: use `Complete` operands so the empty-factor counterexample is + excluded and host-normalization is supplied by `hostNormalized_of_complete`. + + Candidate discharge: list membership through bind/map + amod4 fixpoint + under range normalization. Acceptance requires the pinned Lake build. -/ theorem slice_embedding_left (A B : UCNSObject) (d : Nat) - (hA : HostNormalized A) (hB : HostNormalized B) : + (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 List.mem_of_mem_head? 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). LEAF. -/ +/-- 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`. + Candidate discharge; acceptance requires the pinned Lake build. -/ theorem slice_embedding_right (A B : UCNSObject) (d : Nat) - (hA : HostNormalized A) (hB : HostNormalized B) : + (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 List.mem_of_mem_head? 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) -/ theorem carrier_lcm_law_lower_left (A B : UCNSObject) (d : Nat) - (hA : HostNormalized A) (hB : HostNormalized B) : + (hA : Complete A) (hB : Complete B) : nMin A ∣ nMin (multiplyFuel (d + 1) A B) := by unfold nMin exact nMin_dvd_of_denoms_subset _ _ (slice_embedding_left A B d hA hB) theorem carrier_lcm_law_lower_right (A B : UCNSObject) (d : Nat) - (hA : HostNormalized A) (hB : HostNormalized B) : + (hA : Complete A) (hB : Complete B) : nMin B ∣ nMin (multiplyFuel (d + 1) A B) := by unfold nMin exact nMin_dvd_of_denoms_subset _ _ (slice_embedding_right A B d hA hB) @@ -144,7 +367,7 @@ theorem carrier_lcm_law_lower_right threaded through the bind/map structure. -/ theorem carrier_lcm_law_upper (A B : UCNSObject) (d : Nat) - (hA : HostNormalized A) (hB : HostNormalized B) : + (hA : Complete A) (hB : Complete B) : nMin (multiplyFuel (d + 1) A B) ∣ Nat.lcm (nMin A) (nMin B) := by sorry @@ -152,7 +375,7 @@ theorem carrier_lcm_law_upper is machine-checked; status is inherited from the leaves above. -/ theorem carrier_lcm_law' (A B : UCNSObject) (d : Nat) - (hA : HostNormalized A) (hB : HostNormalized B) : + (hA : Complete A) (hB : Complete B) : nMin (multiplyFuel (d + 1) A B) = Nat.lcm (nMin A) (nMin B) := by apply Nat.dvd_antisymm · exact carrier_lcm_law_upper A B d hA hB diff --git a/formal/Ucns/Core.lean b/formal/Ucns/Core.lean index efaa2cce..a80550c2 100644 --- a/formal/Ucns/Core.lean +++ b/formal/Ucns/Core.lean @@ -160,7 +160,7 @@ def HostNormalized (x : UCNSObject) : Prop := NOTE: not machine-checked in the authoring environment (no Lean toolchain); compile + the proof discharge remain Step-2 work. `sorry` ⇒ no DEFENDED status. -/ -/-- Recursive nonemptiness: no empty cell-list at any level +/- Recursive nonemptiness: no empty cell-list at any level (rules out the empty-left-operand and empty-atom counterexamples). -/ mutual def NonemptyRec : UCNSObject → Prop @@ -173,7 +173,7 @@ mutual | ⟨_, _, some p⟩ => NonemptyRec p end -/-- Recursive host-normalization: head angle 0 for the object AND every payload +/- Recursive host-normalization: head angle 0 for the object AND every payload (the head-only `HostNormalized` above is too weak — payload β0 collapses). -/ mutual def HostNormalizedRec : UCNSObject → Prop @@ -186,7 +186,7 @@ mutual | ⟨_, _, some p⟩ => HostNormalizedRec p end -/-- Canonical carrier: `nDec = nMin cells` at every level +/- Canonical carrier: `nDec = nMin cells` at every level (`Nat.lcm` is not left-cancellative, so a free `nDec` breaks it). -/ mutual def CanonicalCarrier : UCNSObject → Prop @@ -199,7 +199,7 @@ mutual | ⟨_, _, some p⟩ => CanonicalCarrier p end -/-- Per-object uniform depth: all cells share one `depthCell`, recursively +/- Per-object uniform depth: all cells share one `depthCell`, recursively (a complete tree with no early atom). -/ mutual def UniformDepth : UCNSObject → Prop diff --git a/formal/lake-manifest.json b/formal/lake-manifest.json index 9ec4fa5b..48e104ca 100644 --- a/formal/lake-manifest.json +++ b/formal/lake-manifest.json @@ -9,6 +9,60 @@ "manifestFile": "lake-manifest.json", "inputRev": "v4.7.0", "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "rev": "64365c656d5e1bffa127d2a1795f471529ee0178", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.30", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/import-graph.git", + "type": "git", + "subDir": null, + "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "rev": "a45ae63747140c1b2cbad9d46f518015c047047a", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.7.0", + "inherited": false, "configFile": "lakefile.lean"}], "name": "Ucns", "lakeDir": ".lake"} From aaf58c7f9adce04130d20974fb1ee9aa649d732e Mon Sep 17 00:00:00 2001 From: Erin Spencer Date: Wed, 1 Jul 2026 16:58:35 -0700 Subject: [PATCH 2/3] verify Carrier-LCM slice embeddings on pinned Lean --- formal/Ucns/CarrierLcm.lean | 28 ++++++++++++++++++++-------- 1 file changed, 20 insertions(+), 8 deletions(-) diff --git a/formal/Ucns/CarrierLcm.lean b/formal/Ucns/CarrierLcm.lean index 3f8129fe..0534e26b 100644 --- a/formal/Ucns/CarrierLcm.lean +++ b/formal/Ucns/CarrierLcm.lean @@ -14,8 +14,7 @@ lemmas) are targeted SORRY-FREE. - The Rat denominator leaves (`den_add_dvd_lcm`, `den_amod_dvd`) are discharged against the installed `Std` Rat API. - - The slice-embedding proofs are structurally proposed in this file, but - require the pinned Lean/Lake build before being cited as discharged. + - 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). -/ @@ -38,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 @@ -129,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 @@ -271,8 +283,8 @@ 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`. - Candidate discharge: list membership through bind/map + amod4 fixpoint - under range normalization. Acceptance requires the pinned Lake build. -/ + 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) : @@ -282,7 +294,7 @@ theorem slice_embedding_left 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 List.mem_of_mem_head? hcb_head + 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 ⟨ @@ -310,7 +322,7 @@ theorem slice_embedding_left Repaired domain: use `Complete` operands so the empty-factor counterexample is excluded and host-normalization is supplied by `hostNormalized_of_complete`. - Candidate discharge; acceptance requires the pinned Lake build. -/ + Discharged by the symmetric list-membership witness construction. -/ theorem slice_embedding_right (A B : UCNSObject) (d : Nat) (hA : Complete A) (hB : Complete B) : @@ -321,7 +333,7 @@ theorem slice_embedding_right 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 List.mem_of_mem_head? hca_head + 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 ?_ From e1cc6e4bc4d70b06a052aa3fcacf6f7718165e23 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 2 Jul 2026 01:16:34 +0000 Subject: [PATCH 3/3] fix(docs): refresh generated CLAUDE manifest workflows list --- CLAUDE.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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.