refactor(Logic): Consistent provability_TFAE clause order across LogicA/LogicD/LogicS - #33
Merged
Conversation
Reorder each of LogicA/LogicD/LogicS.provability_TFAE consistently as membership → sequent calculus → semantics → relation to other logics, and renumber the corresponding tfae_have steps and downstream `.out` references (within these files and in NotCIP.lean/D_S.lean) to match. Co-Authored-By: Claude <noreply@anthropic.com>
Introduce iff_forces_pseudoTail_root as the general-κ analogue of iff_forces_pseudoTail_root_concrete, and use it in place of the raw provability_TFAE.out 0 2 / out 2 0 index lookups in Basic.lean and NotCIP.lean, per the style guide's ban on referring to TFAE clauses by index outside the defining proof. Co-Authored-By: Claude <noreply@anthropic.com>
Replace raw provability_TFAE.out i j index access with named theorems iff_eventually_forces_tail_nat and iff_forces_root_subfmlsS_imp, mirroring the existing LogicS wrapper style, and update the two external call sites in D/NotCIP.lean and Classification/D_S.lean accordingly. Co-Authored-By: Claude <noreply@anthropic.com>
LogicGL.provableHilbert_of_provableGentzen composed the raw clause indices provability_TFAE.out 2 1 instead of the named corollaries iff_provableGentzen/iff_provableHilbert, and LogicGrz.provable_boxdot_GL_of_provable_Grz in Boxdot.lean referenced LogicGrz.provability_TFAE.out 0 1 directly instead of LogicGrz.iff_provableHilbert. Per the style guide's ban on indexing TFAE clauses outside the defining proof, rewrite both in terms of the named wrapper lemmas. Co-Authored-By: Claude <noreply@anthropic.com>
Several lemmas in A/Basic.lean, D/Basic.lean, S/Basic.lean, and
Boxdot.lean carried docstrings that added nothing beyond a prose
paraphrase of their own type, including two in S/Basic.lean labelled
by the pre-reorder `provability_TFAE` clause numbers ("Direction `6 ->
2`", "Direction `2 -> 3`") that the clause reordering left stale.
Delete these; keep docstrings that add information not visible from
the statement (citations, provenance notes, witness identification,
cross-references to a related lemma). Also replace one remaining
"item 4 of `provability_TFAE`" comment in NotCIP.lean with a direct
reference to the named lemma it actually uses.
Co-Authored-By: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
LogicA.provability_TFAE,LogicD.provability_TFAE,LogicS.provability_TFAEconsistently as: membership in the logic → sequent calculus → semantics → relation to other logics.tfae_havesteps and downstream.outreferences (within these files and inNotCIP.lean/D_S.lean) to match the new clause order.Test plan
lake buildsucceeds for the whole project, no new errors/warnings/sorriesjust mk-allreports no update necessary🤖 Generated with Claude Code