fix(typesetting): a cased expression whose otherwise holds a variable is set as one the solver decides

[FBumann]

Prompt: "Lets do a PR stacked that fixes all of those!" — the six findings from a review of #168.

Stacked on feat/cases-proved-apart, so it targets #168 rather than main.

Note

The following content was generated by AI.

Five fixes from a review pass over #168, four of them fallout from #251's default: → otherwise: rename. Each lands with a test that is red without it.

A cased expression whose only variable is in its otherwise: printed as data. chosen_expressions read block.cases alone, so once the fallback moved out of cases: it stopped counting toward what the block is. previous_status in the commitment example is exactly that shape — two cases holding a constant and a parameter, the variable in the fallback — so its generated page said \mathrm{previous\_status} while the hand-written language reference said \mathit. The tree contradicted itself; docs/examples/commitment.md is regenerated here.

An error inside a case named the constraint that used it. A cased expression is expanded where its name stood, so a fault in an arm was reported 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, the arm with no when is named otherwise rather than a case (what validation, dimensions and expansion already call it), and an exact repeat prints once.

n < 1 against n > 0 on an int was refused at n is 0.5. The gap between two literals got a midpoint representative regardless of dtype, so an integer partition was refused with a witness the data cannot produce and a rewrite the file had already made. Dates were already discrete for this reason; integers now are too.

The soundness fuzz could not fail. Every pair it built was a complement — m against not m — so its grid assertion was X and not X. Collapsing every subject to a single cell, the largest cell-coverage bug there is, left both seeds green while nine other tests in the file went red.

An unreachable guard and five stale default spellings, the retired name in program.py, format.py and two test docstrings.

Evidence per fix

fix	test	on the unfixed tree
the fallback is chosen	test_the_fallback_reaching_a_variable_is_chosen	fails in all three formats
the arm names its declaration	test_a_fault_in_an_arm_names_the_declaration_and_is_reported_once, test_the_fallback_is_not_named_as_a_case	both fail
integers are discrete	test_an_integer_admits_no_value_between_its_bands	fails; test_a_magnitude_still_admits_one guards the over-correction and fails if discrete is forced true
the fuzz is real	test_a_pair_proved_apart_stays_apart_on_a_finer_grid	passed both seeds under the one-cell mutation before, fails both after
the dead guard	—	deleting it leaves the suite green, which is the finding

The fuzz, same atoms and grid, 2000 draws:

	pairs proved apart	with a grid point both claim
real implementation	221	0
_cells_for collapsed to one cell	1770	1295

Checks

pixi run ci clean on the committed tree: lint (all eleven hooks, pyrefly included), 884 passed, mkdocs build --strict, 27 TeX documents compiled.

884 against the base branch's 877: seven new tests — one across three formats, two in test_exclusivity.py, two in test_validation.py.

Departed from a default: one PR rather than five stacked. These are five findings from one review pass on an unmerged branch, and five PRs stacked on an open PR would cost more to land than to read. Split into five commits instead.

Not done here. Two minor findings from the same review, left out to keep this to the six:

• expression: .nan reaches the parser as the name nan and fails with 'nan' not found. _number_is_an_expression argues booleans are left to fail because the type reads better than the spelling; the same argument covers non-finite floats.
• cases: {} beside an otherwise: now fails with raw pydantic (Dictionary should have at least 1 item after validation, not 0). The retired message named the rewrite — "which is what a plain expression: already says". Restoring it means giving up minProperties: 1 in the published schema, which is a trade worth deciding rather than assuming.

#168's own body still describes the default design throughout — the YAML block, the "the name is reserved and the position is fixed" paragraph, and the near-miss list. #251 flagged that as its own not-done; it wants rewriting rather than appending to, and it is yours rather than mine.

[read-the-docs-community]

Documentation build overview

📚 math-spec | 🛠️ Build #34301083 | 📁 Comparing c11821e against latest (a9237ec)

  🔍 Preview build  

16 files changed · + 2 added · ± 14 modified

+ Added

• examples/commitment/index.html
• reference/math_spec/exclusivity/index.html

± Modified

• examples/index.html
• reference/notation/index.html
• reference/language/expressions/index.html
• reference/math_spec/dimensions/index.html
• reference/math_spec/expression_parser/index.html
• reference/math_spec/model/index.html
• reference/math_spec/program/index.html
• reference/math_spec/validation/index.html
• reference/math_spec/typesetting/format/index.html
• reference/math_spec/typesetting/latex/index.html
• and 4 more...