fix(Archive): build the whole ModalLogicArchive under Lean 4.33.1

[jsboige]

Grain: DEEP/lean — lane myia-po-2025:CoursIA — prev: MED/notebook-dotnet jsboige/CoursIA#17513

Summary

ModalLogicArchive did not build under Lean 4.33.1. Modal.Tableau failed with six errors, and every Modal/Kripke/Logic/* module depends on it, so the frame classes, the per-system soundness/completeness instances and the ⪱ instances between systems could not be used from a consumer. Nothing flagged it: the archive is outside defaultTargets (Fin74, Neighborhood), and CI (lake build) never builds it.

This PR makes the whole archive build: lake build ModalLogicArchive (247 modules, 1302 jobs) succeeds. Tracked in jsboige/CoursIA#17522.

Root cause

Most failures share one cause. Several defs start with implicit binders, for instance Tableau.Consistent 𝓢 t := ∀ {Γ Δ}, .... When a hypothesis of such a type is elaborated without an expected type (if_pos h, simpa using h), Lean 4.33 instantiates the implicits. split / split_ifs then fail on an if whose condition is such a def.

Fixes: pass @h, and replace split by explicit equation lemmas.

• Propositional.ConsistentTableau: lindenbaum_next_of_consistent, lindenbaum_next_of_not_consistent, lindenbaum_next_cases.
• Modal.Tableau: the matching lemmas.

The rewritten proofs (next_parametericConsistent, mem_lindenbaum_next_indexed, lindenbaum_next_indexed_subset₁/₂_of_lt, ...) keep their statements.

Other 4.33 / mathlib changes

Step that fails under 4.33	Replacement	Where
simp_all / simp / calc … by simp on pair or subtype equalities	Prod.ext, Subtype.ext	Modal.Tableau, ConsistentTableau (equality_def, equality_of₁), Tree
simp at h to discharge a hypothesis h : ¬ a = a	exact h rfl / exact absurd rfl h	Tree, Logic/GLPoint3
simp on goals over Fin 1 / Fin ↑1	Fin.eq_zero (+ subst), omega	Rank, ExtendRoot
dsimp [f, h] to rewrite an if with a Prop hypothesis h	rw [f, if_pos h]	FMT/Completeness
simp on Rel.Iterate R 1	Rel.Iterate.iff_succ	Rank
simp lemmas on t.1.1 (not_mem₁_falsum, iff_mem₁_and, iff_mem₁_or, canonicalFrame.rel₁) on worlds of the canonical model	the same lemmas applied explicitly, (t := t), and Tableau.subset_def	Propositional/Kripke/Completeness, AxiomWLEM
simp/grind on Finset preimage membership, rintro pattern sized for the old simp normal form	explicit Finset.mem_preimage, Finset.mem_union_*, Finset.mem_filter	Logic/Grz/Completeness, Propositional/Kripke/AxiomKreiselPutnam
simpa using hy on a conjunction	simpa using hy.1	AxiomMcK
reference to an auto-generated instance name, which follows mathlib's set-builder spelling (setOf became ofPred)	name the instance sound_finite_GrzPoint3' and reference it	Logic/GrzPoint3, ModalCompanion/Standard/LC

14 files changed: +160 / −83, all under ModalLogicArchive/. Fin74 and Neighborhood do not import the archive (0 occurrences), so they are unaffected.

Verification

Measured in a consumer at Lean 4.33.1, mathlib 0df444a360, Foundation 81810b9f22, with this branch checked out as the ModalLogic package:

$ lake build ModalLogicArchive
Build completed successfully (1302 jobs).

The aggregate ModalLogicArchive.lean imports all 247 modules of the archive, so this covers every file, Modal.Kripke.Logic.S5 included.

No proof removed, no sorry added. The diff adds no sorry. A collectAxioms scan over every declaration of 21 modules reports sorryAx in exactly three:

• LC.boxdotModalCompanion_LC;
• GrzPoint3's Complete … finite_GrzPoint3;
• GrzPoint2 ⪱ GrzPoint3.

All three rest on the literal sorry at Logic/GrzPoint3.lean:58, which predates this PR. The 21 modules are the repaired ones, plus S4/S5/KT/KTB/KD45/K4 and Kripke.Completeness. Scan results:

• Modal.Tableau: 113 declarations, 0 sorryAx;
• Kripke.Logic.S5: 45 declarations, 0 sorryAx;
• Propositional.ConsistentTableau: 83 declarations, 0 sorryAx.

The eight sorry warnings of the full build are the ones the archive already carried: NNFormula ×2, AxiomMk, Balloon, GrzPoint3, S4H, Makinson, Modality/Basic.

Not measured: the branch's own lean-toolchain (v4.31.0). The fixes target the 4.33.1 configuration that the consumer pins.

CI: the archive is still unguarded (item 2 of CoursIA#17522)

This PR does not add a CI step, and that is deliberate. ci.yml triggers only on push / pull_request / merge_group to main. It builds with the branch's lean-toolchain, v4.31.0. So:

• no workflow runs on this PR, or on anything based on coursia-v4.33.1-compat;
• an archive step added to this branch's lake build would test Lean v4.31.0, not the 4.33.1 configuration that broke.

A guard that matches the consumer needs one of two things:

• align this branch's lean-toolchain and manifest with the consumer (4.33.1 / mathlib 0df444a360), then trigger CI on this branch;
• or add a job that overrides the toolchain and mathlib rev before lake build ModalLogicArchive.Modal.Kripke.Logic.S5.

That choice belongs to the fork maintainer. It stays open in CoursIA#17522.

🤖 Generated with Claude Code