v0.3.2 — notgalen full Konclude parity (Phase 2e)
Highlights
notgalen MISSED 18 → 0 — full Konclude parity. The corpus completeness gap is now just SIO's 2 out-of-EL pairs. FP=0 held across the entire corpus.
Phase 2e — functional super-role witness-merge (#15)
The saturator's witness-merge rule back-propagated the merged synthetic to a subject's other functional-sub-role witnesses but skipped the merge-triggering role, wrongly assuming CR9 covered it (CR9 only lifts the original witness up to the super-role; it never pushes the merged synthetic down to the triggering sub-role). When an existential body lives on that sub-role — notgalen's Anonymous-349 ⊑ ∃hasIntrinsicPathologicalStatus.pathological, where hasIntrinsicPathologicalStatus/hasPathologicalStatus are siblings under the functional StatusAttribute — the merged filler must land there. Which sub-role triggers depends on processing order, so GALEN hit the good order (closed in 2d) while notgalen's equiv-vs-subclass structure hit the bad one, leaving 18 pairs unrecovered through Phases 2a–2d.
Fix: drop the skip. Sound by functionality of R_f (every sub-role witness coincides with the single R_f-successor carrying the full merged atom set). Verified three ways: saturator = rustdl tableau (minimal module) = Konclude (9 corpus ontologies).
Corpus gate (FP=0 throughout)
| Fixture | FP | MISSED |
|---|---|---|
| alehif | 0 | 0 |
| galen | 0 | 0 |
| notgalen | 0 | 18 → 0 |
| ro | 0 | 0 |
| shoiq-knowledge | 0 | 0 |
| ore-10908-sroiq | 0 | 0 |
| sulo | 0 | 0 |
| sio | 0 | 2 (out-of-EL) |
| ore-15672-shoin | 0 | 0 |
Also included
- #14 — sub-tableau-caching lever scoping; corrects the stale "Lever C is dead" roadmap finding (the build-a-model premise is stale for the wedge, but the §2 reuse-soundness trap stands; the sound form already ships as the Phase 1b/1c snapshot cache).
- #13 —
blocks_fired/block_eligibletableau counters + correction of the stale "blocking never fires" roadmap claim.
Full changelog: v0.3.1...v0.3.2