Pith. sign in
module module moderate

IndisputableMonolith.Foundation.RS_Arrow_Of_Time

show as:
view Lean formalization →

Formalizes the Recognition Science arrow of time as a non-negative domain cost that crosses a positive canonical threshold. Physicists citing the thermodynamic or causal direction in RS units will use the certificate bundle. The module packages cost non-negativity, threshold positivity, and an inhabited certificate rather than a deep derivation.

claimIn RS-native units the domain cost $C$ is non-negative, equals a fixed evaluation at the identity, and the canonical threshold $\theta>0$ is positive. An arrow-of-time certificate asserts $C\ge 0$ together with $\theta>0$, and such a certificate is inhabited.

background

Recognition Science treats time as discrete ticks with fundamental quantum $\tau_0=1$ (from Constants). The Cost import supplies the J-cost $J(x)=(x+x^{-1})/2-1$, the unique generator of the Recognition Composition Law, which measures departure from equilibrium on the positive reals.

This module lifts that scalar cost to a domain-level cost functional. The domain cost is required to be non-negative and to match a canonical evaluation; a positive threshold then marks the irreversible crossing that defines a preferred time direction. The local setting is foundational: no spacetime metric or statistical ensemble is assumed, only the cost and the tick quantum.

Sibling definitions package the cost, its non-negativity, the threshold and its positivity, then wrap them in an RSArrowOfTimeCert structure with an inhabited instance.

proof idea

Definition-and-certificate module. Non-negativity of the domain cost and positivity of the canonical threshold are recorded as lemmas (likely thin wrappers on Cost facts). The certificate structure bundles those facts; inhabitance is a one-line constructor application. No multi-step forcing argument appears here.

why it matters in Recognition Science

Supplies the formal arrow-of-time certificate used when later layers need a preferred temporal orientation without importing thermodynamics by hand. It sits in Foundation beside the forcing chain (T0–T8) and the eight-tick octave: once cost is non-negative and a positive threshold exists, irreversible advance along ticks is certified. Downstream use is not yet wired in this graph (used_by empty), so the module is a self-contained cert provider rather than a lemma inside a larger proved theorem. It does not itself derive the second law; it only packages the cost-threshold pair that later arguments may cite.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)