Local-Global Atlas Exactness

Abstract

Canonical local-global exactness is separation plus gluing, independently.

Theorem 1.1 (Atlas exactness splits into independent separation and gluing clauses).

$$\left(\forall X\in Type,A\in \mathrm{RefinementSystem}\left(X\right),\mathrm{Bijective}\left(\mathrm{stateThread}\left(A\right)\right)\iff \left(\ker \left(\mathrm{stateThread}\left(A\right)\right)=\mathrm{diagonal}\left(X\right)\wedge \mathrm{range}\left(\mathrm{stateThread}\left(A\right)\right)=\mathrm{univ}\left(\mathrm{InverseThread}\left(A\right)\right)\right)\right)\wedge \left(\left(\exists A\in \mathrm{RefinementSystem}\left(Bool\right),\ker \left(\mathrm{stateThread}\left(A\right)\right)=\mathrm{diagonal}\left(Bool\right)\wedge \mathrm{range}\left(\mathrm{stateThread}\left(A\right)\right)\ne \mathrm{univ}\left(\mathrm{InverseThread}\left(A\right)\right)\right)\wedge \left(\exists A\in \mathrm{RefinementSystem}\left(Bool\right),\mathrm{range}\left(\mathrm{stateThread}\left(A\right)\right)=\mathrm{univ}\left(\mathrm{InverseThread}\left(A\right)\right)\wedge \ker \left(\mathrm{stateThread}\left(A\right)\right)\ne \mathrm{diagonal}\left(Bool\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/RefinementGeometry/LocalGlobalAtlasExactness.local_global_atlas_exactness (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every refinement system, stateThread is the canonical map from a global state to its compatible inverse-limit thread. Its kernel being diagonal is the separation clause; its range being all threads is the gluing clause.

Bijectivity is equivalent to the conjunction of those exact kernel and range statements. The theorem exposes the canonical map directly.

Two explicit refinement systems on Bool establish logical independence: one has diagonal kernel but non-full range, and one has full range but non-diagonal kernel.

References

• Truth anchor: D5/S3/ConceptDynamics/RefinementGeometry/LocalGlobalAtlasExactness.local_global_atlas_exactness
• Dependency: D5/S3/ConceptDynamics/RefinementGeometry/InverseLimitCompletion