fix(verify): both instrument false-positive mechanisms on the ORE corpus (#87)

[micheldumontier]

Closes #87.

Of the 366 ORE ontologies verify-el can check, 8 reported Violated and all 8
adjudicated to the instrument's own bugs, not engine gaps — so the crate's headline claim
("a Violated is a real engine defect") was, corpus-wide, never once earned. Both mechanisms
are fixed.

F4 — SubClassOf(owl:Thing, C) never reached a Tseitin witness

The saturator emits no fact for a nested existential body and gives its marker an empty
subsumer set by design, so the witness element carried only itself and the checker reported
the very ⊤ ⊑ C axiom that should have closed it. On all four affected ontologies the
violation count equalled the ⊤ ⊑ C axiom count exactly.

The engine was right throughout, and the discriminating pair is what shows it: rustdl subclass X C answers yes, and the same reproducer with the nesting flattened away verifies
clean. It reproduces in ten lines:

SubClassOf(:X ObjectSomeValuesFrom(:r ObjectSomeValuesFrom(:s :A)))   <- nested: Violated
SubClassOf(owl:Thing :C)

FiniteModel::intern now closes a label containing no named class under the ⊤-supers,
collected from both SubClassOf(⊤, …) and EquivalentClasses(⊤, …) and closed through the
reported subsumer closure rather than the axioms — so an engine that failed to derive a
closure step still shows up as a violation instead of being papered over.

F5 — a truncated model reported Violated instead of Unresolved

A BoundTripped means build_model stopped early, so most axioms have no witness left and
the violations are artifacts of the cut: 25369 / 20292 / 54304 / 92573 of them, on the order
of the domain size itself. Now exit 3 (no verdict), not exit 2 (defect found).

Both fixes are deliberately narrow

Closing every label under the ⊤-supers, or downgrading on any build reason, each reads
as the natural generalisation — and each would trade this crate's false-positive problem
for a false-negative one, which is strictly worse for an instrument whose purpose is
finding defects. A named class whose closure lacks a ⊤-super is a genuine D10 gap; a
LabelNotClosed alongside a violation is still a real disagreement against whatever was
checked.

A guard test survived its own sabotage

Worth recording, because it nearly shipped. The scoping canary was first written end-to-end,
removing C from a named class's element via test_only_remove_from_label. That seam runs
after interning, so the check fails under either scoping and the test discriminated
nothing — it passed the "close every label" sabotage it existed to catch. The rule is now
pinned at unit level on intern directly, where it can be observed, and the end-to-end test
was renamed to claim only what it actually checks.

Sabotage: 5 run, 4 caught first pass, 1 survived and was closed.

#	sabotage	result
S1	close every label, not just marker-only	survived, then caught by the unit pin
S2	drop the subsumer-closure step	caught (1 test)
S3	drop the EquivalentClasses arm	caught (1 test)
S4	revert the fix entirely	caught (5 tests)
S5	downgrade on any build reason	caught (negative control)

The sentinel is inverted, not deleted

known_limitations.rs pins F1/F2/F3 as current defective behaviour and its header instructs
that a newly-passing one be updated rather than removed, and be re-checked for whether the
gap is genuinely fixed or merely untriggered by that shape. Answered by measurement: three
further tests cover a 3-deep nesting, the EquivalentClasses(owl:Thing, …) spelling, and a
⊤-super reachable only through the closure. F1 and F3 remain open and still reproduce.

Verification

• the 4 F4 ontologies now report verified; the 4 F5 ones unresolved with exit 3
• suite 1917 passed / 0 failed (CARGO_EXIT=0 — captured directly, not through a pipe)
• cargo clippy --workspace --all-targets --all-features -- -D warnings exit 0
• a two-arm verify-el sweep over all 1,920 ORE ontologies is running; I will post the
  verdict-distribution delta as a comment. The risk it covers is a new false Violated
  from the added labels — the fix only ever adds labels to marker-only elements, so that is
  the direction to check.

🤖 Generated with Claude Code

[micheldumontier]

Closing as a duplicate — #87 was fixed in parallel and merged as 8bbadb7 / 5a9ea3a / 83bff7a while this was in flight.

I compared the two implementations rather than assuming. The merged one is a superset of this one on every point but one:

	merged	this PR
F5 narrow to BoundTripped only	✔ reason_means_model_is_truncated	✔
EquivalentClasses(⊤, …) arm	✔	✔
⊤-supers closed through subsumers_of	✔	✔
⊤ ⊑ ∃r.C — the RULE half	✔	�’✗ missing
label floor scoping	every label	marker-only labels

The ⊤ ⊑ ∃r.C half is a real gap in mine: a label floor cannot build an existential, and I only fixed the label side.

I verified the merged binary independently, on my own harness, on all eight ontologies #87 names — 4 verified/exit 0, 4 unresolved/exit 3.

Two things from this branch are worth keeping, and I am not re-landing either here:

1. A corpus-scale two-arm sweep, which the merged change did not have (its gate was 16 fixtures). Running now against merged main; I will post it to verify-el: all 8 Violated verdicts on ORE are instrument false positives (F4: ⊤⊑C not applied to elements; F5: BoundTripped reported as Violated) #87. It is the gate that can see the specific risk the broader floor introduces — a new false Violated, or a false all-clear, from labels added at corpus scale.
2. The scoping difference. The merged commit states its own residual honestly ("the instrument no longer tests whether the CLOSURE derived ⊤ ⊑ C for a NAMED class"). Restricting the floor to labels containing no named class recovers that at no cost, and I have a sabotage-verified unit pin for it. Filed separately rather than reopening a merged, deliberate decision.

Worth recording from this branch regardless: my first scoping guard survived its own sabotage — it removed a label entry via test_only_remove_from_label, which runs after interning, so it failed under either scoping and discriminated nothing. The merged commit reports hitting the same class of problem independently ("MY OWN GUARD DID NOT GUARD, FIRST TIME ROUND"). Two of us, same afternoon, same trap.