Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Sparse Window Fibres

Abstract

The geometry of sparse Fibonacci window labels on the circle.

Definition 1.1 (Time tuple fibres).

Lean statement: D5/S3/Arith/FibonacciAtomic/SparseWindowFiberGeometry.fiber

Formalization. D5/S3/Arith/FibonacciAtomic/SparseWindowFiberGeometry.fiber (✓ std3).

Source. Repository-derived.

Commentary.

A time tuple fibre is the intersection of the window arcs translated back by their retained observation times. The regular domain removes precisely the translated window cuts.

Definition 1.2 (The regular circle domain).

Lean statement: D5/S3/Arith/FibonacciAtomic/SparseWindowFiberGeometry.regularDomain

Formalization. D5/S3/Arith/FibonacciAtomic/SparseWindowFiberGeometry.regularDomain (✓ std3).

Source. Repository-derived.

Commentary.

For each width and finite set of observation times, the regular domain is the circle with the images of all translated cut indices removed.

Theorem 1.3 (Fibres and connected components).

Lean statement: D5/S3/Arith/FibonacciAtomic/SparseWindowFiberGeometry.sparse_window_fiber_geometry

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/SparseWindowFiberGeometry.sparse_window_fiber_geometry (✓ std3). ∎

Source. Repository-derived.

Commentary.

For width at least two and a nonempty finite set of times, every nonempty tuple fibre equals a connected component of the regular domain. A component determines its tuple uniquely, and each regular point has one tuple. The number of distinct circle cuts equals the number of their natural indices. Every nonempty fibre contains a golden phase with natural index above any given bound. The regular domain has exactly as many connected components as cut indices. The actual natural tuple labels have this same cardinality. Natural digit rows and rotation phases agree through the canonical natural row phase and cylinder arc identities. Sorting real lifts of the finite cut set gives one nonempty open interval after each cut, including the last interval ending at the chart seam. These disjoint intervals cover the regular domain and count its connected components.

References

  • Truth anchor: D5/S3/Arith/FibonacciAtomic/SparseWindowFiberGeometry.fiber
  • Truth anchor: D5/S3/Arith/FibonacciAtomic/SparseWindowFiberGeometry.regularDomain
  • Truth anchor: D5/S3/Arith/FibonacciAtomic/SparseWindowFiberGeometry.sparse_window_fiber_geometry
  • Dependency: D5/S1/Digit/Infinite/SparseWindowMutualDetermination
  • Dependency: D5/S1/Phase/Basic