# Formula with physical quantities

## Intention

I want to compute the work of a force while keeping the result dimension.

The scenes check 2 N × 3 m = 6 J; converting the result to m is rejected at evaluation.

## Incorrect form and why it stays silent

```text title="Incorrect form"
unit_convert(magnitude(2 N) * magnitude(3 m), "m")

pure function Work(force: Magnitude, distance: Magnitude) -> Magnitude = unit_convert(force * distance, "J");
```

Dimension and unit are checked at evaluation: the incorrect expression below yields RUNTIME_ERROR. A separate mutation shows an implementation defect: unit_convert inside a pure function is rejected with LDC-E2403, although conversion is defined as deterministic.

## Correct form

```law
language "law.core" version "0.2";
package recipes.l.r12 version "0.1.0";
namespace "urn:recipe:l-calc:12";

unit m dimension Length scale 1 / 1;
unit N dimension Mass * Length / (Time * Time) scale 1 / 1;
unit J dimension Mass * Length * Length / (Time * Time) scale 1 / 1;
pure function Work(force: Magnitude, distance: Magnitude) -> Magnitude = force * distance;
relation measured(x: Magnitude);
rule Example strict { when true; then measured(unit_convert(magnitude(2 N) * magnitude(3 m), "J")); }
```

## Frozen execution scene

| Facts and choice | Question | Answer |
|---|---|---|
| 1. two newtons over three metres | `if scalar_of(unit_convert(Work(magnitude(2 N), magnitude(3 m)), "J") / magnitude(1 J)) == 6 / 1 then true else false` | `true` / `COMPUTED` |
| 2. zero displacement | `if scalar_of(unit_convert(Work(magnitude(2 N), magnitude(0 m)), "J") / magnitude(1 J)) == 0 / 1 then true else false` | `true` / `COMPUTED` |
| 3. energy cannot be converted to length | `unit_convert(magnitude(2 N) * magnitude(3 m), "m")` | no value / `RUNTIME_ERROR` |

```law
test "two newtons over three metres" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        
    }
    evaluate if scalar_of(unit_convert(Work(magnitude(2 N), magnitude(3 m)), "J") / magnitude(1 J)) == 6 / 1 then true else false;
    expect value == true;
    expect evaluation_status == COMPUTED;
    
}
```

```law
test "zero displacement" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        
    }
    evaluate if scalar_of(unit_convert(Work(magnitude(2 N), magnitude(0 m)), "J") / magnitude(1 J)) == 0 / 1 then true else false;
    expect value == true;
    expect evaluation_status == COMPUTED;
    
}
```

```law
test "energy not convertible to length" {
    given {
        context {
            legal_time @2026-09-13;
            decision_time @2026-09-13T09:00:00+05:00;
            knowledge_time @2026-09-13T09:00:00+05:00;
            timezone "Asia/Almaty";
        }
        
    }
    evaluate unit_convert(magnitude(2 N) * magnitude(3 m), "m");
    
    expect evaluation_status == RUNTIME_ERROR;
    expect issue(UNIT_DIMENSION_MISMATCH);
}
```



## Counterfactual

Mutation: `= force * distance;` → `= unit_convert(force * distance, "J");`; expected `LDC-E2403`. Additional counterfactuals are shown as separate table rows.

A separate witness checks the absence of the required static rejection for a conversion known to be wrong at compile time. The executable rejection is already pinned by the last scene above; a passing static check does not prove this form correct.

```python
>>> import runpy
>>> checks = runpy.run_path("docs/recipes/l-calc/resources/check.py")
>>> checks["check_static_units"](https://github.com/arxohq/law/blob/master/docs/recipes/l-calc/12)
'ДЕФЕКТ lawc: статически известная ошибка единиц проходит check'
```

## Boundary

The formula is work of a constant force along a displacement. It does not solve arbitrary equations and does not derive the premises of a physical model. For ordinary Quantity the product of two dimensioned quantities is undefined; Magnitude is used instead. A statically known wrong conversion or operation passes the static check but is rejected at evaluation. A unit_convert call inside a pure function is rejected (LDC-E2403); the formula stays pure and conversion is moved into the query.

## Pitfall

Energy cannot be converted to length: the dimension check rejects it at evaluation.