[jsboige]

Fix Modal.Tableau under Lean 4.33.1 — split/calc breakage over ite/match under projections

Grain: DEEP/lean — lane myia-po-2024:CoursIA-2 — prev: LIGHT/epic-body #19002-adjacent

Why

At pin 71968137, ModalLogicArchive.Modal.Tableau does not compile when the
consumer builds it with Lean v4.33.1 (CoursIA formal_logic_lean, see
jsboige/CoursIA#17522). All of ModalLogicArchive.Modal.Kripke.Logic.*
depends on it, so the completeness layer is unusable from the consumer.

Measured errors under 4.33.1 (consumer manifest, toolchain v4.33.1):

Tableau.lean:47:2:  unsolved goals   (equality_def mpr: simp_all leaves a pair-equality)
Tableau.lean:229:2: Tactic `split` failed (ite under Tableau.Consistent projection)
Tableau.lean:245:2: Tactic `split` failed (ite under .1/.2 after simp only)
Tableau.lean:260:6: Tactic `split` failed (match decode under .1)
Tableau.lean:269:6: Tactic `split` failed (match decode under .2)
Tableau.lean:383:4: invalid 'calc' step, failed to synthesize `Trans` (anonymous-constructor calc)

Mechanism: under 4.33, whnf no longer unfolds Tableau.Consistent / Prod
projections to expose the ite/match, so split cannot find a splittable
expression; simp-driven closing leaves Prod.ext residues; the
anonymous-constructor calc no longer elaborates (branch types only meet at
the expected type).

What

• equality_def (47): close the residual pair-equality after simp_all with
  rfl / Prod.ext rfl rfl (tolerant first chain).
• consistent_lindenbaum_next (229): by_cases + unfold lindenbaum_next +
  hypothesis-driven ite resolution (simp [hc]), then closers tolerant to both
  goal shapes (exact h or intro hΓ hΔ; exact h hΓ hΔ).
• disjoint_of_consistent (was misattributed as site 47): simpa [Disjoint]
  left a metavariable residue under 4.33; replaced by an explicit
  simp [Disjoint] at hC + obtain, with the original simpa kept as a
  fallback branch so the fork's own toolchain (v4.31.0) keeps working.
• either_mem_lindenbaum_indexed (245): by_cases + simp [.., hc].
• subset₁/subset₂_lindenbaum_indexed_of_lt (260/269): rename_i n,
  rcases hdec : (decode n : Option (Formula α)), then by_cases +
  simp [.., hdec, hc] + Set.subset_insert transitivity.
• equality_of₁ (383): anonymous-constructor calc replaced by
  Subtype.ext $ Tableau.equality_def.mpr ⟨e₁, maximal_duality.mp e₁⟩.

CI: lake build only builds defaultTargets (Fin74, Neighborhood) — the
archive is never compiled. Added an explicit CI step
lake build ModalLogicArchive.Modal.Kripke.Logic.S5 (prescription 2 of
jsboige/CoursIA#17522) so the completeness layer cannot break silently again.

Evidence

• lake build ModalLogicArchive.Modal.Tableau — SUCCESS under
  leanprover/lean4:v4.33.1 with the consumer's dependency pins
  (mathlib rev 0df444a360eaa60ab8c11dca51a86af692955474, Foundation
  81810b9f, batteries 4488d40d), run in WSL on the branch.
• sorry count in Tableau.lean: 0 before and after
  (grep -cE 'sorry' → 0; no proof replaced by stub — all six sites keep
  their original statements, only tactic bodies changed).
• No lake-manifest.json / lean-toolchain change in this PR: the fork stays
  at v4.31.0 with its own pins; the fix is source-level and version-tolerant
  (each closer accepts both the 4.31-folded and 4.33-unfolded goal shapes via
  first | ... | ... fallbacks).

Closes jsboige/CoursIA#17522 steps 1–2 (step 3, the consumer pin bump,
follows in CoursIA once this merges).

See jsboige/CoursIA#15066 (downstream consumer: ModalZoo completeness layer)

🤖 Generated with Claude Code