From 554bc6b194f11aec08d6862b93b2355c677c1438 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 23 Oct 2026 15:15:11 -0400 Subject: [PATCH] refactor(circuit): simplify kernel-step synthesis bookkeeping Use Synthesis.Builder to retain wires and accumulate the same seven named arithmetic stages. Preserve the exact public statement, budget lemma, 8*(n+1)^2 bound, semantic rewrite and source credit. All six project gates and 89 Python tests pass on exact tree f1888b03, plus hygiene, docs configuration, catalogue, proof-length scan and whitespace. Whole-file MCP diagnostics are clean with CSLib6ff325e8. Proof-only change; selected abstracts unaffected. Stacked on #533; no authorship claimed for its inherited pin delta. AI-assisted implementation by worker-codex-kernel-synthesis-20261023. Independent coordinator review requested. Closes #523. --- .../Computability/Circuit/KernelVector.lean | 73 +++++++++---------- 1 file changed, 33 insertions(+), 40 deletions(-) diff --git a/Complexity/Computability/Circuit/KernelVector.lean b/Complexity/Computability/Circuit/KernelVector.lean index bcd3596ea..a64951435 100644 --- a/Complexity/Computability/Circuit/KernelVector.lean +++ b/Complexity/Computability/Circuit/KernelVector.lean @@ -9,6 +9,7 @@ module public import Complexity.Computability.Circuit.FullArithmetic public import Complexity.Foundations.LinearAlgebra.KernelVector +import Complexity.Tactic.Synthesis import Mathlib.Tactic.Linarith import Mathlib.Tactic.Ring @@ -168,64 +169,56 @@ theorem full_kernelStep (a : Fin n → (Fin N → F) → F) (Nv : Fin n → Fin (Set.range fun il : Fin n × Fin n => fun x => kernelStep (fun l => a l x) (fun i l => Nv i l x) il.1 il.2) (8 * (n + 1) ^ 2) := by + let build := Builder.start (fullInterpretation (k := 2)) s -- the row values let b : Fin n → (Fin N → F) → F := fun i x => ∑ l, a l x * Nv i l x - have h₁ := family (I := fullInterpretation (k := 2)) (s := s) b (fun _ => 2 * n + 1) - (fun i => by - simpa [card_univ] using full_dot (s := s) univ a (Nv i) (fun l _ => ha l) - (fun l _ => hN i l)) - set s₁ := s ∪ Set.range b - have hb : ∀ i, b i ∈ s₁ := fun i => Set.mem_union_right _ ⟨i, rfl⟩ + let build := build.add (family (I := fullInterpretation (k := 2)) (s := build.wires) + b (fun _ => 2 * n + 1) (fun i => by + simpa only [card_univ, Fintype.card_fin] using + full_dot (s := build.wires) univ a (Nv i) + (by synthesis_available) (by synthesis_available))) -- the pivot flags let sel : Fin n → (Fin N → F) → F := fun i x => firstFlags (fun j => b j x) i - have h₂ := full_firstFlags (s := s₁) b hb - set s₂ := s₁ ∪ Set.range sel - have hsel : ∀ i, sel i ∈ s₂ := fun i => Set.mem_union_right _ ⟨i, rfl⟩ - have hb₂ : ∀ i, b i ∈ s₂ := fun i => Set.mem_union_left _ (hb i) - have hN₂ : ∀ i l, Nv i l ∈ s₂ := fun i l => - Set.mem_union_left _ (Set.mem_union_left _ (hN i l)) - have ha₂ : ∀ l, a l ∈ s₂ := fun l => Set.mem_union_left _ (Set.mem_union_left _ (ha l)) + synthesis_step build using full_firstFlags b -- the pivot vector let P : Fin n → (Fin N → F) → F := fun l x => ∑ j, sel j x * Nv j l x - have h₃ := family (I := fullInterpretation (k := 2)) (s := s₂) P (fun _ => 2 * n + 1) - (fun l => by - simpa [card_univ] using full_dot (s := s₂) univ sel (fun j => Nv j l) - (fun j _ => hsel j) (fun j _ => hN₂ j l)) - set s₃ := s₂ ∪ Set.range P - have hP : ∀ l, P l ∈ s₃ := fun l => Set.mem_union_right _ ⟨l, rfl⟩ + let build := build.add (family (I := fullInterpretation (k := 2)) (s := build.wires) + P (fun _ => 2 * n + 1) (fun l => by + simpa only [card_univ, Fintype.card_fin] using + full_dot (s := build.wires) univ sel (fun j => Nv j l) + (by synthesis_available) (by synthesis_available))) -- the pivot value let β : (Fin N → F) → F := fun x => ∑ l, a l x * P l x - have h₄ : Synthesis (fullInterpretation (k := 2)) s₃ {β} (2 * n + 1) := by - simpa [card_univ] using full_dot (s := s₃) univ a P - (fun l _ => Set.mem_union_left _ (ha₂ l)) (fun l _ => hP l) - set s₄ := s₃ ∪ {β} + have hβ : Synthesis (fullInterpretation (k := 2)) build.wires {β} (2 * n + 1) := by + simpa only [card_univ, Fintype.card_fin] using + full_dot (s := build.wires) univ a P + (by synthesis_available) (by synthesis_available) + let build := build.add hβ -- the ratios let ρ : Fin n → (Fin N → F) → F := fun i x => b i x / β x - have h₅ := family (I := fullInterpretation (k := 2)) (s := s₄) ρ (fun _ => 1) - (fun i => full_binary_mem (· / ·) - (Set.mem_union_left _ (Set.mem_union_left _ (hb₂ i))) (Set.mem_union_right _ rfl)) - set s₅ := s₄ ∪ Set.range ρ + let build := build.add (family (I := fullInterpretation (k := 2)) (s := build.wires) + ρ (fun _ => 1) (fun i => full_binary_mem (· / ·) + (by synthesis_available) (by synthesis_available))) -- the corrections let t : Fin n × Fin n → (Fin N → F) → F := fun il x => ρ il.1 x * P il.2 x - have h₆ := family (I := fullInterpretation (k := 2)) (s := s₅) t (fun _ => 1) - (fun il => full_binary_mem (· * ·) (Set.mem_union_right _ ⟨il.1, rfl⟩) - (Set.mem_union_left _ (Set.mem_union_left _ (hP il.2)))) - set s₆ := s₅ ∪ Set.range t + let build := build.add (family (I := fullInterpretation (k := 2)) (s := build.wires) + t (fun _ => 1) (fun il => full_binary_mem (· * ·) + (by synthesis_available) (by synthesis_available))) -- the new family let N' : Fin n × Fin n → (Fin N → F) → F := fun il x => Nv il.1 il.2 x - t il x - have h₇ := family (I := fullInterpretation (k := 2)) (s := s₆) N' (fun _ => 1) - (fun il => full_binary_mem (· - ·) - (Set.mem_union_left _ (Set.mem_union_left _ (Set.mem_union_left _ - (Set.mem_union_left _ (hN₂ il.1 il.2))))) - (Set.mem_union_right _ ⟨il, rfl⟩)) - have htotal := h₁.trans (h₂.trans (h₃.trans (h₄.trans (h₅.trans (h₆.trans h₇))))) - refine htotal.mono Set.Subset.rfl ?_ ?_ + let build := build.add (family (I := fullInterpretation (k := 2)) (s := build.wires) + N' (fun _ => 1) (fun il => full_binary_mem (· - ·) + (by synthesis_available) (by synthesis_available))) + refine build.finish ?_ ?_ · rintro _ ⟨⟨i, l⟩, rfl⟩ - refine ⟨(i, l), funext fun x => ?_⟩ + have hmem : N' (i, l) ∈ build.wires := by synthesis_available + convert hmem using 1 + funext x simp only [N', t, ρ, β, P, sel, b, kernelStep, rowValues, pivotVec, dotProduct, Pi.sub_apply, Pi.smul_apply, smul_eq_mul, Finset.sum_apply] rfl - · simp only [sum_const, card_univ, Fintype.card_fin, Fintype.card_prod, smul_eq_mul, mul_one] + · dsimp +zetaDelta [Builder.add, Builder.start] + simp only [sum_const, card_univ, Fintype.card_fin, Fintype.card_prod, smul_eq_mul, mul_one] have := kernelStep_budget n linarith