Transversal Fixed Point

Abstract

A coherent family of states across semiconjugate world models forms a transversal fixed point whenever one anchor state is fixed.

Theorem 1.1 (Transport From Fixed Is Fixed).

$\forall I n d e x : T y p e, m o d e l : W or l d M o d e l D ia g r am I n d e x, an c h or : I n d e x, s t a t e : m o d e l . St a t e an c h or, (F u n c t i o n . I s F i x e d Pt (m o d e l . s t e p an c h or) s t a t e) \Rightarrow (m o d e l . I s F i x e d S ec t i o n (m o d e l . t r an s p or tF ro man c h ors t a t e)) .$

Proof. Machine-checked in Lean as D5/S3/Observer/WorldModel/TransversalFixedPoint.transport_from_fixed_is_fixed (✓ std3). ∎

Source. Repository-derived.

Commentary.

A fixed anchor transports to a fixed state in every target world model.

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

Theorem 1.2 (Coherent Section Fixed From Anchor).

$\forall I n d e x : T y p e, m o d e l : W or l d M o d e l D ia g r am I n d e x, s t a t e : m o d e l . S ec t i o n, an c h or : I n d e x, (m o d e l . I s C o h ere n tS ec t i o n s t a t e) \land (F u n c t i o n . I s F i x e d Pt (m o d e l . s t e p an c h or) (s t a t e an c h or)) \Rightarrow (m o d e l . I s F i x e d S ec t i o n s t a t e) .$

Proof. Machine-checked in Lean as D5/S3/Observer/WorldModel/TransversalFixedPoint.coherent_section_fixed_from_anchor (✓ std3). ∎

Source. Repository-derived.

Commentary.

A coherent section that is fixed at one anchor is fixed in every model.

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

Theorem 1.3 (Fixed At Anchor iff Fixed At Target Of Injective).

$\forall I n d e x : T y p e, m o d e l : W or l d M o d e l D ia g r am I n d e x, s t a t e : m o d e l . S ec t i o n, an c h or : I n d e x, t a r g e t : I n d e x, (m o d e l . I s C o h ere n tS ec t i o n s t a t e) \land (F u n c t i o n . I nj ec t i v e (m o d e l . b r i d g e an c h or t a r g e t)) \Rightarrow (F u n c t i o n . I s F i x e d Pt (m o d e l . s t e p an c h or) (s t a t e an c h or) \Leftrightarrow F u n c t i o n . I s F i x e d Pt (m o d e l . s t e pt a r g e t) (s t a t e t a r g e t)) .$

Proof. Machine-checked in Lean as D5/S3/Observer/WorldModel/TransversalFixedPoint.fixed_at_anchor_iff_fixed_at_target_of_injective (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a coherent section, fixedness at any two anchors is equivalent when the bridge in one direction is injective.

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/WorldModel/TransversalFixedPoint.coherent_section_fixed_from_anchor
Truth anchor: D5/S3/Observer/WorldModel/TransversalFixedPoint.fixed_at_anchor_iff_fixed_at_target_of_injective
Truth anchor: D5/S3/Observer/WorldModel/TransversalFixedPoint.transport_from_fixed_is_fixed
Dependency: D5/S3/Observer/Bridges/FixedPointSemiconjugacy

Keyboard shortcuts

trureturing Blueprint

Transversal Fixed Point

Abstract

References