TauLib · API Book V

TauLib.BookV.Temporal.BaseCircle

TauLib.BookV.Temporal.BaseCircle

The base circle τ¹: the compact profinite temporal substrate generated by the α-orbit, with proper time, causal ordering, and geodesic duration.

Registry Cross-References

  • [V.D15] Base Circle — BaseCircle

  • [V.D16] Alpha-Tick — AlphaTick

  • [V.D17] Proper Time Series — ProperTimeSeries

  • [V.T08] Physical Time is Derived — physical_time_derived

  • [V.P03] Temporal Direction — temporal_direction

  • [V.D18] Causal Ordering — structural (wraps ProtoTime ordering)

  • [V.T09] Causal Ordering Structurally Enforced — causal_ordering_enforced

  • [V.D19] Geodesic Duration — GeodesicDuration

  • [V.T10] Total Proper Time Finite — total_proper_time_bounded

Mathematical Content

Base Circle τ¹ [V.D15]

The base circle τ¹ is the compact profinite space generated by the α-orbit. It is the temporal axis of τ³ = τ¹ ×_f T². Unlike S¹ (which has metric structure), τ¹ has only:

  • Profinite ordering (from refinement tower levels)

  • Causal direction (from α-orbit generation direction)

  • Accumulated arc length (proper time)

Alpha-Tick [V.D16]

An alpha-tick Δ_n is the passage from α_n to α_{n+1} in the refinement tower. Each tick is a single refinement step, the minimal temporal unit. Physical time emerges as accumulated arc length of the tick sequence.

Proper Time [V.D17]

Proper time t(n) is the accumulated arc length along the α-orbit up to depth n. Each tick contributes a decrement proportional to ι_τ^n (deeper ticks are shorter), making the total finite:

t_∞ = Σ_n ι_τ^n = ι_τ/(1 − ι_τ) < ∞

Causal Ordering [V.D18, V.T09]

The ordering α_m < α_n (for m < n) is not postulated but structurally forced by the refinement tower: deeper levels refine shallower ones, and refinement is irreversible (structural arrow of time).

Ground Truth Sources

  • Book V Part II (2nd Edition): Temporal Foundation

  • Book IV Chapter 3: Refinement Tower

Tau.BookV.Temporal.BaseCircle

source structure Tau.BookV.Temporal.BaseCircle :Type

[V.D15] The base circle τ¹: compact profinite space generated by the α-orbit. This is the temporal axis of τ³ = τ¹ ×_f T².

Key properties:

  • Generated by the α-generator (gravity/temporal sector)

  • Profinite: inverse limit of finite quotients

  • Carries causal ordering (from refinement tower directedness)

  • NOT S¹ with metric — profinite ordering only

  • seed : Kernel.Generator The seed generator (must be alpha for temporal).

  • seed_is_alpha : self.seed = Kernel.Generator.alpha Seed is alpha.

  • profinite : BookIV.Arena.ProfiniteLimit Reference to the profinite limit structure.

  • seed_consistent : self.profinite.seed = self.seed Profinite limit uses the same seed.

Instances For

Tau.BookV.Temporal.canonical_base_circle

source def Tau.BookV.Temporal.canonical_base_circle :BaseCircle

The canonical base circle from the α-orbit. Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookV.Temporal.AlphaTick

source structure Tau.BookV.Temporal.AlphaTick :Type

[V.D16] Alpha-tick: the minimal temporal passage from depth n to depth n+1 in the refinement tower.

Δ_n := (α_n → α_{n+1})

Each tick is a single irreversible refinement step. The source depth must be strictly less than the target depth.

  • source : BookIV.Arena.ProtoTime Source proto-time (earlier).

  • target : BookIV.Arena.ProtoTime Target proto-time (later).

  • consecutive : self.target.tick = self.source.tick + 1 Target is exactly one step after source.

Instances For

Tau.BookV.Temporal.instReprAlphaTick.repr

source def Tau.BookV.Temporal.instReprAlphaTick.repr :AlphaTick → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookV.Temporal.instReprAlphaTick

source instance Tau.BookV.Temporal.instReprAlphaTick :Repr AlphaTick

Equations

  • Tau.BookV.Temporal.instReprAlphaTick = { reprPrec := Tau.BookV.Temporal.instReprAlphaTick.repr }

Tau.BookV.Temporal.alpha_tick_at

source **def Tau.BookV.Temporal.alpha_tick_at (n : ℕ)

(hn : n > 0) :AlphaTick**

Construct an alpha-tick from a depth n (tick n → tick n+1). Equations

  • Tau.BookV.Temporal.alpha_tick_at n hn = { source := { tick := n, tick_pos := hn }, target := { tick := n + 1, tick_pos := ⋯ }, consecutive := ⋯ } Instances For

Tau.BookV.Temporal.alpha_tick_causal

source theorem Tau.BookV.Temporal.alpha_tick_causal (t : AlphaTick) :t.source.tick < t.target.tick

Alpha-ticks preserve the causal direction (source < target).

Tau.BookV.Temporal.ProperTimeSeries

source structure Tau.BookV.Temporal.ProperTimeSeries :Type

[V.D17] Proper time series: accumulated arc length along the α-orbit.

Each tick contributes a decrement proportional to the depth: the deeper the tick, the shorter the time increment. At the rational-approximation level, tick n contributes ι_τ^n.

The total proper time is finite: Σ ι_τ^n = ι_τ/(1−ι_τ) < ∞.

We store the accumulated time as a Nat pair (numer, denom).

  • depth : ℕ Current depth (how many ticks accumulated).

  • depth_pos : self.depth > 0 Depth is positive (at least one tick).

  • time_numer : ℕ Accumulated proper time numerator.

  • time_denom : ℕ Accumulated proper time denominator.

  • denom_pos : self.time_denom > 0 Denominator is positive.

Instances For

Tau.BookV.Temporal.instReprProperTimeSeries.repr

source def Tau.BookV.Temporal.instReprProperTimeSeries.repr :ProperTimeSeries → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookV.Temporal.instReprProperTimeSeries

source instance Tau.BookV.Temporal.instReprProperTimeSeries :Repr ProperTimeSeries

Equations

  • Tau.BookV.Temporal.instReprProperTimeSeries = { reprPrec := Tau.BookV.Temporal.instReprProperTimeSeries.repr }

Tau.BookV.Temporal.ProperTimeSeries.toFloat

source def Tau.BookV.Temporal.ProperTimeSeries.toFloat (t : ProperTimeSeries) :Float

Proper time as Float. Equations

  • t.toFloat = Float.ofNat t.time_numer / Float.ofNat t.time_denom Instances For

Tau.BookV.Temporal.physical_time_derived

source theorem Tau.BookV.Temporal.physical_time_derived :(∃ (t : BookIV.Arena.ProtoTime), t.tick > 0) ∧ ∀ (n : ℕ), ∃ (t : BookIV.Arena.ProtoTime), BookIV.Arena.prototime_to_nat t = n

[V.T08] Physical time is a DERIVED quantity: it emerges from the refinement tower ordering and accumulated arc length, NOT from a postulated spacetime manifold.

The derivation path:

  • α-orbit generates refinement tower levels

  • Tower levels carry structural ordering (earlier < later)

  • Each tick contributes proper-time increment

  • Accumulated arc length = physical time

This theorem records that the ProtoTime ordering precedes and generates the proper time series.

Tau.BookV.Temporal.temporal_direction

source theorem Tau.BookV.Temporal.temporal_direction :canonical_base_circle.seed = Kernel.Generator.alpha ∧ canonical_base_circle.profinite.seed = Kernel.Generator.alpha

[V.P03] Temporal direction: the generative direction of the α-orbit defines the arrow of time. Deeper refinement levels are “later.”

The alpha generator uniquely determines this direction:

  • seed = .alpha (gravity/temporal sector)

  • Profinite limit is directed (from structural arrow)

  • Direction is irreversible (from tower monotonicity)

Tau.BookV.Temporal.causal_ordering_enforced

source **theorem Tau.BookV.Temporal.causal_ordering_enforced (t1 t2 : BookIV.Arena.ProtoTime)

(h : t1 < t2) :t2.tick > t1.tick**

[V.T09] Causal ordering is structurally enforced: no axiom needed. Wraps structural_arrow from RefinementTower with Book V interpretation.

The structural arrow of time is built into the refinement tower — it is not an additional postulate but a consequence of tower directedness.

Tau.BookV.Temporal.causal_transitive

source **theorem Tau.BookV.Temporal.causal_transitive (t1 t2 t3 : BookIV.Arena.ProtoTime)

(h12 : t1 < t2)

(h23 : t2 < t3) :t1 < t3**

Causal ordering is transitive.

Tau.BookV.Temporal.causal_irreflexive

source theorem Tau.BookV.Temporal.causal_irreflexive (t : BookIV.Arena.ProtoTime) :¬t < t

Causal ordering is irreflexive.

Tau.BookV.Temporal.GeodesicDuration

source structure Tau.BookV.Temporal.GeodesicDuration :Type

[V.D19] Geodesic duration between two proto-time events: the number of alpha-ticks separating them.

This is the structural (pre-metric) distance on τ¹. The physical proper time requires weighting each tick by the depth-dependent arc-length contribution.

  • start : BookIV.Arena.ProtoTime Start event.

  • stop : BookIV.Arena.ProtoTime End event.

  • causal : self.start.tick < self.stop.tick End is after start.

Instances For

Tau.BookV.Temporal.instReprGeodesicDuration

source instance Tau.BookV.Temporal.instReprGeodesicDuration :Repr GeodesicDuration

Equations

  • Tau.BookV.Temporal.instReprGeodesicDuration = { reprPrec := Tau.BookV.Temporal.instReprGeodesicDuration.repr }

Tau.BookV.Temporal.instReprGeodesicDuration.repr

source def Tau.BookV.Temporal.instReprGeodesicDuration.repr :GeodesicDuration → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookV.Temporal.GeodesicDuration.tick_count

source def Tau.BookV.Temporal.GeodesicDuration.tick_count (g : GeodesicDuration) :ℕ

Number of ticks in the geodesic duration. Equations

  • g.tick_count = g.stop.tick - g.start.tick Instances For

Tau.BookV.Temporal.geodesic_positive

source theorem Tau.BookV.Temporal.geodesic_positive (g : GeodesicDuration) :g.tick_count > 0

Tick count is always positive.

Tau.BookV.Temporal.total_proper_time_bounded

source theorem Tau.BookV.Temporal.total_proper_time_bounded :BookIV.Sectors.iota < BookIV.Sectors.iotaD ∧ BookIV.Sectors.iota < BookIV.Sectors.iotaD - BookIV.Sectors.iota

[V.T10] Total proper time t_∞ is finite.

The proper time series is a geometric sum: t_∞ = Σ_{n≥1} ι_τ^n = ι_τ/(1−ι_τ) < ∞

Since ι_τ ≈ 0.341304 < 1, the series converges. Limit = ι_τ/(1−ι_τ) ≈ 0.518441.

We prove the bound: iota < iotaD (i.e. ι_τ < 1), which is the convergence condition for the geometric series.