From ae55a786272aa028e40c0c1559488353b3b043d1 Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Sat, 4 Jul 2026 10:28:25 -0500
Subject: [PATCH] =?UTF-8?q?docs:=20CRTSidonN=20auto-generated,=20~15=20str?=
 =?UTF-8?q?uctural=20issues=20=E2=80=94=20documenting=20TODO?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The pipeline-math template (5-file frozen pattern, linear_combination tactics,
decide for residue checks, lcoeff-descent for quotient witnesses) is now
documented in docs/frozen_template/. The auto-generated CRTSidonN.lean
needs manual porting to mathlib v4.30.0-rc2 API.

Adopted refinements:
- verify_lean.py: 5-check pipeline (SHA pins, banned keywords, build, axioms, discharge)
- prove.py: 5-check pipeline for LLM proof filling
- docs/frozen_template/: reusable Defs/Theorems/Proofs/Discharge/Solution pattern
---
 lakefile.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lakefile.lean b/lakefile.lean
index 023b9b44..9074ff1a 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -47,7 +47,7 @@ lean_lib «SilverSightFormal» where
     `CoreFormalism.HopfFibration,
     `CoreFormalism.StrandCapacityBound,
     `CoreFormalism.CRTSidon,
-    -- `CoreFormalism.CRTSidonN,  -- TODO(lean-port): auto-generated, targets different mathlib API
+    -- `CoreFormalism.CRTSidonN,  -- TODO(lean-port): auto-generated, ~15 structural issues
     `SilverSight.AngrySphinx,
     `SilverSight.CollatzBraid,
     `SilverSight.GoldenSpiral,