Local Descent and Global Gluing Compatibility

Abstract

Finite local descent requires separate transition, inverse-limit image, and cocycle checks before it becomes a compatible global descent.

Definition 1.1 (Natural numbers form a tower of finite truncations).

$$\forall n,\mathrm{Coordinate}\left(truncatedNaturalSystem,n\right)=\mathrm{Fin}\left(n+1\right),\forall x\in \mathbb{N},\mathrm{readout}\left(truncatedNaturalSystem,n,x\right)=\min \left(x,n\right),\forall y\in \mathrm{Fin}\left(n+2\right),\mathrm{restrict}\left(truncatedNaturalSystem,n,y\right)=\min \left(y,n\right).$$

Formalization. D5/S3/ConceptDynamics/Gluing/LocalDescentGlobalCompatibility.truncatedNaturalSystem (✓ std3).

Source. Repository-derived.

Commentary.

At level n the coordinate carrier is Fin(n+1). A natural number is read as its minimum with n, and restriction to the preceding level truncates once more. The minimum identities supply the transition laws.

Definition 1.2 (The maximal finite coordinates form a compatible thread).

$$\forall n\in \mathbb{N},\mathrm{escapingThread}\left(n\right)=n.$$

Formalization. D5/S3/ConceptDynamics/Gluing/LocalDescentGlobalCompatibility.escapingThread (✓ std3).

Source. Repository-derived.

Commentary.

The thread selects the largest element n at level n. Restriction sends the largest element at level n+1 to the largest element at level n.

Lemma 1.3 (Every finite truncation is realized).

$$\forall n\in \mathbb{N},\mathrm{Surjective}\left(\mathrm{readout}\left(truncatedNaturalSystem,n\right)\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Gluing/LocalDescentGlobalCompatibility.every_finite_readout_is_surjective (✓ std3). ∎

Source. Repository-derived.

Commentary.

A coordinate y in Fin(n+1) is realized by the natural number y itself, because truncating y at n leaves it unchanged.

Lemma 1.4 (The compatible maximal thread has no global realization).

$$escapingThread\neg \in \mathrm{range}\left(\mathrm{stateThread}\left(truncatedNaturalSystem\right)\right).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Gluing/LocalDescentGlobalCompatibility.escaping_thread_not_in_global_image (✓ std3). ∎

Source. Repository-derived.

Commentary.

If a natural number x realized the thread, its coordinate at level x+1 would have to equal both x and x+1. Thus levelwise realizability does not imply membership in the global state-thread image.

Theorem 1.5 (Local closure leaves three global gluing obligations).

$$[\forall c,\mathrm{incompatibleWitnessLocalValue}\left(c,\mathrm{witnessAtomSupport}\left(c\right)\right)=1\wedge \mathrm{IsContextwiseAdditive}\left(witnessEventSupport,IsDisjointUnion,incompatibleWitnessLocalValue\right)\wedge \neg \exists globalValue:\mathrm{CoveredEvent}\left(witnessEventSupport\right)\to \mathbb{R},\mathrm{RestrictsToContexts}\left(witnessEventSupport,incompatibleWitnessLocalValue,globalValue\right)]\wedge [\forall n,\mathrm{Surjective}\left(\mathrm{readout}\left(truncatedNaturalSystem,n\right)\right)\wedge escapingThread\neg \in \mathrm{range}\left(\mathrm{stateThread}\left(truncatedNaturalSystem\right)\right)]\wedge [\forall Index,Base,UnitGroup:\mathrm{Type},[\mathrm{Group}\left(UnitGroup\right)],overlap:Index\to Index\to Base\to \mathrm{Prop},transition:Index\to Index\to Base\to UnitGroup,(\exists globalFrameCoefficients:Index\to Base\to UnitGroup,\forall i,j,x,\mathrm{overlap}\left(i,j,x\right)\Rightarrow \mathrm{globalFrameCoefficients}\left(i,x\right)=\mathrm{transition}\left(i,j,x\right)\cdot \mathrm{globalFrameCoefficients}\left(j,x\right))⟺(\exists localUnit:Index\to Base\to UnitGroup,\forall i,j,x,\mathrm{overlap}\left(i,j,x\right)\Rightarrow \mathrm{transition}\left(i,j,x\right)=\mathrm{inverse}\left(\mathrm{localUnit}\left(i,x\right)\right)\cdot \mathrm{localUnit}\left(j,x\right))].$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Gluing/LocalDescentGlobalCompatibility.local_descent_requires_global_gluing_checks (✓ std3). ∎

Source. Repository-derived.

Commentary.

The first public clause reuses the frozen two-chart witness: each chart is normalized and additive, but disagreement on their shared event precludes a global restriction. This is an explicit local-to-global countermodel, not a converse hidden in a premise.

The second clause exposes the independent inverse-limit image check via the finite truncation tower. The third reuses the frozen criterion that transition-compatible global coefficients exist exactly when the unit-valued transition cocycle is a coboundary.

References

• Truth anchor: D5/S3/ConceptDynamics/Gluing/LocalDescentGlobalCompatibility.escapingThread
• Truth anchor: D5/S3/ConceptDynamics/Gluing/LocalDescentGlobalCompatibility.escaping_thread_not_in_global_image
• Truth anchor: D5/S3/ConceptDynamics/Gluing/LocalDescentGlobalCompatibility.every_finite_readout_is_surjective
• Truth anchor: D5/S3/ConceptDynamics/Gluing/LocalDescentGlobalCompatibility.local_descent_requires_global_gluing_checks
• Truth anchor: D5/S3/ConceptDynamics/Gluing/LocalDescentGlobalCompatibility.truncatedNaturalSystem
• Dependency: D5/S3/ConceptDynamics/Gluing/GlobalFrameCoboundaryCriterion
• Dependency: D5/S3/ConceptDynamics/RefinementGeometry/InverseLimitCompletion
• Dependency: D5/S3/QuantumContext/PublicLedgerDescent