九级说明
- 基设级 1
- 承重的出发点。与定理不在同一确证轴上:地基与楼层不比高低,只分承重与被承。不得有逻辑前提;以基设依赖集向下游标注。
- 定理级 14
- 有证明的数学或逻辑结论:须附证明链接(Lean、Coq、论文、附录、教科书)或立于既有数学的外部锚点。
- 实测级 1
- 经测量得到的结论:应附数据链接与独立方法的交叉核对。
- 结构推论 3
- 由结构论证得出、尚未形式化为定理的推论。
- 阐释级 2
- 在本框架内的解释性读法;不是定理,不作计算基础。
- 词典级 2
- 与其他学科术语的词典级对照;只表示可互相翻译,不表示结构同一。
- 工程级 2
- 工具、软件或模型。不在级联标尺上,不得作逻辑前提;可作 instrument(工具)边。
- 纲领级 2
- 研究纲领或写作中的目标,尚未完成论证;不进入首页精选。
- 须拒斥 3
- 经审视应当拒斥的说法,公开列出并说明理由。不得作非拒斥命题的逻辑前提。
级联规则
- 结论之级 = min(前提之级,推理之严格度)。只有 logical 边参与级联;instrument、context、refutes 边不参与。
- 标尺:基设 6、定理 6、实测 5、结构推论 4、阐释 3、词典 2、纲领 1;工程级与须拒斥不在标尺上。
- 作者的保守声明向下游传播:前提的有效强度取其声明级别与计算上限中的较小者。
- 逻辑循环不是错误:未守护的循环整个强连通分量封顶为结构推论;全部成员有守护证书时不封顶。
- 级联只检查一致性,不检查真伪;推理严格度由作者自报。

