Markdown for LLMs
nb-07 — A document is not yet a proven fact
The source Markdown for this article. Copy it into your assistant or download it as a text file.
# 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.