受限覆盖同余系的极小构造：最小模 ≥ 3/4 时的最小同余式数与 LCM 下界

来源说明：本则出自独立撰写的第二批方案。它与前 20 则同样遵循八块结构与硬门槛要求，但撰写时未做英文文献检索，新颖性边界依据的是历届获奖图谱与既有知识，而非当轮查新。因此其「需核实」条目更多，启动前须自行补一轮英文检索。

1 · 研究问题

最小模为 3（以及 4）的覆盖同余系（covering system，有限组同余式覆盖全体整数）中，同余式条数的最小值与模的最小公倍数（LCM）的最小值各是多少？在"模两两不同且均属于给定区间 [m, Cm]"的限制下，覆盖系统存在的最小 C 是多少（小 m 情形的精确判定）？

2 · 研究背景与空白

覆盖同余系由 Erdős 于 1950 年引入（用于构造无穷算术级数中无 2 的幂加素数表示的奇数），是初等数论中问题极易陈述、结构极深的领域。两个著名问题划定了地形：最小模问题（Erdős 猜测最小模可任意大）被 Hough（2015）否定性解决——最小模有绝对上界；后续工作把上界大幅压低（需核实当前最好数值与作者：搜索关键词 covering system minimum modulus bound 616000 Balister）。奇覆盖问题（全部模为奇数且互不相同）至今开放，本题不进入。

已有工作：最小模 = 2 的极小构造是教材内容；最小模 = 3、4 的极小构造在早期文献（学位论文与期刊，需核实：搜索关键词 Krukenberg covering systems minimum modulus 3 thesis）中有结果，但"条数最小值 / LCM 最小值"的精确表与机器可复核证明未见系统整理；区间限制模的存在性有密度类判据（模的倒数和 ≥ 1 是必要条件）可作下界工具。

空白在：小参数受限覆盖系统的精确极值(条数、LCM、区间常数)缺一份"穷举证明 + 显式构造"的完备记录，而这恰好能用 SAT/分支定界在笔记本上闭合：不存在性由搜索树穷尽证明（可输出证书），存在性由显式构造证明——两个方向都严格。列 ★★ 因为搜索空间控制需要技巧，失败模式是"范围缩水"而非"无结论"。

3 · 可检验假设

• H1：最小模 = 3 的覆盖系统最少需要 N₃ 条同余式（N₃ 预期在 10–20 之间，精确值由穷尽搜索确定），且极小系统的模集合唯一或可完全列出。
• H2：区间限制 [m, Cm] 下，倒数和必要条件给出的下界 C ≥ C₀(m) 与穷举给出的真实最小 C 之间的差距随 m 增大而增大（定量表,m ≤ 8）。

4 · 量化验收标准

1. 方法学校验（硬门槛）：求解器先复现两项已知事实——(a) 验证 Erdős 经典 6 条覆盖系统 {0(2), 0(3), 1(4), 5(6), 7(12)} 及教材最小模 2 极小性结果;(b) 复现文献中最小模 3 的一个已发表构造的合法性（逐残类机器检查）。不过关则全线无效。
2. 极值交付：最小模 3 的最小条数 N₃ 与最小 LCM，附：上界=显式构造（机器验证覆盖完备），下界=穷尽搜索证书（搜索树日志 + 剪枝正确性论证）。最小模 4 为目标线。
3. 区间限制交付：m ≤ 8 的最小 C 精确表 + 密度下界对照。
4. 搜索可信度：主结果用两套独立实现（SAT 编码 / 自写分支定界）复算一致；任一主结果单机重跑 ≤ 7 天。
5. 代码、构造与证书开源，一键复跑。

5 · 数据与工具

用途	来源 / 工具
SAT 编码	PySAT + Kissat（覆盖性 = 每个 mod LCM 残类至少被一条同余式命中）
分支定界	自写：按模从小到大枚举，剩余密度剪枝（∑1/mᵢ 不足即剪）
已有构造对照	覆盖系统综述/原始文献（第 4 周核实清单；仅校验，不计入贡献）
验证器	独立 Python 脚本逐残类检查（LCM ≤ 10⁷ 直接扫描）
算力量级	候选模集合的组合空间随 LCM 增长；通过密度剪枝与模集合规范化控制，预计单实例小时–数天，纯 CPU

6 · 方法路径

1. 写覆盖验证器与 SAT 编码，完成第 4 块第 1 条复现。
2. 文献窗口：核实最小模 3/4 已发表的极值与构造（能力边界核实步），确定本题从"复核"起步还是"填空"起步。
3. 实现分支定界（模集合枚举 + 密度剪枝 + 对称规范化），在最小模 2 上校准完备性。
4. 穷尽搜索最小模 3 的条数/LCM 极值，输出构造与搜索证书。
5. 推进最小模 4 与区间限制表（m ≤ 8）。
6. 独立交叉校验：SAT 与分支定界互证；全部构造过独立验证器。

7 · 新颖性边界

• 本课题不声称触碰奇覆盖问题或最小模的一般上界（Hough 及后续，远超本题工具），已发表的极小构造不计入贡献。
• 已有工作：Hough 2015 最小模有界定理及后续改进（数值第 4 周核实）；最小模 3 的早期构造与可能已有的极值结果（第 4 周核实，若条数极值已发表则本题转为 LCM 极值与区间限制表，框架不变）。丘奖相邻获奖论文：数论方向多篇（筛法、素数定理）但无覆盖系统题材——本题差异即题材本身，且交付形态是"机器证书化的精确极值"。
• 本项目贡献（主结论）：小参数受限覆盖系统的精确极值表 + 显式构造 + 穷尽性证书。
• 价值：把一个经典领域的"民间已知"整理成可复核的严格记录；区间限制表为密度判据的紧性提供第一份系统数据。两方向（存在构造/不存在证明）都是有效结论。

8 · 决策门槛（go / no-go）

• 第 4 周末：文献核实完成，确定空缺清单。若最小模 3 极值全部已发表 → 主战场移到最小模 4 与区间限制表，管线不变。
• 第 8 周末：硬门槛通过 + 分支定界在最小模 2 上确认完备（能重现已知极小构造并证明其极小性）。未过 → 修剪枝逻辑，这是正确性问题必须清零。
• 第 18 周末：最小模 3 穷尽搜索若超算力（单实例 > 7 天）,降级路径 A：加"LCM ≤ B"约束逐步放宽，交付"分层极值表"（每个 B 下的精确极值，严格且可复核）;降级路径 B：主结论改为区间限制表（m ≤ 8 精确判定）+ 最小模 3 的新上界构造。两条都保留"精确极值 + 证书"框架。
• 预算裁剪顺序：最小模 4 线 → 区间限制 m 上限；最小模 3 主线与证书交付不砍。

---