system-achieves-full-correctness
OUT derived (depth 3)
The system achieves correctness at every level: deterministic conservative truth maintenance, a single reversible primitive for all non-monotonic features, and data integrity spanning all architectural layers — the system is sound end-to-end.
Summary
This is a top-level correctness claim saying the system is sound from end to end, combining deterministic truth maintenance, a single reversible primitive for all non-monotonic reasoning, and data integrity across every architectural layer. It is currently unsupported because one or more of its foundations — the determinism of the TMS engine, the sufficiency of the single outlist primitive, or the cross-layer data integrity guarantees — has been retracted or lost support.
Justifications
SL — Three depth-2 correctness properties compose into full-system soundness, but two known defects (agent count bug inflating budgets, unchecked dependent references risking crashes) gate the claim until fixed
Antecedents (all must be IN):
- tms-core-is-deterministic-and-conservative — The TMS engine produces deterministic, terminating truth maintenance through uniform pure evaluation, guaranteed convergence, and conservative asymmetric failure semantics for missing nodes.
- non-monotonic-system-is-single-reversible-primitive — The entire non-monotonic reasoning system — challenges, kill-switches, supersession, and dialectics — is built on a single primitive (outlist) that is inherently reversible, with no dedicated machinery for any defeat pattern.
- data-integrity-spans-architecture — Data integrity is enforced across all three architectural layers: clean layer boundaries prevent cross-cutting mutations, snapshot persistence ensures atomic state transitions, and conservative staleness checking gates CI pipelines.
Unless (any of these IN defeats this justification):
- derive-agent-count-bug — `_build_beliefs_section` has a bug: `count += len(belief_ids)` is inside the per-belief loop instead of outside it, inflating the count and shrinking the non-agent budget below intended size
- propagate-assumes-dependents-exist — Every ID in `node.dependents` is accessed via `self.nodes[dep_id]` without a membership check; a dangling dependent reference will raise `KeyError` — this is intentional (broken invariant = bug)