From 0f757fb29babd129300050a56d8593085968919d Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Mon, 12 Oct 2026 21:32:43 +0200 Subject: [PATCH 1/4] docs: specify cross-reasoner temporal ablation RFC --- ...d-temporal-ablation-reasoner-oracles-v1.md | 160 ++++++++++++++++++ 1 file changed, 160 insertions(+) create mode 100644 .claude/plans/inverted-temporal-ablation-reasoner-oracles-v1.md diff --git a/.claude/plans/inverted-temporal-ablation-reasoner-oracles-v1.md b/.claude/plans/inverted-temporal-ablation-reasoner-oracles-v1.md new file mode 100644 index 000000000..c8833b63c --- /dev/null +++ b/.claude/plans/inverted-temporal-ablation-reasoner-oracles-v1.md @@ -0,0 +1,160 @@ +# D-SAG-CF-1: Inverted temporal ablation as a cross-reasoner epistemic probe + +**Status: RESEARCH RFC / NOT AN IMPLEMENTED ADAPTER.** Parent: [#1509](https://github.com/AdaWorldAPI/lance-graph/pull/1509), the merged one-hop Software Awareness Graph (SAG). Relevant siblings: [#1496](https://github.com/AdaWorldAPI/lance-graph/pull/1496), [#1497](https://github.com/AdaWorldAPI/lance-graph/pull/1497), [#1498](https://github.com/AdaWorldAPI/lance-graph/pull/1498). Literature: [research map](../../.arxiv/2026-10_inverted_temporal_ablation_reasoner_oracles.md). Existing audit: [Gadamer ablation](../research/2026-10-recovery/GADAMER-ABLATION-RESEARCH.md). + +## 0. The question: nine dots, one hidden boundary + +What would the current conclusion, confidence, support set, future prediction and selected decision look like if an **observation**, **rule**, **interpretive method**, or **shared assumption** had never contributed? A further self-introspection experiment asks which conclusions fail when the engine suspends one of its *own* inference procedures. + +A removal from a recorded history is not an inverse update on a compressed belief. A single-edge cut is not enough to establish actual causality under overdetermination. A counterfactual belief must never be written as observed truth. + +Use factual world W0 and detached counterfactual world W_X. For a pinned horizon h, provenance closure P and common execution policy π: + + B0 = Eval(P, history<=h, π) + BX = Eval(P without contributors/dependents of X, history<=h, π) + Shadow(X) = Compare(B0, BX) + +This is initially **model-relative counterfactual dependency**, not automatically real-world causal identification. Pearl do(X) additionally requires a specified structural causal model and intervention semantics. Jøsang subjective-logic fission is a useful analogy, **not** algebraically identical to NARS revision or an inverse of CE64 F/C bytes. + +Three kinds of outputs remain distinct: changed truth/frequency and confidence; changed justification/provenance and certification; changed operational attention/choice. Record each axis separately. No claim of sentience is implied by the word introspection. + +## 1. Existing code seams and their actual limits + +| Seam | Exists | Limit / required interface | +| --- | --- | --- | +| `crates/lance-graph-planner/src/temporal.rs` | HLC/version-aware local causal trajectory deinterlacing; `QueryReference::at`, `EpistemicMode` | DATA-causal dependency closure is explicitly deferred. Default ref `u64::MAX` is **not** a pinned no-hindsight read; use a concrete head. | +| `crates/lance-graph-planner/src/chain_replay.rs` | Shared factual replay and first divergence | Replay-time truth revision can overcount shared evidence: existing Gadamer audit reports that replay_step lacks evidence-base independence guard. Do not trust it as exact retraction baseline until fixed or bracketed by an independent oracle. | +| `crates/lance-graph-planner/src/chain_counterfactual.rs` | Detached single-step cut, same replay kernel, distinct sequence range, counterfactual -6 tag; EdgeRole and threshold verdict | Only one `CutStep`; a threshold verdict can miss support changes, redundancy and joint cuts. | +| `crates/lance-graph-planner/src/pearl.rs` | Limited reason/reaction and intervention-arm comparisons | Not a general SCM do() for arbitrary graphs. Independent `crates/learning/src/scm.rs` exists but is not wired to CE64. | +| `crates/lance-graph-contract/src/revision.rs` | Gadamer claims/revision and counterfactual admission types | Nobody computes an end-to-end CounterfactualVerdict; TruthOnly is not safely equivalent to dispensable. Claim -> chain-step linkage is absent. | +| `crates/lance-graph-glove-parity/src/awareness.rs` | #1509 SAG projection with typed method/program/provenance tiers queried through Quack | In-memory and one hop; cannot silently pass a population mask between independent Quack programs. Needs a legal relation carrier or factored EqU32Via read. | +| OGAR ClassView / schema seal / MethodKey; CE64 / Epi5; mask-risc/R2IL | Existing typed registries and register/ISA interpretation contracts | Caller issues method identity. Never equate 8-bit ISA lanes with NARS fields; interpretations remain typed readings. No new opcodes or registry. | + +Do not describe all these as already connected. This proposal adds the *contract for joining them*, not a second engine. + +## 2. Minimal cross-reasoner contract + +A reasoner adapter is a **read-only export and deterministic replay boundary**. Its hot-side projection is typed ordinals/IDs; strings, Narsese or MeTTa syntax belong at the adapter membrane. + +Required input fields (logical schema; concrete representation deferred to OGAR hotplug): +- `world_id`, `horizon`, `source_version`, `reasoner`, `reasoner_commit`, `config_digest`, `seed`, `cycle_budget`, `allocation_policy`. +- `node_id` + `class_id` and `method_key` + `schema_seal` + `reading_id` where applicable; one stable identity != display label. +- Evidence: `evidence_id`, observed/asserted origin, `evidential_roots` (the actual independence basis), `source_time`, `ingest_time`, temporal event identity; attention/saccade traces **separate**. +- Derivation: `derived_id`, `rule_id@version`, premise IDs, conclusion ID, materialization epoch, bounded-stamp fidelity, admission/selection reason. +- `frequency`, `confidence`, NARS eternal/temporal distinction, and `epi5_class_reading` (not invented CE64 bits). +- Operation: prediction/anticipation, procedure/decision, priority/resource budget and explicit unknown/unsupported status. + +Export event kinds: Observed, Assumed, Derived, Revised, Selected, Evicted, Predicted, Decision, Refused. If internal parentage is not exposed, report **partial provenance** and refuse exact descendant deletion. Never infer parentage solely from identical text or from bounded NARS stamps. + +Ablation specification: + + { target_kind: Evidence | RuleVersion | Method | Assumption, + target_ids: typed IDs, + horizon: pinned version, + mode: observational_leave_one_out | logical_method_suppression + | conditional_contingency | structural_do, + requested_readings: ..., budget: ... } + +Result receipt: + + { factual_world, counterfactual_world, owner, horizon, + target, first_divergence, affected_cone_ids, + factual_and_counterfactual_support_roots, shared_ancestor_ids, + delta_f, delta_c, verdict_before_after, + certification_before_after, predictions_before_after, + decisions_before_after, coverage_grade, cost, refusal_reasons } + +No `structural_do` receipt may claim causal certification if no explicit validated SCM exists. The counterfactual world must be detached and tagged, and all observed rows must be byte-identical to W0. + +## 3. Four ablations, plus the hidden fifth + +1. **Evidence ablation:** Remove observation A everywhere its root contributes, including copies/transitive consequences. Sibling independent B must remain intact. +2. **Rule ablation:** Remove one versioned inference rule R1. Retract and re-evaluate all learned conclusions and procedures downstream from R1. +3. **Interpretive-method ablation:** Keep observation bytes but suppress the *method/reading* responsible for converting them into claims. SAG methods are addressable by MethodKey + seal + reading. +4. **Assumption ablation:** A and B appear independent but share upstream U; remove U and discover both supports collapse. Never use two apparent pathways as independent confidence evidence if their root provenance intersects. +5. **Attention-policy ablation (control):** Hold factual observations/rules fixed, change scheduler or cognitive budget. If conclusions change due to eviction or cycle selection, label the outcome **resource-path sensitivity**, not a demonstrated logical dependency. + +The interesting 'nine-dot' crossing is (3) or (4): the important contributor can lie outside the apparent data graph. The claim is a testable research hypothesis, not novelty established by comparison. + +## 4. Oracle matrix: different systems, different roles + +| Adapter/oracle | Why it matters | First test | Interface/limits | +| --- | --- | --- | --- | +| **ONA** OpenNARS for Applications (C) | Temporal predictions, learned operations, attentional selection, resources | Replay one fixed Narsese history twice with the same build/config/seed/budget; suppress one input *before ingestion*; compare anticipation and procedural choice | CLI `./NAR shell < fixture.nal` and `python3 evaluation.py` are documented upstream. No claim ONA exposes complete derivation ancestry or has a direct retract API. | +| **OpenNARS** (Java) | Evidential stamps, temporal and eternal inference, non-axiomatic revision | Two independent roots vs duplicated evidential root vs partial overlap; distinguish revision from choice | Pin working upstream release and evidence-stamp semantics; bounded stamps are **not** full causal provenance. | +| **Hyperon/MeTTa** | Rewrite rules and rule-as-data make interpretation/method removal explicit | Same atoms, two rewrite rules; remove rule R1 and compare derived graph / trace | Pin interpreter/rewrite semantics and isolation. A MeTTa result is not NARS F/C without explicit mapping. | +| **Differential Dataflow** (Rust) | Independent incremental signed-update execution oracle | Insert/delete roots or rule facts, compare stabilized closure with scratch recomputation | Test lawful joins/fixed points and full proof multiplicity, not just Boolean membership. | +| **Soufflé Datalog provenance** | Independent explanation/proof oracle | Cross-check which tuples and proof trees support C | Minimal-height proof tree != complete support provenance. Exhaust alternative derivations before calling retraction exact. | +| **lance-graph Quack + R2IL** | Candidate optimized execution, typed mask semantics and SAG | Identical observations, outputs and support certificates vs the independent oracle | A one-hop DAG/query only today. No phantom multi-hop lowering, new opcode, or self-modification. | + +Initial engineering order: ONA external black-box first for temporal effects; OpenNARS evidential control; Hyperon method-ablation; Differential Dataflow recomputation oracle; Soufflé provenance audits. An additional **local deterministic truth-table oracle** should be the first smoke test before running any foreign engine. + +## 5. Exact execution protocol (external black-box first) + +0. Pin Git SHA, toolchain, configuration, available resources, seed, cycle budget, query horizon and expected output parser. Normalize output to typed evidence receipts, **not** belief-string equality. +1. Compile or run each upstream reasoner's native upstream tests. Save version/output fingerprints as artifacts, do not vendor engines in the core crate. +2. In W0 ingest one synthetic event sequence, freeze output at a concrete h; repeat W0 identically and require deterministic normalized receipts or document the exact nondeterminism. +3. Build W_X from the **same pristine initialization** with *only* X excluded or R1 disabled at admission. Re-run the complete sequence, including learned rules. Compare at matched logical cycle and event time; do not mix wall-clock timing with logical version. +4. Use a fixed provenance DAG with proof alternatives, materialized derivations, root sets and rule versions; compute descendants. Verify incremental invalidation **against scratch re-evaluation** before attempting shortcut retractions. +5. Query candidate affected rows via SAG/Quack. The current one-hop restriction may require a legal relation-carrier materialization or repeated factored reads; explicitly quantify that cost. +6. Record two costs: whole-world replay and incremental-invalidation path. Compute speedup only after *identical observable outputs*. Attribute costs to ingestion, indexing, join, re-evaluation and I/O; report cold/warm, small/large-cone, density, fanout, cycles, p50/p95 and memory. +7. Produce detached, non-authoritative shadow receipt with `Coverage = Complete | Partial | Unsupported`. No automatic new truth, no causal-bit promotion, no graph transformation, no Rubicon commit. +8. Only after provenance and parity gates pass: feed `Reaction` and mapped `claim -> step` into Gadamer EncounterEvidence; leave TruthOnly unresolved unless the policy explicitly distinguishes redundancy. + +**One-step vs joint cuts:** use bit positions to batch up to 64 *Boolean reachability scenarios* under a proved interpretation. This is **not** 64 CE64 truth replays or 64 SIMD registers. Each non-Boolean NARS revision needs its actual execution or a separately validated vectorization. Rung(0..9), CE64 bit, SIMD lane, scenario ordinal and Alpha overlay owner remain distinct axes. + +## 6. Required fixtures and adversarial falsifiers + +| ID | Fixture | Required outcome / failure signal | +| --- | --- | --- | +| F0 | Duplicate pristine baseline; same version/seed/budget | Byte-equivalent normalized receipts or documented nondeterministic envelope. | +| F1 | A -> R1 -> C, independent B -> R2 -> C; cut A | C survives through B, but support set loses A. | +| F2 | Above, cut R1 | C survives; no stale derivation attributed to R1. | +| F3 | Remove both R1,R2 | C loses all modeled supports. | +| F4 | Two nominally separate paths A,B both depend on hidden U; cut U | Both paths collapse; confidence cannot treat them as independent sources. | +| F5 | Duplicate input A under two aliases; cut A's source root | Both aliases retract; independent B unaffected. | +| F6 | Unrelated contributor X | No change to C, derivations, cert or decision. | +| F7 | A OR B; cut A then conditionally cut B | No but-for flip on first cut; A becomes pivotal under contingency B=off. Do not conclude A cannot be a cause. | +| F8 | A changes truth but not threshold verdict | TruthOnly / support change remains distinguishable from Inert and Necessary. | +| F9 | Delete interpretation method, not stored observations | Original observations remain identical; all and only rule-dependent descendants re-evaluate. | +| F10 | Hindsight injection after pinned horizon | Strict `QueryReference::at` never leaks future rows; default latest sentinel is not accepted as proof. | +| F11 | Cyclic or negated derivations, bounded evidential stamps, evictions | Conservative refusal, SCC/fixpoint or scratch replay; never fabricate complete provenance. | +| F12 | Factual vs detached counterfactual storage | No counterfactual result is certified/committed as observation; -6 tag where existing CE64 replay applies. | +| F13 | Quack one-hop vs multi-hop dependency | No illegal population intermediate; either use approved relation-carrier/eq-via or mark BLOCKED. | +| F14 | Baseline vs differential oracle under insert/delete/reinsert | Exact closure and support-count parity, including multiple derivations and shared root IDs. | +| F15 | Scheduler policy changes under fixed evidence | Changes in emitted decisions are labeled resource-path sensitivity; cannot claim underlying facts changed. | + +The adversarial **disable test** for each gate must actually go red: allow duplicated roots, drop premise dependency, relax horizon pin, or accept a stale method seal; restore afterwards. A green disable run means the guard has no real test. + +## 7. Efficiency question and kill conditions + +If a dependency cone has size k within n recorded facts, a correct indexed deletion/update may avoid scanning all n; **O(k)** is not guaranteed because closure discovery, joins, recomputation, SCCs and provenance fanout have costs. First measure `T_full(n)`, `T_incremental(k,n)` and `T_index(n)`; include index build/amortization and memory. + +Report two performance frontiers: a *small* dependency cone (candidate sparse advantage) and *near-whole-graph* cone (candidate pathological case). Compare to vanilla replay (ONA), Differential Dataflow incremental maintenance, and Quack baseline. KILL incremental optimization at measured regimes where full replay is faster; KILL exact retraction when provenance is incomplete; KILL causal-certification claim without a declared intervention/SCM; KILL method introspection that cannot identify and version the rule actually used. + +Use entropy/expected information gain **only to schedule which falsifiable cut to try next**, not to increase belief confidence. For a budgeted probe choose candidate X using cost-aware expected reduction in uncertainty over hypotheses, then measure its realized discrimination; include random, maximum-confidence and highest-graph-degree baselines. Never require new CE64 bits to store importance, responsibility or entropy. + +## 8. Implementation waves and acceptance gates + +- **W0: Protocol and oracle fixture (this PR).** One pinned spec, references, expected trace schemas and a runnable, dependency-free Boolean/proof-DAG smoke oracle. No external-engine results claimed. +- **W1: ONA shell adapter.** Native fixtures + reproducible external replay; extract stable IDs, evidential origins, temporal predictions and output decisions, mark unknown ancestry Partial. Gate F0,F1,F6,F8,F15. +- **W2: OpenNARS evidential control.** Stamp independence/revision vs choice, duplicate roots and NARS truth-law parity. Gate F4,F5,F11; do not derive exact fission from bytes. +- **W3: Hyperon method-as-data ablation.** Rule/assumption rewrite suppression and inspect alternatives. Gate F2,F3,F9; distinguish model interpretation from source data. +- **W4: Independent incremental oracle.** Differential Dataflow plus Soufflé explanation, full recomputation truth oracle, signed updates and multiset derivations. Gate F7,F11,F14. +- **W5: SAG/Quack projection.** Map to validated OGAR MethodKey, schema seal, typed reading, tier and provenance. Solve the legal multi-hop seam without new engine; gate F10,F12,F13. +- **W6: Gadamer/Rubicon bridge (separate semantic decision).** Claim-to-step identities + distinct Necessary/Redundant/TruthOnly/Unknown admission policy. No automatic writer or intention inference. +- **W7: Bench and active experimental selection.** Bound memory and runtime, ablation selection with entropy/expected information gain; publish all results and negative controls. + +**Review questions before production:** What is the minimum complete evidence root key (not stamp alias)? How can a method/rule be versioned across engines? Are learned rules retracted, or must memory be rebuilt? What does TruthOnly mean at the Gadamer gate? How do we represent incompatible MeTTa and NARS truth semantics without lossy conversion? What is the legally allowed multi-hop Quack carrier? What performance regime actually rewards sparse delta maintenance? + +## 9. Claude Code / implementer prompt + +> Read this RFC, the SAG #1509 plan, Gadamer ablation audit and the research map before writing code. Inventory the exact current commit and the real methods in temporal.rs, chain_counterfactual.rs, chain_replay.rs, revision.rs and awareness.rs. First run the provided synthetic oracle and demonstrate that disabling each guard breaks its named falsifier. Implement **one** external ONA fixture runner at a pinned upstream commit: baseline vs clean-room re-ingestion with one evidence source suppressed; normalize outputs into an explicitly partial receipt. Validate identical baseline executions and do not claim ONA supports retraction without code evidence. Keep the observed history immutable and the counterfactual world detached. Run F0/F1/F6/F8/F15; report the measured output and any inaccessible provenance. Then propose the smallest OGAR/ClassView adapter and an allowed one-hop Quack query. Never silently reinterpret the CE64 register as NARS-specific, invent an opcode, revise factual confidence from a counterfactual, or promote a logical deletion into Pearl causality. Split unresolved semantic decisions into follow-up PRs; no unverified shipped claims. + +## 10. References and traceability + +- Upstream: [ONA C repository](https://github.com/opennars/OpenNARS-for-Applications), [OpenNARS Java](https://github.com/opennars/opennars), [MeTTa / Hyperon](https://github.com/trueagi-io/hyperon-experimental), [Differential Dataflow](https://github.com/TimelyDataflow/differential-dataflow), [Soufflé provenance](https://souffle-lang.github.io/provenance). +- Papers and paraphrased research excerpts: [research map](../../.arxiv/2026-10_inverted_temporal_ablation_reasoner_oracles.md) and [pre-existing Jøsang/NARS excerpts](../../.arxiv/2026-10_nars_self_epistemic_needs_evidence_primary_excerpts.md). +- Prior work: [#1509 SAG](https://github.com/AdaWorldAPI/lance-graph/pull/1509), [#1496 NARS](https://github.com/AdaWorldAPI/lance-graph/pull/1496), [#1497 PLN/entropy](https://github.com/AdaWorldAPI/lance-graph/pull/1497), [#1498 Hyperon](https://github.com/AdaWorldAPI/lance-graph/pull/1498). Existing [causal-replay plan](dismech-causal-replay-v1.md) and [actual-causality map](../../.arxiv/1608.07879_actual_causality_needs_contingencies_not_just_deletion.md). + +**Explicitly not shipped:** ONA/OpenNARS/Hyperon adapters, causal identification, dependency-complete NARS traces, Quack recursive traversal, proof-correct sparse deletion, CE64 confidence fission, self-modification, or any claimed performance improvement. From 3b4e40b6e77a3d15693ba358aeaf51cc1163f4a5 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Mon, 12 Oct 2026 21:34:00 +0200 Subject: [PATCH 2/4] docs: map NARS Hyperon and provenance-oracle research --- ...rted_temporal_ablation_reasoner_oracles.md | 101 ++++++++++++++++++ 1 file changed, 101 insertions(+) create mode 100644 .arxiv/2026-10_inverted_temporal_ablation_reasoner_oracles.md diff --git a/.arxiv/2026-10_inverted_temporal_ablation_reasoner_oracles.md b/.arxiv/2026-10_inverted_temporal_ablation_reasoner_oracles.md new file mode 100644 index 000000000..cdcc2040e --- /dev/null +++ b/.arxiv/2026-10_inverted_temporal_ablation_reasoner_oracles.md @@ -0,0 +1,101 @@ +# Inverted temporal ablation × ONA × OpenNARS × Hyperon: primary-source research map + +**Date:** 2026-10-12. **Status:** annotated reference map; *paraphrased excerpts*, not a claim that any upstream engine has passed our benchmark. Companion RFC: [inverted temporal ablation](../.claude/plans/inverted-temporal-ablation-reasoner-oracles-v1.md). Builds on [existing primary excerpts for NARS/fission](2026-10_nars_self_epistemic_needs_evidence_primary_excerpts.md), [actual causality and contingencies](1608.07879_actual_causality_needs_contingencies_not_just_deletion.md), and [self in NARS](2018_self_in_nars_requires_internal_experience_and_mental_operations.md). + +## Why this collection + +A nine-dot *epistemic* probe differs from ordinary ablation by asking what happens when one **rule, interpretation, or shared epistemic assumption**, not only one observation, is suppressed. Each source below either motivates a testable distinction or acts as an independent oracle. Papers do not establish performance or novelty of the proposed lance-graph composition. + +### R1. Jøsang (2007), Cumulative and Averaging Fission of Beliefs + +- Primary: [arXiv:0712.1182](https://arxiv.org/abs/0712.1182), abstract, fusion and fission definitions; [PDF](https://arxiv.org/pdf/0712.1182). +- **Paraphrased excerpt:** Cumulative fusion models independent evidence; averaging fusion addresses dependent opinions; fission attempts to remove a known contributor from a fused opinion under that particular fusion model. +- **Do not conflate:** Subjective Logic opinions and NARS truth values have different semantics. Compressed u8 CE64 F/C alone cannot reconstruct arbitrary removed support; require contributor IDs, dependence relation, weights and original revision order, or refuse exact inverse. +- **Testable translation:** Independent A+B -> remove A -> only B remains (within stated rounding); duplicated A under aliases -> delete both references to root A; unknown overlap -> `Coverage=Partial/Unsupported`. Compare true recompute to putative algebraic inverse. + +### R2. Wang, Li, Hammer (2018), Self in NARS, an AGI System + +- Primary: [Frontiers Robotics and AI DOI:10.3389/frobt.2018.00020](https://www.frontiersin.org/journals/robotics-and-ai/articles/10.3389/frobt.2018.00020/full), especially §§2–3 on truth, evidence, internal experience, control. +- **Paraphrased excerpt:** Reasoning relies on finite resources and revisable experiential evidence; the system can treat some of its internal processing as experience. Distinguish reasoning about derivation from a claim of phenomenal consciousness. +- **Testable translation:** Track three IDs separately: independent external observation root, derivation/procedure trace, and attention-selection trace. Changing attention may change emitted results without changing logical entailment. A derivation trace alone cannot make a new independent NARS observation. +- **Falsifier:** Give two conclusions with equal final F/C but distinct provenance. Explanation must distinguish them while confidence stays unchanged. + +### R3. Hammer & Lofthouse (2020), OpenNARS for Applications: Architecture and Control + +- Primary artifact: [official ONA repository README and references](https://github.com/opennars/OpenNARS-for-Applications); upstream paper linked there (AGI 2020 conference contribution); [official ONA wiki](https://github.com/opennars/OpenNARS-for-Applications/wiki). +- **Paraphrased excerpt from maintainer README:** ONA is a new C implementation, not an OpenNARS branch, designed for application-oriented event handling, procedure learning and resource-based control. The maintainers explicitly acknowledge conceptual differences from research OpenNARS. +- **Consequences:** Do not silently assume identical revision rules, stamp representation, command syntax or derivation export between the two. Begin with upstream CLI documented `./NAR shell`, example `*.nal` inputs, `python3 evaluation.py`; pin SHA and config and inspect actual output before normalizing. +- **Testable translation:** Same temporal-event fixture, with and without a root observation, measure subsequent temporal implications, anticipation, learned operation and chosen action at equal time/budget. Separately vary priority or memory budget to diagnose resource-path sensitivity. +- **Unverified:** Upstream exposure of exhaustive proof ancestry, a reversible belief deletion API, and deterministic output under all scheduling modes. + +### R4. Hammer, Lofthouse & Wang (2016), The OpenNARS Implementation of the Non-Axiomatic Reasoning System + +- Primary repository: [opennars/opennars](https://github.com/opennars/opennars); maintainer-linked publication is in the ONA README; [OpenNARS stamp discussion](https://github.com/opennars/opennars/wiki/Stamp). +- **Paraphrased excerpt / technical idea:** A stamp records creation/occurrence context and evidential-base identifiers; this informs revision/choice and overlapping-evidence checks. Resource-bounded bases can truncate. +- **Testable translation:** Compare (i) independent evidence, (ii) duplicated evidence with a shared root, (iii) two paths with a hidden common ancestor, (iv) temporal vs eternal conclusions. Stamps may catch overlap, but *do not presume* they form a lossless provenance DAG. +- **Refusal:** When a stamp drops ancestry under capacity limits, report partial provenance; do not claim complete causal shadow or exact fission. + +### R5. Goertzel et al. (2023), OpenCog Hyperon: A Framework for AGI at the Human Level and Beyond + +- Primary: [arXiv:2310.18318](https://arxiv.org/abs/2310.18318), architecture §§3.1–3.2; [PDF](https://arxiv.org/pdf/2310.18318); [maintained experimental MeTTa implementation](https://github.com/trueagi-io/hyperon-experimental). +- **Paraphrased excerpt:** Hyperon represents cognitive processes and rewrite programs in a metagraph/Atomspace; making rules addressable data offers a route toward reflective modification. This is architectural motivation, *not evidence of achieved AGI or an ablation performance result*. +- **Testable translation:** Use two named MeTTa rewrite rules R1/R2 deriving C through distinct branches. Remove R1 from a cloned world, recompute and retain evidence atoms. Then disable a shared method/assumption upstream of both. Compare derived atoms and explanations, not NARS confidence fields. +- **Open question:** Which MeTTa runtime semantics, rewrite ordering and proof export support reproducible source-to-result attribution? Pin the version and distinguish pattern matching, nondeterminism and selection from entailment. + +### R6. Chockler (2016), Causality and Responsibility for Formal Verification and Beyond + +- Primary: [arXiv:1608.07879](https://arxiv.org/abs/1608.07879); [local detailed harvest](1608.07879_actual_causality_needs_contingencies_not_just_deletion.md). +- **Paraphrased excerpt:** Actual-cause analyses under Halpern–Pearl conditions admit contingencies. A contributor can be causally relevant even if a one-at-a-time deletion does not flip the outcome because of alternative support. Responsibility additionally considers how much context must change to make the contributor decisive. +- **Testable translation:** With Y=A OR B, test deleting A alone, then deleting A under the explicit contingency B=off. Record the context and resulting verdict; never equate a deletion's no-flip result with 'not causal'. +- **Boundary:** Conditional logical pivotality is not a claim of causal identification until a valid SCM/intervention model and assumptions are declared. Moral responsibility/intent are not inferred. + +### R7. Differential Dataflow (McSherry et al.), incremental signed-update computation + +- Implementation/doc: [TimelyDataflow/differential-dataflow](https://github.com/TimelyDataflow/differential-dataflow), [crate documentation](https://docs.rs/differential-dataflow/latest/differential_dataflow/), especially Collections and iteration. +- **Paraphrased implementation note:** Collection updates add and remove weighted records. Existing operators maintain derived results incrementally over updates; recursive relations can be iterated to fixed points. +- **Testable translation:** Create materialized support tuples and recursive reachability. Delete evidence and rule tuples, feed signed updates, compare stabilized closure and multiplicity to a *fresh recomputation*. Include cycles, diamond-shaped shared ancestors, and fan-out. +- **Boundary:** Differential Dataflow is a computation oracle, not NARS, OpenCog, or a causal model. Bench costs include arrangement/index build and resident memory. + +### R8. Soufflé provenance and explanation + +- Primary documentation: [Soufflé Provenance](https://souffle-lang.github.io/provenance), including the `-t explain` command and explanation trees. +- **Paraphrased excerpt:** Soufflé can explain derived tuples using reconstructed proof trees of minimal height, and support interactive explanations for failures. Its provenance is lazy, while stored annotations facilitate explanation. +- **Testable translation:** Query support for C and inspect branches, rule IDs and premises. Multiple derivations need complete enumeration or an additional support-count oracle; a *single shortest proof* is insufficient to establish that deleting one branch erases C. + +### R9. Green, Karvounarakis & Tannen (2007), Provenance Semirings + +- Primary: [DBLP bibliographic entry](https://dblp.org/rec/conf/pods/GreenKT07.html), [author PDF](https://www.cis.upenn.edu/~green/papers/pods07.pdf). +- **Paraphrased excerpt:** Annotating database tuples with provenance polynomials distinguishes alternative derivations (sum) from jointly required inputs (product), retaining more information than Boolean membership. +- **Testable translation:** For two proof paths, C may have polynomial terms (A*R1)+(B*R2); setting A=0 removes only its term, whereas shared upstream U in *both* terms factors as U*(A*R1+B*R2). This is a conceptual oracle for hidden shared causes, **not** a direct arithmetic prescription for NARS truth revision. + +## Minimal synthetic world and comparators + + U -> A -> R1 -> C + -> B -> R2 -> C + independent D -> R3 -> C + +World W0 contains C with three derivations; suppress A, C survives via B and D; suppress U, A and B disappear but D survives; suppress U AND D, C disappears. Compare: +- **Boolean conclusion membership**; +- **complete derivation multiplicity** and provenance root sets; +- **numerical truth** only within a specific declared reasoner's semantics; +- **temporal prediction** and selected action; +- **certification** (Observed/Related/Explains/Causes separately, no new earned 'Causes' from ablation); +- **horizon integrity** (future events after pin inaccessible). + +The first hard falsifier is deliberately not 'did C disappear?'. It is **'did the correct support disappear while independent support survived?'** This distinguishes exact source-aware retraction from a deceptively successful but causally blind deletion. + +## A cost-aware cognitive probe, not a truth generator + +Candidate X can be selected from provenance branches/rule assumptions to maximize measured discriminatory value under a time/memory budget. A suggested hypothesis (not a result) is expected information gain per estimated probe cost. Benchmark it against random cuts, largest-subgraph cuts, highest-confidence cuts, and full replay. All candidate scheduling, epistemic certification, and Rubicon commitment remain distinct; an entropy reduction must never be counted as additional observational support. + +## Research stop conditions + +- No truth-law crosswalk: do **not** equate NARS F/C with PLN, subjective-logic opinions or MeTTa rewrite membership. +- No root-level ancestry: exact fission/retraction **Unsupported**. +- Unpinned source horizon: strict historical claim **Unsupported**. +- Incomplete or evicted derivation trace: affected cone **Partial**. +- No SCM and admissible contingency policy: causal identification **Unsupported**. +- No parity against fresh replay: sparse speedup **Not demonstrated**. +- No comparison with code and history: novelty **Not established**. + +Related repo material: [existing 2026-10 NARS primary excerpts](2026-10_nars_self_epistemic_needs_evidence_primary_excerpts.md), [Gadamer ablation audit](../.claude/research/2026-10-recovery/GADAMER-ABLATION-RESEARCH.md), [SAG #1509](https://github.com/AdaWorldAPI/lance-graph/pull/1509). From bc0cdfcdb793b2c71dee7dff61c445f1901089f8 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Mon, 12 Oct 2026 21:35:00 +0200 Subject: [PATCH 3/4] test: add dependency-free provenance ablation smoke oracle --- .../inverted_temporal_ablation_oracle.py | 236 ++++++++++++++++++ 1 file changed, 236 insertions(+) create mode 100644 .claude/tools/inverted_temporal_ablation_oracle.py diff --git a/.claude/tools/inverted_temporal_ablation_oracle.py b/.claude/tools/inverted_temporal_ablation_oracle.py new file mode 100644 index 000000000..f3836c4b7 --- /dev/null +++ b/.claude/tools/inverted_temporal_ablation_oracle.py @@ -0,0 +1,236 @@ +#!/usr/bin/env python3 +"""D-SAG-CF-1: deliberately small, independent *Boolean provenance* oracle. + +Run: python3 .claude/tools/inverted_temporal_ablation_oracle.py +No foreign reasoner, CE64 update, SCM/do(), probabilistic inference, +temporal reconstruction, or Quack implementation is claimed here. +The finite acyclic fixture is a parity baseline, NOT the production engine. +""" +from __future__ import annotations + +from dataclasses import dataclass +from itertools import product +import unittest + +Term = frozenset[str] +Proofs = dict[str, frozenset[Term]] + + +@dataclass(frozen=True) +class Rule: + id: str + premises: tuple[str, ...] + conclusion: str + + +@dataclass(frozen=True) +class World: + # Claim -> source root. An alias of the same observation uses the SAME root. + observations: tuple[tuple[str, str], ...] + rules: tuple[Rule, ...] + + +@dataclass(frozen=True) +class Shadow: + lost_claims: frozenset[str] + gained_claims: frozenset[str] + changed_support: frozenset[str] + removed_proofs: Proofs + added_proofs: Proofs + + +def _validate_acyclic(world: World) -> None: + """Fail closed instead of pretending an unbounded recursive proof is exact.""" + adjacency: dict[str, set[str]] = {} + ids: set[str] = set() + for rule in world.rules: + if rule.id in ids: + raise ValueError("rule ids must be unique and versioned") + ids.add(rule.id) + for premise in rule.premises: + adjacency.setdefault(premise, set()).add(rule.conclusion) + states: dict[str, int] = {} + + def dfs(node: str) -> None: + if states.get(node) == 1: + raise ValueError("recursive/cyclic provenance requires another oracle") + if states.get(node) == 2: + return + states[node] = 1 + for child in sorted(adjacency.get(node, ())): + dfs(child) + states[node] = 2 + + for node in sorted(adjacency): + dfs(node) + + +def evaluate( + world: World, + cut_roots: frozenset[str] = frozenset(), + cut_rules: frozenset[str] = frozenset(), +) -> Proofs: + """Compute all minimal Boolean proof terms on a tiny DAG, from scratch. + + Terms are sets of original source IDs AND rule IDs. Alternatives are a + set of terms. A shared root appears in every proof that depends on it. + No numerical NARS revision, timestamps or causal certification occurs. + """ + _validate_acyclic(world) + roots: dict[str, set[Term]] = {} + for claim, root in world.observations: + if root not in cut_roots: + roots.setdefault(claim, set()).add(frozenset((f"obs:{root}",))) + + # Finite DAG, no negative premises: monotone closure terminates. + while True: + before = sum(len(v) for v in roots.values()) + for rule in world.rules: + if rule.id in cut_rules: + continue + supports = [roots.get(p, set()) for p in rule.premises] + if not supports or any(not s for s in supports): + continue + for chosen in product(*supports): + evidence = frozenset.union(*chosen, frozenset((f"rule:{rule.id}",))) + roots.setdefault(rule.conclusion, set()).add(evidence) + after = sum(len(v) for v in roots.values()) + if after == before: + break + return {k: frozenset(v) for k, v in roots.items()} + + +def ablate( + world: World, + *, + roots: frozenset[str] = frozenset(), + rules: frozenset[str] = frozenset(), +) -> Shadow: + factual = evaluate(world) + counterfactual = evaluate(world, roots, rules) + factual_keys = set(factual) + cf_keys = set(counterfactual) + touched = factual_keys | cf_keys + removed = { + k: frozenset(factual.get(k, frozenset()) - counterfactual.get(k, frozenset())) + for k in sorted(touched) + if factual.get(k, frozenset()) - counterfactual.get(k, frozenset()) + } + added = { + k: frozenset(counterfactual.get(k, frozenset()) - factual.get(k, frozenset())) + for k in sorted(touched) + if counterfactual.get(k, frozenset()) - factual.get(k, frozenset()) + } + return Shadow( + lost_claims=frozenset(factual_keys - cf_keys), + gained_claims=frozenset(cf_keys - factual_keys), + changed_support=frozenset( + k for k in touched if factual.get(k) != counterfactual.get(k) + ), + removed_proofs=removed, + added_proofs=added, + ) + + +def two_paths() -> World: + return World( + (("A", "a"), ("B", "b")), + (Rule("R1@1", ("A",), "C"), Rule("R2@1", ("B",), "C")), + ) + + +def hidden_root() -> World: + return World( + (("U", "u"), ("D", "d")), + ( + Rule("makeA@1", ("U",), "A"), + Rule("makeB@1", ("U",), "B"), + Rule("R1@1", ("A",), "C"), + Rule("R2@1", ("B",), "C"), + Rule("R3@1", ("D",), "C"), + ), + ) + + +class ProbeTests(unittest.TestCase): + def test_f0_pristine_replay_is_exact(self) -> None: + w = hidden_root() + self.assertEqual(evaluate(w), evaluate(w)) + + def test_f1_cut_a_keeps_independent_b(self) -> None: + s = ablate(two_paths(), roots=frozenset(("a",))) + self.assertNotIn("C", s.lost_claims) + self.assertIn("C", s.changed_support) + self.assertEqual(len(s.removed_proofs["C"]), 1) + + def test_f2_cut_rule_not_its_input(self) -> None: + s = ablate(two_paths(), rules=frozenset(("R1@1",))) + self.assertIn("C", s.changed_support) + self.assertNotIn("A", s.changed_support) + self.assertNotIn("C", s.lost_claims) + + def test_f3_joint_cut_removes_all_support(self) -> None: + s = ablate(two_paths(), rules=frozenset(("R1@1", "R2@1"))) + self.assertIn("C", s.lost_claims) + + def test_f4_shared_assumption_collapses_two_paths(self) -> None: + s = ablate(hidden_root(), roots=frozenset(("u",))) + self.assertIn("A", s.lost_claims) + self.assertIn("B", s.lost_claims) + self.assertNotIn("C", s.lost_claims) # D independently supports C + self.assertEqual(len(s.removed_proofs["C"]), 2) + + def test_f5_aliased_observation_cut_by_source(self) -> None: + w = World( + (("A1", "shared"), ("A2", "shared"), ("B", "independent")), + ( + Rule("R1@1", ("A1",), "C"), + Rule("R2@1", ("A2",), "C"), + Rule("R3@1", ("B",), "C"), + ), + ) + s = ablate(w, roots=frozenset(("shared",))) + self.assertEqual(s.lost_claims, frozenset(("A1", "A2"))) + self.assertNotIn("B", s.changed_support) + self.assertNotIn("C", s.lost_claims) + + def test_f6_irrelevant_source_is_noop(self) -> None: + self.assertEqual( + ablate(two_paths(), roots=frozenset(("does-not-exist",))).changed_support, + frozenset(), + ) + + def test_f7_contingency_exposes_pivotality(self) -> None: + w = two_paths() + self.assertNotIn("C", ablate(w, roots=frozenset(("a",))).lost_claims) + self.assertIn("C", ablate(w, roots=frozenset(("a", "b"))).lost_claims) + + def test_f9_rule_cut_never_changes_observations(self) -> None: + w = hidden_root() + s = ablate(w, rules=frozenset(("makeA@1", "makeB@1"))) + self.assertNotIn("U", s.changed_support) + self.assertNotIn("D", s.changed_support) + self.assertIn("A", s.lost_claims) + self.assertIn("B", s.lost_claims) + + def test_refuse_cycle_without_losing_evidence(self) -> None: + w = World((("A", "a"),), (Rule("R@1", ("A",), "B"), + Rule("S@1", ("B",), "A"))) + with self.assertRaisesRegex(ValueError, "cyclic"): + evaluate(w) + + def test_refuse_duplicate_rule_identity(self) -> None: + w = World((("A", "a"),), + (Rule("R@1", ("A",), "C"), Rule("R@1", ("A",), "D"))) + with self.assertRaisesRegex(ValueError, "unique"): + evaluate(w) + + def test_support_and_membership_are_distinct(self) -> None: + s = ablate(hidden_root(), roots=frozenset(("d",))) + self.assertNotIn("C", s.lost_claims) + self.assertIn("C", s.changed_support) + self.assertEqual(len(s.removed_proofs["C"]), 1) + + +if __name__ == "__main__": + unittest.main() From 91791c47eb0ff322bc3cf848cea19055a08d4279 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Mon, 12 Oct 2026 21:35:41 +0200 Subject: [PATCH 4/4] docs: record D-SAG-CF-1 handoff and falsification gates --- .../2026-10-12-inverted-temporal-ablation.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 .claude/board/entries/2026-10-12-inverted-temporal-ablation.md diff --git a/.claude/board/entries/2026-10-12-inverted-temporal-ablation.md b/.claude/board/entries/2026-10-12-inverted-temporal-ablation.md new file mode 100644 index 000000000..0e09a57e1 --- /dev/null +++ b/.claude/board/entries/2026-10-12-inverted-temporal-ablation.md @@ -0,0 +1,15 @@ +# D-SAG-CF-1 — Inverted temporal ablation and independent reasoner oracles (2026-10-12) + +**Status: RFC + synthetic Boolean smoke oracle; no upstream adapters, no production path, no benchmark.** +**Parent:** [merged #1509 SAG](https://github.com/AdaWorldAPI/lance-graph/pull/1509). + +- **Research plan:** [inverted-temporal-ablation-reasoner-oracles-v1.md](../../plans/inverted-temporal-ablation-reasoner-oracles-v1.md), includes the pinned-horizon two-world contract, evidence/rule/method/assumption/attention cuts, OGAR ClassView + MethodKey + schema/reading, Quack one-hop restriction, temporal vs data-causal split, Gadamer admission gap, CE64 no-new-bits rule, W0–W7 experiment sequence, and F0–F15 falsifiers. +- **Annotated sources:** [cross-reasoner arXiv map](../../../.arxiv/2026-10_inverted_temporal_ablation_reasoner_oracles.md) covers Jøsang fission, Wang internal experience, ONA vs OpenNARS, Hyperon MeTTa, actual causality with contingencies, provenance semirings, Differential Dataflow, and Soufflé. +- **Portable local oracle:** [inverted_temporal_ablation_oracle.py](../../tools/inverted_temporal_ablation_oracle.py), stdlib-only DAG/proof-term closure and 12 `unittest` checks. Run from repo root with `python3 .claude/tools/inverted_temporal_ablation_oracle.py`. Its behavior is **not** NARS truth revision, a Pearl SCM, actual causal identification, or production Quack. +- **Existing shipped foundation:** `chain_counterfactual.rs` has a detached single-step cut; `temporal.rs` deinterlaces horizon/owner trajectories; SAG #1509 represents one-hop methods and provenance. None is yet the proposed complete inverse-temporal retraction engine. +- **Biggest correctness blocker:** exact evidence-base dependence and transitive child invalidation are not generally reconstructible from bounded stamps or compressed F/C. Handle as partial/unsupported rather than silently counting redundant evidence. +- **Biggest execution blocker:** legal multi-hop relation passing in Quack; #1509 explicitly prohibits treating population intermediates as native operands. + +**Next smallest PR:** pin an ONA upstream SHA and build a fully reproducible `./NAR shell` external input-suppression fixture, including identical baseline and scheduler-control runs. No irreversible writer. + +**STOP:** Do not merge this research RFC as if the adapters, sparse speedups, or 64-way NARS truth replays were implemented. TruthOnly and claim-to-step mapping remain explicit semantic decisions; conditional logical importance is not automatically Pearl causality.