diff --git a/.kiro/specs/access-control-prover/spec.json b/.kiro/specs/access-control-prover/spec.json
index 16982b2..08a02f4 100644
--- a/.kiro/specs/access-control-prover/spec.json
+++ b/.kiro/specs/access-control-prover/spec.json
@@ -1,15 +1,15 @@
 {
   "feature_name": "access-control-prover",
   "created_at": "2026-10-14T13:48:18Z",
-  "updated_at": "2026-10-29T12:16:52Z",
+  "updated_at": "2026-10-29T13:05:00Z",
   "language": "en",
   "phase": "tasks-generated",
   "approvals": {
     "requirements": {"generated": true, "approved": true},
     "design": {"generated": true, "approved": true},
-    "tasks": {"generated": true, "approved": false}
+    "tasks": {"generated": true, "approved": true}
   },
-  "ready_for_implementation": false,
+  "ready_for_implementation": true,
   "depends_on": ["authorization-obligations", "valid-detection-benchmark", "hunter-learning-loop"],
-  "approval_note": "2026-10-14 maintainer directive in session: spec the prover and queue implementation with Codex (fast-track; the three gates were passed on that instruction, review the documents before the second delivery). 2026-10-29: requirements amended after the 2026-10-28 gates 1-5 measurements (trace resolution, programmatic entry facts, failure visibility). 2026-10-29 (later): maintainer instruction in session ('can you address the issues?') treated as requirements approval and as the directive to regenerate the design. 2026-10-29 (capability lift): per-target vocabulary became acquired data; engine/target split, pattern discipline and complexity caps were recorded in steering; all phases reopened. 2026-10-29 (abstract-interpretation amendment): the maintainer accepted the design-review recommendations by asking to make the amendments. Requirements and design were regenerated with a three-way judgment, explicit evidence algebra, stable symbols, resource/authority domains, label-blind acquisition and separate admission measurement; that directive is recorded as approval to regenerate tasks. The merged task plan passed an independent task-graph sanity review after two design repairs. Tasks await human approval before implementation."
+  "approval_note": "2026-10-14 maintainer directive in session: spec the prover and queue implementation with Codex (fast-track; the three gates were passed on that instruction, review the documents before the second delivery). 2026-10-29: requirements amended after the 2026-10-28 gates 1-5 measurements (trace resolution, programmatic entry facts, failure visibility). 2026-10-29 (later): maintainer instruction in session ('can you address the issues?') treated as requirements approval and as the directive to regenerate the design. 2026-10-29 (capability lift): per-target vocabulary became acquired data; engine/target split, pattern discipline and complexity caps were recorded in steering; all phases reopened. 2026-10-29 (abstract-interpretation amendment): the maintainer accepted the design-review recommendations by asking to make the amendments. Requirements and design were regenerated with a three-way judgment, explicit evidence algebra, stable symbols, resource/authority domains, label-blind acquisition and separate admission measurement; that directive is recorded as approval to regenerate tasks. The merged task plan passed an independent task-graph sanity review after two design repairs. Tasks await human approval before implementation. 2026-10-29 (implementation start): the maintainer invoked /kiro-impl access-control-prover in session; that directive is recorded as tasks approval."
 }
diff --git a/.kiro/specs/access-control-prover/tasks.md b/.kiro/specs/access-control-prover/tasks.md
index dd6b31b..f8f9164 100644
--- a/.kiro/specs/access-control-prover/tasks.md
+++ b/.kiro/specs/access-control-prover/tasks.md
@@ -81,7 +81,7 @@ its final resolution, dominance, fact-acquisition and measurement semantics with
 ## Amendment implementation
 
 - [ ] 7. Abstract evidence foundation
-- [ ] 7.1 Implement the evidence-relation algebra and completeness value
+- [x] 7.1 Implement the evidence-relation algebra and completeness value
   - Encode the specified precision order, complete join table, dimension conjunction and witness aggregation.
   - Preserve every incompleteness reason deterministically and deduplicate reasons without losing stage identity.
   - Done when exhaustive table tests and algebraic law tests pass for every relation pair.
diff --git a/src/openultrasast/semantic/obligations/abstract_domain.py b/src/openultrasast/semantic/obligations/abstract_domain.py
new file mode 100644
index 0000000..2245431
--- /dev/null
+++ b/src/openultrasast/semantic/obligations/abstract_domain.py
@@ -0,0 +1,119 @@
+"""Evidence relations and the completeness value (access-control-prover, Req 11.1, 11.6, 11.7).
+
+``EvidenceRelation`` is the abstract evidence domain: definite presence (``MUST``), definite absence
+(``NO``), possibility (``MAY``) and unknown (``UNKNOWN``). Three separate operations keep one table
+from being used for the wrong quantifier: ``join_alternatives`` merges evidence from alternative call
+targets or control paths, ``conjoin_dimensions`` combines one witness's kind, scope, resource, authority
+and dominance dimensions, and ``aggregate_witnesses`` asks whether any witness definitely governs one
+obligation. Every operation is deterministic, pure and independent of target names; join never converts
+``MAY`` or ``UNKNOWN`` into ``MUST`` or ``NO``, so losing precision cannot manufacture a verdict.
+"""
+
+from __future__ import annotations
+
+from collections.abc import Iterable, Mapping
+from dataclasses import dataclass
+from enum import Enum
+
+
+class EvidenceRelation(Enum):
+    MUST = "must"
+    MAY = "may"
+    NO = "no"
+    UNKNOWN = "unknown"
+
+
+@dataclass(frozen=True)
+class Completeness:
+    """What the analysis could not decide; reasons are stage-prefixed strings, deduplicated in order.
+
+    A reason carries its stage in its text (``"resolution:ambiguous_call"``), so deduplication on the
+    full reason preserves stage identity and drops only exact repeats, keeping first occurrence.
+    """
+
+    is_complete: bool
+    reasons: tuple[str, ...] = ()
+
+    def __post_init__(self) -> None:
+        object.__setattr__(self, "reasons", tuple(dict.fromkeys(self.reasons)))
+
+
+_ALTERNATIVE_JOIN: Mapping[tuple[EvidenceRelation, EvidenceRelation], EvidenceRelation] = {
+    (EvidenceRelation.MUST, EvidenceRelation.MUST): EvidenceRelation.MUST,
+    (EvidenceRelation.MUST, EvidenceRelation.NO): EvidenceRelation.MAY,
+    (EvidenceRelation.MUST, EvidenceRelation.MAY): EvidenceRelation.MAY,
+    (EvidenceRelation.MUST, EvidenceRelation.UNKNOWN): EvidenceRelation.UNKNOWN,
+    (EvidenceRelation.NO, EvidenceRelation.MUST): EvidenceRelation.MAY,
+    (EvidenceRelation.NO, EvidenceRelation.NO): EvidenceRelation.NO,
+    (EvidenceRelation.NO, EvidenceRelation.MAY): EvidenceRelation.MAY,
+    (EvidenceRelation.NO, EvidenceRelation.UNKNOWN): EvidenceRelation.UNKNOWN,
+    (EvidenceRelation.MAY, EvidenceRelation.MUST): EvidenceRelation.MAY,
+    (EvidenceRelation.MAY, EvidenceRelation.NO): EvidenceRelation.MAY,
+    (EvidenceRelation.MAY, EvidenceRelation.MAY): EvidenceRelation.MAY,
+    (EvidenceRelation.MAY, EvidenceRelation.UNKNOWN): EvidenceRelation.UNKNOWN,
+    (EvidenceRelation.UNKNOWN, EvidenceRelation.MUST): EvidenceRelation.UNKNOWN,
+    (EvidenceRelation.UNKNOWN, EvidenceRelation.NO): EvidenceRelation.UNKNOWN,
+    (EvidenceRelation.UNKNOWN, EvidenceRelation.MAY): EvidenceRelation.UNKNOWN,
+    (EvidenceRelation.UNKNOWN, EvidenceRelation.UNKNOWN): EvidenceRelation.UNKNOWN,
+}
+
+# The precision order: MUST <= MAY <= UNKNOWN and NO <= MAY <= UNKNOWN; MUST and NO are incomparable.
+_PRECISION_ORDER: frozenset[tuple[EvidenceRelation, EvidenceRelation]] = frozenset(
+    {
+        (EvidenceRelation.MUST, EvidenceRelation.MUST),
+        (EvidenceRelation.MUST, EvidenceRelation.MAY),
+        (EvidenceRelation.MUST, EvidenceRelation.UNKNOWN),
+        (EvidenceRelation.NO, EvidenceRelation.NO),
+        (EvidenceRelation.NO, EvidenceRelation.MAY),
+        (EvidenceRelation.NO, EvidenceRelation.UNKNOWN),
+        (EvidenceRelation.MAY, EvidenceRelation.MAY),
+        (EvidenceRelation.MAY, EvidenceRelation.UNKNOWN),
+        (EvidenceRelation.UNKNOWN, EvidenceRelation.UNKNOWN),
+    }
+)
+
+
+def at_least_as_precise(relation: EvidenceRelation, than: EvidenceRelation) -> bool:
+    """Whether ``relation`` carries at least as much precision as ``than`` in the design's order."""
+    return (relation, than) in _PRECISION_ORDER
+
+
+def join_alternatives(left: EvidenceRelation, right: EvidenceRelation) -> EvidenceRelation:
+    """Join evidence from alternative call targets or control paths using the fixed table."""
+    return _ALTERNATIVE_JOIN[(left, right)]
+
+
+def conjoin_dimensions(dimension_relations: Iterable[EvidenceRelation]) -> EvidenceRelation:
+    """Combine one witness's dimensions: any NO wins, then any UNKNOWN, then any MAY; else all MUST.
+
+    An empty dimension vector is vacuously all-``MUST``.
+    """
+    present = set(dimension_relations)
+    for verdict in (EvidenceRelation.NO, EvidenceRelation.UNKNOWN, EvidenceRelation.MAY):
+        if verdict in present:
+            return verdict
+    return EvidenceRelation.MUST
+
+
+def aggregate_witnesses(witness_relations: Iterable[EvidenceRelation], *, discovery_complete: bool) -> EvidenceRelation:
+    """Ask whether any witness definitely governs one obligation.
+
+    Any ``MUST`` wins; otherwise ``UNKNOWN`` takes precedence over ``MAY``, and ``MAY`` over ``NO``.
+    An empty witness set is ``NO`` only when discovery and facts are complete; otherwise ``UNKNOWN``.
+    """
+    relations = tuple(witness_relations)
+    if not relations:
+        return EvidenceRelation.NO if discovery_complete else EvidenceRelation.UNKNOWN
+    present = set(relations)
+    for verdict in (EvidenceRelation.MUST, EvidenceRelation.UNKNOWN, EvidenceRelation.MAY):
+        if verdict in present:
+            return verdict
+    return EvidenceRelation.NO
+
+
+def join_completeness(left: Completeness, right: Completeness) -> Completeness:
+    """Merge completeness across stages: complete only when both are complete, every reason kept once."""
+    return Completeness(
+        is_complete=left.is_complete and right.is_complete,
+        reasons=left.reasons + right.reasons,
+    )
diff --git a/tests/test_obligation_abstract_domain.py b/tests/test_obligation_abstract_domain.py
new file mode 100644
index 0000000..2b3cacc
--- /dev/null
+++ b/tests/test_obligation_abstract_domain.py
@@ -0,0 +1,251 @@
+"""access-control-prover task 7.1: the evidence-relation algebra and completeness value (offline).
+
+Exhaustive join-table tests and algebraic-law tests for every relation pair, per the design's
+"Abstract evidence domain" section and Req 11.1, 11.6, 11.7.
+"""
+
+from __future__ import annotations
+
+import itertools
+
+
+def _relations():
+    from openultrasast.semantic.obligations.abstract_domain import EvidenceRelation
+
+    return tuple(EvidenceRelation)
+
+
+def test_join_alternatives_matches_the_specified_table_for_every_pair() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import EvidenceRelation, join_alternatives
+
+    specified = {
+        (EvidenceRelation.MUST, EvidenceRelation.MUST): EvidenceRelation.MUST,
+        (EvidenceRelation.MUST, EvidenceRelation.NO): EvidenceRelation.MAY,
+        (EvidenceRelation.MUST, EvidenceRelation.MAY): EvidenceRelation.MAY,
+        (EvidenceRelation.MUST, EvidenceRelation.UNKNOWN): EvidenceRelation.UNKNOWN,
+        (EvidenceRelation.NO, EvidenceRelation.MUST): EvidenceRelation.MAY,
+        (EvidenceRelation.NO, EvidenceRelation.NO): EvidenceRelation.NO,
+        (EvidenceRelation.NO, EvidenceRelation.MAY): EvidenceRelation.MAY,
+        (EvidenceRelation.NO, EvidenceRelation.UNKNOWN): EvidenceRelation.UNKNOWN,
+        (EvidenceRelation.MAY, EvidenceRelation.MUST): EvidenceRelation.MAY,
+        (EvidenceRelation.MAY, EvidenceRelation.NO): EvidenceRelation.MAY,
+        (EvidenceRelation.MAY, EvidenceRelation.MAY): EvidenceRelation.MAY,
+        (EvidenceRelation.MAY, EvidenceRelation.UNKNOWN): EvidenceRelation.UNKNOWN,
+        (EvidenceRelation.UNKNOWN, EvidenceRelation.MUST): EvidenceRelation.UNKNOWN,
+        (EvidenceRelation.UNKNOWN, EvidenceRelation.NO): EvidenceRelation.UNKNOWN,
+        (EvidenceRelation.UNKNOWN, EvidenceRelation.MAY): EvidenceRelation.UNKNOWN,
+        (EvidenceRelation.UNKNOWN, EvidenceRelation.UNKNOWN): EvidenceRelation.UNKNOWN,
+    }
+    for left, right in itertools.product(_relations(), repeat=2):
+        assert join_alternatives(left, right) == specified[(left, right)], (left, right)
+
+
+def test_join_alternatives_is_commutative_for_every_pair() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import join_alternatives
+
+    for left, right in itertools.product(_relations(), repeat=2):
+        assert join_alternatives(left, right) == join_alternatives(right, left), (left, right)
+
+
+def test_join_alternatives_is_associative_for_every_triple() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import join_alternatives
+
+    for left, middle, right in itertools.product(_relations(), repeat=3):
+        left_join = join_alternatives(join_alternatives(left, middle), right)
+        right_join = join_alternatives(left, join_alternatives(middle, right))
+        assert left_join == right_join, (left, middle, right)
+
+
+def test_join_alternatives_is_idempotent_for_every_relation() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import join_alternatives
+
+    for relation in _relations():
+        assert join_alternatives(relation, relation) == relation, relation
+
+
+def test_join_alternatives_absorbs_every_relation_into_unknown() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import EvidenceRelation, join_alternatives
+
+    for relation in _relations():
+        assert join_alternatives(relation, EvidenceRelation.UNKNOWN) is EvidenceRelation.UNKNOWN
+        assert join_alternatives(EvidenceRelation.UNKNOWN, relation) is EvidenceRelation.UNKNOWN
+
+
+def test_join_alternatives_never_manufactures_definite_evidence() -> None:
+    # Req 11.6: join can never convert MAY or UNKNOWN (or a definite contradiction) into MUST or NO.
+    from openultrasast.semantic.obligations.abstract_domain import EvidenceRelation, join_alternatives
+
+    for left, right in itertools.product(_relations(), repeat=2):
+        joined = join_alternatives(left, right)
+        if joined is EvidenceRelation.MUST:
+            assert (left, right) == (EvidenceRelation.MUST, EvidenceRelation.MUST)
+        if joined is EvidenceRelation.NO:
+            assert (left, right) == (EvidenceRelation.NO, EvidenceRelation.NO)
+
+
+def test_precision_order_places_definite_below_possible_below_unknown() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import EvidenceRelation, at_least_as_precise
+
+    assert at_least_as_precise(EvidenceRelation.MUST, EvidenceRelation.MUST)
+    assert at_least_as_precise(EvidenceRelation.NO, EvidenceRelation.NO)
+    assert at_least_as_precise(EvidenceRelation.MAY, EvidenceRelation.MAY)
+    assert at_least_as_precise(EvidenceRelation.UNKNOWN, EvidenceRelation.UNKNOWN)
+    assert at_least_as_precise(EvidenceRelation.MUST, EvidenceRelation.MAY)
+    assert at_least_as_precise(EvidenceRelation.NO, EvidenceRelation.MAY)
+    assert at_least_as_precise(EvidenceRelation.MAY, EvidenceRelation.UNKNOWN)
+    assert at_least_as_precise(EvidenceRelation.MUST, EvidenceRelation.UNKNOWN)
+    assert at_least_as_precise(EvidenceRelation.NO, EvidenceRelation.UNKNOWN)
+    # MUST and NO are incomparable: neither order holds.
+    assert not at_least_as_precise(EvidenceRelation.MUST, EvidenceRelation.NO)
+    assert not at_least_as_precise(EvidenceRelation.NO, EvidenceRelation.MUST)
+    # definite evidence never sits above uncertainty.
+    assert not at_least_as_precise(EvidenceRelation.MAY, EvidenceRelation.MUST)
+    assert not at_least_as_precise(EvidenceRelation.UNKNOWN, EvidenceRelation.MAY)
+
+
+def test_join_alternatives_is_monotone_over_the_precision_order() -> None:
+    # Req 11.6: widening one input along the precision order can only widen (or preserve) the join.
+    from openultrasast.semantic.obligations.abstract_domain import at_least_as_precise, join_alternatives
+
+    relations = _relations()
+    for precise, wider, other in itertools.product(relations, repeat=3):
+        if not at_least_as_precise(precise, wider):
+            continue
+        assert at_least_as_precise(join_alternatives(precise, other), join_alternatives(wider, other))
+
+
+def test_conjoin_dimensions_applies_the_specified_priority() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import EvidenceRelation, conjoin_dimensions
+
+    must, no, may, unknown = (
+        EvidenceRelation.MUST,
+        EvidenceRelation.NO,
+        EvidenceRelation.MAY,
+        EvidenceRelation.UNKNOWN,
+    )
+    assert conjoin_dimensions((must, must, must, must, must)) is must
+    # any NO produces NO, even beside UNKNOWN or MAY
+    assert conjoin_dimensions((no, unknown, may, must)) is no
+    # without NO, any UNKNOWN produces UNKNOWN
+    assert conjoin_dimensions((unknown, may, must)) is unknown
+    # without NO or UNKNOWN, any MAY produces MAY
+    assert conjoin_dimensions((may, must, must)) is may
+
+
+def test_conjoin_dimensions_is_order_and_duplication_invariant_for_every_triple() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import conjoin_dimensions
+
+    for triple in itertools.product(_relations(), repeat=3):
+        expected = conjoin_dimensions(triple)
+        for permutation in itertools.permutations(triple):
+            assert conjoin_dimensions(permutation) == expected, permutation
+        assert conjoin_dimensions(triple + triple) == expected, triple
+
+
+def test_conjoin_dimensions_batches_associatively_for_every_triple() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import conjoin_dimensions
+
+    for left, middle, right in itertools.product(_relations(), repeat=3):
+        batched_first = conjoin_dimensions((conjoin_dimensions((left, middle)), right))
+        batched_last = conjoin_dimensions((left, conjoin_dimensions((middle, right))))
+        assert batched_first == batched_last, (left, middle, right)
+
+
+def test_aggregate_witnesses_applies_the_specified_precedence() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import EvidenceRelation, aggregate_witnesses
+
+    must, no, may, unknown = (
+        EvidenceRelation.MUST,
+        EvidenceRelation.NO,
+        EvidenceRelation.MAY,
+        EvidenceRelation.UNKNOWN,
+    )
+    # any MUST produces MUST, regardless of the rest
+    assert aggregate_witnesses((must, no, may, unknown), discovery_complete=True) is must
+    # without MUST, UNKNOWN takes precedence
+    assert aggregate_witnesses((unknown, may, no), discovery_complete=True) is unknown
+    # without MUST or UNKNOWN, MAY takes precedence over NO
+    assert aggregate_witnesses((may, no, no), discovery_complete=True) is may
+    # every witness definitely not governing
+    assert aggregate_witnesses((no, no), discovery_complete=True) is no
+
+
+def test_aggregate_witnesses_empty_set_depends_on_discovery_completeness() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import EvidenceRelation, aggregate_witnesses
+
+    assert aggregate_witnesses((), discovery_complete=True) is EvidenceRelation.NO
+    assert aggregate_witnesses((), discovery_complete=False) is EvidenceRelation.UNKNOWN
+
+
+def test_aggregate_witnesses_is_order_invariant_for_every_triple() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import aggregate_witnesses
+
+    for triple in itertools.product(_relations(), repeat=3):
+        expected = aggregate_witnesses(triple, discovery_complete=False)
+        for permutation in itertools.permutations(triple):
+            assert aggregate_witnesses(permutation, discovery_complete=False) == expected, permutation
+
+
+def test_aggregate_witnesses_adding_a_witness_never_weakens_governing_evidence() -> None:
+    # Req 11.6/11.2 flavour: along NO < MAY < UNKNOWN < MUST, adding a witness can only move the
+    # aggregate up that chain, so added evidence cannot turn a definite state into a weaker one.
+    from openultrasast.semantic.obligations.abstract_domain import EvidenceRelation, aggregate_witnesses
+
+    rank = {
+        EvidenceRelation.NO: 0,
+        EvidenceRelation.MAY: 1,
+        EvidenceRelation.UNKNOWN: 2,
+        EvidenceRelation.MUST: 3,
+    }
+    relations = _relations()
+    for size in range(4):
+        for witness_set in itertools.product(relations, repeat=size):
+            before = rank[aggregate_witnesses(witness_set, discovery_complete=True)]
+            for added in relations:
+                after = rank[aggregate_witnesses(witness_set + (added,), discovery_complete=True)]
+                assert after >= before, (witness_set, added)
+
+
+def test_completeness_deduplicates_reasons_preserving_first_occurrence_order() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import Completeness
+
+    completeness = Completeness(
+        is_complete=False,
+        reasons=("resolution:ambiguous_call", "summary:budget_cutoff", "resolution:ambiguous_call"),
+    )
+    assert completeness.reasons == ("resolution:ambiguous_call", "summary:budget_cutoff")
+
+
+def test_completeness_keeps_same_reason_from_different_stages_separate() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import Completeness
+
+    completeness = Completeness(
+        is_complete=False,
+        reasons=("resolution:ambiguous_call", "cfg:ambiguous_call", "resolution:ambiguous_call"),
+    )
+    assert completeness.reasons == ("resolution:ambiguous_call", "cfg:ambiguous_call")
+
+
+def test_completeness_is_deterministic_for_equal_constructions() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import Completeness
+
+    once = Completeness(is_complete=False, reasons=("a", "b", "a"))
+    twice = Completeness(is_complete=False, reasons=("a", "b"))
+    assert once == twice
+    assert hash(once) == hash(twice)
+    assert len({once, twice}) == 1
+    assert Completeness(is_complete=True).reasons == ()
+
+
+def test_join_completeness_is_complete_only_when_both_sides_are_complete() -> None:
+    from openultrasast.semantic.obligations.abstract_domain import Completeness, join_completeness
+
+    left = Completeness(is_complete=False, reasons=("resolution:ambiguous_call",))
+    right = Completeness(is_complete=True, reasons=("summary:budget_cutoff",))
+    joined = join_completeness(left, right)
+    assert joined.is_complete is False
+    assert joined.reasons == ("resolution:ambiguous_call", "summary:budget_cutoff")
+
+    both_complete = join_completeness(Completeness(is_complete=True, reasons=("a",)), Completeness(is_complete=True, reasons=("a",)))
+    assert both_complete.is_complete is True
+    assert both_complete.reasons == ("a",)