Wormhole Category

Abstract

Typed semiconjugate bridges compose and transport fixed behavior.

Theorem 1.1 (Identity Compose).

$\forall so u rce : Dy nami c a l W or l d, t a r g e t : Dy nami c a l W or l d, b r i d g e : W or mh o l eso u rce t a r g e t, (co m p ose (i d e n t i t y t a r g e t) b r i d g e = b r i d g e) .$

Proof. Machine-checked in Lean as D5/S3/Observer/Bridges/WormholeCategory.identity_compose (✓ std3). ∎

Source. Repository-derived.

Commentary.

Left identity for wormhole composition.

The declaration keeps its parameters and hypotheses explicit; the result makes no converse or broader existence claim beyond that scope.

Theorem 1.2 (Compose Identity).

$\forall so u rce : Dy nami c a l W or l d, t a r g e t : Dy nami c a l W or l d, b r i d g e : W or mh o l eso u rce t a r g e t, (co m p ose b r i d g e (i d e n t i t yso u rce) = b r i d g e) .$

Proof. Machine-checked in Lean as D5/S3/Observer/Bridges/WormholeCategory.compose_identity (✓ std3). ∎

Source. Repository-derived.

Commentary.

Right identity for wormhole composition.

The declaration keeps its parameters and hypotheses explicit; the result makes no converse or broader existence claim beyond that scope.

Theorem 1.3 (Compose Assoc).

$\forall so u rce : Dy nami c a l W or l d, mi dd l e : Dy nami c a l W or l d, t a r g e t : Dy nami c a l W or l d, f o u r t h : Dy nami c a l W or l d, t hi r d : W or mh o l e t a r g e t f o u r t h, seco n d : W or mh o l e mi dd l e t a r g e t, f i rs t : W or mh o l eso u rce mi dd l e, (co m p ose t hi r d (co m p oseseco n df i rs t) = co m p ose (co m p ose t hi r d seco n d) f i rs t) .$

Proof. Machine-checked in Lean as D5/S3/Observer/Bridges/WormholeCategory.compose_assoc (✓ std3). ∎

Source. Repository-derived.

Commentary.

Associativity of wormhole composition.

The declaration keeps its parameters and hypotheses explicit; the result makes no converse or broader existence claim beyond that scope.

Theorem 1.4 (Maps Fixed Point).

$\forall so u rce : Dy nami c a l W or l d, t a r g e t : Dy nami c a l W or l d, b r i d g e : W or mh o l eso u rce t a r g e t, s t a t e : so u rce . St a t e, (F u n c t i o n . I s F i x e d Pt so u rce . s t e p s t a t e) \Rightarrow (F u n c t i o n . I s F i x e d Ptt a r g e t . s t e p (b r i d g e . ma p s t a t e)) .$

Proof. Machine-checked in Lean as D5/S3/Observer/Bridges/WormholeCategory.maps_fixed_point (✓ std3). ∎

Source. Repository-derived.

Commentary.

A wormhole transports every fixed source state to a fixed target state.

The declaration keeps its parameters and hypotheses explicit; the result makes no converse or broader existence claim beyond that scope.

Theorem 1.5 (Maps Iterate).

$\forall so u rce : Dy nami c a l W or l d, t a r g e t : Dy nami c a l W or l d, b r i d g e : W or mh o l eso u rce t a r g e t, i t er a t i o n : N, s t a t e : so u rce . St a t e, (b r i d g e . ma p ((so u rce . s t e p^{[i t er a t i o n]}) s t a t e) = (t a r g e t . s t e p^{[i t er a t i o n]}) (b r i d g e . ma p s t a t e)) .$

Proof. Machine-checked in Lean as D5/S3/Observer/Bridges/WormholeCategory.maps_iterate (✓ std3). ∎

Source. Repository-derived.

Commentary.

A wormhole transports every finite iterate of the source dynamics.

The declaration keeps its parameters and hypotheses explicit; the result makes no converse or broader existence claim beyond that scope.

Theorem 1.6 (Composite Maps Fixed Point).

$\forall so u rce : Dy nami c a l W or l d, mi dd l e : Dy nami c a l W or l d, t a r g e t : Dy nami c a l W or l d, seco n d : W or mh o l e mi dd l e t a r g e t, f i rs t : W or mh o l eso u rce mi dd l e, s t a t e : so u rce . St a t e, (F u n c t i o n . I s F i x e d Pt so u rce . s t e p s t a t e) \Rightarrow (F u n c t i o n . I s F i x e d Ptt a r g e t . s t e p ((co m p oseseco n df i rs t) . ma p s t a t e)) .$

Proof. Machine-checked in Lean as D5/S3/Observer/Bridges/WormholeCategory.composite_maps_fixed_point (✓ std3). ∎

Source. Repository-derived.

Commentary.

Composite wormholes transport fixed points across multiple worlds.

The declaration keeps its parameters and hypotheses explicit; the result makes no converse or broader existence claim beyond that scope.

References

Truth anchor: D5/S3/Observer/Bridges/WormholeCategory.compose_assoc
Truth anchor: D5/S3/Observer/Bridges/WormholeCategory.compose_identity
Truth anchor: D5/S3/Observer/Bridges/WormholeCategory.composite_maps_fixed_point
Truth anchor: D5/S3/Observer/Bridges/WormholeCategory.identity_compose
Truth anchor: D5/S3/Observer/Bridges/WormholeCategory.maps_fixed_point
Truth anchor: D5/S3/Observer/Bridges/WormholeCategory.maps_iterate
Dependency: D5/S3/Observer/Bridges/FixedPointSemiconjugacy

Keyboard shortcuts

trureturing Blueprint

Wormhole Category

Abstract

References