发现质量筛
把 BEDC 的发现声明放进候选、静态负证、对抗见证与 Lean 元层载体的同一条质量回路.
发现质量筛
是什么
发现质量筛, 即 Discovery Quality Sieve, 是 BEDC 对发现声明的质量回路。它把”这是不是一次有内容的分类器 shift”拆成三件可查的事: 生产侧只把高精度候选送入 worker flow, 过滤侧用静态负证与确定性对抗见证压低空洞声明, 观察侧把分类器 shift、发现账本、机械分类与覆盖情况作为 informational 审计行暴露出来。
这个名字只指 dossier 层的统一视角。代码里的命令名、JSON 字段、Lean namespace 和提示词术语保持原样: discovery-candidates, discovery-sieve, discovery-adversarial, critical_path.discovery_candidate_top, DiscoveryDeltaLedger, DisagreementSupport。
三个联动表面
生产
生产表面由 python3 lean4/scripts/bedc_ci.py discovery-candidates 与 lean4/scripts/critical_path.py 的 discovery_candidate_top 驱动。候选检测器刻意高精度、低召回: 只有当 paper 与 Lean 表面同时暴露已解析 Lean 目标、before/after 分类器 endpoint、可达 disagreement support、非平凡 semantic endpoint, 且没有硬负证标签时, 目标才会被放行。
硬拒绝包括 human-origin baseline 材料、已经闭合的审计状态、已检查的桥状态、机械分类声明, 以及 target_missing, target_axiom, target_sorry, smoke_template_reuse, trivial_classifier, target_substring_evidence 等负证。实时 dispatch_intent 与 allowed_outcomes 由 python3 lean4/scripts/bedc_ci.py discovery-candidates --json 以及 lean4/scripts/critical_path.py 输出的 discovery_candidate_top 行负责; 当这些实时 outcome 允许时, worker 可以尝试给出真实位移账本, 也可以诚实记录 mechanical_reconstruction 或拒绝候选。
critical_path.discovery_candidate_top 把这些候选作为低权重 dispatch 来源接入工作流。这让候选被看见, 但不把”发现产量”变成调度目标。Lean 与 paper worker 提示词里的 Discovery Candidate Contract 同样要求真实分类器位移声明, 并允许诚实的 mechanical_reconstruction 与可审计 opt-out。
生产指标是 survivor-based: declared_candidate, sieve_survivor, certified_prime。它们不奖励原始声明数, 因为声明数本身不能作为发现质量的代理。
过滤
过滤表面由 python3 lean4/scripts/bedc_ci.py discovery-sieve、python3 lean4/scripts/bedc_ci.py discovery-adversarial 与 critical_path 的 sieve_clearance_top / sieve_demote 驱动。
discovery-sieve 对发现目标做多道静态负证筛。它累积 reason_tags, 记录 negative_witnesses, missing_support, clearance_requirements, 并给出四级分级:
| 分级 | 含义 |
|---|---|
certified_prime |
静态筛下没有负证, 且有非平凡分类器 shift、完整行与独立 support |
probable_prime |
静态筛下没有负证, 或有可见语义锚, 但未达到 stronger support |
probable_composite |
有可疑负证, 或证据形态不足 |
confirmed_composite |
有确定负证, 如目标缺失、axiom、sorry、名称子串证据或缺发现行 |
这四个词是筛分隐喻, 不是真值结论。载荷里的 grade_semantics 明确写成 static_sieve_only_not_truth。
discovery-adversarial 在同一目标族上生成确定性对抗见证。静态家族包括 prior-classifier wrapper / 同形重构、constructor 正规形 deepening、cost 账本 reduction 等 lens。
每个 AdversarialWitness 带 target_fingerprint。fingerprint 绑定目标 header/body、support、adversarial input graph、见证 read graph 与 paper closurestatus 内容; 证据图变化时, 旧快照不再代表当前图。adversarial_resistance_score 只用于排序, score_semantics 是 ranking_only_not_probability。
critical_path.sieve_clearance_top 从小缺口的筛分目标里挑可局部补证的项; critical_path.sieve_demote 把静态低质量目标降权, 不是新的发现任务来源。
观察
观察表面把筛分结果接回 bedc_ci.py audit, 但保持 informational 语义。审计暴露:
| 审计行 | 观察内容 |
|---|---|
classifier shift quality |
classifier-shift 目标是否被筛成 probable / confirmed 复合 |
discovery ledger coverage |
ai-origin chapter 是否有对应 DiscoveryDeltaLedger 声明 |
mechanical opt-out audit |
mechanical_reconstruction / confirmed_composite 是否给出 reason、nearest 目标与 worker 检查记录 |
这些行帮助算子判断质量趋势, 但不把审计变成真值裁判。
素数隐喻与诚实边界
发现质量筛使用”素数/合数/伪素数”的 lens 来整理工作流:
| 隐喻 | 在 BEDC 里的读法 |
|---|---|
| 真发现像素数 | 不能被已知 mechanical 路线分解的分类器位移 |
| 机械重构像合数 | 已知数学 NameCert、carrier-only、bridge-only、marker sync、duplicate 等可分解工作 |
| 伪发现像伪素数 | 表面像 discovery, 但被静态负证或对抗见证分解 |
这个 lens 不声明真素性。系统不裁定”真发现”, 不给概率, 不证明一个目标不可分解。它给的是 adversarial-undecomposed degree: 在当前静态读模型、support 图与对抗家族下, 目标还没有被分解到机械解释的程度。这个 degree 是排序信号, 不是真值。
关键设计理据
软激励优先于硬要求。若 worker 必须产出发现, 最容易出现的是伪造分类器 shift、把 constructor disequality 当语义端点, 或用空账本洗白声明。低权重候选、允许 mechanical_reconstruction、允许 reject_candidate, 让系统把诚实分类作为合格结果。
survivor 不是产量。真实分类器 shift 稀疏, 高精度检测器在一段时间里没有放行候选是正常状态。空转待料比把声明数当目标更可靠。
防 gaming 是双向的。筛分与对抗见证挡假阳性: 目标缺失、sorry、axiom、smoke 模板、名称子串证据、平凡分类器、constructor-only disagreement、无 semantic refs、裸 row-count margin 都会被记录为负证。mechanical opt-out 审计挡假阴性: worker 不能把困难目标随手标成 mechanical, 必须给出 accepted reason、nearest existing 目标和检查记录。
fingerprint 让对抗见证有时效边界。target_fingerprint 绑定目标、support、read graph 与 paper closurestatus; 当证据图变化, 旧的 adversarial snapshot 不再是永久判词。
Live 接口
| 表面 | 接口 |
|---|---|
| 生产命令 | python3 lean4/scripts/bedc_ci.py discovery-candidates [--json] [--verbose] [--max-a N] |
| 过滤命令 | python3 lean4/scripts/bedc_ci.py discovery-sieve [--json] [--verbose] |
| 对抗命令 | python3 lean4/scripts/bedc_ci.py discovery-adversarial [--json] [--verbose] |
| 审计 survey | python3 lean4/scripts/bedc_ci.py discovery-audit [--json] [--verbose] |
| 关键路径视图 | discovery_candidate_top, sieve_clearance_top, sieve_demote |
| Lean 元层载体 | BEDC.Meta.DiscoveryDeltaLedger, BEDC.Meta.DisagreementSupport, BEDC.Meta.TheoremDNA |
| 提示词 contract | Lean 与 paper worker 提示词里的 Discovery Candidate Contract |
| informational 审计行 | classifier shift quality, discovery ledger coverage, mechanical opt-out audit |
DiscoveryDeltaLedger 是每章发现账本。它携带 ChapterTasteGate、行会计, 以及 classifier_shift : Option DiscoveryShift。none 表示没有实际前后位移; some shift 才进入结构发现账本路径。
DisagreementSupport 是分歧的独立支持载体。它把分类器源族与可观察族分开。可观察族可来自解码、读回、账本或角色见证, 并要求稳定的语义分离见证与可观察 NameCert。
TheoremDNA 提供定理层内容角色, 包括陈述、依赖、证明、证书、账本、状态、规范位置与闭合封印。每章 DNA 内容哈希用它来约束证据图读法贴合实时定理表面。
当前边界
发现质量筛接入生产、过滤、观察回路。候选检测器刻意高精度低召回; 当没有目标同时满足前后端点、可达支持、语义端点与无硬负证这些条件时, 诚实读法是空载待料, 不是系统失效。
当前系统提供的是静态分级、确定性对抗见证、fingerprint 时效门与排序信号; 它还没有把对抗者本身提升为 Lean-checked 证明对象。