docs(language): the expressions page says why a case when: cannot compare expressions

[FBumann]

Prompt: Look at the discussion in #469 (comment) […] Help me make this clear […] Do it as a stacked pr

Note

The following content was generated by AI.

Stacked on #469. One paragraph of docs/reference/language/expressions.md is rewritten: it now gives the reason a case when: may not compare expressions, and quotes the loader's message word for word.

What this changes

The paragraph, before and after

Before:

A case when: that compares expressions cannot be proved apart from its neighbours before the data arrives, so it is refused there with the rewrite: compare one parameter against a literal, or precompute the test as a boolean parameter.

After:

A case when: may not compare expressions. The loader proves the cases of a cases: block apart at load: no two of them may claim one coordinate. It proves that by trying every value the masks name. A comparison of expressions names no value, because only the data decides whether c > 2 * k holds. There is nothing to try, so the loader refuses the block:

Named expression 'e': cases wide and narrow cannot be told apart before the data arrives: it compares expressions, whose values only the data decides — compare one parameter against a literal, or precompute the test as a boolean parameter and test that. Two cases claiming one coordinate would give it two values, so this is refused the way a proven overlap is.

A variable's where and a constraint's where are not held to this, because neither is proved apart from anything.

Three things are new. The reason, which is the apartness proof rather than a general bar on complexity in a when:. The message, quoted whole, as AGENTS.md asks. The scope, which says that no other where is held to the rule.

The forward link lands on #the-rules-that-keep-the-cases-apart, the section that owns the rule, so the fact keeps one home.

Why

The reason the old sentence did not land

https://github.com/energy-models/math-spec/pull/469#discussion_r4017530831 reports that the sentence does not read. It carried four claims in one 34-word sentence, and its subject was "a case when: that compares expressions", which cannot be proved apart from anything on its own. "Proved apart" is house vocabulary, and the section that glosses it sits 130 lines further down the page.

The mechanism the paragraph now names is in src/math_spec/exclusivity.py. _Grid.of walks every atom of both masks and _observe records the value each names, _cells_for turns each value into the regions around it, and _witness evaluates both masks in every cell of the product. An ArithmeticComparisonNode names no value, so _observe raises Undecidable.

Verified

uv venv, Python 3.11, since pixi is not installable in this environment:

• mkdocs build --strict: passes. The one error on an unmodified run is Couldn't load inventory https://docs.python.org/3/objects.inv, which this environment's proxy refuses; with those two lines removed from mkdocs.yml the build is clean, so the new anchor resolves.
• pytest tests/test_docs.py tests/test_reading_page.py: 34 passed.
• prettier --check, typos, reuse lint: clean.
• The quoted message is compared character for character against what to_spec raises for a two-case model split on c > 2 * k / c <= 2 * k. Identical.
• Sentence measure, by the script in the docs-writing skill: n 139 avg 17.5 median 16 over25 27 before, n 144 avg 17.2 median 16 over25 26 after.
• Not run: compile-tex, ruff, pyrefly, taplo, zizmor, and the rest of pytest. No Python changed.

Not done here

• The restriction is not lifted. https://github.com/energy-models/math-spec/pull/469#discussion_r4017605575 asks whether it could be. _subject_of already gives every comparison of expressions one placeholder subject that nothing reaches, and keying that subject on the two sides, sharing it between a pair with complementary comparators, and giving it [True, False] cells the way lookup_pair does would prove c > 2 * k apart from c <= 2 * k. That is a feat on src/, and it belongs in its own PR with its own tests.
• The bullet under "The rules that keep the cases apart" is untouched. It already says a pair the check cannot decide is refused. A second copy of the arithmetic case there would drift.

🤖 Generated with Claude Code

https://claude.ai/code/session_011wswYDGW6H9n5Sod42NwUM

---

Generated by Claude Code

[read-the-docs-community]

Documentation build overview

📚 math-spec | 🛠️ Build #34574599 | 📁 Comparing cccf909 against latest (5656b11)

  🔍 Preview build  

9 files changed · ± 9 modified

± Modified

• CHANGELOG/index.html
• about/limits/index.html
• reference/notation/index.html
• reference/language/errors/index.html
• reference/language/expressions/index.html
• reference/language/reading/index.html
• reference/math_spec/lowering/index.html
• reference/math_spec/program/index.html
• reference/math_spec/resolution/index.html