# nb-07 — A document is not yet a proven fact

*Northbridge course, intermediate ([nb-05](/tutorials/northbridge/nb-05-suitable-applicant/) →
[nb-06](/tutorials/northbridge/nb-06-register-silence/) → [nb-07](/tutorials/northbridge/nb-07-document-vs-fact/) →
[nb-08](/tutorials/northbridge/nb-08-edition-and-terms/) → [nb-09](/tutorials/northbridge/nb-09-duties-powers/)).
All law is fictional; every act, document, verifier and hash in this
article is synthetic and unofficial. Nothing here is a claim about real
legislation or a real deployment. Engine `law 0.1.0`, semantics
`law.core/0.2`, std `0.2.0`.*

## Situation

Ann applies for a Northbridge parking permit and brings a paper
certificate that says she lives in Northbridge. The clerk scans it,
files it, and asks the question the whole permit case turns on: does
this piece of paper *prove* that Ann is a resident?

The tempting answer — "the document says so, so it is proven" — is
exactly what Law DSL refuses to give for free. A document sitting in a
folder is only a stored item with a hash and a status. A proven fact is
stronger: a proposition the engine will stand behind, with a recorded
chain showing how it got there.

Between the two sits a pipeline with three gates: the case must
select a policy, link the document to the claim with support, and pin
a verification. This article walks that pipeline using five evidence
tests from the register package: one document admitted end to end
(`TRUE_ONLY`), three setups that yield no support either way
(`NEITHER`), and one accepted refutation — a verified document
speaking *against* the claim, which yields an explicit negative
(`FALSE_ONLY`) rather than silence.

## Prerequisites

- [nb-02: Why a missing fact is not a refusal](/tutorials/northbridge/nb-02-missing-fact/) —
  the four truth statuses (`TRUE_ONLY`, `FALSE_ONLY`, `BOTH`,
  `NEITHER`). This article's results are all truth statuses, so you
  need to read `NEITHER` as "not established" rather than "refused".
- [nb-06: When the register may stay silent](/tutorials/northbridge/nb-06-register-silence/) —
  closure, domain and snapshot: when absence on file may be treated as
  a negative and when it must stay silence. This article covers the
  other half of the register: when *presence* of a document counts as
  proof.

No advanced constructs are required. Everything below uses facts,
rules, and three new declarations that are explained where they first
appear.

## Minimal example

Excerpt 1 from `packs/examples/language-demo/register/package.law`
(lines 39–47, identifiers as written; the surrounding closure rules
and the snapshot tariff at the end of the file are cut):

```law
rule Accept strict {
    for e: Text;
    for d: Text;
    for link: Text;
    when edge(e, d, link) and evidence_status(d, "verified")
        and authentic(d, "urn:demo:northbridge:verifier", "verified")
        and available(d) and current(d);
    then accepted(e);
}
```

The `Accept` rule is the clerk's checklist for when a document counts
as *accepted*. `edge(e, d, link)` links a claim to its document; the
status must read `verified`; a pinned verifier must have marked the
document `authentic` with outcome `verified`; and the document must be
`available` and `current`. All five conjuncts are required — miss one
and acceptance never fires.

Excerpt 2 from the same file (lines 49–59; the rule above and the
tariff rules below are cut):

```law
evidence policy FilePolicy {
    profile "law.core.evidence-policy/0.1";
    accepts accepted;
    protects residency_proof;
    input edge edge;
    input status evidence_status;
    input authentic authentic;
    input available available;
    input current current;
    rule Accept;
}
```

An **evidence policy** is a declaration that selects which acceptance
machinery governs a case. `FilePolicy` says: claims about
`residency_proof` are **protected** (they cannot enter through a bare
assertion — more on that below), acceptance is computed by the
`accepted` relation, and the inputs plus the `Accept` rule feed it.
A case opts into the policy by naming it in its context
(`evidence_policy FilePolicy`); without that line, the whole pipeline
stays switched off and documents remain mere transport.

Two more declarations appear only in the test scenarios. **Support**
links a stored document to the proposition it backs: `support PassDoc
supports residency_proof(...)` means "document PassDoc speaks for Ann's
residency", while `refutes` means it speaks against it. Support alone
carries nothing — it is transport, a labelled arrow from paper to
claim.

**Verification** records that somebody actually checked:
`verification VPass { evidence PassDoc; ... verifier
"urn:demo:northbridge:verifier"; outcome verified; ... }` pins the
document hash, the verifier identity and the outcome together with a
timestamp.

**Provenance** is the recorded origin of every such step — which
document, which verifier, which hashes — so that an answer can later
show *why* a fact counts as proven rather than merely claimed.

## Command and result

The register package is self-contained (its test world is the register
plus vocabulary), so one command checks everything:

```sh
law test packs/examples/language-demo/register
```

Observed result (engine `law 0.1.0`):

```text
law test demo.northbridge.register: мир demo.northbridge.register, demo.northbridge.vocabulary
  ok   [demo.northbridge.register] tests/register.lawtest / on file without a record — not a resident
  ok   [demo.northbridge.register] tests/register.lawtest / outside the domain silence is silence
  ok   [demo.northbridge.register] tests/register.lawtest / file record accepted
  ok   [demo.northbridge.register] tests/register.lawtest / key conflict: two filing dates
  ok   [demo.northbridge.register] tests/register.lawtest / policy selected, authenticity pinned
  ok   [demo.northbridge.register] tests/register.lawtest / without pinned authenticity support is rejected
  ok   [demo.northbridge.register] tests/register.lawtest / without a policy support stays transport
  ok   [demo.northbridge.register] tests/register.lawtest / bare assertion of the protected under a policy
  ok   [demo.northbridge.register] tests/register.lawtest / refuting document
итого: 9 проверено, 9 прошли, 0 не прошли, 0 не исполнены; код 0
```

The package also passes the static check:

```sh
law engine check packs/examples/language-demo/register/package.law
```

```text
check OK: packs/examples/language-demo/register/package.law
```

Five of the nine tests carry this article. The first four belong to
[nb-06: When the register may stay silent](/tutorials/northbridge/nb-06-register-silence/)
(closure and key conflict) and are shown here only to prove the suite
is green as a whole:

| Test | Setup | Asks | Expects |
|---|---|---|---|
| `policy selected, authenticity pinned` | policy + evidence + support + verification | `resident_admitted` | `TRUE_ONLY`, `COMPUTED` |
| `without pinned authenticity support is rejected` | as above minus verification | `resident_admitted` | `NEITHER` |
| `without a policy support stays transport` | evidence + support + verification + five hand asserts, no policy | `resident_admitted` | `NEITHER` |
| `bare assertion of the protected under a policy` | bare `assert` replaces evidence + support + verification, policy on | `resident_admitted` | `NEITHER` |
| `refuting document` | policy + evidence + verification, `refutes` instead of `supports` | `residency_proof` | `FALSE_ONLY` |

Note the last row asks a different question: `residency_proof`, the
protected mid-chain predicate, rather than the end-of-chain
`resident_admitted`. Its `FALSE_ONLY` is an accepted negative
conclusion, not a failed acceptance.

All nine tests pass: each answer matched its expectation. A passing
test is not a ruling in anyone's favour — it only says the engine's
answer agreed with the test's `expect` line.

The summary line is in Russian: `итого: 9 проверено, 9 прошли, 0 не
прошли, 0 не исполнены; код 0` — 9 checked, 9 passed, 0 failed,
0 skipped, exit code 0. The first line names the test world (`мир`):
the register package plus the vocabulary it reads.

The admitted case works because it passes every gate: the context
selects `FilePolicy`, `PassDoc` is a stored record with a content hash,
`support` links it to `residency_proof(ann)`, and `verification VPass`
pins the same hash with verifier `urn:demo:northbridge:verifier` and
outcome `verified`. The engine accepts the document and the
`ProofAdmits` rule turns the protected proof into
`resident_admitted(ann)`: `TRUE_ONLY`.

## Why this construct

The task is to decide when a filed document may promote a claim from
"said on paper" to an engine-backed truth — and to keep a checkable
record of every step that promotion relied on.

Splitting the pipeline into policy, support and verification keeps
the three silent outcomes distinguishable. Only the first is a
one-element removal: dropping the `verification VPass` block from the
admitted case (`without pinned authenticity support is rejected`). The
second drops the policy line while adding five hand-asserted inputs
that change nothing (`without a policy support stays transport`). The
third replaces the whole evidence chain with a single bare assertion
(`bare assertion of the protected under a policy`). All three answer
`NEITHER`, each for its own declared reason.

The fourth outcome runs the full pipeline with `refutes` instead of
`supports`, asks the protected predicate `residency_proof` directly,
and yields `FALSE_ONLY` (`refuting document`) — an accepted negative
conclusion, not a failure. One fused "document proves claim" rule
could not distinguish these four outcomes.

All five expectations (`TRUE_ONLY`, `NEITHER`, `FALSE_ONLY`) are
executed by `law test`, not asserted in prose.

What is not proven: that Ann really lives in Northbridge. The tests
prove the machine admits a document only through the full chain; no
test can prove the paper tells the truth about the world. Residency
data here is fictional, and verification checks document integrity and
origin — not ground truth about where anyone sleeps.

<details>
<summary>Why not a bare assertion or a status-only rule?</summary>

A bare `assert` of `residency_proof` works for unprotected facts (the
closure tests in
[nb-06: When the register may stay silent](/tutorials/northbridge/nb-06-register-silence/)
rely on exactly that), but the policy *protects* `residency_proof`, so
assertion is no longer a lawful entry route. A plain rule deriving
admission from `evidence_status` alone would skip the verifier pin and
admit anything stamped "verified" by anyone — the `authentic` conjunct
with its pinned verifier URN exists to close that hole.

</details>

## Changed condition

Start from the admitted case (`policy selected, authenticity pinned`:
`TRUE_ONLY`) and delete exactly one block — the `verification VPass`
declaration — keeping the policy, the stored record and the `support`
line. That is precisely the next test
(`without pinned authenticity support is rejected`).

The answer collapses to `NEITHER`. Nothing about the document changed:
same bytes, same hash, same link to the claim. What changed is the
*check*: nobody with standing recorded an outcome, so the `authentic`
conjunct of `Accept` has no support and acceptance never fires. The
paper is still filed and still linked — support as transport survives
— but transport is not proof.

The mirror change is symmetric: restore verification but drop the
`evidence_policy FilePolicy` line from the context
(`without a policy support stays transport`). Now even a fully verified
document plus all five `Accept` inputs asserted by hand change nothing
— the policy that would run the rule was never selected, so acceptance
is never computed and the answer is again `NEITHER`.

## Typical mistake

The mistake is asserting the protected fact directly. A newcomer who
wants Ann admitted writes the shortest possible given block:

Excerpt — the bare assertion from
`packs/examples/language-demo/register/tests/register.lawtest` line 101
(single line; indentation normalized in print).

```law
assert "bare-proof": residency_proof(entity_ref("urn:demo:northbridge:ann")) { origin case_input; }
```

with the policy selected — and expects `TRUE_ONLY`, since the fact is
right there. The observed answer is `NEITHER`
(`bare assertion of the protected under a policy`).

The consequence is silent, which is what makes this mistake sharp: no
error, no conflict issue, just `NEITHER`. Protection means the fact's
only lawful entry route is the evidence pipeline; a bare assertion of a
protected predicate is discarded rather than honoured.

The fix: if a predicate appears in a policy's `protects` list, stop
asserting it and start filing documents — the fact must be *earned*
through support plus verification, never injected.

## Limits

- **Protected facts need the full chain.** Policy selected, support
  linked, verification pinned with matching hash and verifier. The
  suite removes the verification and the policy in turn; each removal
  yields `NEITHER`, and hand-asserting the rule inputs changes nothing
  while the policy is off. There is no partial credit and no fallback
  to assertion for protected predicates.
- **Refutation is first-class.** A verified document linked with
  `refutes` yields `FALSE_ONLY` (`refuting document`) — support can
  speak against a claim through the same pipeline, not only for it.
- **Support without a policy is transport only.** Filed, hashed and
  linked documents change nothing until a case selects the policy that
  runs acceptance. Storage is not decision.
- **Verified profile:** engine `law 0.1.0`, semantics `law.core/0.2`.
  Refusals and silent outcomes described here are facts about this
  profile and implementation, never claims about what the language
  could express in principle.

## Exercise

Answer from the suite output and the test sources — no new runs
needed. Predict first, then confirm with `law test`:

1. In `without pinned authenticity support is rejected`, which
   conjunct of the `Accept` rule loses its support, and why does the
   stored record plus the `support` line not compensate?
2. In `without a policy support stays transport`, the scenario asserts
   all five `Accept` inputs by hand (`edge`, `evidence_status`,
   `authentic`, `available`, `current`) — yet the answer is `NEITHER`.
   What single context line is missing, and what does its absence
   switch off?
3. Why does `bare assertion of the protected under a policy` answer
   `NEITHER` rather than raising an error — and what would change if
   `residency_proof` were removed from the policy's `protects` list?
4. What is the status of `truth(residency_proof(ann))` in the
   `refuting document` test, and which single word in the `support`
   line explains why it is `FALSE_ONLY` rather than `NEITHER`?

Checkable solution:
[solutions/nb-07-solutions.md](/tutorials/northbridge/solutions/nb-07-solutions/).

## Sources

- Teaching package:
  `packs/examples/language-demo/register/package.law` (rules `Accept`
  and `ProofAdmits`, `evidence policy FilePolicy` protecting
  `residency_proof`).
- Scenarios:
  `packs/examples/language-demo/register/tests/register.lawtest`
  (`policy selected, authenticity pinned`,
  `without pinned authenticity support is rejected`,
  `without a policy support stays transport`,
  `bare assertion of the protected under a policy`,
  `refuting document`).
- Suite tour: `packs/examples/language-demo/README.md`.
- Prerequisite: [nb-06: When the register may stay silent](/tutorials/northbridge/nb-06-register-silence/); next:
  [nb-08: Which edition applies and when the term expires](/tutorials/northbridge/nb-08-edition-and-terms/).
- Level 1 — Northbridge use: this article (fictional permit office;
  a filed certificate becomes proof only through support plus pinned
  verification under a selected policy).
- Level 2 — domain template: whenever a claim may enter only through
  checked documents, protect the predicate in an evidence policy,
  require support plus a pinned verifier outcome for acceptance, and
  write one scenario per missing gate so each failure stays
  distinguishable.
- Level 3 — confirmed external formalization: burden of proof on
  cancellation notification (EU Regulation 261/2004, art. 5(4)) —
  package `eu.transport.air_passenger_rights`,
  `corpus/laws/eu/air-passenger-rights/04-cancellation.law:190-197`,
  construct presumption with a contrary exception
  (`PassengerUninformedUnlessCarrierProves`: presume uninformed
  `unless carrier_proved_notification(p, f) then not ...`). Why this
  form fits: burden allocation as ground plus presumption plus a named
  exit — the same "who must show what, and what rebuts it" question as
  the `FilePolicy` acceptance pipeline. Evidence:
  `docs/research/constructs/09-presumption-fiction/corpus-forms.en.md`
  section 1 (rated exemplary there). Limit of verification: presence of
  the named construct at the cited lines only, confirmed by direct
  source read; no claim about deployment, runtime behavior, or legal
  correctness.