siddhartha-gadgil/leanaide/compactness-gluing

Skill: Compactness and Local-to-Global Gluing

Pre-condition: Apply this skill when a global statement is expected to follow from local data, open covers, finite subcovers, compatible patches, or finite fragments.

Goal: Prove local statements and assemble them into a global conclusion using compactness, finite extraction, or gluing compatibility.

Instructions:

1. Localize the Goal: Choose a cover, neighborhoods, charts, affine opens, finite fragments, or local pieces.
2. Prove the Local Result: Establish the desired property on each piece.
3. Finite Extraction: If compactness is present, pass from an arbitrary cover or infinite family to finitely many pieces.
4. Compatibility on Overlaps: Check equality, transition, cocycle, or consistency conditions where pieces meet.
5. Glue: Construct the global object or global proof and verify it restricts to the local data.

Common Failure Modes:

• Proving local statements but omitting compatibility on overlaps.
• Using compactness without the correct open-cover, closed-set, or finite-fragment formulation.
• Forgetting uniqueness in gluing arguments.