Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Configurations and rooted transport

Abstract

Configuration ideal completion, actual finite edge composition and invertible graph transport.

Definition 1.1 (Finite configurations form an ideal basis).

Formalization. D5/S3/ConceptDynamics/Fibers/ConfigurationPathTransport.configurationIdealIso (✓ std3).

Source. Repository-derived.

Acknowledgement. Glynn Winskel (1987). Event Structures. URL: https://www.cl.cam.ac.uk/~gw104/Winskel1987_Chapter_EventStructures.pdf.

Commentary.

A configuration is a lower set whose finite subsets are compatible. Each principal predecessor set is finite, while the ambient poset may be infinite. A nonempty directed family has a compatible lower union: every finite test set lies in one member by finite induction on directedness. The finite subconfigurations of any configuration are nonempty, lower closed and directed. Their union is the configuration because each event lies in its finite principal predecessor set. An ideal is sent to its union; any finite subconfiguration of that union belongs to the ideal by a finite upper-bound argument. These constructions are inverse and preserve inclusion. Empty compatibility supplies the bottom finite configuration.

Theorem 1.2 (Positive histories and finite observer clocks).

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Fibers/ConfigurationPathTransport.finite_history_clocks (✓ std3). ∎

Source. Repository-derived.

Commentary.

For C contained in D contained in B, the actual basic-edge schedule from C to D exists and has exactly |D minus C| steps. Every legal path with those endpoints has this same length. These gap cardinalities add across the nested triple. The finite observer clock sums only observed events with strictly positive weights: inclusion cannot decrease it, and any newly observed event makes it strictly larger. If a reverse execution from D to C exists, the forward history is empty. Replacing one event by a list of pieces preserves duration exactly when the original weight equals the sum of the piece weights. No infinite configuration sum is asserted to be a finite real number.

Theorem 1.3 (Actual edge diamonds determine finite path composites).

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Fibers/ConfigurationPathTransport.pathIndependent_iff_diamondCompatible (✓ std3). ∎

Source. Repository-derived.

Commentary.

The path map is recursively the composite of actual edge maps. The diamond hypothesis concerns only the two legal edge composites, without an assumed surrounding-path interchange. At finite endpoints the frozen EnabledPathSwapConnectivity theorem is applied to the finite endpoint subtype, then lifted back to the arbitrary ambient poset. Adjacent incomparable swaps connect all legal schedules. Equality on each local diamond therefore propagates through prefixes and suffixes. Conversely the two length-two paths give each diamond. ConfigurationReadout restricts this result faithfully to the original fibres defined only at legal configurations.

Theorem 1.4 (Parallel sections correspond to closed-walk fixed points).

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Fibers/ConfigurationPathTransport.rootSectionMap_bijective (✓ std3). ∎

Source. Repository-derived.

Commentary.

Walk transports are constructed recursively from bijective oriented edge maps; reversal uses the given inverse edge maps, and concatenation follows by induction. A root point fixed by every closed walk transports consistently to a parallel section along chosen root paths. Comparing two paths forms a closed walk and proves independence. Evaluation at the root is the inverse map. No claim that a loop operator is the identity is needed: it must fix the chosen root point.

Theorem 1.5 (Tree coordinates make the reversible edge maps identity).

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Fibers/ConfigurationPathTransport.tree_coordinate_trivialization (✓ std3). ∎

Source. Repository-derived.

Commentary.

The unique simple root path gives the fibre coordinate at every vertex. Tree path uniqueness and edge reversal imply that every transported edge is the identity on the root fibre. The original walk and every literal edge occurrence are unchanged by this coordinate construction. Inverse transport is an algebraic operation on fibre values; it is not a deletion edge in the positive history relation.

References