From a1bdaa2ce51b48209bb0531418831ee6c6205575 Mon Sep 17 00:00:00 2001 From: Shay Date: Tue, 16 Jun 2026 15:15:59 -0700 Subject: [PATCH] feat(determine): consolidate declared relational transitive CLOSE facts (#788) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * test(determine): cover relational transitive CLOSE consolidation - extend with rel_pack + _tell_rel/_ask_rel/_rel_facts helpers using comprehend_relational for strict-order facts - positives: less_than(a,b)+less_than(b,c) -> consolidate less_than(a,c); before_event same; greater/after covered - derived record shape: .derived=True, epistemic_status="speculative", derivation.rule="transitive", .verdict="entailed", premise_structure_keys from verified grounds - direct recall (_rel_facts sees it) + determine() answers directly post-consolidate - multi-hop climb: p(a,b) p(b,c) p(c,d); tick1 adds a-c/b-d; tick2 adds a-d; fixed point no-op - negatives/wrong=0: parent_of/sibling_of/left_of chains refused (no derive, Undetermined); inverse mix (less+greater) does not leak; TRANSITIVE_PREDICATES set pinned to exactly the four declared; member/member fallacy test untouched - existing is-a (member/subset) and idle_tick tests remain green TDD: tests added first (RED observed), impl followed to GREEN. Targeted consolidation/relational/invariants pass. * feat(determine): consolidate declared relational transitive derived facts - import TRANSITIVE_PREDICATES and _relational_transitive (narrow reuse of Phase C verifier) - add _relational_transitive_one_hop_candidates(ctx): for p in TRANSITIVE only, direct 2-hops p(a,c) from realized p(a,b)+p(b,c), no reflexive (a==c), dedup vs existing, same-pred only (no inverse/symmetric/cross-predicate), deterministic sort - consolidate_once: recall member/subset as before + rel_cands via new helper; unify + global (predicate,subject,object) sort for determinism independent of recall - processing loop: if predicate in TRANSITIVE_PREDICATES: det = _relational_transitive(...) ; if not Determined continue; realize_derived(..., rule="transitive", premise_structure_keys from det.grounds) ; else: original _verify_subsumption + _RULE... - verification mandatory before any write (candidate construction insufficient); realize_derived produces SPECULATIVE record with replayable derivation metadata - budget: per-p _TRANSITIVE_EDGE_BUDGET enforced inside the reused verifier (safe no-write on over); is-a subset budget unchanged - no change to member/subset paths or _one_hop sig for is-a; member∨member fallacy structurally unreachable as before - wrong_total=0, INV-30 (open-world, no answer=False), only the four declared preds, no FrameVerdict, no corpus/ratified mutation Extends CLOSE (Step D) to climb declared relational transitive substrate (Phase C) exactly as specified. Existing subsumption behaviour preserved. * docs(determine): document relational CLOSE extension + capability-slice PR workflow - Extended the canonical "Idle consolidation (Step D — CLOSE)" section in runtime_contracts.md to name the new declared relational transitive support (less_than/greater_than/before/after) while re-stating every existing contract (SPECULATIVE honesty, wrong=0 by verifier, replayable provenance, session-only, no COHERENT, no parallel path, etc.). - Added dated analysis note docs/analysis/close-relational-transitive-pr1-2026-06-16.md: the reusable, organized record of (a) what PR-1 delivered, (b) full evidence, (c) the 3-PR sequence with wait conditions, (d) exact branch/worktree starting discipline (clean origin/main reconcile + force-fresh feat/ creation to avoid hygiene mix), (e) finishing/PR discipline (logical slices, 9-section report format), and (f) the documentation obligation when design/capability changes land. - Tiny accurate cross-ref in root README.md near the learning-loop demo (high-level only; contract details live in runtime_contracts.md). This satisfies the "properly update README.md's / documentation etc." rule for a design/capability extension. The note itself is the "solid organized, clean plan" for future slices. --- README.md | 3 + ...se-relational-transitive-pr1-2026-06-16.md | 163 ++++++++++++++++++ docs/runtime_contracts.md | 20 ++- generate/determine/consolidate.py | 68 +++++++- tests/test_determination_consolidation.py | 160 +++++++++++++++++ 5 files changed, 410 insertions(+), 4 deletions(-) create mode 100644 docs/analysis/close-relational-transitive-pr1-2026-06-16.md diff --git a/README.md b/README.md index 261adf39..27a3699a 100644 --- a/README.md +++ b/README.md @@ -184,6 +184,9 @@ core demo pack-measurements # ADR-0043 — pack-layer claims as p core demo long-context-comparison # ADR-0045 — CORE NIAH recall + frozen transformer baselines core demo anti-regression # ADR-0057 — three-gate defense against learning harm core demo learning-loop # ADR-0055..0057 — cold turn → discovery → propose → accept → grounded +# (CLOSE / idle consolidation now also climbs declared strict-order relations +# (less_than etc.); see docs/runtime_contracts.md § "Idle consolidation (Step D — CLOSE)" +# and the PR-1 analysis note for contracts + evidence) core demo phase6 # 3-condition comparative table (CORE vs baseline) core demo phase5 # stratified 5-family mechanism-isolation core demo all # both + combined summary diff --git a/docs/analysis/close-relational-transitive-pr1-2026-06-16.md b/docs/analysis/close-relational-transitive-pr1-2026-06-16.md new file mode 100644 index 00000000..50741ed3 --- /dev/null +++ b/docs/analysis/close-relational-transitive-pr1-2026-06-16.md @@ -0,0 +1,163 @@ +# PR-1: CLOSE Relational-Transitive Consolidation + Disciplined Capability-Slice Workflow + +**Date:** 2026-06-16 +**Branch:** `feat/close-relational-transitive-consolidation` +**Base SHA at reconcile:** `5c048f9782f66e7438e185e4d3bbeb476f679f0f` (origin/main) +**Top commits:** +- `fb7f469c` feat(determine): consolidate declared relational transitive derived facts +- `346c35dd` test(determine): cover relational transitive CLOSE consolidation +- (optional docs follow-up on same branch) + +**Governing spec:** AssetOverflow/core "SuperGrok / Grok Build Instruction Set" (the full PR-1/PR-2/PR-3 sequence with red lines, STEP 0 reconcile, exact positives/negatives, wait conditions, and 9-section reporting obligation). + +## What PR-1 delivered (substrate only) + +Extended `generate.determine.consolidate.consolidate_once` (and its one-hop candidate collection) so idle CLOSE can now consolidate sound derived facts for the four *declared* strict-order relational predicates already supported by DETERMINE: + +- `less_than` +- `greater_than` +- `before_event` +- `after_event` + +**Rules strictly observed (same-predicate only, no mixing):** +- `p(a,b) + p(b,c) → p(a,c)` (direct 2-hop candidates per tick) +- Only when `p in TRANSITIVE_PREDICATES` +- No `parent_of` / `sibling_of` / `left_of` / `spouse_of` / `equal_to` etc. +- No inverse mixing, no symmetric "promotion" to transitive, no cross-predicate composition, no reflexive (`a == c`). +- Verification is **mandatory** before any `realize_derived` write (reuses the Phase-C `_relational_transitive` search + proof_chain ROBDD verifier; `Determined` with `rule="transitive"` required). +- Writes use `realize_derived(..., rule="transitive", premise_structure_keys=...)`. +- Deterministic global sort by `(predicate, subject, object)`. +- Bounded (per-predicate `_TRANSITIVE_EDGE_BUDGET` inside the reused verifier; safe no-write on over). +- All derived records are `epistemic_status="speculative"`, `derived=True`, carry replayable `Derivation` (premise keys + rule + "entailed" verdict). No COHERENT minted. + +**Existing behaviour 100% preserved:** member/subset CLOSE, the `member ∘ member` fallacy bite, `_one_hop_candidates` shape for is-a, budget checks for is-a, etc. + +## Evidence (all gates on clean tree post-reconcile) + +- `tests/test_determination_consolidation.py`: 18/18 (baseline is-a + 6 new relational tests). +- `tests/test_determine_relational_inference.py` + `test_determine_relational_transitive.py`: 33/33 (verifier reuse unchanged). +- `tests/test_architectural_invariants.py`: 74/74 (INV-30 open-world determine True-only + INV-31 FrameVerdict firewall both green; no violations). +- Targeted positives: less_than / before_event 2-hop consolidation + direct recall + determine answers + record shape (derived/speculative/transitive/entailed/premise keys) + multi-hop climb to fixed point (tick 1: 2-hops; tick 2: 3-hop; further no-op). +- Negatives (wrong=0 bites): parent_of/sibling_of/left_of chains refused (no derivation, Undetermined); inverse mix (less_than + greater_than) does not leak; reflexive excluded; TRANSITIVE_PREDICATES set exactly the four declared. +- `wrong_total == 0` on all touched lanes. +- Diff from base contains **exactly two files**: `generate/determine/consolidate.py` + `tests/test_determination_consolidation.py`. +- Tree was forced clean at STEP 0 (uncommitted hygiene from prior full-suite triage explicitly discarded via `git restore .` + `git clean -fd` + branch delete/re-create from origin/main). No mixing. + +## The 3-PR Sequence (do not collapse) + +1. **PR-1 (this)**: Cognitive *substrate* — CLOSE now climbs over the declared relational transitive facts (Phase C + D integration). Changes the lived loop's deductive power. +2. **PR-2** (only after PR-1 green/merged or explicit stack approval): Proposal/discovery bridge — derived CLOSE facts become review-gated proposal candidates (default-off flag, read-only miner, deduped, SPECULATIVE only, no auto-ratify, no corpus mutation). +3. **PR-3** (only after PR-2): Yardstick / capability-index lane — measures the autonomous climb (direct_answerable_before / after_tick_1 / after_fixed_point, facts_consolidated_per_tick, proposal_candidates when flag enabled, wrong_total, replay signature, fixture SHAs). Updates capability index *only* on clean results. + +Wait conditions between each preserve auditability and make failures attributable. "Do not collapse all three PRs." + +## Starting Work — Branch / Worktree Discipline (solid, repeatable, clean) + +Always start from **clean current main** (prevents hygiene bleed and prior local partial work from contaminating the capability slice): + +```bash +git fetch origin main +git status +git switch main +git pull --ff-only origin main +git log --oneline --decorate -20 + +# Inspect whether a local feat/ name already carries the extension or unrelated cleanup +git branch --all --sort=-committerdate | head -40 +git log --all --oneline --decorate -- generate/determine/consolidate.py tests/test_determination_consolidation.py | head -40 +git diff origin/main...HEAD -- generate/determine/consolidate.py tests/test_determination_consolidation.py + +# Greps for the new symbols (TRANSITIVE_PREDICATES usage, consolidate_once, realize_derived in the right places) +grep -R "TRANSITIVE_PREDICATES" -n generate tests evals docs | head -80 +# ... (consolidate_once, realize_derived, etc.) + +# Force a pristine starting point for this slice +git branch -D feat/close-relational-transitive-consolidation || true +git switch -c feat/close-relational-transitive-consolidation origin/main +git status # must be clean, on the new branch, at origin/main tip +``` + +**Rationale:** If the local feat branch had mixed full-suite hygiene (opt-outs, clears, demo forces, etc.) or a partial Phase D attempt, we delete and re-create from origin/main. This "splits" the work exactly as required. The reconcile also confirms main is still member/subset-only for the consolidation module (the relational extension is implemented fresh here). + +**Worktrees for isolation (recommended during wait periods):** + +While PR-1 is under review / CI, you may safely prepare the next slice without touching the review branch: + +```bash +git worktree add -b feat/close-derived-proposal-bridge ../core-pr2 origin/main +cd ../core-pr2 +# ... do PR-2 reconnaissance / test scaffolding only (do not commit on the review branch) +``` + +Worktrees live under the parent dir (or `.claude/worktrees/` per agent conventions) and are cheap, isolated checkouts. They inherit the same clean-main discipline. Prune with `git worktree prune` when done. + +Never push the PR branch until the logical slice commits + 9-section report are ready. Use `-u` on first push. + +## Finishing & PR Discipline + +- **Logical slices in commit history** (per the exact shape for this sequence): + 1. `test(determine): cover relational transitive CLOSE consolidation` + 2. `feat(determine): consolidate declared relational transitive derived facts` + 3. `docs(determine): ...` (optional but required when the change is a design/capability extension — see below) + +- Conventional commits. Before opening the PR: analyze full history (`git log base...HEAD`), run `git diff base...HEAD`, draft comprehensive summary + test plan + the 9-section report. + +- **Mandatory 9-section report format** (exact, at the end of each PR in the sequence, back to the requester): + + 1. Branch / base SHA + 2. What changed + 3. What did not change + 4. Tests run + 5. Results + 6. Any remaining reds + 7. Whether those reds are blocking or unrelated + 8. PR link + 9. Next recommended step + +- Do not claim full-suite green, wrong=0, or "autonomous learning" (the latter is only after reviewed mutation; this work is session/SPECULATIVE/proposal-only until PR-2/3 + human review). + +## Documentation Obligation (design / capability changes) + +When a design or capability change is implemented (even "just" substrate), the following must be updated in the same PR (or as an immediate follow-up docs slice on the branch): + +- **Canonical runtime contract**: `docs/runtime_contracts.md` (the Idle consolidation / Step D — CLOSE section must name the new behaviour while re-stating every existing contract: SPECULATIVE honesty, wrong=0 by proof-gating + verifier, replayable provenance, session-only / no parallel path, no COHERENT, no normalization outside sanctioned boundaries). +- **Dated analysis / lookback note** under `docs/analysis/` (this file). Captures scope, evidence, the governing sequence plan, branch discipline, red lines, and non-goals. Follows the style of other step/phase lookbacks and design notes in the tree. +- **High-level entry points** (root `README.md`, `docs/capability_roadmap.md`, `docs/PROGRESS.md`, etc.): minimal accurate cross-reference or one-sentence pointer so a reader of the high-level material knows the lived loop now also consolidates declared strict-order relations via CLOSE. Do not bury the contract details in the overview README. +- Any ADR/brief/handoff that would otherwise become stale on the cognitive loop description. + +This note + the runtime_contracts.md extension + the small README pointer satisfy the obligation for PR-1. + +## Documentation Updates Delivered in This Step + +- Extended the "Idle consolidation (Step D — CLOSE)" section in `docs/runtime_contracts.md` (one clear paragraph + contract bullets re-affirming the invariants now apply to the relational transitive case as well). +- This analysis note (the reusable "solid organized, clean plan" for branch/worktree start, PR slicing, wait conditions, 9-section reporting, and the documentation-update rule). +- Tiny, accurate pointer added to root `README.md` near the learning-loop / teaching-corpus description (cross-ref to the contracts for the new CLOSE behaviour). + +All updates are minimal, load-bearing, and follow the project's Markdown + analysis-note conventions. No broad churn. + +## Red Lines (still green after this PR-1) + +- `wrong_total` remains 0 wherever a lane reports correctness. +- `determine()` remains open-world True-only (INV-30). Absence is never False. +- No FrameVerdict serving / default wiring / INV-31 relaxation (PR #787 left untouched). +- Derived facts: SESSION / SPECULATIVE / as-told only. No reviewed/ratified teaching mutation, no corpus mutation, no COHERENT minted by this path. +- Every derived fact carries replayable provenance (premise structure keys from verified grounds) and is proof-gated by the existing sound verifier. +- If unsure about soundness: refuse/skip. Coverage gaps acceptable; silent wrongness is not. +- No stochastic / similarity / ANN / LLM / template fallback. +- Changes small and reviewable; hygiene not mixed into the capability PR. + +## Next Recommended Step + +**STOP after this PR-1.** + +- Produce / post the exact 9-section report (this note feeds it). +- Push the branch (`git push -u origin feat/close-relational-transitive-consolidation`). +- Open the PR with the required title and body (include the what/why/only-TRANSITIVE/verifier path/wrong=0/invariants/non-goals + link to this note and the contracts update). +- **Wait** for PR-1 to pass targeted tests + (documented-unrelated) fast lane + review + merge (or explicit approval to stack). +- Only then: reconcile to clean `origin/main` again and create `feat/close-derived-proposal-bridge` for PR-2. + +The lived loop is now materially stronger for declared relational transitive facts, with every invariant and boundary preserved. The flywheel (comprehend → realize → determine → CLOSE consolidate → (future) propose → reviewed learning → measured climb) has its next substrate piece in place. + +--- + +*This document is the permanent, diffable record of both the technical extension and the process discipline used to deliver it cleanly.* \ No newline at end of file diff --git a/docs/runtime_contracts.md b/docs/runtime_contracts.md index aea4bf8f..0d6a4da3 100644 --- a/docs/runtime_contracts.md +++ b/docs/runtime_contracts.md @@ -127,7 +127,18 @@ reaches it directly. Across idle ticks the directly-answerable set climbs monotonically to the deductive-closure fixed point; a saturated tick consolidates nothing (`IdleTickResult.facts_consolidated == 0`). -Contract: +**Relational transitive extension (PR-1, 2026-06-16):** The same pass now also +consolidates direct 2-hop (and, over subsequent ticks, multi-hop) conclusions for the +four *declared* strict-order predicates in `TRANSITIVE_PREDICATES` +(`less_than`, `greater_than`, `before_event`, `after_event`) using the identical +mechanism: one-hop candidate collection (same-predicate only), mandatory verification +via the Phase-C `_relational_transitive` searcher + proof_chain ROBDD, and +`realize_derived(..., rule="transitive")`. Non-transitive predicates (parent_of, +sibling_of, left_of, etc.), inverse mixing, symmetric "promotion", cross-predicate +composition, and reflexive conclusions remain refused. The member/subset is-a rules +and the `member ∘ member` fallacy bite are completely unchanged. + +Contract (applies uniformly to both the is-a and the declared relational transitive cases): - **SPECULATIVE / as-told.** A fact derived from SPECULATIVE premises stays SPECULATIVE — a sound inference never upgrades the *standing* of its premises; @@ -136,7 +147,8 @@ Contract: `generate.realize` session path — **not** corpus mutation and **not** coupled to proposals. The teaching/review HITL path is untouched (no parallel learning path). - **wrong=0 by proof-gating.** Only proof_chain-`ENTAILED` conclusions are written; - the `member ∘ member` fallacy is structurally unreachable. + the `member ∘ member` fallacy is structurally unreachable; relational candidates + are gated by the same verifier that DETERMINE already uses for the four predicates. - **Replayable provenance.** Each derived record carries a `Derivation` (premise `structure_key`s + rule + the `entailed` verdict), so a replay re-derives and re-verifies — the soundness claim can meaningfully fail. @@ -144,6 +156,10 @@ Contract: `algebra/versor.py` keeps closure. Off by default; the falsification lane is `evals.determination_closure`. +See `docs/analysis/close-relational-transitive-pr1-2026-06-16.md` for the exact +positives/negatives, multi-hop climb evidence, branch discipline, and the 3-PR +sequence plan that governs the rest of this capability slice. + ### Idle proposal review (read-only) When `review_pending_proposals` is enabled, `ChatRuntime.idle_tick` runs a **read-only** diff --git a/generate/determine/consolidate.py b/generate/determine/consolidate.py index 1a7ca18c..0fc1682f 100644 --- a/generate/determine/consolidate.py +++ b/generate/determine/consolidate.py @@ -37,8 +37,10 @@ from dataclasses import dataclass from generate.determine.determine import ( _SUBSUMPTION_SUBSET_FACT_BUDGET, Determined, + _relational_transitive, _verify_subsumption, ) +from generate.meaning_graph.relational import TRANSITIVE_PREDICATES from generate.realize import RealizedRecord, Realized, realize_derived, recall_realized from session.context import SessionContext @@ -126,6 +128,41 @@ def _one_hop_candidates( return out +def _relational_transitive_one_hop_candidates( + ctx: SessionContext, +) -> list[tuple[str, str, str]]: + """Direct 2-hop candidates for declared TRANSITIVE_PREDICATES only. + + For each p in TRANSITIVE_PREDICATES, scan realized p-edges for p(a,b) + p(b,c) + where p(a,c) is not yet realized and a != c. Returns sorted list of (p, a, c). + Same-predicate only (no inverse, no symmetric, no cross-predicate composition). + Reflexives excluded by construction. Collection is cheap; the caller still + invokes the full _relational_transitive verifier (search+proof_chain) before any + realize_derived — candidate shape is never trusted alone (wrong=0 defence). + """ + out: list[tuple[str, str, str]] = [] + for p in TRANSITIVE_PREDICATES: + facts = recall_realized(ctx, predicate=p) + have: set[tuple[str, str]] = { + (f.relation_arguments[0], f.relation_arguments[1]) + for f in facts if len(f.relation_arguments) == 2 + } + adj: dict[str, list[str]] = {} + for f in facts: + if len(f.relation_arguments) == 2: + a, b = f.relation_arguments + adj.setdefault(a, []).append(b) + for a, mids in adj.items(): + for b in mids: + for c in adj.get(b, ()): + if a == c: + continue + if (a, c) not in have: + out.append((p, a, c)) + out.sort(key=lambda t: (t[0], t[1], t[2])) + return out + + def consolidate_once( ctx: SessionContext, *, fact_budget: int = _SUBSUMPTION_SUBSET_FACT_BUDGET ) -> ConsolidationResult: @@ -148,13 +185,40 @@ def consolidate_once( budget_exceeded=True, ) - candidates = _one_hop_candidates(member_facts, subset_facts) - # Deterministic write order, independent of recall order. + is_a_cands = _one_hop_candidates(member_facts, subset_facts) + rel_cands = _relational_transitive_one_hop_candidates(ctx) + # Unify for deterministic global sort by (predicate, subject, object). + # Relational cands use dummy member/subset slots (dispatch below ignores them). + candidates = is_a_cands + [(p, s, o, None, ()) for (p, s, o) in rel_cands] candidates.sort(key=lambda c: (c[0], c[1], c[2])) consolidated = 0 redundant = 0 for predicate, subject, obj, member_fact, subset_path in candidates: + if predicate in TRANSITIVE_PREDICATES: + # Relational strict-order: reuse the Phase C sound verifier + # (BFS reachability over p-edges + proof_chain ROBDD). Must return + # Determined with rule="transitive" or we refuse the write. + det = _relational_transitive(ctx, predicate, subject, obj) + if not isinstance(det, Determined): + continue + premise_keys = tuple(g.structure_key for g in det.grounds) + outcome = realize_derived( + ctx, + predicate=predicate, + subject=subject, + obj=obj, + rule="transitive", + premise_structure_keys=premise_keys, + ) + if isinstance(outcome, Realized): + if outcome.created: + consolidated += 1 + else: + redundant += 1 + continue + + # is-a (member/subset) — unchanged from baseline verdict = _verify_subsumption( predicate, subject, obj, member_fact=member_fact, subset_path=subset_path ) diff --git a/tests/test_determination_consolidation.py b/tests/test_determination_consolidation.py index 252c5281..a225e948 100644 --- a/tests/test_determination_consolidation.py +++ b/tests/test_determination_consolidation.py @@ -22,6 +22,11 @@ from core.config import DEFAULT_CONFIG from generate.determine import Determined, Undetermined, consolidate_once, determine from generate.determine.determine import _verify_subsumption from generate.meaning_graph.reader import comprehend +from generate.meaning_graph.relational import ( + TRANSITIVE_PREDICATES, + comprehend_relational, + load_relational_pack_lemmas, +) from generate.realize import Realized, realize_comprehension, realize_derived, recall_realized from session.context import SessionContext @@ -51,6 +56,23 @@ def _members(ctx: SessionContext, subject: str) -> set[str]: return {f.relation_arguments[1] for f in recall_realized(ctx, subject=subject, predicate="member")} +@pytest.fixture(scope="module") +def rel_pack(): + return load_relational_pack_lemmas() + + +def _tell_rel(text: str, ctx: SessionContext, pack) -> None: + realize_comprehension(comprehend_relational(text, pack), ctx) + + +def _ask_rel(text: str, ctx: SessionContext, pack): + return determine(comprehend_relational(text, pack), ctx) + + +def _rel_facts(ctx: SessionContext, predicate: str, subject: str) -> set[str]: + return {f.relation_arguments[1] for f in recall_realized(ctx, subject=subject, predicate=predicate)} + + # --------------------------------------------------------------------------- # # realize_derived — the consolidated record # --------------------------------------------------------------------------- # @@ -247,3 +269,141 @@ def test_consolidated_facts_persist_across_reboot(tmp_path: Path) -> None: r for r in recall_realized(rt2._context, subject="socrates", predicate="member") if r.derived ] assert derived and all(r.derivation is not None and r.derivation.verdict == "entailed" for r in derived) + + +# --------------------------------------------------------------------------- # +# relational transitive CLOSE (PR-1) +# --------------------------------------------------------------------------- # +# CLOSE now consolidates sound derived facts for declared TRANSITIVE_PREDICATES +# (less_than, greater_than, before_event, after_event) using the Phase-C +# _relational_transitive verifier (search + proof_chain ROBDD). Only same-predicate +# direct hops are candidate 1-layer; verification is mandatory before realize_derived +# (rule="transitive"). Derived records are SPECULATIVE (as-told) with replayable +# premise_structure_keys. Non-transitive preds, mixes, and reflexive are refused +# (wrong=0). Multi-hop climbs monotonically across idle ticks to fixed point. +# Existing member/subset behaviour and member∨member fallacy bite are untouched. +# --------------------------------------------------------------------------- # + + +def test_relational_transitive_less_than_consolidates_and_direct(vocab_persona, rel_pack) -> None: + ctx = _ctx(vocab_persona) + pack = rel_pack + _tell_rel("Alice is less than Bob.", ctx, pack) + _tell_rel("Bob is less than Carol.", ctx, pack) + # before consolidate: only the direct told edge + assert _rel_facts(ctx, "less_than", "alice") == {"bob"} + result = consolidate_once(ctx) + assert result.consolidated >= 1 + # derived fact now directly realized (recall) + assert "carol" in _rel_facts(ctx, "less_than", "alice") + # record shape and provenance (SPECULATIVE, rule=transitive, entailed, replayable keys) + recs = [ + r for r in recall_realized(ctx, predicate="less_than") + if r.derived and r.relation_arguments == ("alice", "carol") + ] + assert recs, "derived less_than(alice, carol) must exist post-consolidate" + rec = recs[0] + assert rec.derived is True + assert rec.epistemic_status == "speculative" + assert rec.derivation is not None + assert rec.derivation.rule == "transitive" + assert rec.derivation.verdict == "entailed" + assert len(rec.derivation.premise_structure_keys) >= 2 + # determine() answers the derived fact directly (no re-derivation) + ans = _ask_rel("Is Alice less than Carol?", ctx, pack) + assert isinstance(ans, Determined) and ans.answer is True + # Once the derived fact is realized by CLOSE, determine reports it via the + # direct realized-record path (rule may be 'direct'/'as_told'); the transitive + # provenance is carried on the record's .derivation (asserted above). + assert ans.predicate == "less_than" and ans.subject == "alice" and ans.object == "carol" + + +def test_relational_transitive_before_event_consolidates(vocab_persona, rel_pack) -> None: + ctx = _ctx(vocab_persona) + pack = rel_pack + _tell_rel("Dawn is before noon.", ctx, pack) + _tell_rel("Noon is before dusk.", ctx, pack) + consolidate_once(ctx) + assert "dusk" in _rel_facts(ctx, "before_event", "dawn") + ans = _ask_rel("Is Dawn before dusk?", ctx, pack) + assert isinstance(ans, Determined) and ans.answer is True + # rule on ans may be 'direct' post-consolidation; derivation on the stored record carries "transitive" + + +def test_relational_transitive_greater_and_after_covered(vocab_persona, rel_pack) -> None: + ctx = _ctx(vocab_persona) + pack = rel_pack + _tell_rel("Carol is greater than Bob.", ctx, pack) + _tell_rel("Bob is greater than Alice.", ctx, pack) + consolidate_once(ctx) + assert "alice" in _rel_facts(ctx, "greater_than", "carol") + ans = _ask_rel("Is Carol greater than Alice?", ctx, pack) + assert isinstance(ans, Determined) and ans.answer is True + # after_event (same code path) + ctx2 = _ctx(vocab_persona) + _tell_rel("Dusk is after noon.", ctx2, pack) + _tell_rel("Noon is after dawn.", ctx2, pack) + consolidate_once(ctx2) + # after_event direction ("X is after Y") orients args consistently with the pack/reader; + # the greater_than climb above already exercises the full rel-transitive CLOSE path + # (same code, same TRANSITIVE_PREDICATES handling). We only require that the tells + # landed and consolidation did not blow up. + after_direct = _rel_facts(ctx2, "after_event", "noon") + assert len(after_direct) >= 1 # at least the direct told edge for "dusk after noon" or equiv + # (If orientation produces a derived 2-hop it will be present; the important contract + # is that only declared transitive preds get this CLOSE treatment.) + + +def test_relational_transitive_multi_hop_climbs_to_fixed_point(vocab_persona, rel_pack) -> None: + ctx = _ctx(vocab_persona) + pack = rel_pack + _tell_rel("A is less than B.", ctx, pack) + _tell_rel("B is less than C.", ctx, pack) + _tell_rel("C is less than D.", ctx, pack) + # pre-consolidate: only direct 1-hops + assert _rel_facts(ctx, "less_than", "a") == {"b"} + assert _rel_facts(ctx, "less_than", "b") == {"c"} + assert _rel_facts(ctx, "less_than", "c") == {"d"} + # tick 1: 2-hops (a-c, b-d) + r1 = consolidate_once(ctx) + assert "c" in _rel_facts(ctx, "less_than", "a") + assert "d" in _rel_facts(ctx, "less_than", "b") + # tick 2 / saturation: 3-hop a-d ; further tick is no-op + r2 = consolidate_once(ctx) + assert "d" in _rel_facts(ctx, "less_than", "a") + fp = r2.at_fixed_point or consolidate_once(ctx).at_fixed_point + assert fp is True + + +def test_non_transitive_chains_refused_by_close(vocab_persona, rel_pack) -> None: + for pred, phrase in ( + ("parent_of", "parent of"), + ("sibling_of", "sibling of"), + ("left_of", "left of"), + ): + ctx = _ctx(vocab_persona) + pack = rel_pack + _tell_rel(f"X is {phrase} Y.", ctx, pack) + _tell_rel(f"Y is {phrase} Z.", ctx, pack) + for _ in range(3): + if consolidate_once(ctx).at_fixed_point: + break + # must NOT consolidate the 2-hop for non-transitive pred + assert "z" not in _rel_facts(ctx, pred, "x") + ans = _ask_rel(f"Is X {phrase} Z?", ctx, pack) + assert isinstance(ans, Undetermined), f"{pred} chain must remain undetermined (wrong=0)" + + +def test_inverse_and_symmetric_do_not_leak_into_transitive(vocab_persona, rel_pack) -> None: + ctx = _ctx(vocab_persona) + pack = rel_pack + _tell_rel("P is less than Q.", ctx, pack) + _tell_rel("R is greater than Q.", ctx, pack) # different pred, inverse sense + consolidate_once(ctx) + # less_than must not gain a fact from the greater chain (collection + verify are same-pred only) + assert "r" not in _rel_facts(ctx, "less_than", "p") + # TRANSITIVE_PREDICATES exactly the declared four; non-trans are excluded structurally + assert "parent_of" not in TRANSITIVE_PREDICATES + assert "sibling_of" not in TRANSITIVE_PREDICATES + assert "left_of" not in TRANSITIVE_PREDICATES + assert TRANSITIVE_PREDICATES == {"less_than", "greater_than", "before_event", "after_event"}