feat: a static partition check for expression cases

[FBumann]

Prototype for #2, stacked on #31 — base is claude/new-session-divgg4, so the diff here is one module and its tests. Retarget to main once #31 lands.

Follows @FabianHofmann's proposal: the cases go on a named expression, not on the constraint. Not wired into the schema — expressions: accepts neither foreach nor cases yet, and that is the next change rather than this one. This is the decision procedure the #2 argument turns on, so it can be judged on what it proves and what it refuses.

Why expressions

Three independent axes — horizon boundary, is_modular, is_committable — multiply at the constraint level and add at the expression level: eight constraint cases against seven expression cases. The count is the smaller half of it. The eight write the ramp inequality eight times, so a change to it is eight edits that nothing checks agree; the seven write it once:

expression: p - previous_p <= ramp_limit_up * ramp_capacity * previous_status

It also answers the objection that opened #2 better than a constraint cases: did: the constraint keeps one name and one expression, so Generator_ramp_limit_up.dual is unambiguous by construction rather than by proof.

And the obligation factors. If each expression's cases partition independently, the product is automatically a partition of the constraint's rows — 2+2+3 small proofs rather than one eight-way one. The three quantities #2 factors that ramp limit into are a test here.

What it decides

check_partition(cases, schema) answers whether a set of when masks claims each coordinate of the frame exactly once. Three obligations, all the same unsatisfiability question:

disjoint	case_i AND case_j unsatisfiable, for each pair
exhaustive	NOT (case_1 OR … OR case_n) unsatisfiable
no dead case	case_i alone satisfiable

Three outcomes: PARTITION, VIOLATED, UNDECIDED. The third is refused by a caller exactly as the second is; a checker that guesses where it cannot decide buys nothing over no checker.

Atoms are grouped by the subject they talk about and each subject is cut into cells, so equality against distinct labels comes out exclusive. A purely propositional reading invents a region where one storage is both a battery and hydrogen, and refuses the category split that motivates the feature.

case set	verdict
the three ramp quantities from #2	partition
the storage split from #2	partition
a written complement, x / NOT (x)	partition
an ordering on a position, == 0 / > 0	partition — what #31 unblocks
the same counted from the back, == -1 / < -1	partition
a category split, with a case for the labels it does not name	partition
numeric bands, with a case for an absent capacity	partition
first/last/middle on a dimension declaring values:	partition
two cases that can both claim a coordinate	violated, naming both and a witness
a coordinate no case claims	violated
a case whose when can never hold	violated
bare soc_initial vs soc_initial == 0	violated — defined is not non-zero
first/last on a data-bound axis	undecided — 0 and -1 are one row on a one-member axis
first/last within a by= group	undecided — no declaration sizes a group

Decisions this encodes

• cases:, not branches:. It renders to \begin{cases}, and "branch" is a control-flow word for a language whose ceiling forbids control flow.
• when:, not where:. A case selects which value a coordinate takes — it creates no absence and deletes no row, which is what where means everywhere else (rule 6). Under this design an expression has no where at all, so a where: here would be the only one on the block and would read as extent.
• No where on expressions; cases are total over the frame. Two masked expressions would intersect in the constraint using them — absence spreads and takes the row — so the constraint's row set would stop being readable at the constraint. That is what diagnostics().omissions exists to catch: "rows lost to a mask the constraint never mentions." The price is visible in the tests: with nothing to narrow the frame, the cases have to say what an absent capacity or an unnamed label gets.
• Constraints get no cases:. Everything varying in the value factors into a named quantity; what cannot factor is the relation, and a differing relation is a differing rule that wants its own name and its own dual. piecewise.py already settles this by precedent — facing >= on the first breakpoint and <= on the last, it emits two named constraints.
• Macros are a follow-up. Cases there are safe only under a stronger obligation — provable with the names uninterpreted, since a macro has no frame until it is called — which is worth doing separately.

Soundness

The check rests on its cells covering every value a subject can take, so "no witness among the cells" means "no witness". TestSoundness walks a value grid finer than the cells — two points per band, both infinities, absence, labels no mask names — and asserts anything proved a partition survives it. Wider runs off-branch, with ordering comparators in both frames: 40,000 random case sets per frame, 202 and 167 proved partitions, 0 unsound; and 3,000 sets built to be partitions gave 2,187 proved, every one of the 813 refusals a dead case rather than a spurious overlap or gap.

Independence between subjects is an over-approximation, so a spurious world can only manufacture a witness, never hide one — every outcome is conservative in the safe direction.

Still open

The dim rule. A named expression has no foreach today — dims fall out of the body — but no single case's body gives the quantity's shape once cases exist, and one case's body may be a scalar while its when is not. foreach required alongside cases is the proposal; that is the wiring change, not this one.

Checks

Gates reproduced with a 3.13 venv on the versions pixi.toml pins plus prettier@3.9.3: ruff clean, pyrefly 0 errors, reuse lint compliant, 379 passed / 4 skipped.

[read-the-docs-community]

Documentation build overview

📚 math-spec | 🛠️ Build #34195476 | 📁 Comparing 0a622c5 against latest (526fdf8)

  🔍 Preview build  

41 files changed · + 4 added · ± 37 modified

+ Added

• examples/index.html
• examples/dispatch/index.html
• examples/operators/index.html
• reference/math_spec/partition/index.html

± Modified

• 404.html
• index.html
• CHANGELOG/index.html
• contributing/index.html
• installation/index.html
• about/ceiling/index.html
• about/what-counts-as-language/index.html
• reference/language/index.html
• reference/notation/index.html
• reference/typeset/index.html
• and 27 more...

[FBumann]

Superseded by #70, along with #36 — the PR this decision procedure existed for.

The difference. This module answers "do these cases partition the frame?" without data: pairwise disjointness, joint exhaustiveness and no dead case, all as one unsatisfiability question over cells of each where-atom's subject. It is careful work and the conservatism argument is right.

#70 makes the question not arise. The arms of a cases: block are ordered, first match wins, and the last one carries no when::

cases:
  always_on: { when: "not committable", expression: 1 }
  boundary:  { when: "position(snapshot) == 0", expression: status_initial }
  interior:  { expression: shift(status, over=snapshot, offset=1) }

Disjointness is then unrepresentable rather than proved — two arms cannot disagree at a coordinate, because only the first to match is read. Totality is structural — the fallback has no condition to fail. Both properties belong to the shape of the block, so nothing has to decide what a predicate could be true of, and there is no case set that loads and later turns out to have a hole in it.

The reason to close this rather than keep it for a stricter mode later is the coupling: every atom the where grammar gains would have to teach partition.py about its cells, or the procedure gets quietly more conservative — refusing case sets that are fine, with no test that would notice. That is a standing maintenance obligation on a language that is still growing, in exchange for diagnostics the ordered form does not need.

What is genuinely lost: a fully shadowed arm is now silently dead rather than a load error naming a witness. If that turns out to matter, it is a much smaller check than this one — and it can be written against the arms that are actually there, rather than against every world the atoms could describe.

The branch stays; nothing here is deleted, only unmerged.