[FBumann]

Prompt: In energy-models/mathspec, src/mathspec/_exclusivity.py builds the subject of a RelationPairComparison as Subject('relation_pair', name, other). The subject keys on the two relation names only and drops column and other_column. So two different column pairs of one relation share one subject, and the checker reads them as one equal/different fact. That is unsound: it proves apart two cases that can both claim a coordinate.

Reproduction (confirmed on main at 97c44b4, and after PR #949):

model = {
    'dimensions': {'line': {}, 'bus': {}},
    'relations': {'ends': {'key': 'line', 'values': {'bus0': 'bus', 'bus1': 'bus', 'bus2': 'bus'}}},
    'variables': {'flow': {'dims': ['line']}},
    'constraints': {'c': {'dims': ['line'], 'expression': 'flow >= 0'}},
}
# with tests/test_exclusivity.py's `refusals` helper:
refusals(to_spec(model), {'a': 'ends[bus0] == ends[bus1]', 'b': 'ends[bus0] != ends[bus2]'})  # returns [], should refuse

A line with bus0 == bus1 != bus2 is in both cases.

To do, following AGENTS.md:

1. Write the failing test first in tests/test_exclusivity.py. Watch it fail, and put what was wrong in its docstring.
2. Key the subject by the columns too. One way is to put both column names in Subject.group or in the qualifier, normalized so that ends[bus0] == ends[bus1] and ends[bus1] == ends[bus0] stay one subject. Update Subject.__str__ so the witness names the columns, such as ends[bus0] vs ends[bus1], rather than ends vs ends. Keep _columns_of (added in fix(language): the case check reads a comparison on a relation as false where the relation has no row #949) working: it reads the pair subject's two relation names to hide the clause where a relation has no row.
3. Check the existing tests in tests/test_exclusivity.py and tests/test_validation.py that assert witness text.
4. Run pixi run lint, then pixi run ci. Open a fix(language): PR and add its title under ## Upcoming version in CHANGELOG.md.

Note: pair subjects that share a column, such as b0==b1, b1==b2 and b0!=b2, stay independent. That over-approximates and is safe, so it is out of scope.

Note

The following content was generated by AI.

The case check now reads each pair of relation columns as its own fact. ends[bus0] == ends[bus1] and ends[bus0] != ends[bus2] are refused, and the witness names the columns. Stacked on #949.

Method, gate output, alternatives

The change

_subject_of builds the pair subject as Subject('relation_pair', name, other, (column, other_column)). The two (relation, column) sides are sorted first, so ends[bus0] == ends[bus1] and ends[bus1] != ends[bus0] stay one subject. Subject.__str__ prints ends[bus0] vs ends[bus1]. name and qualifier still hold the two relation names, so _columns_of from #949 reads them as before.

Tests

tests/test_exclusivity.py:

• TestAPairOfColumns::test_two_pairs_of_columns_are_two_facts: the reproduction from the prompt. It failed on the fix(language): the case check reads a comparison on a relation as false where the relation has no row #949 head (ValueError: not enough values to unpack (expected 1, got 0), no refusal). It now asserts the witness where ends[bus0] vs ends[bus1] is equal, ends[bus0] vs ends[bus2] is different.
• TestAPairOfColumns::test_one_pair_written_both_ways_is_one_fact: one pair with its sides swapped is proved apart. It passes on the broken tree too, because there every pair was one subject. It guards the sort.
• Updated: the witness text in test_a_row_both_cases_read_is_still_found[a-column-value-says-the-row-exists] (ends vs ends became ends[bus0] vs ends[bus1]), and the pair subject that the relation fuzz builds by hand. tests/test_validation.py asserts no pair witness text, and no docs page prints one.

Guard table

I deleted each guard, ran pixi run pytest tests/, and restored the file.

Guard deleted	Result
sort the two sides before the subject is built	1 failed (test_one_pair_written_both_ways_is_one_fact)
the columns in the subject key (replaced by ('', ''))	4 failed (both relation fuzz seeds, the witness-text case, test_two_pairs_of_columns_are_two_facts)

Gates

pixi run lint passed. pixi run ci: lint passed, test passed (3076 passed, 1 skipped), docs-build passed. compile-tex failed because tectonic could not download its bundle from this container (relay.fullyjustified.net), the same as on #949. This diff does not touch the typesetter. CI will run it.

Base branch

This PR targets the #949 branch (claude/modest-fermat-dif3dq), not main, because the fix must keep _columns_of from #949 working. AGENTS.md says to branch from origin/main. I departed from that because this PR depends on #949. When #949 merges, retarget this PR to main.

Not done

• Pair subjects that share a column (b0 == b1, b1 == b2, b0 != b2) stay independent. That over-approximates and is safe. Out of scope, as the prompt says.
• The relation fuzz in TestSoundness still walks a two-column ends. A third column there would have caught this defect. I did not widen it.
• No doc change. No limit moved.

---

Generated by Claude Code

[read-the-docs-community]

Documentation build overview

📚 mathspec | 🛠️ Build #35350003 | 📁 Comparing a326340 against latest (97c44b4)

  🔍 Preview build  

1 file changed

± reference/changelog/index.html

[FBumann]

Prompt: I dont want to merge any yet, bu make them better reviewable — We can merge, but not into main!

Note

The following content was generated by AI.

This PR duplicates #951, which a second session opened for the same bug. #951 is now merged into #949's branch, so #949 carries the fix. The source changes are the same in both. #951 also widens the relation fuzz to three columns and adds a negated swap case. I am closing this PR; its branch stays.

---

Generated by Claude Code