[FBumann]

Prompt: Fix column-pair bug — ends[bus0] == ends[bus1] and ends[bus0] != ends[bus2] are proved apart, but they can overlap. Strict xfail first, then the fix, in a new PR.

Note

The following content was generated by AI.

What this changes

The case check now refuses ends[bus0] == ends[bus1] beside ends[bus0] != ends[bus2], because a line where bus0 equals bus1 but not bus2 is in both cases. Before, it proved them apart. This PR is stacked on #949.

Method, gate output, alternatives

Why

_subject_of keyed a RelationPairComparison by its two relation names and dropped the columns. So every comparison of two columns of ends read one shared fact, equal or different. The checker then read the two cases above as complements and proved them apart.

The change: the pair subject now carries both columns in Subject.group. The two sides are sorted, so ends[bus1] != ends[bus0] and ends[bus0] == ends[bus1] stay one subject. The witness now names the columns, for example ends[bus0] vs ends[bus1] is equal, not ends vs ends.

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

Tests

In tests/test_exclusivity.py:

• TestTwoPairsOfColumns::test_two_pairs_that_share_a_relation_both_claim_a_line: I watched it fail on the base branch (ValueError: not enough values to unpack, which means no refusal).
• test_one_pair_written_either_way_round_is_one_fact: two cases. They passed before the fix and guard the sort.
• The relation soundness fuzz now uses three columns and two more pair atoms. Its points carry one pair subject per column pair.
• test_a_row_both_cases_read_is_still_found now expects the new witness wording.

Guard table

I deleted each guard in turn and ran the full suite. I restored each one with git checkout -- and dropped __pycache__ on both sides. The tree came back clean.

Guard	Result
the pair subject carries its columns (replaced by ('?', '?'))	4 failed, including test_two_pairs_that_share_a_relation_both_claim_a_line
the two sides are sorted into one order	4 failed, including both cases of test_one_pair_written_either_way_round_is_one_fact

The fuzz fails under both mutations, but with a KeyError: it builds the subjects by hand, so they no longer match. It does not find a witness. The tests written for each guard are what catch them.

Gates

pixi run ci: lint, test (3077 passed, 1 skipped) and docs-build passed. compile-tex failed on all 54 documents because tectonic could not download its bundle in this container. This diff does not touch the typesetter.

Not done

• I did not make the pairs that share a column depend on each other. That would only make the checker more precise, not more correct.
• No doc change: the language reference already says what a comparison of two columns means.
• I wrote the reproduction as a failing test that I watched fail, not as a strict xfail. The fix lands in the same commit, so the marker would come off at once.

---

Generated by Claude Code

[read-the-docs-community]

Documentation build overview

📚 mathspec | 🛠️ Build #35351459 | 📁 Comparing 87d21fa against latest (97c44b4)

  🔍 Preview build  

1 file changed

± reference/changelog/index.html