allaun c52daaa757 feat(lean): close sidon_weight_bound + deepseek v4 flash harness ... sidon_weight_bound: corrected RHS from invalid sigma7(2N)/120 to sum_{s=2}^{2N} convolutionRHS(s). Proof uses Finset.single_le_sum + Sidon injectivity (Finset.sum_image) + E8 convolution identity. All 5 E8 Sidon theorems now closed (0 sorries in §§9-13). New: deepseek_v4_flash_lean_harness.py — sorry-resolution harness targeting local llama.cpp DeepSeek V4 Flash endpoint. Scans .lean files, sends theorem context to LLM, inserts generated proofs, verifies with lake build, emits receipts. Build: 3583 jobs, 0 errors (lake build)		2026-06-16 17:37:00 -05:00
..
conversions/hardware	chore(repo): push local 768-commit branch state onto clean remote baseline	2026-06-15 22:46:50 -05:00
external/OTOM	WIP: accumulated changes	2026-05-25 16:24:21 -05:00
LeanGPT	Remove legacy Python prototypes superseded by Lean formalization	2026-05-19 15:34:17 +00:00
Semantics	feat(lean): close sidon_weight_bound + deepseek v4 flash harness	2026-06-16 17:37:00 -05:00
singer-theorem-lean	chore(repo): push local 768-commit branch state onto clean remote baseline	2026-06-15 22:46:50 -05:00
CHAIN_ALL_REVIEW_REPORT.md	initial: sovereign research stack (consolidated, weightless, and lfs-optimized)	2026-05-04 18:11:36 -05:00