refactor: engine/ module — wire to Derivation ontology, delete primitive-string fields

[i-am-logger]

Tracks: core-cleanup audit 2026-04-18

Problem

pr4xis/src/engine/ contains a parallel primitive-typed runtime system that duplicates the formal/logic/derivation ontology and leaks Rust primitives across its public API.

Specific violations

engine/trace.rs:

pub struct TraceEntry {
    pub step: usize,
    pub situation_before: String,  // primitive
    pub action: String,             // primitive
    pub precondition_results: Vec<PreconditionResult>,
    pub situation_after: Option<String>,  // primitive
    pub success: bool,              // primitive bool
}
pub struct Trace { entries: Vec<TraceEntry> }

Trace + TraceEntry duplicate DerivationConcept::Derivation + DerivationConcept::DerivationStep (JSV 1996; Plotkin 1981; Lambek 1968).

engine/precondition.rs:

pub enum PreconditionResult {
    Satisfied { rule: String, reason: String },
    Violated  { rule: String, reason: String, situation: String, attempted_action: String },
}

Every field is String. Satisfied maps to DerivationConcept::Witness (Martin-Löf 1984); Violated maps to ProofTheoryConcept::Counterexample. Both should be typed ontological entities.

engine/situation.rs:

pub trait Situation { fn describe(&self) -> String; ... }

describe() -> String is a primitive-leak. Situations ARE Hypothesis (pre-state) / Consequence (post-state) in Derivation.

engine/engine.rs:

pub enum EngineError<A: Action> {
    LogicalError { reason: String },  // primitive string
    ...
}

Why this is an ontological issue

Violates feedback_api_ontological_from_day_one. Was surfaced in the prior-session summary as "Unify pr4xis::engine::Trace + PipelineTrace into one Derivation type".

Proposed direction

1. Move / wire engine types through the formal/logic/derivation ontology (or whichever core logic home Derivation ends up in).
2. Trace → uses DerivationConcept::Derivation (or is one).
3. TraceEntry → DerivationStep carrying typed Witness / Hypothesis / Consequence.
4. PreconditionResult::Satisfied → Witness; Violated → Counterexample.
5. Situation trait → returns typed representation (DOLCE Being or ontology-specific), not String.
6. EngineError::LogicalError → typed ontological entity.

Depends on

• refactor: Axiom::verify() → Proof — delete holds()/description() primitive-leak API #160 (Axiom::verify → Proof) — resolves the Proof / Witness return-type question

[i-am-logger]

Partially addressed by #160's Verdict work — remaining scope narrowed

What's done (via #160)

• PreconditionResult::Satisfied ↔ Box<dyn Proof> (Martin-Löf witness) — same ontological shape
• PreconditionResult::Violated ↔ Box<dyn Counterexample> — same ontological shape
• Trace+TraceEntry aggregation ↔ CompositeProof/CompositeCounterexample — same ontological shape
• success: bool in TraceEntry is redundant once Verdict is used

Still open — inner-field primitive leaks

pub struct TraceEntry {
    pub situation_before: String,   // ← should be A::Sit
    pub action: String,              // ← should be A
    pub situation_after: Option<String>,  // ← should be Option<A::Sit>
    ...
}

pub enum PreconditionResult {
    Satisfied { rule: String, reason: String },
    Violated  { rule: String, reason: String, situation: String, attempted_action: String },
}

pub trait Situation { fn describe(&self) -> String; }      // ← String return
pub enum EngineError { LogicalError { reason: String } }   // ← String field

Remaining work

1. Type PreconditionResult over A: Action — situation: A::Sit, attempted_action: A
2. Replace rule: String with typed reference (axiom's meta().name as OntologyName)
3. Replace reason: String with Label (Lemon) or reference to axiom meta
4. Rename Situation::describe() -> String to return a typed Lemon Label or remove (debug trait suffices for dev display)
5. Type EngineError::LogicalError fields
6. Consider: replace PreconditionResult entirely with Verdict, and have Precondition check return Verdict directly

Scope is narrower now — the outer "did it succeed" shape is solved (#160). The remaining is field-typing.