# LDC-E2401 — A computability promise the body contradicts

## What it means

A declaration may state the computability class it claims — pure,
snapshot-bound, or one of the heavier dependencies. The compiler
independently infers the lower bound of what the body actually depends on:
a rule that reads a judgment relation can never be pure, no matter what
the annotation says. When the claimed class is weaker than the inferred
bound, the annotation hides a real dependency and the compiler refuses it
at the annotation.

The fix aligns the claim with the body: state the inferred class, or
rewrite the body so it no longer reaches the heavier dependency. Claiming
a stricter class than the bound stays silent — the bound is a floor, not
an exact measure.

## Example

```law
language "law.core" version "0.2";
package demo.diagnostics version "0.1.0";
namespace "urn:law:demo:diagnostics";

external judgment relation confirmed(x: Integer) { authority Court; }
relation flagged(x: Integer) kind institutional;
@expected_computability("PURE_DETERMINISTIC")
rule R defeasible { for x: Integer; when confirmed(x); then flagged(x); }
```

## Fix

```law
language "law.core" version "0.2";
package demo.diagnostics version "0.1.0";
namespace "urn:law:demo:diagnostics";

external judgment relation confirmed(x: Integer) { authority Court; }
relation flagged(x: Integer) kind institutional;
@expected_computability("JUDGMENT_DEPENDENT")
rule R defeasible { for x: Integer; when confirmed(x); then flagged(x); }
```

## Engine message

The engine reports this in its own wording:

```text
example.law:7:1: error LDC-E2401: @expected_computability(PURE_DETERMINISTIC) on "R": inferred lower bound — JUDGMENT_DEPENDENT (§47.5: the author cannot hide by declaration judgment/external dependency)
```

## Related

- [Expressions and quantities](/constructs/expressions-quantities/) — what function bodies may compute.