Dimensions: what the numbers in your rules mean

A solver sees integers and reals. A departure time, a shift length, a claim value and a suspicion score are all just numbers to it — which is how a rule set ends up comparing a clock reading to a currency amount and getting a confident, meaningless answer back.

A dimension is the declaration that keeps them apart. In Guardrail Calculus it is data: a carrier, an algebraic structure, an invariant, units, and constructors. What follows from it — which operators exist, what they return, what the solver may assume about every slot of that kind, how a client renders a value — is derived from that one record rather than written out again per dimension.

Every code block below is quoted from the source it describes, and every table of results is produced by running that source during this site's build. The module tests/examples/test_dimensions.py pins the outcomes, so a change that moved a verdict or stopped a rejection fails a test rather than quietly rotting this page.

A dimension is a declaration

Here is the whole of what Instant — a clock reading — is:

INSTANT = Dimension(
    name="Instant",
    carrier=Carriers.INT,
    invariant=_And(_Ge(CarrierValue(), 0), _Le(CarrierValue(), 1439)),
    base_unit="minutes_of_day",
    # Cyclic-affine over Duration derives the temporal algebra: Instant - Instant ->
    # Duration, Instant +/- Duration -> Instant (and the inert Duration + Instant).
    structure=CyclicAffine(
        displacement=DURATION, modulus=24 * 60, difference_policy="signed"
    ),
    # Clients render this dimension's values as a 24h clock reading rather
    # than a raw minute count -- declared here, interpreted client-side;
    # solvers return raw values and never format.
    display=DisplayFormat(radices=(60,), pattern="{0:02}:{1:02}"),
)

Five decisions, all in one place. The carrier is the solver-visible sort (int), so an Instant lowers to an integer and nothing else. The invariant is what is true of every value of this kind, and it travels with the dimension all the way into the solver. The base unit fixes what the carrier counts. The structure says what algebra a clock reading admits — that it is a point on a cycle, over Duration as its displacement. The display format says how a client should render one; solvers return raw values and never format.

The four shipped dimensions differ only in those fields:

Dimension	Carrier	Structure	Declared invariant	Authored with
`Duration`	`int` (minutes)	`Vector`	none — a difference may be negative	`duration_minutes`, `duration_hours`, `duration_hm`
`Instant`	`int` (minutes of day)	`CyclicAffine` over `Duration`	`0 <= v <= 1439`	`clock_hm`, `clock_from_hhmm`, `time_at`
`Money`	`int`	`TaggedVector` (equal tags only)	none — signed, for credits and refunds	`money_gbp`, `money_usd`
`Probability`	`real`	`ScalarKind` (comparison-only)	`0 <= v <= 1`	`probability`

Money is the interesting one. Its currencies are unit tags, not scales:

MONEY = Dimension(
    name="Money",
    carrier=Carriers.INT,
    invariant=None,  # current Money enforces no bound; signed-vs->=0 is an open pin
    # Currencies are unit *tags*, not scales: each is base-1 and not inter-convertible
    # (no implicit FX). Cross-currency arithmetic is blocked by the algebra precondition.
    base_unit="GBP",
    # Tagged-vector derives same-tag +/- (with the equal-tag precondition and left-tag
    # result) and tag-agnostic scalar multiplication.
    structure=TaggedVector(compatibility="equal-tag-only"),
)

Nothing converts between them, because there is no honest constant to convert with. Probability, at the other extreme, declares that it has no arithmetic at all:

PROBABILITY = Dimension(
    name="Probability",
    carrier=Carriers.REAL,
    invariant=_And(_Ge(CarrierValue(), 0), _Le(CarrierValue(), 1)),
    base_unit="",
    structure=ScalarKind(arithmetic="comparison-only"),
    # Comparison-only: no constructors and no arithmetic.
)

The structure derives the algebra

A structure is not a label. It is the single source of a dimension's operators:

Structure	Derives	Declared by
`Vector`	`+` and `-` with itself; scalar multiplication both ways	`Duration`, and most user quantities
`Affine` / `CyclicAffine`	point − point → displacement; point ± displacement → point	`Instant` over `Duration`
`TaggedVector`	`+`/`-` under an equal-tag precondition, result keeping the left tag; tag-agnostic scaling	`Money`
`ScalarKind`	nothing — comparison only	`Probability`

Point + point is absent from the affine row on purpose: two clock readings do not add. Neither list is written out anywhere as operator code — a dimension declares its structure and inherits the mechanics every other dimension uses.

Arithmetic that keeps its meaning

A schema field names a dimension, and the slot behind it carries that dimension through every expression it appears in:

@dataclass(frozen=True)
class Shift:
    """One shift: two clock readings, both declared as ``Instant`` slots."""

    start: ClockRef
    close: ClockRef

Given that the early shift starts at 06:20 and runs eight hours, three questions about its own algebra:

early_shift = (
    subject()
    .given(
        (
            (_shift.start @ clock_from_hhmm(620))
            & (_shift.close @ (_shift.start + duration_hours(8)))
        ).annotate("The early shift starts at 06:20 and runs eight hours.")
    )
    .check("A", (_shift.close @ clock_from_hhmm(1420)).annotate("It closes at 14:20."))
    .check(
        "B",
        ((_shift.close - _shift.start) @ duration_hours(8)).annotate(
            "Close minus start is a duration of eight hours."
        ),
    )
    .check("C", (_shift.close > _shift.start).annotate("It closes after it starts."))
    .block()
)

Check	Proposition	Verdict
A	It closes at 14:20	`VERIFIED`
B	Close minus start is a duration of eight hours	`VERIFIED`
C	It closes after it starts	`VERIFIED`

Check B is the one that shows what a dimension buys. close - start is not an integer difference that happens to be comparable against another integer: the affine structure says two Instants subtract to a Duration, so the result can be compared against duration_hours(8) and against nothing else. Check A runs the same rule in the other direction — an Instant plus a Duration is an Instant, which is why 06:20 + 8h can be checked against a clock reading at all.

What the solver assumes about every slot

A declared invariant is not documentation. Each of these candidates is classified against no givens whatsoever:

DECLARED_BOUND_CASES: tuple[tuple[str, Any], ...] = (
    ("_.risk <= probability(1.0)", _.risk <= probability(1.0)),
    ("_.risk <= probability(0.5)", _.risk <= probability(0.5)),
    ("_.start <= clock_from_hhmm(2359)", _.start <= clock_from_hhmm(2359)),
    ("_.budget >= money_gbp(0)", _.budget >= money_gbp(0)),
)

Proposition	Verdict	Model
`_.risk <= probability(1.0)`	`VERIFIED`	{ risk: 0 }
`_.risk <= probability(0.5)`	`UNKNOWN`	{ risk: 0 }
`_.start <= clock_from_hhmm(2359)`	`VERIFIED`	{ start: 0 }
`_.budget >= money_gbp(0)`	`UNKNOWN`	{ budget: 0 }

Two of them are VERIFIED with nothing given at all, because the classifier realises every dimensioned slot's declared invariant as a constraint before it asks its two questions. Probability declared 0 <= v <= 1, so a risk score is at most 1.0 as a matter of what a probability is — while "at most 0.5" stays UNKNOWN, because the declaration bounds the score at 1 and nothing bounds it at 0.5. The same declaration is what makes a clock reading no later than 23:59. (The model column is the assignment the solver returned — a satisfying example, not a counterexample.)

The last row is the honest counterpart: Money declares no invariant, so a budget is not known to be non-negative. That is a decision recorded in the declaration — money is signed, because credits and refunds are real — and not an omission the analysis papers over.

Combinations the declarations do not admit

The rules above are also the rules for what you cannot write:

REJECTED_CASES: tuple[tuple[str, Any], ...] = (
    # Two dimensions, no rule joining them: Duration's algebra admits Durations.
    ("duration_hours(2) + money_gbp(5)", lambda: duration_hours(2) + money_gbp(5)),  # type: ignore[operator]
    # One dimension, two unit tags: Money's equal-tag precondition fails.
    ("money_gbp(5) + money_usd(5)", lambda: money_gbp(5) + money_usd(5)),
    # Probability is declared comparison-only, so it has no `+` at all. Unlike
    # the two above, this one type-checks: the static layer admits operands of
    # one family, and whether that family *has* a `+` is the declaration's call,
    # made when the value is built.
    (
        "probability(0.2) + probability(0.3)",
        lambda: probability(0.2) + probability(0.3),
    ),
    # Two points on a cycle: an affine structure derives no point + point rule.
    ("clock_hm(9, 30) + clock_hm(1, 0)", lambda: clock_hm(9, 30) + clock_hm(1, 0)),  # type: ignore[operator]
    # The same check one layer down, for a payload Python never authored.
    (
        "normalize([budget >= money_gbp(0), budget >= duration_hours(1)])",
        _cross_dimension_comparison,
    ),
)

Expression	Rejected with
`duration_hours(2) + money_gbp(5)`	`TypeError` — unsupported operand type(s) for +: 'DisplacementValue' and 'DisplacementValue'
`money_gbp(5) + money_usd(5)`	`TypeError` — Precondition failed for + on DisplacementValue(_node=5, unit='GBP', _dimension=Dimension(name='M…
`probability(0.2) + probability(0.3)`	`TypeError` — unsupported operand type(s) for +: 'DisplacementValue' and 'DisplacementValue'
`clock_hm(9, 30) + clock_hm(1, 0)`	`TypeError` — unsupported operand type(s) for +: 'PointValue' and 'PointValue'
`normalize([budget >= money_gbp(0), budget >= duration_hours(1)])`	`ValueError` — dimension mismatch in 'ge' comparison: 'Money' vs 'Duration'

Those are the exceptions the library actually raised, quoted rather than described. The two rows that mix different dimensions are also static errors — the # type: ignore comments above are executable proof of that, since the type gate rejects an ignore that has stopped being necessary. For those, the first line of defence is the type checker, at the moment the rule is written.

The other two expressions type-check, and are refused when the value is built. That split is the design, not a gap: the static layer decides whether two operands belong to the same family, and the declaration decides what that family admits. Two Money values are the same family — it is the declared equal-tag precondition that separates pounds from dollars. Two Probability values are the same family too — it is ScalarKind(arithmetic="comparison-only") that says there is no + to reach for.

The final row is the same check one layer down. A payload that arrives already encoded — from a generated guard, or a client in another language — never passed through Python's type checker, so the normalizer re-derives every slot's dimension from the registry and refuses a comparison between two definitively different ones.

Author your own dimension

The four built-ins are not privileged. A dimension of your own is a params dataclass, a Dimension record, a constructor formula, and one binder line:

@dataclass(frozen=True)
class TokensParams:
    """The one constructor's parameters -- its names survive into the API."""

    count: int


TOKENS = Dimension(
    name="Tokens",
    carrier=Carriers.INT,
    invariant=_Ge(CarrierValue(), 0),  # a token budget cannot go negative
    base_unit="tokens",
    structure=Vector(),  # derives +, -, and scalar multiplication
)


@dataclass(frozen=True)
class TokensConstructors[OfT]:
    """A constructor namespace; generic so dotted access keeps its signature."""

    of: OfT


TOKENS_SPEC = DimensionSpec(
    dimension=TOKENS,
    constructors=TokensConstructors(
        of=ConstructorDescriptor(
            params=TokensParams,
            carrier_expr=param_ref[TokensParams].count,
            result_unit="tokens",
        )
    ),
)

tokens = dim[Literal["Tokens"]](TOKENS_SPEC).ctor(TOKENS_SPEC.constructors.of)

That is the whole declaration — no kernel change, no subclass, and not one operator method. Declaring structure=Vector() derived these:

Operation	Result
`Tokens * scalar`	`Tokens`
`scalar * Tokens`	`Tokens`
`Tokens + Tokens`	`Tokens`
`Tokens - Tokens`	`Tokens`

And the analysis machinery treats it exactly as it treats a built-in. Putting _.budget >= tokens(0) through the same normalizer, against a registry holding Tokens and nothing else:

slot sorts      = { budget: int }
slot dimensions = { budget: Tokens }
invariants      = 1 realised

The slot's sort and dimension are inferred from the literal it is compared against, and the invariant declared above is realised as a constraint on that slot — with no Tokens-specific code anywhere in the wire, the registry artifact, or the normalizer.

Limits today

Tags are tags, not scales. Arithmetic across currencies is refused, as the table above shows. A comparison across them is not: both sides are Money, and the dimension check works at that level.
Not every entry point runs every check. The classification path infers slot dimensions and asserts their declared invariants, but the cross-dimension comparison rejection above belongs to the normalization pass that the guard generation and cross-language paths run.
A cycle is declared, not yet computed. CyclicAffine's modulus ships in the registry artifact for clients that need it; the analyses treat an Instant as a bounded integer and do not wrap arithmetic around midnight.
A solver is built with a registry, not handed one. A request carries the digest of the declarations it was built against, and a mismatch is an error rather than a quietly different analysis — so a user dimension reaches a deployed solver as part of its registry, not as a per-request payload.

How reasoning works · Guardrails over a whole rule set · Dimensions API reference