core-labs/core
1
0
Fork 0
Code Issues Pull requests 1 Projects Releases Packages Wiki Activity Actions

feat: Phase 2 — finite-entity grounding compiler + Phase 1.5 finding

Browse source 
The first comprehension->structure compiler: evals/deductive_logic/grounding.py
lowers a typed finite-entity problem (finite entities + unary predicates +
single-variable universal rules) into the propositional regime the ADR-0206
entailment operator decides, refusal-first with a closed typed reason vocabulary
(unsafe_symbol / unknown_entity / unsupported_predicate_arity / unsupported_
quantifier / malformed_case / empty_case) and collision-safe atom slugging.

finite_entity/v1/cases.jsonl: 8 cases with INDEPENDENT (oracle-derived) gold
(4 entailed, 2 unknown, 1 refuted, 1 refused) — chained rules, conjunctive
bodies, negative heads, inconsistent premises. 20 tests gate engine==oracle==gold.

This is the second diversity-panel domain (distinct comprehension, same checkable
substrate) — the universal-structure thesis validated on a different problem shape,
with the anti-overfit >=2-domain discipline now live.

Phase 1.5 finding recorded: a clean geometric/algebraic propositional decoder
agrees 716/716 with the oracle but is O(2^n) (enumeration-class), so logic is the
wrong first domain for field-as-reasoner; the wedge redirects to quantitative-
relational structure where the field is the natural non-redundant decoder.
This commit is contained in:
Shay 2026-06-04 16:32:03 -07:00
parent 4d964020a9
commit 3e2a52870d
4 changed files with 425 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

68
docs/analysis/universal-structure-and-field-symbol-coherence-gate-2026-06-04.md
View file

@ -112,13 +112,28 @@ result is an acceptable, honest outcome: where the field cannot earn agreement,
**stays a servant** and the symbolic path carries that domain, refusing where it
cannot verify. **No unfalsifiable "the field knows" claim ever enters the codebase.**
**The wedge (Phase 1.5):** *Can the field decide propositional entailment
geometrically and agree with the ROBDD oracle on held-out, `wrong = 0`?* Logic is
the ideal first test — the ROBDD + independent oracle already give a rock-solid gold
(500/500). Embed atoms/clauses as geometric objects; decide entailment by
incidence/coherence; require `field_verdict == ROBDD_verdict == oracle` on a
held-out set. Agree → the field has earned a reasoning role and we have our first
genuine second derivation. Cannot → we learned it cheaply and honestly.
**The wedge (Phase 1.5) — FINDING (2026-06-04): logic is the wrong first domain.**
The original wedge asked whether the field could decide *propositional entailment*
geometrically and agree with the ROBDD oracle. A bounded experiment settled it: the
cleanest geometric/algebraic encoding (the commuting-idempotent *function-algebra*,
each formula → its function on the `2^n` minterms) **agrees 716/716 with the oracle
but is `O(2^n)`** — it is truth-table enumeration in algebraic clothing, *not* a
genuine sub-enumeration reduction the way the ROBDD is. So a geometric decoder for
logic would either re-encode enumeration (adding no independence the oracle does not
already provide) or be decoration. **Propositional logic is combinatorial
(all-assignments), not geometric/metric** — the field engine's native strength
(distance, incidence, proportion, betweenness) has no purchase there.
**Corrected wedge — quantitative-relational structure.** The field must first earn
its reasoning role where the structure is genuinely *metric*: quantitative-relational
problems (`A is twice B`, `A is 3 more than B`, part-whole, ratios) — exactly where
GSM8K *comprehension* lives. There, the field derivation (solve the linear/metric
relation system by propagation) and the symbolic derivation (step-by-step arithmetic)
are two genuinely distinct decodings, and their agreement on the dataset answer is a
real second derivation. Logic keeps its independent gold (ROBDD ⟂ truth-table oracle)
as a *symbolic* second derivation; the *field* earns its role in the metric domains.
This is the plan working as designed: the field earned nothing it did not deserve,
and we learned the right domain cheaply.
## 4. Phased plan
@ -126,20 +141,31 @@ genuine second derivation. Cannot → we learned it cheaply and honestly.
(`tests/test_architectural_invariants.py`): no capability claim without an
independent gold sharing no code with the SUT; deductive lane SHA-pinned
(`deductive_logic_v1`). The foundation every later phase rides on.
- **Phase 1 — canonize the universal structure.** Promote
`SemanticSymbolicBindingGraph` to *the* documented problem-structure interlingua;
resolve its closed-vocab placeholder (`semantic_role="unknown"`) only when a
load-bearing consumer defines it. Add a **hemisphere-role invariant**: servant
modules (parsers, metrics, vault) may not bypass the structure's consistency
checks. (The taxonomy is a proposal to validate before the enforcing INV lands.)
- **Phase 1.5 — the keystone wedge.** Field-decides-entailment vs. ROBDD oracle on
the deductive lane. Prove (or honestly refute) field-as-reasoner on the safest
gold. Gate to everything geometric.
- **Phase 2 — comprehension compiler → binding graph** (finite-entity grounding
first), with **field ⟂ symbol agreement** as the admission gate from the moment
Phase 1.5 succeeds. **The diversity panel starts here** (see cross-cutting): the
compiler is validated against ≥2 structurally-distinct golded domains from its
first commit, so it cannot overfit to math-shaped problems.
- **Phase 1 — canonize the universal structure. ✅ SHIPPED.**
`SemanticSymbolicBindingGraph` is the documented problem-structure interlingua;
**INV-26** enforces its neutrality (the interlingua imports no field/eval/runtime,
and its core imports no domain reader — only allowlisted bridges may). Deferred:
resolving the closed-vocab placeholder (`semantic_role="unknown"`) until a
load-bearing consumer defines it; the stronger "servant may not bypass consistency
checks" rule (the checkable neutrality half shipped; the rest stays doctrine until
a checkable form exists).
- **Phase 1.5 — the keystone wedge. ✅ RUN (logic ruled out; wedge redirected).**
The propositional-logic wedge was settled by experiment (§3): a clean geometric
encoding is enumeration-class, so logic cannot prove field-as-reasoner. The wedge
is redirected to **quantitative-relational** structure, where the field
(metric/proportion propagation) and the symbol (step arithmetic) are genuinely
distinct decodings. The dedicated quantitative wedge is the next field-reasoner
experiment.
- **Phase 2 — comprehension compiler → binding graph.** **✅ FIRST SLICE SHIPPED:**
the finite-entity grounding compiler (`evals/deductive_logic/grounding.py`) lowers
a typed finite-entity problem (entities + unary predicates + single-var universal
rules) into the propositional regime, refusal-first, gated by `engine == oracle ==
gold` — the first reader proving a *different problem shape* compiles into the same
checkable substrate. **The diversity panel starts here** (see cross-cutting):
finite-entity is the second golded domain, so the compiler is validated against ≥2
structurally-distinct domains from its first commit and cannot overfit to one
shape. Remaining Phase 2: target the binding-graph interlingua directly and add
**field ⟂ symbol agreement** as the admission gate once the quantitative wedge lands.
- **Phase 3 — activate `t2_precision`.** The field⟂symbol agreement *is* the t2
signal; wire the propose-loop consuming `checker="t2_precision"`. No invented
second derivation needed — it is real now.

8
evals/deductive_logic/finite_entity/v1/cases.jsonl Normal file
View file

@ -0,0 +1,8 @@
{"entities": ["cat", "dog"], "facts": [{"entity": "cat", "polarity": true, "predicate": "furry"}], "gold": "entailed", "id": "fe-v1-0001", "query": {"entity": "cat", "polarity": true, "predicate": "mammal"}, "rules": [{"if": [{"polarity": true, "predicate": "furry", "var": "x"}], "then": {"polarity": true, "predicate": "mammal", "var": "x"}}]}
{"entities": ["cat", "dog"], "facts": [{"entity": "cat", "polarity": true, "predicate": "furry"}], "gold": "unknown", "id": "fe-v1-0002", "query": {"entity": "dog", "polarity": true, "predicate": "mammal"}, "rules": [{"if": [{"polarity": true, "predicate": "furry", "var": "x"}], "then": {"polarity": true, "predicate": "mammal", "var": "x"}}]}
{"entities": ["alice"], "facts": [{"entity": "alice", "polarity": true, "predicate": "human"}], "gold": "entailed", "id": "fe-v1-0003", "query": {"entity": "alice", "polarity": true, "predicate": "mortal"}, "rules": [{"if": [{"polarity": true, "predicate": "human", "var": "x"}], "then": {"polarity": true, "predicate": "mortal", "var": "x"}}]}
{"entities": ["bird1"], "facts": [{"entity": "bird1", "polarity": true, "predicate": "penguin"}], "gold": "refuted", "id": "fe-v1-0004", "query": {"entity": "bird1", "polarity": true, "predicate": "flies"}, "rules": [{"if": [{"polarity": true, "predicate": "penguin", "var": "x"}], "then": {"polarity": false, "predicate": "flies", "var": "x"}}]}
{"entities": ["x1"], "facts": [{"entity": "x1", "polarity": true, "predicate": "a"}], "gold": "entailed", "id": "fe-v1-0005", "query": {"entity": "x1", "polarity": true, "predicate": "c"}, "rules": [{"if": [{"polarity": true, "predicate": "a", "var": "v"}], "then": {"polarity": true, "predicate": "b", "var": "v"}}, {"if": [{"polarity": true, "predicate": "b", "var": "v"}], "then": {"polarity": true, "predicate": "c", "var": "v"}}]}
{"entities": ["t"], "facts": [{"entity": "t", "polarity": true, "predicate": "red"}, {"entity": "t", "polarity": true, "predicate": "round"}], "gold": "entailed", "id": "fe-v1-0006", "query": {"entity": "t", "polarity": true, "predicate": "apple"}, "rules": [{"if": [{"polarity": true, "predicate": "red", "var": "x"}, {"polarity": true, "predicate": "round", "var": "x"}], "then": {"polarity": true, "predicate": "apple", "var": "x"}}]}
{"entities": ["t"], "facts": [{"entity": "t", "polarity": true, "predicate": "red"}], "gold": "unknown", "id": "fe-v1-0007", "query": {"entity": "t", "polarity": true, "predicate": "apple"}, "rules": [{"if": [{"polarity": true, "predicate": "red", "var": "x"}, {"polarity": true, "predicate": "round", "var": "x"}], "then": {"polarity": true, "predicate": "apple", "var": "x"}}]}
{"entities": ["s"], "facts": [{"entity": "s", "polarity": true, "predicate": "sick"}, {"entity": "s", "polarity": false, "predicate": "sick"}], "gold": "refused", "id": "fe-v1-0008", "query": {"entity": "s", "polarity": true, "predicate": "sick"}, "rules": []}

201
evals/deductive_logic/grounding.py Normal file
View file

@ -0,0 +1,201 @@
"""Finite-entity grounding — compile a typed finite-entity problem to
propositional atoms (Phase 2 of the universal-structure plan; the deductive-logic
runway doc's PR-1).
This is the first **comprehension compiler**: it lowers a structured, finite-entity
problem (finite named entities, unary predicates, single-variable universal rules)
into the propositional regime the ADR-0206 entailment operator already decides —
exactly where `wrong == 0` is structural. A grounded finite-entity problem (each
``predicate(entity)`` pair → one atom) IS propositional and in scope; anything
outside the narrow v1 grammar refuses with a typed reason rather than guessing.
Lowering law (deterministic):
predicate(entity) -> ``predicate_slug__entity_slug`` (atom)
negative literal -> ``~atom``
rule body (∧ of literals) -> conjunction of lowered body literals
universal rule ∀x. B(x)->H(x)-> for each entity e: ``lower(B[e]) -> lower(H[e])``
query -> the lowered query literal
The lowered ``(premises, query)`` is decided by **two independent procedures**
(the ROBDD engine and the truth-table oracle); a case counts only when both agree
with the gold (INV-25). v1 keeps the grammar intentionally narrow — that narrowness
is the firewall, not a weakness.
Sealed: no ``chat`` import, no serving path. Deterministic.
"""
from __future__ import annotations
import re
from dataclasses import dataclass
from typing import Any, Final
# Closed refusal vocabulary for the grounding layer — distinct from the entailment
# operator's reasons so a malformed case never leaks into an ambiguous failure.
UNSUPPORTED_PREDICATE_ARITY: Final[str] = "unsupported_predicate_arity"
UNSUPPORTED_QUANTIFIER: Final[str] = "unsupported_quantifier"
UNSAFE_SYMBOL: Final[str] = "unsafe_symbol"
UNKNOWN_ENTITY: Final[str] = "unknown_entity"
UNKNOWN_VARIABLE: Final[str] = "unknown_variable"
MALFORMED_CASE: Final[str] = "malformed_case"
EMPTY_CASE: Final[str] = "empty_case"
GROUNDING_REASONS: Final[frozenset[str]] = frozenset({
UNSUPPORTED_PREDICATE_ARITY,
UNSUPPORTED_QUANTIFIER,
UNSAFE_SYMBOL,
UNKNOWN_ENTITY,
UNKNOWN_VARIABLE,
MALFORMED_CASE,
EMPTY_CASE,
})
_ATOM_SEPARATOR: Final[str] = "__"
# A slug component: lowercase ASCII letters/digits/single underscores, no leading
# digit, no empty, no double-underscore (would collide with the separator).
_SLUG_RE: Final[re.Pattern[str]] = re.compile(r"[a-z][a-z0-9]*(?:_[a-z0-9]+)*")
class GroundingError(ValueError):
"""A finite-entity case outside the v1 grammar. Carries a typed reason."""
def __init__(self, reason: str, detail: str = "") -> None:
if reason not in GROUNDING_REASONS:
raise ValueError(f"unknown grounding reason: {reason!r}")
self.reason = reason
super().__init__(f"{reason}: {detail}" if detail else reason)
@dataclass(frozen=True, slots=True)
class GroundedProblem:
"""The lowered finite-entity problem: propositional premises + query."""
premises: tuple[str, ...]
query: str
def slug(token: Any) -> str:
"""Deterministic, collision-safe slug. Rejects (never silently repairs)
anything outside ``[a-z][a-z0-9]*(_[a-z0-9]+)*`` — including the separator,
leading digits, empties, and double underscores."""
if not isinstance(token, str):
raise GroundingError(UNSAFE_SYMBOL, f"non-string symbol {token!r}")
s = token.strip().lower()
if not s:
raise GroundingError(UNSAFE_SYMBOL, "empty symbol")
if _ATOM_SEPARATOR in s:
raise GroundingError(UNSAFE_SYMBOL, f"symbol {token!r} contains separator '{_ATOM_SEPARATOR}'")
if not _SLUG_RE.fullmatch(s):
raise GroundingError(UNSAFE_SYMBOL, f"symbol {token!r} is not a safe slug")
return s
def atom(predicate: Any, entity: Any) -> str:
"""``predicate(entity)`` → the canonical propositional atom."""
return f"{slug(predicate)}{_ATOM_SEPARATOR}{slug(entity)}"
def _literal(predicate: Any, entity: Any, polarity: Any) -> str:
if not isinstance(polarity, bool):
raise GroundingError(MALFORMED_CASE, f"polarity must be a bool, got {polarity!r}")
a = atom(predicate, entity)
return a if polarity else f"~{a}"
def _require(condition: bool, reason: str, detail: str = "") -> None:
if not condition:
raise GroundingError(reason, detail)
def _check_unary(obj: dict[str, Any], *, allow_var: bool) -> None:
"""Reject any non-unary / relational / functional shape (v1 is unary only)."""
keys = set(obj)
# A binary relation / function would carry extra argument keys.
extra = keys - {"predicate", "entity", "var", "polarity"}
_require(not extra, UNSUPPORTED_PREDICATE_ARITY, f"unexpected keys {sorted(extra)}")
has_entity = "entity" in obj
has_var = "var" in obj
if allow_var:
_require(has_entity ^ has_var, MALFORMED_CASE, "literal needs exactly one of entity/var")
else:
_require(has_entity and not has_var, UNKNOWN_VARIABLE, "free variable outside a rule")
def lower_case(case: dict[str, Any]) -> GroundedProblem:
"""Lower a finite-entity case to ``(premises, query)``. Refuse-first.
Schema (v1):
{"entities": [str, ...],
"facts": [{"predicate": str, "entity": str, "polarity": bool}, ...],
"rules": [{"if": [<unary literal with var>, ...],
"then": <unary literal with var>}, ...],
"query": {"predicate": str, "entity": str, "polarity": bool}}
"""
if not isinstance(case, dict) or not case:
raise GroundingError(EMPTY_CASE, "case is empty or not a mapping")
entities = case.get("entities")
if not (isinstance(entities, list) and entities):
raise GroundingError(EMPTY_CASE, "no entities")
entity_set = {slug(e) for e in entities} # also validates each entity slug
_require(len(entity_set) == len(entities), MALFORMED_CASE, "duplicate entities after slugging")
if "query" not in case:
raise GroundingError(MALFORMED_CASE, "no query")
premises: list[str] = []
facts = case.get("facts", []) or []
rules = case.get("rules", []) or []
_require(isinstance(facts, list), MALFORMED_CASE, "facts must be a list")
_require(isinstance(rules, list), MALFORMED_CASE, "rules must be a list")
# Facts — ground unary literals over named entities.
for fact in facts:
_require(isinstance(fact, dict), MALFORMED_CASE, f"fact is not a mapping: {fact!r}")
_check_unary(fact, allow_var=False)
_require(slug(fact["entity"]) in entity_set, UNKNOWN_ENTITY, str(fact.get("entity")))
premises.append(_literal(fact["predicate"], fact["entity"], fact.get("polarity", True)))
# Rules — single-variable universal rules, grounded by explicit entity expansion.
for rule in rules:
_require(isinstance(rule, dict), MALFORMED_CASE, f"rule is not a mapping: {rule!r}")
_require("quantifier" not in rule and "exists" not in rule,
UNSUPPORTED_QUANTIFIER, "only implicit single-var universal rules in v1")
body = rule.get("if")
head = rule.get("then")
if not (isinstance(body, list) and body):
raise GroundingError(MALFORMED_CASE, "rule body must be a non-empty list")
if not isinstance(head, dict):
raise GroundingError(MALFORMED_CASE, "rule head must be a literal")
var = _rule_variable(body, head)
for ent in entities:
body_atoms = [_literal(lit["predicate"], ent, lit.get("polarity", True)) for lit in body]
head_atom = _literal(head["predicate"], ent, head.get("polarity", True))
body_conj = " & ".join(f"({b})" for b in body_atoms)
premises.append(f"({body_conj}) -> ({head_atom})")
_ = var # validated; grounding is by explicit entity expansion, not by name
query = case["query"]
_require(isinstance(query, dict), MALFORMED_CASE, "query must be a literal")
_check_unary(query, allow_var=False)
_require(slug(query["entity"]) in entity_set, UNKNOWN_ENTITY, str(query.get("entity")))
query_lit = _literal(query["predicate"], query["entity"], query.get("polarity", True))
return GroundedProblem(premises=tuple(premises), query=query_lit)
def _rule_variable(body: list[dict[str, Any]], head: dict[str, Any]) -> str:
"""Confirm the rule is single-variable: every literal uses one shared var,
no named entities (those would make it not universal). Returns the var name."""
seen: set[str] = set()
for lit in (*body, head):
_require(isinstance(lit, dict), MALFORMED_CASE, f"rule literal not a mapping: {lit!r}")
_check_unary(lit, allow_var=True)
_require("var" in lit, MALFORMED_CASE, "rule literals must use a variable, not a named entity")
v = lit["var"]
_require(isinstance(v, str) and bool(v.strip()), MALFORMED_CASE, "empty variable")
seen.add(v)
_require(len(seen) == 1, UNSUPPORTED_QUANTIFIER, f"v1 allows one variable per rule, saw {sorted(seen)}")
return seen.pop()

169
tests/test_deductive_logic_finite_entity_grounding.py Normal file
View file

@ -0,0 +1,169 @@
"""Phase 2 — finite-entity grounding compiler (deductive-logic runway PR-1/PR-2).
Proves the first comprehension compiler lowers a typed finite-entity problem into
the propositional regime deterministically and refusal-first, and that the lowered
form is decided identically by the ROBDD engine AND the independent truth-table
oracle (INV-25: the committed gold is reproduced by a procedure sharing no code
with the engine).
"""
from __future__ import annotations
import json
from pathlib import Path
import pytest
from evals.deductive_logic.grounding import (
MALFORMED_CASE,
UNKNOWN_ENTITY,
UNSAFE_SYMBOL,
UNSUPPORTED_PREDICATE_ARITY,
UNSUPPORTED_QUANTIFIER,
GroundingError,
atom,
lower_case,
slug,
)
from evals.deductive_logic.oracle import oracle_entailment
from generate.proof_chain.entail import evaluate_entailment
_FIXTURE = Path(__file__).resolve().parents[1] / "evals" / "deductive_logic" / "finite_entity" / "v1" / "cases.jsonl"
def _load_fixture() -> list[dict]:
return [json.loads(line) for line in _FIXTURE.read_text(encoding="utf-8").splitlines() if line.strip()]
# --- lowering correctness -----------------------------------------------------
def test_atom_lowering_is_deterministic_and_canonical() -> None:
assert atom("Furry", "Cat") == "furry__cat"
assert atom("furry", "cat") == atom("Furry", " CAT ") # case/space-insensitive
assert atom("needs_food", "cat") == "needs_food__cat"
def test_unsafe_symbols_and_separator_ambiguity_reject() -> None:
for bad in ("fur__ry", "9lives", "", "has-claws", "a b", "tïger"):
with pytest.raises(GroundingError) as exc:
slug(bad)
assert exc.value.reason == UNSAFE_SYMBOL
def test_fact_lowering_including_negative_facts() -> None:
case = {
"entities": ["cat"],
"facts": [
{"predicate": "furry", "entity": "cat", "polarity": True},
{"predicate": "aquatic", "entity": "cat", "polarity": False},
],
"query": {"predicate": "furry", "entity": "cat", "polarity": True},
}
gp = lower_case(case)
assert "furry__cat" in gp.premises
assert "~aquatic__cat" in gp.premises
def test_unary_universal_rule_expands_over_all_entities() -> None:
case = {
"entities": ["cat", "dog", "fish"],
"facts": [],
"rules": [{"if": [{"predicate": "furry", "var": "x", "polarity": True}],
"then": {"predicate": "mammal", "var": "x", "polarity": True}}],
"query": {"predicate": "mammal", "entity": "cat", "polarity": True},
}
gp = lower_case(case)
grounded = [p for p in gp.premises if "->" in p]
assert len(grounded) == 3 # one per entity
assert any("furry__cat" in p and "mammal__cat" in p for p in grounded)
assert any("furry__dog" in p and "mammal__dog" in p for p in grounded)
assert any("furry__fish" in p and "mammal__fish" in p for p in grounded)
def test_conjunctive_rule_body_lowers_to_conjunction() -> None:
case = {
"entities": ["t"],
"facts": [],
"rules": [{"if": [{"predicate": "red", "var": "x", "polarity": True},
{"predicate": "round", "var": "x", "polarity": True}],
"then": {"predicate": "apple", "var": "x", "polarity": True}}],
"query": {"predicate": "apple", "entity": "t", "polarity": True},
}
gp = lower_case(case)
rule = next(p for p in gp.premises if "->" in p)
assert "red__t" in rule and "round__t" in rule and "&" in rule and "apple__t" in rule
# --- refusal boundary (typed reasons) ----------------------------------------
def test_unknown_entity_query_refuses() -> None:
case = {"entities": ["cat"], "facts": [],
"query": {"predicate": "furry", "entity": "mouse", "polarity": True}}
with pytest.raises(GroundingError) as exc:
lower_case(case)
assert exc.value.reason == UNKNOWN_ENTITY
def test_unknown_entity_in_fact_refuses() -> None:
case = {"entities": ["cat"],
"facts": [{"predicate": "furry", "entity": "mouse", "polarity": True}],
"query": {"predicate": "furry", "entity": "cat", "polarity": True}}
with pytest.raises(GroundingError) as exc:
lower_case(case)
assert exc.value.reason == UNKNOWN_ENTITY
def test_binary_relation_refuses_as_unsupported_arity() -> None:
# a relation carries a second argument key -> not unary -> refuse
case = {"entities": ["a", "b"],
"facts": [{"predicate": "loves", "entity": "a", "object": "b", "polarity": True}],
"query": {"predicate": "loves", "entity": "a", "polarity": True}}
with pytest.raises(GroundingError) as exc:
lower_case(case)
assert exc.value.reason == UNSUPPORTED_PREDICATE_ARITY
def test_multi_variable_rule_refuses() -> None:
case = {"entities": ["a"],
"rules": [{"if": [{"predicate": "p", "var": "x", "polarity": True}],
"then": {"predicate": "q", "var": "y", "polarity": True}}],
"query": {"predicate": "p", "entity": "a", "polarity": True}}
with pytest.raises(GroundingError) as exc:
lower_case(case)
assert exc.value.reason == UNSUPPORTED_QUANTIFIER
def test_empty_case_refuses() -> None:
with pytest.raises(GroundingError) as exc:
lower_case({})
assert exc.value.reason in {"empty_case", MALFORMED_CASE}
# --- determinism + the lane gate (engine == oracle == committed gold) --------
def test_lowering_is_deterministic_across_replay() -> None:
case = _load_fixture()[0]
a = lower_case(case)
b = lower_case(case)
assert a == b
@pytest.mark.parametrize("case", _load_fixture(), ids=lambda c: c["id"])
def test_committed_gold_is_engine_and_independent_oracle_agreement(case: dict) -> None:
"""The lane gate: every committed finite-entity case is decided identically by
the ROBDD engine AND the independent oracle, both equal to the committed gold."""
gp = lower_case(case)
engine = evaluate_entailment(gp.premises, gp.query).outcome.value
oracle = oracle_entailment(gp.premises, gp.query)
assert oracle == case["gold"], f"{case['id']}: independent oracle != committed gold"
assert engine == case["gold"], f"{case['id']}: engine confabulated vs gold (wrong=0 breach)"
def test_fixture_has_nontrivial_signal() -> None:
"""Guard against a vacuous fixture: it must carry entailed/refuted cases, not
only unknown/refused, or the lane proves nothing."""
golds = {c["gold"] for c in _load_fixture()}
assert "entailed" in golds and "refuted" in golds