Add the distributive laws and negating a conditional to Proof Writing by d-morrison · Pull Request #599 · Morrison-Lab/mds

d-morrison · 2026-11-03T16:50:30Z

Important

Merge after #596. Both PRs add includes right after De Morgan's laws in _proof-writing.qmd, so whichever merges second needs a one-hunk conflict fix there.

Adds four results from mcs (CSCI 201) after De Morgan's laws, each with an example:

the distributive laws (thm-distributive);
replacing a part by an equivalent part (thm-substitution-logic), now stated exactly;
negating a conditional (thm-negate-conditional);
the conditional as an or (cor-conditional-as-or).

These were in #596 until its review asked for an example after each result, which took that PR past the size cap.

Part of #453 and of the mds/mcs consolidation plan (https://claude.ai/artifact/De8D2LiAwjX3fpLezVDdS7).
Only definitions, theorems and proofs move; mcs keeps its own examples and exercises, and the examples here are new.
Each block keeps its mcs id, so mcs can switch to the include without breaking a link.

Checked locally against gha main: check-term-links (0 errors), check-avoided-words and check-new-line-breaks are clean.

Generated by Claude Code

mcs (CSCI 201) defines these general results locally. Moving them here, one block per subfile, lets mcs include them instead of keeping its own copies, per the mds/mcs consolidation plan. Each block keeps its mcs id. They were in #596 until its review asked for an example after each result, which took that PR past the size cap. Each result here now has an example. The substitution theorem now states its claim exactly: a proposition F built from A with connectives, and F' with A replaced by B. Long "when" clauses in the negated-conditional proof are split onto their own lines. Part of #453. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019xfc9pMBq15Hq3DgNBx1ox

d-morrison · 2026-11-03T16:59:20Z

Addressing the blocking finding: #thm-double-negation is added by #596 (_thm-double-negation.qmd, included right after De Morgan, ahead of every include this PR adds). The two PRs were split for the size cap and share that insertion point, which is why the body says to merge #596 first. Once it merges I will merge main into this branch, so the link resolves with no forward reference, and fold in the unused-$P$/$Q$ suggestion on _exm-negate-conditional.qmd in the same push.

Posted by Claude Code (AI agent) --- not written by a human.

Generated by Claude Code

Resolve the _proof-writing.qmd conflict by keeping #596's blocks first, so thm-double-negation precedes its first use here. Also name P and Q in the negate-conditional example, as the review suggested. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019xfc9pMBq15Hq3DgNBx1ox

Review suggestion on #599: one line for F and one for A and B. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019xfc9pMBq15Hq3DgNBx1ox

d-morrison · 2026-11-03T17:48:09Z

Re the round-2 review:

Blocking, _thm-substitution-logic.qmd:21 — rebutted. The line already breaks after "every row,": line 21 is $A$ and $B$ have the same truth value in every row, and line 22 starts so each step of the computation .... The quoted text spans two lines. Local check-new-line-breaks (gha main, *.qmd) reports no lines missing semantic breaks.
Suggestion, _exm-substitution-logic.qmd:7 — done in the next push: "with $A = ... and $B = Q$." now has its own line.

Posted by Claude Code (AI agent) --- not written by a human.

Generated by Claude Code

#4922) * check-pr-fully-clean: skip agent-disclosed replies in the verdict scan An agent replying to a review under the maintainer's login often quotes the reviewer's "Blocking" label. The verdict scan admitted every non-bot not-clean comment, so the quote became a standing maintainer veto that no later clean review could clear, and the only way out was editing the agent's own comment (measured on Morrison-Lab/mds#599, where two clean Claude reviews of the head could not pass the gate). Skip a comment only on positive evidence that it is a reply: it ends with the Claude Code disclosure footer, carries no review shape the scan admits from a human login (report structure, a named review head) and no review-data payload, and once each disposition label is removed (a bold finding label followed at once by rebutted, deferred, done, ..., or "Addressing the blocking finding") the rest of the body no longer reads as not-clean. The rest is classified as a whole, so a relayed "Needs more work", a second finding after a disposition, or a verdict spread over several lines still blocks. What may follow a disposition is an allowlist, so the skip fails closed: nothing, punctuation or a commit reference after any disposition, or, after rebutted, declined or deferred only, an explanation holding no negation, contrast, modal, open-work word, number or file path. Anything else keeps the whole line, label included. The residual risk is an explanation that states an open defect in none of those words, which is then dropped; that is accepted as the price of not editing the agent's own comments, and is stated here so a reviewer can refuse it. Closes #4826. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019xfc9pMBq15Hq3DgNBx1ox * check-pr-fully-clean: allowlist the rebuttal shape after rebutted/declined/deferred An explanation after a weighed disposition now drops its line only when it reads as a rebuttal of the reviewer's reading ("The line already breaks ...", "The reviewer misread ...") and holds no risky word, so "Persists on the head." and "Agree with the reviewer." keep blocking. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019xfc9pMBq15Hq3DgNBx1ox * check-pr-fully-clean: close the rebuttal phrases Each rebuttal opener is now a closed phrase followed by at most six plain words, and confirmations (valid, true, confirmed, persists, ...) are risky words, so "The finding is already valid." keeps blocking. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019xfc9pMBq15Hq3DgNBx1ox * check-pr-fully-clean: allow only a place after a rebuttal phrase Six free words after a closed phrase still admitted "The check handles nothing."; only an optional "after/before/at the X" may follow now. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019xfc9pMBq15Hq3DgNBx1ox * check-pr-fully-clean: spell the em dash as an escape in the label regex Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019xfc9pMBq15Hq3DgNBx1ox --------- Co-authored-by: Claude <noreply@anthropic.com>

github-actions · 2026-11-03T23:17:57Z

Claude finished review — View run

I fetched PR 599 live just now. It is open, not a draft and not merged, and its head is 8b4186b1085f6634b0e3ad3438ec33e76c3f802a. That is the commit I reviewed, so the verdict stands.

Verdict

Ready for merge.

Structured Review Data (JSON)

{
  "schema_version": "1.1",
  "reviewer": "claude",
  "commit_sha": "8b4186b1085f6634b0e3ad3438ec33e76c3f802a",
  "verdict": "CLEAN",
  "findings": [],
  "detailed_assessment": "The merge 8b4186b of main, which brings in #610, matches git's automatic merge, so the proof-writing subfiles and inst/WORDLIST gain no new conflict or defect.",
  "holistic_assessment": "The range holds no commit of this PR's own, the content from #610 is already on main, and the prior Ready for merge verdict at comment 6617580399 still stands."
}

Reviewed commit: 8b4186b

github-actions · 2026-11-03T23:17:58Z

💰 Cost: $0.1864 (review) — run

github-actions · 2026-11-04T00:00:03Z

PR Preview Action v1.8.1
🚀 Preview available at: https://Morrison-Lab.github.io/mds/pr-preview/pr-599/

_{Built to branch gh-pages at 2026-11-03 23:59 UTC.}

dem-extra1 · 2026-11-04T00:21:08Z

Holding this PR: the proof-writing content it adds belongs in mcs under the consolidation plan (Morrison-Lab/mcs#60, phase 1). I'll land the same content in mcs instead, then close this PR.

Posted by Claude Code (AI agent) --- not written by a human.

Generated by Claude Code