[FBumann]

Prompt: I found two things in the case checker (_exclusivity.py) that the PR describes but does not fix: a missed overlap (NOT ends[bus0] == ends[bus1] and NOT ends[bus0] != ends[bus1] both claim a line with no row) and an over-refusal (end_of != 'x' and NOT end_of cannot overlap). Lets fix that. ANd test it

Note

The following content was generated by AI.

The case check now follows #947's rule: a comparison on a relation is false where the relation has no row. It also tells two pairs of columns of one relation apart. Two missed overlaps are now refused, and one false refusal is gone.

Cases	main	This PR
NOT ends[bus0] == ends[bus1] / NOT ends[bus0] != ends[bus1]	proved apart (wrong: both claim a line with no row)	refused
ends[bus0] == ends[bus1] / ends[bus0] != ends[bus2]	proved apart (wrong: both claim bus0 == bus1 != bus2)	refused
ends[bus0] != 'north' / NOT ends	refused (needlessly)	proved apart

Review commit by commit: b4748c53 is the missing row, and the squashed #951 commit is the column pairs.

Method, guard tables, gate output

The change

All in src/mathspec/_exclusivity.py.

A missing row (b4748c53). Subject('relation', name) with no column is now whether the relation has a row, with the cells [True, NULL]. Each relation that a comparison reads gets this subject. A comparison is false in a cell where a relation it reads has no row. A relation column no longer carries its own null or infinity cells, the same as a dimension. The witness leaves out the columns of a missing row, and leaves out "has a row" where a column value of that relation already shows it.

Before, a RelationPairComparison had the cells [True, False] and no cell for a missing row. RelationDefined and RelationComparison were independent subjects, so the checker invented a cell where ends has no row and ends[bus0] still holds a value.

Two pairs of columns (#951). The pair subject was keyed by the two relation names only, so every comparison of two columns of ends read one fact. It now carries both columns in Subject.group. The two sides are sorted, so ends[bus1] != ends[bus0] is the same subject as ends[bus0] == ends[bus1]. The witness names the columns: ends[bus0] vs ends[bus1] is equal, not ends vs ends.

Pairs that share a column, such as bus0 == bus1, bus1 == bus2 and bus0 != bus2, stay independent subjects. That over-approximates: it can produce a witness no data has, but never hides a real one.

Tests

tests/test_exclusivity.py:

• TestARelationWithNoRow: the negated complements are refused with ends has no row as the witness; three pairs (a label, two columns, a number) against NOT of the bare name are proved apart; a row both cases read is still found.
• TestTwoPairsOfColumns: the two pairs above are refused; one pair written either way round, plain or negated, is one fact.
• TestSoundness::test_a_relation_proved_apart_stays_apart_on_every_row: the existing fuzz, run over ends with three columns. It checks every pair the checker proves apart on concrete points: no row, or a row whose columns hold three labels each.

I watched each new reproduction fail on its base before writing the fix.

Guard tables

I deleted each guard in turn and ran the full suite, restoring with git checkout -- and dropping __pycache__ on both sides. The tree came back clean each time.

Guard deleted	Result
row check before an atom is read	5 failed
a relation column carries no null cell	1 failed
witness leaves out the columns of a missing row	2 failed
witness names the row once, not beside a column	3 failed
witness says has a row	1 failed
each relation a comparison reads gets a row subject	7 failed
a row subject's cells are a row and no row	4 failed
the pair subject carries its columns	4 failed
the two sides of a pair are sorted into one order	4 failed

Gates

pixi run ci before each push: lint, test and docs-build passed. compile-tex failed on all 54 documents because tectonic could not download its bundle in that container; the diff does not touch the typesetter. GitHub CI is green on both parts.

Not done

• No doc change: docs(language): a comparison on a relation is false where the relation has no row, whatever its operator #947 already states the rule this PR makes the checker follow. No limit moved.
• fix(language): the case check reads each pair of relation columns as its own fact #950 was a duplicate of fix(language): the case check tells two pairs of columns of one relation apart #951, opened by a second session; it is closed.

🤖 Generated with Claude Code

https://claude.ai/code/session_015MPR9MKVJ9XwN68qHLrX5g

[read-the-docs-community]

Documentation build overview

📚 mathspec | 🛠️ Build #35353643 | 📁 Comparing 1fe5f0e against latest (97c44b4)

  🔍 Preview build  

1 file changed

± reference/changelog/index.html