v0.3.4 — nominal-reasoning lever + corpus expansion (wine, bibtex)

Highlights

Corpus expansion + a new saturator capability for nominal reasoning (#17).

Nominal-reasoning lever (saturator)

The EL fold now handles nominal-filler existentials (∃R.{a} / ObjectHasValue) via an opaque per-individual synthetic class (NomKey) at the lowering chokepoint, plus transitive-ABox propagation: X ⊑ ∃R.{a}, a R⁺ b (R transitive) ⟹ X ⊑ ∃R.{b}.

• Saturator-private (no tableau impact). Sound by 1:1 individual identity + transitivity gating; inverse×nominal soundness is a verified code invariant.
• wine MISSED 57 → 34 (region/colour cluster recovered), FP=0 across all 10 corpus fixtures; the 9 core parity fixtures stay MISSED=0.
• Canary nominal_transitive_abox_fold_classifies.

Corpus fixtures

• wine — W3C OWL-guide SHOIN(D), nominal/disjointness-heavy (207 value restrictions); the corpus's nominal/value-restriction stressor.
• bibtex — ORE-2015 datatype-heavy (41 DataMinCardinality + 40 DataPropertyDomain); FP=0, MISSED=0, validating Phase-D's sound under-approximation on real data.

Scoping (turning gaps into measured frontiers)

• docs/nominal-lever-scoping-2026-06-06.md — the lever + why the residual 34 (grape ≤1, sugar ∀) are tableau-grade.
• docs/corpus-datatype-2026-06-06.md — real datatypes don't drive non-redundant classification; synthetic suite remains the D4/D5 completeness test.
• docs/tableau-perf-scoping-2026-06-06.md — wine's residual is disjunction-branching interdependence (measured: 90/137 classes stall, restores=branches with precise deps). Every cheaper lever (relevance, blocking, dep-precision, completeness) is measured-out; conflict-driven nogood learning is the only remaining lever (multi-week, soundness-critical) — a deliberate future project.

Status

The 9 core corpus fixtures remain at full Konclude parity (FP=0, MISSED=0). wine sits at FP=0, MISSED=34 (sound; the residual is the documented hard-SROIQ-disjunction frontier). bibtex at full parity.

Full changelog: v0.3.3...v0.3.4