Commit graph

12 commits

Author SHA1 Message Date
Shay
f4afb34cb9
feat(proposals): bridge derived CLOSE facts into review proposals (#789)
* test(proposals): cover derived CLOSE proposal bridge

- Flag-off and emission for member/subset + relational transitive derived facts.
- Stable dedupe, skips for non-derived/malformed/unsupported.
- No status upgrade, no corpus side-effects.
- Runtime flag wiring smoke (consolidate + bridge on → emits after idle_tick).
- Re-runs of PR-1 tests + invariants stay green.

* feat(proposals): emit review-gated proposals from derived CLOSE facts

- New focused emitter generate/determine/derived_close_proposals.py:
  - collect eligible derived (member/subset + TRANSITIVE) with entailed Derivation + SPECULATIVE.
  - deterministic sort + stable dedupe key (predicate+args+derivation+structure_key).
  - write proposal-only artifacts (source=derived_close_fact) to dedicated sink.
  - best-effort, counts returned, safe skips.
- RuntimeConfig: review_derived_close_proposals (default False), documented.
- ChatRuntime.idle_tick: after consolidation (when flag on), call emitter best-effort (no did_work, no engine checkpoint).
- IdleTickResult: new field derived_close_proposals_emitted (additive, documented).
- No change to existing proposal_review contract or comprehension-failure sink.
- No serving/determine side-effects.

* docs(proposals): document derived CLOSE proposal bridge

- docs/runtime_contracts.md: new subsection under idle passes describing eligibility,
  contract (proposal-only, review-gated, default-off, no corpus/COHERENT/serving change),
  and cross-ref to the analysis note.
- New dated analysis note with why (flywheel bridge after PR-1), architecture/boundaries,
  artifact schema, dedupe, tests, non-goals, and composition with PR-1/PR-3.
- Tiny high-level pointer not added (no suitable learning-loop section in README at this granularity).

* fix(proposals): harden derived CLOSE proposal emission
2026-06-16 15:39:46 -07:00
Shay
a1bdaa2ce5
feat(determine): consolidate declared relational transitive CLOSE facts (#788)
* 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.
2026-06-16 15:15:59 -07:00
Shay
ba05ebb0cd
feat(frame-verdict): closed-world FrameVerdict substrate — PR-1..4 + hardening (ADR-0222 B4) (#787)
* wip(b4): lift _basis to generate/epistemic_basis.py (behavior-preserving)

B4 PR-1 foundation checkpoint — the shared epistemic-basis helper extracted
byte-identically from determine.py so the closed-world frame_verdict evaluator
(coming) can compute standing without importing determine (ADR-0222 §8 A3).
determine.py imports it aliased; its 3 Determined sites + INV-30 unchanged.
PAUSED: rest of B4 (FrameVerdict type, evaluator, INV-31, PR-2/3/4) resumes
after the suite-speed arc.

* feat(frame-verdict): closed-world envelope + isolated evaluator + INV-31 (B4 PR-1)

The sealed, off-serving FrameVerdict type + the isolated text-frame evaluator + the
INV-31 firewall (ADR-0222). Composes proof_chain.entail (no second prover); a
closed-world False comes ONLY from an ROBDD refutation; absence is never false.

- generate/frame_verdict/{types,evaluate,__init__}: FrameVerdict / ClosedFrame /
  ClosedWorldProof + PositiveRefutationKind enum. evaluate_frame_verdict(frame, query)
  maps entail ENTAILED/REFUTED/UNKNOWN/REFUSED -> entailed_true/false/undetermined/
  contradiction/scope_boundary; OPEN / undeclared-closure / non-TEXT -> scope_boundary.
  __post_init__ admissibility: entailed_false needs a NAMED positive refutation; a
  generic FALSIFIED raises. trace_hash is order-invariant + replay-stable.
- INV-31 (test_architectural_invariants.py): A1 determine.py clean+visible; A2 exact
  construction allowlist (evals-inclusive, tests-excluded) + non-vacuity anchor; A3
  transitive spine -/-> frame_verdict (reuses INV-27 walker) + resolve anchor; B1
  determine() refuses a ClosedFrame. B2 deferred to the governance slice (no
  non-vacuous surface yet; ADR §8 permits).

No serving wire. determine.py unchanged except the _basis import. No Determined(answer=False).
INV-30 green. Shapes follow the B4 operator master brief (PositiveRefutationKind enum,
closure_declared/source/provenance) — a consistent refinement of ADR-0222 §3.

Verified: 97 (full INV incl. INV-31 + FrameVerdict + OWA floor) + 20 frame_verdict + 35 determine.

* feat(frame-verdict): text closed-world (CWA) evaluation lane (B4 PR-2)

A measure-only lane over the text FrameVerdict evaluator (ADR-0222). Proves the sealed
type evaluates propositional closed frames safely — incl. a sound entailed_false —
without touching determine() or runtime serving.

- evals/frame_verdict_text_cwa/: cases.jsonl (12 cases across all 5 verdict kinds +
  gating + absence safety), oracle.py (an INDEPENDENT truth-table propositional checker —
  own recursive-descent parser + brute-force enumeration, disjoint from the ROBDD; imports
  no engine module), score.py, README.
- tests/test_frame_verdict_text_cwa_lane.py: wrong=0; the disjoint oracle confirms every
  gold (non-vacuity) AND the engine matches the oracle on every case; entailed_false is
  proof-backed (ROBDD_REFUTATION); absence / OPEN / undeclared-closure are never
  entailed_false; SHA-pinned fixtures.

Input contract: propositional-formula strings (no prose lowering). Capability-index
deliberately NOT touched (off-serving lane; documented). No Determined, no answer=False,
no serving wire. INV-30 / INV-31 / ProofWriter-OWA stay green.

* feat(frame-verdict): perception changed-slot falsification adapter (B4 PR-3)

Lift an ADR-0211 FalsificationRun into a FrameVerdict SAFELY (ADR-0222 §5.2). Critical
doctrine: "FALSIFIED" is not enough — only a POSITIVELY observed changed-slot contradiction
produces entailed_false (PERCEPTION_CHANGED_SLOT). Missing observation (absence), unexpected
extra (over-observation), and a whole-missing actual frame NEVER become false — they refuse
(undetermined / scope_boundary). SUPPORTED -> entailed_true (frame-conformance proven).

- generate/frame_verdict/perception_adapter.py: frame_verdict_from_perception_falsification;
  the proof carries the FULL run trace_hash (binds expected+actual+verdict, ADR §5.4).
- generate/frame_verdict/_construct.py: extracted the single FrameVerdict builder; the text
  evaluator + perception adapter both funnel through it, so the literal FrameVerdict(...)
  lives in ONE file -> INV-31 ALLOWED_FRAME_VERDICT_SITES = {_construct.py}.
- tests: changed-slot -> entailed_false (+ empty-hash raises); missing/unexpected/whole-missing
  never false; supported -> entailed_true; non-perception -> scope_boundary.

Off-serving; perception_adapter is in generate.frame_verdict, so INV-31 A3 already proves it
unreachable from the open-world spine. No determine() change, no answer=False. INV-30 / INV-31
/ ProofWriter-OWA / text-CWA lane stay green.

* feat(response-governance): default-dark FrameVerdict surface mapping (B4 PR-4)

The only lawful surface path for a closed-world verdict (ADR-0222 §7/§14). Lowers a
FrameVerdict to a served disposition through the EXISTING epistemic_disclosure tables (no
parallel object): entailed_true/false -> COMMIT at INFERRED + DisclosureClaim.NONE (a
committed "Yes"/"No"; entailed_false is an answer, NOT a contradiction/refusal/LimitationKind);
contradiction -> REPORT; undetermined -> REFUSE; scope_boundary -> EXPLAIN.

DEFAULT-DARK: a NEW module that changes no existing file — the open-world govern_response /
shape_surface STRICT path is byte-identical, and nothing in the live runtime calls it. The
TYPE is the closed-world tag: a forged dict / untagged object cannot widen serving (raises).

INV-31: A3 still green — core/response_governance/frame_verdict.py is NOT imported by the
package __init__ or the open-world spine, so frame_verdict stays unreachable from
chat/runtime/session/vault. The B2 anchor is now live (the forged-object rejection); all six
INV-31 anchors firm. The open-world render_determination cannot render a FrameVerdict;
determine() still has no answer=False.

Verified: 84 (governance + full INV incl. INV-31 A3/B2) green.

* harden(frame-verdict): fold in adversarial-review findings (B4)

A 4-skeptic adversarial read of PR-1..4 against real source surfaced one
soundness gap (major) and four defensive gaps (minor). All folded in; the
4 B4 files + full INV suite stay green (128 passed).

S1 (major) — perception negation was not frame-gated. The text evaluator
refuses OPEN / undeclared-closure frames (-> SCOPE_BOUNDARY) but the
perception adapter only gated frame_kind + the missing-frame sentinel, so a
PERCEPTION + OPEN + changed-slot residual produced entailed_false with
world_assumption=OPEN — a verdict that self-contradicts the type invariant
(OPEN => negation illegal). Fixed two ways:
  * perception_adapter: gate OPEN / not-closure_declared -> SCOPE_BOUNDARY,
    mirroring the text evaluator (graceful upstream refusal);
  * types.__post_init__ §(0): STRUCTURAL backstop — ENTAILED_FALSE + OPEN
    raises, frame-general, so NO producer (text/perception/future) can emit
    an OPEN-world negation even if it forgets the gate.

S4-a — entailed_true was admissibility-asymmetric. Only entailed_false was
proof-gated at construction; a committed "Yes." leaned entirely on the
INV-31-A2 allowlist. Added a symmetric §(2) guard: entailed_true requires a
positive entailment/support proof (proof_chain.entail/ENTAILED or
sensorium.falsification/SUPPORTED), non-empty sha, and NO refutation kind —
a mutation test can now trip a forged positive.

S2 — A2 construction detector extended to flag FrameVerdict.<factory>(...)
classmethod constructions and module-qualified mod.FrameVerdict(...), so a
future alternate constructor cannot evade ALLOWED_FRAME_VERDICT_SITES. The
dataclasses.replace gap is RECORDED (a blanket replace() match would
false-positive tree-wide) for the serving-wiring PR, not faked.

S4-b/c — A3 firewall now bars core.response_governance.frame_verdict
DIRECTLY (not only via its re-import of generate.frame_verdict), plus a new
test proving the response_governance package __init__ stays default-dark
(does not re-export the adapter).

S3 — oracle grammar is a strict SUBSET of proof_chain.entail (it mis-parses
`false` as a free atom). Corrected the docstring and added a lane guard:
every DECIDED cases.jsonl formula must stay inside the subset, so a future
out-of-subset case fails loudly at SHA-add review instead of as a confusing
engine-vs-oracle red. SCOPE_BOUNDARY-gold garbage is exempt (both refuse).

S1-minor (construction-time-only admissibility) documented in __post_init__:
a future codec/deserialization path must re-construct via build_frame_verdict.

* docs(analysis): B4 FrameVerdict implementation lookback (PR-1..4 + hardening)

Mandatory multi-slice lookback (CLAUDE.md triggers 2+3). Audits all six B4
commits across the lookback template: documentation drift, test-coverage /
parity gaps, wrong=0 hazard surface, cross-slice consistency, honest LOC.

Categorized findings: solid (INV-30 untouched; entailed_false positive-only;
INV-31 firewall non-vacuous; default-dark; replay determinism) / hazards (the
5 adversarial-review findings, ALL fixed in the hardening commit) / recorded
gaps (dataclasses.replace A2 hole + construction-time-only admissibility,
both deferred with an explicit guard obligation on the serving-wiring PR) /
drift (type shapes are a consistent refinement of ADR-0222 §3; one non-gating
ADR note filed). Global red-line ledger: all green.
2026-06-16 06:23:03 -07:00
Shay
1ff06726a6
feat(determine): add transitive strict-order relational inference (#781)
* feat(determine): add transitive strict-order relational inference

Add sound transitive closure for declared strict-order relational predicates —
less_than, greater_than, before_event, after_event, and ONLY these. A query
p(a, c) determines True when a same-predicate chain p(a, b), p(b, c), ... over the
predicate's OWN realized edges is found (BFS reachability) and the proof_chain ROBDD
verifies the transitive entailment (search-then-verify, through the UNCHANGED
evaluate_entailment via a new lower_transitive_chain). Mirrors _determine_subsumption.

Scope / firewall:
- TRANSITIVE_PREDICATES is closed and default-off; sibling_of, parent_of,
  left_of/right_of, inside_of, during_event, overlaps_event are EXCLUDED.
- Same-predicate edges only — no transitive-through-inverse, no cross-predicate
  (triple firewall: recall filter + lowering re-reject + ROBDD re-verify).
- Open-world: asserts only answer=True via the shared _relational_determined
  surface (rule="transitive"), so INV-30 stays at exactly 3 Determined sites and
  no answer=False is added. One-hop inverse/symmetric (#775) is unchanged.
  FrameVerdict / closed-world (ADR-0222) is untouched.

wrong=0 bite (unit + lane + independent oracle): non-transitive-predicate chains,
non-admitted spatial chains, mixed-predicate chains, disjoint chains, reflexive
cycles, and inverse+transitive composition all REFUSE.

Measurement: new evals/relational_transitive lane with an INDEPENDENT BFS
transitive-closure oracle (imports no engine module; INV-25/27), cross-checked both
directions (positives oracle-True, confusers oracle-False). Capability-index breadth
10 -> 11, wrong_total 0, deterministic digest re-frozen.

Cross-PR reconcile: migrated the one-hop confuser rinf-ref-001 (a less_than chain,
which now correctly determines transitively) to a B2 positive; repurposed its unit
test to a non-transitive parent_of chain; corrected a pre-existing stale breadth==9
assertion (#775 added a 10th domain but never updated test_capability_index).

Verified in the worktree: determine + transitive/one-hop lanes + capability
baseline/index + ProofWriter-OWA floor + INV-30/29/21/02 + full smoke — all green.
A 3-skeptic read-only adversarial review found no wrong=0 leak.

* test(determine): B2 hardening — TRANSITIVE_PREDICATES pin + lower_transitive defensive + budget

Add the required B2 hardening tests before merge:

- test_transitive_predicates_closed_and_excludes: the table is EXACTLY
  {less_than, greater_than, before_event, after_event}, every member is in
  RELATIONAL_PREDICATES, and every deliberately-excluded predicate (sibling_of,
  spouse_of, parent_of, child_of, left_of, right_of, inside_of, during_event,
  overlaps_event) is explicitly absent. (Closes the gap where relational.py's
  comment claimed this test existed but it did not.)

- tests/test_composition_lower_transitive.py: direct defensive tests on
  lower_transitive_chain — empty path, mislabeled (cross-predicate) edge, wrong
  arity, non-contiguous path, and path-not-reaching-target all lower to None
  (refuse); plus exact 2-hop and 3-hop theory pins.

- test_edge_budget_exhaustion_refuses: above _TRANSITIVE_EDGE_BUDGET the transitive
  search declines (a safe coverage refusal), never proves.
2026-06-15 14:20:30 -07:00
Shay
6f70e834ff
feat: one-hop sound relational entailment (inverse/symmetric) + capability-index lane (#775)
* feat(determine): one-hop sound relational entailment — inverse/converse + symmetric

Mastery-v2 Step 3 lead capability (core). DETERMINE could perceive relational
structure (16 predicates, breadth-complete) but could not derive the simplest
entailed relational facts — it read only the stored direction. This adds two
SOUND one-hop rules that read a stored edge in its other lawful direction:

  INVERSE/converse   greater_than(a,b)  <=  told less_than(b,a)
  SYMMETRIC          sibling_of(b,a)    <=  told sibling_of(a,b)

Strictly scoped (per review): OPEN-WORLD (asserts only True, never False — the
answer=False path stays unbuilt, INV-30's firewall holds), ONE hop (NO transitive
chaining), DECLARED rules only. Ontology/metadata-driven, not prose intuition:

- generate/meaning_graph/relational.py: declarative algebra tables — _INVERSE_PAIRS
  (the converse edges; the pack carries no inverse metadata) + INVERSE_OF (derived,
  an involution) + SYMMETRIC_PREDICATES (mirrors the pack's graph.edge.symmetric tag).
  load_relational_pack_symmetric() reads the pack ontology; a test pins the constant
  equal to it (no silent divergence).
- generate/determine/determine.py: _relational_one_hop() between direct entailment
  and transitive subsumption; new Determined.rule provenance field (direct/inverse/
  symmetric/subsumption) — replay-safe (render reads only basis; trace hashes surface).

wrong=0 confuser block proves the rule cannot over-fire: less_than is not
self-inverse, sibling_of does not imply parent_of, greater_than does not imply
equal_to, NO transitive chain (direct or through-inverse), and no answer=False is
ever emitted. An obsolete pin (test_symmetric_converse_is_not_faked, which asserted
the pre-rule direct-only floor) is updated to the new sound behavior and a preserved
asymmetric-converse bite.

Tests: test_determine_relational_inference.py (13, the capability contract) +
updated test_relational_reader.py. Broad relational/determine/grounding +
capability_index baseline sweep: 114 green; baseline digest UNCHANGED (this is a
determination capability; the comprehension lanes are untouched).

REMAINING for the full lead PR (next): the measurement lane — an independent-oracle
evals/relational_inference lane + a capability_index adapter + baseline re-freeze
(breadth 9->10, wrong_total still 0), so the capability registers on the yardstick.

INTEGRATION NOTE (cross-PR): this adds 2 Determined() construction sites (now 4:
direct/inverse/symmetric/subsumption, ALL answer=True). When rebased onto main with
INV-30 (PR #770), update INV-30's test_determine_construction_sites_are_visible count
2 -> 4 and confirm all four assert True. Merge order: #770 -> this.

* feat(capability-index): relational-inference lane — breadth 9->10, wrong=0

Mastery-v2 Step 3 lead, measurement half. Puts the one-hop relational-inference
capability ON the capability index with an independent-oracle lane:

- evals/relational_inference/v1/: cases.jsonl (13 positive: 8 inverse + 5 symmetric,
  authored from the relation algebra INDEPENDENTLY of determine/relational per
  INV-25/27), refusals.jsonl (8 confusers that MUST refuse), provenance.md (incl. the
  honest overlaps_event reader-surface coverage gap).
- evals/comprehension/relational_inference_runner.py: told fact(s) -> determine(query)
  vs gold; refusal = coverage miss, disagreement = wrong (structurally 0 on positives).
- evals/capability_index/adapters.py: comprehension_relational_inference_result added
  to ADAPTERS.
- baseline.json re-frozen: breadth 9 -> 10, capability_score 0.94403 -> 0.949483,
  wrong_total still 0, digest deliberately changed (35dea2b2...).
- tests/test_relational_inference_lane.py: SHA-pinned gold, positive wrong=0 +
  coverage>0, and the confuser wrong=0 BITE (every confuser must refuse).

Also reconciles INV-30 (now in main via #770): determine.py grew from 2 to 3
Determined() construction sites (direct, the shared relational one-hop constructor,
transitive subsumption) — ALL answer=True. test_determine_construction_sites_are_visible
updated 2 -> 3 (correcting the prior commit note's overcount of 4; inverse and symmetric
share the single _relational_determined constructor, so it is ONE new site).

Also fixes a .gitignore gap: ADR-0219 gen-dir checkpoints (engine_state/current,
engine_state/gen-*/) were not ignored (only the old flat engine_state/*.json patterns
were), so runtime checkpoints could be committed by accident.

Verification: new lane 13/0/0 coverage 1.0; capability_baseline digest matches the
re-freeze; INV-30 + architectural invariants green; smoke 99/99.

* docs+test: reconcile stale relational-inference docstrings; assert rule provenance (review #775)

Addresses two review-requested cleanups on #775:

1. Stale docstrings. generate/meaning_graph/relational.py said the symmetric converse
   is "a sound-but-incomplete refusal at DETERMINE" and there is "NO transitive/
   symmetric/rule inference"; generate/determine/determine.py said "symmetric-converse
   questions are Undetermined", "no transitive/symmetric/rule inference", and "asserts
   only answer=True on a direct hit". All false after the one-hop relational algebra
   landed. Updated: the reader does direct-reading only; DETERMINE applies declared
   one-hop inverse/converse + pack-declared symmetric (plus the existing member/subset
   subsumption), still open-world / never answer=False; transitive relational closure,
   negation, and closed-world falsehood remain out of scope.

2. Rule-provenance gold now meaningful. The relational_inference runner compared only
   (answer, predicate, subject, object), ignoring res.rule though the gold carries
   "rule": "inverse"/"symmetric". Added res.rule to the got/gold tuple so a "right
   answer via the wrong rule path" can no longer pass silently. Lane still 13/0/0;
   baseline counts (and digest) unchanged.

Verification: runner 13/0/0; lane + capability_baseline + unit + INV-30 green (22).
2026-06-15 11:39:41 -07:00
Shay
0711988b67 feat(composition): M1 — extract the logic is-a chain into a plan->lower->verify spine (byte-parity)
First phase of the domain-general compositional reading layer (the comprehension
coverage wall is composition — docs/analysis/comprehension-coverage-wall-map-2026-06-14.md).
M1 is a pure PARITY refactor on the flagship logic path, no new capability:

- new generate/composition/ package: LogicChainPlan (plan.py) + lower_logic_chain
  (lower_logic.py), the is-a chain lowering extracted BYTE-IDENTICALLY from
  determine.py::_verify_subsumption.
- _verify_subsumption now builds a plan -> lowers it -> routes through the UNCHANGED
  evaluate_entailment gate. The composer proposes structure; the sound ROBDD gate
  remains the sole wrong=0 firewall.
- only the logic instantiation ships; no math lowering, no join-op vocabulary
  (defer-substrate-vocab-commitment — the chain discriminates on its relational
  predicate, an explicit join-op field lands when a second op dispatches on it).

Verification: byte-identical lowering (3-reviewer adversarial panel: byte-parity PASS
char-for-char, wrong=0 PASS — the instance-of-fallacy refusal mutation-proven
load-bearing); 5 new non-vacuous lowering tests; 28 determine/transitive/consolidation
+ 163-test broad sweep (incl. gsm8k serving + ADR-0218) green; cognition eval 100%.
2026-06-14 15:42:24 -07:00
Shay
7cb826a548 feat(determine): calibrated disclosed estimation — the engine earns the right to guess (Step E)
The final AGI-spine step (A INSTRUMENT → B WIRE → C DEEPEN → D CLOSE → E ESTIMATION).
The engine may now SERVE a DISCLOSED estimate for a query it would otherwise refuse —
but only for a predicate-class that has measured itself reliable, and never as fact.

This executes the ADR-0206 §5 cognition-path widening: the bridge's LICENSE node
(reliability_gate.license_for), previously "built — not yet called from serving", is now
called. govern_response returns APPROXIMATE iff a genuine licensed Action.SERVE
LicenseDecision is passed (STRICT for every other input — so every existing serving call
site is byte-identical); shape_surface DISCLOSES the estimate as "[approximate] …".

Mechanism:
- generate/determine/estimate.py — a BLIND converse-guesser: told p(a,b), asked p(b,a),
  it commits the converse. It never reads the pack's symmetry metadata; whether the guess
  is right is MEASURED, not assumed.
- evals/determination_estimation/ — the gold lane: run_practice (sealed, ADR-0199) folds
  the converse-guesser over symmetric (sibling_of) vs directed (parent_of) cases, scored
  against the pack's graph.edge.symmetric truth (gold independent of the solver). The gate
  DISCRIMINATES: sibling_of earns SERVE (660 correct → Wilson floor 0.990046 ≥ θ_SERVE),
  parent_of does not (660 wrong → 0.0). The license is earned by VOLUME — 657 perfect
  commits is the exact θ_SERVE=0.99 threshold (656 is below).
- generate/determine/data/estimation_ledger.json — the ratified committed ledger,
  hash-verified on load (a hand-edited ledger raises RatifiedLedgerError); it IS the
  deterministic sealed-practice output (a GSM8K-style --check test pins this).
- chat/runtime.py — when a converse query is refused and the class holds a SERVE license,
  the disclosed estimate is surfaced through the bridge (gated by config.estimation_enabled,
  default OFF; only meaningful with accrue_realized_knowledge).

Invariants:
- wrong=0 by construction — an estimate is ALWAYS disclosed ([approximate]), never a silent
  commit (UNVERIFIED_POSSIBLE is never in APPROXIMATE's admissible set), and only a genuine
  ratified license widens (a forged {"licensed":True} dict / a PROPOSE license / an
  unlicensed SERVE all stay STRICT). Defense-in-depth: type-gate ∧ admissible-set ∧
  hardcoded disclosed state.
- never self-authored — ceilings stay at safe defaults (θ_SERVE=0.99); the engine cannot
  raise its own bar. The ledger is sealed practice, hash-verified.
- session/serving only — no corpus/pack/identity/proposal/vault mutation; the HITL teaching
  path is untouched. Deterministic; no clock/random.
- byte-identical for every non-E turn (the 2643 govern_response call passes no license).

Out of scope (separate ADR-0206 §5 PRs): the math-serving seam (select_self_verified,
touches the sealed metric), SITUATE (stakes), and the live FEED-BACK loop.

Verified green: smoke (90), architectural invariants (56), response_governance (321,
incl. the new license-gated widening test), the determination-estimation lane (12), and
the B/D/determine regression net. Four-lens adversarial review (disclosure/wrong=0,
calibration integrity, byte-identity, boundary/determinism): all held. Design:
docs/analysis/E-estimation-design-2026-06-06.md.
2026-06-06 13:49:07 -07:00
Shay
8edafd04ac feat(determine): idle deductive consolidation — the loop learns from determined facts (Step D)
CLOSE the autonomous-loop spine: when idle, the engine consolidates each
soundly-derived determination back into the held self, so the next determine()
reaches it directly and can chain one hop further. The directly-answerable set
climbs monotonically across idle ticks to the deductive-closure fixed point.

Mechanism — generate/determine/consolidate.py::consolidate_once runs ONE
semi-naive layer of the member/subset deductive closure (member∘subset → member,
subset∘subset → subset; NEVER member∘member — instance-of is not transitive).
Each one-hop conclusion not yet realized is VERIFIED by the sound+complete
proof_chain ROBDD (reusing C's single verifier _verify_subsumption) and written
back via generate/realize::realize_derived as a SPECULATIVE realized record
carrying derived-provenance (premise structure_keys + rule + the ENTAILED
verdict). idle_tick gains a consolidation pass gated by the new
config.consolidate_determinations (default OFF); IdleTickResult.facts_consolidated
reports the layer.

Invariants held:
- wrong=0 — every consolidated fact is a sound-rule conclusion confirmed by the
  sound+complete decider; member∘member is structurally unreachable (a member fact
  is only ever extended by a subset edge). _verify_subsumption now refuses a
  mislabeled/wrong-arity path (belt-and-suspenders now that consolidation is a
  second caller), so the fallacy cannot be laundered through a corrupted chain.
- honesty — a fact derived from SPECULATIVE premises stays SPECULATIVE / as-told;
  the soundness of the inference never upgrades the standing of the premises.
  COHERENT is never minted.
- teaching-safety — SESSION memory (immediate), an extension of the realize path;
  NOT corpus mutation and NOT coupled to proposals. The HITL path is untouched.
- determinism/replay — pure function of the realized set; sorted write order;
  derived structure_key identical to a told fact's; provenance round-trips through
  the Shape B+ snapshot (consolidated facts resume the SAME life across reboot).
- no new normalization — writes reuse the INV-21-allowed vault writer;
  algebra/versor.py keeps closure.

Falsification — evals/determination_closure: a frozen replay seeds a deep is-a
chain and runs idle ticks; asserts the closure climbs monotonically to a complete
fixed point (no-op final tick), wrong=0 (member∘member canary never derived, no
fabricated membership), all derived facts SPECULATIVE, and every derived record
re-verifies ENTAILED from its recorded premises.

Verified green: smoke, runtime, cognition, architectural invariants, plus the new
D unit + lane tests and the determine/realize/persistence regression net. Five-lens
adversarial review: 4 lenses held; the 5th (normalization) was a misattribution
(pre-existing vault reproject, triggered identically by the merged realize path,
on sanctioned null-vector storage). Design + findings: docs/analysis/
D-close-consolidation-design-2026-06-06.md.
2026-06-06 12:28:09 -07:00
Shay
cd1a9cbe80 feat(determine): transitive subsumption — sound is-a reasoning over accrued knowledge (Step C)
DETERMINE was one-hop. C answers a member/subset query that holds by SOUND transitive
subsumption when direct entailment misses: member∘subset* and subset∘subset (the
Description-Logic is-a rules). 'Socrates is a man. All men are mortal. Is Socrates
mortal?' -> yes, as told.

wrong=0 hazard surfaced and closed: member∘member is NOT transitive (instance-of vs
subclass-of) — 'Socrates is a man. Man is a species.' does NOT entail 'Socrates is a
species'. That rule is NEVER an edge, so the fallacy is unreachable (bite-tested). The
reader's member/subset split (X is a Y vs all Xs are Ys) is exactly the instance-of/
subclass-of distinction that makes the included rules sound.

Mechanism: SEARCH-then-VERIFY. Reachability over the sound edges finds the chain, then
the proof_chain ROBDD verifies that chain's propositional entailment (O(path) premises).
Full O(n³) grounding into proof_chain was tried and rejected: it overruns the
canonicalizer's per-conjunct recursion, and transitive closure is reachability, not
general SAT. Search-then-verify scales (11-hop chain determines in ~2ms) and keeps the
sound+complete decider as the wrong=0 verifier + proof artifact.

subset is now a supported direct-entailment predicate (a told subset(a,b) answers it);
the other categoricals (disjoint/intersects/some_not) stay excluded. Two existing tests
updated accordingly (subset->ungrounded, disjoint stays unsupported_query).
2026-06-06 11:09:41 -07:00
Shay
dc06bd5a3c feat(runtime): surface the determination — the engine answers from accrued knowledge (Step B-2)
When accrue_realized_knowledge is on and a question turn is Determined over realized
knowledge, the user-facing surface IS that answer (generate.determine.render_determination):
'Yes — as I was told, truth is a concept.' The realizer's articulation_surface is
RETAINED as evidence — the determination is a user-facing SELECTION (like the
unknown-domain gate), not a rewrite. An Undetermined turn keeps the default
articulation surface (the honest 'I don't know'); flag-off never takes this path.

Basis is rendered honestly: SPECULATIVE grounds read 'as I was told', never 'verified'
(D0 only asserts answer=True, so the surface is an affirmation — no fabricated or
asserted-False string). Selection only: no field op, no normalization, proposes no
learning (HITL untouched).

Updates docs/runtime_contracts.md selection policy + adds the contract test in the
same PR (per the surface-contract discipline).
2026-06-06 10:52:54 -07:00
Shay
aa66047b35 feat(comprehend): relational reader — binary-relation NL→structure
First consumer of en_core_relational_predicates_v1: a fail-closed sibling reader
that maps '<A> is [the] <connective> <B>' onto the pack's closed predicate
vocabulary (parent_of, less_than, left_of, before_event, ...), producing a standard
Comprehension. realize_comprehension consumes it unchanged; determine's guard widens
from the single 'member' predicate to a CLOSED direct-entailment set (member + the
ground binary relational predicates), keeping categorical/propositional predicates
soundly excluded.

Direct entailment only — no transitive/symmetric/rule inference (symmetric-converse
questions are a sound-but-incomplete refusal, never a faked assertion). Only the
predicate is closed-vocabulary; arguments may be OOV. The pack is loaded explicitly,
not default-mounted.

wrong=0 bites: reader refuses non-template/negated/pack-absent surfaces; determine
asserts only on direct entailment and excludes categorical predicates.
2026-06-06 09:32:08 -07:00
Shay
bf9ad77fda feat(determine): D0 — reason over realized structure → assert (as-told) / refuse
The honest gear (roadmap Step 4). `determine(question: Comprehension | Refusal, ctx)`
answers a membership question ("Is X a Y?") ONLY from what the held self has already
REALIZED (R1a structural recall) — never from the field, an LLM, or absence.

Honesty (from the design review): every realizable record is SPECULATIVE, and
ADMISSIBLE_AS_EVIDENCE = {COHERENT}, so a determination grounded in SPECULATIVE records
carries `basis="as_told"` — "based on what I was told (unverified)", NEVER "verified".
Until COHERENT promotion exists (out of scope), D0 produces only as-told assertions or
typed `Undetermined` refusals. No estimation; no corpus mutation (teaching stays HITL
proposal-only).

Soundness (open-world, wrong=0): D0 asserts an answer ONLY on DIRECT structural
entailment by a realized fact; absence never refutes (so it never asserts a positive
answer from missing knowledge — it refuses). It asserts only `answer=True` on a direct
hit; it never asserts False. Negated questions and non-`member` queries are an explicit
`Undetermined` — D0 ships no entailment path the reader cannot exercise.

Tests (test_determine_d0.py, 8) BITE: present-but-non-entailing (a record about the
subject exists but not the asked relation) MUST refuse; the same question against a
fresh context with no realized fact flips Determined→Undetermined (the verdict is
entailment, not mere presence); the negated + unsupported-query refusals are exercised
via hand-built queries (the reader refuses them upstream, so a comprehend-based test
would pass vacuously). Independent of #593: reasons over R0/R1 `member` facts only.
2026-06-06 06:18:55 -07:00