feat(ClusterExpansion): prove the general pathGraph closed form and drop the six decide instances

[phasetr]

Motivation

IsingModel/ClusterExpansion/GraphCases.lean proves alternatingConnectedSubgraphSum (pathGraph k) = ±1 separately for k = 3..8, each by decide +kernel. That file is the most expensive in the repository to elaborate (~36.8s wall even after PR #4629 cut it from 63.7s). A general closed form removes the decide dependence entirely, generalizes the result to every n, and is estimated to bring the file down to ~4-6s.

Statement

alternatingConnectedSubgraphSum (pathGraph (n+1)) = (-1)^n for all n.

Proof sketch

A connected spanning subgraph on n+1 vertices needs at least n edges (SimpleGraph.Connected.card_vert_le_card_edgeSet_add_one), and pathGraph (n+1) has exactly n edges (card_pathGraph_edgeFinset), so squeezing with Finset.eq_of_subset_of_card_le forces the subset to be the whole edge set; the converse direction is SimpleGraph.pathGraph_connected. Hence connectedSpanningEdgeSubsets (pathGraph (n+1)) = {edgeFinset} and the alternating sum collapses to a single term via Finset.sum_singleton. No acyclicity or bridge argument is needed — this is strictly simpler than the existing cycleGraph counterpart it is modelled on (CycleGraphAlternatingSum.lean:134,197).

Plan

Add IsingModel/ClusterExpansion/PathGraphAlternatingSum.lean (sibling of CycleGraphAlternatingSum.lean) with one private characterisation lemma and one public closed form; then replace the six decide proofs in GraphCases.lean with instantiations of it, verify the #check @ dumps are unchanged, and remove the now-unnecessary private DecidableRel (pathGraph k).Adj instances and the set_option maxHeartbeats 400000.

Note that the six instances are then reference-0 duplicates of the general form; whether to delete them outright (updating the docs/index.md and tex/proof-guide.tex mentions to cite the general theorem instead) is decided in this PR.

Review follow-up (commit d76f85d4)

Two review findings addressed:

1. (Med) Umbrella root closure regression. Deleting GraphCases.lean removed the only path by which PathGraphAlternatingSum and CycleGraphAlternatingSum reached the IsingModel root import closure (previously GraphCases ← TanhBounds), leaving both modules orphaned: still built by the lakefile glob, but invisible to scripts/audit_gate.py V3, which runs #print axioms from a temporary file that only does import IsingModel. Both modules are now imported from IsingModel.lean (next to AlternatingFinThree), restoring auditability. Demonstrated: from a file whose sole import is IsingModel, both alternatingConnectedSubgraphSum_pathGraph and alternatingConnectedSubgraphSum_cycleGraph resolve and report [propext, Classical.choice, Quot.sound].
2. (Low) Ambiguous doc comment. The value table in the doc comment of alternatingConnectedSubgraphSum_pathGraph wrote n = 2 ↦ 1 where n could be read as either the exponent or the vertex count; entries are now spelled n = 2 ↦ pathGraph 3 = 1, etc.

lake exe shake does not flag either new umbrella import as redundant. (It does report a pre-existing import-narrowing suggestion inside CycleGraphAlternatingSum.lean itself — AlternatingCompleteGraph → AlternatingCompleteGraph.SignedSums — which predates this PR and is left alone.)

Out of scope for this PR, recorded for follow-up: three modules are orphaned from the root closure on main as well, i.e. not caused by this PR — ClusterExpansion.MayerCore.MayerTermThreeEval, PseudoMass.Composition, PseudoMass.FromParamsBounds.JZeroComparisons (0 importers on both main and this branch).

Verification checklist

• The new module builds warning-free as part of the full build (this repo has autoImplicit on, so a missing import silently becomes an auto-bound implicit)
• [~] #check @ dumps for the six instances identical before/after the proof replacement — superseded: the six per-n instances were deleted outright (commit 7274a9f5) rather than reproved, so there is no before/after dump to compare; rg confirms no remaining reference to any of the six names in IsingModel/, docs/index.md or tex/proof-guide.tex
• lake build warning-free (5063 jobs, zero warning lines)
• #print axioms = [propext, Classical.choice, Quot.sound] with no decide-specific assumptions — verified through import IsingModel, so V3 can see it
• scripts/audit_gate.py --full V1-V4 all PASS (13 capstones)
• lake exe GKSTest
• No circular imports
• [~] Measured elaboration time for GraphCases.lean reported before/after — moot: GraphCases.lean is deleted, so its full ~36.8s elaboration cost is removed rather than reduced
• docs/tex updated to cite the general theorem (docs/index.md cites alternatingConnectedSubgraphSum_pathGraph; zero stale references to the six deleted per-n lemma names in docs/index.md / tex/proof-guide.tex)
• CI green (run 29790889993, "build" check, 2m35s — https://github.com/phasetr/ising-model/actions/runs/29790889993/job/88512247083)

Part of #4637

🤖 Generated with Claude Code

[phasetr]

dev-issue-manager: pre-merge resolution verification (HEAD d76f85d)

Verdict: PASS. Merge-ready.

Independent re-verification (not relying on prior gate reports)

• lake build: 5063 jobs, Build completed successfully, zero warning lines (only two unrelated pre-existing ring_nf info suggestions in Phi4AllOdd.lean / TwoSiteInteractingLayerOpenBoundaryWindow.lean, not touched by this PR).
• #print axioms re-run from a fresh scratch file whose sole import is import IsingModel (mirrors audit_gate.py V3's method exactly):
  • alternatingConnectedSubgraphSum_pathGraph → [propext, Classical.choice, Quot.sound]
  • alternatingConnectedSubgraphSum_cycleGraph → [propext, Classical.choice, Quot.sound]
    This confirms the umbrella-closure fix (commit d76f85d4) actually restores V3 auditability of both modules, not just that the code builds.
• python3 scripts/audit_gate.py --full: V1 PASS, V2 PASS, V3 PASS (13 capstones, axiom union = {Classical.choice, Quot.sound, propext}), V4 PASS.
• lake exe GKSTest: === All tests passed ===.
• CI (gh pr checks 4638): build check pass (run 29790889993, 2m35s).

Mathematical-content preservation (no information loss from the GraphCases.lean deletion)

• IsingModel/ClusterExpansion/GraphCases.lean confirmed removed; PathGraphAlternatingSum.lean confirmed present with alternatingConnectedSubgraphSum_pathGraph (n : ℕ) : alternatingConnectedSubgraphSum (pathGraph (n+1)) = (-1)^n, doc comment spells out all 6 former per-n values (n=2..7 ↦ pathGraph 3..8).
• docs/index.md cites the general theorem by name (alternatingConnectedSubgraphSum_pathGraph, ClusterExpansion/PathGraphAlternatingSum.lean) and explicitly records what it replaces (the former pathGraph_{three,...,eight} decide+kernel cases), including the build-time improvement (38s → 2s for the module).
• grep/rg across docs/index.md, tex/proof-guide.tex, IsingModel/: zero remaining references to GraphCases, pathGraph_{three,four,five,six,seven,eight}, or cycleGraph_{three,...,seven} per-n names. No stale citations, no silent loss of the specific values (all 6 recoverable from the general theorem plus doc comment).

PR body checklist

Reviewed dev-implement's [~] (superseded/moot) judgments on the #check @ dump comparison and elaboration-time comparison — both correctly reflect that the comparison targets (GraphCases.lean, the six per-n decls) no longer exist post-deletion, so marking them [x] would have been false. Updated the final [ ] CI green to [x] now that CI is confirmed green (run 29790889993).

Full ledger

See .self-local/issues/4637.md for the updated tracking-issue mirror and follow-up disposition (orphan-module registration, PR-3 scope reduction to 12/22 Profile.lean declarations, CycleSeven.lean rename).