这是覆盖系统的交互式 Visualization 项目。首页现在并列提供两个实验空间：
树形覆盖的输入由 01_主线/形式化验证/code/covering.hpp 编译成的 WebAssembly 直接解析。网页不再维护一套独立的正式语法；cpp/parser_bridge.cpp 只负责把 C++ AST 无损地转换成页面使用的 JSON，不修改验证器。0 与 1 分别画成白色与黑色圆叶子，普通树节点只保留分叉线，递归树的最后一支以加粗箭头收尾。
在本目录运行：
node server.js然后访问 http://127.0.0.1:4173/tree.html。树形覆盖与矩形覆盖运行时都调用这个 WebAssembly 解析器；包括 5^\uparrow(...)、Unicode 5↑(...)、p_w↑A 与 p↑_wA 在内的输入都走同一个 C++ Parser。修改 covering.hpp 后运行 cpp/build-wasm.ps1 重建浏览器模块。
tree/syntax-contract.json 是网页解析器与 covering.hpp 的共享样例契约。运行 node tree/parser.test.js 检查网页语义；运行 node tree/parser.sync.test.js 会临时编译一个很薄的 C++ 探针，并把两套解析器对同一批输入的接受行为与公共归一形逐项比较。以后修改符号时，先改这份契约，任一实现未同步都会直接报错。
覆盖系统是由 P. Erdos [1] 的1950年论文中首次引入的。覆盖系统是一个模数大于
虽然现在已知覆盖系统的最小模数不能任意大，但最小模数可以有多大仍是一个问题。迄今为止最好的结果是 Tyler Owens [3]，构造了一个模数
- 简记剩余类
$a\pmod n$ 或$a+n\mathbb{Z}$ 为$n_a$ ，
特别的$1=\mathbb{Z}$ ，$0=\varnothing$。 - 再简记集合运算
$A\cup B=A+B$ ，$A\cap B=AB$。
由于中国剩余定理，我们可以分解剩余类为若干素数幂的剩余类：
$$
\begin{aligned}
n&=\prod_{i=1}^kp_i^{n_i}\
\to n_a&=\prod_{i=1}^k(p_i^{n_i}){a}=\prod{i=1}^k(p_i^{n_i})_{a\bmod p_i^{n_i}}
\end{aligned}
$$
例如
这里
注意到
更一般的，我们定义同质数的幂的乘积不是交集，而是：
$$
\begin{aligned}
(p^{n_1}){a_1}(p^{n_2}){a_2}&=(p^{n_1+n_2}){a_1+a_2}=p^{n_1+n_2}{a_1+a_2}\
\to p_{a_1}p_{a_2}\dots p_{a_n}&=p^n_{a_1+a_2p+\dots+a_np^{n-1}}
\end{aligned}
$$
以此类推，我们可以得到：
这个符号是 Nielsen [4] 符号的一种变体，目的是更紧凑地表示覆盖系统。
对于
于是我们还可以形式化的做验证，例如最小模数等于
我们可以不断分配+合并来验证这是一个覆盖： $$ \begin{aligned} &2(1,2_0)+3(1,2_1,4_3)\ =&3(1+2(1,2_0),2_1+2(1,2_0),2_12_1+2(1,2_0))\ =&3(1,2(1,1+2_0),2(1,2(1,1)))\ =&3(1,2(1,1),2(1,1))\ =&3(1,1,1)=1\ \end{aligned} $$
然后再利用分配率+中国剩余定理可以得到具体的剩余类： $$ \begin{aligned} &2(1,2_0)+3(1,2_1,4_3)\ =&2_0+2_12_0+3_0+3_12_1+3_24_3\ =&2_0+4_1+3_0+6_1+12_{11} \end{aligned} $$
然而大部分情况下我们都没必要合并为具体的剩余类，
只需要检验是否有相同的模数即可。
按照这个形式化方法，读者可以自行验证最小模数等于
最小模数等于
对于一个中缀表达式的森林：
[1] P. Erdos. On integers of the form 2^k + p and some related problems. Summa Brasil. Math., 2:113123, 1950.
[2] Bob Hough. Solution of the minimum modulus problem for covering systems. Ann. of Math. (2), 181(1):361382, 2015.
[3] Owens, Tyler E.. “A Covering System with Minimum Modulus 42.” (2014).
[4] Pace P. Nielsen. A covering system whose smallest modulus is 40. J. Number Theory, 129(3):640666, 2009