# Facts and evidence

**In one sentence:** `assert` lays support — positive or negative — on a
ground atom: rules infer from supports, while provenance (`origin`), times
(`valid`/`observed`/`recorded`), and documents (`evidence`) say where the
support came from and when it holds. The author takes a fact when an
inference needs a premise: without an established premise the rule stays
silent, and the question answers Not established, not refuted.

The language specification treats a fact as support laid on a ground atom:
rules infer from supports, while provenance, times, and documents say where
the support came from and when it holds. Package facts state the act’s
standing data; case facts state one computation’s input.

## 1. When to use and when not to

| Instead | Selection rule |
|---|---|
| `assert p(x)` vs `assert not p(x)` | An established fact is positive support; an established absence is negative support. Absence of a fact is not negation: without `not` the question never gives Refuted. Criterion: the organ recorded the absence — `not`; data simply missing — nothing |
| `origin case_input` vs `origin source_asserted` | A fact of the case side is `case_input`; an assertion of the act itself, visible in every case against the package, is `source_asserted` (the package-fact default). The origin list is closed: a typo is `LDC-E1374`, not “a new provenance kind” |
| A package fact vs a case fact (`given`) | The act’s handbook (rate, vocabulary, an organ decision with a date) is a package fact: always visible. One computation’s input is the case: the program is presented separately, the case cannot change law. Both supplies add into one support store — a case fact does not “override” a package fact but disputes it (Contradiction) |
| `valid [a, b)` vs `observed`/`recorded` | `valid` is when the assertion is true of the world: checked against the law date, a non-covering fact does not enter supports (`ASSERTION_OUTSIDE_VALID`). `observed`/`recorded` are bitemporal qualifiers: compared with nothing except order between themselves (`LDC-E3101`) |
| `evidence Name;` vs a document in the package | A document reference lives in the fact, the document itself is a case input. An `evidence` declaration in the package is warning `LDC-E1314`: a document is not part of the program |

## 2. Minimal example

Package `research.facts.polarity`: “Acme” registration — a positive package
fact, absence of liquidation — a negative one; the rule reads both premises
plus a licence from the case:

```law
assert registered(entity_ref("urn:case:research:facts:acme")) {
    id "assert-acme-registered";
    origin source_asserted;
}
assert not in_liquidation(entity_ref("urn:case:research:facts:acme")) {
    id "assert-acme-not-in-liquidation";
    origin source_asserted;
}
rule MayTrade strict {
    for c: Company;
    when registered(c) and licensed(c);
    then may_trade(c);
}
```

Case facts: `licensed(acme)` with `origin case_input`. Query: `evaluate
truth(may_trade(acme))` — both premises Established (the package fact is
visible in an empty case).

Actual engine answer:

```text
law test research.facts.polarity: мир research.facts.polarity
  ok   [research.facts.polarity#authored] tests/01-may-trade.lawtest / urn:query:research-facts-01
  ok   [research.facts.polarity#authored] tests/02-no-support.lawtest / urn:query:research-facts-02
итого: 2 проверено, 2 прошли, 0 не прошли, 0 не исполнены; код 0
```

`law engine check` — `check OK`, no warnings. Sensitivity:
an empty case (no `licensed`) gives `may_trade` = Not established, not refuted
(the no-support test): the package fact `registered` gives
support, but the second premise is missing — the rule stays silent.

Second package `research.facts.valid_window`: an audit exemption with window
`valid [@2027-01-01, infinity)`. Actual answer: law date 2027-06-01 —
Established (the inside-window test); law date 2026-03-01 —
Not established, not refuted (the outside-window test), `law test` — 2/2.
Sensitivity is on the law date, not on the fact: one and the same fact
enters supports or not depending on the law date. The window is
half-open: the first day is included.

Nearest wrong outcome: reading off-window Not established, not refuted as “no fact”. The fact
exists — it is not accepted into supports, and the engine attaches issue
`ASSERTION_OUTSIDE_VALID` (info). A guard test must distinguish “no support”
from “support not accepted”, otherwise window silence is indistinguishable
from a missing fact.

## 3. Example by domain

- **Law (health insurance):** package `kz.corpus.osms` (Mandatory Social Health Insurance, Kazakhstan) —
  block `assert defined_term(…)` with the term’s text as label:
  the act’s vocabulary as facts, the term as the
  value, the text as the label.
- **Science (grammar):** package `kz.grammar.lexicon` (Kazakh language lexicon) —
  `pub facts KirispeMysaldary` with qualified neighbour facts:
  exporting a fact vocabulary across the package boundary.
- **Regulator:** package `kz.national_bank.fx` (National Bank of Kazakhstan, exchange rates) —
  one-line `assert` reference rates: a package fact as part
  of the program, visible in every case.
- **Teaching case:** package `research.facts.valid_window` — a `valid` window in
  miniature: the same mechanics of dated organ decisions as in acts with an
  effective date.

## 4. How the engine answers

Table — actual runs of this section’s teaching packages:

| Facts | Question | Answer | Why |
|---|---|---|---|
| package fact `registered`, case `licensed` | `may_trade(acme)` | Established | both premises established |
| package fact, empty case | `may_trade(acme)` | Not established, not refuted | no `licensed` premise |
| `valid` window from 2027, law date 2027-06-01 | `exempt_from_audit(acme)` | Established | window covers the law date |
| same window, law date 2026-03-01 | `exempt_from_audit(acme)` | Not established, not refuted | fact not in supports; issue `ASSERTION_OUTSIDE_VALID` |

Additionally, further checked behaviours of the earlier edition (not fixed
by a run in these teaching packages):

| Case facts | Question | Answer | Why |
|---|---|---|---|
| nothing | `registered(beta)` | Established | an anonymous fact is the same kind of fact |
| nothing | `in_liquidation(acme)` | Refuted | a negative package fact |
| nothing | `licensed(acme)` | Not established, not refuted | no support at all — not Refuted |
| `not licensed` | `licensed(acme)` | Refuted | a negative case support |
| `licensed`, `not licensed` | `licensed(acme)` | Contradiction | both polarities preserved |
| `licensed`, `not licensed` | `may_trade(acme)` | Not established, not refuted | a Contradiction premise does not activate the rule |
| `not registered` | `registered(acme)` | Contradiction | a case fact does not cancel a package fact — it disputes it |
| `licensed` with a case document | `licensed(acme)` | Established | a fact with a case document |
| `licensed` with `origin assumed_for_simulation` (mode not simulation) | `licensed(acme)` | Not established, not refuted + `ASSERTION_NOT_ACCEPTED` | the assumption is not accepted |

- Supports add up, they are not overwritten: case `not licensed` plus
  case `licensed` is Contradiction, not cancellation; a case fact against a
  package fact is a dispute (Contradiction), not an override. On these teaching
  packages the addition of opposite supports is not fixed by a run — the
  claim is marked here as “not checked”.
- A rule body reads established: a Contradiction premise does not activate
  the rule — the same mechanics as on the [strict-rules page](/constructs/rule-strict/).
- Provenance is modal: an `assumed_for_simulation` assumption outside
  simulation does not reach supports — Not established, not refuted with warning-issue
  `ASSERTION_NOT_ACCEPTED`. Not checked on examples: both examples are
  `case_input`/`source_asserted`.
- An anonymous fact in 0.2 gets its id from content:
  `<namespace>#assert-h<sha256>`; two exact anonymous duplicates are a
  rejection `LDC-E1331`.

Note on fact addressing: an explicit `id` is needed where the fact is
referenced from outside the file — proof-graph premises address it by
StableId, and a case is hashed whole, so the case hash must not change
on renumbering. The short spelling is a string before the colon
(`assert "a": licensed(…) { origin case_input; }`): the same
`id` field as in the block — exactly how all case facts in this section’s
teaching packages are written. An anonymous package fact (no `id`)
is the same kind of fact: in 0.2
it gets a content-derived id, and rules read
it equally with a named one.

## 5. Common mistakes

1. The fact exists but the rule stays silent: a Contradiction premise, an
   unaccepted fact, or a value mismatch (pitfalls, item 1).
2. Two identical anonymous facts — `LDC-E1331` (pitfalls, item 2).
3. A `valid` window in the future with today’s law date — silent Not established, not refuted
   (pitfalls, item 3).
4. A typo in `origin` — `LDC-E1374` (pitfalls, item 4).
5. A rule in `given` — a case carries no law (pitfalls, item 5).
6. An `evidence` declaration in the package — `LDC-E1314`
   (pitfalls, item 6).
7. A computation in a fact argument — `LDC-E1325`/`LDC-E1324`
   (pitfalls, item 7).

## 6. References

- Neighbour pages: [strict rules](/constructs/rule-strict/),
  [vocabulary](/constructs/vocabulary/), [negation](/constructs/negation-and-status/).
- The [first-package](/tutorials/first-package/) and [defeaters](/tutorials/defeaters/)
  tutorials live in the tutorials catalogue.
- The pitfalls page lists the diagnostics (`LDC-E1331`, `LDC-E1374`,
  `LDC-E1314`, `LDC-E1325`/`LDC-E1324`, `LDC-E3101`) with wrong forms and fixes.

## 7. Grammar excerpts

An assertion and its qualifiers (the `assertion_decl`, `assertion_item`
productions):

```ebnf
assertion_decl          = "assert", [ string_literal, ":" ], proposition,
                          [ "{", { assertion_item }, "}" ],
                          [ ";" ] ;
assertion_item          = "valid", interval_literal, ";"
                        | "observed", temporal_literal, ";"
                        | "recorded", temporal_literal, ";"
                        | "evidence", reference_list, ";"
                        | "origin", identifier, ";"
                        | stable_id_item
                        | source_anchor_item
                        | label_item
                        | metadata_item ;
```

A fact group and its inclusion (the `facts_decl`, `facts_use_decl`
productions; inclusion is an explicit `facts package::Name;` line):

```ebnf
facts_decl              = "facts", identifier, "{",
                            { assertion_decl | label_item },
                          "}" ;
```