feat(trust): wire diminishment detection into the credibility pass #36

Open
hugooconnor wants to merge 1 commit from feat/wire-diminishment into main
hugooconnor commented 2026-07-17 11:56:07 +00:00 (Migrated from codeberg.org)

Wires defeated-defeater detection and diminishment into compute_weighted_conclusions, populating the previously unused WeightedConclusion::diminished_by.

Semantics

A defeater diminishes a +d conclusion when its head complements the conclusion's literal and its body is positively provable (it fired). Since the conclusion is nonetheless positive, the proof theory guarantees the defeater was overruled by the superiority relation, so no separate superiority check is needed. Defeaters whose antecedents are not provable mount no challenge and do not diminish.

Defeater credibility is the weakest link of its own derivation (build_trust_tree); degrees fold as degree * (1 - defeater_degree) per defeater in rule order, matching the Lean-verified diminish_all. Thresholds evaluate on the post-diminishment degree. +D conclusions are exempt: a strict conclusion cannot be challenged by a defeater.

Tests

Six new integration tests in trust_integration_tests.rs:

  • The COMMA 2026 SLA example end-to-end for all three parties: plaintiff 0.63, defendant 0.04, court 0.30
  • Unfired defeaters do not diminish
  • Two defeaters fold multiplicatively (0.9 x 0.5 x 0.8 = 0.36)
  • +D conclusions are not diminished

Full workspace: 2083 passed, 0 failed. Verified end-to-end via spindle reason --trust --json.

🤖 Generated with Claude Code

Wires defeated-defeater detection and diminishment into `compute_weighted_conclusions`, populating the previously unused `WeightedConclusion::diminished_by`. ## Semantics A defeater diminishes a `+d` conclusion when its head complements the conclusion's literal and its body is positively provable (it *fired*). Since the conclusion is nonetheless positive, the proof theory guarantees the defeater was overruled by the superiority relation, so no separate superiority check is needed. Defeaters whose antecedents are not provable mount no challenge and do not diminish. Defeater credibility is the weakest link of its own derivation (`build_trust_tree`); degrees fold as `degree * (1 - defeater_degree)` per defeater in rule order, matching the Lean-verified `diminish_all`. Thresholds evaluate on the post-diminishment degree. `+D` conclusions are exempt: a strict conclusion cannot be challenged by a defeater. ## Tests Six new integration tests in `trust_integration_tests.rs`: - The COMMA 2026 SLA example end-to-end for all three parties: plaintiff 0.63, defendant 0.04, court 0.30 - Unfired defeaters do not diminish - Two defeaters fold multiplicatively (0.9 x 0.5 x 0.8 = 0.36) - `+D` conclusions are not diminished Full workspace: 2083 passed, 0 failed. Verified end-to-end via `spindle reason --trust --json`. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
This pull request can be merged automatically.
You are not authorized to merge this pull request.
View command line instructions

Checkout

From your project repository, check out a new branch and test the changes.
git fetch -u origin feat/wire-diminishment:feat/wire-diminishment
git switch feat/wire-diminishment

Merge

Merge the changes and update on Forgejo.

Warning: The "Autodetect manual merge" setting is not enabled for this repository, you will have to mark this pull request as manually merged afterwards.

git switch main
git merge --no-ff feat/wire-diminishment
git switch feat/wire-diminishment
git rebase main
git switch main
git merge --ff-only feat/wire-diminishment
git switch feat/wire-diminishment
git rebase main
git switch main
git merge --no-ff feat/wire-diminishment
git switch main
git merge --squash feat/wire-diminishment
git switch main
git merge --ff-only feat/wire-diminishment
git switch main
git merge feat/wire-diminishment
git push origin main
Sign in to join this conversation.
No reviewers
No labels
No milestone
No project
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference
anuna-research/spindle-rust!36
No description provided.