From c01030c40eec12f7b05537bc0352ff23622bc8fb Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 28 Oct 2026 18:55:20 +0000 Subject: [PATCH 1/7] planner: tactic warrant over grounded markers; contract: recipe rule, unmeasured outcomes - contract epistemic_state5::RecipeRule: requires/forbids over declared facts, per-state check and V1 population (moved from the lab law). - contract CertificationModel::measured_only: unknown outcomes are excluded, not read as negatives; an arm left empty refuses. - planner nars::warrant: Marker (ledger evidence + declared Epi5 state + thought slot), tactic_rule for recipes 4/6/7/8/11, fire() runs RCR/TR/CAS on markers, admits candidates into the DerivationLedger, and returns judgments at Unknown x Open with the proof's roots. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMPWTwovjYJEUMuGPb4 --- .../lance-graph-contract/src/certification.rs | 66 ++ .../src/epistemic_state5.rs | 86 +++ crates/lance-graph-planner/src/nars/mod.rs | 1 + .../lance-graph-planner/src/nars/warrant.rs | 681 ++++++++++++++++++ 4 files changed, 834 insertions(+) create mode 100644 crates/lance-graph-planner/src/nars/warrant.rs diff --git a/crates/lance-graph-contract/src/certification.rs b/crates/lance-graph-contract/src/certification.rs index 0d5014cac..572e60053 100644 --- a/crates/lance-graph-contract/src/certification.rs +++ b/crates/lance-graph-contract/src/certification.rs @@ -289,6 +289,35 @@ impl CertificationModel { ) } + /// The model restricted to the units whose outcome was measured. + /// + /// `outcome` is a positive mask: a unit outside it reads as a known + /// negative. A unit whose outcome is UNKNOWN must not read that way, so + /// before certifying, every mask (population, strata, ordering, + /// robustness, and the trial arms, which `causes` reads without the + /// universe) is intersected with `measured`. An arm left with no measured + /// unit refuses as [`NotGrounded::EmptyArm`] rather than deciding. + #[must_use] + pub fn measured_only(&self, measured: &M) -> Self { + let keep = |m: &M| m.intersection(measured); + CertificationModel { + universe: keep(&self.universe), + exposed: keep(&self.exposed), + outcome: keep(&self.outcome), + strata: [ + keep(&self.strata[0]), + keep(&self.strata[1]), + keep(&self.strata[2]), + keep(&self.strata[3]), + ], + ordered: keep(&self.ordered), + clean: keep(&self.clean), + trial: keep(&self.trial), + assigned: keep(&self.assigned), + ..self.clone() + } + } + /// The randomized arms read as a population of their own. pub fn trial_view(&self) -> CertificationModel { CertificationModel { @@ -458,6 +487,43 @@ impl ModelBuilder { mod tests { use super::*; + /// Unmeasured outcomes are not negatives. Treated arm: 4 units with the + /// outcome, 4 whose outcome was never measured. Control arm: 3 of 8. + /// Reading the unmeasured units as negatives gives 4/8 against 3/8, so + /// `causes` holds; restricted to measured units it is 4/4 against 3/8. + /// The second fixture moves the gap the other way: 2 of 8 treated + /// measured positive, 6 unmeasured; as negatives 2/8 < 3/8 refutes, as + /// unknown 2/2 > 3/8 holds. + #[test] + fn unmeasured_outcomes_are_not_read_as_negatives() { + let build = |treated_hits: u32, treated_unknown: u32| { + let mut b = ModelBuilder::new(); + b.sources(SupportBasis::InterventionBacked, &[1, 2]); + let (t_known, _) = b.arm(true, treated_hits, treated_hits); + let (t_unknown, _) = b.arm(true, treated_unknown, 0); + let (c, _) = b.arm(false, 8, 3); + let measured = t_known.union(&c); + assert!(!t_unknown.is_empty() && !t_unknown.intersects(&measured)); + (b.build(), measured) + }; + + let (m, measured) = build(2, 6); + assert_eq!(m.causes(), Ok(false), "unknowns read as negatives refute"); + assert_eq!(m.measured_only(&measured).causes(), Ok(true)); + + let (m, measured) = build(4, 4); + assert_eq!(m.causes(), Ok(true)); + assert_eq!(m.measured_only(&measured).causes(), Ok(true)); + + // An arm with no measured unit refuses instead of deciding. + let (m, _) = build(2, 6); + let control_only = m.trial.difference(&m.assigned); + assert_eq!( + m.measured_only(&control_only).causes(), + Err(NotGrounded::EmptyArm) + ); + } + /// Every fold of a model, so two models can be compared fold by fold. fn folds(m: &CertificationModel) -> [Sat; 6] { [ diff --git a/crates/lance-graph-contract/src/epistemic_state5.rs b/crates/lance-graph-contract/src/epistemic_state5.rs index 06e7ab0ee..3d4f3d842 100644 --- a/crates/lance-graph-contract/src/epistemic_state5.rs +++ b/crates/lance-graph-contract/src/epistemic_state5.rs @@ -306,6 +306,59 @@ pub const fn facts_population(required: Facts) -> Population { population } +/// A recipe's epistemic obligations: the facts a state must assert +/// (`requires`) and must not assert (`forbids`) for the recipe to be eligible +/// on an edge in that state. +/// +/// This is the affordance law's rule, moved from the D-GSO-AFF-0 lab +/// (`cognitive-shader-driver/examples/shared/affordance_law.rs`) so a +/// production consumer can read it. Eligibility is a read-only derivation from +/// declared facts: it does not authorize execution, does not say a +/// conclusion is true, and never writes an edge. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Default)] +pub struct RecipeRule { + /// Facts every eligible state asserts. + pub requires: Facts, + /// Facts no eligible state asserts. + pub forbids: Facts, +} + +impl RecipeRule { + /// A rule with these obligations. + #[must_use] + pub const fn new(requires: Facts, forbids: Facts) -> Self { + Self { requires, forbids } + } + + /// Whether a state asserting `facts` satisfies the rule. + #[must_use] + pub const fn holds(self, facts: Facts) -> bool { + facts & self.requires == self.requires && facts & self.forbids == 0 + } + + /// Whether `state` satisfies the rule. + #[must_use] + pub const fn admits(self, state: EpistemicState5) -> bool { + self.holds(state.facts()) + } + + /// The V1 codes on which the rule holds. Reserved codes never appear. + #[must_use] + pub const fn population(self) -> Population { + let mut population = 0; + let mut raw = 0; + while raw < CODES { + if let Some(facts) = COMPILED_FACTS_V1[raw] { + if self.holds(facts) { + population |= 1 << raw; + } + } + raw += 1; + } + population + } +} + /// A reading generation. V1 is the 2 × 3 product above. #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Default)] pub enum Epi5Gen { @@ -540,6 +593,39 @@ mod tests { EpistemicState5::new(Epi5Gen::V1, t, c).raw() } + /// A rule's population is exactly the meaningful codes it admits, and + /// `forbids` removes codes `requires` alone would keep. + #[test] + fn a_recipe_rule_population_matches_its_per_state_check() { + let rule = RecipeRule::new(ASSOCIATED, INTERMEDIATE_KNOWN); + let mut expected = 0; + for raw in 0u8..32 { + if let Ok(s) = EpistemicState5::decode(Epi5Gen::V1, raw) { + if rule.admits(s) { + expected |= 1 << raw; + } + } + } + assert_eq!(rule.population(), expected); + assert_eq!( + RecipeRule::new(ASSOCIATED, 0).population() & !rule.population(), + facts_population(ASSOCIATED | INTERMEDIATE_KNOWN), + "forbids removes exactly the states that assert the forbidden fact" + ); + assert!(!rule.admits(EpistemicState5::new( + Epi5Gen::V1, + T::IndirectKnown, + C::Causes + ))); + assert!(rule.admits(EpistemicState5::new( + Epi5Gen::V1, + T::IndirectUnknown, + C::Causes + ))); + assert!(!rule.admits(EpistemicState5::new(Epi5Gen::V1, T::Direct, C::Open))); + assert_eq!(rule.population() >> 24, 0, "reserved codes never admitted"); + } + /// The layout is the product: `raw5 = t | c << 2`, 24 meaningful, 8 /// reserved, and decode inverts it on every code. #[test] diff --git a/crates/lance-graph-planner/src/nars/mod.rs b/crates/lance-graph-planner/src/nars/mod.rs index 4e6b8393e..c3c265274 100644 --- a/crates/lance-graph-planner/src/nars/mod.rs +++ b/crates/lance-graph-planner/src/nars/mod.rs @@ -23,6 +23,7 @@ pub mod support; pub mod tactic_select; pub mod tactics; pub mod truth; +pub mod warrant; pub use basin_resonance::{rank_basins, Basin, BasinKind, ResonanceConfig}; pub use belief::{Belief, BeliefArena, CStmt, Copula, ReviseOutcome, Stamp}; diff --git a/crates/lance-graph-planner/src/nars/warrant.rs b/crates/lance-graph-planner/src/nars/warrant.rs new file mode 100644 index 000000000..e87436f33 --- /dev/null +++ b/crates/lance-graph-planner/src/nars/warrant.rs @@ -0,0 +1,681 @@ +//! `warrant`: which planner tactic may run on which grounded statements, and +//! what it may conclude (D-EPI-COT C3). +//! +//! A tactic runs only on [`Marker`]s. A marker is a statement whose evidence +//! comes from the [`DerivationLedger`] (truth and source roots) and whose +//! bits 59..63 project under a declared reading to an [`EpistemicState5`]. +//! [`fire`] checks every premise against the tactic's [`RecipeRule`], runs the +//! planner's own tactic function over the markers, admits each candidate into +//! the ledger, and returns [`Judgment`]s. +//! +//! # What a judgment may claim +//! +//! - **Truth:** the tactic's NARS truth over the premises' pooled evidence. +//! The ledger stays the authority: [`DerivationLedger::pooled`] answers for +//! the conclusion afterwards. +//! - **Roots:** the source roots of the proof through the new derivation, +//! which are the union of the premises' roots. A thought that replays the +//! same premises adds no root. +//! - **Epistemic state:** always `Unknown × Open`. A term-logic step earns no +//! certification and fixes no topology. Certification rises only through +//! `crate::pearl::reason` + `revise` (executed trial arms for `Causes`), and +//! topology only through `crate::pearl::hydrate`. Two `Causes` premises do +//! not make their deduction a cause: causation is not transitive in general. +//! - **Breadcrumb:** the [`ThoughtRef`] the step ran in (the 53..58 slot and +//! its generation). The operation is not written into the result. +//! +//! # The tactic law (policy pins) +//! +//! | recipe | tactic | requires | forbids | +//! |---|---|---|---| +//! | 4 | RCR abduction | `ASSOCIATED` | `INTERMEDIATE_KNOWN` | +//! | 6 | TR analogy | `ASSOCIATED` | — | +//! | 7 | ASC self-critique | `ASSOCIATED` | — | +//! | 8 | CAS induction / deduction | `ASSOCIATED` | — | +//! | 11 | CR revision | — | — | +//! +//! - DECISION: a Datapath tactic composes statements that have at least been +//! associated from independent sources; an `Open` statement has nothing to +//! compose. +//! - DECISION: RCR does not abduce a middle term for a relation whose mediator +//! is already known (the lab rule `HYDRATE_INTERMEDIATE` forbids the same). +//! - SCOPE: [`fire`] runs the Datapath tactics (4, 6, 8). ASC and CR are +//! revisions; in the ledger they are new observations, pooled by +//! [`DerivationLedger::pooled`]. +//! - BASIS: none measured; these are the smallest rules that make the +//! eligibility boundary testable. +//! - REVISIT WHEN: a tactic produces a measured wrong conclusion that a +//! stricter rule would have refused, or refuses a step a fixture needs. + +use std::collections::BTreeSet; + +use lance_graph_contract::band_reading::EdgeProvenance; +use lance_graph_contract::class_view::ClassId; +use lance_graph_contract::epistemic_state5::{ + fact, Certification3, Epi5Declarations, Epi5Gen, Epi5ReadError, EpistemicState5, RecipeRule, + Topology2, +}; +use lance_graph_contract::rail_geometry::RailAxis; + +use super::belief::{BeliefArena, CStmt, Stamp}; +use super::support::{ + Ablation, ChainId, DerivationId, DerivationLedger, NotAFigure, Refusal, SourceId, +}; +use super::tactics::{ + cas_abstract, rcr_abduce, tr_diverge, Throttle, ASC_ID, CAS_ID, CR_ID, RCR_ID, TR_ID, +}; +use super::truth::TruthValue; + +/// The thought a step ran in: the CE64 bits 53..58 slot (0 = WORLD) and the +/// slot's generation, so a reused slot is not mistaken for the old thought. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +pub struct ThoughtRef { + /// Slot `0..=63`. + pub slot: u8, + /// Generation of the slot. + pub generation: u32, +} + +/// Highest thought slot (six bits). +pub const MAX_SLOT: u8 = 63; + +/// The tactic law: a rule per recipe id. Recipes outside the table have no +/// rule and are never eligible. +#[must_use] +pub const fn tactic_rule(recipe: u8) -> Option { + match recipe { + RCR_ID => Some(RecipeRule::new(fact::ASSOCIATED, fact::INTERMEDIATE_KNOWN)), + TR_ID | ASC_ID | CAS_ID => Some(RecipeRule::new(fact::ASSOCIATED, 0)), + CR_ID => Some(RecipeRule::new(0, 0)), + _ => None, + } +} + +/// Where a statement's bits 59..63 came from and how they are declared. +#[derive(Clone, Copy)] +pub struct Declared<'a> { + /// The declarations. + pub declarations: &'a Epi5Declarations, + /// The statement's class. + pub class: ClassId, + /// The rail the class declared the reading on. + pub rail: RailAxis, + /// Where the bits came from. + pub provenance: EdgeProvenance, + /// The raw bits 59..63. + pub raw5: u8, +} + +/// A statement grounded in the ledger with a declared epistemic state. +/// Built only by [`Marker::ground`]. +#[derive(Debug, Clone, PartialEq)] +pub struct Marker { + stmt: CStmt, + truth: TruthValue, + roots: BTreeSet, + state: EpistemicState5, + thought: ThoughtRef, +} + +/// Why no marker was built. +#[derive(Debug, Clone, PartialEq)] +pub enum MarkerRefusal { + /// The ledger has no evidence for the statement. + NoEvidence(CStmt), + /// The ledger refused to evaluate. + Ledger(Refusal), + /// Bits 59..63 do not project under the declaration. + Epi5(Epi5ReadError), + /// The slot does not fit in six bits. + Slot(u8), +} + +impl Marker { + /// Ground `stmt`: truth and roots from the ledger's pooled evidence, + /// the state from the declared projection. + /// + /// # Errors + /// A [`MarkerRefusal`]. + pub fn ground( + ledger: &DerivationLedger, + stmt: CStmt, + declared: Declared<'_>, + thought: ThoughtRef, + ) -> Result { + if thought.slot > MAX_SLOT { + return Err(MarkerRefusal::Slot(thought.slot)); + } + let state = declared + .declarations + .project_state5( + declared.class, + declared.rail, + Epi5Gen::V1, + declared.raw5, + declared.provenance, + ) + .map_err(MarkerRefusal::Epi5)?; + let pooled = ledger + .pooled(stmt, &Ablation::none()) + .map_err(MarkerRefusal::Ledger)? + .ok_or(MarkerRefusal::NoEvidence(stmt))?; + Ok(Self { + stmt, + truth: pooled.truth, + roots: pooled.roots, + state, + thought, + }) + } + + /// The statement. + #[must_use] + pub fn stmt(&self) -> CStmt { + self.stmt + } + /// Its pooled truth when grounded. + #[must_use] + pub fn truth(&self) -> TruthValue { + self.truth + } + /// Its source roots when grounded. + #[must_use] + pub fn roots(&self) -> &BTreeSet { + &self.roots + } + /// Its declared epistemic state. + #[must_use] + pub fn state(&self) -> EpistemicState5 { + self.state + } + /// The thought it was grounded in. + #[must_use] + pub fn thought(&self) -> ThoughtRef { + self.thought + } +} + +/// A Datapath tactic step. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum Step { + /// RCR: abduction over every shared predicate (recipe 4). + Rcr, + /// TR: analogy from a focus statement (recipe 6). + Tr(CStmt), + /// CAS: induction and deduction around a focus subject (recipe 8). + Cas(u16), +} + +impl Step { + /// The recipe id the step implements. + #[must_use] + pub fn recipe(self) -> u8 { + match self { + Step::Rcr => RCR_ID, + Step::Tr(_) => TR_ID, + Step::Cas(_) => CAS_ID, + } + } +} + +/// What a step concluded. +#[derive(Debug, Clone, PartialEq)] +pub struct Judgment { + /// The conclusion. + pub stmt: CStmt, + /// The tactic's truth over the premises. + pub truth: TruthValue, + /// The derivation admitted into the ledger. + pub derivation: DerivationId, + /// Roots of the proof through that derivation. + pub roots: BTreeSet, + /// The thought the step ran in. + pub thought: ThoughtRef, + /// Always `Unknown × Open`: see the module documentation. + pub state: EpistemicState5, +} + +/// Why a step did not run, or stopped. +#[derive(Debug, Clone, PartialEq)] +pub enum FireRefusal { + /// No markers. + NoPremises, + /// Two markers name the same statement. + DuplicatePremise(CStmt), + /// The recipe has no rule. + NoRule(u8), + /// A premise's state does not satisfy the rule. + Ineligible { + /// The premise. + stmt: CStmt, + /// Its state. + state: EpistemicState5, + /// The recipe. + recipe: u8, + }, + /// A premise's ledger evidence changed after its marker was built. + Stale(CStmt), + /// The ledger refused. + Ledger(Refusal), + /// The ledger refused a candidate's figure. + Figure(NotAFigure), + /// No proof uses the admitted derivation. + NoProof(CStmt), +} + +/// The state every judgment carries. +pub const JUDGMENT_STATE: EpistemicState5 = + EpistemicState5::new(Epi5Gen::V1, Topology2::Unknown, Certification3::Open); + +/// Run `step` over `markers` in `chain`, as thought `thought`. +/// +/// Refuses before anything is admitted when a premise is ineligible or stale. +/// +/// # Errors +/// A [`FireRefusal`]. +pub fn fire( + ledger: &mut DerivationLedger, + chain: ChainId, + thought: ThoughtRef, + step: Step, + markers: &[Marker], +) -> Result, FireRefusal> { + if markers.is_empty() { + return Err(FireRefusal::NoPremises); + } + let recipe = step.recipe(); + let rule = tactic_rule(recipe).ok_or(FireRefusal::NoRule(recipe))?; + let mut arena = BeliefArena::new(); + let mut seen: Vec = Vec::new(); + for m in markers { + if seen.contains(&m.stmt) { + return Err(FireRefusal::DuplicatePremise(m.stmt)); + } + seen.push(m.stmt); + if !rule.admits(m.state) { + return Err(FireRefusal::Ineligible { + stmt: m.stmt, + state: m.state, + recipe, + }); + } + let now = ledger + .pooled(m.stmt, &Ablation::none()) + .map_err(FireRefusal::Ledger)?; + if now.as_ref().map(|p| (p.truth, &p.roots)) != Some((m.truth, &m.roots)) { + return Err(FireRefusal::Stale(m.stmt)); + } + let stamp = m + .roots + .iter() + .fold(Stamp(0), |s, &r| s.union(Stamp::source(r))); + arena.observe(m.stmt, m.truth, stamp); + } + + let throttle = Throttle::permissive(); + let frontier = match step { + Step::Rcr => rcr_abduce(&arena, &throttle), + Step::Tr(focus) => tr_diverge(&arena, focus), + Step::Cas(subject) => cas_abstract(&arena, subject, &throttle), + }; + + let mut out = Vec::with_capacity(frontier.candidates.len()); + for c in &frontier.candidates { + let derivation = ledger + .admit(chain, &arena, c) + .map_err(FireRefusal::Figure)?; + let roots = ledger + .proofs(c.stmt, &Ablation::none()) + .map_err(FireRefusal::Ledger)? + .into_iter() + .find(|p| p.uses.contains(&derivation)) + .map(|p| p.roots) + .ok_or(FireRefusal::NoProof(c.stmt))?; + out.push(Judgment { + stmt: c.stmt, + truth: c.truth, + derivation, + roots, + thought, + state: JUDGMENT_STATE, + }); + } + Ok(out) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::nars::belief::Copula; + use crate::pearl::{reason, revise, Edit, Evidence, Reading}; + use causal_edge::edge::{CausalEdge64, InferenceType}; + use causal_edge::{CausalMask, PlasticityState}; + use lance_graph_contract::causal_audit::SupportBasis; + use lance_graph_contract::certification::ModelBuilder; + use lance_graph_contract::epistemic_state5::Epi5Reading; + + const CLASS: ClassId = 0x0902; + const RAIL: RailAxis = RailAxis::Taxonomy; + const THOUGHT: ThoughtRef = ThoughtRef { + slot: 1, + generation: 1, + }; + + fn inh(s: u16, p: u16) -> CStmt { + CStmt { + s, + cop: Copula::Inh, + p, + } + } + + fn decls() -> Epi5Declarations { + let mut d = Epi5Declarations::new(); + d.declare( + CLASS, + RAIL, + Epi5Reading { + generation: Epi5Gen::V1, + }, + ); + d + } + + fn raw(t: Topology2, c: Certification3) -> u8 { + EpistemicState5::new(Epi5Gen::V1, t, c).raw() + } + + fn declared(d: &Epi5Declarations, raw5: u8) -> Declared<'_> { + Declared { + declarations: d, + class: CLASS, + rail: RAIL, + provenance: EdgeProvenance::V2Stamped, + raw5, + } + } + + /// `1 → 9` from source 1 and `2 → 9` from source 2: a shared predicate. + fn ledger() -> DerivationLedger { + let mut l = DerivationLedger::new(); + l.observe(inh(1, 9), TruthValue::new(0.9, 0.9), 1); + l.observe(inh(2, 9), TruthValue::new(0.8, 0.9), 2); + l + } + + fn markers(l: &DerivationLedger, d: &Epi5Declarations, raw5: u8) -> Vec { + [inh(1, 9), inh(2, 9)] + .into_iter() + .map(|s| Marker::ground(l, s, declared(d, raw5), THOUGHT).expect("grounded")) + .collect() + } + + /// The acceptance path: RCR runs on two grounded markers, its candidates + /// enter the ledger, and each judgment carries the tactic's truth, the + /// union of the premises' roots, the thought, and `Unknown × Open`. + #[test] + fn a_tactic_consumes_grounded_markers_and_keeps_their_roots() { + let d = decls(); + let mut l = ledger(); + let ms = markers(&l, &d, raw(Topology2::Direct, Certification3::Associated)); + let js = fire(&mut l, ChainId(1), THOUGHT, Step::Rcr, &ms).expect("eligible"); + + assert_eq!(js.len(), 2, "1→2 and 2→1"); + assert_eq!(l.derivations().len(), 2); + let both: BTreeSet = [1, 2].into_iter().collect(); + for j in &js { + assert_eq!(j.roots, both); + assert_eq!(j.thought, THOUGHT); + assert_eq!(j.state, JUDGMENT_STATE); + let pooled = l.pooled(j.stmt, &Ablation::none()).unwrap().unwrap(); + assert_eq!(pooled.truth, j.truth, "the ledger agrees with the tactic"); + } + let (rule, obs) = (TruthValue::new(0.8, 0.9), TruthValue::new(0.9, 0.9)); + let j12 = js.iter().find(|j| j.stmt == inh(1, 2)).expect("1→2"); + assert_eq!(j12.truth, rule.abduction(&obs)); + } + + /// Eligibility follows the declared facts only: `Open` refuses, the same + /// topology at `Associated` runs; for RCR a known mediator refuses where + /// an unknown one runs, while CAS takes both. A refusal admits nothing. + #[test] + fn eligibility_follows_the_declared_facts() { + let d = decls(); + let cases = [ + (Step::Rcr, Topology2::Direct, Certification3::Open, false), + ( + Step::Rcr, + Topology2::Direct, + Certification3::Associated, + true, + ), + ( + Step::Rcr, + Topology2::IndirectKnown, + Certification3::Associated, + false, + ), + ( + Step::Rcr, + Topology2::IndirectUnknown, + Certification3::Associated, + true, + ), + ( + Step::Cas(1), + Topology2::IndirectKnown, + Certification3::Associated, + true, + ), + ( + Step::Cas(1), + Topology2::Unknown, + Certification3::Open, + false, + ), + ]; + for (step, t, c, ok) in cases { + let mut l = ledger(); + let ms = markers(&l, &d, raw(t, c)); + let r = fire(&mut l, ChainId(1), THOUGHT, step, &ms); + match (ok, r) { + (true, Ok(_)) => {} + (false, Err(FireRefusal::Ineligible { recipe, .. })) => { + assert_eq!(recipe, step.recipe()); + assert!(l.derivations().is_empty(), "a refusal admits nothing"); + } + (_, other) => panic!("{step:?} on {t:?} × {c:?}: {other:?}"), + } + } + } + + /// No evidence, an undeclared class, untrusted provenance or an + /// out-of-range slot: no marker. + #[test] + fn a_marker_needs_evidence_and_a_declared_reading() { + let d = decls(); + let l = ledger(); + let ok = raw(Topology2::Direct, Certification3::Associated); + assert_eq!( + Marker::ground(&l, inh(3, 9), declared(&d, ok), THOUGHT), + Err(MarkerRefusal::NoEvidence(inh(3, 9))) + ); + let mut undeclared = declared(&d, ok); + undeclared.class = 0x0903; + assert_eq!( + Marker::ground(&l, inh(1, 9), undeclared, THOUGHT), + Err(MarkerRefusal::Epi5(Epi5ReadError::UndeclaredClass(0x0903))) + ); + let mut legacy = declared(&d, ok); + legacy.provenance = EdgeProvenance::V1Legacy; + assert!(matches!( + Marker::ground(&l, inh(1, 9), legacy, THOUGHT), + Err(MarkerRefusal::Epi5(Epi5ReadError::UnknownProvenance(_))) + )); + let far = ThoughtRef { + slot: 64, + generation: 0, + }; + assert_eq!( + Marker::ground(&l, inh(1, 9), declared(&d, ok), far), + Err(MarkerRefusal::Slot(64)) + ); + } + + /// Premises at `Causes` do not make a judgment a cause: every eligible + /// premise state yields `Unknown × Open`. The only promotion is an + /// executed trial through `pearl`: observation alone leaves the edge + /// `Open`, and the trial arms raise it. + #[test] + fn a_judgment_is_never_promoted_by_its_premises() { + let d = decls(); + let rule = tactic_rule(RCR_ID).unwrap(); + for t in Topology2::ALL { + for c in Certification3::ALL { + let state = EpistemicState5::new(Epi5Gen::V1, t, c); + if !rule.admits(state) { + continue; + } + let mut l = ledger(); + let ms = markers(&l, &d, state.raw()); + for j in fire(&mut l, ChainId(1), THOUGHT, Step::Rcr, &ms).unwrap() { + assert_eq!(j.state, JUDGMENT_STATE, "premises at {t:?} × {c:?}"); + } + } + } + + let edge = CausalEdge64::pack( + 1, + 0x91, + 2, + 200, + 200, + CausalMask::PO, + causal_edge::Orientation::from_code(0b101), + InferenceType::Deduction, + PlasticityState::S_HOT, + 0, + ) + .with_epistemic_raw5(JUDGMENT_STATE.raw()); + let reading = Reading { + declarations: &d, + class: CLASS, + rail: RAIL, + provenance: EdgeProvenance::V2Stamped, + }; + let mut b = ModelBuilder::new(); + b.cell(0, true, 5, 4); + b.cell(0, false, 5, 1); + b.sources(SupportBasis::DirectlyObserved, &[1, 2]); + let observed = b.build(); + let m = reason( + edge, + &Evidence { + model: &observed, + chain: None, + }, + Edit::None, + ); + let after = revise(&m, reading).unwrap(); + assert_eq!(after.epistemic_raw5(), JUDGMENT_STATE.raw()); + + b.arm(true, 6, 5); + b.arm(false, 6, 1); + b.sources(SupportBasis::InterventionBacked, &[10, 11]); + let trial = b.build(); + let m = reason( + edge, + &Evidence { + model: &trial, + chain: None, + }, + Edit::None, + ); + let after = revise(&m, reading).unwrap(); + assert_eq!( + EpistemicState5::decode(Epi5Gen::V1, after.epistemic_raw5()) + .unwrap() + .certification(), + Certification3::Causes + ); + } + + /// The same step in 63 thoughts admits 63 derivations, and the + /// conclusion's pooled truth and roots stay those of one. + #[test] + fn replaying_a_step_in_many_thoughts_adds_no_evidence() { + let d = decls(); + let mut l = ledger(); + let ms = markers(&l, &d, raw(Topology2::Direct, Certification3::Associated)); + let once = fire(&mut l, ChainId(1), THOUGHT, Step::Rcr, &ms).unwrap(); + let target = once[0].stmt; + let first = l.pooled(target, &Ablation::none()).unwrap().unwrap(); + for slot in 2..=MAX_SLOT { + let t = ThoughtRef { + slot, + generation: 1, + }; + fire(&mut l, ChainId(u32::from(slot)), t, Step::Rcr, &ms).unwrap(); + } + assert_eq!(l.derivations().len(), 2 * 63); + let after = l.pooled(target, &Ablation::none()).unwrap().unwrap(); + assert_eq!(after.truth, first.truth); + assert_eq!(after.roots, first.roots); + } + + /// A marker built before its statement's evidence changed is refused, + /// and nothing is admitted. + #[test] + fn a_stale_marker_is_refused() { + let d = decls(); + let mut l = ledger(); + let ms = markers(&l, &d, raw(Topology2::Direct, Certification3::Associated)); + l.observe(inh(1, 9), TruthValue::new(0.1, 0.9), 3); + assert_eq!( + fire(&mut l, ChainId(1), THOUGHT, Step::Rcr, &ms), + Err(FireRefusal::Stale(inh(1, 9))) + ); + assert!(l.derivations().is_empty()); + } + + /// CAS on a focus subject admits induction and deduction, each a valid + /// figure, with the tactic's truth. + #[test] + fn cas_deduction_runs_on_grounded_markers() { + let d = decls(); + let mut l = DerivationLedger::new(); + l.observe(inh(1, 5), TruthValue::new(0.9, 0.9), 1); + l.observe(inh(5, 7), TruthValue::new(0.8, 0.9), 2); + let st = raw(Topology2::Direct, Certification3::Associated); + let ms: Vec = [inh(1, 5), inh(5, 7)] + .into_iter() + .map(|s| Marker::ground(&l, s, declared(&d, st), THOUGHT).unwrap()) + .collect(); + let js = fire(&mut l, ChainId(1), THOUGHT, Step::Cas(1), &ms).unwrap(); + let ded = js + .iter() + .find(|j| j.stmt == inh(1, 7)) + .expect("1→7 by deduction"); + assert_eq!( + ded.truth, + TruthValue::new(0.8, 0.9).deduction(&TruthValue::new(0.9, 0.9)) + ); + assert_eq!(ded.roots, [1, 2].into_iter().collect()); + } + + #[test] + fn a_duplicate_premise_is_refused() { + let d = decls(); + let mut l = ledger(); + let mut ms = markers(&l, &d, raw(Topology2::Direct, Certification3::Associated)); + ms.push(ms[0].clone()); + assert_eq!( + fire(&mut l, ChainId(1), THOUGHT, Step::Rcr, &ms), + Err(FireRefusal::DuplicatePremise(inh(1, 9))) + ); + assert_eq!( + fire(&mut l, ChainId(1), THOUGHT, Step::Rcr, &[]), + Err(FireRefusal::NoPremises) + ); + } +} From 6deeceafc49aa486db56ed3c6e44dcbd7b34a3ec Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 28 Oct 2026 18:57:13 +0000 Subject: [PATCH 2/7] contract: unmeasured-outcome test covers unknown control units Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMPWTwovjYJEUMuGPb4 --- crates/lance-graph-contract/src/certification.rs | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/crates/lance-graph-contract/src/certification.rs b/crates/lance-graph-contract/src/certification.rs index 572e60053..5c2672011 100644 --- a/crates/lance-graph-contract/src/certification.rs +++ b/crates/lance-graph-contract/src/certification.rs @@ -515,6 +515,21 @@ mod tests { assert_eq!(m.causes(), Ok(true)); assert_eq!(m.measured_only(&measured).causes(), Ok(true)); + // Unknowns in the control arm: treated 1 of 4 measured, control 3 of + // 8 measured plus 8 unmeasured. Read as negatives the control rate + // is 3/16 and treated (1/4) looks higher; restricted it is 3/8 and + // treated is lower. + let mut b = ModelBuilder::new(); + b.sources(SupportBasis::InterventionBacked, &[1, 2]); + let (t, _) = b.arm(true, 4, 1); + let (c_known, _) = b.arm(false, 8, 3); + let (c_unknown, _) = b.arm(false, 8, 0); + let m = b.build(); + let measured = t.union(&c_known); + assert!(!c_unknown.intersects(&measured)); + assert_eq!(m.causes(), Ok(true), "unknown controls read as negatives"); + assert_eq!(m.measured_only(&measured).causes(), Ok(false)); + // An arm with no measured unit refuses instead of deciding. let (m, _) = build(2, 6); let control_only = m.trial.difference(&m.assigned); From 86afa383c51075cfb5de0e1e2c413a11aad9948f Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 28 Oct 2026 18:59:31 +0000 Subject: [PATCH 3/7] =?UTF-8?q?docs:=20C3=20first=20slice=20=E2=80=94=20ow?= =?UTF-8?q?ner=20map,=20falsifiers,=20open=20items?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMPWTwovjYJEUMuGPb4 --- docs/research/epistemic-cot/c3-plan.md | 93 +++++++++++++++++++++++++- 1 file changed, 91 insertions(+), 2 deletions(-) diff --git a/docs/research/epistemic-cot/c3-plan.md b/docs/research/epistemic-cot/c3-plan.md index ce2e4c04d..4e9e636f4 100644 --- a/docs/research/epistemic-cot/c3-plan.md +++ b/docs/research/epistemic-cot/c3-plan.md @@ -1,7 +1,7 @@ # D-EPI-COT C3 — plan: Epi5 bridge, scenting, numerical learning -Status: PLAN. Nothing here is implemented. C1/C2 (`nars::support`) is unchanged -by this document. +Status: PLAN, with the first C3 slice delivered (§8). C1/C2 (`nars::support`) +is unchanged. C3 has three parts, in this order: @@ -169,3 +169,92 @@ The learned output is a ranking. It is never passed in as an observation. 2. Whether the `learn` gate's behaviour on `deepnsm-v2` edges is a live defect, which depends on whether those edges ever reach `learn`. 3. Where the TFLite kernels live (§5). + +## 8. Delivered: first C3 slice + +Source pins: lance-graph main `694b243bd`, ndarray master `2cbe131`. + +### Owner and overlap map + +| file | owner contract | change | +|---|---|---| +| `lance-graph-contract/src/epistemic_state5.rs` | D-EPI-CANON-0 | adds `RecipeRule` (additive) | +| `lance-graph-contract/src/certification.rs` | P7a #1369 / D-PEARL-PROD-0 | adds `CertificationModel::measured_only` (additive) | +| `lance-graph-planner/src/nars/warrant.rs` | D-EPI-COT (new) | new module | +| `lance-graph-planner/src/pearl.rs` | D-PEARL-PROD-0 | unchanged; still the only writer of bits 59..63 | +| `cognitive-shader-driver/examples/shared/affordance_law.rs` | D-GSO-AFF-0 | unchanged; still uses its own rule type (follow-up) | + +EXO-50, read to its latest message (08:45Z): no open message claims these +files. Numeric admission stays with EXO-152. + +### What runs + +- **`RecipeRule`** (contract): `requires` / `forbids` over declared facts, a + per-state check and the V1 population. This moves the lab law's rule into the + contract. The lab still has its own copy; switching it over is a follow-up. +- **`CertificationModel::measured_only`** (contract): units whose outcome + was not measured are excluded from every mask, including the trial arms, + instead of being read as negatives. An arm left with no measured unit + refuses with `EmptyArm`. +- **`nars::warrant`** (planner): + - **`Marker::ground`** builds a marker from three things: the ledger's + pooled truth and roots, the bits 59..63 projected through + `Epi5Declarations`, and the thought slot and generation. It refuses + with `NoEvidence`, an `Epi5` read error, or `Slot`. + - **`tactic_rule`** gives the eligibility rule for recipes 4, 6, 7, 8 + and 11. These are policy pins, documented in the module. + - **`fire`**: + 1. checks every premise against its rule; + 2. refuses a stale or duplicate marker; + 3. runs the planner's own RCR, TR or CAS function; + 4. admits each candidate through `DerivationLedger::admit`. + + Each judgment carries the tactic's truth, the roots of the proof through + the new derivation, the thought, and `Unknown × Open`. + +### Falsifiers + +Each is disable-verified: the named disable turns its test red. + +| falsifier | test | disable | +|---|---|---| +| acceptance path, roots preserved | `a_tactic_consumes_grounded_markers_and_keeps_their_roots` | — | +| eligibility follows declared facts | `eligibility_follows_the_declared_facts` | skip the rule check; drop RCR's `forbids` | +| no marker without evidence or declaration | `a_marker_needs_evidence_and_a_declared_reading` | skip the slot check | +| no promotion from premises; only trial arms promote | `a_judgment_is_never_promoted_by_its_premises` | judgment takes a premise's state | +| replayed thoughts add no evidence | `replaying_a_step_in_many_thoughts_adds_no_evidence` | — (ledger L7) | +| stale marker refused | `a_stale_marker_is_refused` | skip the staleness check | +| duplicate premise refused | `a_duplicate_premise_is_refused` | skip the duplicate check | +| UNKNOWN is not negative | `unmeasured_outcomes_are_not_read_as_negatives` | trial arms not restricted (red only after adding unmeasured control units) | +| rule population | `a_recipe_rule_population_matches_its_per_state_check` | `holds` ignores `forbids` | + +L1–L5 are already pinned by `pearl.rs` tests; this slice does not duplicate +them: + +- L1: `f1_observation_alone_never_promotes_to_causes`. +- L2 and L3: `cui_bono_script_moves_the_state_only_where_evidence_earned_it`, + which ends at `IndirectKnown × Causes`. +- L4: `hydration_only_promotes_the_edge_whose_path_it_is` and + `f5_a_proposed_beneficiary_is_not_evidence`. +- L5: `f7_one_at_a_time_removal_is_not_the_definition_of_causality`, the + overdetermined trial. + +### Clippy + +`cargo clippy -p lance-graph-planner --lib --tests -D warnings` reports the +same 8 sites on main `694b243bd` as on this branch: +`nested_bands.rs` 601/978/1025, `cache/nars_engine.rs:1413` and +`tests/moore_nars16_probe.rs`. `--lib` alone is clean. + +### Still open + +- **Statistics:** effect size, sample-size bounds, uncertainty, and + multiple-comparison correction across the up to five populations + `associated` tries. Today `CertificationModel` reports none of these, and + nothing here asserts more than it reports. +- **Missingness:** missing-at-random is assumed by `measured_only`; it is + not tested. +- **ASC and CR (7, 11)** are not run through `fire`. They are revisions, + and the ledger already pools them. +- **The lab affordance law** still has its own rule type. +- **C3b and C3c,** which wait on the decisions in §7. From 89e90d91fb6c1c19c56ae923a8e8bba26a2e56ea Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 28 Oct 2026 19:00:11 +0000 Subject: [PATCH 4/7] board: D-EPI-COT C3 first slice entry Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMPWTwovjYJEUMuGPb4 --- .../2026-10-28-d-epi-cot-c3-warrant.md | 34 +++++++++++++++++++ .claude/board/entries/README.md | 3 +- 2 files changed, 36 insertions(+), 1 deletion(-) create mode 100644 .claude/board/entries/2026-10-28-d-epi-cot-c3-warrant.md diff --git a/.claude/board/entries/2026-10-28-d-epi-cot-c3-warrant.md b/.claude/board/entries/2026-10-28-d-epi-cot-c3-warrant.md new file mode 100644 index 000000000..e0f81f8af --- /dev/null +++ b/.claude/board/entries/2026-10-28-d-epi-cot-c3-warrant.md @@ -0,0 +1,34 @@ +# D-EPI-COT-C3 (first slice): tactics run only on grounded, Epi5-eligible markers + +**Status:** TEST-PINNED. Code: +- `crates/lance-graph-planner/src/nars/warrant.rs` +- `epistemic_state5::RecipeRule` +- `certification::CertificationModel::measured_only` + +Plan: `docs/research/epistemic-cot/c3-plan.md` §8. + +## Decision + +- **SCOPE:** a planner tactic (RCR 4, TR 6, CAS 8) runs only on `Marker`s. A marker is three things together: + - the ledger's pooled truth and roots; + - bits 59..63 projected through `Epi5Declarations`; + - a thought slot and generation. + + Each premise must satisfy the recipe's `RecipeRule`. The rule's requires/forbids are policy pins: Associated for 4/6/7/8, and no intermediate-known for RCR. +- **Judgments** carry the tactic's truth, the proof's roots, the thought, and `Unknown × Open`. A term-logic step earns no certification. The only promotion is `pearl::reason` + `revise` over executed trial arms (pinned in the same test). +- **`measured_only`:** an unmeasured outcome is excluded, not read as negative. That includes trial arms, which `causes` reads without the universe. + +## Evidence + +- 9 new tests. 9 disables, each red. +- One disable (trial arms unrestricted) was green on the first fixture: every control unit was measured. An unmeasured-control fixture was added before recording. +- Planner lib 485 pass; contract lib 1561 pass. +- Clippy `--lib --tests` reports the same 8 sites as main `694b243bd`. + +## Open + +- Effect size, sample size, uncertainty and multiple comparisons are still unreported by `CertificationModel`. +- Missing-at-random is assumed. +- ASC and CR are not run through `fire`. +- The lab affordance law still has its own rule type. +- C3b and C3c wait on the bits 50..52 order decision and the TFLite location. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 6f379afec..a6f8e64ef 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,13 +25,14 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately opposite directions; the stranding this convention prevents shows up in exactly one of them, never both. -497 entries, 2026-08-06 .. 2026-10-28. +498 entries, 2026-08-06 .. 2026-10-28. | date | entry id | finding | file | |---|---|---|---| | 2026-10-28 | `thought-layers-nan-skip` | | [2026-10-28-thought-layers-nan-skip.md](2026-10-28-thought-layers-nan-skip.md) | | 2026-10-28 | `lane-layout-from-classview` | | [2026-10-28-lane-layout-from-classview.md](2026-10-28-lane-layout-from-classview.md) | | 2026-10-28 | `D-SAG-6-1` | | [2026-10-28-d-sag-6-1-audit-reference-ledger.md](2026-10-28-d-sag-6-1-audit-reference-ledger.md) | +| 2026-10-28 | `D-EPI-COT-C3` | | [2026-10-28-d-epi-cot-c3-warrant.md](2026-10-28-d-epi-cot-c3-warrant.md) | | 2026-10-28 | `D-EPI-COT` | | [2026-10-28-d-epi-cot-c0-c2.md](2026-10-28-d-epi-cot-c0-c2.md) | | 2026-10-28 | `D-DT64-6` | | [2026-10-28-d-dt64-6-routing-bindstore-behavior.md](2026-10-28-d-dt64-6-routing-bindstore-behavior.md) | | 2026-10-28 | `D-DT64-6-1a` | | [2026-10-28-d-dt64-6-ogit-predicates-impl.md](2026-10-28-d-dt64-6-ogit-predicates-impl.md) | From 00a70e8bb449dba056a5c1335b4854d619e71211 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 28 Oct 2026 19:03:17 +0000 Subject: [PATCH 5/7] planner: ledger-to-pearl::hydrate mediator seam; explicit deduction chains Impl - nars::mediator::hydrate_from_ledger: finds the ledger's grounded deductions of A->Y through B, hands the path to the existing pearl::hydrate, and returns the receipt (derivations, roots, hydration, the edge after hydrate, sensitivity with the mediated path removed). Refuses without a grounded ledger path; the sealed chain alone decides topology. Reads step subject/object only (#1572). - support::Law::Deduction now admits Impl in an explicit step (never closure; Rel still never composes), so causal mediator paths can be recorded. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMPWTwovjYJEUMuGPb4 --- .../lance-graph-planner/src/nars/mediator.rs | 353 ++++++++++++++++++ crates/lance-graph-planner/src/nars/mod.rs | 1 + .../lance-graph-planner/src/nars/support.rs | 23 +- 3 files changed, 376 insertions(+), 1 deletion(-) create mode 100644 crates/lance-graph-planner/src/nars/mediator.rs diff --git a/crates/lance-graph-planner/src/nars/mediator.rs b/crates/lance-graph-planner/src/nars/mediator.rs new file mode 100644 index 000000000..f22682c22 --- /dev/null +++ b/crates/lance-graph-planner/src/nars/mediator.rs @@ -0,0 +1,353 @@ +//! `mediator`: the seam from the derivation ledger to `pearl::hydrate` +//! (D-EPI-COT C3a). +//! +//! The ledger (#1840) can hold a grounded deduction `A → Y` through a +//! mediator `B`. That is a reasoning result, not a source-attested chain. +//! [`hydrate_from_ledger`] hands the step to the existing topology gate, +//! [`crate::pearl::hydrate`], and leaves the decision there: +//! +//! - the ledger supplies the receipt: which derivations go through `B`, their +//! source roots, and what removing them does to `A → Y`; +//! - the sealed chain decides the topology. `IndirectUnknown` becomes +//! `IndirectKnown` only when both `A → B` and `B → Y` are bindings in the +//! sealed chain. A ledger path whose links are not in the chain changes +//! nothing; +//! - certification never moves here. +//! +//! The adapter refuses when the ledger has no grounded path through `B`, so a +//! hydration it reports always has a ledger receipt behind it. It reads only +//! the subject and object of each chain step, as `pearl::hydrate` does; the +//! step's `u8` tag is not a predicate (the withdrawn #1572 guard). + +use std::collections::BTreeSet; + +use causal_edge::edge::CausalEdge64; +use lance_graph_contract::epistemic_state5::Epi5ReadError; + +use super::belief::CStmt; +use super::support::{ + Ablation, DerivationId, DerivationLedger, Law, Refusal, Sensitivity, SourceId, +}; +use crate::chain_replay::ChainStep; +use crate::pearl::{hydrate, Hydration, Reading}; + +/// What the ledger and the sealed chain said about `A → Y` through `B`. +#[derive(Debug, Clone, PartialEq)] +pub struct MediatorReceipt { + /// Grounded deductions of `A → Y` through `B`. + pub derivations: Vec, + /// Source roots of the proofs through them. + pub roots: BTreeSet, + /// What `pearl::hydrate` found in the sealed chain. + pub hydration: Hydration, + /// The edge after `pearl::hydrate`. + pub edge: CausalEdge64, + /// `A → Y` with and without the derivations through `B`. + pub mediated: Sensitivity, +} + +/// Why no receipt was produced. +#[derive(Debug, Clone, PartialEq)] +pub enum MediatorRefusal { + /// A term does not fit the edge's 8-bit index. + TermRange(u16), + /// The edge is not the relation `A → Y`. + EdgeMismatch, + /// The ledger has no grounded deduction of `A → Y` through `B`. + NoLedgerPath, + /// The ledger refused to evaluate. + Ledger(Refusal), + /// The edge's bits 59..63 do not project. + Epi5(Epi5ReadError), +} + +fn idx(term: u16) -> Result { + u8::try_from(term).map_err(|_| MediatorRefusal::TermRange(term)) +} + +/// Hand a ledger path `A → B → Y` to `pearl::hydrate` for the edge `A → Y`. +/// +/// # Errors +/// A [`MediatorRefusal`]. +pub fn hydrate_from_ledger( + ledger: &DerivationLedger, + edge: CausalEdge64, + target: CStmt, + mediator: u16, + sealed: &[ChainStep], + reading: Reading<'_>, +) -> Result { + let (a, b, y) = (idx(target.s)?, idx(mediator)?, idx(target.p)?); + if edge.s_idx() != a || edge.o_idx() != y { + return Err(MediatorRefusal::EdgeMismatch); + } + + let first = CStmt { + s: target.s, + cop: target.cop, + p: mediator, + }; + let second = CStmt { + s: mediator, + cop: target.cop, + p: target.p, + }; + let through: Vec = ledger + .derivations() + .iter() + .enumerate() + .filter(|(_, d)| { + d.law == Law::Deduction + && d.conclusion == target + && (d.premises == [first, second] || d.premises == [second, first]) + }) + .map(|(i, _)| DerivationId(i as u32)) + .collect(); + + let proofs = ledger + .proofs(target, &Ablation::none()) + .map_err(MediatorRefusal::Ledger)?; + let mut derivations = Vec::new(); + let mut roots = BTreeSet::new(); + for id in through { + if let Some(p) = proofs.iter().find(|p| p.uses.contains(&id)) { + derivations.push(id); + roots.extend(p.roots.iter().copied()); + } + } + if derivations.is_empty() { + return Err(MediatorRefusal::NoLedgerPath); + } + + let (edge, hydration) = + hydrate(edge, (a, b, y), sealed, reading).map_err(MediatorRefusal::Epi5)?; + let mediated = ledger + .sensitivity(target, &Ablation::derivations(&derivations)) + .map_err(MediatorRefusal::Ledger)?; + Ok(MediatorReceipt { + derivations, + roots, + hydration, + edge, + mediated, + }) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::nars::belief::Copula; + use crate::nars::support::ChainId; + use crate::nars::truth::TruthValue; + use causal_edge::edge::InferenceType; + use causal_edge::{CausalMask, PlasticityState}; + use lance_graph_contract::band_reading::EdgeProvenance; + use lance_graph_contract::class_view::ClassId; + use lance_graph_contract::epistemic_state5::{ + Certification3, Epi5Declarations, Epi5Gen, Epi5Reading, EpistemicState5, Topology2, + }; + use lance_graph_contract::rail_geometry::RailAxis; + + const CLASS: ClassId = 0x0902; + const RAIL: RailAxis = RailAxis::Taxonomy; + const A: u16 = 10; + const B: u16 = 20; + const C: u16 = 25; + const Y: u16 = 30; + + fn imp(s: u16, p: u16) -> CStmt { + CStmt { + s, + cop: Copula::Impl, + p, + } + } + + fn decls() -> Epi5Declarations { + let mut d = Epi5Declarations::new(); + d.declare( + CLASS, + RAIL, + Epi5Reading { + generation: Epi5Gen::V1, + }, + ); + d + } + + fn reading(d: &Epi5Declarations) -> Reading<'_> { + Reading { + declarations: d, + class: CLASS, + rail: RAIL, + provenance: EdgeProvenance::V2Stamped, + } + } + + fn edge(s: u16, o: u16, t: Topology2, c: Certification3) -> CausalEdge64 { + CausalEdge64::pack( + s as u8, + 0x91, + o as u8, + 200, + 200, + CausalMask::SO, + causal_edge::Orientation::from_code(0b101), + InferenceType::Deduction, + PlasticityState::S_HOT, + 0, + ) + .with_epistemic_raw5(EpistemicState5::new(Epi5Gen::V1, t, c).raw()) + } + + fn state(e: CausalEdge64) -> (Topology2, Certification3) { + let s = EpistemicState5::decode(Epi5Gen::V1, e.epistemic_raw5()).unwrap(); + (s.topology(), s.certification()) + } + + /// `A → B` from source 1, `B → Y` from source 2, and their deduction. + fn ledger_through(m: u16) -> DerivationLedger { + let mut l = DerivationLedger::new(); + l.observe(imp(A, m), TruthValue::new(0.9, 0.9), 1); + l.observe(imp(m, Y), TruthValue::new(0.9, 0.9), 2); + l.derive( + ChainId(1), + Law::Deduction, + [imp(m, Y), imp(A, m)], + imp(A, Y), + ) + .unwrap(); + l + } + + /// Sealed steps; the `u8` tag is deliberately not the predicate. + fn sealed(links: &[(u16, u16)]) -> Vec { + links + .iter() + .map(|&(s, o)| { + ( + 0xFF, + edge(s, o, Topology2::Direct, Certification3::Associated), + ) + }) + .collect() + } + + fn query() -> CausalEdge64 { + edge(A, Y, Topology2::IndirectUnknown, Certification3::Causes) + } + + /// Ledger and chain agree: `IndirectUnknown × Causes` (raw5 22) becomes + /// `IndirectKnown × Causes` (raw5 21), with the ledger's roots, and the + /// mediated path carries the conclusion. + #[test] + fn a_ledger_path_witnessed_by_the_chain_hydrates() { + let d = decls(); + let l = ledger_through(B); + let r = hydrate_from_ledger( + &l, + query(), + imp(A, Y), + B, + &sealed(&[(A, B), (B, Y)]), + reading(&d), + ) + .unwrap(); + assert_eq!(r.hydration, Hydration::Hydrated); + assert_eq!( + state(r.edge), + (Topology2::IndirectKnown, Certification3::Causes) + ); + assert_eq!(r.edge.epistemic_raw5(), 21); + assert_eq!(r.roots, [1, 2].into_iter().collect()); + assert!(!r.mediated.survives(), "the only path goes through B"); + } + + /// A ledger path whose links are not both in the sealed chain does not + /// hydrate: the edge keeps raw5 22. + #[test] + fn a_ledger_path_alone_does_not_hydrate() { + let d = decls(); + let l = ledger_through(B); + for links in [&[(A, B)][..], &[][..]] { + let r = hydrate_from_ledger(&l, query(), imp(A, Y), B, &sealed(links), reading(&d)) + .unwrap(); + assert_ne!(r.hydration, Hydration::Hydrated); + assert_eq!(r.edge, query()); + } + } + + /// No grounded ledger path through `B`: refused, even when the chain has + /// both links. Covers no derivation, a derivation through another + /// mediator, and a derivation whose premise has no evidence. + #[test] + fn the_adapter_needs_a_grounded_ledger_path_through_the_mediator() { + let d = decls(); + let chain = sealed(&[(A, B), (B, Y)]); + let run = |l: &DerivationLedger| { + hydrate_from_ledger(l, query(), imp(A, Y), B, &chain, reading(&d)) + }; + + assert_eq!( + run(&DerivationLedger::new()), + Err(MediatorRefusal::NoLedgerPath) + ); + assert_eq!(run(&ledger_through(C)), Err(MediatorRefusal::NoLedgerPath)); + + let mut ungrounded = DerivationLedger::new(); + ungrounded.observe(imp(B, Y), TruthValue::new(0.9, 0.9), 2); + ungrounded + .derive( + ChainId(1), + Law::Deduction, + [imp(B, Y), imp(A, B)], + imp(A, Y), + ) + .unwrap(); + assert_eq!(run(&ungrounded), Err(MediatorRefusal::NoLedgerPath)); + } + + /// With an independent direct observation of `A → Y`, removing the + /// mediated path leaves the conclusion: the path through `B` is not + /// individually necessary, though it still hydrates. + #[test] + fn a_redundant_mediated_path_is_not_reported_as_necessary() { + let d = decls(); + let mut l = ledger_through(B); + l.observe(imp(A, Y), TruthValue::new(0.8, 0.9), 3); + let r = hydrate_from_ledger( + &l, + query(), + imp(A, Y), + B, + &sealed(&[(A, B), (B, Y)]), + reading(&d), + ) + .unwrap(); + assert_eq!(r.hydration, Hydration::Hydrated); + assert!(r.mediated.survives()); + assert_eq!(r.mediated.after.unwrap().roots, [3].into_iter().collect()); + } + + #[test] + fn the_edge_must_be_the_target_relation() { + let d = decls(); + let l = ledger_through(B); + let other = edge(A, B, Topology2::IndirectUnknown, Certification3::Causes); + assert_eq!( + hydrate_from_ledger( + &l, + other, + imp(A, Y), + B, + &sealed(&[(A, B), (B, Y)]), + reading(&d) + ), + Err(MediatorRefusal::EdgeMismatch) + ); + assert_eq!( + hydrate_from_ledger(&l, query(), imp(A, Y), 300, &[], reading(&d)), + Err(MediatorRefusal::TermRange(300)) + ); + } +} diff --git a/crates/lance-graph-planner/src/nars/mod.rs b/crates/lance-graph-planner/src/nars/mod.rs index c3c265274..3259a432d 100644 --- a/crates/lance-graph-planner/src/nars/mod.rs +++ b/crates/lance-graph-planner/src/nars/mod.rs @@ -15,6 +15,7 @@ pub mod ghost_prior; pub mod inference; pub mod insight; pub mod insights; +pub mod mediator; pub mod meta_basin; pub mod reach_out; pub mod regulate; diff --git a/crates/lance-graph-planner/src/nars/support.rs b/crates/lance-graph-planner/src/nars/support.rs index 00e00b33d..5df2dfd88 100644 --- a/crates/lance-graph-planner/src/nars/support.rs +++ b/crates/lance-graph-planner/src/nars/support.rs @@ -103,6 +103,17 @@ pub enum Refusal { Pool, } +/// Whether an explicit deduction step may chain two statements of `cop`. +/// +/// Wider than [`Copula::transits`], which governs blanket closure: `Impl` is +/// never closed transitively, but an admitted step may chain it, as the +/// copula's own documentation requires ("causal chaining goes through explicit +/// tactics"). The step earns NARS truth only; it certifies no cause. `Rel` +/// never composes. +fn composes(cop: Copula) -> bool { + matches!(cop, Copula::Inh | Copula::Sim | Copula::Impl) +} + /// The NARS law a derivation applies, as [`TruthValue`] implements it. #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum Law { @@ -136,7 +147,7 @@ impl Law { let [a, b] = premises; let drawn = match self { Law::Deduction => { - if a.cop != b.cop || !a.cop.transits() { + if a.cop != b.cop || !composes(a.cop) { return None; } if a.s == b.p { @@ -1044,6 +1055,16 @@ mod tests { assert!(l .derive(A, Law::Deduction, [rel(1, 2), rel(2, 3)], rel(1, 3)) .is_err()); + // An explicit implication step chains, though closure never would. + let imp = |s, p| CStmt { + s, + cop: Copula::Impl, + p, + }; + let mut chained = DerivationLedger::new(); + assert!(chained + .derive(A, Law::Deduction, [imp(1, 2), imp(2, 3)], imp(1, 3)) + .is_ok()); assert!(l.derivations().is_empty()); assert!(l.grounded_since(0).unwrap().is_empty()); assert!(l From 093f4622d364cce29167b01ab2f097c6e3c5fae4 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 28 Oct 2026 19:05:02 +0000 Subject: [PATCH 6/7] docs: C3 ledger-to-hydrate seam, maturation order and TFLite location Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMPWTwovjYJEUMuGPb4 --- .../2026-10-28-d-epi-cot-c3-warrant.md | 8 +++ docs/research/epistemic-cot/c3-plan.md | 69 +++++++++++++++++++ 2 files changed, 77 insertions(+) diff --git a/.claude/board/entries/2026-10-28-d-epi-cot-c3-warrant.md b/.claude/board/entries/2026-10-28-d-epi-cot-c3-warrant.md index e0f81f8af..e8f92ee76 100644 --- a/.claude/board/entries/2026-10-28-d-epi-cot-c3-warrant.md +++ b/.claude/board/entries/2026-10-28-d-epi-cot-c3-warrant.md @@ -32,3 +32,11 @@ Plan: `docs/research/epistemic-cot/c3-plan.md` §8. - ASC and CR are not run through `fire`. - The lab affordance law still has its own rule type. - C3b and C3c wait on the bits 50..52 order decision and the TFLite location. + +## Addendum, same day: ledger → `pearl::hydrate` + +- `nars::mediator::hydrate_from_ledger` connects the ledger's grounded deductions of `A → Y` through `B` to the unchanged `pearl::hydrate`. It returns derivations, roots, the `Hydration` result, the edge and the mediated-path sensitivity. +- The ledger never creates a chain, and a path the chain does not witness leaves the edge unchanged. A chain-only path has no ledger receipt and is refused. +- `Law::Deduction` admits `Impl` in an explicit step: never closure, and `Rel` never composes. +- 5 tests; 5 disables red. The first grounding disable did not bind (no proofs exist without evidence); it was replaced before recording. +- Maturation order for new declared readings is `7 = Staunen … 0 = Wisdom`. The TFLite kernels are in ndarray. diff --git a/docs/research/epistemic-cot/c3-plan.md b/docs/research/epistemic-cot/c3-plan.md index 4e9e636f4..1e5d513e1 100644 --- a/docs/research/epistemic-cot/c3-plan.md +++ b/docs/research/epistemic-cot/c3-plan.md @@ -258,3 +258,72 @@ same 8 sites on main `694b243bd` as on this branch: and the ledger already pools them. - **The lab affordance law** still has its own rule type. - **C3b and C3c,** which wait on the decisions in §7. + +## 9. Ledger → `pearl::hydrate` seam + +**Existing:** `planner::pearl::{reason, revise, hydrate}` (#1390/#1391) already +writes bits 59..63. `hydrate` moves `IndirectUnknown` to `IndirectKnown` when +both bindings `A → B` and `B → Y` are in the sealed chain. None of the files +named `hydrate.rs` is that gate: + +- `deepnsm-v2/src/hydrate.rs` addresses parsed triples to their verse; +- `lance-graph/src/graph/hydrate.rs` loads bgz7 vectors into Lance; +- `bgz-tensor/src/hydrate.rs` is a download binary. + +**Added:** `nars::mediator::hydrate_from_ledger`. + +1. It finds the ledger's grounded deductions of `A → Y` through `B`. +2. It hands the path to the unchanged `pearl::hydrate`. +3. It returns a receipt: derivation ids, source roots, the `Hydration` + result, the edge after `hydrate`, and `A → Y`'s sensitivity with the + mediated derivations removed. + +What each side is allowed to do: + +- **The ledger never creates a chain.** A ledger path whose links are not + both in the sealed chain leaves the edge unchanged. +- **The adapter refuses a chain-only path.** If the ledger has no grounded + path through `B`, there is no receipt. +- **Only subject and object are read** from each chain step. The step tag is + not a predicate; that was the #1572 guard, which was withdrawn. + +To record causal mediator paths, `Law::Deduction` now admits `Impl` in an +explicit step: + +- `Copula::transits` still keeps `Impl` out of blanket closure, and `Rel` + still never composes. +- The step earns NARS truth only. It certifies nothing. + +| falsifier | test | disable | +|---|---|---| +| chain-witnessed ledger path hydrates (raw5 22 → 21) with roots | `a_ledger_path_witnessed_by_the_chain_hydrates` | — | +| ledger path alone does not hydrate | `a_ledger_path_alone_does_not_hydrate` | — (`pearl::hydrate` owns it) | +| grounded path through B required | `the_adapter_needs_a_grounded_ledger_path_through_the_mediator` | accept ungrounded derivations; accept any mediator | +| redundant mediated path not reported as necessary | `a_redundant_mediated_path_is_not_reported_as_necessary` | — | +| edge must be the target | `the_edge_must_be_the_target_relation` | skip the edge check | +| `Impl` chains, `Rel` never | `l8_an_invalid_figure_is_not_admitted` | `Rel` composes; `Impl` refused | + +**One disable did not bind on its first form.** Falling back to "any proof" +changed nothing, because without evidence there are no proofs at all. +Accepting derivations without a proof does bind, and that is the form +recorded. + +**Maturation (operator, 2026-10-28):** `7 = Staunen … 0 = Wisdom` (the #1494 +order) is the order for new, explicitly declared maturation readings. + +- Wisdom stays revisable: an independently witnessed contradiction reopens + it. +- No existing class is reinterpreted. `deepnsm-v2` keeps its opposite + `novelty_wisdom` order. +- Before any production write, four things must be settled: the reading, + its provenance, a migration, and the `CausalEdge64::learn` collision. +- Until then, maturation stays transient and fail-closed. + +**TFLite (operator, 2026-10-28):** the kernels are in `AdaWorldAPI/ndarray`: + +- `src/simd_fixedpoint.rs`: TFLite fixed-point arithmetic; +- `src/simd_stride.rs`: `lut9`; +- `src/hpc/codec9.rs`: Palette512. + +`AdaWorldAPI/tflite-micro` is the reference, and lance-graph #1800 has the +softmax oracle. No `lance-graph-tflite` crate. No training kernel exists yet. From ace782d0f850a61cbf26a0389110f62c9df85b4b Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 28 Oct 2026 19:15:38 +0000 Subject: [PATCH 7/7] planner: a judgment reports the truth of its admitted proof A premise whose pooled evidence runs through the conclusion loses that evidence in the admitted proof (cycle guard). The judgment now returns that proof's truth together with its roots instead of the tactic's snapshot truth (codex P2). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMPWTwovjYJEUMuGPb4 --- .../lance-graph-planner/src/nars/warrant.rs | 60 ++++++++++++++++--- 1 file changed, 52 insertions(+), 8 deletions(-) diff --git a/crates/lance-graph-planner/src/nars/warrant.rs b/crates/lance-graph-planner/src/nars/warrant.rs index e87436f33..a80ca1937 100644 --- a/crates/lance-graph-planner/src/nars/warrant.rs +++ b/crates/lance-graph-planner/src/nars/warrant.rs @@ -10,9 +10,11 @@ //! //! # What a judgment may claim //! -//! - **Truth:** the tactic's NARS truth over the premises' pooled evidence. -//! The ledger stays the authority: [`DerivationLedger::pooled`] answers for -//! the conclusion afterwards. +//! - **Truth:** the truth of the ledger proof through the new derivation, +//! returned with that proof's roots. It equals the tactic's own truth +//! unless a premise's evidence depends on the conclusion itself: the +//! ledger's cycle guard drops that evidence from the proof, and the +//! judgment reports what the proof actually rests on. //! - **Roots:** the source roots of the proof through the new derivation, //! which are the union of the premises' roots. A thought that replays the //! same premises adds no root. @@ -223,7 +225,7 @@ impl Step { pub struct Judgment { /// The conclusion. pub stmt: CStmt, - /// The tactic's truth over the premises. + /// The truth of the proof through [`Self::derivation`]. pub truth: TruthValue, /// The derivation admitted into the ledger. pub derivation: DerivationId, @@ -324,18 +326,17 @@ pub fn fire( let derivation = ledger .admit(chain, &arena, c) .map_err(FireRefusal::Figure)?; - let roots = ledger + let proof = ledger .proofs(c.stmt, &Ablation::none()) .map_err(FireRefusal::Ledger)? .into_iter() .find(|p| p.uses.contains(&derivation)) - .map(|p| p.roots) .ok_or(FireRefusal::NoProof(c.stmt))?; out.push(Judgment { stmt: c.stmt, - truth: c.truth, + truth: proof.truth, derivation, - roots, + roots: proof.roots, thought, state: JUDGMENT_STATE, }); @@ -600,6 +601,49 @@ mod tests { ); } + /// A premise whose pooled evidence runs through the conclusion: `1 → 9` + /// is observed weakly and also derived through `1 → 2`. RCR then + /// proposes `1 → 2` from `1 → 9` and `2 → 9`. The admitted proof cannot + /// use the derivation through `1 → 2` (it would support itself), so the + /// judgment carries the proof's weaker truth and its roots, not the + /// snapshot truth. + #[test] + fn a_judgment_reports_the_truth_its_roots_support() { + let d = decls(); + let mut l = DerivationLedger::new(); + l.observe(inh(1, 2), TruthValue::new(0.9, 0.9), 1); + l.observe(inh(2, 9), TruthValue::new(0.9, 0.9), 2); + l.observe(inh(1, 9), TruthValue::new(0.1, 0.1), 3); + l.derive( + ChainId(0), + crate::nars::support::Law::Deduction, + [inh(1, 2), inh(2, 9)], + inh(1, 9), + ) + .unwrap(); + let st = raw(Topology2::Direct, Certification3::Associated); + let ms: Vec = [inh(1, 9), inh(2, 9)] + .into_iter() + .map(|s| Marker::ground(&l, s, declared(&d, st), THOUGHT).unwrap()) + .collect(); + let js = fire(&mut l, ChainId(1), THOUGHT, Step::Rcr, &ms).unwrap(); + let j = js.iter().find(|j| j.stmt == inh(1, 2)).expect("1→2"); + let snapshot = ms[1].truth().abduction(&ms[0].truth()); + assert!(j.truth.confidence < snapshot.confidence / 10.0); + let proof = l + .proofs(inh(1, 2), &Ablation::none()) + .unwrap() + .into_iter() + .find(|p| p.uses.contains(&j.derivation)) + .unwrap(); + assert_eq!(j.truth, proof.truth); + assert_eq!(j.roots, proof.roots); + assert!( + !j.roots.contains(&1), + "the conclusion's own source is not a root" + ); + } + /// The same step in 63 thoughts admits 63 derivations, and the /// conclusion's pooled truth and roots stay those of one. #[test]