# From article text to norm — and where the language says "no"

Article 175 speaks not only of the right to benefit but of the date from
which it is granted. This half of the article is more interesting than
the first: it shows both how formalisation catches its own mistakes and
where the core's expressiveness ends.

```law
language "law.core" version "0.2";
package tutorial.kz.social version "0.2.0";
namespace "urn:law:tutorial:kz:social";

entity Actor;
entity Person : Actor;
entity DisabilityStatus;
entity Benefit;
entity BenefitApplication;

const DisabilityBenefit: Benefit = entity_ref("urn:law:tutorial:kz:social#DisabilityBenefit") {
    label ru-KZ official "Пособие по инвалидности";
};
const SurvivorBenefit: Benefit = entity_ref("urn:law:tutorial:kz:social#SurvivorBenefit") {
    label ru-KZ official "Пособие по случаю потери кормильца";
};

relation disability_established(person: Person, status: DisabilityStatus, from: Date) kind institutional;
relation entitled(person: Person, benefit: Benefit) kind institutional;
relation application_for(application: BenefitApplication, person: Person, benefit: Benefit) kind empirical;
relation application_registered(application: BenefitApplication, day: Date) kind institutional;
relation benefit_start_date(person: Person, benefit: Benefit, day: Date) kind institutional;
relation beneficiary_choice(person: Person, benefit: Benefit) kind institutional;
```

The labels read: "Disability benefit" and "Survivor benefit".

## A bound variable instead of a pseudo-function

The first draft of this norm held `any_status(person)` in its body —
"disability established with some group". It looks like a function and
reads like a function, but there is no such function in the language:
`any_status` was declared nowhere. The formaliser wrote an intention, not
a norm.

The correct record is a **bound variable**: declare `status` in `for`
and use it in the body. Existential quantification is expressed by the
variable being bound and needed nowhere else.

Right there a second find surfaced: the head predicate
`benefit_start_date` was not declared at all. Both finds were caught
by the compiler, not by reading.

```law
@source("KZ-SOCIAL-CODE-224-VII-ART-175")
rule DisabilityBenefitStart strict {
    label ru-KZ official "Статья 175. Дата назначения пособия по инвалидности";
    for person: Person;
    for status: DisabilityStatus;
    for from: Date;
    for application: BenefitApplication;
    for registered: Date;
    when entitled(person, DisabilityBenefit)
        and disability_established(person, status, from)
        and application_for(application, person, DisabilityBenefit)
        and application_registered(application, registered);
    then benefit_start_date(person, DisabilityBenefit, max(from, registered));
}
```

The rule label reads: "Article 175. The grant date of disability benefit".

Note that the body rests on `entitled(person, DisabilityBenefit)` — the
head of the norm from [the previous tutorial](/tutorials/real-article-source/).
Norms chain through predicates, not through references to each other:
law knows nothing of law; it knows of facts.

## Where the language says "no"

The real article grants the benefit not from the application
registration date but no earlier than **three months before it**. That
is, the norm head should read
`max(from, registered - 3 calendar_month)`.

So it is written in
[the worked example](https://github.com/arxohq/law/blob/master/spec/examples/kz/social-code-art175.law).
And that file fails the compiler check:

```text
error LDC-E2108: «-»: несовместимые виды Date и Quantity — §58 требует
совпадения видов для сложения и вычитания; правило скаляра §49 действует
ТОЛЬКО для умножения (§48: неявных конверсий нет)
```

The diagnostic reads: "'`-`': incompatible kinds Date and Quantity — kinds must match for addition and subtraction; the scalar rule applies ONLY to multiplication (no implicit conversions)".

Replace `max(from, registered)` with
`max(from, registered - 3 calendar_month)` in the norm above and you get
exactly this diagnostic with the `LDC-E2108` code: the lesson is
checked, not told.

**This is not a defect of the example.** The core's computable surface
is closed deliberately: subtraction requires kinds to match, while
"three calendar months" is not a duration in the same sense in which
a date is a point. A month is not a fixed number of days; "minus three
months" from 31 March needs a policy that the core lacks and that must
not be chosen silently.

Hence three honest exits, none of which is to add a conversion:

1. **The date arrives in the case.** The threshold date is computed
   outside the core and fed as a fact — then whoever chose the rounding
   policy answers for it, visibly in the case.
2. **The norm is expressed as a table.** Layer A3 (temporal parameters,
   decision tables) describes such terms as data, not as arithmetic in
   a rule head.
3. **A language change.** If the core needs calendar arithmetic, that is
   a semantic change, and it goes the full circle: prose, schema, and
   both implementations. "Simply allowing subtraction" is not an option,
   because then the month-boundary policy would turn silent.

The worked example keeps the inexpressible form on purpose:
it shows the article as it is, and thereby marks the boundary. The
boundary is worth seeing before you write forty norms and hit it on the
forty-first.

## Restriction: law requires, not derives

The last part of article 175 says: two benefits are not granted at once;
the recipient chooses one. This is not an inference rule — nothing
follows from it. It is a **requirement on the case**.

```law
@source("KZ-SOCIAL-CODE-224-VII-ART-175")
constraint OneBenefitByChoice {
    label ru-KZ official "Статья 175. Одно из двух пособий по выбору получателя";
    for person: Person;
    scope true;
    when entitled(person, DisabilityBenefit) and entitled(person, SurvivorBenefit);
    require beneficiary_choice(person, DisabilityBenefit) or beneficiary_choice(person, SurvivorBenefit);
    severity error;
    message "One of the two concurrent benefits must be selected by the beneficiary.";
}
```

The constraint label reads: "Article 175. One of the two benefits at the recipient's choice".

The difference from a rule is fundamental. A rule written in this place
**would choose** the benefit for the recipient — by order, by size, by
alphabet — and the choice would stay invisible. A constraint does not
choose: it records that a case without a choice is incomplete, and names
the culprit in the words of `message`.

A rule says "hence follows". A constraint says "so it must not be".
Confusing them is the cheapest way to teach a system to take decisions
it is not authorised to take.

## Next

The norm is tied to the text by an anchor, but the text bytes have not
yet been presented to the core. The tutorial [on pinning an
edition](/tutorials/pinned-edition/) is about how the official text is
placed next to the package and verified by hash on every build.

The exercise for this page is [/tutorials/exercise-real-article-rules/](/tutorials/exercise-real-article-rules/).