From a67d0eca08ffed42b1c95edff14cd2bd6c6a8962 Mon Sep 17 00:00:00 2001
From: FBumann <117816358+FBumann@users.noreply.github.com>
Date: Sun, 30 Aug 2026 19:54:56 +0200
Subject: [PATCH 1/5] fix(typesetting): a cased expression whose otherwise
 holds a variable is set as one the solver decides
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Reading only `cases:` for what a block is left the fallback out, so a
quantity whose only variable sits there printed upright — the notation
for something the model is handed rather than something it solves for.
`previous_status` in the commitment example is exactly that shape, and
its generated page disagreed with the hand-written one in the language
reference.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XJMiQWNo9b5VD3Aac5gTXX
---
 docs/examples/commitment.md          |  4 ++--
 src/math_spec/typesetting/symbols.py | 21 ++++++++++++++++++---
 tests/typesetting/test_cases.py      | 13 +++++++++++++
 3 files changed, 33 insertions(+), 5 deletions(-)

diff --git a/docs/examples/commitment.md b/docs/examples/commitment.md
index aa47a41c..48154c5a 100644
--- a/docs/examples/commitment.md
+++ b/docs/examples/commitment.md
@@ -145,13 +145,13 @@ $$p_{t,g} \ge \mathit{status}_{t,g} \cdot \mathrm{p}^{\mathrm{min}}_{g} \qquad \
 
 **`ramp_up`**
 
-$$p_{t,g} - p_{t \boxminus_{0} 1,g} \le \mathrm{ramp\_limit}_{g} \cdot \mathrm{previous\_status}_{t,g} + \mathrm{start\_up\_limit}_{g} \cdot \left( 1 - \mathrm{previous\_status}_{t,g} \right) \qquad \forall\thinspace t \in \mathcal{T},\enspace g \in \mathcal{G}$$
+$$p_{t,g} - p_{t \boxminus_{0} 1,g} \le \mathrm{ramp\_limit}_{g} \cdot \mathit{previous\_status}_{t,g} + \mathrm{start\_up\_limit}_{g} \cdot \left( 1 - \mathit{previous\_status}_{t,g} \right) \qquad \forall\thinspace t \in \mathcal{T},\enspace g \in \mathcal{G}$$
 
 #### Definitions
 
 **`previous_status`**
 
-$$\mathrm{previous\_status}_{t,g} = \begin{cases} 1 & \text{if } \neg \mathrm{committable}_{g} \cr \mathrm{status}^{\mathrm{initial}}_{g} & \text{if } \mathrm{committable}_{g} \wedge \mathrm{pos}(t) = 0 \cr \mathit{status}_{t - 1,g} & \text{otherwise} \end{cases} \qquad \forall\thinspace t \in \mathcal{T},\enspace g \in \mathcal{G}$$
+$$\mathit{previous\_status}_{t,g} = \begin{cases} 1 & \text{if } \neg \mathrm{committable}_{g} \cr \mathrm{status}^{\mathrm{initial}}_{g} & \text{if } \mathrm{committable}_{g} \wedge \mathrm{pos}(t) = 0 \cr \mathit{status}_{t - 1,g} & \text{otherwise} \end{cases} \qquad \forall\thinspace t \in \mathcal{T},\enspace g \in \mathcal{G}$$
 
 #### Variable domains
 
diff --git a/src/math_spec/typesetting/symbols.py b/src/math_spec/typesetting/symbols.py
index 6cb89d25..ff3c1191 100644
--- a/src/math_spec/typesetting/symbols.py
+++ b/src/math_spec/typesetting/symbols.py
@@ -25,7 +25,9 @@
 from math_spec.resolution import Namespace, expression_of
 
 if TYPE_CHECKING:
-    from math_spec.model import _ExpandedSpec
+    from collections.abc import Iterator
+
+    from math_spec.model import ExpressionBlock, _ExpandedSpec
     from math_spec.typesetting.format import Format
 
 __all__ = ['SymbolTable', 'Symbols']
@@ -100,12 +102,25 @@ def chosen_expressions(schema: _ExpandedSpec) -> frozenset[str]:
         name
         for name in printed_expressions(schema)
         if any(
-            carries_variable(expression_of(case.expression, schema, namespace, f"expression '{name}', case '{label}'"))
-            for label, case in schema.expressions[name].cases.items()
+            carries_variable(expression_of(text, schema, namespace, f"expression '{name}', {where}"))
+            for text, where in _values_of(schema.expressions[name])
         )
     )
 
 
+def _values_of(block: ExpressionBlock) -> Iterator[tuple[str, str]]:
+    """Every value a cased block holds, the ``otherwise:`` included, and where it sits.
+
+    The fallback is a value of the quantity like any case's, so it decides what
+    the block *is* alongside them: a block whose only variable is there is one
+    the solver returns, and printing it upright would call it data.
+    """
+    for label, case in block.cases.items():
+        yield case.expression, f"case '{label}'"
+    assert block.otherwise is not None
+    yield block.otherwise, 'otherwise'
+
+
 class Symbols:
     r"""How every declared name prints: overrides first, derivation for the rest.
 
diff --git a/tests/typesetting/test_cases.py b/tests/typesetting/test_cases.py
index fb003b41..91e2a159 100644
--- a/tests/typesetting/test_cases.py
+++ b/tests/typesetting/test_cases.py
@@ -100,6 +100,19 @@ def test_a_case_reaching_a_variable_is_chosen(fmt: Format):
     assert fmt.italic('headroom') in typeset(decided, fmt, legend=False)
 
 
+@EVERY_FORMAT
+def test_the_fallback_reaching_a_variable_is_chosen(fmt: Format):
+    """The `otherwise:` is a value of the quantity like any case's.
+
+    `previous_status` in the commitment example is this shape and no other: its
+    two cases are a constant and a parameter, and the variable is in the
+    fallback alone. Read only the cases and the block prints upright, which
+    says the model was handed a quantity it in fact solves for.
+    """
+    decided = override(CASED, **{'expressions.headroom.otherwise': 'p'})
+    assert fmt.italic('headroom') in typeset(decided, fmt, legend=False)
+
+
 @EVERY_FORMAT
 def test_a_definition_naming_another_one_prints_both(fmt: Format):
     """The cases are walked too, so the collection runs to a fixpoint."""

From b7f70eb82f69b6bcb0fac2a5facab490bb26c70f Mon Sep 17 00:00:00 2001
From: FBumann <117816358+FBumann@users.noreply.github.com>
Date: Sun, 30 Aug 2026 19:55:04 +0200
Subject: [PATCH 2/5] fix(language): an error inside a case names the
 expression that declares it, and is printed once
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

A cased expression is expanded where its name stood, so a fault in one
of its arms was reported against the constraint that pulled it in — as
`Constraint 'ramp_up', case 'boundary'`, a case on a constraint that has
none, once per constraint naming the expression. The arm now names its
declaration, and the arm with no `when` is named `otherwise` rather than
a case, which is what every other check already calls it. Two errors
that differ at all carry different contexts, so an exact repeat is one
fault seen twice and is printed once.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XJMiQWNo9b5VD3Aac5gTXX
---
 src/math_spec/resolution.py | 14 +++++++++++++-
 src/math_spec/validation.py | 13 ++++++++++++-
 tests/test_validation.py    | 35 +++++++++++++++++++++++++++++++++++
 3 files changed, 60 insertions(+), 2 deletions(-)

diff --git a/src/math_spec/resolution.py b/src/math_spec/resolution.py
index 95d92e83..92b37689 100644
--- a/src/math_spec/resolution.py
+++ b/src/math_spec/resolution.py
@@ -270,6 +270,18 @@ def resolve_expression(
     return None if len(errors) > before else resolved
 
 
+def _arm_context(name: str, arm: CaseArm) -> str:
+    """Where an error inside one arm is reported: the declaration, not the use site.
+
+    A cased expression is expanded where its name stood, so the context in hand
+    at that point is the constraint's — and naming it would report a case on a
+    constraint that has none. The arm without a ``when`` is the block's
+    ``otherwise:``, which is not a case and is not named as one.
+    """
+    where = 'otherwise' if arm.when is None else f"case '{arm.label}'"
+    return f"Named expression '{name}', {where}"
+
+
 def _resolve_arith(
     node: ArithmeticNode,
     ns: Namespace,
@@ -372,7 +384,7 @@ def _resolve_arith(
     if isinstance(node, CasesNode):
         arms = []
         for arm in node.arms:
-            arm_context = f"{context}, case '{arm.label}'"
+            arm_context = _arm_context(node.name, arm)
             when = None if arm.when is None else _resolve_where(arm.when, ns, arm_context, errors)
             arms.append(CaseArm(arm.label, when, _resolve_arith(arm.value, ns, arm_context, errors)))
         return CasesNode(node.name, tuple(arms))
diff --git a/src/math_spec/validation.py b/src/math_spec/validation.py
index dd7c3bfb..f6542465 100644
--- a/src/math_spec/validation.py
+++ b/src/math_spec/validation.py
@@ -60,6 +60,17 @@ def to_spec(model: str | Path | dict[str, Any] | Spec) -> Spec:
     return Spec.model_validate(model if isinstance(model, dict) else read_yaml(Path(model)))
 
 
+def _once(errors: list[str]) -> str:
+    """The errors as one message, an identical sentence kept only the first time.
+
+    A cased expression is expanded at every use, so a fault in one of its arms
+    is found again at each constraint naming it. Every error carries the
+    context it was found in, so two that differ at all are two faults and an
+    exact repeat is one seen twice.
+    """
+    return '\n'.join(dict.fromkeys(errors))
+
+
 def validate_expressions(schema: Spec) -> None:
     """Validate and resolve every expression and where string in *schema*.
 
@@ -127,7 +138,7 @@ def validate_expressions(schema: Spec) -> None:
         _check_expression(schema.objective.expression, schema, ns, 'The objective', errors, comparison=False, ceiling=2)
 
     if errors:
-        raise SchemaError('\n'.join(errors))
+        raise SchemaError(_once(errors))
 
     check_schema(schema)
 
diff --git a/tests/test_validation.py b/tests/test_validation.py
index 28f1250a..28a8da07 100644
--- a/tests/test_validation.py
+++ b/tests/test_validation.py
@@ -761,6 +761,41 @@ def test_a_constraint_naming_it_carries_the_declared_frame(self):
         with pytest.raises(DimensionError, match='snapshot'):
             to_spec(model)
 
+    def test_a_fault_in_an_arm_names_the_declaration_and_is_reported_once(self):
+        """The block is expanded at every use, and the fault is in one place.
+
+        Naming the use site would report a case on a constraint that has none,
+        and one sentence per constraint reading the expression is the same
+        fault as many.
+        """
+        model = _cased({'opening': {'when': 'position(snapshot) == 0', 'expression': 'nope'}})
+        model['constraints'] = {
+            name: {'foreach': ['snapshot', 'generator'], 'expression': f'p <= headroom + {n}'}
+            for n, name in enumerate(('cap', 'floor'))
+        }
+        with pytest.raises(SchemaError) as caught:
+            to_spec(model)
+
+        message = str(caught.value)
+        assert message.count("'nope' not found") == 1, 'two constraints read it; the fault is reported once'
+        assert "Named expression 'headroom', case 'opening'" in message
+        assert 'Constraint' not in message, "the arm is the declaration's, not the use site's"
+
+    def test_the_fallback_is_not_named_as_a_case(self):
+        """`otherwise:` is what is left, not a region like the cases are.
+
+        Reached through a constraint, which is where the arms are walked a
+        second time and where the label was read off the arm.
+        """
+        model = _cased(otherwise='nope')
+        model['constraints'] = {'cap': {'foreach': ['snapshot', 'generator'], 'expression': 'p <= headroom'}}
+        with pytest.raises(SchemaError) as caught:
+            to_spec(model)
+
+        message = str(caught.value)
+        assert "Named expression 'headroom', otherwise: 'nope' not found" in message
+        assert "case 'otherwise'" not in message, 'the fallback is not one of the cases'
+
     def test_a_case_may_name_another_expression(self):
         model = _cased({'opening': {'when': 'position(snapshot) == 0', 'expression': 'spare'}})
         model['expressions']['spare'] = 'p_max * 2'

From b8c8970ee71817a826d8b0c537b91a603fe4d61b Mon Sep 17 00:00:00 2001
From: FBumann <117816358+FBumann@users.noreply.github.com>
Date: Sun, 30 Aug 2026 19:55:20 +0200
Subject: [PATCH 3/5] fix(language): two integer bands with no integer between
 them are proved apart
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The cells for an ordered subject put a representative in every gap
between the literals a pair of masks names, and the midpoint it chose
was one no integer can be. So `n < 1` against `n > 0` on an `int` was
refused with a witness of `n is 0.5` — a coordinate the data cannot
produce, naming a rewrite the file had already made. A date was already
handled this way; an integer is discrete for the same reason and now
says so.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XJMiQWNo9b5VD3Aac5gTXX
---
 src/math_spec/exclusivity.py | 22 +++++++++++++++-------
 tests/test_exclusivity.py    | 16 ++++++++++++++++
 2 files changed, 31 insertions(+), 7 deletions(-)

diff --git a/src/math_spec/exclusivity.py b/src/math_spec/exclusivity.py
index 9edc3f84..6bebf32f 100644
--- a/src/math_spec/exclusivity.py
+++ b/src/math_spec/exclusivity.py
@@ -296,7 +296,10 @@ def _cells_for(subject: Subject, values: set[Any], dtypes: Mapping[str, str]) ->
             raise Undecidable(msg)
         return [True, False, Special.NULL]
     numeric = _numeric(dtype, values)
-    cells: list[Cell] = list(_ordered_cells(values) if numeric or _dated(values) else _label_cells(values))
+    dated = _dated(values)
+    cells: list[Cell] = list(
+        _ordered_cells(values, discrete=dated or dtype == 'int') if numeric or dated else _label_cells(values)
+    )
     # A dimension's coordinates are its own index, so there is no null among
     # them; everything else may be absent, and absence is a region of its own
     # because a null compares false and is not `defined`.
@@ -320,7 +323,7 @@ def _dated(literals: set[Any]) -> bool:
     return bool(literals) and all(isinstance(value, datetime.date) for value in literals)
 
 
-def _ordered_cells(literals: set[Any]) -> list[Cell]:
+def _ordered_cells(literals: set[Any], *, discrete: bool) -> list[Cell]:
     """Each literal, and one representative of the gap on either side of it."""
     if not literals:
         return [0.0]
@@ -332,7 +335,7 @@ def _ordered_cells(literals: set[Any]) -> list[Cell]:
         following = values[index + 1] if index + 1 < len(values) else None
         if following is None:
             continue
-        between = _between(value, following, step)
+        between = _between(value, following, step, discrete=discrete)
         if between is not None:
             cells.append(between)
     cells.append(values[-1] + step)
@@ -348,13 +351,18 @@ def _step(value: Any) -> Any:
     return 1.0
 
 
-def _between(value: Any, following: Any, step: Any) -> Any | None:
+def _between(value: Any, following: Any, step: Any, *, discrete: bool) -> Any | None:
     """A value strictly between two literals, where the type admits one.
 
-    A magnitude always does — the midpoint. A date is discrete, so the gap has
-    to be wider than one unit before there is anything in it to stand for.
+    A continuous magnitude always admits one — the midpoint. A **discrete**
+    subject, an ``int`` or a date, need not: between 0 and 1 there is no
+    integer and between two adjacent days no date, so the gap has to be wider
+    than one unit before there is anything in it to stand for. A midpoint
+    invented there is a coordinate the subject cannot take, and the only thing
+    it can do is manufacture a witness — refusing ``n < 1`` against ``n > 0``,
+    which no integer claims twice, at a coordinate named ``0.5``.
     """
-    if isinstance(value, datetime.date):
+    if discrete:
         return value + step if following - value > step else None
     return (value + following) / 2.0
 
diff --git a/tests/test_exclusivity.py b/tests/test_exclusivity.py
index 9b9e70e6..be95e94b 100644
--- a/tests/test_exclusivity.py
+++ b/tests/test_exclusivity.py
@@ -41,6 +41,7 @@
         'kind': {'dims': ['storage'], 'dtype': 'str'},
         'soc_initial': {'dims': ['storage']},
         'capacity': {'dims': ['storage']},
+        'age': {'dims': ['storage'], 'dtype': 'int'},
     },
     'variables': {'soc': {'foreach': ['snapshot', 'storage']}},
     'constraints': {'balance': {'foreach': ['snapshot', 'storage'], 'expression': 'soc == 1'}},
@@ -119,6 +120,21 @@ def test_numeric_bands(self, schema: Spec):
         cases = {'small': 'capacity and capacity <= 10', 'large': 'capacity and capacity > 10'}
         assert refusals(schema, cases) == [], 'a capacity is at most 10 or above it'
 
+    def test_an_integer_admits_no_value_between_its_bands(self, schema: Spec):
+        """`age` is declared `int`, and the two bands are complements over the integers.
+
+        A midpoint invented in the gap is a coordinate the subject cannot take,
+        and the refusal it manufactures names `0.5` — a value no data produces,
+        with a rewrite the file has already followed.
+        """
+        cases = {'new': 'age < 1', 'old': 'age > 0'}
+        assert refusals(schema, cases) == [], 'an integer is below 1 or above 0, never between'
+
+    def test_a_magnitude_still_admits_one(self, schema: Spec):
+        """The mirror: `capacity` is a float, so 0.5 is a coordinate it can take."""
+        cases = {'small': 'capacity < 1', 'large': 'capacity > 0'}
+        assert refusals(schema, cases), 'a float between the two bands is claimed by both'
+
     def test_a_when_of_true_is_not_a_default(self, schema: Spec):
         """`default` is the case *without* a `when`, and nothing here stands in for it.
 

From 5b96fa12e414ebd231959e82ff85199122ac366a Mon Sep 17 00:00:00 2001
From: FBumann <117816358+FBumann@users.noreply.github.com>
Date: Sun, 30 Aug 2026 19:55:34 +0200
Subject: [PATCH 4/5] test(exclusivity): the soundness fuzz draws two masks
 apart rather than one and its negation
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Every pair it generated was a complement by construction, so the grid
assertion was `X and not X` — false at every point, under every
implementation, for every set of cells. Collapsing each subject to a
single cell, which is the most a cell-coverage bug could ever be, left
both seeds green while nine other tests in the file went red. Drawn
independently and filtered to the pairs the check proves apart, the same
mutation now fails it 1295 times over.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XJMiQWNo9b5VD3Aac5gTXX
---
 tests/test_exclusivity.py | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/tests/test_exclusivity.py b/tests/test_exclusivity.py
index be95e94b..5f6fae6d 100644
--- a/tests/test_exclusivity.py
+++ b/tests/test_exclusivity.py
@@ -213,6 +213,12 @@ class TestSoundness:
     infinities, an absent value, labels the masks never name — and asserts that
     nothing it proved apart has a point claimed by both.
 
+    **The two masks are drawn independently**, and only the pairs the check
+    proves apart are walked. A pair built as a complement — `m` against
+    `not m` — makes the assertion `X and not X`, false at every point under
+    every implementation, so a fuzz over those shapes cannot fail and certifies
+    nothing.
+
     What it does not test is the reading of an individual atom: ground truth
     here evaluates through the same `_evaluate` the checker uses, so a misread
     atom would agree with itself. That is what `TestProvesApart` and
@@ -270,12 +276,8 @@ def test_a_pair_proved_apart_stays_apart_on_a_finer_grid(self, schema: Spec, see
         rng = random.Random(seed)
         dtypes = namespace.dtypes
         proved = 0
-        for _ in range(300):
-            split = self._mask(rng, atoms)
-            first, second = split, NotNode(split)
-            if rng.random() < 0.5:
-                inner = self._mask(rng, atoms)
-                first, second = AndNode(split, inner), AndNode(split, NotNode(inner))
+        for _ in range(2000):
+            first, second = self._mask(rng, atoms), self._mask(rng, atoms)
             if list(overlapping({'a': first, 'b': second}, schema)):
                 continue
             proved += 1
@@ -285,4 +287,4 @@ def test_a_pair_proved_apart_stays_apart_on_a_finer_grid(self, schema: Spec, see
             for point in grid:
                 both = _evaluate(first, point, frame) and _evaluate(second, point, frame)
                 assert not both, f'both cases claim {point} — the cells hid a witness'
-        assert proved > 50, f'only {proved} pairs proved apart; the fuzz is not exercising the check'
+        assert proved > 150, f'only {proved} pairs proved apart; the fuzz is not exercising the check'

From c11821e7f3c2fa88ee63fa4ad7073987ad0ddaa9 Mon Sep 17 00:00:00 2001
From: FBumann <117816358+FBumann@users.noreply.github.com>
Date: Sun, 30 Aug 2026 19:55:50 +0200
Subject: [PATCH 5/5] chore: drop an unreachable lookup guard and the default
 spelling the otherwise rename left behind
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`_lower_expression` looked its name up in the very mapping its only
caller iterates, so the `KeyError` and its `did_you_mean` were a branch
nothing reaches — and the one place in the file raising something other
than `LanguageError`. Deleting it leaves the suite green, which is what
the guard was worth.

Beside it, five docstrings and a test name still called the fallback
`default`, which the language no longer has.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XJMiQWNo9b5VD3Aac5gTXX
---
 src/math_spec/lowering.py           | 10 +++-------
 src/math_spec/program.py            | 13 +++++++------
 src/math_spec/typesetting/format.py |  2 +-
 tests/test_exclusivity.py           |  6 +++---
 4 files changed, 14 insertions(+), 17 deletions(-)

diff --git a/src/math_spec/lowering.py b/src/math_spec/lowering.py
index 94b9abf9..f51b3097 100644
--- a/src/math_spec/lowering.py
+++ b/src/math_spec/lowering.py
@@ -33,7 +33,7 @@
 
 import math_spec.program as program
 from math_spec.dimensions import dims_of
-from math_spec.errors import LanguageError, did_you_mean
+from math_spec.errors import LanguageError
 from math_spec.expression_parser import (
     ArithmeticNode,
     BinaryOperatorNode,
@@ -228,16 +228,12 @@ def _lower_expression(schema: _ExpandedSpec, ns: Namespace, name: str) -> progra
     """Compile the named expression *name* into a program expression.
 
     Raises:
-        KeyError: No named expression called *name*.
         LanguageError: A construct outside the streaming language.
     """
-    expanded = schema
     context = f"named expression '{name}'"
-    if name not in expanded.expressions:
-        raise KeyError(f"unknown named expression '{name}'. " + did_you_mean(name, expanded.expressions))
-    ast = expression_of(name, expanded, ns, context)
+    ast = expression_of(name, schema, ns, context)
     assert not isinstance(ast, ComparisonNode), 'load-time validation refuses a comparison in a named expression'
-    return _Lowering(expanded, context).expr(ast)
+    return _Lowering(schema, context).expr(ast)
 
 
 # ---------------------------------------------------------------------------
diff --git a/src/math_spec/program.py b/src/math_spec/program.py
index 6889904c..2399d5ef 100644
--- a/src/math_spec/program.py
+++ b/src/math_spec/program.py
@@ -407,10 +407,11 @@ class Window(Expression):
 class Region:
     """One region of a :class:`Cases`: where it applies, and the value there.
 
-    ``when`` is stated on every region, the file's ``default`` included — its
-    mask is the negation of the others, resolved once here rather than by each
-    consumer in turn. A consumer builds a region without holding the rest in
-    mind, and both facts it needs are on the region it is reading.
+    ``when`` is stated on every region, the one the file wrote as
+    ``otherwise:`` included — its mask is the negation of the others, resolved
+    once here rather than by each consumer in turn. A consumer builds a region
+    without holding the rest in mind, and both facts it needs are on the region
+    it is reading.
     """
 
     when: WhereNode
@@ -422,8 +423,8 @@ class Cases(Expression):
     """A value defined by region — exactly one region applies at each coordinate.
 
     The language proves the regions apart before any data binds, and the
-    file's ``default`` covers whatever the rest leave, so they are disjoint and
-    total by construction: a consumer adds the regions rather than ranking
+    file's ``otherwise:`` covers whatever the rest leave, so they are disjoint
+    and total by construction: a consumer adds the regions rather than ranking
     them, and needs neither an order nor a tie-break.
 
     Not a shape operator — every region spans the dims the expression does, and
diff --git a/src/math_spec/typesetting/format.py b/src/math_spec/typesetting/format.py
index 2fe1681b..04e344d9 100644
--- a/src/math_spec/typesetting/format.py
+++ b/src/math_spec/typesetting/format.py
@@ -171,7 +171,7 @@ def summation(self, domain: str, body: str) -> str: ...
     def cases(self, arms: list[tuple[str, str]]) -> str:
         """A value defined by region: ``(value, condition)`` per arm, in order.
 
-        Both halves arrive rendered — which arm is the ``default`` is the walk's
+        Both halves arrive rendered — which arm is the fallback is the walk's
         to decide, and this only stacks the rows.
         """
         ...
diff --git a/tests/test_exclusivity.py b/tests/test_exclusivity.py
index 5f6fae6d..1077beef 100644
--- a/tests/test_exclusivity.py
+++ b/tests/test_exclusivity.py
@@ -91,7 +91,7 @@ def test_a_category_split(self, schema: Spec):
         assert refusals(schema, cases) == [], 'a storage carries one kind, so the two labels are apart'
 
     def test_the_ramp_regimes_from_the_issue(self, schema: Spec):
-        """The three quantities #2 factors a PyPSA ramp limit into, less each one's `default`.
+        """The three quantities #2 factors a PyPSA ramp limit into, less each one's `otherwise`.
 
         The point of putting cases on an expression rather than on the
         constraint: three independent axes multiply into eight constraint cases
@@ -135,8 +135,8 @@ def test_a_magnitude_still_admits_one(self, schema: Spec):
         cases = {'small': 'capacity < 1', 'large': 'capacity > 0'}
         assert refusals(schema, cases), 'a float between the two bands is claimed by both'
 
-    def test_a_when_of_true_is_not_a_default(self, schema: Spec):
-        """`default` is the case *without* a `when`, and nothing here stands in for it.
+    def test_a_when_of_true_is_not_a_fallback(self, schema: Spec):
+        """The fallback is the block's `otherwise:`, and nothing inside `cases:` stands in for it.
 
         A mask that happens to be true everywhere is read as any other mask is,
         so it collides with every case beside it.